Searched refs:trav (Results 1 - 25 of 27) sorted by relevance

12

/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/
H A Dclosure.sml20 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 Dbasic.sml199 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 DfuncCall.sml180 (* 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 Drefine.sml193 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 Dinline.sml35 fun trav t = function
40 else trav M
41 in mk_plet (v, M', trav N)
45 trav tm
H A DNormal.sml303 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 DregAlloc.sml452 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 Ddefunctionalize.sml93 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 DLVTermNet.sml64 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 DTypeNet.sml64 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 DLVTermNetFunctor.sml97 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 DPreterm.sml712 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 DProof.C71 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 DProof.h50 ProofTraverser* trav; member in class:Proof
81 void traverse (ProofTraverser& trav, int& res_count, ClauseId goal = ClauseId_NULL) ;
H A DMain.C172 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 DTerm.sig16 val trav : (term -> unit) -> term -> unit value
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/
H A DACF.sml39 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 DANF.sml34 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 DTraverse.sml232 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 DHtmlsigs.sml193 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 Dzc2hs.cpp173 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 DpairTools.sml148 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 DANF.sml34 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 DANF.sml34 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 Dc_outputLib.sml403 fun trav M = function
406 val M1' = trav M1
407 val M2' = trav M2
412 in mk_abs(v,trav N)
416 trav tm

Completed in 192 milliseconds

12