Searched refs:mk_var (Results 51 - 75 of 368) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/pfl/
H A Dindex.sml143 val v = variant vs (mk_var("v",ty))
171 val v = variant (free_vars tm) (mk_var("v",bool))
186 val v = variant (free_vars tm) (mk_var("v",type_of ob))
220 fvar |-> mk_var(pfname, ty')
229 fvar |-> mk_comb(mk_var(ifname, ty'),d)
237 let val v = variant away (mk_var(name,ty))
291 val d = variant vars (mk_var("d",num))
315 (variant (all_vars base_case)) (mk_var(lim_name,num))
330 val pfn_var = mk_var(pfn_name,ty)
341 val fn_var = mk_var(nam
[all...]
H A DpflLib.sml53 val a = variant argfrees (mk_var("a",ty))
66 val d1 = variant argfrees (mk_var("d1",num))
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/Solitaire/
H A DMiniTLHexSolitaireScript.sml63 if n<10 then mk_var("v0"^(int_to_string n),bool)
64 else mk_var("v"^(int_to_string n),bool);
71 if n<10 then mk_var("v0"^(int_to_string n)^"'",bool)
72 else mk_var("v"^(int_to_string n)^"'",bool);
95 (fn s => mk_var(s,bool))
199 (mk_var("s",type_of s))
/seL4-l4v-10.1.1/HOL4/src/1/
H A DRsyntax.sml10 fun mk_var{Name,Ty} = Term.mk_var(Name,Ty) function
H A DPsyntax.sig8 val mk_var : string * hol_type -> term value
H A DboolSyntax.sml272 val f = mk_var(dest_const f) handle HOL_ERR _ => f
341 val f = mk_var ("f", alpha --> alpha --> alpha)
342 val g = mk_var ("g", alpha --> alpha --> alpha)
343 val g1 = mk_var ("g", alpha --> alpha)
344 val x = mk_var ("x", alpha)
345 val y = mk_var ("y", alpha)
346 val z = mk_var ("z", alpha)
/seL4-l4v-10.1.1/HOL4/src/boss/
H A Dselftest.sml83 val P = mk_var("P",bool)
84 val Q = mk_var("Q",bool)
/seL4-l4v-10.1.1/HOL4/examples/logic/
H A DfoltypesScript.sml44 val VAR_t = mk_var("VAR", ``:string -> ^term_ty``)
53 val FN_t = mk_var("FN", ``:string -> ^term_ty list -> ^term_ty``)
103 val ALL_t = mk_var("ALL", ``:string -> ^form_ty -> ^form_ty``)
113 val REL_t = mk_var("REL", ``:string -> ^term_ty list -> ^form_ty``)
129 val FALSE_t = mk_var("FALSE", ``:^form_ty``)
141 val IMP_t = mk_var("IMP", ``:^form_ty -> ^form_ty -> ^form_ty``)
191 val t = mk_var("t", term_ty)
249 val t = mk_var("f", form_ty)
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/
H A Ddefunctionalize.sml237 in mk_var(name, type2closure tp)
248 handle e => mk_var("dispatch" ^ f_index, (* the dispatch function has not been defined *)
273 val df_var = mk_var(df_name, df_type)
296 val new_fname = mk_var(new_name, new_f_type)
337 val v' = mk_var (#1 (dest_var v), type_of M')
376 mk_var(#1 (dest_const M) handle _ => #1 (dest_var M),
388 NONE => mk_var(#1 (dest_const t) handle _ => #1 (dest_var t),
406 val new_fname = mk_var(new_fname_str, new_f_tp)
478 val new_args = if is_fun args then mk_var (new_arg_str, type2closure arg_tp)
481 let val input = mk_var("
[all...]
/seL4-l4v-10.1.1/HOL4/src/parse/
H A Dselftest.sml398 val mk_var = Term.mk_var value
402 val CONS_t = mk_var("CONS", bool --> (bool --> bool))
403 val NIL_t = mk_var("NIL", bool)
416 mk_list00 elty n c (map (fn c => mk_var(str c, elty)) (String.explode s))
494 val fx = mk_comb(mk_var("f", alpha --> bool), mk_var("x", alpha))
495 val y = mk_var("y", bool)
563 (mk_comb(cEMP_t, mk_var("x", alpha)))
566 (mk_comb(pbmk_list "x", mk_var("
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A DencodeLib.sml205 mk_var(mk_encode_string t,get_encode_type target t)
208 mk_var(mk_decode_string t,get_decode_type target t)
211 mk_var(mk_detect_string t,get_detect_type target t)
214 mk_var(mk_map_string t,get_map_type t)
217 mk_var(mk_fix_string t,get_fix_type target t)
220 mk_var(mk_all_string t,get_all_type t)
223 mk_var(mk_fix_string t,get_fix_type target t)
330 val vars = map (mk_var o (implode o base26 ## I)) (enumerate 0 list)
352 val label = mk_var("l",num)
353 val rest = mk_var("
[all...]
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractLib.sml222 val rw = Define `^(mk_eq(mk_var(name,type_of z),z))`
315 val xs3 = map (fn x => mk_var(simplify_name(fst x),``:SExp``)) xs
350 val new_var = mk_var(new_name,type_of x)
383 |> map (fn s => mk_var(simplify_name s,``:SExp``))
385 val v = mk_var("__result__",``:SExp list -> SExp``)
403 val new_fun = mk_var(good_name,ty)
447 |> map (fn s => mk_var(simplify_name s,``:SExp``))
449 val v = mk_var("__" ^ name ^ "__result__",``:SExp list -> SExp``)
473 fun mk_tuple [] = mk_var("()",``:unit``)
482 val new_fun = mk_var(good_nam
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A DmechReasoning.sml75 mk_var ("v" ^ (i := !i + 1; Int.toString (!i)) , Type `:DATA`)
149 List.map (fn exp => (i := !i + 1; {redex = exp, residue = mk_var ("v" ^ (Int.toString (!i)), Type `:DATA`)})) expL
248 val st = mk_pair (mk_var ("regs", Type `:REGISTER |-> DATA`), mk_var ("mem", Type `:ADDR |-> DATA`));
297 val st' = mk_var ("st", Type `:DSTATE`);
340 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`);
411 val ir_abbr = mk_var ("ir", Type `:CTL_STRUCTURE`);
412 val st = mk_var ("st", Type `:DSTATE`);
534 val st = mk_var ("st", Type `:DSTATE`);
577 val ir_abbr = mk_var ("i
[all...]
/seL4-l4v-10.1.1/HOL4/src/Boolify/src/
H A DEncode.sml54 in mk_var(pass Name, Ty)
58 let val v = num_variant away (mk_var("f", vty --> bool_list))
83 (* mk_abs (mk_var ("v", ty), bool_nil) *)
153 mk_var(n, itlist (curry op-->) fparams_tyl (ty --> bool_list))
/seL4-l4v-10.1.1/HOL4/src/datatype/
H A DDataSize.sml12 fun Kzero ty = mk_abs(mk_var("v",ty), numSyntax.zero_tm)
33 in mk_var(pass Name, Ty)
38 val v = num_variant away (mk_var("f", fty))
115 mk_var(n, itlist (curry op-->) fparams_tyl (ty --> num))
H A Dind_types.sml52 let val v = variant avoid (mk_var(s^Int.toString n, h))
57 then [variant avoid (mk_var(s, hd tys))]
139 val x = mk_var("x", dom_ty)
171 and n_tm = mk_var("n",numSyntax.num)
184 (* val epstms = map (fn ty => mk_select(mk_var("v",ty),T_tm)) alltys *)
217 mk_eq(mk_var(cname,conty),list_mk_abs(args,condef))
226 val rels = map (fn s => mk_var(dest_vartype s,predty)) newtys
238 mk_comb(mk_var(dest_vartype argty,predty),arg)::sofar
240 val conc = mk_comb(mk_var(dest_vartype r,predty),lapp)
313 fun safeid_genvar ty = Term.mk_var(vary_to_avoid_constant
[all...]
/seL4-l4v-10.1.1/HOL4/src/hol88/
H A Dhol88Lib.sml71 then Term.variant L (Term.mk_var (Term.dest_const tm))
/seL4-l4v-10.1.1/HOL4/src/integer/testing/
H A Dgenproblem.sml7 val vars = map (fn s => mk_var(s, num)) ["u", "v", "x", "y", "z"]
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DSub_and_cond.sml79 val p = mk_var("p", numSyntax.num)
80 val n = mk_var("n", numSyntax.num)
214 val p = mk_var("p", bool)
215 val P = mk_var("P", bool --> bool)
/seL4-l4v-10.1.1/HOL4/src/patricia/
H A Dpatricia_castsLib.sml78 val thm2 = Definition.new_definition(s1^"_def", mk_eq(mk_var(s1,Term.type_of tree), tree))
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/
H A Dpred_setSimps.sml48 val f = mk_var ("f", beta --> mk_prod(alpha, bool))
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/
H A Darm_random_testingLib.sml633 fun reg tm = mk_var ("r" ^ Int.toString (uint_of_word tm), ``:word32``);
634 fun flag tm = mk_var (fst (dest_const tm), bool);
635 val arch = mk_var ("architecture",``:ARMarch``)
636 val cpsr = mk_var ("cpsr", ``:ARMpsr``)
637 val spsr = mk_var ("spsr", ``:ARMpsr``)
638 val GE = mk_var ("GE", ``:word4``)
639 val IT = mk_var ("IT", ``:word8``)
640 val teehbr = mk_var ("TEEHBR", ``:word32``)
641 val mode = mk_var ("mode", ``:word5``)
642 val mem = mk_var ("me
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/eval/
H A Darm_emitScript.sml33 FAIL bytes ^(mk_var("n not 1, 2 or 4",bool)) (w,n)`,
49 | _ => FAIL parallel_add_sub_op1 ^(mk_var("can't decode",bool)) w`,
62 | _ => FAIL parallel_add_sub_op2 ^(mk_var("can't decode",bool)) w`,
76 ^(mk_var("can't decode",bool)) w`,
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/
H A DcompilerLib.sml19 fun counter_genvar ty = mk_var("auto_"^ Arbnum.toString (inc()),ty)
203 val zs = map (fn (n,x) => pred_setSyntax.mk_in(x,mk_var("d"^n,``:word32 set``))) (xs1@xs2)
213 val cond_var = mk_var("cond",``:bool``)
217 val pre_f = mk_var(pre_name,mk_type ("fun",[type_of args, ``:bool``]))
238 val pre_f = mk_var(fname ^ "_pre",mk_type ("fun",[type_of args, ``:bool``]))
268 val s = map (fn c => c |-> mk_var(make_temp_name (fst (dest_const c)),type_of c)) cs
281 val s = [mk_var(make_temp_name(f),type_of x2c) |-> x2c]
/seL4-l4v-10.1.1/graph-refine/
H A Dlogic.py14 (mk_var, mk_plus, mk_uminus, mk_minus, mk_times, mk_modulus, mk_bwand, mk_eq,
58 return [mk_var (nm, typ) for (nm, typ) in tups]
111 return [syntax.mk_var (v, typ) for v in vs]
134 sp = mk_var ('r13', word32T)
135 st = mk_var ('stack', builtinTs['Mem'])
136 r0_input = mk_var ('r0_input', word32T)
139 ret = mk_var ('ret', word32T)
140 preconds = [mk_aligned (sp, 2), mk_eq (ret, mk_var ('r14', word32T)),
175 mem = mk_var ('mem', builtinTs['Mem'])
299 x = mk_var ('
[all...]

Completed in 306 milliseconds

1234567891011>>