author | paulson <lp15@cam.ac.uk> |
Sun, 20 May 2018 18:37:34 +0100 | |
changeset 68239 | 0764ee22a4d1 |
parent 64556 | 851ae0e7b09c |
child 69575 | f77cc54f6d47 |
permissions | -rw-r--r-- |
12784 | 1 |
(* Title: Pure/pattern.ML |
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
28348
diff
changeset
|
2 |
Author: Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer, TU Muenchen |
0 | 3 |
|
4 |
Unification of Higher-Order Patterns. |
|
5 |
||
6 |
See also: |
|
7 |
Tobias Nipkow. Functional Unification of Higher-Order Patterns. |
|
8 |
In Proceedings of the 8th IEEE Symposium Logic in Computer Science, 1993. |
|
678
6151b7f3b606
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
nipkow
parents:
63
diff
changeset
|
9 |
|
6151b7f3b606
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
nipkow
parents:
63
diff
changeset
|
10 |
TODO: optimize red by special-casing it |
0 | 11 |
*) |
12 |
||
13 |
signature PATTERN = |
|
14787 | 14 |
sig |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
15 |
exception Unif |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
16 |
exception Pattern |
52709
0e4bacf21e77
turned pattern unify flag into configuration option (global only);
wenzelm
parents:
52220
diff
changeset
|
17 |
val unify_trace_failure_raw: Config.raw |
0e4bacf21e77
turned pattern unify flag into configuration option (global only);
wenzelm
parents:
52220
diff
changeset
|
18 |
val unify_trace_failure: bool Config.T |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
19 |
val unify_types: Context.generic -> typ * typ -> Envir.env -> Envir.env |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
20 |
val unify: Context.generic -> term * term -> Envir.env -> Envir.env |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
21 |
exception MATCH |
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
22 |
val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv |
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
23 |
val first_order_match: theory -> term * term |
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
24 |
-> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv |
14787 | 25 |
end; |
0 | 26 |
|
17203 | 27 |
structure Pattern: PATTERN = |
0 | 28 |
struct |
29 |
||
30 |
exception Unif; |
|
31 |
exception Pattern; |
|
32 |
||
52709
0e4bacf21e77
turned pattern unify flag into configuration option (global only);
wenzelm
parents:
52220
diff
changeset
|
33 |
val unify_trace_failure_raw = |
64556 | 34 |
Config.declare ("unify_trace_failure", \<^here>) (fn _ => Config.Bool false); |
52709
0e4bacf21e77
turned pattern unify flag into configuration option (global only);
wenzelm
parents:
52220
diff
changeset
|
35 |
val unify_trace_failure = Config.bool unify_trace_failure_raw; |
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
36 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
37 |
fun string_of_term ctxt env binders t = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
38 |
Syntax.string_of_term ctxt (Envir.norm_term env (subst_bounds (map Free binders, t))); |
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
39 |
|
18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17756
diff
changeset
|
40 |
fun bname binders i = fst (nth binders i); |
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
41 |
fun bnames binders is = space_implode " " (map (bname binders) is); |
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
42 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
43 |
fun typ_clash context (tye,T,U) = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
44 |
if Config.get_generic context unify_trace_failure then |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
45 |
let |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
46 |
val ctxt = Context.proof_of context; |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
47 |
val t = Syntax.string_of_typ ctxt (Envir.norm_type tye T); |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
48 |
val u = Syntax.string_of_typ ctxt (Envir.norm_type tye U); |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
49 |
in tracing ("The following types do not unify:\n" ^ t ^ "\n" ^ u) end |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
50 |
else (); |
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
51 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
52 |
fun clash context a b = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
53 |
if Config.get_generic context unify_trace_failure |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
54 |
then tracing ("Clash: " ^ a ^ " =/= " ^ b) else (); |
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
55 |
|
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
56 |
fun boundVar binders i = |
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
57 |
"bound variable " ^ bname binders i ^ " (depth " ^ string_of_int i ^ ")"; |
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
58 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
59 |
fun clashBB context binders i j = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
60 |
if Config.get_generic context unify_trace_failure |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
61 |
then clash context (boundVar binders i) (boundVar binders j) else (); |
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
62 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
63 |
fun clashB context binders i s = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
64 |
if Config.get_generic context unify_trace_failure |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
65 |
then clash context (boundVar binders i) s else (); |
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
66 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
67 |
fun proj_fail context (env,binders,F,_,is,t) = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
68 |
if Config.get_generic context unify_trace_failure then |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
69 |
let |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
70 |
val ctxt = Context.proof_of context |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
71 |
val f = Term.string_of_vname F |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
72 |
val xs = bnames binders is |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
73 |
val u = string_of_term ctxt env binders t |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
74 |
val ys = bnames binders (subtract (op =) is (loose_bnos t)) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
75 |
in |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
76 |
tracing ("Cannot unify variable " ^ f ^ |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
77 |
" (depending on bound variables " ^ xs ^ ")\nwith term " ^ u ^ |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
78 |
"\nTerm contains additional bound variable(s) " ^ ys) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
79 |
end |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
80 |
else (); |
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
81 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
82 |
fun ocheck_fail context (F,t,binders,env) = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
83 |
if Config.get_generic context unify_trace_failure then |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
84 |
let |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
85 |
val ctxt = Context.proof_of context |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
86 |
val f = Term.string_of_vname F |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
87 |
val u = string_of_term ctxt env binders t |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
88 |
in tracing ("Variable " ^ f ^ " occurs in term\n" ^ u ^ "\nCannot unify!\n") end |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
89 |
else (); |
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
90 |
|
12784 | 91 |
fun occurs(F,t,env) = |
51700 | 92 |
let fun occ(Var (G, T)) = (case Envir.lookup env (G, T) of |
15531 | 93 |
SOME(t) => occ t |
94 |
| NONE => F=G) |
|
0 | 95 |
| occ(t1$t2) = occ t1 orelse occ t2 |
96 |
| occ(Abs(_,_,t)) = occ t |
|
97 |
| occ _ = false |
|
98 |
in occ t end; |
|
99 |
||
100 |
||
101 |
fun mapbnd f = |
|
102 |
let fun mpb d (Bound(i)) = if i < d then Bound(i) else Bound(f(i-d)+d) |
|
103 |
| mpb d (Abs(s,T,t)) = Abs(s,T,mpb(d+1) t) |
|
678
6151b7f3b606
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
nipkow
parents:
63
diff
changeset
|
104 |
| mpb d ((u1 $ u2)) = (mpb d u1)$(mpb d u2) |
6151b7f3b606
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
nipkow
parents:
63
diff
changeset
|
105 |
| mpb _ atom = atom |
0 | 106 |
in mpb 0 end; |
107 |
||
14861
ca5cae7fb65a
Removed ~10000 hack in function idx that can lead to inconsistencies
berghofe
parents:
14787
diff
changeset
|
108 |
fun idx [] j = raise Unif |
16668 | 109 |
| idx(i::is) j = if (i:int) =j then length is else idx is j; |
0 | 110 |
|
111 |
fun mkabs (binders,is,t) = |
|
18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17756
diff
changeset
|
112 |
let fun mk(i::is) = let val (x,T) = nth binders i |
12784 | 113 |
in Abs(x,T,mk is) end |
0 | 114 |
| mk [] = t |
115 |
in mk is end; |
|
116 |
||
117 |
val incr = mapbnd (fn i => i+1); |
|
118 |
||
119 |
fun ints_of [] = [] |
|
12784 | 120 |
| ints_of (Bound i ::bs) = |
0 | 121 |
let val is = ints_of bs |
20672 | 122 |
in if member (op =) is i then raise Pattern else i::is end |
0 | 123 |
| ints_of _ = raise Pattern; |
124 |
||
12232 | 125 |
fun ints_of' env ts = ints_of (map (Envir.head_norm env) ts); |
126 |
||
0 | 127 |
|
128 |
fun app (s,(i::is)) = app (s$Bound(i),is) |
|
129 |
| app (s,[]) = s; |
|
130 |
||
131 |
fun red (Abs(_,_,s)) (i::is) js = red s is (i::js) |
|
678
6151b7f3b606
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
nipkow
parents:
63
diff
changeset
|
132 |
| red t [] [] = t |
18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17756
diff
changeset
|
133 |
| red t is jn = app (mapbnd (nth jn) t,is); |
678
6151b7f3b606
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
nipkow
parents:
63
diff
changeset
|
134 |
|
0 | 135 |
|
136 |
(* split_type ([T1,....,Tn]---> T,n,[]) = ([Tn,...,T1],T) *) |
|
137 |
fun split_type (T,0,Ts) = (Ts,T) |
|
138 |
| split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts) |
|
52133 | 139 |
| split_type _ = raise Fail "split_type"; |
0 | 140 |
|
32032 | 141 |
fun type_of_G env (T, n, is) = |
142 |
let |
|
143 |
val tyenv = Envir.type_env env; |
|
144 |
val (Ts, U) = split_type (Envir.norm_type tyenv T, n, []); |
|
18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17756
diff
changeset
|
145 |
in map (nth Ts) is ---> U end; |
0 | 146 |
|
52130 | 147 |
fun mk_hnf (binders,is,G,js) = mkabs (binders, is, app(G,js)); |
0 | 148 |
|
52130 | 149 |
fun mk_new_hnf(env,binders,is,F as (a,_),T,js) = |
13891
ae9a2a433388
type_of_G now applies type substitution before decomposing type.
berghofe
parents:
13645
diff
changeset
|
150 |
let val (env',G) = Envir.genvar a (env,type_of_G env (T,length is,js)) |
52130 | 151 |
in Envir.update ((F, T), mk_hnf (binders, is, G, js)) env' end; |
0 | 152 |
|
153 |
||
23222 | 154 |
(*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*) |
155 |
fun downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1) |
|
156 |
| downto0 ([], n) = n = ~1; |
|
157 |
||
158 |
(*mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ]*) |
|
0 | 159 |
fun mk_proj_list is = |
19502 | 160 |
let fun mk(i::is,j) = if is_some i then j :: mk(is,j-1) else mk(is,j-1) |
0 | 161 |
| mk([],_) = [] |
162 |
in mk(is,length is - 1) end; |
|
163 |
||
164 |
fun proj(s,env,binders,is) = |
|
165 |
let fun trans d i = if i<d then i else (idx is (i-d))+d; |
|
12232 | 166 |
fun pr(s,env,d,binders) = (case Envir.head_norm env s of |
0 | 167 |
Abs(a,T,t) => let val (t',env') = pr(t,env,d+1,((a,T)::binders)) |
168 |
in (Abs(a,T,t'),env') end |
|
169 |
| t => (case strip_comb t of |
|
170 |
(c as Const _,ts) => |
|
171 |
let val (ts',env') = prs(ts,env,d,binders) |
|
172 |
in (list_comb(c,ts'),env') end |
|
173 |
| (f as Free _,ts) => |
|
174 |
let val (ts',env') = prs(ts,env,d,binders) |
|
175 |
in (list_comb(f,ts'),env') end |
|
176 |
| (Bound(i),ts) => |
|
177 |
let val j = trans d i |
|
14861
ca5cae7fb65a
Removed ~10000 hack in function idx that can lead to inconsistencies
berghofe
parents:
14787
diff
changeset
|
178 |
val (ts',env') = prs(ts,env,d,binders) |
ca5cae7fb65a
Removed ~10000 hack in function idx that can lead to inconsistencies
berghofe
parents:
14787
diff
changeset
|
179 |
in (list_comb(Bound j,ts'),env') end |
0 | 180 |
| (Var(F as (a,_),Fty),ts) => |
12232 | 181 |
let val js = ints_of' env ts; |
14861
ca5cae7fb65a
Removed ~10000 hack in function idx that can lead to inconsistencies
berghofe
parents:
14787
diff
changeset
|
182 |
val js' = map (try (trans d)) js; |
0 | 183 |
val ks = mk_proj_list js'; |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19300
diff
changeset
|
184 |
val ls = map_filter I js' |
13891
ae9a2a433388
type_of_G now applies type substitution before decomposing type.
berghofe
parents:
13645
diff
changeset
|
185 |
val Hty = type_of_G env (Fty,length js,ks) |
0 | 186 |
val (env',H) = Envir.genvar a (env,Hty) |
187 |
val env'' = |
|
52130 | 188 |
Envir.update ((F, Fty), mk_hnf (binders, js, H, ks)) env' |
0 | 189 |
in (app(H,ls),env'') end |
190 |
| _ => raise Pattern)) |
|
191 |
and prs(s::ss,env,d,binders) = |
|
192 |
let val (s',env1) = pr(s,env,d,binders) |
|
193 |
val (ss',env2) = prs(ss,env1,d,binders) |
|
194 |
in (s'::ss',env2) end |
|
195 |
| prs([],env,_,_) = ([],env) |
|
196 |
in if downto0(is,length binders - 1) then (s,env) |
|
197 |
else pr(s,env,0,binders) |
|
198 |
end; |
|
199 |
||
200 |
||
201 |
(* mk_ff_list(is,js) = [ length(is) - k | 1 <= k <= |is| and is[k] = js[k] ] *) |
|
12784 | 202 |
fun mk_ff_list(is,js) = |
203 |
let fun mk([],[],_) = [] |
|
16668 | 204 |
| mk(i::is,j::js, k) = if (i:int) = j then k :: mk(is,js,k-1) |
0 | 205 |
else mk(is,js,k-1) |
52133 | 206 |
| mk _ = raise Fail "mk_ff_list" |
0 | 207 |
in mk(is,js,length is-1) end; |
208 |
||
209 |
fun flexflex1(env,binders,F,Fty,is,js) = |
|
210 |
if is=js then env |
|
211 |
else let val ks = mk_ff_list(is,js) |
|
52130 | 212 |
in mk_new_hnf(env,binders,is,F,Fty,ks) end; |
0 | 213 |
|
214 |
fun flexflex2(env,binders,F,Fty,is,G,Gty,js) = |
|
215 |
let fun ff(F,Fty,is,G as (a,_),Gty,js) = |
|
33038 | 216 |
if subset (op =) (js, is) |
0 | 217 |
then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js)) |
51700 | 218 |
in Envir.update ((F, Fty), t) env end |
33049
c38f02fdf35d
curried inter as canonical list operation (beware of argument order)
haftmann
parents:
33038
diff
changeset
|
219 |
else let val ks = inter (op =) js is |
13891
ae9a2a433388
type_of_G now applies type substitution before decomposing type.
berghofe
parents:
13645
diff
changeset
|
220 |
val Hty = type_of_G env (Fty,length is,map (idx is) ks) |
0 | 221 |
val (env',H) = Envir.genvar a (env,Hty) |
222 |
fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks)); |
|
51700 | 223 |
in Envir.update ((G, Gty), lam js) (Envir.update ((F, Fty), lam is) env') |
0 | 224 |
end; |
35408 | 225 |
in if Term_Ord.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end |
0 | 226 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
227 |
fun unify_types context (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) = |
32032 | 228 |
if T = U then env |
229 |
else |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
230 |
let |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
231 |
val thy = Context.theory_of context |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
232 |
val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx) |
32032 | 233 |
in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
234 |
handle Type.TUNIFY => (typ_clash context (tyenv, T, U); raise Unif); |
0 | 235 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
236 |
fun unif context binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of |
0 | 237 |
(Abs(ns,Ts,ts),Abs(nt,Tt,tt)) => |
238 |
let val name = if ns = "" then nt else ns |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
239 |
in unif context ((name,Ts)::binders) (ts,tt) (unify_types context (Ts, Tt) env) end |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
240 |
| (Abs(ns,Ts,ts),t) => unif context ((ns,Ts)::binders) (ts,(incr t)$Bound(0)) env |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
241 |
| (t,Abs(nt,Tt,tt)) => unif context ((nt,Tt)::binders) ((incr t)$Bound(0),tt) env |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
242 |
| p => cases context (binders,env,p) |
0 | 243 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
244 |
and cases context (binders,env,(s,t)) = case (strip_comb s,strip_comb t) of |
12784 | 245 |
((Var(F,Fty),ss),(Var(G,Gty),ts)) => |
52220
c4264f71dc3b
backout 3b9c31867707 -- too risky to "amend" modules from 25 years ago that don't handle Vars with different types;
wenzelm
parents:
52179
diff
changeset
|
246 |
if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts) |
c4264f71dc3b
backout 3b9c31867707 -- too risky to "amend" modules from 25 years ago that don't handle Vars with different types;
wenzelm
parents:
52179
diff
changeset
|
247 |
else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts) |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
248 |
| ((Var(F,Fty),ss),_) => flexrigid context (env,binders,F,Fty,ints_of' env ss,t) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
249 |
| (_,(Var(F,Fty),ts)) => flexrigid context (env,binders,F,Fty,ints_of' env ts,s) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
250 |
| ((Const c,ss),(Const d,ts)) => rigidrigid context (env,binders,c,d,ss,ts) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
251 |
| ((Free(f),ss),(Free(g),ts)) => rigidrigid context (env,binders,f,g,ss,ts) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
252 |
| ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB context (env,binders,i,j,ss,ts) |
0 | 253 |
| ((Abs(_),_),_) => raise Pattern |
254 |
| (_,(Abs(_),_)) => raise Pattern |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
255 |
| ((Const(c,_),_),(Free(f,_),_)) => (clash context c f; raise Unif) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
256 |
| ((Const(c,_),_),(Bound i,_)) => (clashB context binders i c; raise Unif) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
257 |
| ((Free(f,_),_),(Const(c,_),_)) => (clash context f c; raise Unif) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
258 |
| ((Free(f,_),_),(Bound i,_)) => (clashB context binders i f; raise Unif) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
259 |
| ((Bound i,_),(Const(c,_),_)) => (clashB context binders i c; raise Unif) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
260 |
| ((Bound i,_),(Free(f,_),_)) => (clashB context binders i f; raise Unif) |
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
261 |
|
0 | 262 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
263 |
and rigidrigid context (env,binders,(a,Ta),(b,Tb),ss,ts) = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
264 |
if a<>b then (clash context a b; raise Unif) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
265 |
else env |> unify_types context (Ta,Tb) |> fold (unif context binders) (ss~~ts) |
0 | 266 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
267 |
and rigidrigidB context (env,binders,i,j,ss,ts) = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
268 |
if i <> j then (clashBB context binders i j; raise Unif) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
269 |
else fold (unif context binders) (ss~~ts) env |
0 | 270 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
271 |
and flexrigid context (params as (env,binders,F,Fty,is,t)) = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
272 |
if occurs(F,t,env) then (ocheck_fail context (F,t,binders,env); raise Unif) |
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
273 |
else (let val (u,env') = proj(t,env,binders,is) |
51700 | 274 |
in Envir.update ((F, Fty), mkabs (binders, is, u)) env' end |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
275 |
handle Unif => (proj_fail context params; raise Unif)); |
0 | 276 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58859
diff
changeset
|
277 |
fun unify context = unif context []; |
0 | 278 |
|
279 |
||
678
6151b7f3b606
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
nipkow
parents:
63
diff
changeset
|
280 |
|
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
281 |
(*** Matching ***) |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
282 |
|
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
283 |
exception MATCH; |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
284 |
|
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
285 |
fun typ_match thy TU tyenv = Sign.typ_match thy TU tyenv |
16939 | 286 |
handle Type.TYPE_MATCH => raise MATCH; |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
287 |
|
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
288 |
(*First-order matching; |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
289 |
The pattern and object may have variables in common. |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
290 |
Instantiation does not affect the object, so matching ?a with ?a+1 works. |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
291 |
Object is eta-contracted on the fly (by eta-expanding the pattern). |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
292 |
Precondition: the pattern is already eta-contracted! |
63718 | 293 |
Types are matched on the fly. |
294 |
The parameter inAbs is an optimization to avoid calling is_open; |
|
295 |
it has the funny consequence that outside abstractions |
|
296 |
?x matches terms containing loose Bounds. |
|
297 |
*) |
|
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
298 |
fun first_order_match thy = |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
299 |
let |
63718 | 300 |
fun mtch inAbs (instsp as (tyinsts,insts)) = fn |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
301 |
(Var(ixn,T), t) => |
63718 | 302 |
if inAbs andalso Term.is_open t then raise MATCH |
51700 | 303 |
else (case Envir.lookup1 insts (ixn, T) of |
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
304 |
NONE => (typ_match thy (T, fastype_of t) tyinsts, |
17412 | 305 |
Vartab.update_new (ixn, (T, t)) insts) |
52131 | 306 |
| SOME u => if Envir.aeconv (t, u) then instsp else raise MATCH) |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
307 |
| (Free (a,T), Free (b,U)) => |
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
308 |
if a=b then (typ_match thy (T,U) tyinsts, insts) else raise MATCH |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
309 |
| (Const (a,T), Const (b,U)) => |
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
310 |
if a=b then (typ_match thy (T,U) tyinsts, insts) else raise MATCH |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
311 |
| (Bound i, Bound j) => if i=j then instsp else raise MATCH |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
312 |
| (Abs(_,T,t), Abs(_,U,u)) => |
63718 | 313 |
mtch true (typ_match thy (T,U) tyinsts, insts) (t,u) |
314 |
| (f$t, g$u) => mtch inAbs (mtch inAbs instsp (f,g)) (t, u) |
|
315 |
| (t, Abs(_,U,u)) => mtch true instsp ((incr t)$(Bound 0), u) |
|
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
316 |
| _ => raise MATCH |
63718 | 317 |
in fn tu => fn env => mtch false env tu end; |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
318 |
|
8406
a217b0cd304d
Type.unify and Type.typ_match now use Vartab instead of association lists.
berghofe
parents:
6539
diff
changeset
|
319 |
|
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
320 |
(* Matching of higher-order patterns *) |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
321 |
|
15797 | 322 |
fun match_bind(itms,binders,ixn,T,is,t) = |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
323 |
let val js = loose_bnos t |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
324 |
in if null is |
17412 | 325 |
then if null js then Vartab.update_new (ixn, (T, t)) itms else raise MATCH |
33038 | 326 |
else if subset (op =) (js, is) |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
327 |
then let val t' = if downto0(is,length binders - 1) then t |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
328 |
else mapbnd (idx is) t |
17412 | 329 |
in Vartab.update_new (ixn, (T, mkabs (binders, is, t'))) itms end |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
330 |
else raise MATCH |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
331 |
end; |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
332 |
|
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
333 |
fun match thy (po as (pat,obj)) envir = |
678
6151b7f3b606
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
nipkow
parents:
63
diff
changeset
|
334 |
let |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
335 |
(* Pre: pat and obj have same type *) |
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
336 |
fun mtch binders (pat,obj) (env as (iTs,itms)) = |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
337 |
case pat of |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
338 |
Abs(ns,Ts,ts) => |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
339 |
(case obj of |
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
340 |
Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (ts,tt) env |
32035 | 341 |
| _ => let val Tt = Envir.subst_type iTs Ts |
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
342 |
in mtch((ns,Tt)::binders) (ts,(incr obj)$Bound(0)) env end) |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
343 |
| _ => (case obj of |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
344 |
Abs(nt,Tt,tt) => |
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
345 |
mtch((nt,Tt)::binders) ((incr pat)$Bound(0),tt) env |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
346 |
| _ => cases(binders,env,pat,obj)) |
678
6151b7f3b606
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
nipkow
parents:
63
diff
changeset
|
347 |
|
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
348 |
and cases(binders,env as (iTs,itms),pat,obj) = |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
349 |
let val (ph,pargs) = strip_comb pat |
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
350 |
fun rigrig1(iTs,oargs) = fold (mtch binders) (pargs~~oargs) (iTs,itms) |
41067 | 351 |
handle ListPair.UnequalLengths => raise MATCH |
16668 | 352 |
fun rigrig2((a:string,Ta),(b,Tb),oargs) = |
353 |
if a <> b then raise MATCH |
|
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
354 |
else rigrig1(typ_match thy (Ta,Tb) iTs, oargs) |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
355 |
in case ph of |
15797 | 356 |
Var(ixn,T) => |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
357 |
let val is = ints_of pargs |
51700 | 358 |
in case Envir.lookup1 itms (ixn, T) of |
15797 | 359 |
NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj)) |
52131 | 360 |
| SOME u => if Envir.aeconv (obj, red u is []) then env |
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
361 |
else raise MATCH |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
362 |
end |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
363 |
| _ => |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
364 |
let val (oh,oargs) = strip_comb obj |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
365 |
in case (ph,oh) of |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
366 |
(Const c,Const d) => rigrig2(c,d,oargs) |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
367 |
| (Free f,Free g) => rigrig2(f,g,oargs) |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
368 |
| (Bound i,Bound j) => if i<>j then raise MATCH |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
369 |
else rigrig1(iTs,oargs) |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
370 |
| (Abs _, _) => raise Pattern |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
371 |
| (_, Abs _) => raise Pattern |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
372 |
| _ => raise MATCH |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
373 |
end |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
374 |
end; |
678
6151b7f3b606
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
nipkow
parents:
63
diff
changeset
|
375 |
|
4820
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
376 |
val pT = fastype_of pat |
8f6dbbd8d497
Tried to speed up the rewriter by eta-contracting all patterns beforehand and
nipkow
parents:
4667
diff
changeset
|
377 |
and oT = fastype_of obj |
18182
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
378 |
val envir' = apfst (typ_match thy (pT, oT)) envir; |
786d83044780
tuned interfaces to support incremental match/unify (cf. versions in type.ML);
wenzelm
parents:
18011
diff
changeset
|
379 |
in mtch [] po envir' handle Pattern => first_order_match thy po envir' end; |
0 | 380 |
|
381 |
end; |
|
13642
a3d97348ceb6
added failure trace information to pattern unification
nipkow
parents:
13195
diff
changeset
|
382 |