/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | closure.sml | 20 fun trav t = function 25 (v, mk_comb(inst[alpha |-> type_of M] fun_tm,trav M),trav N)) M 26 else mk_plet (v, trav M, trav N) 30 mk_cond (J, trav M, trav N) 34 mk_pabs (trav M, trav N) end 37 trav t 60 fun trav t = function 81 fun trav t = function [all...] |
H A D | basic.sml | 199 fun trav t = function 202 in trav N end 205 val t1 = trav M1 206 val t2 = trav M2 216 let val (M,N) = dest_pabs t in trav N end 223 valOf (trav t) 235 let fun trav M = function 236 if is_plet M then trav (#1 (dest_plet M)) 237 else if is_comb M then trav (#2 (dest_comb M)) 238 else if is_pair M then trav (# [all...] |
H A D | funcCall.sml | 180 (* Function "trav" traverses a term and adds pre-call saving and post-call saving instructions 185 fun trav t output = function 188 val (M', _) = trav M NONE 194 val (N', output') = trav N output 201 let val (N', output') = trav N output 205 let val (N', output') = trav N output 210 val (M1', output1) = trav M1 output 211 val (M2', output2) = trav M2 output1 221 val (N', _) = trav N NONE 238 val (body', _) = trav bod [all...] |
H A D | refine.sml | 193 fun trav t = function 196 val N' = trav N 199 val M1' = mk_flat_let (v, trav M1, N') 200 val M2' = mk_flat_let (v, trav M2, N') 203 mk_flat_let(v, trav M, trav N) 207 val M1' = trav M1 208 val M2' = trav M2 213 in mk_pabs(v,trav M) 218 val fbody' = trav fbod [all...] |
H A D | inline.sml | 35 fun trav t = function 40 else trav M 41 in mk_plet (v, M', trav N) 45 trav tm
|
H A D | Normal.sml | 303 fun trav t = function 309 trav M (* to be revised *) 310 else trav M 311 in mk_plet (v, M', trav N) 315 val M1' = trav M1 316 val M2' = trav M2 321 in mk_pabs(v,trav M) 325 trav tm 366 fun trav M = function 369 val M1' = trav M [all...] |
H A D | regAlloc.sml | 452 fun trav t env cont = function 460 val N' = trav N env' cont 466 val N' = trav N env cont 480 mk_plet (v', trav M env' cont', trav N env' cont) 482 else mk_plet (v, trav M env cont, trav N env cont) 486 val M1' = trav M1 env cont 487 val M2' = trav M2 env cont 503 trav bod 583 let fun trav t = function [all...] |
H A D | defunctionalize.sml | 93 fun trav t = function 96 val _ = (trav M; trav N) 104 in (trav M; trav N) 108 in (trav M; trav N) 114 if is_comb M then trav M else () 117 if is_comb M then trav M else () 121 in trav [all...] |
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | LVTermNet.sml | 64 fun trav (net, tms) = function 72 NONE => trav(newnode ks, ks) 73 | SOME n => trav(n, ks) 77 | (EMPTY, ks) => trav(mkempty(), ks) 80 (trav(net,[k]), sz + 1) 85 fun trav (net, acc) = function 89 fun foldthis (k,v,acc) = trav(v,acc) 95 trav(net, []) 101 fun trav (net, tms) = function 109 | SOME n => trav( 137 fun trav acc (net, ks) = function 170 fun trav (p as (net, ks)) = function 205 fun trav n = function 222 fun trav acc n = function 242 fun trav n = function [all...] |
H A D | TypeNet.sml | 64 fun trav (net, tys) = function 72 NONE => trav(newnode tys, tys) 73 | SOME n => trav(n, tys) 78 | (EMPTY, tys) => trav(mkempty(), tys) 81 (trav(net,[ty]), sz + 1) 86 fun trav (net, acc) = function 90 fun foldthis (k,v,acc) = trav(v,acc) 96 trav(net, []) 102 fun trav (net, tys) = function 110 | SOME n => trav( 122 fun trav acc (net, tyl) = function 147 fun trav (p as (net, tyl)) = function 182 fun trav n = function 192 fun trav acc n = function 202 fun trav n = function [all...] |
H A D | LVTermNetFunctor.sml | 97 fun trav (net, tms) = function 105 NONE => trav(newnode ks, ks) 106 | SOME n => trav(n, ks) 112 (trav(net,[k]), sz + 1) 117 fun trav (net, acc) = function 121 fun foldthis (k,v,acc) = trav(v,acc) 126 trav(net, []) 132 fun trav (net, tms) = function 140 | SOME n => trav(n, rest @ ks) 144 trav(ne 167 fun trav acc (net, ks) = function 199 fun trav (p as (net, ks)) = function 233 fun trav n = function 249 fun trav acc n = function [all...] |
H A D | Preterm.sml | 712 fun trav acc t = let function 715 trav (trav acc r) l 718 trav [] t0
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Proof.C | 71 trav = NULL; 79 trav = &t; 89 if (trav != NULL) 90 trav->root(clause); 141 if (trav != NULL) 142 trav->chain(chain_id, chain_var); 164 if (trav != NULL) 165 trav->deleted(abs(gone)); 364 void Proof::traverse(ProofTraverser& trav, int& res_count, ClauseId goal) argument 392 trav [all...] |
H A D | Proof.h | 50 ProofTraverser* trav; member in class:Proof 81 void traverse (ProofTraverser& trav, int& res_count, ClauseId goal = ClauseId_NULL) ;
|
H A D | Main.C | 172 Checker trav; local 174 proof->traverse(trav, res_count, goal); 176 vec<Lit>& c = trav.clauses.last();
|
/seL4-l4v-10.1.1/HOL4/src/0/ |
H A D | Term.sig | 16 val trav : (term -> unit) -> term -> unit value
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | ACF.sml | 39 fun trav M = function 42 val M1' = trav M1 43 val M2' = trav M2 48 in mk_abs(v,trav N) 52 trav tm
|
H A D | ANF.sml | 34 fun trav M = function 37 val M1' = trav M1 38 val M2' = trav M2 43 in mk_abs(v,trav N) 47 trav tm
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Traverse.sml | 232 fun trav stack context = let function 238 EQT_ELIM (trav stack (change_relation' (context,equality)) tm) 244 trav stack (change_relation' (context,equality)) tm 266 trav stack (change_relation' (add_context' (context,thms), relation)) 296 trav stack ctxt tm
|
/seL4-l4v-10.1.1/HOL4/help/src-sml/ |
H A D | Htmlsigs.sml | 193 fun trav [] = NONE function 194 | trav({comp=Database.Term(x,SOME "HOL"),file,line}::rst) 197 else trav rst 198 | trav (_::rst) = trav rst 200 Option.map (fn x => (x, id)) (trav (lookup(db,id)))
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/zc2hs/ |
H A D | zc2hs.cpp | 173 Checker trav; local 174 proof->traverse(trav, goal); 176 vec<Lit>& c = trav.clauses.last(); 185 printf("Inferences: %d\n",trav.res_count);
|
/seL4-l4v-10.1.1/HOL4/src/coretypes/ |
H A D | pairTools.sml | 148 local fun trav tm A = function 149 trav (mk_fst tm) (trav (mk_snd tm) A) handle HOL_ERR _ => (tm::A) 153 fun TUPLE v thm = GEN v (SPECL (trav v []) thm)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | ANF.sml | 34 fun trav M = function 37 val M1' = trav M1 38 val M2' = trav M2 43 in mk_abs(v,trav N) 47 trav tm
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | ANF.sml | 34 fun trav M = function 37 val M1' = trav M1 38 val M2' = trav M2 43 in mk_abs(v,trav N) 47 trav tm
|
/seL4-l4v-10.1.1/HOL4/examples/elliptic/c_output/ |
H A D | c_outputLib.sml | 403 fun trav M = function 406 val M1' = trav M1 407 val M2' = trav M2 412 in mk_abs(v,trav N) 416 trav tm
|