/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/ |
H A D | Tree.sml | 8 | CJUMP of exp * Temp.label 9 | MOVE of exp * exp 10 | EXP of exp 12 and exp = BINOP of binop * exp * exp type 13 | RELOP of relop * exp * exp 14 | MEM of exp [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | Tree.sml | 8 | CJUMP of exp * Temp.label 9 | MOVE of exp * exp 10 | EXP of exp 12 and exp = BINOP of binop * exp * exp type 13 | RELOP of relop * exp * exp 14 | MEM of exp 47 and exp = BINOP of binop * exp * exp type [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | Tree.sml | 8 | CJUMP of exp * Temp.label 9 | MOVE of exp * exp 10 | EXP of exp 12 and exp = BINOP of binop * exp * exp type 13 | RELOP of relop * exp * exp 14 | MEM of exp 47 and exp = BINOP of binop * exp * exp type [all...] |
H A D | IR.sml | 149 fun flow [] exp = exp 150 | flow (h::t) exp = Tree.ESEQ(h, flow t exp); 163 | mk_PAIR exp = 166 fun analyzeExp exp = 168 if is_let exp then 169 let val (var, rhs) = dest_let exp; 176 else if is_numeral exp then 177 Tree.NCONST (Arbint.fromNat (dest_numeral exp)) [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
H A D | lisp_evalScript.sml | 9 val renamer = Q.INST [`x1`|->`exp`,`x2`|->`x`,`x3`|->`y`,`x4`|->`z`,`x5`|->`stack`,`x6`|->`alist`] o INST [``limit:num``|->``l:num``] 18 val renamer = Q.INST [`x1`|->`exp`,`x2`|->`x`,`x3`|->`y`,`x4`|->`z`,`x5`|->`stack`,`x6`|->`alist`] o INST [``limit:num``|->``l:num``] 27 val renamer = Q.INST [`x1`|->`exp`,`x2`|->`x`,`x3`|->`y`,`x4`|->`z`,`x5`|->`stack`,`x6`|->`alist`] o 38 val STATE = ``(exp:SExp,x:SExp,y:SExp,z:SExp,stack:SExp,alist:SExp,l:num)`` 45 if exp = x then 47 let exp = CDR x in 55 let (exp,x,y,z,stack,alist,l) = lookup_aux ^STATE in 60 let alist = exp in 61 let exp = CAR y in 63 let exp [all...] |
/seL4-l4v-master/HOL4/examples/bootstrap/ |
H A D | source_syntaxScript.sml | 22 exp = Const num (* constant number *) 24 | Op op (exp list) (* primitive operations *) 25 | If test (exp list) exp exp (* if test .. then .. else .. *) 26 | Let name exp exp (* let name = .. in .. *) 27 | Call name (exp list) (* call a function *) 31 dec = Defun name (name list) exp (* func name, formal params, body *) 35 prog = Program (dec list) exp (* functio [all...] |
/seL4-l4v-master/HOL4/tools/mlyacc/src/ |
H A D | absyn-sig.sml | 22 datatype exp = EVAR of string type 23 | EAPP of exp * exp 24 | ETUPLE of exp list 26 | FN of pat * exp 27 | LET of decl list * exp 29 | SEQ of exp * exp 38 and decl = VB of pat * exp 39 and rule = RULE of pat * exp [all...] |
H A D | absyn.sml | 26 datatype exp type 28 | EAPP of exp * exp 30 | ETUPLE of exp list 32 | FN of pat * exp 33 | LET of decl list * exp 34 | SEQ of exp * exp 44 and decl = VB of pat * exp 45 and rule = RULE of pat * exp [all...] |
/seL4-l4v-master/HOL4/examples/hardware/hol88/mos-count/ |
H A D | exp.ml | 1 new_theory `exp`;;
|
/seL4-l4v-master/HOL4/src/boss/theory_tests/ |
H A D | github416Script.sml | 5 val _ = Datatype `exp = Const num num | Downcast num exp`; 8 test (e:exp) (map: exp -> num option) : bool =
|
H A D | github462Script.sml | 5 val _ = Datatype ���exp = Lit num | Log exp exp���; 7 val _ = Datatype ���exp_or_val = Exp exp | Val num���;
|
/seL4-l4v-master/HOL4/examples/Hoare-for-divergence/ |
H A D | while_langScript.sml | 12 Type exp = ���: store -> value ��� 16 | Assign name exp 17 | Print exp 19 | If exp prog prog 20 | While exp prog
|
/seL4-l4v-master/HOL4/polyml/modules/IntInfAsInt/ |
H A D | RealStringCvt.sml | 25 { class : float_class, sign : bool, digits : int list, exp : int } 28 fun toNewDA {class, sign, digits, exp } : decimal_approx = 29 {class=class, sign=sign, digits = map FixedInt.toLarge digits, exp = FixedInt.toLarge exp } 30 and fromNewDA ({class, sign, digits, exp } : decimal_approx) = 31 {class=class, sign=sign, digits = map FixedInt.fromLarge digits, exp = FixedInt.fromLarge exp } 64 val toManExp = fn r => let val {man, exp} = toManExp r in {man=man, exp= FixedInt.toLarge exp} en [all...] |
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/parse/ |
H A D | lisp_parseScript.sml | 419 ``!exp b abbrevs ps xs1 xs2 ps1 ps2. 420 ((xs1,ps1) = sexp2abbrev_aux exp b abbrevs ps) ==> 421 ((xs2,ps2) = sexp2abbrevt_aux exp b abbrevs ps) ==> 425 \\ Q.ABBREV_TAC `index = abbrevs ' exp` 427 \\ Q.ABBREV_TAC `t_prefix = if exp IN FDOM abbrevs then [(Val index,Val 2)] else []` 428 \\ Q.ABBREV_TAC `s_prefix = if exp IN FDOM abbrevs then STRCAT (STRCAT "#" (num2str index)) "=" else ""` 429 \\ `?t_str1 t_ps1. sexp2abbrevt_aux (CAR exp) T abbrevs ps = (t_str1,t_ps1)` by METIS_TAC [PAIR] 430 \\ `?t_str2 t_ps2. sexp2abbrevt_aux (CDR exp) F abbrevs t_ps1 = (t_str2,t_ps2)` by METIS_TAC [PAIR] 431 \\ `?t_str3 t_ps3. sexp2abbrevt_aux (CAR (CDR exp)) T abbrevs ps = (t_str3,t_ps3)` by METIS_TAC [PAIR] 432 \\ `?s_str1 s_ps1. sexp2abbrev_aux (CAR exp) [all...] |
/seL4-l4v-master/HOL4/src/0/ |
H A D | Subst.sml | 74 let fun exp (lams, Id, n) = (lams+n, NONE) function 75 | exp (lams, Cons(s,x), 0) = (lams, SOME x) 76 | exp (lams, Cons(s,x), n) = exp(lams, s, n-1) 77 | exp (lams, Shift(k,s), n) = exp(lams+k, s, n) 78 | exp (lams, Lift(k,s), n) = if n < k then (lams+n, NONE) 79 else exp(lams+k, s, n-k) 80 in exp(0,subs,db)
|
/seL4-l4v-master/HOL4/examples/MLsyntax/ |
H A D | MLScript.sml | 33 * | "let" <dec> "in" <exp> "end" * 35 * exp ::= <atexp> * 36 * | <exp> <atexp> * 42 * rule ::= <pat> "=>" <exp> * 48 * valbind ::= <pat> "=" <exp> * 49 * | <pat> "=" <exp> "and" <valbind> * 79 | let_exp dec exp ; 81 exp = aexp atexp 82 | app_exp exp atexp 88 rule = rule pat exp ; [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | regAlloc.sml | 67 fun is_fun exp = 68 (* is_var exp andalso *) 69 (#1 (dest_type (type_of exp)) = "fun") 92 fun fv exp = 93 let val xs = free_vars exp 242 fun save x exp regenv = 249 in (* let m[.] = r[.] in exp[m[.]] *) 250 (mk_plet (v, M.find(regenv,x), exp), regenv1) 253 fun restore x exp regenv = 260 subst_exp [x |-> v] exp) (* le 373 let val (exp,regenv) = value 591 val exp = subst [src |-> args] (subst [v |-> M] N) value [all...] |
H A D | basic.sml | 150 fun last_exp exp = 151 if is_let exp then 152 last_exp (#3 (dest_plet exp)) 153 else exp; 160 fun subst_exp rule exp = 161 if is_plet exp then 162 let val (v, M, N) = dest_plet exp 166 else if is_cond exp then 167 let val (c,t,f) = dest_cond exp 171 else if is_pair exp the [all...] |
H A D | Normal.sml | 71 fun norm_mult (th0,th1) (d0,d1) exp = 75 (ONCE_REWRITE_CONV [C_BINOP,C_WORDS_BINOP] exp) 77 SUBST_2_RULE (REWRITE_RULE [Once ATOM_ID] th0,th1) (ONCE_REWRITE_CONV [C_BINOP,C_WORDS_BINOP] exp) 81 SUBST_2_RULE (th0, REWRITE_RULE [Once ATOM_ID] th1) (ONCE_REWRITE_CONV [C_BINOP,C_WORDS_BINOP] exp) 83 SUBST_2_RULE (th0,th1) (ONCE_REWRITE_CONV [C_BINOP,C_WORDS_BINOP] exp) 88 fun Normalize_Atom_Cond (lem0,lem1,lem2,lem3) exp = 90 val th1 = ONCE_REWRITE_CONV [C_ATOM_COND] exp 106 fun Normalize_Atom_Cond_Ex (lem0,lem1,lem2,lem3) exp = 108 val th1 = ONCE_REWRITE_CONV [C_ATOM_COND_EX] exp 142 fun K_Normalize exp 282 val exp = mk_C (rhs (concl (SPEC_ALL thm1))) value [all...] |
H A D | SALGen.sml | 67 type spec_type = {body : term, dst : term, entry : term, exit : term, exp : term, thm : thm} 80 {entry = entry_l, exit = exit_l, body = instr, thm = spec_thm, exp = src, dst = dest} 88 val exp = mk_plet (#dst spec1, #exp spec1, value 89 mk_comb(mk_pabs (#dst spec1, #exp spec2), #dst spec1)) 90 val value = mk_pair(exp, #dst spec2) 102 {entry = #entry spec1, exit = #exit spec2, body = union_body, thm = spec_thm, exp = exp, dst = #dst spec2} 138 val exp = mk_cond (mk_comb(c,args), value 139 mk_comb(mk_pabs(args, #exp spec [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | IR.sml | 149 fun flow [] exp = exp 150 | flow (h::t) exp = Tree.ESEQ(h, flow t exp); 163 | mk_PAIR exp = 166 fun analyzeExp exp = 168 if is_let exp then 169 let val (lt, rhs) = dest_let exp; 176 else if is_numeral exp then 177 Tree.NCONST (Arbint.fromNat (dest_numeral exp)) [all...] |
/seL4-l4v-master/HOL4/src/datatype/mutrec/examples/ |
H A D | example.sml | 26 | let <dec> in <exp> end 28 exp ::= <atexp> 29 | <exp> <atexp> 35 rule ::= <pat> => <exp> 41 valbind ::= <pat> = <exp> 42 | <pat> = <exp> and <valbind> 57 being_defined "exp"]}]}, 58 {type_name = "exp", 61 {name = "app_exp", arg_info = [being_defined "exp", 72 being_defined "exp"]}]}, [all...] |
H A D | var_example.sml | 20 being_defined "exp"]}]}, 21 {type_name = "exp", 24 {name = "app_exp", arg_info = [being_defined "exp", 35 being_defined "exp"]}]}, 46 being_defined "exp"]}, 48 being_defined "exp",
|
/seL4-l4v-master/HOL4/examples/miller/formalize/ |
H A D | extra_realScript.sml | 942 (* --------------------- exp is a convex function -------------------------- *) 957 ``!t. (t + (1 - t) * exp 0 - exp ((1 - t) * 0) = 0) /\ 958 (t * exp 0 + (1 - t) - exp (t * 0) = 0)``, 963 ``!t x. ((\x. (1 - t) * exp x - exp ((1 - t) * x)) diffl 964 (\x. (1-t) * exp x - (1 - t)*exp ((1-t)*x)) x) x``, 966 >> `(\x. (1 - t) * exp [all...] |
/seL4-l4v-master/HOL4/examples/elliptic/c_output/ |
H A D | c_outputLib.sml | 208 val (exp, n) = (true_exp, 1); 211 fun translate_exp exp n = 213 fun translate_bool_exp exp = 214 if (exp = T) then ([], "1") 215 else if (exp = F) then ([], "0") 216 else if (is_neg exp) then 218 val exp' = dest_neg exp; 219 val (inst, exp_s) = translate_bool_exp exp'; 223 else if (is_conj exp) the [all...] |