/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | regAllocation.sml | 882 fun replace exp = 883 if is_let exp then 884 let val (lt, rhs) = dest_let exp; 889 else if is_cond exp then 890 let val (c,t,f) = dest_cond exp 894 else if is_pair exp then 895 let val (t1,t2) = dest_pair exp 898 else rw exp
|
H A D | mechReasoning.sml | 104 fun mk_vars exp = 109 | set_vars exp = 112 set_vars exp 194 List.map (fn exp => (exp |-> new_var())) expL 197 fun read_one_var s exp = 198 let val v0 = IRSyntax.read_exp s exp; 201 val v1 = rhs (concl ((conv exp) v0)) 374 | calculate_outs st exp = 375 read_one_var st exp [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | regAllocation.sml | 882 fun replace exp = 883 if is_let exp then 884 let val (lt, rhs) = dest_let exp; 889 else if is_cond exp then 890 let val (c,t,f) = dest_cond exp 894 else if is_pair exp then 895 let val (t1,t2) = dest_pair exp 898 else rw exp
|
H A D | mechReasoning.sml | 69 fun mk_vars exp = 74 | set_vars exp = 77 set_vars exp 149 List.map (fn exp => (i := !i + 1; {redex = exp, residue = mk_var ("v" ^ (Int.toString (!i)), Type `:DATA`)})) expL 152 fun read_one_var s exp = 154 val v0 = IRSyntax.read_exp s exp; 157 val v1 = rhs (concl ((conv exp) v0)) 286 | calculate_outs st exp = 287 read_one_var st exp [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | regAllocation.sml | 882 fun replace exp = 883 if is_let exp then 884 let val (lt, rhs) = dest_let exp; 889 else if is_cond exp then 890 let val (c,t,f) = dest_cond exp 894 else if is_pair exp then 895 let val (t1,t2) = dest_pair exp 898 else rw exp
|
/seL4-l4v-master/HOL4/examples/machine-code/hoare-triple/ |
H A D | temporalScript.sml | 11 TEMPORAL ((to_set,next,instr,less,allow): ('a,'b,'c) processor) c exp = 16 exp f seq`
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | reals.cpp | 297 // RTS call for exp. 300 return exp(arg); 456 int exp = 0; // The value of exp is not always defined. local 457 Handle mantH = real_result(taskData, frexp(real_arg(pushedArg), &exp)); 461 result->WordP()->Set(0, TAGGED(exp)); 496 // RTS call for exp.
|
/seL4-l4v-master/HOL4/examples/algebra/finitefield/ |
H A D | ffAdvancedScript.sml | 620 and f*.exp = $** by field_nonzero_mult_property 1128 Thus g.exp z om = (z ** om) MOD ox = 1 by ZN_order_property, EXP_MOD 1131 Note !x k. g.exp x k = (ZN ox).prod.exp x k by Invertibles_property 1132 and !x k. (ZN ox).prod.exp x k = (x ** k) MOD ox by ZN_exp 1134 g.exp z d 1141 Given g.exp z d = 1, 1142 and g.exp z om = 1 1166 `f*.exp = $**` by rw[field_nonzero_mult_property] >> 1169 `!x k. !x k. g.exp [all...] |
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | BackendIntermediateCode.sml | 219 | BICHandle of (* Exception handler. *) { exp: backendIC, handler: backendIC, exPacketAddr: int } 564 | BICHandle {exp, handler, exPacketAddr} => 568 pretty exp, 584 fn (SOME exp) => 589 pretty exp
|
H A D | CODETREE_SIMPLIFIER.sml | 94 fun mkEnv([], exp) = exp 95 | mkEnv(decs, exp as Extract(LoadLocal loadAddr)) = 106 else Newenv(decs, exp) 107 | _ => Newenv(decs, exp) 109 | mkEnv(decs, exp) = Newenv(decs, exp) 224 | foldLoop f n (Newenv(_, exp)) = foldLoop f n exp 287 | changeLoops(Newenv(decs, exp)) [all...] |
H A D | CODETREE_LAMBDA_LIFT.sml | 78 | checkCode(Newenv(decs, exp)) = 82 val processedExp = checkMapCode exp (* The expression first. *) 218 | processCode(Newenv(decs, exp)) = 273 SOME(Newenv(processDecs decs, processMapCode exp))
|
H A D | CODETREE_CODEGEN_CONSTANT_FUNCTIONS.sml | 301 | extractProps(Newenv(_, exp)) = extractProps exp
|
/seL4-l4v-master/HOL4/examples/AKS/theories/ |
H A D | AKSsetsScript.sml | 161 !x. x IN M ==> !n. (Invertibles (ZN k).prod).exp x n IN M 762 (* Theorem: 1 < k /\ x IN M ==> !n. (Invertibles (ZN k).prod).exp x n IN M *) 765 Base case: (Invertibles (ZN k).prod).exp x 0 IN M 766 (Invertibles (ZN k).prod).exp x 0 771 Step case: x IN M /\ (Invertibles (ZN k).prod).exp x n IN M ==> 772 (Invertibles (ZN k).prod).exp x (SUC n) IN M 773 Let y = ((Invertibles (ZN k).prod).exp x n) 777 (Invertibles (ZN k).prod).exp x (SUC n) 787 !x. x IN M ==> !n. (Invertibles (ZN k).prod).exp x n IN M``, 803 !m. (Invertibles (ZN k).prod).exp [all...] |
/seL4-l4v-master/HOL4/examples/fun-op-sem/ml/ |
H A D | typeSoundScript.sml | 66 val _ = Datatype`exp = 69 | App exp exp 70 | Let string exp exp 71 | Fun string exp 72 | Funrec string string exp 73 | Ref exp 74 | Deref exp 75 | Assign exp ex [all...] |
/seL4-l4v-master/HOL4/examples/algebra/polynomial/ |
H A D | polyModuloRingScript.sml | 72 x ##z n = (PolyModRing r z).sum.exp x n 73 x **z n = (PolyModRing r z).prod.exp x n 152 !n. ((PolyModRing r z).prod excluding |0|).exp p n = p ** n % z 211 !n. ((PolyModRing r z).prod excluding |0|).exp p n = p ** n % z 262 val _ = overload_on("##z", ``(PolyModRing r z).sum.exp``); 263 val _ = overload_on("**z", ``(PolyModRing r z).prod.exp``); 1111 !n. ((PolyModRing r z).prod excluding |0|).exp p n = (p ** n) % z *) 1158 !n. ((PolyModRing r z).prod excluding |0|).exp p n = (p ** n) % z``, 1316 !n. ((PolyModRing r z).prod excluding |0|).exp p n = (p ** n) % z``,
|
/seL4-l4v-master/HOL4/src/portableML/mosml/ |
H A D | Arbnumcore.sml | 124 val (sig_part, exp) = count_base_powers r 127 val sig_anum = shl exp (fromInt sig_part) 128 val sig_real = exp_r exp (real sig_part) 130 if exp > 0 then sig_anum + floor (r - sig_real)
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Useful.sig | 45 val exp : ('a * 'a -> 'a) -> 'a -> int -> 'a -> 'a value
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Useful.sig | 45 val exp : ('a * 'a -> 'a) -> 'a -> int -> 'a -> 'a value
|
/seL4-l4v-master/HOL4/examples/algebra/ring/ |
H A D | ringMapScript.sml | 60 ##_ = (r_:'b ring).sum.exp 61 **_ = (r_:'b ring).prod.exp 188 subring_num |- !r s. s <= r ==> !n. s.sum.exp s.prod.id n = ##n 189 subring_exp |- !r s. s <= r ==> !x. x IN B ==> !n. s.prod.exp x n = x ** n 278 val _ = overload_on("##_", ``(r_:'b ring).sum.exp``); 279 val _ = overload_on("**_", ``(r_:'b ring).prod.exp``); 1414 (* Theorem: s <= r ==> !n. s.sum.exp s.prod.id n = ##n *) 1418 ``!(r s):'a ring. s <= r ==> !n. s.sum.exp s.prod.id n = ##n``, 1421 (* Theorem: s <= r ==> !n. s.sum.exp s.prod.id n = ##n *) 1425 ``!(r s):'a ring. s <= r ==> !x. x IN B ==> !n. s.prod.exp [all...] |
/seL4-l4v-master/HOL4/examples/dev/ |
H A D | inlineCompile.sml | 130 (* CompileExp2 exp *) 132 (* [REC assumption] |- <circuit> ===> DEV exp *)
|
/seL4-l4v-master/HOL4/examples/elliptic/swsep/ |
H A D | swsepLib.sml | 149 fun spec_sep (comp:(string * hol_type * (IRSyntax.exp * 'a * IRSyntax.exp) * thm list * thm * thm * thm * thm * thm * string * string list)) =
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | metisTools.sml | 69 | num_map "arithmetic.EXP" = SOME "exp" 100 | int_map "integer.int_exp" = SOME "exp"
|
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootParser.sml | 408 val (os_opt, exp) = holfoot_expression2absyn vs os_opt arg_exp 410 (os_opt, cs_opt, SOME exp) 493 | holfoot_a_space_pred2absyn vs (os_opt, cs_opt) (Aspred_pointsto (exp, pl)) = 495 val (os_opt, a1) = holfoot_expression2absyn vs os_opt exp; 804 val (_, exp) = holfoot_expression2absyn vs NONE expr; 805 val comb_a = Absyn.list_mk_app (Absyn.mk_AQ holfoot_prog_assign_term, [Absyn.mk_AQ var_term, exp]); 830 val (_, exp) = holfoot_expression2absyn vs NONE expr; 833 val comb_a = Absyn.list_mk_app (Absyn.mk_AQ holfoot_prog_new_term, [exp, Absyn.mk_AQ var_term, Absyn.mk_AQ tl_t]);
|
/seL4-l4v-master/HOL4/src/tactictoe/src/ |
H A D | tttBigSteps.sml | 288 val (bstatus,(exv,exp,exa)) = run_bigsteps searchobj g 293 write_tnnex (poldir ^ "/" ^ pb) (basicex_to_tnnex exp);
|
/seL4-l4v-master/HOL4/examples/algebra/group/ |
H A D | groupMapScript.sml | 65 !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n 79 !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n 285 (* Theorem: Group g /\ Group h /\ GroupHomo f g h ==> !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n *) 294 !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n``, 406 (* Theorem: Group g /\ Group h /\ GroupIso f g h ==> !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n *) 415 !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n``,
|