/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | graph_specsLib.sml | 14 val s_var = mk_var("s",``:state``) 53 in mk_var(str,ty) |-> tm end) 70 in mk_var(str,ty) |-> tm end) 75 (mk_var("count",``:num``) |->
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/ |
H A D | x64_compilerLib.sml | 19 fun counter_genvar ty = mk_var("auto_"^ Arbnum.toString (inc()),ty)
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | ctl2muTools.sml | 14 (*fun mk_bool_var v = mk_var(v,``:bool``);
|
H A D | ctlSyntax.sml | 109 val pvar = mk_var("p",p_ty)
|
H A D | ctlTools.sml | 136 val avar= mk_var("a",stringSyntax.string_ty) 142 val pvar = mk_var("p",stset_ty)
|
H A D | ksTools.sml | 41 fun mk_bool_var s = mk_var(s,bool) 48 else mk_var((term_to_string2 s)^"'",type_of s) 201 val cpvar = mk_var("p",cstate_type --> bool) 215 val avar= mk_var("t",stringLib.string_ty) 225 val pvar = mk_var("p",prop_type) 238 val Rvar = mk_var("R",(mk_prod(state_type,state_type)) --> bool)
|
H A D | cearTools.sml | 143 val res = PBETA_RULE (GEN_ALL (ISPECL [ksname,mk_var("e",stringLib.string_ty-->(type_of st1)-->bool),aht] th5)) 157 val nav = mk_var(navn,bool) 331 val gl2 = mk_forall(mk_var("e",stringLib.string_ty --> (type_of state) --> bool), 371 val Qvar = mk_var("Q",stringLib.string_ty) 372 val gvar = mk_var("g",mu_ty) 373 val avar = mk_var("a",stringLib.string_ty) 374 fun pvar p_ty = mk_var("p",p_ty) 474 val Qvar = mk_var("Q",stringLib.string_ty) 475 val svar = mk_var("s",s_ty) 477 val asvar = mk_var("s [all...] |
H A D | lzConv.sml | 627 val P = mk_var{Name=Pname, Ty=ty} 628 val Q = mk_var{Name=Qname, Ty=ty} 1338 val fv = mk_var{Name=Name, Ty = itlist mkfty xs Ty} 1386 val x = variant vars (mk_var{Name=varnm, Ty=ty1}) 1444 local val f = mk_var{Name="f",Ty=alpha-->bool} 1681 val P = mk_var{Name="P", Ty=alpha-->bool} 1713 val x = mk_var{Name="x",Ty=ty} 1714 and y = mk_var{Name="y",Ty=ty} 1715 and z = mk_var{Name="z",Ty=ty} 1791 val newv = mk_var{Nam [all...] |
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | TypeBase.sml | 354 rev ((mk_var("_",type_of p),v)::flatten (map snd lgs)) 397 [u,(mk_var("_",type_of p),v_rest)]
|
/seL4-l4v-10.1.1/HOL4/src/new-datatype/ |
H A D | NDDB.sml | 328 mk_abs (mk_var("x", alpha), 329 mk_abs (mk_var("y", one_ty),
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | problem.py | 9 from syntax import (Expr, mk_var, Node, true_term, false_term, namespace 67 return mk_var (name, typ) 711 return mk_var (nm, typ2) 737 out_vs = [mk_var (vs[v], typ) for (v, typ) in fun.outputs]
|
H A D | check.py | 23 from syntax import (true_term, false_term, boolT, mk_var, mk_word32, mk_word8, namespace 406 lsub = mksub (mk_plus (mk_var ('%n', word32T), 581 isub = mksub (mk_plus (mk_var ('%n', word32T), 630 return eq_hyp ((mk_var ('%n', word32T), visit), 810 v = syntax.mk_var ('#seq-visits', word32T)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/prog/ |
H A D | x64_progLib.sml | 49 List.tabulate (20, fn i => Term.mk_var ("opc" ^ Int.toString i, byte)) 131 val st = Term.mk_var ("s", ``:x64_state``)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/prog/ |
H A D | arm_progLib.sml | 131 val pc_tm = Term.mk_var ("pc", word) 299 val st = Term.mk_var ("s", ``:arm_state``) 592 val v3 = Term.mk_var ("x3", Type.bool) 593 val v4 = Term.mk_var ("x4", Type.bool) 594 val v5 = Term.mk_var ("x5", Type.bool) 595 val v6 = Term.mk_var ("x6", Type.bool)
|
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
H A D | Recftn.sml | 259 let val arg_var = mk_var {Name = "arg", Ty = ftn_dom} 414 (mk_var {Name = "r", Ty = rng_ty}) 466 (mk_var {Name = "r", Ty = rng_ty}) 476 (mk_var {Name = "r", Ty = rng_ty}) 563 val Pvar = mk_var {Name = "P", Ty = type_of Ptm} 564 val Qvar = mk_var {Name = "Q", Ty = type_of Ptm}
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | Induction.sml | 300 val a = variant FV0 (mk_var("a",type_of(Lib.trye hd pats))) 301 val z = variant (a::FV0) (mk_var("z",type_of a)) 430 val P = variant (all_varsl (pats@flatten TCsl)) (mk_var("P",domn-->bool)) 439 val v = variant (free_varsl (map concl proved_cases)) (mk_var("v",domn)) 525 val P = variant (all_varsl (pats@flatten TCsl)) (mk_var("P",domn-->bool)) 534 val v = variant (free_varsl (map concl proved_cases)) (mk_var("v",domn))
|
/seL4-l4v-10.1.1/HOL4/examples/dev/ |
H A D | compile.sml | 1108 (GEN_ALPHA_CONV (mk_var((s^Int.toString n),ty)) 1120 fun mkv ty = let val newv = mk_var((s^Int.toString(!count_ref)),ty) 1143 fun mkv ty = let val newv = mk_var((s^Int.toString(!count_ref)),ty) 1193 fun mkv ty = let val newv = mk_var((s^Int.toString(!count_ref)),ty) 1314 fun mkv ty = let val newv = mk_var(("v"^Int.toString(!count_ref)),ty) 1377 mk_var(name,``:^time_ty -> ^ty``) 1895 bus_split(mk_var((name^Int.toString n),``:^ty1->^vty``))) 1918 [mk_var("load",load_ty), 1919 bus_split(mk_var("inp",inp_ty)), 1920 mk_var("don [all...] |
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootParser.sml | 50 fun string_to_label s = mk_var (s, markerSyntax.label_ty); 177 val nv = mk_var ("old_"^v, numLib.num); 231 mk_var(const_name k, numLib.num))) (valOf cs_opt) used_varsL) 261 val nv = mk_var ("old_"^x, numLib.num); 694 val unit_var_term = mk_var("uv", Type `:unit`); 1107 val v = variant (!used_vars) (mk_var x); 1126 val arg_val_numL = map (fn s => mk_var (s, numLib.num)) val_args;
|
H A D | holfoot_pp_print.sml | 90 val v' = mk_var (prefix^v_name, v_type); 572 val v1 = mk_var (arg1, numSyntax.num); 573 val v2 = mk_var (arg2, numSyntax.num); 584 val evL = map (fn n => mk_var (n, numSyntax.num)) esL; 1065 val argL2_const = map (fn n => mk_var (n, numSyntax.num)) argL2_string
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
H A D | sexp.sml | 256 val qtm' = subst [f |-> mk_var(name,fty)] qtm 268 val qtm' = subst [f |-> mk_var(name,fty)] qtm 972 `^(mk_var 1361 (* mlsym(pkg,nam) |--> mk_var("pkg::nam",``:sexp``) *) 1364 mk_var(mlsym_to_string sym,``:sexp``) 1370 (* mlsym(pkg,nam) ty |--> mk_var("pkg::nam",ty) *) 1373 mk_var(mlsym_to_string sym,ty) 1403 mk_var(sym_string,ty)) 1813 mk_var(hol_name, ty) 1839 else ALPHA_CONV (mk_var(hol_vnam [all...] |
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
H A D | helperLib.sml | 428 val vn = mk_var ("n", ``:num``) 562 val v = mk_var ("cond",``:bool``) 578 val v = mk_var("cond",``:bool``) 873 val th = INST [mk_var("boolean_variable_name",``:bool``) |-> frame] th 892 val new_var = mk_var(new_name,type_of x) 905 fun f v = v |-> mk_var((Substring.string o hd o tl o 999 (INST [mk_var("p",``:word64``)|->tm] tha) 1014 RAND_CONV (ALPHA_CONV (mk_var(next_var_name(),ty)))) tm end 1463 val s = map (fn v => v |-> mk_var(make_new_name v,type_of v)) vs
|
/seL4-l4v-10.1.1/HOL4/src/IndDef/ |
H A D | InductiveDefinition.sml | 34 local fun prime v = let val (n,ty) = dest_var v in mk_var(n^"'",ty) end 90 let val v = variant avoid (mk_var("a"^(int_to_string n),hd tys)) 491 val IMP_REFL = let val p = mk_var("p", bool) in ASSUME p |> DISCH p |> GEN p end 575 val l' = mk_var(lname,itlist (curry (op -->) o type_of) vs lty) 687 fun hack_fn tm = mk_var(fst(dest_var(repeat rator tm)),type_of tm)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
H A D | lisp_finalScript.sml | 27 val v = mk_var(def_name,type_of(mk_pabs(x,c))) 52 val th = INST [mk_var("boolean_variable_name",``:bool``) |-> frame] th 60 val tm = subst [mk_var("p",``:word32``) |-> p] tm 85 val new_var = mk_var(new_name,type_of x) 150 in ALPHA_CONV (mk_var(s,type_of v)) tm end
|
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/ |
H A D | DerivedBddRules.sml | 215 else Psyntax.mk_cond(mk_var(get_node_name(bdd.var bdd),bool), 318 val ntm = mk_var("n",num) 692 SOME(s,_) => BddVar true vm (mk_var(s,bool)) 807 val prime_var = mk_var o (prime ## I) o dest_var 904 SOME(s,_) => mk_var(s,bool)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/prog/ |
H A D | m0_progLib.sml | 236 val st = Term.mk_var ("s", ``:m0_state``) 267 val R_name_b_tm = Term.mk_comb (R_name_tm, Term.mk_var ("b", Type.bool)) 555 fun x n = Term.mk_var ("x" ^ Int.toString n, Type.bool)
|