Searched refs:eval (Results 1 - 25 of 112) sorted by relevance

12345

/seL4-l4v-master/HOL4/examples/hardware/hol88/MISC/
H A Dinit.ml5 lisp `(load 'eval)`;;
H A Deval-test.ml1 % 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 Dgithub462Script.sml13 "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 DpegML.sml61 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 Dsource_semanticsScript.sml186 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 Dpred_setLib.sml21 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 DffExtendScript.sml150 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 DffMinimalScript.sml107 !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 DffPolyScript.sml262 (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 DpolyRootScript.sml91 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 DpolyWeakScript.sml64 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 DpolyMultiplicityScript.sml1146 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 DpolyDivisionScript.sml202 !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 DpolyEvalScript.sml106 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 DpolyRingScript.sml375 # 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 DpolyBinomialScript.sml221 !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 Dinternal_functions.sml294 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 Dinternal_functions.sig65 [function_call(fnname, args, eval)] evaluates the internal function
69 by the eval function.
/seL4-l4v-master/HOL4/examples/lambda/other-models/
H A DdiagsScript.sml20 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 DtttSetup.sml20 val ttt_eval_dir = tactictoe_dir ^ "/eval"
/seL4-l4v-master/HOL4/examples/fun-op-sem/ml/
H A DtypeSoundScript.sml318 (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 DjrhCore.sml57 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 Darm_evalLib.sml28 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 DfloatScript.sml21 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 Darm_evalLib.sig45 val eval : int * term * term * term -> thm list value

Completed in 218 milliseconds

12345