Searched refs:pat (Results 1 - 25 of 134) sorted by relevance

123456

/seL4-l4v-master/HOL4/examples/boyer_moore/
H A Dboyer_mooreScript.sml28 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 Dboyer_moore_specScript.sml25 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 Dhelper_funcsScript.sml167 (* 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 Dabsyn-sig.sml26 | 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 Dabsyn.sml32 | 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 DtripleLib.sml68 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 Dsimplifier.sml10 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 Dmlpp131 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 Dmlpp131 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 Dmatch_goal.sml44 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 Dmp_then.sml8 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 DRules.sml97 (* 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 DMLScript.sml42 * 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 DskiTools.sml210 | 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 Dho_discrimTools.sml155 | 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 Dinternal_functions.sig23 [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 Dtailbuffer.sml38 List.map (fn pat as (_, true) => pat
/seL4-l4v-master/HOL4/src/datatype/mutrec/examples/
H A Dexample.sml35 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 Dvar_example.sml34 [{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 Ddate.scala54 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 Ddate.scala54 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 DexportLib.sml65 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 DDB.sml225 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 DType.sml223 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 Dhol88Lib.sml32 fun match_term pat ob = (hol88subst_of ## hol88subst_of)
33 (Term.match_term pat ob)

Completed in 987 milliseconds

123456