author | wenzelm |
Sun, 22 Jul 2012 12:26:41 +0200 | |
changeset 48423 | 0ccf143a2a69 |
parent 48263 | 94a7dc2276e4 |
child 51700 | c8f2bad67dbb |
permissions | -rw-r--r-- |
15797 | 1 |
(* Title: Pure/unify.ML |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 3 |
Copyright Cambridge University 1992 |
4 |
||
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset
|
5 |
Higher-Order Unification. |
0 | 6 |
|
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset
|
7 |
Types as well as terms are unified. The outermost functions assume |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset
|
8 |
the terms to be unified already have the same type. In resolution, |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset
|
9 |
this is assured because both have type "prop". |
0 | 10 |
*) |
11 |
||
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset
|
12 |
signature UNIFY = |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset
|
13 |
sig |
39163
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39116
diff
changeset
|
14 |
val trace_bound_raw: Config.raw |
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset
|
15 |
val trace_bound: int Config.T |
39163
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39116
diff
changeset
|
16 |
val search_bound_raw: Config.raw |
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset
|
17 |
val search_bound: int Config.T |
39163
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39116
diff
changeset
|
18 |
val trace_simp_raw: Config.raw |
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset
|
19 |
val trace_simp: bool Config.T |
39163
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39116
diff
changeset
|
20 |
val trace_types_raw: Config.raw |
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset
|
21 |
val trace_types: bool Config.T |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset
|
22 |
val unifiers: theory * Envir.env * ((term * term) list) -> |
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset
|
23 |
(Envir.env * (term * term) list) Seq.seq |
19864 | 24 |
val smash_unifiers: theory -> (term * term) list -> Envir.env -> Envir.env Seq.seq |
25 |
val matchers: theory -> (term * term) list -> Envir.env Seq.seq |
|
26 |
val matches_list: theory -> term list -> term list -> bool |
|
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset
|
27 |
end |
0 | 28 |
|
19864 | 29 |
structure Unify : UNIFY = |
0 | 30 |
struct |
31 |
||
32 |
(*Unification options*) |
|
33 |
||
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset
|
34 |
(*tracing starts above this depth, 0 for full*) |
39163
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39116
diff
changeset
|
35 |
val trace_bound_raw = Config.declare_global "unify_trace_bound" (K (Config.Int 50)); |
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39116
diff
changeset
|
36 |
val trace_bound = Config.int trace_bound_raw; |
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset
|
37 |
|
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset
|
38 |
(*unification quits above this depth*) |
39163
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39116
diff
changeset
|
39 |
val search_bound_raw = Config.declare_global "unify_search_bound" (K (Config.Int 60)); |
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39116
diff
changeset
|
40 |
val search_bound = Config.int search_bound_raw; |
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset
|
41 |
|
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset
|
42 |
(*print dpairs before calling SIMPL*) |
39163
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39116
diff
changeset
|
43 |
val trace_simp_raw = Config.declare_global "unify_trace_simp" (K (Config.Bool false)); |
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39116
diff
changeset
|
44 |
val trace_simp = Config.bool trace_simp_raw; |
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset
|
45 |
|
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset
|
46 |
(*announce potential incompleteness of type unification*) |
39163
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39116
diff
changeset
|
47 |
val trace_types_raw = Config.declare_global "unify_trace_types" (K (Config.Bool false)); |
4d701c0388c3
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents:
39116
diff
changeset
|
48 |
val trace_types = Config.bool trace_types_raw; |
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset
|
49 |
|
0 | 50 |
|
51 |
type binderlist = (string*typ) list; |
|
52 |
||
53 |
type dpair = binderlist * term * term; |
|
54 |
||
32032 | 55 |
fun body_type env = |
56 |
let |
|
57 |
val tyenv = Envir.type_env env; |
|
58 |
fun bT (Type ("fun", [_, T])) = bT T |
|
59 |
| bT (T as TVar v) = |
|
60 |
(case Type.lookup tyenv v of |
|
61 |
NONE => T |
|
62 |
| SOME T' => bT T') |
|
63 |
| bT T = T; |
|
64 |
in bT end; |
|
0 | 65 |
|
32032 | 66 |
fun binder_types env = |
67 |
let |
|
68 |
val tyenv = Envir.type_env env; |
|
69 |
fun bTs (Type ("fun", [T, U])) = T :: bTs U |
|
37636 | 70 |
| bTs (TVar v) = |
32032 | 71 |
(case Type.lookup tyenv v of |
72 |
NONE => [] |
|
73 |
| SOME T' => bTs T') |
|
74 |
| bTs _ = []; |
|
75 |
in bTs end; |
|
0 | 76 |
|
77 |
fun strip_type env T = (binder_types env T, body_type env T); |
|
78 |
||
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
8406
diff
changeset
|
79 |
fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t; |
0 | 80 |
|
81 |
||
32032 | 82 |
(* eta normal form *) |
83 |
||
84 |
fun eta_norm env = |
|
85 |
let |
|
86 |
val tyenv = Envir.type_env env; |
|
87 |
fun etif (Type ("fun", [T, U]), t) = |
|
88 |
Abs ("", T, etif (U, incr_boundvars 1 t $ Bound 0)) |
|
89 |
| etif (TVar v, t) = |
|
90 |
(case Type.lookup tyenv v of |
|
91 |
NONE => t |
|
92 |
| SOME T => etif (T, t)) |
|
93 |
| etif (_, t) = t; |
|
94 |
fun eta_nm (rbinder, Abs (a, T, body)) = |
|
95 |
Abs (a, T, eta_nm ((a, T) :: rbinder, body)) |
|
96 |
| eta_nm (rbinder, t) = etif (fastype env (rbinder, t), t); |
|
0 | 97 |
in eta_nm end; |
98 |
||
99 |
||
100 |
(*OCCURS CHECK |
|
19864 | 101 |
Does the uvar occur in the term t? |
0 | 102 |
two forms of search, for whether there is a rigid path to the current term. |
103 |
"seen" is list of variables passed thru, is a memo variable for sharing. |
|
15797 | 104 |
This version searches for nonrigid occurrence, returns true if found. |
105 |
Since terms may contain variables with same name and different types, |
|
106 |
the occurs check must ignore the types of variables. This avoids |
|
107 |
that ?x::?'a is unified with f(?x::T), which may lead to a cyclic |
|
108 |
substitution when ?'a is instantiated with T later. *) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
109 |
fun occurs_terms (seen: indexname list Unsynchronized.ref, |
19864 | 110 |
env: Envir.env, v: indexname, ts: term list): bool = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
111 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
112 |
fun occurs [] = false |
37636 | 113 |
| occurs (t :: ts) = occur t orelse occurs ts |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
114 |
and occur (Const _) = false |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
115 |
| occur (Bound _) = false |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
116 |
| occur (Free _) = false |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
117 |
| occur (Var (w, T)) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
118 |
if member (op =) (!seen) w then false |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
119 |
else if Term.eq_ix (v, w) then true |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
120 |
(*no need to lookup: v has no assignment*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
121 |
else |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
122 |
(seen := w :: !seen; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
123 |
case Envir.lookup (env, (w, T)) of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
124 |
NONE => false |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
125 |
| SOME t => occur t) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
126 |
| occur (Abs (_, _, body)) = occur body |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
127 |
| occur (f $ t) = occur t orelse occur f; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
128 |
in occurs ts end; |
0 | 129 |
|
130 |
||
131 |
(* f(a1,...,an) ----> (f, [a1,...,an]) using the assignments*) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
132 |
fun head_of_in (env, t) : term = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
133 |
(case t of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
134 |
f $ _ => head_of_in (env, f) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
135 |
| Var vT => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
136 |
(case Envir.lookup (env, vT) of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
137 |
SOME u => head_of_in (env, u) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
138 |
| NONE => t) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
139 |
| _ => t); |
0 | 140 |
|
141 |
||
142 |
datatype occ = NoOcc | Nonrigid | Rigid; |
|
143 |
||
144 |
(* Rigid occur check |
|
145 |
Returns Rigid if it finds a rigid occurrence of the variable, |
|
146 |
Nonrigid if it finds a nonrigid path to the variable. |
|
147 |
NoOcc otherwise. |
|
148 |
Continues searching for a rigid occurrence even if it finds a nonrigid one. |
|
149 |
||
150 |
Condition for detecting non-unifable terms: [ section 5.3 of Huet (1975) ] |
|
151 |
a rigid path to the variable, appearing with no arguments. |
|
152 |
Here completeness is sacrificed in order to reduce danger of divergence: |
|
153 |
reject ALL rigid paths to the variable. |
|
19864 | 154 |
Could check for rigid paths to bound variables that are out of scope. |
0 | 155 |
Not necessary because the assignment test looks at variable's ENTIRE rbinder. |
156 |
||
157 |
Treatment of head(arg1,...,argn): |
|
158 |
If head is a variable then no rigid path, switch to nonrigid search |
|
19864 | 159 |
for arg1,...,argn. |
160 |
If head is an abstraction then possibly no rigid path (head could be a |
|
0 | 161 |
constant function) so again use nonrigid search. Happens only if |
19864 | 162 |
term is not in normal form. |
0 | 163 |
|
164 |
Warning: finds a rigid occurrence of ?f in ?f(t). |
|
165 |
Should NOT be called in this case: there is a flex-flex unifier |
|
166 |
*) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
167 |
fun rigid_occurs_term (seen: indexname list Unsynchronized.ref, env, v: indexname, t) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
168 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
169 |
fun nonrigid t = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
170 |
if occurs_terms (seen, env, v, [t]) then Nonrigid |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
171 |
else NoOcc |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
172 |
fun occurs [] = NoOcc |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
173 |
| occurs (t :: ts) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
174 |
(case occur t of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
175 |
Rigid => Rigid |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
176 |
| oc => (case occurs ts of NoOcc => oc | oc2 => oc2)) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
177 |
and occomb (f $ t) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
178 |
(case occur t of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
179 |
Rigid => Rigid |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
180 |
| oc => (case occomb f of NoOcc => oc | oc2 => oc2)) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
181 |
| occomb t = occur t |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
182 |
and occur (Const _) = NoOcc |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
183 |
| occur (Bound _) = NoOcc |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
184 |
| occur (Free _) = NoOcc |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
185 |
| occur (Var (w, T)) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
186 |
if member (op =) (!seen) w then NoOcc |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
187 |
else if Term.eq_ix (v, w) then Rigid |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
188 |
else |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
189 |
(seen := w :: !seen; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
190 |
case Envir.lookup (env, (w, T)) of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
191 |
NONE => NoOcc |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
192 |
| SOME t => occur t) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
193 |
| occur (Abs (_, _, body)) = occur body |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
194 |
| occur (t as f $ _) = (*switch to nonrigid search?*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
195 |
(case head_of_in (env, f) of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
196 |
Var (w,_) => (*w is not assigned*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
197 |
if Term.eq_ix (v, w) then Rigid |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
198 |
else nonrigid t |
37636 | 199 |
| Abs _ => nonrigid t (*not in normal form*) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
200 |
| _ => occomb t) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
201 |
in occur t end; |
0 | 202 |
|
203 |
||
19864 | 204 |
exception CANTUNIFY; (*Signals non-unifiability. Does not signal errors!*) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
205 |
exception ASSIGN; (*Raised if not an assignment*) |
0 | 206 |
|
207 |
||
32032 | 208 |
fun unify_types thy (T, U, env) = |
209 |
if T = U then env |
|
210 |
else |
|
211 |
let |
|
212 |
val Envir.Envir {maxidx, tenv, tyenv} = env; |
|
213 |
val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx); |
|
214 |
in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end |
|
215 |
handle Type.TUNIFY => raise CANTUNIFY; |
|
0 | 216 |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
217 |
fun test_unify_types thy (args as (T, U, _)) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
218 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
219 |
val str_of = Syntax.string_of_typ_global thy; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
220 |
fun warn () = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
221 |
val env' = unify_types thy args; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
222 |
in if is_TVar T orelse is_TVar U then warn () else (); env' end; |
0 | 223 |
|
224 |
(*Is the term eta-convertible to a single variable with the given rbinder? |
|
225 |
Examples: ?a ?f(B.0) ?g(B.1,B.0) |
|
226 |
Result is var a for use in SIMPL. *) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
227 |
fun get_eta_var ([], _, Var vT) = vT |
0 | 228 |
| get_eta_var (_::rbinder, n, f $ Bound i) = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
229 |
if n = i then get_eta_var (rbinder, n + 1, f) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
230 |
else raise ASSIGN |
0 | 231 |
| get_eta_var _ = raise ASSIGN; |
232 |
||
233 |
||
234 |
(*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u. |
|
235 |
If v occurs rigidly then nonunifiable. |
|
236 |
If v occurs nonrigidly then must use full algorithm. *) |
|
16664 | 237 |
fun assignment thy (env, rbinder, t, u) = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
238 |
let val vT as (v,T) = get_eta_var (rbinder, 0, t) in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
239 |
(case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
240 |
NoOcc => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
241 |
let val env = unify_types thy (body_type env T, fastype env (rbinder, u), env) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
242 |
in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
243 |
| Nonrigid => raise ASSIGN |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
244 |
| Rigid => raise CANTUNIFY) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
245 |
end; |
0 | 246 |
|
247 |
||
248 |
(*Extends an rbinder with a new disagreement pair, if both are abstractions. |
|
249 |
Tries to unify types of the bound variables! |
|
250 |
Checks that binders have same length, since terms should be eta-normal; |
|
251 |
if not, raises TERM, probably indicating type mismatch. |
|
19864 | 252 |
Uses variable a (unless the null string) to preserve user's naming.*) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
253 |
fun new_dpair thy (rbinder, Abs (a, T, body1), Abs (b, U, body2), env) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
254 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
255 |
val env' = unify_types thy (T, U, env); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
256 |
val c = if a = "" then b else a; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
257 |
in new_dpair thy ((c,T) :: rbinder, body1, body2, env') end |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
258 |
| new_dpair _ (_, Abs _, _, _) = raise TERM ("new_dpair", []) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
259 |
| new_dpair _ (_, _, Abs _, _) = raise TERM ("new_dpair", []) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
260 |
| new_dpair _ (rbinder, t1, t2, env) = ((rbinder, t1, t2), env); |
0 | 261 |
|
262 |
||
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
263 |
fun head_norm_dpair thy (env, (rbinder, t, u)) : dpair * Envir.env = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
264 |
new_dpair thy (rbinder, |
19864 | 265 |
eta_norm env (rbinder, Envir.head_norm env t), |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
266 |
eta_norm env (rbinder, Envir.head_norm env u), env); |
0 | 267 |
|
268 |
||
269 |
||
270 |
(*flexflex: the flex-flex pairs, flexrigid: the flex-rigid pairs |
|
271 |
Does not perform assignments for flex-flex pairs: |
|
646 | 272 |
may create nonrigid paths, which prevent other assignments. |
273 |
Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to |
|
274 |
do so caused numerous problems with no compensating advantage. |
|
275 |
*) |
|
48263 | 276 |
fun SIMPL0 thy dp0 (env,flexflex,flexrigid) : Envir.env * dpair list * dpair list = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
277 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
278 |
val (dp as (rbinder, t, u), env) = head_norm_dpair thy (env, dp0); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
279 |
fun SIMRANDS (f $ t, g $ u, env) = |
48263 | 280 |
SIMPL0 thy (rbinder, t, u) (SIMRANDS (f, g, env)) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
281 |
| SIMRANDS (t as _$_, _, _) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
282 |
raise TERM ("SIMPL: operands mismatch", [t, u]) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
283 |
| SIMRANDS (t, u as _ $ _, _) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
284 |
raise TERM ("SIMPL: operands mismatch", [t, u]) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
285 |
| SIMRANDS (_, _, env) = (env, flexflex, flexrigid); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
286 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
287 |
(case (head_of t, head_of u) of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
288 |
(Var (_, T), Var (_, U)) => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
289 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
290 |
val T' = body_type env T and U' = body_type env U; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
291 |
val env = unify_types thy (T', U', env); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
292 |
in (env, dp :: flexflex, flexrigid) end |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
293 |
| (Var _, _) => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
294 |
((assignment thy (env, rbinder,t,u), flexflex, flexrigid) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
295 |
handle ASSIGN => (env, flexflex, dp :: flexrigid)) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
296 |
| (_, Var _) => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
297 |
((assignment thy (env, rbinder, u, t), flexflex, flexrigid) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
298 |
handle ASSIGN => (env, flexflex, (rbinder, u, t) :: flexrigid)) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
299 |
| (Const (a, T), Const (b, U)) => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
300 |
if a = b then SIMRANDS (t, u, unify_types thy (T, U, env)) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
301 |
else raise CANTUNIFY |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
302 |
| (Bound i, Bound j) => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
303 |
if i = j then SIMRANDS (t, u, env) else raise CANTUNIFY |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
304 |
| (Free (a, T), Free (b, U)) => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
305 |
if a = b then SIMRANDS (t, u, unify_types thy (T, U, env)) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
306 |
else raise CANTUNIFY |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
307 |
| _ => raise CANTUNIFY) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
308 |
end; |
0 | 309 |
|
310 |
||
311 |
(* changed(env,t) checks whether the head of t is a variable assigned in env*) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
312 |
fun changed (env, f $ _) = changed (env, f) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
313 |
| changed (env, Var v) = (case Envir.lookup (env, v) of NONE => false | _ => true) |
0 | 314 |
| changed _ = false; |
315 |
||
316 |
||
317 |
(*Recursion needed if any of the 'head variables' have been updated |
|
318 |
Clever would be to re-do just the affected dpairs*) |
|
16664 | 319 |
fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
320 |
let |
48263 | 321 |
val all as (env', flexflex, flexrigid) = fold_rev (SIMPL0 thy) dpairs (env, [], []); |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
322 |
val dps = flexrigid @ flexflex; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
323 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
324 |
if exists (fn (_, t, u) => changed (env', t) orelse changed (env', u)) dps |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
325 |
then SIMPL thy (env', dps) else all |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
326 |
end; |
0 | 327 |
|
328 |
||
19864 | 329 |
(*Makes the terms E1,...,Em, where Ts = [T...Tm]. |
0 | 330 |
Each Ei is ?Gi(B.(n-1),...,B.0), and has type Ti |
331 |
The B.j are bound vars of binder. |
|
19864 | 332 |
The terms are not made in eta-normal-form, SIMPL does that later. |
0 | 333 |
If done here, eta-expansion must be recursive in the arguments! *) |
37636 | 334 |
fun make_args _ (_, env, []) = (env, []) (*frequent case*) |
0 | 335 |
| make_args name (binder: typ list, env, Ts) : Envir.env * term list = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
336 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
337 |
fun funtype T = binder ---> T; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
338 |
val (env', vars) = Envir.genvars name (env, map funtype Ts); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
339 |
in (env', map (fn var => Logic.combound (var, 0, length binder)) vars) end; |
0 | 340 |
|
341 |
||
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42279
diff
changeset
|
342 |
(*Abstraction over a list of types*) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
343 |
fun types_abs ([], u) = u |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
344 |
| types_abs (T :: Ts, u) = Abs ("", T, types_abs (Ts, u)); |
0 | 345 |
|
346 |
(*Abstraction over the binder of a type*) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
347 |
fun type_abs (env, T, t) = types_abs (binder_types env T, t); |
0 | 348 |
|
349 |
||
350 |
(*MATCH taking "big steps". |
|
351 |
Copies u into the Var v, using projection on targs or imitation. |
|
352 |
A projection is allowed unless SIMPL raises an exception. |
|
353 |
Allocates new variables in projection on a higher-order argument, |
|
354 |
or if u is a variable (flex-flex dpair). |
|
355 |
Returns long sequence of every way of copying u, for backtracking |
|
356 |
For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a. |
|
19864 | 357 |
The order for trying projections is crucial in ?b'(?a) |
0 | 358 |
NB "vname" is only used in the call to make_args!! *) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
359 |
fun matchcopy thy vname = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
360 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
361 |
fun mc (rbinder, targs, u, ed as (env, dpairs)) : (term * (Envir.env * dpair list)) Seq.seq = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
362 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
363 |
val trace_tps = Config.get_global thy trace_types; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
364 |
(*Produce copies of uarg and cons them in front of uargs*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
365 |
fun copycons uarg (uargs, (env, dpairs)) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
366 |
Seq.map (fn (uarg', ed') => (uarg' :: uargs, ed')) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
367 |
(mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg), |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
368 |
(env, dpairs))); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
369 |
(*Produce sequence of all possible ways of copying the arg list*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
370 |
fun copyargs [] = Seq.cons ([], ed) Seq.empty |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
371 |
| copyargs (uarg :: uargs) = Seq.maps (copycons uarg) (copyargs uargs); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
372 |
val (uhead, uargs) = strip_comb u; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
373 |
val base = body_type env (fastype env (rbinder, uhead)); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
374 |
fun joinargs (uargs', ed') = (list_comb (uhead, uargs'), ed'); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
375 |
(*attempt projection on argument with given typ*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
376 |
val Ts = map (curry (fastype env) rbinder) targs; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
377 |
fun projenv (head, (Us, bary), targ, tail) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
378 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
379 |
val env = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
380 |
if trace_tps then test_unify_types thy (base, bary, env) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
381 |
else unify_types thy (base, bary, env) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
382 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
383 |
Seq.make (fn () => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
384 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
385 |
val (env', args) = make_args vname (Ts, env, Us); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
386 |
(*higher-order projection: plug in targs for bound vars*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
387 |
fun plugin arg = list_comb (head_of arg, targs); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
388 |
val dp = (rbinder, list_comb (targ, map plugin args), u); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
389 |
val (env2, frigid, fflex) = SIMPL thy (env', dp :: dpairs); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
390 |
(*may raise exception CANTUNIFY*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
391 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
392 |
SOME ((list_comb (head, args), (env2, frigid @ fflex)), tail) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
393 |
end handle CANTUNIFY => Seq.pull tail) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
394 |
end handle CANTUNIFY => tail; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
395 |
(*make a list of projections*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
396 |
fun make_projs (T::Ts, targ::targs) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
397 |
(Bound(length Ts), T, targ) :: make_projs (Ts,targs) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
398 |
| make_projs ([],[]) = [] |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
399 |
| make_projs _ = raise TERM ("make_projs", u::targs); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
400 |
(*try projections and imitation*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
401 |
fun matchfun ((bvar,T,targ)::projs) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
402 |
(projenv(bvar, strip_type env T, targ, matchfun projs)) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
403 |
| matchfun [] = (*imitation last of all*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
404 |
(case uhead of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
405 |
Const _ => Seq.map joinargs (copyargs uargs) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
406 |
| Free _ => Seq.map joinargs (copyargs uargs) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
407 |
| _ => Seq.empty) (*if Var, would be a loop!*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
408 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
409 |
(case uhead of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
410 |
Abs (a, T, body) => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
411 |
Seq.map (fn (body', ed') => (Abs (a, T, body'), ed')) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
412 |
(mc ((a, T) :: rbinder, (map (incr_boundvars 1) targs) @ [Bound 0], body, ed)) |
37636 | 413 |
| Var (w, _) => |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
414 |
(*a flex-flex dpair: make variable for t*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
415 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
416 |
val (env', newhd) = Envir.genvar (#1 w) (env, Ts ---> base); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
417 |
val tabs = Logic.combound (newhd, 0, length Ts); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
418 |
val tsub = list_comb (newhd, targs); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
419 |
in Seq.single (tabs, (env', (rbinder, tsub, u) :: dpairs)) end |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
420 |
| _ => matchfun (rev (make_projs (Ts, targs)))) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
421 |
end; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
422 |
in mc end; |
0 | 423 |
|
424 |
||
425 |
(*Call matchcopy to produce assignments to the variable in the dpair*) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
426 |
fun MATCH thy (env, (rbinder, t, u), dpairs) : (Envir.env * dpair list) Seq.seq = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
427 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
428 |
val (Var (vT as (v, T)), targs) = strip_comb t; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
429 |
val Ts = binder_types env T; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
430 |
fun new_dset (u', (env', dpairs')) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
431 |
(*if v was updated to s, must unify s with u' *) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
432 |
(case Envir.lookup (env', vT) of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
433 |
NONE => (Envir.update ((vT, types_abs (Ts, u')), env'), dpairs') |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
434 |
| SOME s => (env', ([], s, types_abs (Ts, u')) :: dpairs')); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
435 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
436 |
Seq.map new_dset (matchcopy thy (#1 v) (rbinder, targs, u, (env, dpairs))) |
0 | 437 |
end; |
438 |
||
439 |
||
440 |
||
441 |
(**** Flex-flex processing ****) |
|
442 |
||
19864 | 443 |
(*At end of unification, do flex-flex assignments like ?a -> ?f(?b) |
0 | 444 |
Attempts to update t with u, raising ASSIGN if impossible*) |
19864 | 445 |
fun ff_assign thy (env, rbinder, t, u) : Envir.env = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
446 |
let val vT as (v, T) = get_eta_var (rbinder, 0, t) in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
447 |
if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
448 |
else |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
449 |
let val env = unify_types thy (body_type env T, fastype env (rbinder, u), env) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
450 |
in Envir.vupdate ((vT, Logic.rlist_abs (rbinder, u)), env) end |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
451 |
end; |
0 | 452 |
|
453 |
||
37720
50a9e2fa4f6b
Unification (flexflex) bug fix; making "auto" deterministic
paulson
parents:
37637
diff
changeset
|
454 |
(*If an argument contains a banned Bound, then it should be deleted. |
50a9e2fa4f6b
Unification (flexflex) bug fix; making "auto" deterministic
paulson
parents:
37637
diff
changeset
|
455 |
But if the only path is flexible, this is difficult; the code gives up! |
50a9e2fa4f6b
Unification (flexflex) bug fix; making "auto" deterministic
paulson
parents:
37637
diff
changeset
|
456 |
In %x y.?a(x) =?= %x y.?b(?c(y)) should we instantiate ?b or ?c *) |
50a9e2fa4f6b
Unification (flexflex) bug fix; making "auto" deterministic
paulson
parents:
37637
diff
changeset
|
457 |
exception CHANGE_FAIL; (*flexible occurrence of banned variable, or other reason to quit*) |
50a9e2fa4f6b
Unification (flexflex) bug fix; making "auto" deterministic
paulson
parents:
37637
diff
changeset
|
458 |
|
50a9e2fa4f6b
Unification (flexflex) bug fix; making "auto" deterministic
paulson
parents:
37637
diff
changeset
|
459 |
|
0 | 460 |
(*Flex argument: a term, its type, and the index that refers to it.*) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
461 |
type flarg = {t: term, T: typ, j: int}; |
0 | 462 |
|
463 |
(*Form the arguments into records for deletion/sorting.*) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
464 |
fun flexargs ([], [], []) = [] : flarg list |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
465 |
| flexargs (j :: js, t :: ts, T :: Ts) = {j = j, t = t, T = T} :: flexargs (js, ts, Ts) |
37720
50a9e2fa4f6b
Unification (flexflex) bug fix; making "auto" deterministic
paulson
parents:
37637
diff
changeset
|
466 |
| flexargs _ = raise CHANGE_FAIL; |
41422
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
467 |
(*We give up if we see a variable of function type not applied to a full list of |
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
468 |
arguments (remember, this code assumes that terms are fully eta-expanded). This situation |
37720
50a9e2fa4f6b
Unification (flexflex) bug fix; making "auto" deterministic
paulson
parents:
37637
diff
changeset
|
469 |
can occur if a type variable is instantiated with a function type. |
50a9e2fa4f6b
Unification (flexflex) bug fix; making "auto" deterministic
paulson
parents:
37637
diff
changeset
|
470 |
*) |
0 | 471 |
|
651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEX-FLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset
|
472 |
(*Check whether the 'banned' bound var indices occur rigidly in t*) |
19864 | 473 |
fun rigid_bound (lev, banned) t = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
474 |
let val (head,args) = strip_comb t in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
475 |
(case head of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
476 |
Bound i => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
477 |
member (op =) banned (i - lev) orelse exists (rigid_bound (lev, banned)) args |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
478 |
| Var _ => false (*no rigid occurrences here!*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
479 |
| Abs (_, _, u) => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
480 |
rigid_bound (lev + 1, banned) u orelse |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
481 |
exists (rigid_bound (lev, banned)) args |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
482 |
| _ => exists (rigid_bound (lev, banned)) args) |
0 | 483 |
end; |
484 |
||
651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEX-FLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset
|
485 |
(*Squash down indices at level >=lev to delete the banned from a term.*) |
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEX-FLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset
|
486 |
fun change_bnos banned = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
487 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
488 |
fun change lev (Bound i) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
489 |
if i < lev then Bound i |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
490 |
else if member (op =) banned (i - lev) then |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
491 |
raise CHANGE_FAIL (**flexible occurrence: give up**) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
492 |
else Bound (i - length (filter (fn j => j < i - lev) banned)) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
493 |
| change lev (Abs (a, T, t)) = Abs (a, T, change(lev + 1) t) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
494 |
| change lev (t $ u) = change lev t $ change lev u |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
495 |
| change lev t = t; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
496 |
in change 0 end; |
0 | 497 |
|
498 |
(*Change indices, delete the argument if it contains a banned Bound*) |
|
48263 | 499 |
fun change_arg banned {j, t, T} args : flarg list = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
500 |
if rigid_bound (0, banned) t then args (*delete argument!*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
501 |
else {j = j, t = change_bnos banned t, T = T} :: args; |
0 | 502 |
|
503 |
||
504 |
(*Sort the arguments to create assignments if possible: |
|
48262
a0d8abca8d7a
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset
|
505 |
create eta-terms like ?g B.1 B.0*) |
a0d8abca8d7a
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset
|
506 |
local |
a0d8abca8d7a
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset
|
507 |
fun less_arg ({t = Bound i1, ...}, {t = Bound i2, ...}) = (i2 < i1) |
a0d8abca8d7a
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset
|
508 |
| less_arg (_: flarg, _: flarg) = false; |
a0d8abca8d7a
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset
|
509 |
|
a0d8abca8d7a
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset
|
510 |
fun ins_arg x [] = [x] |
a0d8abca8d7a
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset
|
511 |
| ins_arg x (y :: ys) = |
a0d8abca8d7a
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset
|
512 |
if less_arg (y, x) then y :: ins_arg x ys else x :: y :: ys; |
a0d8abca8d7a
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset
|
513 |
in |
a0d8abca8d7a
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset
|
514 |
fun sort_args [] = [] |
a0d8abca8d7a
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset
|
515 |
| sort_args (x :: xs) = ins_arg x (sort_args xs); |
a0d8abca8d7a
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset
|
516 |
end; |
0 | 517 |
|
518 |
(*Test whether the new term would be eta-equivalent to a variable -- |
|
519 |
if so then there is no point in creating a new variable*) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
520 |
fun decreasing n ([]: flarg list) = (n = 0) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
521 |
| decreasing n ({j, ...} :: args) = j = n - 1 andalso decreasing (n - 1) args; |
0 | 522 |
|
523 |
(*Delete banned indices in the term, simplifying it. |
|
524 |
Force an assignment, if possible, by sorting the arguments. |
|
525 |
Update its head; squash indices in arguments. *) |
|
526 |
fun clean_term banned (env,t) = |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
527 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
528 |
val (Var (v, T), ts) = strip_comb t; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
529 |
val (Ts, U) = strip_type env T |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
530 |
and js = length ts - 1 downto 0; |
48263 | 531 |
val args = sort_args (fold_rev (change_arg banned) (flexargs (js, ts, Ts)) []) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
532 |
val ts' = map #t args; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
533 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
534 |
if decreasing (length Ts) args then (env, (list_comb (Var (v, T), ts'))) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
535 |
else |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
536 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
537 |
val (env', v') = Envir.genvar (#1 v) (env, map #T args ---> U); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
538 |
val body = list_comb (v', map (Bound o #j) args); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
539 |
val env2 = Envir.vupdate ((((v, T), types_abs (Ts, body)), env')); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
540 |
(*the vupdate affects ts' if they contain v*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
541 |
in (env2, Envir.norm_term env2 (list_comb (v', ts'))) end |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
542 |
end; |
0 | 543 |
|
544 |
||
545 |
(*Add tpair if not trivial or already there. |
|
546 |
Should check for swapped pairs??*) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
547 |
fun add_tpair (rbinder, (t0, u0), tpairs) : (term * term) list = |
19864 | 548 |
if t0 aconv u0 then tpairs |
0 | 549 |
else |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
550 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
551 |
val t = Logic.rlist_abs (rbinder, t0) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
552 |
and u = Logic.rlist_abs (rbinder, u0); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
553 |
fun same (t', u') = (t aconv t') andalso (u aconv u') |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
554 |
in if exists same tpairs then tpairs else (t, u) :: tpairs end; |
0 | 555 |
|
556 |
||
557 |
(*Simplify both terms and check for assignments. |
|
558 |
Bound vars in the binder are "banned" unless used in both t AND u *) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
559 |
fun clean_ffpair thy ((rbinder, t, u), (env, tpairs)) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
560 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
561 |
val loot = loose_bnos t and loou = loose_bnos u |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
562 |
fun add_index (j, (a, T)) (bnos, newbinder) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
563 |
if member (op =) loot j andalso member (op =) loou j |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
564 |
then (bnos, (a, T) :: newbinder) (*needed by both: keep*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
565 |
else (j :: bnos, newbinder); (*remove*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
566 |
val (banned, rbin') = fold_rev add_index ((0 upto (length rbinder - 1)) ~~ rbinder) ([], []); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
567 |
val (env', t') = clean_term banned (env, t); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
568 |
val (env'',u') = clean_term banned (env',u); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
569 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
570 |
(ff_assign thy (env'', rbin', t', u'), tpairs) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
571 |
handle ASSIGN => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
572 |
(ff_assign thy (env'', rbin', u', t'), tpairs) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
573 |
handle ASSIGN => (env'', add_tpair (rbin', (t', u'), tpairs)) |
0 | 574 |
end |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
575 |
handle CHANGE_FAIL => (env, add_tpair (rbinder, (t, u), tpairs)); |
0 | 576 |
|
577 |
||
578 |
(*IF the flex-flex dpair is an assignment THEN do it ELSE put in tpairs |
|
579 |
eliminates trivial tpairs like t=t, as well as repeated ones |
|
19864 | 580 |
trivial tpairs can easily escape SIMPL: ?A=t, ?A=?B, ?B=t gives t=t |
0 | 581 |
Resulting tpairs MAY NOT be in normal form: assignments may occur here.*) |
48263 | 582 |
fun add_ffpair thy (rbinder,t0,u0) (env,tpairs) : Envir.env * (term * term) list = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
583 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
584 |
val t = Envir.norm_term env t0 |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
585 |
and u = Envir.norm_term env u0; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
586 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
587 |
(case (head_of t, head_of u) of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
588 |
(Var (v, T), Var (w, U)) => (*Check for identical variables...*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
589 |
if Term.eq_ix (v, w) then (*...occur check would falsely return true!*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
590 |
if T = U then (env, add_tpair (rbinder, (t, u), tpairs)) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
591 |
else raise TERM ("add_ffpair: Var name confusion", [t, u]) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
592 |
else if Term_Ord.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
593 |
clean_ffpair thy ((rbinder, u, t), (env, tpairs)) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
594 |
else clean_ffpair thy ((rbinder, t, u), (env, tpairs)) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
595 |
| _ => raise TERM ("add_ffpair: Vars expected", [t, u])) |
0 | 596 |
end; |
597 |
||
598 |
||
599 |
(*Print a tracing message + list of dpairs. |
|
600 |
In t==u print u first because it may be rigid or flexible -- |
|
601 |
t is always flexible.*) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
602 |
fun print_dpairs thy msg (env, dpairs) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
603 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
604 |
fun pdp (rbinder, t, u) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
605 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
606 |
fun termT t = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
607 |
Syntax.pretty_term_global thy (Envir.norm_term env (Logic.rlist_abs (rbinder, t))); |
42279
6da43a5018e2
constant =?= no longer exists (cf. 8c09e1fa24a7);
wenzelm
parents:
41422
diff
changeset
|
608 |
val bsymbs = [termT u, Pretty.str " =?=", Pretty.brk 1, termT t]; |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
609 |
in tracing (Pretty.string_of (Pretty.blk (0, bsymbs))) end; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
610 |
in tracing msg; List.app pdp dpairs end; |
0 | 611 |
|
612 |
||
613 |
(*Unify the dpairs in the environment. |
|
19864 | 614 |
Returns flex-flex disagreement pairs NOT IN normal form. |
0 | 615 |
SIMPL may raise exception CANTUNIFY. *) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
616 |
fun hounifiers (thy, env, tus : (term * term) list) : (Envir.env * (term * term) list) Seq.seq = |
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset
|
617 |
let |
36787
f60e4dd6d76f
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
wenzelm
parents:
36001
diff
changeset
|
618 |
val trace_bnd = Config.get_global thy trace_bound; |
f60e4dd6d76f
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
wenzelm
parents:
36001
diff
changeset
|
619 |
val search_bnd = Config.get_global thy search_bound; |
f60e4dd6d76f
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
wenzelm
parents:
36001
diff
changeset
|
620 |
val trace_smp = Config.get_global thy trace_simp; |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
621 |
fun add_unify tdepth ((env, dpairs), reseq) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
622 |
Seq.make (fn () => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
623 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
624 |
val (env', flexflex, flexrigid) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
625 |
(if tdepth > trace_bnd andalso trace_smp |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
626 |
then print_dpairs thy "Enter SIMPL" (env, dpairs) else (); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
627 |
SIMPL thy (env, dpairs)); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
628 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
629 |
(case flexrigid of |
48263 | 630 |
[] => SOME (fold_rev (add_ffpair thy) flexflex (env', []), reseq) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
631 |
| dp :: frigid' => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
632 |
if tdepth > search_bnd then |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
633 |
(warning "Unification bound exceeded"; Seq.pull reseq) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
634 |
else |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
635 |
(if tdepth > trace_bnd then |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
636 |
print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
637 |
else (); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
638 |
Seq.pull (Seq.it_right |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
639 |
(add_unify (tdepth + 1)) (MATCH thy (env',dp, frigid'@flexflex), reseq)))) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
640 |
end |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
641 |
handle CANTUNIFY => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
642 |
(if tdepth > trace_bnd then tracing"Failure node" else (); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
643 |
Seq.pull reseq)); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
644 |
val dps = map (fn (t, u) => ([], t, u)) tus; |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset
|
645 |
in add_unify 1 ((env, dps), Seq.empty) end; |
0 | 646 |
|
18184 | 647 |
fun unifiers (params as (thy, env, tus)) = |
19473 | 648 |
Seq.cons (fold (Pattern.unify thy) tus env, []) Seq.empty |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset
|
649 |
handle Pattern.Unif => Seq.empty |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
650 |
| Pattern.Pattern => hounifiers params; |
0 | 651 |
|
652 |
||
653 |
(*For smash_flexflex1*) |
|
654 |
fun var_head_of (env,t) : indexname * typ = |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
655 |
(case head_of (strip_abs_body (Envir.norm_term env t)) of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
656 |
Var (v, T) => (v, T) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
657 |
| _ => raise CANTUNIFY); (*not flexible, cannot use trivial substitution*) |
0 | 658 |
|
659 |
||
660 |
(*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975) |
|
661 |
Unifies ?f(t1...rm) with ?g(u1...un) by ?f -> %x1...xm.?a, ?g -> %x1...xn.?a |
|
19864 | 662 |
Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g -> %(x,y)?a, |
663 |
though just ?g->?f is a more general unifier. |
|
0 | 664 |
Unlike Huet (1975), does not smash together all variables of same type -- |
665 |
requires more work yet gives a less general unifier (fewer variables). |
|
666 |
Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *) |
|
48263 | 667 |
fun smash_flexflex1 (t, u) env : Envir.env = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
668 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
669 |
val vT as (v, T) = var_head_of (env, t) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
670 |
and wU as (w, U) = var_head_of (env, u); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
671 |
val (env', var) = Envir.genvar (#1 v) (env, body_type env T); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
672 |
val env'' = Envir.vupdate ((wU, type_abs (env', U, var)), env'); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
673 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
674 |
if vT = wU then env'' (*the other update would be identical*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
675 |
else Envir.vupdate ((vT, type_abs (env', T, var)), env'') |
0 | 676 |
end; |
677 |
||
678 |
||
679 |
(*Smash all flex-flexpairs. Should allow selection of pairs by a predicate?*) |
|
37636 | 680 |
fun smash_flexflex (env, tpairs) : Envir.env = |
48263 | 681 |
fold_rev smash_flexflex1 tpairs env; |
0 | 682 |
|
683 |
(*Returns unifiers with no remaining disagreement pairs*) |
|
19864 | 684 |
fun smash_unifiers thy tus env = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
685 |
Seq.map smash_flexflex (unifiers (thy, env, tus)); |
0 | 686 |
|
19864 | 687 |
|
688 |
(*Pattern matching*) |
|
32032 | 689 |
fun first_order_matchers thy pairs (Envir.Envir {maxidx, tenv, tyenv}) = |
20020
9e7d3d06c643
matchers: fall back on plain first_order_matchers, not pattern;
wenzelm
parents:
19920
diff
changeset
|
690 |
let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv) |
32032 | 691 |
in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end |
19864 | 692 |
handle Pattern.MATCH => Seq.empty; |
693 |
||
41422
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
694 |
(*General matching -- keep variables disjoint*) |
19864 | 695 |
fun matchers _ [] = Seq.single (Envir.empty ~1) |
696 |
| matchers thy pairs = |
|
697 |
let |
|
698 |
val maxidx = fold (Term.maxidx_term o #2) pairs ~1; |
|
699 |
val offset = maxidx + 1; |
|
700 |
val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs; |
|
701 |
val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1; |
|
702 |
||
703 |
val pat_tvars = fold (Term.add_tvars o #1) pairs' []; |
|
704 |
val pat_vars = fold (Term.add_vars o #1) pairs' []; |
|
705 |
||
706 |
val decr_indexesT = |
|
707 |
Term.map_atyps (fn T as TVar ((x, i), S) => |
|
708 |
if i > maxidx then TVar ((x, i - offset), S) else T | T => T); |
|
709 |
val decr_indexes = |
|
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20098
diff
changeset
|
710 |
Term.map_types decr_indexesT #> |
19864 | 711 |
Term.map_aterms (fn t as Var ((x, i), T) => |
712 |
if i > maxidx then Var ((x, i - offset), T) else t | t => t); |
|
713 |
||
32032 | 714 |
fun norm_tvar env ((x, i), S) = |
41422
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
715 |
let |
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
716 |
val tyenv = Envir.type_env env; |
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
717 |
val T' = Envir.norm_type tyenv (TVar ((x, i), S)); |
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
718 |
in |
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
719 |
if (case T' of TVar (v, _) => v = (x, i) | _ => false) then NONE |
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
720 |
else SOME ((x, i - offset), (S, decr_indexesT T')) |
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
721 |
end; |
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
722 |
|
32032 | 723 |
fun norm_var env ((x, i), T) = |
19864 | 724 |
let |
32032 | 725 |
val tyenv = Envir.type_env env; |
19864 | 726 |
val T' = Envir.norm_type tyenv T; |
727 |
val t' = Envir.norm_term env (Var ((x, i), T')); |
|
41422
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
728 |
in |
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
729 |
if (case t' of Var (v, _) => v = (x, i) | _ => false) then NONE |
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
730 |
else SOME ((x, i - offset), (decr_indexesT T', decr_indexes t')) |
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
731 |
end; |
19864 | 732 |
|
733 |
fun result env = |
|
19876 | 734 |
if Envir.above env maxidx then (* FIXME proper handling of generated vars!? *) |
19864 | 735 |
SOME (Envir.Envir {maxidx = maxidx, |
41422
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
736 |
tyenv = Vartab.make (map_filter (norm_tvar env) pat_tvars), |
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
737 |
tenv = Vartab.make (map_filter (norm_var env) pat_vars)}) |
19866 | 738 |
else NONE; |
19864 | 739 |
|
740 |
val empty = Envir.empty maxidx'; |
|
741 |
in |
|
19876 | 742 |
Seq.append |
19920
8257e52164a1
matchers: try pattern_matchers only *after* general matching (The
wenzelm
parents:
19876
diff
changeset
|
743 |
(Seq.map_filter result (smash_unifiers thy pairs' empty)) |
20020
9e7d3d06c643
matchers: fall back on plain first_order_matchers, not pattern;
wenzelm
parents:
19920
diff
changeset
|
744 |
(first_order_matchers thy pairs empty) |
19864 | 745 |
end; |
746 |
||
747 |
fun matches_list thy ps os = |
|
748 |
length ps = length os andalso is_some (Seq.pull (matchers thy (ps ~~ os))); |
|
749 |
||
0 | 750 |
end; |