/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/adder/ |
H A D | adder.cxx | 180 int test_vector(bdd av, bdd bv, int a, int b) argument 186 bdd resv = av & bv & xout[n]; 206 bdd av = setval(a,0); local 209 if (test_vector(av,bv,a,b) == 0)
|
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | bddtest.cxx | 75 int main(int ac, char** av) argument
|
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/queen/ |
H A D | queen.cxx | 75 int main(int ac, char **av) argument 85 N = atoi(av[1]);
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibTerm.sml | 587 fun fvt av = 590 if null av then mem else (fn v => fn vs => mem v av orelse mem v vs) 601 | fv vs ((av, Atom t ) :: fms) = fv (fvt av vs [t]) fms 602 | fv vs ((av, Not p ) :: fms) = fv vs ((av, p) :: fms) 603 | fv vs ((av, And (p, q) ) :: fms) = fv vs ((av, p) :: (av, [all...] |
H A D | mlibOmega.sml | 51 fun factoid_key (ALT av) = KEY(av, V.length av - 1) 53 fun keyhash (KEY(av, len)) = khash av (SOME len) 82 fun toList (ALT av) = V.foldr op:: [] av 88 ALT av => V.sub(av, V.length av [all...] |
/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | Intmap.sml | 70 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) = 71 N(b,bv,N(a,av,x,y),z) 73 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) = 74 N(a,av,x,N(b,bv,y,z)) 76 fun double_L (a,av,w,T{key=c,value=cv,left=T{key=b,value=bv,left=x,right=y,...},right=z,...}) = 77 N(b,bv,N(a,av,w,x),N(c,cv,y,z)) 79 fun double_R (c,cv,T{key=a,value=av,left=w,right=T{key=b,value=bv,left=x,right=y,...},...},z) = 80 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
|
/seL4-l4v-master/HOL4/tools-poly/poly/ |
H A D | Binarymap.sml | 73 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) = 74 N(b,bv,N(a,av,x,y),z) 76 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) = 77 N(a,av,x,N(b,bv,y,z)) 79 fun double_L (a,av,w,T{key=c,value=cv, 82 N(b,bv,N(a,av,w,x),N(c,cv,y,z)) 84 fun double_R (c,cv,T{key=a,value=av,left=w, 86 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
|
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | int-binary-map.sml | 86 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) = 87 N(b,bv,N(a,av,x,y),z) 89 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) = 90 N(a,av,x,N(b,bv,y,z)) 92 fun double_L (a,av,w,T{key=c,value=cv,left=T{key=b,value=bv,left=x,right=y,...},right=z,...}) = 93 N(b,bv,N(a,av,w,x),N(c,cv,y,z)) 95 fun double_R (c,cv,T{key=a,value=av,left=w,right=T{key=b,value=bv,left=x,right=y,...},...},z) = 96 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | int-binary-map.sml | 86 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) = 87 N(b,bv,N(a,av,x,y),z) 89 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) = 90 N(a,av,x,N(b,bv,y,z)) 92 fun double_L (a,av,w,T{key=c,value=cv,left=T{key=b,value=bv,left=x,right=y,...},right=z,...}) = 93 N(b,bv,N(a,av,w,x),N(c,cv,y,z)) 95 fun double_R (c,cv,T{key=a,value=av,left=w,right=T{key=b,value=bv,left=x,right=y,...},...},z) = 96 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | int-binary-map.sml | 86 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) = 87 N(b,bv,N(a,av,x,y),z) 89 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) = 90 N(a,av,x,N(b,bv,y,z)) 92 fun double_L (a,av,w,T{key=c,value=cv,left=T{key=b,value=bv,left=x,right=y,...},right=z,...}) = 93 N(b,bv,N(a,av,w,x),N(c,cv,y,z)) 95 fun double_R (c,cv,T{key=a,value=av,left=w,right=T{key=b,value=bv,left=x,right=y,...},...},z) = 96 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
|
/seL4-l4v-master/HOL4/developers/mlton-srcs/ |
H A D | Binarymap.sml | 142 fun single_L (a,av,x,T{key=b,value=bv,left=y,right=z,...}) = 143 N(b,bv,N(a,av,x,y),z) 145 fun single_R (b,bv,T{key=a,value=av,left=x,right=y,...},z) = 146 N(a,av,x,N(b,bv,y,z)) 148 fun double_L (a,av,w,T{key=c,value=cv, 151 N(b,bv,N(a,av,w,x),N(c,cv,y,z)) 153 fun double_R (c,cv,T{key=a,value=av,left=w, 155 N(b,bv,N(a,av,w,x),N(c,cv,y,z))
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | OmegaMLShadow.sml | 41 ALT av => extract(av, 0, SOME (Vector.length av - 1)) 44 ALT av => Vector.sub(av, Vector.length av - 1) 47 case f of ALT av => Vector.length av 110 ALT av => Vector.foldri 114 av [all...] |
H A D | int_arithScript.sml | 826 mn | dx + bqn + vpm /\ d | av - ub ) 867 (* m | ax + b /\ n | ux + v ==> d | av - ub *) 889 (* mn | dx + vmp + bnq /\ d | av - ub ==> m | ax + b *) 949 (* mn | dx + vmp + bnq /\ d | av - ub ==> n | ux + v *)
|
/seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/examples/calculator/ |
H A D | parser.y | 210 int main(int ac, char **av) 214 while ((c=getopt(ac, av, "hg")) != EOF) 230 yyin = fopen(av[optind],"r"); 233 cerr << "Could not open file: " << av[optind] << endl;
|
/seL4-l4v-master/HOL4/src/datatype/ |
H A D | DatatypeSimps.sml | 148 val (avoid, case_args') = Lib.foldl_map (fn (av, (args, v)) => 149 let val v' = variant av v in 150 (v' :: av, (args, v')) end) (input_arg'::avoid, case_args) 445 val (_, args') = foldl_map (fn (av, v) => let val v' = variant av v in (v' :: av, v') end) (free_vars_full, args)
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | poly_specific.cpp | 395 PolyWord *av = (PolyWord*)a; local 397 if ((*av).IsTagged() || (*bv).IsTagged()) return 0; // Shouldn't happen 398 PolyObject *ao = (*av).AsObjPtr(), *bo = (*bv).AsObjPtr();
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | dbgTools.sml | 21 fun set_pfx s k = foldr (fn (v,av) => if String.isPrefix v k then true else av) false s
|
H A D | muSyntax.sml | 468 in List.foldl (fn (_,av) => mk_subs2 av l) mv l end 477 | "RV" => (inst [``:'a``|->prop_type] ``RV ^(List.foldr (fn (sb,av) => if (Term.compare(snd sb,av)=EQUAL) 478 then fst sb else av) (List.hd args) subs)``,l)
|
H A D | cearTools.sml | 78 val astate = pairSyntax.list_mk_pair(List.tabulate(nabsv,fn i => mk_bool_var("av"^(int_to_string i)))) 156 val navn = "av"^(int_to_string(nabsv-1)) 252 val vmabs = List.filter (fn (t,_) => (String.size t) >= 3 andalso String.compare("av",String.substring(t,0,2))=EQUAL )
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Term.sml | 241 fun avoid av n = NameSet.member n av; 243 fun variantPrime av = Name.variantPrime {avoid = avoid av}; 245 fun variantNum av = Name.variantNum {avoid = avoid av};
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Term.sml | 241 fun avoid av n = NameSet.member n av; 243 fun variantPrime av = Name.variantPrime {avoid = avoid av}; 245 fun variantNum av = Name.variantNum {avoid = avoid av};
|
/seL4-l4v-master/HOL4/src/IndDef/ |
H A D | InductiveDefinition.sml | 43 fun variants av [] = [] 44 | variants av (h::t) = 45 let val vh = vary av h 46 in vh::variants (vh::av) t
|
/seL4-l4v-master/graph-refine/ |
H A D | rep_graph.py | 422 def av (nm, typ, mem_name = None): function in function:GraphSlice.get_loop_pc_env 435 env[(nm, typ)] = av (nm + '_after', typ, 445 pc = mk_smt_expr (av ('pc_of', boolT), boolT)
|
/seL4-l4v-master/HOL4/src/quotient/examples/ |
H A D | tactics.sml | 130 `<|vv`;`<|vsv`;`<|av`;`:==`;`//v`;`<<`]; ();
|
/seL4-l4v-master/HOL4/src/AI/ |
H A D | aiLib.sml | 355 val av = Array.sub (arr,a) value 359 Array.update (arr,b,av)
|