Searched refs:exp (Results 1 - 25 of 228) sorted by relevance

12345678910

/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/
H A DTree.sml8 | 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 DTree.sml8 | 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 DTree.sml8 | 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 DIR.sml149 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 Dlisp_evalScript.sml9 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 Dsource_syntaxScript.sml22 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 Dabsyn-sig.sml22 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 Dabsyn.sml26 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 Dexp.ml1 new_theory `exp`;;
/seL4-l4v-master/HOL4/src/boss/theory_tests/
H A Dgithub416Script.sml5 val _ = Datatype `exp = Const num num | Downcast num exp`;
8 test (e:exp) (map: exp -> num option) : bool =
H A Dgithub462Script.sml5 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 Dwhile_langScript.sml12 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 DRealStringCvt.sml25 { 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 Dlisp_parseScript.sml419 ``!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 DSubst.sml74 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 DMLScript.sml33 * | "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 DregAlloc.sml67 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 Dbasic.sml150 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 DNormal.sml71 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 DSALGen.sml67 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 DIR.sml149 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 Dexample.sml26 | 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 Dvar_example.sml20 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 Dextra_realScript.sml942 (* --------------------- 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 Dc_outputLib.sml208 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...]

Completed in 171 milliseconds

12345678910