Searched refs:exp (Results 101 - 125 of 228) sorted by relevance

12345678910

/seL4-l4v-master/HOL4/examples/AKS/theories/
H A DAKSshiftScript.sml265 ((PolyRing t).prod.exp p n ==
266 poly_peval t p ((PolyRing t).prod.exp (poly_shift t (PolyRing t).prod.id 1) n))
267 (pmod t (poly_sub t ((PolyRing t).prod.exp (poly_shift t (PolyRing t).prod.id 1) k)
307 qabbrev_tac `a = \c:num. (PolyRing (ZN n)).sum.exp (PolyRing (ZN n)).prod.id c` >>
308 qabbrev_tac `z = \c:num. (PolyRing (ZN m)).sum.exp (PolyRing (ZN m)).prod.id c` >>
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DBASE_PARSE_TREE.sml132 | Localdec of (* Local dec in dec and let dec in exp. *)
176 { exp: parsetree, hrules: matchtree list, location: location, listLocation: location }
209 exp: parsetree,
236 exp: parsetree,
282 exp: parsetree,
H A DTYPECHECK_PARSETREE.sml1316 | (aHandler as HandleTree {exp, hrules, location, ...}) =>
1320 val expType = assValues aHandler exp;
1420 and assMatchTree _ (MatchTree {vars, exp, resType, argType, ...}) =
1457 val expType = assignValues(newLevel, letDepth, bodyEnv, v, exp);
1529 fun checkTypes (patType, (ValBind {dec, exp, line, isRecursive, ...})) =
1559 val expType = assignValues(newLevel, letDepth, newEnv, exp, exp);
1567 valTypeMessage (lex, typeEnv) ("Expression:", exp, expType),
1573 definition it says "exp must be of the form fn match". In ML90
1584 if isRecursive andalso not (isConstrainedFn exp)
[all...]
H A DCODEGEN_PARSETREE.sml170 | tupleWidth(HandleTree{exp, ...}) =
175 tupleWidth exp
185 fun getWidth(MatchTree{exp, ...}) = tupleWidth exp
356 val MatchTree {vars, exp, breakPoint, ... } = List.nth(alt, pattChosenIndex)
365 addBreakPointCall(breakPoint, getLocation exp, context |> repDebugEnv varDebugEnv)
367 mkEnv(envDec @ bptCode, codegen (exp, context |> repDebugEnv bptEnv))
421 | cgExps (MatchTree {vars, exp, breakPoint, ...} ::al,
458 addBreakPointCall(breakPoint, getLocation exp, fnContext |> repDebugEnv varDebugEnv)
461 mkEnv(localDecs @ envDec @ bptCode, codegen (exp, fnContex
1613 val exp = codegen (vbExp, localContext |> repDecName (decName ^ fName ^ "-")) value
[all...]
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DCODETREE_STATIC_LINK_AND_CASES.sml398 BICNewenv(decs, exp) => decs @ (BICNullBinding exp :: copiedRest)
413 fun mkEnv([], exp) = exp
414 | mkEnv(decs, exp) = BICNewenv(decs, exp)
419 | splitLast decs [BICNullBinding exp] = (List.rev decs, exp)
438 | insert(Handle { exp, handler, exPacketAddr }) =
444 val exp value
[all...]
H A DCODETREE_REMOVE_REDUNDANT.sml154 fun doClean codeUse (Newenv(decs, exp)) =
157 val processedExp = cleanCode (exp, codeUse)
225 | processDecs(NullBinding exp :: rest) =
229 if sideEffectFree exp
231 else NullBinding(cleanCode(exp, [UseGeneral])) :: processedRest
H A DCODETREE_OPTIMISER.sml432 | bodyReturnsTuple(Newenv(_, exp)) = bodyReturnsTuple exp
839 | mapbinding(NullBinding exp) = NullBinding(mapExp [UseGeneral] exp)
906 and optGeneral context exp = mapCodetree (optimise(context, [UseGeneral])) exp
1160 | pushContainer(Newenv(decs, exp), leafFn) =
1161 Newenv(decs, pushContainer(exp, leafFn))
1173 | pushContainer(Handle{exp, handler, exPacketAddr}, leafFn) =
1174 Handle{exp
[all...]
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/spec/
H A Dlisp_semanticsScript.sml218 (!args a fc fns params exp x ok2.
220 (fns ' fc = (params,exp)) /\ (LENGTH params = LENGTH args) /\
221 R_ev (exp,VarBind params args,fns,io,ok) (x,fns2,io2,ok2)
240 (fns ' fname = (params,exp)) /\ (LENGTH params = LENGTH args) /\
241 R_ev (exp,VarBind params args,fns,io,ok) (x,fns2,io2,ok2)
247 (fns ' f = (params,exp)) /\ (LENGTH params = LENGTH args) ==>
341 (!input fns io input2 exp rest s fns2 io2 ok2 io3 ok3.
343 (sexp_parse_stream input2 = (exp,rest)) /\
344 R_ev (sexp2term exp,FEMPTY,fns,io,T) (s,fns2,io2,ok2) /\
/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/
H A Dmilawa_execScript.sml78 (!args a fc fns params exp x ok2.
80 fc IN FDOM fns /\ ~(?xs. exp = App Error xs) /\
81 (fns ' fc = (params,exp)) /\ (LENGTH params = LENGTH args) /\
82 MR_ev (exp,VarBind params args,ctxt,fns,ok) (x,ok2)
108 (fns ' fname = (params,exp)) /\ (LENGTH params = LENGTH args) /\
109 MR_ev (exp,VarBind params args,ctxt,fns,ok) (x,ok2)
1823 inst_term a exp = term_sub (MAP (\v. (v,mConst (a v))) (free_vars exp)) exp`;
1931 ``!exp
[all...]
H A Dmilawa_initScript.sml27 (!xs fns io exp s fns2 io2 ok2 io3 ok3.
28 R_ev (sexp2term exp,FEMPTY,fns,io,T) (s,fns2,io2,ok2) /\
30 R_aux_exec (exp::xs,fns,io) (io3,ok2 /\ ok3))`;
114 val (v,exp) = dest_eq (first (can dest_var_eq) (list_dest dest_conj tm))
115 in REWRITE_EQS (INST [v|->exp] th) end handle HOL_ERR _ => th
/seL4-l4v-master/isabelle/src/Pure/ML/
H A Dml_lex.scala215 val exp = ("E" | "e") ~ decint ^^ { case x ~ y => x + y }
229 (decint ~ "." ~ dec ~ (opt(exp) ^^ { case Some(x) => x case None => "" }) ^^
231 decint ~ exp ^^ { case x ~ y => x + y }) ^^ (x => Token(Kind.REAL, x))
/seL4-l4v-master/HOL4/examples/machine-code/graph/
H A DexportLib.sml270 type_of s = ``:64 state`` orelse failwith("bad exp")
271 val _ = type_of e = ``:bool`` orelse failwith("bad exp")
273 fun exp tm = function
280 type_of s = ``:64 state`` orelse failwith("bad exp")
289 "" ^ n ^ " " ^ get_var_type n ^ " " ^ exp tm
320 export_list (map exp input),
/seL4-l4v-master/l4v/isabelle/src/Pure/ML/
H A Dml_lex.scala215 val exp = ("E" | "e") ~ decint ^^ { case x ~ y => x + y }
229 (decint ~ "." ~ dec ~ (opt(exp) ^^ { case Some(x) => x case None => "" }) ^^
231 decint ~ exp ^^ { case x ~ y => x + y }) ^^ (x => Token(Kind.REAL, x))
/seL4-l4v-master/HOL4/src/datatype/
H A Dselftest.sml76 | let_exp of dec => exp ;
78 exp = aexp of atexp
79 | app_exp of exp => atexp
85 rule = rule of pat => exp ;
91 valbind = bind of pat => exp
92 | bindl of pat => exp => valbind
/seL4-l4v-master/HOL4/examples/algebra/field/
H A DfieldScript.sml65 ## = r.sum.exp
70 ** = r.prod.exp
296 (f*.exp = $** )
297 field_nonzero_exp |- !r. Field r ==> (f*.exp = $** )
460 field_add_exp_eqn |- !r. Field r ==> !x. x IN R ==> !n. r.sum.exp x n = x * ##n
487 (#e = #1) /\ (g.op = $* ) /\ (!x n. x IN G ==> (g.exp x n = x ** n)) /\
491 field_subgroup_exp |- !r g. Field r /\ g <= f* ==> !x n. x IN G ==> (g.exp x n = x ** n)
1326 For f*.exp = r.prod.exp
1334 (f*.exp
[all...]
H A DfieldOrderScript.sml151 = case OLEAST k. 0 < k /\ (f*.exp x k = f*.id) of NONE => 0 | SOME k => k by period_def
165 val it = |- FiniteGroup f* ==> !x. x IN F* ==> 0 < forder x /\ (f*.exp x (forder x) = f*.id): thm
176 val it = |- !x. f*.exp x (forder x) = f*.id: thm
187 val it = |- !x n. 0 < n /\ n < forder x ==> f*.exp x n <> f*.id: thm
235 <=> !n. 0 < n ==> f*.exp #0 n <> f*.id by order_eq_0
248 also !n. f*.exp x n = x ** n by monoid_exp_def
252 val it = |- !x. (forder x = 0) <=> !n. 0 < n ==> f*.exp x n <> f*.id: thm
260 `!n. f*.exp x n = x ** n` by rw[monoid_exp_def] >>
433 val it = |- Group f* ==> !x. x IN F* ==> !n. (f*.exp x n = f*.id) <=> forder x divides n: thm
489 val it = |- Group f* ==> !x. x IN F* ==> !k. forder (f*.exp
[all...]
/seL4-l4v-master/HOL4/examples/algebra/group/
H A DsubgroupScript.sml57 g.exp = Iteration of g.op (added by monoid)
88 subgroup_exp |- !g h. h <= g ==> !x. x IN H ==> !n. h.exp x n = x ** n
209 subset_group_exp |- !g s x. x IN s ==> !n. (subset_group g s).exp x n = x ** n
364 (* Theorem: h <= g ==> !x. x IN H ==> !n. h.exp x n = x ** n *)
368 ``!(g:'a group) h. h <= g ==> !x. x IN H ==> !n. h.exp x n = x ** n``,
1650 (* Theorem: x IN s ==> !n. (subset_group g s).exp x n = x ** n *)
1653 Base: (subset_group g s).exp x 0 = x ** 0
1654 (subset_group g s).exp x 0
1658 Step: x IN s /\ (subset_group g s).exp x n = x ** n ==>
1659 (subset_group g s).exp
[all...]
H A DgroupScript.sml53 g.exp = Iteration of g.op (added by monoid)
171 group_excluding_exp |- !g z x n. (g excluding z).exp x n = x ** n
1140 (* Theorem: (g excluding z).exp x n = x ** n *)
1143 Base: (g excluding z).exp x 0 = x ** 0
1144 (g excluding z).exp x 0
1148 Step: (g excluding z).exp x n = x ** n ==> (g excluding z).exp x (SUC n) = x ** SUC n
1149 (g excluding z).exp x (SUC n)
1150 = (g excluding z).op x (g excluding z).exp x n by group_exp_SUC
1157 ``!(g:'a group) z x n. (g excluding z).exp
[all...]
/seL4-l4v-master/graph-refine/
H A Dcheck.py396 return lambda exp: logic.var_subst (exp, {('%i', word32T) : v},
398 def inst (exp):
399 return logic.inst_eq_at_visit (exp, visit)
573 return lambda exp: logic.var_subst (exp, {('%i', word32T) : v},
583 hyps += [(eq_hyp ((zsub (exp), start), (isub (exp), visit),
585 for exp in eqs if logic.inst_eq_at_visit (exp, visit_nu
[all...]
/seL4-l4v-master/HOL4/examples/algebra/monoid/
H A DmonoidScript.sml51 ** = g.exp
361 (* Convert exp function to exp field, i.e. g.exp is defined to be monoid_exp. *)
362 val _ = add_record_field ("exp", ``monoid_exp``);
364 - type_of ``g.exp``;
370 val _ = overload_on ("**", ``g.exp``);
H A DmonoidInstancesScript.sml77 plus_mod_exp |- !n. 0 < n ==> !x k. (plus_mod n).exp x k = (k * x) MOD n
98 times_mod_exp |- !n. 0 < n ==> !x k. (times_mod n).exp x k = (x MOD n) ** k MOD n
207 (* Theorem: 0 < n ==> !x k. (plus_mod n).exp x k = (k * x) MOD n *)
230 ``!n. 0 < n ==> !x k. (plus_mod n).exp x k = (k * x) MOD n``,
317 (* Theorem: 0 < n ==> !x k. (times_mod n).exp x k = ((x MOD n) ** k) MOD n *)
342 ``!n. 0 < n ==> !x k. (times_mod n).exp x k = ((x MOD n) ** k) MOD n``,
/seL4-l4v-master/HOL4/examples/algebra/finitefield/
H A DffUnityScript.sml286 and (f*.id = #1) /\ (f*.exp = $** ) by field_nonzero_mult_property
370 so g.exp x (CARD G) = g.id by finite_group_Fermat
371 or f*.exp x k = f*.id by generated_property, generated_exp
446 = IMAGE (\j. f*.exp z j) (count (forder z)) by generated_carrier_as_image
468 BIJ (\n. f*.exp z n) (count (forder z)) (Generated f* z).carrier: thm
1753 <=> p IN g.carrier /\ (g.exp p n = |1|) by roots_of_unity_element
1754 <=> poly p /\ p <> |0| /\ deg p < deg z /\ (g.exp p n = |1|) by poly_mod_ring_nonzero_element, 0 < deg z
1771 `p IN (roots_of_unity g n).carrier <=> p IN g.carrier /\ (g.exp p n = |1|)` by rw[roots_of_unity_element] >>
1772 `_ = (poly p /\ p <> |0| /\ deg p < deg z /\ (g.exp p n = |1|))` by metis_tac[poly_mod_ring_nonzero_element] >>
1879 Z_2 = {0, 1} = {0, exp(
[all...]
/seL4-l4v-master/HOL4/examples/acl2/lisp/
H A Dbook-essence.lisp241 (let ((exp (cadr (assoc-keyword :check-expansion (cddr form)))))
242 (cond ((consp exp)
243 (essential-events (cons exp (cdr forms)) acc ctx state))
/seL4-l4v-master/HOL4/examples/algebra/ring/
H A DringScript.sml58 ## = r.sum.exp
62 ** = r.prod.exp
136 ring_sum_zero |- !r. Ring r ==> !n. r.sum.exp #0 n = #0
312 ring_add_exp_eqn |- !r. Ring r ==> !x. x IN R ==> !n. r.sum.exp x n = x * ##n
764 val _ = overload_on ("ring_numr", ``r.sum.exp #1``); (* for fallback *)
765 val _ = overload_on ("##", ``r.sum.exp #1``); (* current use *)
789 val _ = overload_on ("**", ``r.prod.exp``);
804 > val it = [] |- Group r.sum ==> !x. x IN r.sum.carrier ==> !n. r.sum.exp x n IN r.sum.carrier : thm
806 > val it = [Group r.sum] |- !x. x IN r.sum.carrier ==> !n. r.sum.exp x n IN r.sum.carrier : thm
829 (* Lifting Group exp theore
[all...]
/seL4-l4v-master/HOL4/tools/mllex/
H A Dmllex.sml257 datatype exp = EPS | CLASS of bool array * int | CLOSURE of exp type
258 | ALT of exp * exp | CAT of exp * exp | TRAIL of int
684 val SymTab = ref (create String.<=) : (string,exp) dictionary ref
686 fun GetExp () : exp =
797 fun renum(e : exp) : exp
[all...]

Completed in 177 milliseconds

12345678910