author  wenzelm 
Fri, 24 May 2013 14:31:44 +0200  
changeset 52127  a40dfe02dd83 
parent 52126  5386150ed067 
child 52128  7f3549a316f4 
permissions  rwrr 
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 
HigherOrder 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 
52126  22 
val hounifiers: theory * Envir.env * ((term * term) list) > 
23 
(Envir.env * (term * term) list) Seq.seq 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

24 
val unifiers: theory * Envir.env * ((term * term) list) > 
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

25 
(Envir.env * (term * term) list) Seq.seq 
19864  26 
val smash_unifiers: theory > (term * term) list > Envir.env > Envir.env Seq.seq 
27 
val matchers: theory > (term * term) list > Envir.env Seq.seq 

28 
val matches_list: theory > term list > term list > bool 

16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

29 
end 
0  30 

19864  31 
structure Unify : UNIFY = 
0  32 
struct 
33 

34 
(*Unification options*) 

35 

24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset

36 
(*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

37 
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

38 
val trace_bound = Config.int trace_bound_raw; 
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset

39 

4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset

40 
(*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

41 
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

42 
val search_bound = Config.int search_bound_raw; 
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset

43 

4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset

44 
(*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

45 
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

46 
val trace_simp = Config.bool trace_simp_raw; 
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset

47 

4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset

48 
(*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

49 
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

50 
val trace_types = Config.bool trace_types_raw; 
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23178
diff
changeset

51 

0  52 

52126  53 
type binderlist = (string * typ) list; 
0  54 

55 
type dpair = binderlist * term * term; 

56 

32032  57 
fun body_type env = 
58 
let 

59 
val tyenv = Envir.type_env env; 

60 
fun bT (Type ("fun", [_, T])) = bT T 

61 
 bT (T as TVar v) = 

62 
(case Type.lookup tyenv v of 

63 
NONE => T 

64 
 SOME T' => bT T') 

65 
 bT T = T; 

66 
in bT end; 

0  67 

32032  68 
fun binder_types env = 
69 
let 

70 
val tyenv = Envir.type_env env; 

71 
fun bTs (Type ("fun", [T, U])) = T :: bTs U 

37636  72 
 bTs (TVar v) = 
32032  73 
(case Type.lookup tyenv v of 
74 
NONE => [] 

75 
 SOME T' => bTs T') 

76 
 bTs _ = []; 

77 
in bTs end; 

0  78 

79 
fun strip_type env T = (binder_types env T, body_type env T); 

80 

12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
8406
diff
changeset

81 
fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t; 
0  82 

83 

32032  84 
(* eta normal form *) 
85 

86 
fun eta_norm env = 

87 
let 

88 
val tyenv = Envir.type_env env; 

89 
fun etif (Type ("fun", [T, U]), t) = 

90 
Abs ("", T, etif (U, incr_boundvars 1 t $ Bound 0)) 

91 
 etif (TVar v, t) = 

92 
(case Type.lookup tyenv v of 

93 
NONE => t 

94 
 SOME T => etif (T, t)) 

95 
 etif (_, t) = t; 

96 
fun eta_nm (rbinder, Abs (a, T, body)) = 

97 
Abs (a, T, eta_nm ((a, T) :: rbinder, body)) 

98 
 eta_nm (rbinder, t) = etif (fastype env (rbinder, t), t); 

0  99 
in eta_nm end; 
100 

101 

102 
(*OCCURS CHECK 

19864  103 
Does the uvar occur in the term t? 
0  104 
two forms of search, for whether there is a rigid path to the current term. 
105 
"seen" is list of variables passed thru, is a memo variable for sharing. 

15797  106 
This version searches for nonrigid occurrence, returns true if found. 
107 
Since terms may contain variables with same name and different types, 

108 
the occurs check must ignore the types of variables. This avoids 

109 
that ?x::?'a is unified with f(?x::T), which may lead to a cyclic 

110 
substitution when ?'a is instantiated with T later. *) 

37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

111 
fun occurs_terms (seen: indexname list Unsynchronized.ref, 
19864  112 
env: Envir.env, v: indexname, ts: term list): bool = 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

113 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

114 
fun occurs [] = false 
37636  115 
 occurs (t :: ts) = occur t orelse occurs ts 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

116 
and occur (Const _) = false 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

117 
 occur (Bound _) = false 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

118 
 occur (Free _) = false 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

119 
 occur (Var (w, T)) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

120 
if member (op =) (!seen) w then false 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

121 
else if Term.eq_ix (v, w) then true 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

122 
(*no need to lookup: v has no assignment*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

123 
else 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

124 
(seen := w :: !seen; 
51700  125 
case Envir.lookup env (w, T) of 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

126 
NONE => false 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

127 
 SOME t => occur t) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

128 
 occur (Abs (_, _, body)) = occur body 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

129 
 occur (f $ t) = occur t orelse occur f; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

130 
in occurs ts end; 
0  131 

132 

52126  133 
(* f a1 ... an > f using the assignments*) 
134 
fun head_of_in env t = 

37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

135 
(case t of 
52126  136 
f $ _ => head_of_in env f 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

137 
 Var vT => 
51700  138 
(case Envir.lookup env vT of 
52126  139 
SOME u => head_of_in env u 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

140 
 NONE => t) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

141 
 _ => t); 
0  142 

143 

144 
datatype occ = NoOcc  Nonrigid  Rigid; 

145 

146 
(* Rigid occur check 

147 
Returns Rigid if it finds a rigid occurrence of the variable, 

148 
Nonrigid if it finds a nonrigid path to the variable. 

149 
NoOcc otherwise. 

150 
Continues searching for a rigid occurrence even if it finds a nonrigid one. 

151 

152 
Condition for detecting nonunifable terms: [ section 5.3 of Huet (1975) ] 

153 
a rigid path to the variable, appearing with no arguments. 

154 
Here completeness is sacrificed in order to reduce danger of divergence: 

155 
reject ALL rigid paths to the variable. 

19864  156 
Could check for rigid paths to bound variables that are out of scope. 
0  157 
Not necessary because the assignment test looks at variable's ENTIRE rbinder. 
158 

159 
Treatment of head(arg1,...,argn): 

160 
If head is a variable then no rigid path, switch to nonrigid search 

19864  161 
for arg1,...,argn. 
162 
If head is an abstraction then possibly no rigid path (head could be a 

0  163 
constant function) so again use nonrigid search. Happens only if 
19864  164 
term is not in normal form. 
0  165 

166 
Warning: finds a rigid occurrence of ?f in ?f(t). 

167 
Should NOT be called in this case: there is a flexflex unifier 

168 
*) 

37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

169 
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

170 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

171 
fun nonrigid t = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

172 
if occurs_terms (seen, env, v, [t]) then Nonrigid 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

173 
else NoOcc 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

174 
fun occurs [] = NoOcc 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

175 
 occurs (t :: ts) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

176 
(case occur t of 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

177 
Rigid => Rigid 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

178 
 oc => (case occurs ts of NoOcc => oc  oc2 => oc2)) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

179 
and occomb (f $ t) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

180 
(case occur t of 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

181 
Rigid => Rigid 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

182 
 oc => (case occomb f of NoOcc => oc  oc2 => oc2)) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

183 
 occomb t = occur t 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

184 
and occur (Const _) = NoOcc 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

185 
 occur (Bound _) = NoOcc 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

186 
 occur (Free _) = NoOcc 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

187 
 occur (Var (w, T)) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

188 
if member (op =) (!seen) w then NoOcc 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

189 
else if Term.eq_ix (v, w) then Rigid 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

190 
else 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

191 
(seen := w :: !seen; 
51700  192 
case Envir.lookup env (w, T) of 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

193 
NONE => NoOcc 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

194 
 SOME t => occur t) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

195 
 occur (Abs (_, _, body)) = occur body 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

196 
 occur (t as f $ _) = (*switch to nonrigid search?*) 
52126  197 
(case head_of_in env f of 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

198 
Var (w,_) => (*w is not assigned*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

199 
if Term.eq_ix (v, w) then Rigid 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

200 
else nonrigid t 
37636  201 
 Abs _ => nonrigid t (*not in normal form*) 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

202 
 _ => occomb t) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

203 
in occur t end; 
0  204 

205 

19864  206 
exception CANTUNIFY; (*Signals nonunifiability. Does not signal errors!*) 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

207 
exception ASSIGN; (*Raised if not an assignment*) 
0  208 

209 

52127
a40dfe02dd83
reuse Pattern.unify_types, including its trace_unify_fail option;
wenzelm
parents:
52126
diff
changeset

210 
fun unify_types thy TU env = 
a40dfe02dd83
reuse Pattern.unify_types, including its trace_unify_fail option;
wenzelm
parents:
52126
diff
changeset

211 
Pattern.unify_types thy TU env handle Pattern.Unif => raise CANTUNIFY; 
0  212 

52126  213 
fun test_unify_types thy (T, U) env = 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

214 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

215 
val str_of = Syntax.string_of_typ_global thy; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

216 
fun warn () = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T); 
52126  217 
val env' = unify_types thy (T, U) env; 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

218 
in if is_TVar T orelse is_TVar U then warn () else (); env' end; 
0  219 

220 
(*Is the term etaconvertible to a single variable with the given rbinder? 

221 
Examples: ?a ?f(B.0) ?g(B.1,B.0) 

222 
Result is var a for use in SIMPL. *) 

37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

223 
fun get_eta_var ([], _, Var vT) = vT 
0  224 
 get_eta_var (_::rbinder, n, f $ Bound i) = 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

225 
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

226 
else raise ASSIGN 
0  227 
 get_eta_var _ = raise ASSIGN; 
228 

229 

230 
(*Solve v=u by assignment  "fixedpoint" to Huet  if v not in u. 

231 
If v occurs rigidly then nonunifiable. 

232 
If v occurs nonrigidly then must use full algorithm. *) 

52126  233 
fun assignment thy (rbinder, t, u) env = 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

234 
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

235 
(case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

236 
NoOcc => 
52126  237 
let val env = unify_types thy (body_type env T, fastype env (rbinder, u)) env 
51700  238 
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

239 
 Nonrigid => raise ASSIGN 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

240 
 Rigid => raise CANTUNIFY) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

241 
end; 
0  242 

243 

244 
(*Extends an rbinder with a new disagreement pair, if both are abstractions. 

245 
Tries to unify types of the bound variables! 

246 
Checks that binders have same length, since terms should be etanormal; 

247 
if not, raises TERM, probably indicating type mismatch. 

19864  248 
Uses variable a (unless the null string) to preserve user's naming.*) 
52126  249 
fun new_dpair thy (rbinder, Abs (a, T, body1), Abs (b, U, body2)) env = 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

250 
let 
52126  251 
val env' = unify_types thy (T, U) env; 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

252 
val c = if a = "" then b else a; 
52126  253 
in new_dpair thy ((c,T) :: rbinder, body1, body2) env' end 
254 
 new_dpair _ (_, Abs _, _) _ = raise TERM ("new_dpair", []) 

255 
 new_dpair _ (_, _, Abs _) _ = raise TERM ("new_dpair", []) 

256 
 new_dpair _ (rbinder, t1, t2) env = ((rbinder, t1, t2), env); 

0  257 

258 

37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

259 
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

260 
new_dpair thy (rbinder, 
19864  261 
eta_norm env (rbinder, Envir.head_norm env t), 
52126  262 
eta_norm env (rbinder, Envir.head_norm env u)) env; 
0  263 

264 

265 

266 
(*flexflex: the flexflex pairs, flexrigid: the flexrigid pairs 

267 
Does not perform assignments for flexflex pairs: 

646  268 
may create nonrigid paths, which prevent other assignments. 
269 
Does not even identify Vars in dpairs such as ?a =?= ?b; an attempt to 

270 
do so caused numerous problems with no compensating advantage. 

271 
*) 

48263  272 
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

273 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

274 
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

275 
fun SIMRANDS (f $ t, g $ u, env) = 
48263  276 
SIMPL0 thy (rbinder, t, u) (SIMRANDS (f, g, env)) 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

277 
 SIMRANDS (t as _$_, _, _) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

278 
raise TERM ("SIMPL: operands mismatch", [t, u]) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

279 
 SIMRANDS (t, u as _ $ _, _) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

280 
raise TERM ("SIMPL: operands mismatch", [t, u]) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

281 
 SIMRANDS (_, _, env) = (env, flexflex, flexrigid); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

282 
in 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

283 
(case (head_of t, head_of u) of 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

284 
(Var (_, T), Var (_, U)) => 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

285 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

286 
val T' = body_type env T and U' = body_type env U; 
52126  287 
val env = unify_types thy (T', U') env; 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

288 
in (env, dp :: flexflex, flexrigid) end 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

289 
 (Var _, _) => 
52126  290 
((assignment thy (rbinder,t,u) env, flexflex, flexrigid) 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

291 
handle ASSIGN => (env, flexflex, dp :: flexrigid)) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

292 
 (_, Var _) => 
52126  293 
((assignment thy (rbinder, u, t) env, flexflex, flexrigid) 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

294 
handle ASSIGN => (env, flexflex, (rbinder, u, t) :: flexrigid)) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

295 
 (Const (a, T), Const (b, U)) => 
52126  296 
if a = b then SIMRANDS (t, u, unify_types thy (T, U) env) 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

297 
else raise CANTUNIFY 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

298 
 (Bound i, Bound j) => 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

299 
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

300 
 (Free (a, T), Free (b, U)) => 
52126  301 
if a = b then SIMRANDS (t, u, unify_types thy (T, U) env) 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

302 
else raise CANTUNIFY 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

303 
 _ => raise CANTUNIFY) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

304 
end; 
0  305 

306 

307 
(* changed(env,t) checks whether the head of t is a variable assigned in env*) 

52126  308 
fun changed env (f $ _) = changed env f 
309 
 changed env (Var v) = (case Envir.lookup env v of NONE => false  _ => true) 

310 
 changed _ _ = false; 

0  311 

312 

313 
(*Recursion needed if any of the 'head variables' have been updated 

314 
Clever would be to redo just the affected dpairs*) 

16664  315 
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

316 
let 
48263  317 
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

318 
val dps = flexrigid @ flexflex; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

319 
in 
52126  320 
if exists (fn (_, t, u) => changed env' t orelse changed env' u) dps 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

321 
then SIMPL thy (env', dps) else all 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

322 
end; 
0  323 

324 

19864  325 
(*Makes the terms E1,...,Em, where Ts = [T...Tm]. 
0  326 
Each Ei is ?Gi(B.(n1),...,B.0), and has type Ti 
327 
The B.j are bound vars of binder. 

19864  328 
The terms are not made in etanormalform, SIMPL does that later. 
0  329 
If done here, etaexpansion must be recursive in the arguments! *) 
37636  330 
fun make_args _ (_, env, []) = (env, []) (*frequent case*) 
0  331 
 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

332 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

333 
fun funtype T = binder > T; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

334 
val (env', vars) = Envir.genvars name (env, map funtype Ts); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

335 
in (env', map (fn var => Logic.combound (var, 0, length binder)) vars) end; 
0  336 

337 

46219
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
42279
diff
changeset

338 
(*Abstraction over a list of types*) 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

339 
fun types_abs ([], u) = u 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

340 
 types_abs (T :: Ts, u) = Abs ("", T, types_abs (Ts, u)); 
0  341 

342 
(*Abstraction over the binder of a type*) 

37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

343 
fun type_abs (env, T, t) = types_abs (binder_types env T, t); 
0  344 

345 

346 
(*MATCH taking "big steps". 

347 
Copies u into the Var v, using projection on targs or imitation. 

348 
A projection is allowed unless SIMPL raises an exception. 

349 
Allocates new variables in projection on a higherorder argument, 

350 
or if u is a variable (flexflex dpair). 

351 
Returns long sequence of every way of copying u, for backtracking 

352 
For example, projection in ?b'(?a) may be wrong if other dpairs constrain ?a. 

19864  353 
The order for trying projections is crucial in ?b'(?a) 
0  354 
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

355 
fun matchcopy thy vname = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

356 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

357 
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

358 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

359 
val trace_tps = Config.get_global thy trace_types; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

360 
(*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

361 
fun copycons uarg (uargs, (env, dpairs)) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

362 
Seq.map (fn (uarg', ed') => (uarg' :: uargs, ed')) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

363 
(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

364 
(env, dpairs))); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

365 
(*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

366 
fun copyargs [] = Seq.cons ([], ed) Seq.empty 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

367 
 copyargs (uarg :: uargs) = Seq.maps (copycons uarg) (copyargs uargs); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

368 
val (uhead, uargs) = strip_comb u; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

369 
val base = body_type env (fastype env (rbinder, uhead)); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

370 
fun joinargs (uargs', ed') = (list_comb (uhead, uargs'), ed'); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

371 
(*attempt projection on argument with given typ*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

372 
val Ts = map (curry (fastype env) rbinder) targs; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

373 
fun projenv (head, (Us, bary), targ, tail) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

374 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

375 
val env = 
52126  376 
if trace_tps then test_unify_types thy (base, bary) env 
377 
else unify_types thy (base, bary) env 

37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

378 
in 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

379 
Seq.make (fn () => 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

380 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

381 
val (env', args) = make_args vname (Ts, env, Us); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

382 
(*higherorder projection: plug in targs for bound vars*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

383 
fun plugin arg = list_comb (head_of arg, targs); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

384 
val dp = (rbinder, list_comb (targ, map plugin args), u); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

385 
val (env2, frigid, fflex) = SIMPL thy (env', dp :: dpairs); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

386 
(*may raise exception CANTUNIFY*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

387 
in 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

388 
SOME ((list_comb (head, args), (env2, frigid @ fflex)), tail) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

389 
end handle CANTUNIFY => Seq.pull tail) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

390 
end handle CANTUNIFY => tail; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

391 
(*make a list of projections*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

392 
fun make_projs (T::Ts, targ::targs) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

393 
(Bound(length Ts), T, targ) :: make_projs (Ts,targs) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

394 
 make_projs ([],[]) = [] 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

395 
 make_projs _ = raise TERM ("make_projs", u::targs); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

396 
(*try projections and imitation*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

397 
fun matchfun ((bvar,T,targ)::projs) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

398 
(projenv(bvar, strip_type env T, targ, matchfun projs)) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

399 
 matchfun [] = (*imitation last of all*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

400 
(case uhead of 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

401 
Const _ => Seq.map joinargs (copyargs uargs) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

402 
 Free _ => Seq.map joinargs (copyargs uargs) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

403 
 _ => Seq.empty) (*if Var, would be a loop!*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

404 
in 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

405 
(case uhead of 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

406 
Abs (a, T, body) => 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

407 
Seq.map (fn (body', ed') => (Abs (a, T, body'), ed')) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

408 
(mc ((a, T) :: rbinder, (map (incr_boundvars 1) targs) @ [Bound 0], body, ed)) 
37636  409 
 Var (w, _) => 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

410 
(*a flexflex dpair: make variable for t*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

411 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

412 
val (env', newhd) = Envir.genvar (#1 w) (env, Ts > base); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

413 
val tabs = Logic.combound (newhd, 0, length Ts); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

414 
val tsub = list_comb (newhd, targs); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

415 
in Seq.single (tabs, (env', (rbinder, tsub, u) :: dpairs)) end 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

416 
 _ => matchfun (rev (make_projs (Ts, targs)))) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

417 
end; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

418 
in mc end; 
0  419 

420 

421 
(*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

422 
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

423 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

424 
val (Var (vT as (v, T)), targs) = strip_comb t; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

425 
val Ts = binder_types env T; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

426 
fun new_dset (u', (env', dpairs')) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

427 
(*if v was updated to s, must unify s with u' *) 
51700  428 
(case Envir.lookup env' vT of 
429 
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

430 
 SOME s => (env', ([], s, types_abs (Ts, u')) :: dpairs')); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

431 
in 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

432 
Seq.map new_dset (matchcopy thy (#1 v) (rbinder, targs, u, (env, dpairs))) 
0  433 
end; 
434 

435 

436 

437 
(**** Flexflex processing ****) 

438 

19864  439 
(*At end of unification, do flexflex assignments like ?a > ?f(?b) 
0  440 
Attempts to update t with u, raising ASSIGN if impossible*) 
19864  441 
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

442 
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

443 
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

444 
else 
52126  445 
let val env = unify_types thy (body_type env T, fastype env (rbinder, u)) env 
51700  446 
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

447 
end; 
0  448 

449 

37720
50a9e2fa4f6b
Unification (flexflex) bug fix; making "auto" deterministic
paulson
parents:
37637
diff
changeset

450 
(*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

451 
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

452 
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

453 
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

454 

50a9e2fa4f6b
Unification (flexflex) bug fix; making "auto" deterministic
paulson
parents:
37637
diff
changeset

455 

0  456 
(*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

457 
type flarg = {t: term, T: typ, j: int}; 
0  458 

459 
(*Form the arguments into records for deletion/sorting.*) 

37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

460 
fun flexargs ([], [], []) = [] : flarg list 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

461 
 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

462 
 flexargs _ = raise CHANGE_FAIL; 
41422
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset

463 
(*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

464 
arguments (remember, this code assumes that terms are fully etaexpanded). This situation 
37720
50a9e2fa4f6b
Unification (flexflex) bug fix; making "auto" deterministic
paulson
parents:
37637
diff
changeset

465 
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

466 
*) 
0  467 

651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

468 
(*Check whether the 'banned' bound var indices occur rigidly in t*) 
19864  469 
fun rigid_bound (lev, banned) t = 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

470 
let val (head,args) = strip_comb t in 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

471 
(case head of 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

472 
Bound i => 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

473 
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

474 
 Var _ => false (*no rigid occurrences here!*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

475 
 Abs (_, _, u) => 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

476 
rigid_bound (lev + 1, banned) u orelse 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

477 
exists (rigid_bound (lev, banned)) args 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

478 
 _ => exists (rigid_bound (lev, banned)) args) 
0  479 
end; 
480 

651
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

481 
(*Squash down indices at level >=lev to delete the banned from a term.*) 
4b0455fbcc49
Pure/Unify/IMPROVING "CLEANING" OF FLEXFLEX PAIRS: Old code would refuse
lcp
parents:
646
diff
changeset

482 
fun change_bnos banned = 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

483 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

484 
fun change lev (Bound i) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

485 
if i < lev then Bound i 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

486 
else if member (op =) banned (i  lev) then 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

487 
raise CHANGE_FAIL (**flexible occurrence: give up**) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

488 
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

489 
 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

490 
 change lev (t $ u) = change lev t $ change lev u 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

491 
 change lev t = t; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

492 
in change 0 end; 
0  493 

494 
(*Change indices, delete the argument if it contains a banned Bound*) 

48263  495 
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

496 
if rigid_bound (0, banned) t then args (*delete argument!*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

497 
else {j = j, t = change_bnos banned t, T = T} :: args; 
0  498 

499 

500 
(*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 quasiorder and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset

501 
create etaterms 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 quasiorder and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset

502 
local 
a0d8abca8d7a
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation  NB: make_ord arg_less was not a quasiorder and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset

503 
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 quasiorder and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset

504 
 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 quasiorder and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset

505 

a0d8abca8d7a
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation  NB: make_ord arg_less was not a quasiorder and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset

506 
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 quasiorder and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset

507 
 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 quasiorder and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset

508 
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 quasiorder and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset

509 
in 
a0d8abca8d7a
back to naive insertion sort before 1997 to accommodate peculiar less_arg relation  NB: make_ord arg_less was not a quasiorder and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset

510 
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 quasiorder and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset

511 
 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 quasiorder and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
wenzelm
parents:
46219
diff
changeset

512 
end; 
0  513 

514 
(*Test whether the new term would be etaequivalent to a variable  

515 
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

516 
fun decreasing n ([]: flarg list) = (n = 0) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

517 
 decreasing n ({j, ...} :: args) = j = n  1 andalso decreasing (n  1) args; 
0  518 

519 
(*Delete banned indices in the term, simplifying it. 

520 
Force an assignment, if possible, by sorting the arguments. 

521 
Update its head; squash indices in arguments. *) 

522 
fun clean_term banned (env,t) = 

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 (Var (v, T), ts) = strip_comb t; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

525 
val (Ts, U) = strip_type env T 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

526 
and js = length ts  1 downto 0; 
48263  527 
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

528 
val ts' = map #t args; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

529 
in 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

530 
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

531 
else 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

532 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

533 
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

534 
val body = list_comb (v', map (Bound o #j) args); 
51700  535 
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

536 
(*the vupdate affects ts' if they contain v*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

537 
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

538 
end; 
0  539 

540 

541 
(*Add tpair if not trivial or already there. 

542 
Should check for swapped pairs??*) 

37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

543 
fun add_tpair (rbinder, (t0, u0), tpairs) : (term * term) list = 
19864  544 
if t0 aconv u0 then tpairs 
0  545 
else 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

546 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

547 
val t = Logic.rlist_abs (rbinder, t0) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

548 
and u = Logic.rlist_abs (rbinder, u0); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

549 
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

550 
in if exists same tpairs then tpairs else (t, u) :: tpairs end; 
0  551 

552 

553 
(*Simplify both terms and check for assignments. 

554 
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

555 
fun clean_ffpair thy ((rbinder, t, u), (env, tpairs)) = 
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 loot = loose_bnos t and loou = loose_bnos u 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

558 
fun add_index (j, (a, T)) (bnos, newbinder) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

559 
if member (op =) loot j andalso member (op =) loou j 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

560 
then (bnos, (a, T) :: newbinder) (*needed by both: keep*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

561 
else (j :: bnos, newbinder); (*remove*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

562 
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

563 
val (env', t') = clean_term banned (env, t); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

564 
val (env'',u') = clean_term banned (env',u); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

565 
in 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

566 
(ff_assign thy (env'', rbin', t', u'), tpairs) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

567 
handle ASSIGN => 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

568 
(ff_assign thy (env'', rbin', u', t'), tpairs) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

569 
handle ASSIGN => (env'', add_tpair (rbin', (t', u'), tpairs)) 
0  570 
end 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

571 
handle CHANGE_FAIL => (env, add_tpair (rbinder, (t, u), tpairs)); 
0  572 

573 

574 
(*IF the flexflex dpair is an assignment THEN do it ELSE put in tpairs 

575 
eliminates trivial tpairs like t=t, as well as repeated ones 

19864  576 
trivial tpairs can easily escape SIMPL: ?A=t, ?A=?B, ?B=t gives t=t 
0  577 
Resulting tpairs MAY NOT be in normal form: assignments may occur here.*) 
48263  578 
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

579 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

580 
val t = Envir.norm_term env t0 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

581 
and u = Envir.norm_term env u0; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

582 
in 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

583 
(case (head_of t, head_of u) of 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

584 
(Var (v, T), Var (w, U)) => (*Check for identical variables...*) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

585 
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

586 
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

587 
else raise TERM ("add_ffpair: Var name confusion", [t, u]) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

588 
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

589 
clean_ffpair thy ((rbinder, u, t), (env, tpairs)) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

590 
else clean_ffpair thy ((rbinder, t, u), (env, tpairs)) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

591 
 _ => raise TERM ("add_ffpair: Vars expected", [t, u])) 
0  592 
end; 
593 

594 

595 
(*Print a tracing message + list of dpairs. 

596 
In t==u print u first because it may be rigid or flexible  

597 
t is always flexible.*) 

37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

598 
fun print_dpairs thy msg (env, dpairs) = 
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 
fun pdp (rbinder, t, u) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

601 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

602 
fun termT t = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

603 
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

604 
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

605 
in tracing (Pretty.string_of (Pretty.blk (0, bsymbs))) end; 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

606 
in tracing msg; List.app pdp dpairs end; 
0  607 

608 

609 
(*Unify the dpairs in the environment. 

19864  610 
Returns flexflex disagreement pairs NOT IN normal form. 
0  611 
SIMPL may raise exception CANTUNIFY. *) 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

612 
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

613 
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

614 
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

615 
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

616 
val trace_smp = Config.get_global thy trace_simp; 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

617 
fun add_unify tdepth ((env, dpairs), reseq) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

618 
Seq.make (fn () => 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

619 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

620 
val (env', flexflex, flexrigid) = 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

621 
(if tdepth > trace_bnd andalso trace_smp 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

622 
then print_dpairs thy "Enter SIMPL" (env, dpairs) else (); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

623 
SIMPL thy (env, dpairs)); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

624 
in 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

625 
(case flexrigid of 
48263  626 
[] => SOME (fold_rev (add_ffpair thy) flexflex (env', []), reseq) 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

627 
 dp :: frigid' => 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

628 
if tdepth > search_bnd then 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

629 
(warning "Unification bound exceeded"; Seq.pull reseq) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

630 
else 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

631 
(if tdepth > trace_bnd then 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

632 
print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

633 
else (); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

634 
Seq.pull (Seq.it_right 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

635 
(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

636 
end 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

637 
handle CANTUNIFY => 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

638 
(if tdepth > trace_bnd then tracing"Failure node" else (); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

639 
Seq.pull reseq)); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

640 
val dps = map (fn (t, u) => ([], t, u)) tus; 
16425
2427be27cc60
accomodate identification of type Sign.sg and theory;
wenzelm
parents:
15797
diff
changeset

641 
in add_unify 1 ((env, dps), Seq.empty) end; 
0  642 

18184  643 
fun unifiers (params as (thy, env, tus)) = 
19473  644 
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

645 
handle Pattern.Unif => Seq.empty 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

646 
 Pattern.Pattern => hounifiers params; 
0  647 

648 

649 
(*For smash_flexflex1*) 

650 
fun var_head_of (env,t) : indexname * typ = 

37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

651 
(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

652 
Var (v, T) => (v, T) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

653 
 _ => raise CANTUNIFY); (*not flexible, cannot use trivial substitution*) 
0  654 

655 

656 
(*Eliminate a flexflex pair by the trivial substitution, see Huet (1975) 

657 
Unifies ?f(t1...rm) with ?g(u1...un) by ?f > %x1...xm.?a, ?g > %x1...xn.?a 

19864  658 
Unfortunately, unifies ?f(t,u) with ?g(t,u) by ?f, ?g > %(x,y)?a, 
659 
though just ?g>?f is a more general unifier. 

0  660 
Unlike Huet (1975), does not smash together all variables of same type  
661 
requires more work yet gives a less general unifier (fewer variables). 

662 
Handles ?f(t1...rm) with ?f(u1...um) to avoid multiple updates. *) 

48263  663 
fun smash_flexflex1 (t, u) env : Envir.env = 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

664 
let 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

665 
val vT as (v, T) = var_head_of (env, t) 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

666 
and wU as (w, U) = var_head_of (env, u); 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

667 
val (env', var) = Envir.genvar (#1 v) (env, body_type env T); 
51700  668 
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

669 
in 
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

670 
if vT = wU then env'' (*the other update would be identical*) 
51700  671 
else Envir.vupdate (vT, type_abs (env', T, var)) env'' 
0  672 
end; 
673 

674 

675 
(*Smash all flexflexpairs. Should allow selection of pairs by a predicate?*) 

37636  676 
fun smash_flexflex (env, tpairs) : Envir.env = 
48263  677 
fold_rev smash_flexflex1 tpairs env; 
0  678 

679 
(*Returns unifiers with no remaining disagreement pairs*) 

19864  680 
fun smash_unifiers thy tus env = 
37635
484efa650907
recovered some indentation from the depths of time;
wenzelm
parents:
36787
diff
changeset

681 
Seq.map smash_flexflex (unifiers (thy, env, tus)); 
0  682 

19864  683 

684 
(*Pattern matching*) 

32032  685 
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

686 
let val (tyenv', tenv') = fold (Pattern.first_order_match thy) pairs (tyenv, tenv) 
32032  687 
in Seq.single (Envir.Envir {maxidx = maxidx, tenv = tenv', tyenv = tyenv'}) end 
19864  688 
handle Pattern.MATCH => Seq.empty; 
689 

41422
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset

690 
(*General matching  keep variables disjoint*) 
19864  691 
fun matchers _ [] = Seq.single (Envir.empty ~1) 
692 
 matchers thy pairs = 

693 
let 

694 
val maxidx = fold (Term.maxidx_term o #2) pairs ~1; 

695 
val offset = maxidx + 1; 

696 
val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs; 

697 
val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1; 

698 

699 
val pat_tvars = fold (Term.add_tvars o #1) pairs' []; 

700 
val pat_vars = fold (Term.add_vars o #1) pairs' []; 

701 

702 
val decr_indexesT = 

703 
Term.map_atyps (fn T as TVar ((x, i), S) => 

704 
if i > maxidx then TVar ((x, i  offset), S) else T  T => T); 

705 
val decr_indexes = 

20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20098
diff
changeset

706 
Term.map_types decr_indexesT #> 
19864  707 
Term.map_aterms (fn t as Var ((x, i), T) => 
708 
if i > maxidx then Var ((x, i  offset), T) else t  t => t); 

709 

32032  710 
fun norm_tvar env ((x, i), S) = 
41422
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset

711 
let 
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset

712 
val tyenv = Envir.type_env env; 
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset

713 
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

714 
in 
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset

715 
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

716 
else SOME ((x, i  offset), (S, decr_indexesT T')) 
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset

717 
end; 
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset

718 

32032  719 
fun norm_var env ((x, i), T) = 
19864  720 
let 
32032  721 
val tyenv = Envir.type_env env; 
19864  722 
val T' = Envir.norm_type tyenv T; 
723 
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

724 
in 
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset

725 
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

726 
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

727 
end; 
19864  728 

729 
fun result env = 

19876  730 
if Envir.above env maxidx then (* FIXME proper handling of generated vars!? *) 
19864  731 
SOME (Envir.Envir {maxidx = maxidx, 
41422
8a765db7e0f8
uniform treatment of type vs. term environment (cf. b654fa27fbc4);
wenzelm
parents:
39997
diff
changeset

732 
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

733 
tenv = Vartab.make (map_filter (norm_var env) pat_vars)}) 
19866  734 
else NONE; 
19864  735 

736 
val empty = Envir.empty maxidx'; 

737 
in 

19876  738 
Seq.append 
19920
8257e52164a1
matchers: try pattern_matchers only *after* general matching (The
wenzelm
parents:
19876
diff
changeset

739 
(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

740 
(first_order_matchers thy pairs empty) 
19864  741 
end; 
742 

743 
fun matches_list thy ps os = 

744 
length ps = length os andalso is_some (Seq.pull (matchers thy (ps ~~ os))); 

745 

0  746 
end; 