/seL4-l4v-10.1.1/HOL4/Manual/Guide/ |
H A D | guide.tex | 1314 -------------- <name & args> ============ <name & args>
|
/seL4-l4v-10.1.1/HOL4/developers/ |
H A D | comparelogs.sml | 30 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 D | CongruenceScript.sml | 1376 (* 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 D | SHA1Script.sml | 222 `(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 D | cacheTools.sml | 121 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 D | cearTools.sml | 473 val (hnc,args) = dest_comb(lhs(snd(strip_forall(concl hd_def)))) 476 val as_ty = snd(dest_prod(type_of args))
|
H A D | ctl2muTools.sml | 28 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 D | decompTools.sml | 80 (* other than that, all the args here are from the stuff returned by ksTools.mk_formal_KS *)
|
H A D | ksTools.sml | 107 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 D | muCheck.sml | 251 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 D | muSyntax.sml | 133 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 D | hol_defaxiomsScript.sml | 200 |- 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 D | sexp.sml | 245 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 D | hol_defaxiomsScript.sml | 199 |- 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 D | sexp.sml | 243 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 D | book-essence.lisp | 82 (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 D | check-file.lisp | 23 (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 D | untranslate-file.lisp | 82 (('defun fn args . &) 83 `(defp ,fn ,args
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | acl2encodeLib.sml | 1451 val (opr,args) = strip_comb (lhs concl) 1456 mk_mlsexp_list(map term_to_mlsexp args),
|
H A D | encodeLib.sml | 603 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 D | functionEncodeLib.sml | 2115 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 D | hol_defaxiomsScript.sml | 195 |- 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 D | polytypicLib.sml | 426 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 D | sexp.sml | 243 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 D | m1-story.lisp | 1010 ; 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...] |