/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | funCall.sml | 70 | (arg, (t,i)) => (t, i+1) 319 (* | arg 3 | *) 320 (* | arg 2 | *) 321 (* sp | arg 1 | *)
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | funCall.sml | 70 | (arg, (t,i)) => (t, i+1) 316 (* | arg 3 | *) 317 (* | arg 2 | *) 318 (* sp | arg 1 | *)
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | boolSyntax.sml | 76 fun mk_let (func, arg) = 80 list_mk_comb (inst [alpha |-> dom, beta |-> rng] let_tm, [func, arg]) 88 fun mk_literal_case (func, arg) = 93 (inst [alpha |-> dom, beta |-> rng] literal_case, [func, arg])
|
H A D | ThmSetData.sml | 197 fun check_thydelta (arg as (sexp,td)) = revise_data (hook td) arg
|
/seL4-l4v-master/HOL4/src/tactictoe/src/ |
H A D | tttSearch.sml | 128 fun eval_arg ann g stac arg = 130 val tm1 = nntm_of_statearg ((g,stac),arg) 299 fun arg_create atyl arg = 300 {token = arg, atyl = atyl, svis = 0.0, ssum = 0.0, sstatus = StacFresh}
|
H A D | tttBigSteps.sml | 217 val _ = print_endline ("best arg: " ^ its an) 279 val argdir = gendir ^ "/arg"
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | arb.cpp | 108 POLYEXTERNALSYMBOL POLYUNSIGNED PolyGetLowOrderAsLargeWord(FirstArgument threadId, PolyWord arg); 1910 POLYUNSIGNED PolyGetLowOrderAsLargeWord(FirstArgument threadId, PolyWord arg) 1918 if (arg.IsTagged()) 1919 p = arg.UnTagged(); 1922 bool negative = OBJ_IS_NEGATIVE(GetLengthWord(arg)) ? true : false; 1924 mp_limb_t c = *(mp_limb_t*)arg.AsCodePtr(); 1927 POLYUNSIGNED length = get_length(arg); 1929 byte *ptr = arg.AsCodePtr();
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_OPTIMISER.sml | 146 fun mapArg((arg, argT)::rest, n) = 148 else (mapCode arg, argT) :: mapArg(rest, n+1) 543 (* Transform it if it's curried or if there is a tuple in the first arg. *) 594 | mapArg(ArgPattTuple{filter, allConst=false, ...} :: patts, arg :: argctl) = 598 List.map(fn p => (mkInd(p, Extract arg), GeneralType)) fields @ 601 | mapArg(_ :: patts, arg :: argctl) = 602 (Extract arg, GeneralType) :: mapArg(patts, argctl) 1106 (* Function has at least one tupled arg. *) 1108 (* Function has an arg that is a function that returns a tuple. 1112 (* Function has an arg tha [all...] |
/seL4-l4v-master/HOL4/src/num/ |
H A D | numLib.sml | 198 val (meas, arg) = dest_comb tm 200 val st = BasicProvers.prim_find_subterm FVs arg g
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | ParseDatatype.sml | 286 val arg = parse_harg G qb value 289 arg::args
|
H A D | parse_type.sml | 108 fun bit b arg = qtyop {Thy = "fcp", Tyop = if b then "bit1" else "bit0", 109 Locn = locn, Args = [arg]}
|
/seL4-l4v-master/HOL4/developers/mlton-srcs/ |
H A D | Binarymap.sml | 231 fun peek arg = (SOME(find arg)) handle NotFound => NONE
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | stringBinTree.sml | 47 (*apply first arg(conv) to test part of the cond term which is on the rhs of the snd arg (an eq term)*)
|
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootParser.sml | 404 fun arg2absyn vs (os_opt, cs_opt) Aspred_arg_ty_tag (Aspred_arg_exp (Aexp_ident arg)) = 405 (os_opt, cs_opt, SOME (Absyn.mk_AQ (string2holfoot_tag arg))) 412 | arg2absyn vs (os_opt, cs_opt) Aspred_arg_ty_hol (Aspred_arg_exp (Aexp_hol arg)) = 414 val ((os_opt, cs_opt), hol) = HOL_Absyn_old_vars vs (os_opt, cs_opt) arg; 418 | arg2absyn vs (os_opt, cs_opt) Aspred_arg_ty_hol (Aspred_arg_exp (Aexp_ident arg)) = 419 arg2absyn vs (os_opt, cs_opt) Aspred_arg_ty_hol (Aspred_arg_exp (Aexp_hol arg)) 437 | args2absyn vs (os_opt, cs_opt) (ty::tys) (arg::args) = 439 val (os_opt, cs_opt, r_opt) = arg2absyn vs (os_opt, cs_opt) ty arg;
|
/seL4-l4v-master/HOL4/examples/separationLogic/src/ |
H A D | vars_as_resourceSyntax.sml | 81 fun var_res_mk_call_by_value_arg ((arg,expr),term) = 82 list_mk_icomb (var_res_prog_call_by_value_arg_term, [mk_abs (arg, term), expr]);
|
/seL4-l4v-master/HOL4/src/bool/ |
H A D | boolpp.sml | 265 List.foldl (fn(arg, b) => APP(central_locn, 267 arg))
|
/seL4-l4v-master/HOL4/examples/lambda/barendregt/ |
H A D | reductionEval.sml | 196 val (f,arg) = dest_comb t 242 recurse arg
|
H A D | chap3Script.sml | 271 val beta_def = Define`beta M N = ?x body arg. (M = LAM x body @@ arg) /\ 272 (N = [arg/x]body)`; 278 (beta M N = ?x body arg. (M = LAM x body @@ arg) /\ 279 (N = [arg/x] body) /\ 336 Q.ABBREV_TAC `N' = tpm p arg` THEN
|
/seL4-l4v-master/HOL4/tools/mlyacc/src/ |
H A D | yacc.sml | 68 arg: string, (* user argument for parser *) 151 sayln ("type arg = " ^ arg_type); 311 NAMES {actionsStruct,valueStruct,tableStruct,arg,...}) => 414 say " ("; say arg; sayln "):arg) =>"; 811 arg= #1 arg_decl,
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Windows.sml | 656 and launchApplication (command, arg) = 659 ref(Word.toInt size, SEE_MASK_FLAG_NO_UI, Memory.null, "open", command, SOME arg, NONE, 1 (* SW_SHOWNORMAL *), 690 fun execute(command, arg): ('a,'b) proc = 692 val run: pid = winCall (command, arg) 809 fun simpleExecute (command, arg) = 811 val run: pid = winCall(command, arg)
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | CODEGEN_PARSETREE.sml | 126 fun loadArgsFromTuple([t], arg) = [(arg, t)](* "tuple" is a singleton *) 127 | loadArgsFromTuple(types, arg) = 128 ListPair.zip(List.tabulate(List.length types, fn num => mkInd (num, arg)), types) 290 | getVariablesInPatt(Applic {arg, ...}, varl) = getVariablesInPatt (arg, varl) 304 fun codeMatch(near, alt : matchtree list, arg, 326 val decCode = multipleUses (arg, fn () => mkAddr 1, level); 520 | codeGenerate(Applic {f = Ident {value = ref function, expType=ref expType, ...}, arg, location, ...}, context as { level, typeVarMap, lex, ...}) = 525 val (argCode, argEnv) = codeGenerate (arg, contex [all...] |
H A D | EXPORT_PARSETREE.sml | 186 | Applic{location, f, arg = TupleTree{fields=[left, right], ...}, isInfix = true, expType=ref expType, ...} => 191 | Applic{location, f, arg, expType=ref expType, ...} => 192 (location, PTtype expType :: exportList(getExportTree, SOME asParent) [f, arg] @ commonProps)
|
/seL4-l4v-master/HOL4/src/IndDef/ |
H A D | IndDefRules.sml | 361 fun is_param icvs slis arg = 362 let val vl = case residue_assoc arg slis of SOME x => x | NONE => arg
|
/seL4-l4v-master/HOL4/examples/ARM_security_properties/ |
H A D | ARM_prover_extLib.sml | 361 val (opr, arg) = 363 COMB (opr, arg) => (opr, arg)
|
/seL4-l4v-master/HOL4/examples/computability/kolmog/ |
H A D | plain_kolmog_inequalitiesScript.sml | 282 recCn (rec1 (SOME o nblfst)) [SOME o proj 0] (* f is fst(fst arg) *) 291 recCn (SOME o pr1 nblsnd) [SOME o proj 0] (* x is snd (arg) *) 299 recCn (SOME o pr1 nblsnd) [SOME o proj 0] (* x is snd (arg) *)
|