Searched refs:exp (Results 126 - 150 of 228) sorted by relevance

12345678910

/seL4-l4v-master/HOL4/examples/dev/sw/
H A DregAllocation.sml882 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 DmechReasoning.sml104 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 DregAllocation.sml882 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 DmechReasoning.sml69 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 DregAllocation.sml882 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 DtemporalScript.sml11 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 Dreals.cpp297 // 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 DffAdvancedScript.sml620 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 DBackendIntermediateCode.sml219 | 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 DCODETREE_SIMPLIFIER.sml94 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 DCODETREE_LAMBDA_LIFT.sml78 | 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 DCODETREE_CODEGEN_CONSTANT_FUNCTIONS.sml301 | extractProps(Newenv(_, exp)) = extractProps exp
/seL4-l4v-master/HOL4/examples/AKS/theories/
H A DAKSsetsScript.sml161 !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 DtypeSoundScript.sml66 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 DpolyModuloRingScript.sml72 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 DArbnumcore.sml124 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 DUseful.sig45 val exp : ('a * 'a -> 'a) -> 'a -> int -> 'a -> 'a value
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DUseful.sig45 val exp : ('a * 'a -> 'a) -> 'a -> int -> 'a -> 'a value
/seL4-l4v-master/HOL4/examples/algebra/ring/
H A DringMapScript.sml60 ##_ = (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 DinlineCompile.sml130 (* CompileExp2 exp *)
132 (* [REC assumption] |- <circuit> ===> DEV exp *)
/seL4-l4v-master/HOL4/examples/elliptic/swsep/
H A DswsepLib.sml149 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 DmetisTools.sml69 | num_map "arithmetic.EXP" = SOME "exp"
100 | int_map "integer.int_exp" = SOME "exp"
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/
H A DholfootParser.sml408 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 DtttBigSteps.sml288 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 DgroupMapScript.sml65 !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``,

Completed in 155 milliseconds

12345678910