/seL4-l4v-master/HOL4/examples/boyer_moore/ |
H A D | boyer_mooreScript.sml | 28 checkDeltaC pat all_chars j a d = 29 ((d = j+1) \/ (EL (j-d) pat = EL a all_chars)) 36 ``!pat all_chars j a d . d IN valid_cha_shifts pat all_chars j a 37 <=> (1 <= d /\ d <= j+1 /\ checkDeltaC pat all_chars j a d)``, 49 ``valid_cha_shifts pat all_chars j a = {d | 1 <= d /\ d <= j+1 50 /\ checkDeltaC pat all_chars j a d}``, 58 cmRecur pat all_chars j a d = 60 else if (checkDeltaC pat all_chars j a d) then d 61 else (cmRecur pat all_char [all...] |
H A D | boyer_moore_specScript.sml | 25 solutions pat search = 27 ~(LENGTH pat <= LENGTH search) 31 {k| k <= LENGTH search - LENGTH pat 32 /\ (!i. i < LENGTH pat 33 ==> (EL (i+k) search = EL i pat) 41 (!d. d < m ==> ~(d IN solutions pat search)) 42 ==> (!x. x IN solutions pat (DROP m search) 43 <=> (m+x) IN solutions pat search)`, 56 >> `i + x + m <= i + (LENGTH search - (m + LENGTH pat)) + m` 58 >> `i + (LENGTH search - (m + LENGTH pat)) [all...] |
H A D | helper_funcsScript.sml | 167 (* check if pat is prefix of search from left to right and return failure point. 168 Returns LENGTH pat if perfect match *) 263 (* check if pat is prefix of search from right to left and return failure point. 264 Returns LENGTH pat if perfect match. Returns LENGTH pat + 1 if search string 269 checkPrefixRL pat search = 271 (L = LENGTH pat); 280 jLR = checkPairs (ZIP ((REVERSE pat), 291 (* Confirming checkPrefixRL checks pat matches search from right 295 ``checkPrefixRL pat searc [all...] |
/seL4-l4v-master/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-master/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-master/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-master/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-master/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-master/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 | 8 fun match_subterm pat = find_term (can (match_term pat)) 64 | SOME (pat, rest) => 67 if can (match_subterm pat) subterm then
|
/seL4-l4v-master/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-master/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-master/HOL4/examples/miller/ho_prover/ |
H A D | skiTools.sml | 210 | add a (pat :: next) [] = [BRANCH (pat, add a next [])] 211 | add a (pats as pat :: next) ((b as BRANCH (pat', trees)) :: branches) = 212 if skipat_eq pat pat' then BRANCH (pat', add a next trees) :: branches 236 | advance pat (state as RIGHT _ :: _, sub) = 237 advance pat (ski_pattern_term_break empty_vars state, sub) 238 | advance pat (LEF [all...] |
H A D | ho_discrimTools.sml | 155 | add a [] (pat :: next) = [BRANCH (pat, add a [] next)] 156 | add a ((b as BRANCH (pat', ts')) :: rest) (ps as pat :: next) = 157 if pat_eq pat pat' then BRANCH (pat', add a ts' next) :: rest 192 | advance pat (state as (_, RIGHT _::_), ho_sub) = 193 advance pat (tm_pat_break state, ho_sub) 194 | advance pat ((bv [all...] |
/seL4-l4v-master/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-master/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-master/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-master/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-master/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() 91 val pat = ``Cond n1 n2 p`` value 94 val _ = can (match_term pat) tm orelse fail() 102 val pat = ``Call next name args strs`` value 105 val _ = can (match_term pat) tm orelse fail() 119 val pat = ``NextNode n`` value 122 val _ = can (match_term pat) t 128 val pat = ``var_acc str`` value 136 val pat = ``SKIP_TAG str`` value [all...] |
/seL4-l4v-master/HOL4/src/postkernel/ |
H A D | DB.sml | 225 fun findpred pat s = 227 val pat = toLower pat and s = toLower s value 228 val orparts = String.tokens (equal #"|") pat 269 fun matcher f thyl pat = 270 matchp (fn th => can (find_term (can (f pat))) (concl th)) thyl; 277 fun matches pat th = 278 can (find_term (can (ho_match_term [] empty_tmset pat))) (concl th) ; 280 fun apropos_in pat dbdata = 281 List.filter (fn (_, (th, _)) => matches pat t [all...] |
/seL4-l4v-master/HOL4/src/experimental-kernel/ |
H A D | Type.sml | 223 fun raw_match_type pat ob Sids = tymatch [pat] [ob] Sids 225 fun match_type_restr fixed pat ob = fst (raw_match_type pat ob ([],fixed)) 226 fun match_type_in_context pat ob S = fst (raw_match_type pat ob (S,[])) 228 fun match_type pat ob = match_type_in_context pat ob []
|
/seL4-l4v-master/HOL4/src/hol88/ |
H A D | hol88Lib.sml | 32 fun match_term pat ob = (hol88subst_of ## hol88subst_of) 33 (Term.match_term pat ob)
|