/seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
H A D | absyn-sig.sml | 26 | FN of pat * exp 31 and pat = PVAR of string type 32 | PAPP of string * pat 33 | PTUPLE of pat list 34 | PLIST of pat list 37 | AS of pat * pat 38 and decl = VB of pat * exp 39 and rule = RULE of pat * exp
|
H A D | absyn.sml | 32 | FN of pat * exp 36 and pat type 38 | PAPP of string * pat 40 | PLIST of pat list 41 | PTUPLE of pat list 43 | AS of pat * pat 44 and decl = VB of pat * exp 45 and rule = RULE of pat * exp 74 val simplifyPat : pat [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | tripleLib.sml | 68 fun abbrev_conv pat post = 69 if pat = pc 71 else if is_var pat 72 then if pat = post 74 else ASSUME (mk_eq (post, add_prime pat)) 75 else if is_comb pat 76 then (RAND_CONV (abbrev_conv (rand pat)) 77 THENC RATOR_CONV (abbrev_conv (rator pat))) post 78 else if pat = post 96 val pat value [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | simplifier.sml | 10 val pat = lhs(snd(dest_imp(concl thm))) value 14 key = SOME([],pat), 16 let val (theta,ty_theta) = match_term pat tm
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/scripts/ |
H A D | mlpp | 131 my $pat = $2; 135 if ($pat eq "(*") { 136 print STDOUT $pat; 139 elsif ($pat eq "*)") { 140 print STDOUT $pat; 185 my $pat = $2; 189 if ($pat eq "`") { 192 elsif ($pat eq "(*") { 205 print STDOUT $pat; 210 elsif ($pat e [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/scripts/ |
H A D | mlpp | 131 my $pat = $2; 135 if ($pat eq "(*") { 136 print STDOUT $pat; 139 elsif ($pat eq "*)") { 140 print STDOUT $pat; 185 my $pat = $2; 189 if ($pat eq "`") { 192 elsif ($pat eq "(*") { 205 print STDOUT $pat; 210 elsif ($pat e [all...] |
/seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
H A D | skiTools.sml | 202 | add a (pat :: next) [] = [BRANCH (pat, add a next [])] 203 | add a (pats as pat :: next) ((b as BRANCH (pat', trees)) :: branches) = 204 if pat = pat' then BRANCH (pat', add a next trees) :: branches 228 | advance pat (state as RIGHT _ :: _, sub) = 229 advance pat (ski_pattern_term_break empty_vars state, sub) 230 | advance pat (LEF [all...] |
H A D | ho_discrimTools.sml | 144 | add a [] (pat :: next) = [BRANCH (pat, add a [] next)] 145 | add a ((b as BRANCH (pat', ts')) :: rest) (ps as pat :: next) = 146 if pat = pat' then BRANCH (pat', add a ts' next) :: rest 181 | advance pat (state as (_, RIGHT _::_), ho_sub) = 182 advance pat (tm_pat_break state, ho_sub) 183 | advance pat ((bv [all...] |
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | match_goal.sml | 44 fun umatch avoid_tms ((tmS,tyS):named_tms) pat ob : named_tms = 46 val ((tmS',tmIds'),(tyS',_)) = raw_match [] avoid_tms pat ob (tmS,tyS) 55 fun umatch_subterms avoid_tms (ntms:named_tms) pat ob : unit -> named_tms stream = 57 (fn () => Stream(umatch avoid_tms ntms pat ob,empty_stream)) 62 (umatch_subterms avoid_tms ntms pat t1) 63 (umatch_subterms avoid_tms ntms pat t2) 65 umatch_subterms (HOLset.add(avoid_tms,v)) ntms pat b 75 ((nm,pat,whole):name * term * bool) ((nths,ntms):data) : unit -> data stream = 90 (fn() => Stream ((nths, umatch fvs ntms pat w),empty_stream)) 92 stream_map (fn ntms => (nths,ntms)) (umatch_subterms fvs ntms pat [all...] |
H A D | mp_then.sml | 39 fun match_subterm pat = find_term (can (match_term pat)) 103 | SOME (pat, rest) => 106 if can (match_subterm pat) subterm then
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | Rules.sml | 97 (* v = pat[v1,...,vn] |- M[x] *) 99 (* ?v1 ... vn. v = pat[v1,...,vn] |- M[x] *) 111 val pat = rhs veq value 112 in snd(itlist CHOOSER (free_vars_lr pat) (veq,thm)) 117 (* Gamma, (x = pat[v1,...,vn]) /\ constraints |- M[x] *) 119 (* Gamma, ?v1 ... vn. (x = pat[v1,...,vn]) /\ constraints |- M[x] *) 127 let val (_,pat) = dest_eq (hd (strip_conj veq_conj)) 128 in snd (itlist CHOOSER (free_vars_lr pat) (veq_conj,thm))
|
/seL4-l4v-10.1.1/HOL4/examples/MLsyntax/ |
H A D | MLScript.sml | 42 * rule ::= <pat> "=>" <exp> * 48 * valbind ::= <pat> "=" <exp> * 49 * | <pat> "=" <exp> "and" <valbind> * 52 * pat ::= "_" (* wildcard *) * 88 rule = rule pat exp ; 94 valbind = bind pat exp 95 | bindl pat exp valbind 98 pat = wild_pat
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | internal_functions.sig | 23 [pcsubst(s,pat)] replaces every unescaped occurrence of "%" in pat with 26 [pattern_match pat obj] attempts to match the pattern pat against 33 there is no match, or SOME s, where performing pcsubst(s,pat) gives 36 If pat doesn't contain a % character, return SOME "", which is otherwise
|
H A D | tailbuffer.sml | 38 List.map (fn pat as (_, true) => pat
|
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/examples/ |
H A D | example.sml | 35 rule ::= <pat> => <exp> 41 valbind ::= <pat> = <exp> 42 | <pat> = <exp> and <valbind> 45 pat ::= _ (* wildcard *) 71 [{name = "rule", arg_info = [being_defined "pat", 82 [{name = "bind", arg_info = [being_defined "pat", 84 {name = "bind_list", arg_info = [being_defined "pat", 88 {type_name = "pat",
|
H A D | var_example.sml | 34 [{name = "rule", arg_info = [being_defined "pat", 45 [{name = "bind", arg_info = [being_defined "pat", 47 {name = "bind_list", arg_info = [being_defined "pat", 51 {type_name = "pat",
|
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | date.scala | 54 def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat) 57 pats.flatMap(pat => { 58 val fmt = pattern(pat)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
H A D | date.scala | 54 def pattern(pat: String): DateTimeFormatter = DateTimeFormatter.ofPattern(pat) 57 pats.flatMap(pat => { 58 val fmt = pattern(pat)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | exportLib.sml | 65 val pat = ``GraphFunction inps outps gg ep`` value 68 val _ = can (match_term pat) tm orelse fail() 77 val pat = ``Basic n xs`` value 80 val _ = can (match_term pat) tm orelse fail() 90 val pat = ``Cond n1 n2 p`` value 93 val _ = can (match_term pat) tm orelse fail() 101 val pat = ``Call next name args strs`` value 104 val _ = can (match_term pat) tm orelse fail() 116 val pat = ``NextNode n`` value 119 val _ = can (match_term pat) t 125 val pat = ``var_acc str`` value 133 val pat = ``SKIP_TAG str`` value [all...] |
/seL4-l4v-10.1.1/HOL4/src/experimental-kernel/ |
H A D | Type.sml | 222 fun raw_match_type pat ob Sids = tymatch [pat] [ob] Sids 224 fun match_type_restr fixed pat ob = fst (raw_match_type pat ob ([],fixed)) 225 fun match_type_in_context pat ob S = fst (raw_match_type pat ob (S,[])) 227 fun match_type pat ob = match_type_in_context pat ob []
|
/seL4-l4v-10.1.1/HOL4/src/hol88/ |
H A D | hol88Lib.sml | 32 fun match_term pat ob = (hol88subst_of ## hol88subst_of) 33 (Term.match_term pat ob)
|
/seL4-l4v-10.1.1/HOL4/src/q/ |
H A D | Q.sml | 202 val pat = ptm_with_ctxtty' ctxt Type.bool q value 204 first (can (ho_match_term [] Term.empty_tmset pat)) asl 375 fun do_one_pat pat = 378 raw_match [] fvs_set pat tm ([],[]) 389 | SOME (pat, rest) => do_one_pat pat handle HOL_ERR _ => test_parses rest 428 fun test (pat, thetasz) (bvs, subt) = 429 case Lib.total (fn t => raw_match [] fvs_set pat t ([],[])) subt of 459 fun mapthis pat = let 460 val patfvs = free_vars pat [all...] |
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | TermNet.sml | 277 fun foldEqualTerms pat inc acc = 279 fun fold ([],net) = inc (pat,net,acc) 280 | fold (pat :: pats, Single (qtm,net)) = 281 if equalQterm pat qtm then fold (pats,net) else acc 290 fn net => fold ([pat],net) 303 | fold inc acc ((pat :: pats, stack, Single (qtm,net)) :: rest) = 304 (case unifyQtermQterm pat qtm of 310 (((pat as Fn (f,a)) :: pats, stack, Multiple (v,fns)) :: rest) = 315 | SOME net => (pats, stackAddQterm pat stack, net) :: rest 326 fun foldUnifiableTerms pat in [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | TermNet.sml | 277 fun foldEqualTerms pat inc acc = 279 fun fold ([],net) = inc (pat,net,acc) 280 | fold (pat :: pats, Single (qtm,net)) = 281 if equalQterm pat qtm then fold (pats,net) else acc 290 fn net => fold ([pat],net) 303 | fold inc acc ((pat :: pats, stack, Single (qtm,net)) :: rest) = 304 (case unifyQtermQterm pat qtm of 310 (((pat as Fn (f,a)) :: pats, stack, Multiple (v,fns)) :: rest) = 315 | SOME net => (pats, stackAddQterm pat stack, net) :: rest 326 fun foldUnifiableTerms pat in [all...] |
/seL4-l4v-10.1.1/HOL4/src/0/ |
H A D | Type.sml | 275 fun raw_match_type pat ob Sids = tymatch [pat] [ob] Sids 277 fun match_type_restr fixed pat ob = fst (raw_match_type pat ob ([],fixed)) 278 fun match_type_in_context pat ob S = fst (raw_match_type pat ob (S,[])) 280 fun match_type pat ob = match_type_in_context pat ob []
|