/seL4-l4v-master/HOL4/examples/hardware/hol88/MISC/ |
H A D | init.ml | 5 lisp `(load 'eval)`;;
|
H A D | eval-test.ml | 1 % File for testing the Lisp functions defined in hol/lisp/eval.l 2 and hol/lisp/dml-eval.l (not part of the HOL system) %
|
/seL4-l4v-master/HOL4/src/boss/theory_tests/ |
H A D | github462Script.sml | 13 "eval" 14 ���(eval st [Log e1 e2] = 15 case eval st [e1] of 17 SOME (Exp e) => eval st' [e] 21 (eval st other = ARB)���;
|
/seL4-l4v-master/HOL4/examples/formal-languages/context-free/ |
H A D | pegML.sml | 61 fun eval G (e:(''i,'v)pegsym) input (results:'v option list) k fk = function 72 eval G e1 input results 75 | choice(e1,e2,f) => eval G e1 81 eval G e input results 85 eval G e input (NONE::results) (listsym(e,f,k)) (poplist(f,k)) 86 | nt(n,f) => eval G (G n) input results k fk 91 | sym(e,k,f) => eval G e input results k f 95 eval G e input results (listsym(e,f,k)) (poplist(f, k)) 125 eval testG (nt("E",I)) (mk "1+2*3") [] done failed, 126 eval test [all...] |
/seL4-l4v-master/HOL4/examples/bootstrap/ |
H A D | source_semanticsScript.sml | 186 Definition fix_def: (* helps prove termination of the definition of eval *) 194 eval (env:num -> v option) (Const n) s = (Res (Num n), s) ��� 195 eval env (Var t) s = 199 eval env (Op f xs) s = 203 eval env (Let t x y) s = 204 (case fix s (eval env x s) of 206 | (Res v, s1) => eval ((t =+ SOME v) env) y s1) ��� 207 eval env (If test xs y z) s = 212 | (Res b, s1) => eval env (if b then y else z) s1 214 eval en [all...] |
/seL4-l4v-master/HOL4/src/pred_set/src/ |
H A D | pred_setLib.sml | 21 fun mk_in_conv eval tm = 26 IN_CONV eval tm 78 val eval = computeLib.CBV_CONV compset value 80 [ (in_tm, 2, mk_in_conv eval), 81 (insert_tm, 2, INSERT_CONV eval),
|
/seL4-l4v-master/HOL4/examples/algebra/finitefield/ |
H A D | ffExtendScript.sml | 150 field_generator_def |- !r s z. generator s z <=> (IMAGE (\p. eval p z) (PolyRing s).carrier = R) 153 (generator s z <=> !x. x IN R ==> ?p. Poly s p /\ (x = eval p z)) 162 GroupHomo (\p. eval p x) (PolyModRing s (minimal x)).sum r.sum 164 MonoidHomo (\p. eval p x) (PolyModRing s (minimal x)).prod r.prod 166 FieldHomo (\p. eval p x) (PolyModRing s (minimal x)) r 168 INJ (\p. eval p x) (PolyModRing s (minimal x)).carrier R 170 SURJ (\p. eval p x) (PolyModRing s (minimal x)).carrier R 172 BIJ (\p. eval p x) (PolyModRing s (minimal x)).carrier R 174 FieldIso (\p. eval p x) (PolyModRing s (minimal x)) r 176 (PolyModRing s (minimal x) === r) (\p. eval [all...] |
H A D | ffMinimalScript.sml | 107 !x. x IN R ==> (p <o> ebasis x n = eval p x) 154 ((eval p x = eval q x) <=> (p % minimal x = q % minimal x)) 169 !x. x IN R ==> (p <o> ebasis x n = eval p x) 397 !x. x IN R ==> (p <o> (ebasis x n) = eval p x) *) 401 !x. x IN R ==> (p <o> ebasis x 0 = eval p x) 414 = eval [c] x by poly_eval_const 416 !x. x IN R ==> (p <o> ebasis x (SUC n) = eval p x) 423 and eval t x IN R by weak_eval_element 427 = h * (x ** SUC n) + eval [all...] |
H A D | ffPolyScript.sml | 262 (eval p x ** CARD R = eval p (x ** CARD R)) 264 !n. eval p x ** CARD R ** n = eval p (x ** CARD R ** n) 276 (eval p x ** char r = eval p (x ** char r)) 278 !n. eval p x ** char r ** n = eval p (x ** char r ** n) 292 !x. x IN R ==> (eval p x ** CARD B = eval [all...] |
/seL4-l4v-master/HOL4/examples/algebra/polynomial/ |
H A D | polyRootScript.sml | 91 poly_eval_factor |- !r. Ring r ==> !c x. c IN R /\ x IN R ==> (eval (factor c) x = x - c) 92 poly_factor_eval |- !r. Ring r ==> !c x. c IN R /\ x IN R ==> (eval (factor c) x = x - c) 95 !x. x IN R ==> (eval (factor c) x = x - c) 110 (p % factor x = chop [eval p x]) 178 poly_unity_eval |- !r. Ring r ==> !x. x IN R ==> !n. eval (unity n) x = x ** n - #1 189 poly_master_eval |- !r. Ring r ==> !x n. x IN R ==> (eval (master n) x = x ** n - x) 473 (* Theorem: eval (factor c) x = x - c *) 475 eval (factor c) x 476 = eval (-c:: |1|) x by poly_factor_def 477 = -c + (eval | [all...] |
H A D | polyWeakScript.sml | 64 eval = poly_eval r 376 poly_eval_of_zero |- !r x. eval [] x = #0 377 poly_eval_cons |- !r h t x. eval (h::t) x = h + eval t x * x 378 # poly_eval_zero |- !r x. eval |0| x = #0 379 # poly_eval_const |- !r. Ring r ==> !h x. h IN R /\ x IN R ==> (eval [h] x = h) 380 # weak_eval_element |- !r. Ring r ==> !p. weak p ==> !x. x IN R ==> eval p x IN R 381 # poly_eval_zerop |- !r. Ring r ==> !p x. zerop p /\ x IN R ==> (eval p x = #0) 382 # poly_eval_chop |- !r. Ring r ==> !p x. x IN R ==> (eval (chop p) x = eval [all...] |
H A D | polyMultiplicityScript.sml | 1146 Now, eval (factor c) c = #0 by poly_eval_factor, root p c 1148 eval (diff p) c 1149 = eval (diff q * factor c ** k + q * diff (factor c ** k)) c by poly_diff_mult 1150 = eval (diff q * factor c ** k) c + eval (q * diff (factor c ** k)) c by poly_eval_add 1151 = (eval (diff q) c) * (eval (factor c ** k) c) + 1152 (eval q c) * (eval (diff (factor c ** k)) c) by poly_eval_mult 1154 eval (facto [all...] |
H A D | polyDivisionScript.sml | 202 !x. x IN roots q ==> (eval (p % q) x = eval p x) 1548 !x. x IN roots q ==> (eval (p % q) x = eval p x) *) 1554 and eval q x = #0 by poly_root_def 1555 eval p x 1556 = eval (s * q + t) x by p = s * q + t 1557 = eval (s * q) x + eval t x by poly_eval_add 1558 = (eval [all...] |
H A D | polyEvalScript.sml | 106 poly_peval_by_zero |- !r p. Ring r /\ poly p ==> peval p |0| = chop [eval p #0] 107 poly_peval_by_one |- !r p. Ring r /\ poly p ==> peval p |1| = chop [eval p #1] 979 (* Theorem: peval p |0| == chop [eval p #0]), the constant term *) 989 Base case: poly [] ==> (peval [] |0| == chop [eval [] #0]) 991 Step case: poly p ==> (peval p |0| == chop [eval p #0]) ==> 992 !h. poly (h::p) ==> (peval (h::p) |0| == chop [eval (h::p) #0]) 995 = h * |1| + (chop [eval p #0]) * |0| by induction hypothesis 998 = chop [eval (h::p) #0] by poly_eval_def, poly_chop_def 1002 ``!r:'a ring p. Ring r /\ poly p ==> (peval p |0| = chop [eval p #0])``, 1007 (* Theorem: peval p |1| == chop [eval [all...] |
H A D | polyRingScript.sml | 375 # poly_eval_element |- !r. Ring r ==> !p. poly p ==> !x. x IN R ==> eval p x IN R 376 # poly_eval_cmult |- !r. Ring r ==> !p c x. poly p /\ c IN R /\ x IN R ==> (eval (c * p) x = c * eval p x) 377 # poly_eval_neg |- !r. Ring r ==> !p x. poly p /\ x IN R ==> (eval (-p) x = -eval p x) 378 # poly_eval_add |- !r. Ring r ==> !p q x. poly p /\ poly q /\ x IN R ==> (eval (p + q) x = eval p x + eval q x) 379 # poly_eval_sub |- !r. Ring r ==> !p q x. poly p /\ poly q /\ x IN R ==> (eval (p - q) x = eval [all...] |
H A D | polyBinomialScript.sml | 221 !x. x IN R ==> rlist (MAP (\p. eval p x) s) 223 !x. x IN R ==> (eval (poly_sum s) x = rsum (MAP (\p. eval p x) s)) 225 !n. eval (poly_sum (GENLIST f n)) x = rsum (MAP (\p. eval p x) (GENLIST f n)) 227 !n. eval (poly_sum (GENLIST (\k. f k * p ** k) n)) x = 228 rsum (GENLIST (\k. f k * eval p x ** k) n) 230 (eval p x = rsum (GENLIST (\k. p ' k * x ** k) (SUC (deg p)))) 2395 (* Theorem: poly_list s ==> !x. x IN R ==> rlist (MAP (\p. eval p x) s) *) 2398 Base case: poly_list [] ==> rlist (MAP (\p. eval [all...] |
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | internal_functions.sml | 294 fun function_call (fnname, args, eval) = let 303 val condition_evalled = eval condition 305 if condition_evalled <> "" then eval (List.nth(args, 1)) 306 else if length args = 3 then eval (List.nth(args, 2)) 313 val args_evalled = map eval args 324 val args_evalled = map eval args 334 Systeml.protect (eval (hd args)) 337 else subst(" ", "\\ ", eval (hd args)) 342 val (findstr, instr) = case map eval args of 353 val arg_evalled = eval (h [all...] |
H A D | internal_functions.sig | 65 [function_call(fnname, args, eval)] evaluates the internal function 69 by the eval function.
|
/seL4-l4v-master/HOL4/examples/lambda/other-models/ |
H A D | diagsScript.sml | 20 eval (Fa : ('n # 'a # 'a # bool # reltype) -> bool) 41 ``eval {(0,0,1,T,Atomic); (0,0,2,T,Atomic)} 57 ``eval {} {(0, INL 0, INL 1, T, Atomic)} R = !x y. R 0 x y``, 64 ``eval {(0,0,1,T,Atomic); (0,0,2,T,TC)} 80 ``eval {(0,0,1,T,Atomic)} 92 ``eval Fa {} R' = T``, 97 ``eval {(0,0,1,T,Atomic)} 112 ``eval {(0,0,1,T,Atomic); (0,0,2,T,Atomic)} 124 ``eval {} {(0,INR 0,INL 0,F,Atomic)} R = !y. ?x. ~R 0 x y``, 145 (evalform (Lf fa ex) R <=> eval f [all...] |
/seL4-l4v-master/HOL4/src/tactictoe/src/ |
H A D | tttSetup.sml | 20 val ttt_eval_dir = tactictoe_dir ^ "/eval"
|
/seL4-l4v-master/HOL4/examples/fun-op-sem/ml/ |
H A D | typeSoundScript.sml | 318 (eval env s (Lit i) (Rval (Litv i), s)) ��� 320 eval env s (Var x) (Rfail, s)) ��� 322 eval env s (Var x) (Rval v, s)) ��� 323 (eval env s e1 (Rval v1, s1) ��� 324 eval env s1 e2 (Rval v2, s2) ��� 326 eval env' (dec_clock s2) e res 328 eval env s (App e1 e2) res) ��� 329 (eval env s e1 (Rval v1, s1) ��� 330 eval env s1 e2 (Rval v2, s2) ��� 333 eval en [all...] |
/seL4-l4v-master/HOL4/src/integer/ |
H A D | jrhCore.sml | 57 val eval = MK_COMB (AP_TERM (rator (rator tm)) eval1, eval2) value 60 TRANS eval (binop_rwt_CONV (rand (concl eval))) 65 val eval = AP_TERM (rator tm) eval0 value 67 TRANS eval (REWR_CONV negn_rwt (rand (concl eval))) 183 profile "eb.eval" eval_f_CONV THENC
|
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/ |
H A D | arm_evalLib.sml | 28 val eval = boolSyntax.rhs o Thm.concl o bossLib.EVAL; value 144 val _ = Feedback.register_trace ("arm eval", arm_eval_trace, 6); 218 Term.mk_comb(``arm_coretypes$encode_psr``, tm) |> eval |> hex 8 220 fun registers s = case (``^s.registers`` |> eval |> dest_strip) 226 fun psrs s = case (``^s.psrs`` |> eval |> dest_strip) 233 |> eval 288 let val l = ``^s.accesses`` |> eval |> listSyntax.dest_list |> fst in 376 fun decode_psr n = Term.mk_comb(``arm_coretypes$decode_psr``, n) |> eval 504 |> eval
|
/seL4-l4v-master/HOL4/src/float/ |
H A D | floatScript.sml | 21 fun eval thms = rhs o concl o EVAL' thms function 22 val expw_tm = eval [expwidth, float_format] ``expwidth float_format`` 23 val fracw_tm = eval [fracwidth, float_format] ``fracwidth float_format`` 24 val bias_tm = eval [bias, expwidth, float_format] ``bias float_format`` 25 val emax_tm = eval [emax, expwidth, float_format] ``emax float_format`` 26 val pemax_tm = eval [] ``^emax_tm - 1`` 27 val sfracw_tm = eval [] ``^fracw_tm + 1`` 28 val frac_tm = eval [] ``2 EXP ^fracw_tm`` 29 val pfrac_tm = eval [] ``&(^frac_tm - 1) : real`` 30 val exp_pemax_tm = eval [] `` [all...] |
/seL4-l4v-master/HOL4/examples/ARM/v4/ |
H A D | arm_evalLib.sig | 45 val eval : int * term * term * term -> thm list value
|