Searched refs:exp (Results 26 - 50 of 228) sorted by relevance

12345678910

/seL4-l4v-master/HOL4/examples/dev/sw/
H A DIR.sml13 val hashtable : ((string, (Tree.stm list * Tree.exp * Tree.exp)) Polyhash.hash_table) ref =
158 fun flow [] exp = exp
159 | flow (h::t) exp = Tree.ESEQ(h, flow t exp);
172 | mk_PAIR exp =
175 fun analyzeExp exp =
177 if is_let exp then
178 let val (var, rhs) = dest_let exp;
398 val exp = (Tree.CALL (Tree.NAME s, e)); value
[all...]
H A DdeclFuncs.sml17 type func = {name : string, ftype : hol_type, ir : IRSyntax.exp * annotatedIR.anntIR * IRSyntax.exp,
H A DAssem.sml20 datatype exp = NAME of Temp.label type
24 | PAIR of exp * exp
25 | CALL of exp * exp
36 dst: exp list,
37 src: exp list,
40 | MOVE of {dst: exp,
41 src: exp};
147 fun one_exp exp
[all...]
H A DIRSyntax.sml22 datatype exp = NCONST of Arbint.int type
24 | PAIR of exp * exp
33 type instr = {oper: operator, dst: exp list, src: exp list}
376 ( List.map (fn exp => update_mode exp READ) src1;
377 List.map (fn exp => update_mode exp WRITE) dst1
476 format_exp (hd sList) ^ itlist (curry (fn (exp,st
[all...]
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/
H A DholfootParserGenpreds.sml99 fun mk_holfoot_ap_tree_absyn (tagL, tagR, exp) =
101 Absyn.mk_pair (tagL, tagR), exp])
105 fn [exp] => mk_holfoot_ap_tree_absyn (
108 exp));
112 fn [tagL, tagR, exp] => mk_holfoot_ap_tree_absyn (
113 tagL,tagR,exp));
116 fun mk_holfoot_ap_data_tree_absyn (tagL, exp, dtagL, data) =
118 tagL, exp,
123 fn [exp,data] => mk_holfoot_ap_data_tree_absyn (
126 exp,
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DdeclFuncs.sml17 type func = {name : string, ftype : hol_type, ir : IRSyntax.exp * annotatedIR.anntIR * IRSyntax.exp,
H A DAssem.sml20 datatype exp = NAME of Temp.label type
24 | PAIR of exp * exp
25 | CALL of exp * exp
36 dst: exp list,
37 src: exp list,
40 | MOVE of {dst: exp,
41 src: exp};
147 fun one_exp exp
[all...]
H A DIRSyntax.sml22 datatype exp = NCONST of Arbint.int type
24 | PAIR of exp * exp
33 type instr = {oper: operator, dst: exp list, src: exp list}
368 ( List.map (fn exp => update_mode exp READ) src1;
369 List.map (fn exp => update_mode exp WRITE) dst1
468 format_exp (hd sList) ^ itlist (curry (fn (exp,st
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DdeclFuncs.sml17 type func = {name : string, ftype : hol_type, ir : IRSyntax.exp * annotatedIR.anntIR * IRSyntax.exp,
H A DAssem.sml20 datatype exp = NAME of Temp.label type
24 | PAIR of exp * exp
25 | CALL of exp * exp
36 dst: exp list,
37 src: exp list,
40 | MOVE of {dst: exp,
41 src: exp};
147 fun one_exp exp
[all...]
H A DIRSyntax.sml22 datatype exp = NCONST of Arbint.int type
24 | PAIR of exp * exp
33 type instr = {oper: operator, dst: exp list, src: exp list}
368 ( List.map (fn exp => update_mode exp READ) src1;
369 List.map (fn exp => update_mode exp WRITE) dst1
468 format_exp (hd sList) ^ itlist (curry (fn (exp,st
[all...]
/seL4-l4v-master/HOL4/examples/hardware/hol88/mos-count/
H A Dmisc.ml4 new_parent `exp`;;
5 let EXP = theorem `exp` `EXP`;;
/seL4-l4v-master/HOL4/src/Boolify/test/
H A Dtest.sml81 `exp = VAR of 'a
82 | IF of bexp => exp => exp
83 | APP of 'b => exp list
85 bexp = EQ of exp => exp
86 | LEQ of exp => exp
/seL4-l4v-master/HOL4/polyml/basis/
H A DIEEEReal.sml78 { class : float_class, sign : bool, digits : int list, exp : int }
84 fun toString {class, sign=true, digits, exp} = (* Sign bit set *)
85 "~" ^ toString {class=class, sign=false, digits=digits, exp=exp}
89 | toString {digits, exp, ...} = (* NORMAL or SUBNORMAL *)
91 (if exp = 0 then "" else "E"^(Int.toString exp))
178 SOME ({class=ZERO, sign=sign, digits=[], exp=0}, src4)
182 exp=exponent + List.length leading}, src4)
186 SOME src' => SOME ({class=INF, sign=sign, digits=[], exp
[all...]
H A DReal.sml47 and exp = Real.rtsCallFastR_R "PolyRealExp" value
61 val e = exp one
147 then {man=r, exp=0}
150 val (exp, man) = frExp r value
152 {man=man, exp=exp}
155 fun fromManExp {man, exp} =
160 else if LibrarySupport.isShortInt exp
161 then fromManAndExp(man, exp)
163 copySign(if Int.>(exp,
[all...]
/seL4-l4v-master/HOL4/examples/algebra/group/
H A DgroupInstancesScript.sml83 Zadd_exp |- !n. 0 < n ==> !x m. (Z n).exp x m = (x * m) MOD n
102 Zstar_exp |- !p a. prime p /\ a IN (Z* p).carrier ==> !n. (Z* p).exp a n = a ** n MOD p
106 ((Z* p).inv x = (Z* p).exp x (order (Z* p) x - 1))
108 then (Z* p).exp x (order (Z* p) x - 1)
131 Estar_exp |- !n a. 1 < n /\ a IN (Estar n).carrier ==> !k. (Estar n).exp a k = a ** k MOD n
185 add_mod_exp |- !n. 0 < n ==> !x m. (add_mod n).exp x m = (x * m) MOD n
209 mult_mod_exp |- !p a. prime p /\ a IN (mult_mod p).carrier ==> !n. (mult_mod p).exp a n = a ** n MOD p
213 ((mult_mod p).inv x = (mult_mod p).exp x (order (mult_mod p) x - 1))
215 then (mult_mod p).exp x (order (mult_mod p) x - 1)
357 (* Theorem: 0 < n ==> !x m. (Z n).exp
[all...]
/seL4-l4v-master/HOL4/examples/algebra/ring/
H A DringInstancesScript.sml98 ZN_exp |- !n. 0 < n ==> !x k. (ZN n).prod.exp x k = x ** k MOD n
99 ZN_num |- !n. 0 < n ==> !k. (ZN n).sum.exp 1 k = k MOD n
100 ZN_num_1 |- !n. (ZN n).sum.exp (ZN n).prod.id 1 = 1 MOD n
101 ZN_num_0 |- !n c. 0 < n ==> (ZN n).sum.exp 0 c = 0
102 ZN_num_mod |- !n c. 0 < n ==> (ZN n).sum.exp (ZN n).prod.id c = c MOD n
114 ZN_1_exp |- !n k. (ZN 1).prod.exp n k = 0
493 (ZN n).sum.exp 1 n
496 Hence (ZN n).sum.exp 1 n = 0
500 (ZN n).sum.exp 1 m
513 `(ZN n).sum.exp
[all...]
/seL4-l4v-master/HOL4/examples/acl2/examples/LTL/
H A DCOIRScript.sml58 `exp = CONST of 'val
60 | UNOP of ('val -> 'val) => exp
61 | BINOP of ('val -> 'val -> 'val) => (exp # exp)`;
79 * of equations, represented as a value of type (string#exp)set, as
87 * ((string |-> 'val)set # (string # ('val)exp)set))
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_compiler_opScript.sml1587 BC_is_reserved_name exp =
1588 if MEM exp (MAP Sym macro_names) then Val 0 else
1589 if MEM exp (MAP Sym reserved_names) then exp else Sym "NIL"`;
1625 ``!exp. mc_is_reserved_name exp = BC_is_reserved_name exp``,
1939 BC_expand_macro (temp:SExp,task,exp,a,ret,consts,xs) =
1940 let temp = exp in
1941 let exp
[all...]
/seL4-l4v-master/HOL4/examples/elliptic/
H A DAlgebra.sml182 fun isInt exp = Option.isSome (toInt exp);
295 else raise Error "explSubtract*: wrong exp"
346 fun normalize {equations} exp =
348 val _ = print ("normalize: input =\n" ^ toString exp ^ "\n")
349 val exp = repeat_norm equations exp value
350 val _ = print ("normalize: result =\n" ^ toString exp ^ "\n")
352 exp
/seL4-l4v-master/HOL4/src/num/arith/src/
H A DNorm_arith.sml201 (* SUC (const + exp) ---> const' + exp *)
202 (* SUC (exp + const) ---> const' + exp *)
250 (* 0 * exp ---> 0 *)
251 (* exp * 0 ---> 0 *)
253 (* exp * const ---> SOPM (const * exp) *)
385 (* const + exp ---> const + exp (
[all...]
/seL4-l4v-master/HOL4/src/holyhammer/examples/
H A Dhh_demoScript.sml44 (* hh ([], ``exp (i * (2 * pi)) = 1``); set_timeout 60; *)
/seL4-l4v-master/HOL4/examples/algebra/finitefield/
H A DffBasicScript.sml46 val _ = overload_on ("ring_numr", ``r.sum.exp #1``); (* for fallback *)
47 val _ = overload_on ("##", ``r.sum.exp #1``); (* current use *)
48 val _ = overload_on ("**", ``r.prod.exp``);
53 val _ = overload_on ("##", ``(PolyRing r).sum.exp |1|``);
54 val _ = overload_on ("**", ``(PolyRing r).prod.exp``);
79 ((PF r).prod.exp = $** )
133 <| carrier := IMAGE (r.sum.exp #1) univ(:num);
134 sum := <| carrier := IMAGE (r.sum.exp #1) univ(:num); op := r.sum.op; id := #0 |>;
135 prod := <| carrier := IMAGE (r.sum.exp #1) univ(:num); op := r.prod.op; id := #1 |>
141 For the last one: (PF r).prod.exp
[all...]
/seL4-l4v-master/HOL4/examples/formal-languages/context-free/
H A Dselftest.sml27 fun test (s, exp) = let
28 val exp_t = ``Result (SOME ([], ^exp)) : (char, sexpNT, sexp) evalcase``
/seL4-l4v-master/HOL4/src/metis/
H A DmlibModel.sig22 val modulo_fix : fix (* 0 1 2 suc pre ~ + - * exp mod *)
24 val heap_fix : fix (* 0 1 2 suc pre + - * exp < <= > >= is_0 *)

Completed in 160 milliseconds

12345678910