Searched refs:leaves (Results 1 - 25 of 63) sorted by relevance

123

/seL4-l4v-master/isabelle/lib/browser/GraphBrowser/
H A DTreeNode.java21 Vector leaves=new Vector(10,10); field in class:TreeNode
26 leaves.addElement(new TreeNode(n,p,num));
38 Enumeration e1=leaves.elements();
49 leaves.addElement(nd);
73 for (int i=0;i<leaves.size();i++)
75 TreeNode t=((TreeNode)leaves.elementAt(i)).lookup(y);
83 if (!leaves.isEmpty()) {
95 for(int i=0;i<leaves.size();i++)
96 ((Tree)leaves.elementAt(i)).collapse();
102 Enumeration e1=leaves
[all...]
/seL4-l4v-master/l4v/isabelle/lib/browser/GraphBrowser/
H A DTreeNode.java21 Vector leaves=new Vector(10,10); field in class:TreeNode
26 leaves.addElement(new TreeNode(n,p,num));
38 Enumeration e1=leaves.elements();
49 leaves.addElement(nd);
73 for (int i=0;i<leaves.size();i++)
75 TreeNode t=((TreeNode)leaves.elementAt(i)).lookup(y);
83 if (!leaves.isEmpty()) {
95 for(int i=0;i<leaves.size();i++)
96 ((Tree)leaves.elementAt(i)).collapse();
102 Enumeration e1=leaves
[all...]
/seL4-l4v-master/HOL4/src/integer/
H A DOmegaSymbolic.sig22 as long as the leaves are relations over integer expressions.
25 leaves are relations over integer expressions), finds a quantifier
H A DOmegaMath.sig96 disjunction of two normalised <= leaves. (The latter happens if
115 where body is a conjunction of leaves, possibly including
123 where body is a conjunction of leaves, possibly including
H A DOmegaSymbolic.sml42 leaves.
481 Given a list of variables vs, and a conjunction of leaves t, pick the
569 fully normalised leaves. This function picks one of the quantifiers
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/
H A DtailrecLib.sml76 fun leaves (FUN_VAL tm) f = FUN_VAL (f tm) function
77 | leaves (FUN_COND (c,t)) f = FUN_COND (c, leaves t f)
78 | leaves (FUN_IF (a,b,c)) f = FUN_IF (a, leaves b f, leaves c f)
79 | leaves (FUN_LET (v,y,t)) f = FUN_LET (v, y, leaves t f)
101 fun leaves_inl body f1 f2 = ftree2tm (leaves (tm2ftree body) (fn tm =>
145 val pre_tm = ftree2tm (leaves (tm2ftre
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/compiler/
H A Dreg_allocLib.sml214 fun leaves (FUN_COND (_,t)) = leaves t function
215 | leaves (FUN_LET (_,_,t)) = leaves t
216 | leaves (FUN_IF (_,t1,t2)) = leaves t1 @ leaves t2
217 | leaves (FUN_VAL tm) = [tm]
218 val bases = filter (not o can (match_term lhs)) (leaves (tm2ftree rhs))
278 fun leaves (FUN_CON function
[all...]
/seL4-l4v-master/HOL4/src/boss/
H A Dselftest.sml193 val _ = tprint "Simp -* APPEND_ASSOC leaves list unchanged"
196 val _ = tprint "Simp -* list.APPEND_ASSOC leaves list unchanged"
200 val _ = tprint "Simp -* list.APPEND_ASSOC.1 leaves list unchanged"
204 val _ = tprint "Simp Excl APPEND_ASSOC leaves list unchanged"
207 val _ = tprint "Simp Excl list.APPEND_ASSOC leaves list unchanged"
213 printarg = fn _ => "simp Excl on arith d.p. leaves input unchanged",
/seL4-l4v-master/HOL4/src/real/
H A Dselftest.sml165 fn _ => "simp w/o nat d.p. but with real d.p. leaves input unchanged",
172 fn _ => "simp with nat d.p. but w/o real d.p. leaves input unchanged",
/seL4-l4v-master/HOL4/src/simp/src/
H A DboolSimps.sig50 Note that it leaves ==> alone, but includes the following
/seL4-l4v-master/HOL4/examples/bootstrap/
H A Dsource_valuesScript.sml8 leaves are natural numbers (num) *)
/seL4-l4v-master/HOL4/src/metis/
H A DmlibUseful.sml650 fun f (LEAF _) = {leaves = 1, branches = 0}
651 | f (BRANCH (_, ts)) = foldl g {leaves = 0, branches = 1} ts
652 and g (t, {leaves = l, branches = b}) =
653 let val {leaves=l', branches=b'} = f t in {leaves=l+l', branches=b+b'} end;
H A DmlibUseful.sig173 val tree_size : ('a,'b) tree -> {branches : int, leaves : int}
/seL4-l4v-master/HOL4/examples/hardware/hol88/
H A Dbinary-trees.ml91 % The next one counts the number of leaves in the tree. %
/seL4-l4v-master/HOL4/src/parse/
H A DPreterm.sig57 if the types attached to the leaves aren't valid for the kernel. *)
H A DLiteral.sml6 * difference in treatment between zero and the other numerals leaves
/seL4-l4v-master/HOL4/examples/
H A DThery.sml68 This leaves two goals. The first is easy to show.
/seL4-l4v-master/HOL4/examples/lambda/typing/
H A DcontextlistsScript.sml9 (* permutation over contexts swaps the strings and leaves the types alone *)
/seL4-l4v-master/HOL4/src/lite/
H A DliteLib.sml388 (* Apply at leaves of op-tree; NB any failures at leaves cause failure. *)
/seL4-l4v-master/HOL4/examples/miller/ho_prover/
H A DskiTools.sml209 fun add a [] leaves = LEAF a :: leaves
/seL4-l4v-master/HOL4/examples/machine-code/decompiler/
H A DdecompilerLib.sml1397 fun leaves (FUN_VAL tm) f = FUN_VAL (f tm) function
1398 | leaves (FUN_COND (c,t)) f = FUN_COND (c, leaves t f)
1399 | leaves (FUN_IF (a,b,c)) f = FUN_IF (a, leaves b f, leaves c f)
1400 | leaves (FUN_LET (v,y,t)) f = FUN_LET (v, y, leaves t f)
1596 free_vars o rm_pc o ftree2tm o leaves t)
1600 free_vars o rm_pc o ftree2tm o leaves
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw2/
H A DpatternMatch.sml20 (* leaves, executing the tests corresponding to the test nodes along the path. *)
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/
H A Dppc_astScript.sml14 It leaves out the following which don't correspond to a PowerPC instruction:
/seL4-l4v-master/HOL4/src/unwind/Manual/
H A Ddescription.tex252 Unwinding {\small\verb%l3%} then leaves us with the required recursive
475 the internal lines except for {\small\verb%l4%} can be pruned. This leaves
/seL4-l4v-master/HOL4/examples/dev/sw2/test/
H A Dtea.sml204 (* TEAEncrypt unwound a bit, but leaves some simplifications still possible *)

Completed in 176 milliseconds

123