/seL4-l4v-10.1.1/HOL4/src/pfl/ |
H A D | index.sml | 143 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 D | pflLib.sml | 53 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 D | MiniTLHexSolitaireScript.sml | 63 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 D | Rsyntax.sml | 10 fun mk_var{Name,Ty} = Term.mk_var(Name,Ty) function
|
H A D | Psyntax.sig | 8 val mk_var : string * hol_type -> term value
|
H A D | boolSyntax.sml | 272 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 D | selftest.sml | 83 val P = mk_var("P",bool) 84 val Q = mk_var("Q",bool)
|
/seL4-l4v-10.1.1/HOL4/examples/logic/ |
H A D | foltypesScript.sml | 44 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 D | defunctionalize.sml | 237 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 D | selftest.sml | 398 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 D | encodeLib.sml | 205 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 D | lisp_extractLib.sml | 222 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 D | mechReasoning.sml | 75 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 D | Encode.sml | 54 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 D | DataSize.sml | 12 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 D | ind_types.sml | 52 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 D | hol88Lib.sml | 71 then Term.variant L (Term.mk_var (Term.dest_const tm))
|
/seL4-l4v-10.1.1/HOL4/src/integer/testing/ |
H A D | genproblem.sml | 7 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 D | Sub_and_cond.sml | 79 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 D | patricia_castsLib.sml | 78 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 D | pred_setSimps.sml | 48 val f = mk_var ("f", beta --> mk_prod(alpha, bool))
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | arm_random_testingLib.sml | 633 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 D | arm_emitScript.sml | 33 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 D | compilerLib.sml | 19 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 D | logic.py | 14 (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...] |