/seL4-l4v-master/HOL4/examples/l3-machine-code/lib/ |
H A D | Ptree.sml | 69 fun traverse (Empty, a) = a 70 | traverse (Leaf x, a) = x :: a 71 | traverse (Branch (p, m, l, r), a) = traverse (l, traverse (r, a)) 73 fun list_of_ptree t = traverse (t, [])
|
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | funcCall.sml | 50 fun traverse t (rS, wS) = function 53 val (rS1, wS1) = traverse M (rS, S.addList(wS, List.filter is_reg (strip_pair v))) 55 traverse N (rS1, wS1) 59 ((traverse N) o (traverse M) o (traverse J)) (rS, wS) 63 ((traverse N) o (traverse M)) (rS, wS) 67 ((traverse N) o (traverse [all...] |
H A D | monomorphisation.sml | 175 (* traverse an expression and build the instantiation map *)
|
/seL4-l4v-master/isabelle/src/Pure/PIDE/ |
H A D | xml.scala | 90 /* traverse text */ 94 def traverse(x: A, t: Tree): A = 96 case XML.Wrapped_Elem(_, _, ts) => (x /: ts)(traverse) 97 case XML.Elem(_, ts) => (x /: ts)(traverse) 100 (a /: body)(traverse)
|
H A D | markup_tree.scala | 197 def traverse( 210 val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest) 213 case None => traverse(last, (parent, subtree ::: more) :: rest) 218 val nexts = traverse(stop, rest) 228 traverse(root_range.start,
|
/seL4-l4v-master/l4v/isabelle/src/Pure/PIDE/ |
H A D | xml.scala | 90 /* traverse text */ 94 def traverse(x: A, t: Tree): A = 96 case XML.Wrapped_Elem(_, _, ts) => (x /: ts)(traverse) 97 case XML.Elem(_, ts) => (x /: ts)(traverse) 100 (a /: body)(traverse)
|
H A D | markup_tree.scala | 197 def traverse( 210 val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest) 213 case None => traverse(last, (parent, subtree ::: more) :: rest) 218 val nexts = traverse(stop, rest) 228 traverse(root_range.start,
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | Absyn.sml | 19 fun traverse applyp f t = let function 20 val traverse = traverse applyp f value 22 if applyp t then f traverse t 24 APP(locn,t1,t2) => APP(locn,traverse t1, traverse t2) 25 | LAM(locn,vs,t) => LAM(locn,vs, traverse t) 26 | TYPED(locn,t,pty) => TYPED(locn,traverse t, pty)
|
H A D | Absyn.sig | 13 val traverse : (absyn -> bool) -> value
|
H A D | Preterm.sml | 773 fun traverse acc actions = function 784 traverse acc (Input body :: Ab (v,t) :: rest) 790 traverse acc (in_args @ 794 traverse (Unch t::acc) rest 799 Ch bod' :: acc0 => traverse (Ch (mk_abs(v,bod'))::acc0) 801 | Unch _ :: acc0 => traverse (Unch orig :: acc0) rest 846 traverse (newt::acc_base) rest 848 end (* act :: rest *) (* end traverse *) 850 traverse [] [Input tm0]
|
H A D | Parse_support.sml | 65 fun traverse localbvs t e = function 91 | COMB(f,x) => traverse localbvs x (traverse localbvs f e) 92 | LAMB(bv, bod) => traverse (HOLset.add(localbvs,bv)) bod e 94 (Preterm.Antiq{Tm = tm, Locn = l}, traverse empty_tmset tm e)
|
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Proof.h | 81 void traverse (ProofTraverser& trav, int& res_count, ClauseId goal = ClauseId_NULL) ;
|
H A D | Main.C | 174 proof->traverse(trav, res_count, goal);
|
H A D | Proof.C | 364 void Proof::traverse(ProofTraverser& trav, int& res_count, ClauseId goal) function in class:Proof
|
/seL4-l4v-master/HOL4/tools/ |
H A D | make_iss.sml | 65 fun traverse worklist acc excludes = function 87 traverse newworklist ((dir,filefound)::acc) excludes 112 (filefound, List.rev (traverse ids [] excludes))
|
/seL4-l4v-master/isabelle/src/Pure/GUI/ |
H A D | gui.scala | 197 def traverse(comp: Component) 203 traverse(cont.getComponent(i)) 207 traverse(component)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/GUI/ |
H A D | gui.scala | 197 def traverse(comp: Component) 203 traverse(cont.getComponent(i)) 207 traverse(component)
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | patriciaLib.sig | 21 val traverse : term_ptree -> num list value
|
/seL4-l4v-master/HOL4/src/bool/ |
H A D | boolpp.sml | 277 traverse (fn APP(_,APP(_,IDENT (_,letstr), _), _) => letstr = let_special 280 traverse (fn IDENT(_,andstr) => andstr = and_special | _ => false) 316 traverse
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | normalFormsTest.sml | 66 fun traverse tm s = function 68 | SOME (x, y) => traverse x (traverse y s) 69 val set = traverse tm (Binaryset.empty Term.compare)
|
/seL4-l4v-master/HOL4/help/src-sml/ |
H A D | Htmlsigs.sml | 274 fun traverse process = function 285 traverse pass1; 299 traverse (pass2 (isTheorysig sigfile));
|
/seL4-l4v-master/HOL4/src/AI/machine_learning/ |
H A D | mlTreeNeuralNetwork.sml | 121 fun traverse tm = function 124 val nl = map traverse argl 129 val subtml = (app (ignore o traverse) tml; dkeys (!d))
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Traverse.sig | 2 * FILE : traverse.sig
|
H A D | Traverse.sml | 2 * FILE : traverse.sml
|
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/zc2hs/ |
H A D | zc2hs.cpp | 174 proof->traverse(trav, goal);
|