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

12345

/seL4-l4v-10.1.1/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-10.1.1/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-10.1.1/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-10.1.1/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-10.1.1/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-10.1.1/HOL4/examples/miller/ho_prover/
H A DskiTools.sml202 | 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 Dho_discrimTools.sml144 | 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 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.sml39 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 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-10.1.1/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-10.1.1/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-10.1.1/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-10.1.1/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-10.1.1/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-10.1.1/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()
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 DType.sml222 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 Dhol88Lib.sml32 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 DQ.sml202 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 DTermNet.sml277 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 DTermNet.sml277 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 DType.sml275 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 []

Completed in 201 milliseconds

12345