author | paulson <lp15@cam.ac.uk> |
Sun, 20 May 2018 18:37:34 +0100 | |
changeset 68239 | 0764ee22a4d1 |
parent 67725 | e6cd1fd4eb19 |
child 69575 | f77cc54f6d47 |
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 |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
22 |
val hounifiers: Context.generic * Envir.env * ((term * term) list) -> |
52126 | 23 |
(Envir.env * (term * term) list) Seq.seq |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
24 |
val unifiers: Context.generic * Envir.env * ((term * term) list) -> |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset
|
25 |
(Envir.env * (term * term) list) Seq.seq |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
26 |
val smash_unifiers: Context.generic -> (term * term) list -> Envir.env -> Envir.env Seq.seq |
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*) |
64556 | 35 |
val trace_bound_raw = Config.declare ("unify_trace_bound", \<^here>) (K (Config.Int 50)); |
39163
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*) |
64556 | 39 |
val search_bound_raw = Config.declare ("unify_search_bound", \<^here>) (K (Config.Int 60)); |
39163
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*) |
64556 | 43 |
val trace_simp_raw = Config.declare ("unify_trace_simp", \<^here>) (K (Config.Bool false)); |
39163
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*) |
64556 | 47 |
val trace_types_raw = Config.declare ("unify_trace_types", \<^here>) (K (Config.Bool false)); |
39163
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 |
|
52126 | 51 |
type binderlist = (string * typ) list; |
0 | 52 |
|
53 |
type dpair = binderlist * term * term; |
|
54 |
||
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
8406
diff
changeset
|
55 |
fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t; |
0 | 56 |
|
57 |
||
32032 | 58 |
(* eta normal form *) |
59 |
||
60 |
fun eta_norm env = |
|
61 |
let |
|
62 |
val tyenv = Envir.type_env env; |
|
63 |
fun etif (Type ("fun", [T, U]), t) = |
|
64 |
Abs ("", T, etif (U, incr_boundvars 1 t $ Bound 0)) |
|
65 |
| etif (TVar v, t) = |
|
66 |
(case Type.lookup tyenv v of |
|
67 |
NONE => t |
|
68 |
| SOME T => etif (T, t)) |
|
69 |
| etif (_, t) = t; |
|
70 |
fun eta_nm (rbinder, Abs (a, T, body)) = |
|
71 |
Abs (a, T, eta_nm ((a, T) :: rbinder, body)) |
|
72 |
| eta_nm (rbinder, t) = etif (fastype env (rbinder, t), t); |
|
0 | 73 |
in eta_nm end; |
74 |
||
75 |
||
76 |
(*OCCURS CHECK |
|
19864 | 77 |
Does the uvar occur in the term t? |
0 | 78 |
two forms of search, for whether there is a rigid path to the current term. |
79 |
"seen" is list of variables passed thru, is a memo variable for sharing. |
|
15797 | 80 |
This version searches for nonrigid occurrence, returns true if found. |
81 |
Since terms may contain variables with same name and different types, |
|
82 |
the occurs check must ignore the types of variables. This avoids |
|
83 |
that ?x::?'a is unified with f(?x::T), which may lead to a cyclic |
|
84 |
substitution when ?'a is instantiated with T later. *) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
85 |
fun occurs_terms (seen: indexname list Unsynchronized.ref, |
19864 | 86 |
env: Envir.env, v: indexname, ts: term list): bool = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
87 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
88 |
fun occurs [] = false |
37636 | 89 |
| occurs (t :: ts) = occur t orelse occurs ts |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
90 |
and occur (Const _) = false |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
91 |
| occur (Bound _) = false |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
92 |
| occur (Free _) = false |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
93 |
| occur (Var (w, T)) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
94 |
if member (op =) (!seen) w then false |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
95 |
else if Term.eq_ix (v, w) then true |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
96 |
(*no need to lookup: v has no assignment*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
97 |
else |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
98 |
(seen := w :: !seen; |
51700 | 99 |
case Envir.lookup env (w, T) of |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
100 |
NONE => false |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
101 |
| SOME t => occur t) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
102 |
| occur (Abs (_, _, body)) = occur body |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
103 |
| occur (f $ t) = occur t orelse occur f; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
104 |
in occurs ts end; |
0 | 105 |
|
106 |
||
52126 | 107 |
(* f a1 ... an ----> f using the assignments*) |
108 |
fun head_of_in env t = |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
109 |
(case t of |
52126 | 110 |
f $ _ => head_of_in env f |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
111 |
| Var vT => |
51700 | 112 |
(case Envir.lookup env vT of |
52126 | 113 |
SOME u => head_of_in env u |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
114 |
| NONE => t) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
115 |
| _ => t); |
0 | 116 |
|
117 |
||
118 |
datatype occ = NoOcc | Nonrigid | Rigid; |
|
119 |
||
120 |
(* Rigid occur check |
|
121 |
Returns Rigid if it finds a rigid occurrence of the variable, |
|
122 |
Nonrigid if it finds a nonrigid path to the variable. |
|
123 |
NoOcc otherwise. |
|
124 |
Continues searching for a rigid occurrence even if it finds a nonrigid one. |
|
125 |
||
126 |
Condition for detecting non-unifable terms: [ section 5.3 of Huet (1975) ] |
|
127 |
a rigid path to the variable, appearing with no arguments. |
|
128 |
Here completeness is sacrificed in order to reduce danger of divergence: |
|
129 |
reject ALL rigid paths to the variable. |
|
19864 | 130 |
Could check for rigid paths to bound variables that are out of scope. |
0 | 131 |
Not necessary because the assignment test looks at variable's ENTIRE rbinder. |
132 |
||
133 |
Treatment of head(arg1,...,argn): |
|
134 |
If head is a variable then no rigid path, switch to nonrigid search |
|
19864 | 135 |
for arg1,...,argn. |
136 |
If head is an abstraction then possibly no rigid path (head could be a |
|
0 | 137 |
constant function) so again use nonrigid search. Happens only if |
19864 | 138 |
term is not in normal form. |
0 | 139 |
|
140 |
Warning: finds a rigid occurrence of ?f in ?f(t). |
|
141 |
Should NOT be called in this case: there is a flex-flex unifier |
|
142 |
*) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
143 |
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
|
144 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
145 |
fun nonrigid t = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
146 |
if occurs_terms (seen, env, v, [t]) then Nonrigid |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
147 |
else NoOcc |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
148 |
fun occurs [] = NoOcc |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
149 |
| occurs (t :: ts) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
150 |
(case occur t of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
151 |
Rigid => Rigid |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
152 |
| oc => (case occurs ts of NoOcc => oc | oc2 => oc2)) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
153 |
and occomb (f $ t) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
154 |
(case occur t of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
155 |
Rigid => Rigid |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
156 |
| oc => (case occomb f of NoOcc => oc | oc2 => oc2)) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
157 |
| occomb t = occur t |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
158 |
and occur (Const _) = NoOcc |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
159 |
| occur (Bound _) = NoOcc |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
160 |
| occur (Free _) = NoOcc |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
161 |
| occur (Var (w, T)) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
162 |
if member (op =) (!seen) w then NoOcc |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
163 |
else if Term.eq_ix (v, w) then Rigid |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
164 |
else |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
165 |
(seen := w :: !seen; |
51700 | 166 |
case Envir.lookup env (w, T) of |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
167 |
NONE => NoOcc |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
168 |
| SOME t => occur t) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
169 |
| occur (Abs (_, _, body)) = occur body |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
170 |
| occur (t as f $ _) = (*switch to nonrigid search?*) |
52126 | 171 |
(case head_of_in env f of |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
172 |
Var (w,_) => (*w is not assigned*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
173 |
if Term.eq_ix (v, w) then Rigid |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
174 |
else nonrigid t |
37636 | 175 |
| Abs _ => nonrigid t (*not in normal form*) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
176 |
| _ => occomb t) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
177 |
in occur t end; |
0 | 178 |
|
179 |
||
19864 | 180 |
exception CANTUNIFY; (*Signals non-unifiability. Does not signal errors!*) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
181 |
exception ASSIGN; (*Raised if not an assignment*) |
0 | 182 |
|
183 |
||
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
184 |
fun unify_types context TU env = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
185 |
Pattern.unify_types context TU env handle Pattern.Unif => raise CANTUNIFY; |
0 | 186 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
187 |
fun test_unify_types context (T, U) env = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
188 |
let |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
189 |
fun trace () = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
190 |
if Context_Position.is_visible_generic context then |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
191 |
let val str_of = Syntax.string_of_typ (Context.proof_of context) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
192 |
in tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T) end |
52701
51dfdcd88e84
guard unify tracing via visible status of global theory;
wenzelm
parents:
52698
diff
changeset
|
193 |
else (); |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
194 |
val env' = unify_types context (T, U) env; |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
195 |
in if is_TVar T orelse is_TVar U then trace () else (); env' end; |
0 | 196 |
|
197 |
(*Is the term eta-convertible to a single variable with the given rbinder? |
|
198 |
Examples: ?a ?f(B.0) ?g(B.1,B.0) |
|
199 |
Result is var a for use in SIMPL. *) |
|
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
|
200 |
fun get_eta_var ([], _, Var vT) = vT |
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
|
201 |
| get_eta_var (_::rbinder, n, f $ Bound i) = |
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
|
202 |
if n = i then get_eta_var (rbinder, n + 1, f) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
203 |
else raise ASSIGN |
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
|
204 |
| get_eta_var _ = raise ASSIGN; |
0 | 205 |
|
206 |
||
207 |
(*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u. |
|
208 |
If v occurs rigidly then nonunifiable. |
|
209 |
If v occurs nonrigidly then must use full algorithm. *) |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
210 |
fun assignment context (rbinder, t, u) env = |
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
|
211 |
let val vT as (v,T) = get_eta_var (rbinder, 0, t) in |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
212 |
(case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
213 |
NoOcc => |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
214 |
let val env = unify_types context (Envir.body_type env T, fastype env (rbinder, u)) env |
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
|
215 |
in Envir.update (vT, Logic.rlist_abs (rbinder, u)) env end |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
216 |
| Nonrigid => raise ASSIGN |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
217 |
| Rigid => raise CANTUNIFY) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
218 |
end; |
0 | 219 |
|
220 |
||
221 |
(*Extends an rbinder with a new disagreement pair, if both are abstractions. |
|
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
|
222 |
Tries to unify types of the bound variables! |
0 | 223 |
Checks that binders have same length, since terms should be eta-normal; |
224 |
if not, raises TERM, probably indicating type mismatch. |
|
19864 | 225 |
Uses variable a (unless the null string) to preserve user's naming.*) |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
226 |
fun new_dpair context (rbinder, Abs (a, T, body1), Abs (b, U, body2)) env = |
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
|
227 |
let |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
228 |
val env' = unify_types context (T, U) env; |
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
|
229 |
val c = if a = "" then b else a; |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
230 |
in new_dpair context ((c,T) :: rbinder, body1, body2) env' end |
52126 | 231 |
| new_dpair _ (_, Abs _, _) _ = raise TERM ("new_dpair", []) |
232 |
| new_dpair _ (_, _, Abs _) _ = raise TERM ("new_dpair", []) |
|
233 |
| new_dpair _ (rbinder, t1, t2) env = ((rbinder, t1, t2), env); |
|
0 | 234 |
|
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
|
235 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
236 |
fun head_norm_dpair context (env, (rbinder, t, u)) : dpair * Envir.env = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
237 |
new_dpair context (rbinder, |
19864 | 238 |
eta_norm env (rbinder, Envir.head_norm env t), |
52126 | 239 |
eta_norm env (rbinder, Envir.head_norm env u)) env; |
0 | 240 |
|
241 |
||
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
|
242 |
|
0 | 243 |
(*flexflex: the flex-flex pairs, flexrigid: the flex-rigid pairs |
244 |
Does not perform assignments for flex-flex pairs: |
|
646 | 245 |
may create nonrigid paths, which prevent other assignments. |
67725 | 246 |
Does not even identify Vars in dpairs such as ?a \<equiv>\<^sup>? ?b; an attempt to |
646 | 247 |
do so caused numerous problems with no compensating advantage. |
248 |
*) |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
249 |
fun SIMPL0 context 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
|
250 |
let |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
251 |
val (dp as (rbinder, t, u), env) = head_norm_dpair context (env, dp0); |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
252 |
fun SIMRANDS (f $ t, g $ u, env) = |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
253 |
SIMPL0 context (rbinder, t, u) (SIMRANDS (f, g, env)) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
254 |
| SIMRANDS (t as _$_, _, _) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
255 |
raise TERM ("SIMPL: operands mismatch", [t, u]) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
256 |
| SIMRANDS (t, u as _ $ _, _) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
257 |
raise TERM ("SIMPL: operands mismatch", [t, u]) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
258 |
| SIMRANDS (_, _, env) = (env, flexflex, flexrigid); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
259 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
260 |
(case (head_of t, head_of u) of |
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
|
261 |
(Var (_, T), Var (_, U)) => |
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
|
262 |
let |
52221 | 263 |
val T' = Envir.body_type env T and U' = Envir.body_type env U; |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
264 |
val env = unify_types context (T', U') env; |
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
|
265 |
in (env, dp :: flexflex, flexrigid) end |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
266 |
| (Var _, _) => |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
267 |
((assignment context (rbinder,t,u) env, flexflex, flexrigid) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
268 |
handle ASSIGN => (env, flexflex, dp :: flexrigid)) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
269 |
| (_, Var _) => |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
270 |
((assignment context (rbinder, u, t) env, flexflex, flexrigid) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
271 |
handle ASSIGN => (env, flexflex, (rbinder, u, t) :: flexrigid)) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
272 |
| (Const (a, T), Const (b, U)) => |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
273 |
if a = b then SIMRANDS (t, u, unify_types context (T, U) env) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
274 |
else raise CANTUNIFY |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
275 |
| (Bound i, Bound j) => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
276 |
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
|
277 |
| (Free (a, T), Free (b, U)) => |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
278 |
if a = b then SIMRANDS (t, u, unify_types context (T, U) env) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
279 |
else raise CANTUNIFY |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
280 |
| _ => raise CANTUNIFY) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
281 |
end; |
0 | 282 |
|
283 |
||
284 |
(* changed(env,t) checks whether the head of t is a variable assigned in env*) |
|
52126 | 285 |
fun changed env (f $ _) = changed env f |
286 |
| changed env (Var v) = (case Envir.lookup env v of NONE => false | _ => true) |
|
287 |
| changed _ _ = false; |
|
0 | 288 |
|
289 |
||
290 |
(*Recursion needed if any of the 'head variables' have been updated |
|
291 |
Clever would be to re-do just the affected dpairs*) |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
292 |
fun SIMPL context (env,dpairs) : Envir.env * dpair list * dpair list = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
293 |
let |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
294 |
val all as (env', flexflex, flexrigid) = fold_rev (SIMPL0 context) dpairs (env, [], []); |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
295 |
val dps = flexrigid @ flexflex; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
296 |
in |
52126 | 297 |
if exists (fn (_, t, u) => changed env' t orelse changed env' u) dps |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
298 |
then SIMPL context (env', dps) else all |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
299 |
end; |
0 | 300 |
|
301 |
||
19864 | 302 |
(*Makes the terms E1,...,Em, where Ts = [T...Tm]. |
0 | 303 |
Each Ei is ?Gi(B.(n-1),...,B.0), and has type Ti |
304 |
The B.j are bound vars of binder. |
|
19864 | 305 |
The terms are not made in eta-normal-form, SIMPL does that later. |
0 | 306 |
If done here, eta-expansion must be recursive in the arguments! *) |
37636 | 307 |
fun make_args _ (_, env, []) = (env, []) (*frequent case*) |
0 | 308 |
| 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
|
309 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
310 |
fun funtype T = binder ---> T; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
311 |
val (env', vars) = Envir.genvars name (env, map funtype Ts); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
312 |
in (env', map (fn var => Logic.combound (var, 0, length binder)) vars) end; |
0 | 313 |
|
314 |
||
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42279
diff
changeset
|
315 |
(*Abstraction over a list of types*) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
316 |
fun types_abs ([], u) = u |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
317 |
| types_abs (T :: Ts, u) = Abs ("", T, types_abs (Ts, u)); |
0 | 318 |
|
319 |
(*Abstraction over the binder of a type*) |
|
52221 | 320 |
fun type_abs (env, T, t) = types_abs (Envir.binder_types env T, t); |
0 | 321 |
|
322 |
||
323 |
(*MATCH taking "big steps". |
|
324 |
Copies u into the Var v, using projection on targs or imitation. |
|
325 |
A projection is allowed unless SIMPL raises an exception. |
|
326 |
Allocates new variables in projection on a higher-order argument, |
|
327 |
or if u is a variable (flex-flex dpair). |
|
328 |
Returns long sequence of every way of copying u, for backtracking |
|
329 |
For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a. |
|
19864 | 330 |
The order for trying projections is crucial in ?b'(?a) |
0 | 331 |
NB "vname" is only used in the call to make_args!! *) |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
332 |
fun matchcopy context vname = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
333 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
334 |
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
|
335 |
let |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
336 |
val trace_types = Config.get_generic context trace_types; |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
337 |
(*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
|
338 |
fun copycons uarg (uargs, (env, dpairs)) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
339 |
Seq.map (fn (uarg', ed') => (uarg' :: uargs, ed')) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
340 |
(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
|
341 |
(env, dpairs))); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
342 |
(*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
|
343 |
fun copyargs [] = Seq.cons ([], ed) Seq.empty |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
344 |
| copyargs (uarg :: uargs) = Seq.maps (copycons uarg) (copyargs uargs); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
345 |
val (uhead, uargs) = strip_comb u; |
52221 | 346 |
val base = Envir.body_type env (fastype env (rbinder, uhead)); |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
347 |
fun joinargs (uargs', ed') = (list_comb (uhead, uargs'), ed'); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
348 |
(*attempt projection on argument with given typ*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
349 |
val Ts = map (curry (fastype env) rbinder) targs; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
350 |
fun projenv (head, (Us, bary), targ, tail) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
351 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
352 |
val env = |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
353 |
if trace_types then test_unify_types context (base, bary) env |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
354 |
else unify_types context (base, bary) env |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
355 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
356 |
Seq.make (fn () => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
357 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
358 |
val (env', args) = make_args vname (Ts, env, Us); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
359 |
(*higher-order projection: plug in targs for bound vars*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
360 |
fun plugin arg = list_comb (head_of arg, targs); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
361 |
val dp = (rbinder, list_comb (targ, map plugin args), u); |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
362 |
val (env2, frigid, fflex) = SIMPL context (env', dp :: dpairs); |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
363 |
(*may raise exception CANTUNIFY*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
364 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
365 |
SOME ((list_comb (head, args), (env2, frigid @ fflex)), tail) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
366 |
end handle CANTUNIFY => Seq.pull tail) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
367 |
end handle CANTUNIFY => tail; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
368 |
(*make a list of projections*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
369 |
fun make_projs (T::Ts, targ::targs) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
370 |
(Bound(length Ts), T, targ) :: make_projs (Ts,targs) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
371 |
| make_projs ([],[]) = [] |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
372 |
| make_projs _ = raise TERM ("make_projs", u::targs); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
373 |
(*try projections and imitation*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
374 |
fun matchfun ((bvar,T,targ)::projs) = |
52221 | 375 |
(projenv(bvar, Envir.strip_type env T, targ, matchfun projs)) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
376 |
| matchfun [] = (*imitation last of all*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
377 |
(case uhead of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
378 |
Const _ => Seq.map joinargs (copyargs uargs) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
379 |
| Free _ => Seq.map joinargs (copyargs uargs) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
380 |
| _ => Seq.empty) (*if Var, would be a loop!*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
381 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
382 |
(case uhead of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
383 |
Abs (a, T, body) => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
384 |
Seq.map (fn (body', ed') => (Abs (a, T, body'), ed')) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
385 |
(mc ((a, T) :: rbinder, (map (incr_boundvars 1) targs) @ [Bound 0], body, ed)) |
37636 | 386 |
| Var (w, _) => |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
387 |
(*a flex-flex dpair: make variable for t*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
388 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
389 |
val (env', newhd) = Envir.genvar (#1 w) (env, Ts ---> base); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
390 |
val tabs = Logic.combound (newhd, 0, length Ts); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
391 |
val tsub = list_comb (newhd, targs); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
392 |
in Seq.single (tabs, (env', (rbinder, tsub, u) :: dpairs)) end |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
393 |
| _ => matchfun (rev (make_projs (Ts, targs)))) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
394 |
end; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
395 |
in mc end; |
0 | 396 |
|
397 |
||
398 |
(*Call matchcopy to produce assignments to the variable in the dpair*) |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
399 |
fun MATCH context (env, (rbinder, t, u), dpairs) : (Envir.env * dpair list) Seq.seq = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
400 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
401 |
val (Var (vT as (v, T)), targs) = strip_comb t; |
52221 | 402 |
val Ts = Envir.binder_types env T; |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
403 |
fun new_dset (u', (env', dpairs')) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
404 |
(*if v was updated to s, must unify s with u' *) |
51700 | 405 |
(case Envir.lookup env' vT of |
406 |
NONE => (Envir.update (vT, types_abs (Ts, u')) env', dpairs') |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
407 |
| SOME s => (env', ([], s, types_abs (Ts, u')) :: dpairs')); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
408 |
in |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
409 |
Seq.map new_dset (matchcopy context (#1 v) (rbinder, targs, u, (env, dpairs))) |
0 | 410 |
end; |
411 |
||
412 |
||
413 |
||
414 |
(**** Flex-flex processing ****) |
|
415 |
||
19864 | 416 |
(*At end of unification, do flex-flex assignments like ?a -> ?f(?b) |
0 | 417 |
Attempts to update t with u, raising ASSIGN if impossible*) |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
418 |
fun ff_assign context (env, rbinder, t, u) : Envir.env = |
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
|
419 |
let val vT as (v, T) = get_eta_var (rbinder, 0, t) in |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
420 |
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
|
421 |
else |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
422 |
let val env = unify_types context (Envir.body_type env T, fastype env (rbinder, u)) env |
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
|
423 |
in Envir.vupdate (vT, Logic.rlist_abs (rbinder, u)) env end |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
424 |
end; |
0 | 425 |
|
426 |
||
37720
50a9e2fa4f6b
Unification (flexflex) bug fix; making "auto" deterministic
paulson
parents:
37637
diff
changeset
|
427 |
(*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
|
428 |
But if the only path is flexible, this is difficult; the code gives up! |
67725 | 429 |
In \<lambda>x y. ?a x \<equiv>\<^sup>? \<lambda>x y. ?b (?c y) should we instantiate ?b or ?c *) |
37720
50a9e2fa4f6b
Unification (flexflex) bug fix; making "auto" deterministic
paulson
parents:
37637
diff
changeset
|
430 |
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
|
431 |
|
50a9e2fa4f6b
Unification (flexflex) bug fix; making "auto" deterministic
paulson
parents:
37637
diff
changeset
|
432 |
|
0 | 433 |
(*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
|
434 |
type flarg = {t: term, T: typ, j: int}; |
0 | 435 |
|
436 |
(*Form the arguments into records for deletion/sorting.*) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
437 |
fun flexargs ([], [], []) = [] : flarg list |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
438 |
| 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
|
439 |
| flexargs _ = raise CHANGE_FAIL; |
41422
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset
|
440 |
(*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
|
441 |
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
|
442 |
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
|
443 |
*) |
0 | 444 |
|
651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEX-FLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset
|
445 |
(*Check whether the 'banned' bound var indices occur rigidly in t*) |
19864 | 446 |
fun rigid_bound (lev, banned) t = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
447 |
let val (head,args) = strip_comb t in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
448 |
(case head of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
449 |
Bound i => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
450 |
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
|
451 |
| Var _ => false (*no rigid occurrences here!*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
452 |
| Abs (_, _, u) => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
453 |
rigid_bound (lev + 1, banned) u orelse |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
454 |
exists (rigid_bound (lev, banned)) args |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
455 |
| _ => exists (rigid_bound (lev, banned)) args) |
0 | 456 |
end; |
457 |
||
651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEX-FLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset
|
458 |
(*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
|
459 |
fun change_bnos banned = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
460 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
461 |
fun change lev (Bound i) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
462 |
if i < lev then Bound i |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
463 |
else if member (op =) banned (i - lev) then |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
464 |
raise CHANGE_FAIL (**flexible occurrence: give up**) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
465 |
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
|
466 |
| 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
|
467 |
| change lev (t $ u) = change lev t $ change lev u |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
468 |
| change lev t = t; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
469 |
in change 0 end; |
0 | 470 |
|
471 |
(*Change indices, delete the argument if it contains a banned Bound*) |
|
48263 | 472 |
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
|
473 |
if rigid_bound (0, banned) t then args (*delete argument!*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
474 |
else {j = j, t = change_bnos banned t, T = T} :: args; |
0 | 475 |
|
476 |
||
477 |
(*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
|
478 |
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
|
479 |
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
|
480 |
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
|
481 |
| 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
|
482 |
|
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
|
483 |
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
|
484 |
| 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
|
485 |
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
|
486 |
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
|
487 |
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
|
488 |
| 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
|
489 |
end; |
0 | 490 |
|
491 |
(*Test whether the new term would be eta-equivalent to a variable -- |
|
492 |
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
|
493 |
fun decreasing n ([]: flarg list) = (n = 0) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
494 |
| decreasing n ({j, ...} :: args) = j = n - 1 andalso decreasing (n - 1) args; |
0 | 495 |
|
496 |
(*Delete banned indices in the term, simplifying it. |
|
497 |
Force an assignment, if possible, by sorting the arguments. |
|
498 |
Update its head; squash indices in arguments. *) |
|
499 |
fun clean_term banned (env,t) = |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
500 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
501 |
val (Var (v, T), ts) = strip_comb t; |
52221 | 502 |
val (Ts, U) = Envir.strip_type env T |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
503 |
and js = length ts - 1 downto 0; |
48263 | 504 |
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
|
505 |
val ts' = map #t args; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
506 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
507 |
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
|
508 |
else |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
509 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
510 |
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
|
511 |
val body = list_comb (v', map (Bound o #j) args); |
51700 | 512 |
val env2 = Envir.vupdate ((v, T), types_abs (Ts, body)) env'; |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
513 |
(*the vupdate affects ts' if they contain v*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
514 |
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
|
515 |
end; |
0 | 516 |
|
517 |
||
518 |
(*Add tpair if not trivial or already there. |
|
519 |
Should check for swapped pairs??*) |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
520 |
fun add_tpair (rbinder, (t0, u0), tpairs) : (term * term) list = |
19864 | 521 |
if t0 aconv u0 then tpairs |
0 | 522 |
else |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
523 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
524 |
val t = Logic.rlist_abs (rbinder, t0) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
525 |
and u = Logic.rlist_abs (rbinder, u0); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
526 |
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
|
527 |
in if exists same tpairs then tpairs else (t, u) :: tpairs end; |
0 | 528 |
|
529 |
||
530 |
(*Simplify both terms and check for assignments. |
|
531 |
Bound vars in the binder are "banned" unless used in both t AND u *) |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
532 |
fun clean_ffpair context ((rbinder, t, u), (env, tpairs)) = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
533 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
534 |
val loot = loose_bnos t and loou = loose_bnos u |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
535 |
fun add_index (j, (a, T)) (bnos, newbinder) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
536 |
if member (op =) loot j andalso member (op =) loou j |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
537 |
then (bnos, (a, T) :: newbinder) (*needed by both: keep*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
538 |
else (j :: bnos, newbinder); (*remove*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
539 |
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
|
540 |
val (env', t') = clean_term banned (env, t); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
541 |
val (env'',u') = clean_term banned (env',u); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
542 |
in |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
543 |
(ff_assign context (env'', rbin', t', u'), tpairs) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
544 |
handle ASSIGN => |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
545 |
(ff_assign context (env'', rbin', u', t'), tpairs) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
546 |
handle ASSIGN => (env'', add_tpair (rbin', (t', u'), tpairs)) |
0 | 547 |
end |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
548 |
handle CHANGE_FAIL => (env, add_tpair (rbinder, (t, u), tpairs)); |
0 | 549 |
|
550 |
||
551 |
(*IF the flex-flex dpair is an assignment THEN do it ELSE put in tpairs |
|
552 |
eliminates trivial tpairs like t=t, as well as repeated ones |
|
19864 | 553 |
trivial tpairs can easily escape SIMPL: ?A=t, ?A=?B, ?B=t gives t=t |
0 | 554 |
Resulting tpairs MAY NOT be in normal form: assignments may occur here.*) |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
555 |
fun add_ffpair context (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
|
556 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
557 |
val t = Envir.norm_term env t0 |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
558 |
and u = Envir.norm_term env u0; |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
559 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
560 |
(case (head_of t, head_of u) of |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
561 |
(Var (v, T), Var (w, U)) => (*Check for identical variables...*) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
562 |
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
|
563 |
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
|
564 |
else raise TERM ("add_ffpair: Var name confusion", [t, u]) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
565 |
else if Term_Ord.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*) |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
566 |
clean_ffpair context ((rbinder, u, t), (env, tpairs)) |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
567 |
else clean_ffpair context ((rbinder, t, u), (env, tpairs)) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
568 |
| _ => raise TERM ("add_ffpair: Vars expected", [t, u])) |
0 | 569 |
end; |
570 |
||
571 |
||
572 |
(*Print a tracing message + list of dpairs. |
|
67721 | 573 |
In t \<equiv> u print u first because it may be rigid or flexible -- |
0 | 574 |
t is always flexible.*) |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
575 |
fun print_dpairs context msg (env, dpairs) = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
576 |
if Context_Position.is_visible_generic context then |
52701
51dfdcd88e84
guard unify tracing via visible status of global theory;
wenzelm
parents:
52698
diff
changeset
|
577 |
let |
51dfdcd88e84
guard unify tracing via visible status of global theory;
wenzelm
parents:
52698
diff
changeset
|
578 |
fun pdp (rbinder, t, u) = |
51dfdcd88e84
guard unify tracing via visible status of global theory;
wenzelm
parents:
52698
diff
changeset
|
579 |
let |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
580 |
val ctxt = Context.proof_of context; |
52701
51dfdcd88e84
guard unify tracing via visible status of global theory;
wenzelm
parents:
52698
diff
changeset
|
581 |
fun termT t = |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
582 |
Syntax.pretty_term ctxt (Envir.norm_term env (Logic.rlist_abs (rbinder, t))); |
67725 | 583 |
val prt = Pretty.blk (0, [termT u, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, termT t]); |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
584 |
in tracing (Pretty.string_of prt) end; |
52701
51dfdcd88e84
guard unify tracing via visible status of global theory;
wenzelm
parents:
52698
diff
changeset
|
585 |
in tracing msg; List.app pdp dpairs end |
51dfdcd88e84
guard unify tracing via visible status of global theory;
wenzelm
parents:
52698
diff
changeset
|
586 |
else (); |
0 | 587 |
|
588 |
||
589 |
(*Unify the dpairs in the environment. |
|
19864 | 590 |
Returns flex-flex disagreement pairs NOT IN normal form. |
0 | 591 |
SIMPL may raise exception CANTUNIFY. *) |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
592 |
fun hounifiers (context, 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
|
593 |
let |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
594 |
val trace_bound = Config.get_generic context trace_bound; |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
595 |
val search_bound = Config.get_generic context search_bound; |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
596 |
val trace_simp = Config.get_generic context trace_simp; |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
597 |
fun add_unify tdepth ((env, dpairs), reseq) = |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
598 |
Seq.make (fn () => |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
599 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
600 |
val (env', flexflex, flexrigid) = |
52698 | 601 |
(if tdepth > trace_bound andalso trace_simp |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
602 |
then print_dpairs context "Enter SIMPL" (env, dpairs) else (); |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
603 |
SIMPL context (env, dpairs)); |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
604 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
605 |
(case flexrigid of |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
606 |
[] => SOME (fold_rev (add_ffpair context) flexflex (env', []), reseq) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
607 |
| dp :: frigid' => |
52698 | 608 |
if tdepth > search_bound then |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
609 |
(if Context_Position.is_visible_generic context |
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
52701
diff
changeset
|
610 |
then warning "Unification bound exceeded" else (); Seq.pull reseq) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
611 |
else |
52698 | 612 |
(if tdepth > trace_bound then |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
613 |
print_dpairs context "Enter MATCH" (env',flexrigid@flexflex) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
614 |
else (); |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
615 |
Seq.pull (Seq.it_right |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
616 |
(add_unify (tdepth + 1)) (MATCH context (env',dp, frigid'@flexflex), reseq)))) |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
617 |
end |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
618 |
handle CANTUNIFY => |
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
619 |
(if tdepth > trace_bound andalso Context_Position.is_visible_generic context |
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
52701
diff
changeset
|
620 |
then tracing "Failure node" |
52701
51dfdcd88e84
guard unify tracing via visible status of global theory;
wenzelm
parents:
52698
diff
changeset
|
621 |
else (); Seq.pull reseq)); |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
622 |
val dps = map (fn (t, u) => ([], t, u)) tus; |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset
|
623 |
in add_unify 1 ((env, dps), Seq.empty) end; |
0 | 624 |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
625 |
fun unifiers (params as (context, env, tus)) = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
626 |
Seq.cons (fold (Pattern.unify context) tus env, []) Seq.empty |
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset
|
627 |
handle Pattern.Unif => Seq.empty |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
628 |
| Pattern.Pattern => hounifiers params; |
0 | 629 |
|
630 |
||
631 |
(*For smash_flexflex1*) |
|
632 |
fun var_head_of (env,t) : indexname * typ = |
|
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
633 |
(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
|
634 |
Var (v, T) => (v, T) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
635 |
| _ => raise CANTUNIFY); (*not flexible, cannot use trivial substitution*) |
0 | 636 |
|
637 |
||
638 |
(*Eliminate a flex-flex pair by the trivial substitution, see Huet (1975) |
|
67721 | 639 |
Unifies ?f t1 ... rm with ?g u1 ... un by ?f -> \<lambda>x1...xm. ?a, ?g -> \<lambda>x1...xn. ?a |
640 |
Unfortunately, unifies ?f t u with ?g t u by ?f, ?g -> \<lambda>x y. ?a, |
|
19864 | 641 |
though just ?g->?f is a more general unifier. |
0 | 642 |
Unlike Huet (1975), does not smash together all variables of same type -- |
643 |
requires more work yet gives a less general unifier (fewer variables). |
|
67721 | 644 |
Handles ?f t1 ... rm with ?f u1 ... um to avoid multiple updates. *) |
48263 | 645 |
fun smash_flexflex1 (t, u) env : Envir.env = |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
646 |
let |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
647 |
val vT as (v, T) = var_head_of (env, t) |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
648 |
and wU as (w, U) = var_head_of (env, u); |
52221 | 649 |
val (env', var) = Envir.genvar (#1 v) (env, Envir.body_type env T); |
51700 | 650 |
val env'' = Envir.vupdate (wU, type_abs (env', U, var)) env'; |
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
651 |
in |
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset
|
652 |
if vT = wU then env'' (*the other update would be identical*) |
51700 | 653 |
else Envir.vupdate (vT, type_abs (env', T, var)) env'' |
0 | 654 |
end; |
655 |
||
656 |
||
657 |
(*Smash all flex-flexpairs. Should allow selection of pairs by a predicate?*) |
|
37636 | 658 |
fun smash_flexflex (env, tpairs) : Envir.env = |
48263 | 659 |
fold_rev smash_flexflex1 tpairs env; |
0 | 660 |
|
661 |
(*Returns unifiers with no remaining disagreement pairs*) |
|
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
662 |
fun smash_unifiers context tus env = |
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
56438
diff
changeset
|
663 |
Seq.map smash_flexflex (unifiers (context, env, tus)); |
0 | 664 |
|
665 |
end; |