/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | IR.sml | 13 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 D | declFuncs.sml | 17 type func = {name : string, ftype : hol_type, ir : IRSyntax.exp * annotatedIR.anntIR * IRSyntax.exp,
|
H A D | Assem.sml | 20 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 D | IRSyntax.sml | 22 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 D | holfootParserGenpreds.sml | 99 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 D | declFuncs.sml | 17 type func = {name : string, ftype : hol_type, ir : IRSyntax.exp * annotatedIR.anntIR * IRSyntax.exp,
|
H A D | Assem.sml | 20 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 D | IRSyntax.sml | 22 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 D | declFuncs.sml | 17 type func = {name : string, ftype : hol_type, ir : IRSyntax.exp * annotatedIR.anntIR * IRSyntax.exp,
|
H A D | Assem.sml | 20 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 D | IRSyntax.sml | 22 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 D | misc.ml | 4 new_parent `exp`;; 5 let EXP = theorem `exp` `EXP`;;
|
/seL4-l4v-master/HOL4/src/Boolify/test/ |
H A D | test.sml | 81 `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 D | IEEEReal.sml | 78 { 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 D | Real.sml | 47 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 D | groupInstancesScript.sml | 83 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 D | ringInstancesScript.sml | 98 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 D | COIRScript.sml | 58 `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 D | lisp_compiler_opScript.sml | 1587 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 D | Algebra.sml | 182 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 D | Norm_arith.sml | 201 (* 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 D | hh_demoScript.sml | 44 (* hh ([], ``exp (i * (2 * pi)) = 1``); set_timeout 60; *)
|
/seL4-l4v-master/HOL4/examples/algebra/finitefield/ |
H A D | ffBasicScript.sml | 46 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 D | selftest.sml | 27 fun test (s, exp) = let 28 val exp_t = ``Result (SOME ([], ^exp)) : (char, sexpNT, sexp) evalcase``
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibModel.sig | 22 val modulo_fix : fix (* 0 1 2 suc pre ~ + - * exp mod *) 24 val heap_fix : fix (* 0 1 2 suc pre + - * exp < <= > >= is_0 *)
|