/seL4-l4v-master/HOL4/examples/AKS/theories/ |
H A D | AKSshiftScript.sml | 265 ((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 D | BASE_PARSE_TREE.sml | 132 | 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 D | TYPECHECK_PARSETREE.sml | 1316 | (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 D | CODEGEN_PARSETREE.sml | 170 | 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 D | CODETREE_STATIC_LINK_AND_CASES.sml | 398 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 D | CODETREE_REMOVE_REDUNDANT.sml | 154 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 D | CODETREE_OPTIMISER.sml | 432 | 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 D | lisp_semanticsScript.sml | 218 (!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 D | milawa_execScript.sml | 78 (!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 D | milawa_initScript.sml | 27 (!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 D | ml_lex.scala | 215 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 D | exportLib.sml | 270 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 D | ml_lex.scala | 215 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 D | selftest.sml | 76 | 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 D | fieldScript.sml | 65 ## = 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 D | fieldOrderScript.sml | 151 = 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 D | subgroupScript.sml | 57 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 D | groupScript.sml | 53 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 D | check.py | 396 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 D | monoidScript.sml | 51 ** = 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 D | monoidInstancesScript.sml | 77 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 D | ffUnityScript.sml | 286 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 D | book-essence.lisp | 241 (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 D | ringScript.sml | 58 ## = 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 D | mllex.sml | 257 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...] |