Searched refs:args (Results 1 - 25 of 661) sorted by path

1234567891011>>

/seL4-l4v-10.1.1/HOL4/Manual/Guide/
H A Dguide.tex1314 -------------- <name & args> ============ <name & args>
/seL4-l4v-10.1.1/HOL4/developers/
H A Dcomparelogs.sml30 fun getargs appname args =
32 fun recurse args =
33 case args of
39 | _ => {bequiet = false, diffsort = false, files = args}
41 recurse args
86 fun print_line m args thyname = let
94 app print_entry args;
106 val {bequiet,diffsort,files = args} = getargs (CommandLine.name()) args0
108 val _ = if null args then die "Must specify at least one file to \"analyse\""
111 val _ = if length args <>
[all...]
/seL4-l4v-10.1.1/HOL4/examples/CCS/
H A DCongruenceScript.sml1376 (* The only difference from WG is at WGS4, in which the sum has prefixed args,
/seL4-l4v-10.1.1/HOL4/examples/Crypto/SHA-1/
H A DSHA1Script.sml222 `(Round _ _ args [] = (args,[])) /\
223 (Round helper i args (w::t) =
224 if i<20 then Round helper (i+1) (helper (i MOD 5) args w) t
225 else (args, w::t))`;
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A DcacheTools.sml121 fun mk_inv_one_ante args cthm tthm ithm left =
124 (*val _ = dbgTools.DTM (dpfx^ (List.hd args)) val _ = dbgTools.DST (dpfx^ " hd args\n") (*DBG*)
125 val _ = dbgTools.DTM (dpfx^ (List.last args)) val _ = dbgTools.DST (dpfx^ " last args\n") (*DBG*)
141 val geninv = (ISPECL [List.hd args,List.last args, List.hd ql,List.last ql] ithm)
152 val th = mk_lthm (fn _ => (list_mk_forall(List.drop(l,List.length args),
153 mk_imp(ante,subst (List.map (fn (f,r) => (f|->r)) (ListPair.zip(l,args))) (rand bod))),
160 fun mk_inv_two_ante args ithm
[all...]
H A DcearTools.sml473 val (hnc,args) = dest_comb(lhs(snd(strip_forall(concl hd_def))))
476 val as_ty = snd(dest_prod(type_of args))
H A Dctl2muTools.sml28 val (opr,args) = HolKernel.strip_comb f;
31 "B_PROP" => mu_ap(List.hd args) (* ``AP ^(List.hd args)``*)
32 | "B_NOT" => mu_neg(ctl2mu_aux (List.hd args) cons) (* ``~^(ctl2mu_aux prop_type (List.hd args))``*)
33 | "B_AND" => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
36 | "B_OR" => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
41 | "C_BOOL" => ctl2mu_aux (List.hd args) cons
42 | "C_NOT" => mu_neg(ctl2mu_aux (List.hd args) cons)
43 | "C_AND" => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
[all...]
H A DdecompTools.sml80 (* other than that, all the args here are from the stuff returned by ksTools.mk_formal_KS *)
H A DksTools.sml107 then let val (_,args) = strip_comb tm
108 val res = List.concat (List.map get_APs_aux args)
111 andalso List.null (List.filter has_primed_vars args) (* neither lhs nor rhs contain a primed var *)
H A DmuCheck.sml251 val (opr,args) = strip_comb mf
259 | "RV" => let val Hv = List.hd args
405 | muCheck_aux (args as (msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muAnd(cch,(f1,f2))) =
408 val tb = cache_get cch ie (BinExp (args,(seth,sel,state,ie)) bdd.And (snd(strip_comb(mf))) vm (f1,f2) dp abthm)
413 | muCheck_aux (args as (msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muOr(cch,(f1,f2))) =
416 val tb = cache_get cch ie (BinExp (args,(seth,sel,state,ie)) bdd.Or (snd(strip_comb(mf))) vm (f1,f2) dp abthm)
421 | muCheck_aux (args as (msp,_,_,_,_),(seth,sel,state,ie)) mf vm dp (muNot(cch,f1)) =
424 val tb = cache_get cch ie (NotExp (args,(seth,sel,state,ie)) mf1 vm dp f1 abthm)
431 | muCheck_aux (args as (_,_,_,(_,Tth,(dmdth,_),_,_),_),(seth,sel,state,ie)) mf vm dp (muDIAMOND(cch,(act,f1))) =
434 val tb = cache_get cch ie (ModalExp (args,(set
[all...]
H A DmuSyntax.sml133 let val (opr,args) = HolKernel.strip_comb mf;
137 | "RV" => [List.hd args]
138 | "And" => (fv (List.hd args))@(fv (List.last args))
139 | "Or" => (fv (List.hd args))@(fv (List.last args))
140 | "Not" => fv (List.hd args)
143 | "DIAMOND" => fv (List.last args)
144 | "BOX" => fv (List.last args)
145 | "mu" => List.filter (fn v => not (Term.compare(v,List.hd args)
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/
H A Dhol_defaxiomsScript.sml200 |- xxxjoin fn args =
201 ite (cddr args) (List [fn; car args; xxxjoin fn (cdr args)])
202 (cons fn args),
207 (`xxxjoin fn args =
208 ite (cddr args)
209 (List [fn; car args; xxxjoin fn (cdr args)])
210 (cons fn args)`,
[all...]
H A Dsexp.sml245 val ((f,args),rhs) = dest_hd_eqn qtm
266 val ((f,args),rhs) = dest_hd_eqn qtm
333 val ((f,args),rhs) = dest_hd_eqn qtm'
602 fun is_mllambda (mlpair(mlpair(x,mlpair(params,mlpair(bdy,n))),args)) =
605 is_mlsexp_list args andalso
617 fun dest_mllambda (mlpair(mlpair(_,mlpair(params,mlpair(bdy,_))),args)) =
618 (dest_mlsexp_list params, bdy, dest_mlsexp_list args)
841 let val (opr,args) = strip_comb tm
843 if opr = ``int_of_num:num->int`` andalso (tl args = [])
844 then (if is_numeral(hd args)
1076 val args = (flatten o map strip_pair) arg_tuples value
1441 then let val args = map mlsexp_to_term (dest_mlsexp_list y) value
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A Dhol_defaxiomsScript.sml199 |- xxxjoin fn args =
200 ite (cddr args) (List [fn; car args; xxxjoin fn (cdr args)])
201 (cons fn args),
206 (`xxxjoin fn args =
207 ite (cddr args)
208 (List [fn; car args; xxxjoin fn (cdr args)])
209 (cons fn args)`,
[all...]
H A Dsexp.sml243 val ((f,args),rhs) = dest_hd_eqn qtm
525 fun is_mllambda (mlpair(mlpair(x,mlpair(params,mlpair(bdy,n))),args)) =
528 is_mlsexp_list args andalso
540 fun dest_mllambda (mlpair(mlpair(_,mlpair(params,mlpair(bdy,_))),args)) =
541 (dest_mlsexp_list params, bdy, dest_mlsexp_list args)
767 let val (opr,args) = strip_comb tm
769 if opr = ``int_of_num:num->int`` andalso (tl args = [])
770 then (if is_numeral(hd args)
771 then Arbnum.toString(dest_numeral(hd args))
775 else (if opr = ``int_neg:int->int`` andalso (tl args
1002 val args = (flatten o map strip_pair) arg_tuples value
1367 then let val args = map mlsexp_to_term (dest_mlsexp_list y) value
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/lisp/
H A Dbook-essence.lisp82 (defmacro internal-error (ctx string &rest args)
85 (msg ,string ,@args)))
169 (let* ((kwd-args (cddr form))
170 (dir (cadr (assoc-keyword :dir kwd-args))))
H A Dcheck-file.lisp23 (t (let ((args (fold-conses-lst (fargs term))))
25 (quotep (car args))
26 (quotep (cadr args)))
27 (kwote (cons (unquote (car args))
28 (unquote (cadr args)))))
34 args))
36 args)))))))
46 (('defun fn args . rest)
48 ((not (equal args (formals fn wrld)))
H A Duntranslate-file.lisp82 (('defun fn args . &)
83 `(defp ,fn ,args
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A Dacl2encodeLib.sml1451 val (opr,args) = strip_comb (lhs concl)
1456 mk_mlsexp_list(map term_to_mlsexp args),
H A DencodeLib.sml603 val args = map (fn c => map (fn (n,t) => value
606 val combs = map2 (curry list_mk_comb) cs args
621 val args = map (fn c => map (fn (n,t) => value
623 val combs = map2 (curry list_mk_comb) cs args
632 args combs)
1949 val args = map (fn (n,t) => mk_var((implode o base26) n,t)) value
1951 val cons = list_mk_comb(c,args)
1969 val eterm = list_mk_exists(args,mk_eq(var,cons))
1971 val chosen = DISCH_ALL_CONJ (CHOOSE_L (args,ASSUME eterm) rapped);
1976 (PRODUCTS (length args) rewritte
[all...]
H A DfunctionEncodeLib.sml2115 let val (c,args) = strip_comb term
2119 (fst (strip_fun (type_of c'))) args)
2706 val args = (snd o strip_comb) left value
2723 decoded_args args
2746 (map2 (fn arg => fn ed => arg |-> ed) args encoded_args)
2858 val (fconst,args) = with_exn (strip_comb o lhs o STRIP) sfunction exn1
2860 val (normal_args,higher_args) = partition is_var args
2873 zip higher_args higher_args)) args
3003 val args = map2 (fn an => fn c => variant fvs (mk_var(an,type_of c))) value
3008 (zip args constructor
[all...]
H A Dhol_defaxiomsScript.sml195 |- xxxjoin fn args =
196 ite (cddr args) (List [fn; car args; xxxjoin fn (cdr args)])
197 (cons fn args),
202 (`xxxjoin fn args =
203 ite (cddr args)
204 (List [fn; car args; xxxjoin fn (cdr args)])
205 (cons fn args)`,
[all...]
H A DpolytypicLib.sml426 let val (f,args) = strip_comb term
428 foldl (fn (a,b) => beta_conv (mk_comb(b,a))) f args
1488 val (type_subst,args) =
1490 let val args = with_exn (snd o strip_comb o rator) func exn1 value
1493 (res_t |-> list_mk_fun(map type_of args,type_of func),args)
1502 args thm_clauses handle e => wrap "" e;
1506 let val args = snd (strip_comb (lhs (concl tc))) value
1508 (repeat rator func |-> list_mk_abs(tl args,(mk_abs(hd args,lh
[all...]
H A Dsexp.sml243 val ((f,args),rhs) = dest_hd_eqn qtm
525 fun is_mllambda (mlpair(mlpair(x,mlpair(params,mlpair(bdy,n))),args)) =
528 is_mlsexp_list args andalso
540 fun dest_mllambda (mlpair(mlpair(_,mlpair(params,mlpair(bdy,_))),args)) =
541 (dest_mlsexp_list params, bdy, dest_mlsexp_list args)
767 let val (opr,args) = strip_comb tm
769 if opr = ``int_of_num:num->int`` andalso (tl args = [])
770 then (if is_numeral(hd args)
771 then Arbnum.toString(dest_numeral(hd args))
775 else (if opr = ``int_neg:int->int`` andalso (tl args
1002 val args = (flatten o map strip_pair) arg_tuples value
1367 then let val args = map mlsexp_to_term (dest_mlsexp_list y) value
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/
H A Dm1-story.lisp1010 ; among the args to modify, then the make-state has the corresponding
1016 (defmacro modify (s &rest args)
1018 (if (suppliedp :pc args)
1019 (actual :pc args)
1021 (if (suppliedp :locals args)
1022 (actual :locals args)
1024 (if (suppliedp :stack args)
1025 (actual :stack args)
1027 (if (suppliedp :program args)
1028 (actual :program args)
[all...]

Completed in 292 milliseconds

1234567891011>>