1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
28 exception UnificationFailure of string;;
29 exception Uncertain of string;;
30 exception AssertFailure of string;;
32 let debug_print = prerr_endline
34 let type_of_aux' metasenv subst context term =
36 CicMetaSubst.type_of_aux' metasenv subst context term
38 | CicMetaSubst.MetaSubstFailure msg ->
41 "Type checking error: %s in context\n%s\nand metasenv\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
42 (CicMetaSubst.ppterm subst term)
43 (CicMetaSubst.ppcontext subst context)
44 (CicMetaSubst.ppmetasenv metasenv subst) msg)))
46 let rec beta_expand test_equality_only metasenv subst context t arg =
47 let module S = CicSubstitution in
49 let rec aux metasenv subst n context t' =
52 fo_unif_subst test_equality_only subst context metasenv
53 (CicSubstitution.lift n arg) t'
55 subst,metasenv,C.Rel (1 + n)
58 | UnificationFailure _ ->
60 | C.Rel m -> subst,metasenv, if m <= n then C.Rel m else C.Rel (m+1)
61 | C.Var (uri,exp_named_subst) ->
62 let subst,metasenv,exp_named_subst' =
63 aux_exp_named_subst metasenv subst n context exp_named_subst
65 subst,metasenv,C.Var (uri,exp_named_subst')
68 let (_, t') = CicMetaSubst.lookup_subst i subst in
69 aux metasenv subst n context (CicSubstitution.lift_meta l t')
70 with CicMetaSubst.SubstNotFound _ ->
71 let (subst, metasenv, context, local_context) =
73 (fun (subst, metasenv, context, local_context) t ->
75 | None -> (subst, metasenv, context, None :: local_context)
77 let (subst, metasenv, t) =
78 aux metasenv subst n context t
80 (subst, metasenv, context, Some t :: local_context))
81 (subst, metasenv, context, []) l
83 (subst, metasenv, C.Meta (i, local_context)))
85 | C.Implicit _ as t -> subst,metasenv,t
87 let subst,metasenv,te' = aux metasenv subst n context te in
88 let subst,metasenv,ty' = aux metasenv subst n context ty in
89 subst,metasenv,C.Cast (te', ty')
91 let subst,metasenv,s' = aux metasenv subst n context s in
92 let subst,metasenv,t' =
93 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
95 subst,metasenv,C.Prod (nn, s', t')
96 | C.Lambda (nn,s,t) ->
97 let subst,metasenv,s' = aux metasenv subst n context s in
98 let subst,metasenv,t' =
99 aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
101 subst,metasenv,C.Lambda (nn, s', t')
102 | C.LetIn (nn,s,t) ->
103 let subst,metasenv,s' = aux metasenv subst n context s in
104 let subst,metasenv,t' =
105 aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
107 subst,metasenv,C.LetIn (nn, s', t')
109 let subst,metasenv,revl' =
111 (fun (subst,metasenv,appl) t ->
112 let subst,metasenv,t' = aux metasenv subst n context t in
113 subst,metasenv,t'::appl
114 ) (subst,metasenv,[]) l
116 subst,metasenv,C.Appl (List.rev revl')
117 | C.Const (uri,exp_named_subst) ->
118 let subst,metasenv,exp_named_subst' =
119 aux_exp_named_subst metasenv subst n context exp_named_subst
121 subst,metasenv,C.Const (uri,exp_named_subst')
122 | C.MutInd (uri,i,exp_named_subst) ->
123 let subst,metasenv,exp_named_subst' =
124 aux_exp_named_subst metasenv subst n context exp_named_subst
126 subst,metasenv,C.MutInd (uri,i,exp_named_subst')
127 | C.MutConstruct (uri,i,j,exp_named_subst) ->
128 let subst,metasenv,exp_named_subst' =
129 aux_exp_named_subst metasenv subst n context exp_named_subst
131 subst,metasenv,C.MutConstruct (uri,i,j,exp_named_subst')
132 | C.MutCase (sp,i,outt,t,pl) ->
133 let subst,metasenv,outt' = aux metasenv subst n context outt in
134 let subst,metasenv,t' = aux metasenv subst n context t in
135 let subst,metasenv,revpl' =
137 (fun (subst,metasenv,pl) t ->
138 let subst,metasenv,t' = aux metasenv subst n context t in
139 subst,metasenv,t'::pl
140 ) (subst,metasenv,[]) pl
142 subst,metasenv,C.MutCase (sp,i,outt', t', List.rev revpl')
144 (*CSC: not implemented
145 let tylen = List.length fl in
148 (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
151 C.Fix (i, substitutedfl)
152 *) subst,metasenv,CicMetaSubst.lift subst 1 t'
154 (*CSC: not implemented
155 let tylen = List.length fl in
158 (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
161 C.CoFix (i, substitutedfl)
162 *) subst,metasenv,CicMetaSubst.lift subst 1 t'
164 and aux_exp_named_subst metasenv subst n context ens =
166 (fun (uri,t) (subst,metasenv,l) ->
167 let subst,metasenv,t' = aux metasenv subst n context t in
168 subst,metasenv,(uri,t')::l) ens (subst,metasenv,[])
170 let argty = type_of_aux' metasenv subst context arg in
172 FreshNamesGenerator.mk_fresh_name
173 metasenv context (Cic.Name "Heta") ~typ:argty
175 let subst,metasenv,t' = aux metasenv subst 0 context t in
176 subst, metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
178 and beta_expand_many test_equality_only metasenv subst context t =
180 (fun (subst,metasenv,t) arg ->
181 beta_expand test_equality_only metasenv subst context t arg
184 (* NUOVA UNIFICAZIONE *)
185 (* A substitution is a (int * Cic.term) list that associates a
186 metavariable i with its body.
187 A metaenv is a (int * Cic.term) list that associate a metavariable
189 fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
190 a new substitution which is _NOT_ unwinded. It must be unwinded before
193 and fo_unif_subst test_equality_only subst context metasenv t1 t2 =
194 let module C = Cic in
195 let module R = CicMetaSubst in
196 let module S = CicSubstitution in
198 (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
199 let ok,subst,metasenv =
202 (fun (b,subst,metasenv) t1 t2 ->
203 if b then true,subst,metasenv else
206 | _,None -> true,subst,metasenv
207 | Some t1', Some t2' ->
208 (* First possibility: restriction *)
209 (* Second possibility: unification *)
210 (* Third possibility: convertibility *)
211 if R.are_convertible subst context t1' t2' then
217 test_equality_only subst context metasenv t1' t2'
221 Not_found -> false,subst,metasenv)
222 ) (true,subst,metasenv) ln lm
224 Invalid_argument _ ->
225 raise (UnificationFailure (sprintf
226 "Error trying to unify %s with %s: the lengths of the two local contexts do not match." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
231 raise (UnificationFailure (sprintf
232 "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
233 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
234 | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
235 fo_unif_subst test_equality_only subst context metasenv t2 t1
237 | (t, C.Meta (n,l)) ->
240 C.Meta (n,_), C.Meta (m,_) when n < m -> false
241 | _, C.Meta _ -> false
244 let lower = fun x y -> if swap then y else x in
245 let upper = fun x y -> if swap then x else y in
246 let fo_unif_subst_ordered
247 test_equality_only subst context metasenv m1 m2 =
248 fo_unif_subst test_equality_only subst context metasenv
249 (lower m1 m2) (upper m1 m2)
253 let (_, oldt) = CicMetaSubst.lookup_subst n subst in
254 let lifted_oldt = S.lift_meta l oldt in
256 type_of_aux' metasenv subst context lifted_oldt
258 let tyt = type_of_aux' metasenv subst context t in
259 let (subst, metasenv) =
260 fo_unif_subst_ordered test_equality_only subst context metasenv
263 fo_unif_subst_ordered
264 test_equality_only subst context metasenv t lifted_oldt
265 with CicMetaSubst.SubstNotFound _ ->
266 (* First of all we unify the type of the meta with the type of the term *)
268 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
270 let tyt = type_of_aux' metasenv subst context t in
273 subst context metasenv tyt (S.lift_meta l meta_type)
274 with AssertFailure _ ->
275 (* TODO huge hack!!!!
276 * we keep on unifying/refining in the hope that the problem will be
277 * eventually solved. In the meantime we're breaking a big invariant:
278 * the terms that we are unifying are no longer well typed in the
279 * current context (in the worst case we could even diverge)
282 prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
283 prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
287 let t',metasenv,subst =
289 CicMetaSubst.delift n subst context metasenv l t
291 (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
292 | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
296 C.Sort (C.Type u) when not test_equality_only ->
297 let u' = CicUniv.fresh () in
298 let s = C.Sort (C.Type u') in
299 ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
303 (* Unifying the types may have already instantiated n. Let's check *)
305 let (_, oldt) = CicMetaSubst.lookup_subst n subst in
306 let lifted_oldt = S.lift_meta l oldt in
307 fo_unif_subst_ordered
308 test_equality_only subst context metasenv t lifted_oldt
310 CicMetaSubst.SubstNotFound _ ->
311 let (_, context, _) = CicUtil.lookup_meta n metasenv in
312 let subst = (n, (context, t'')) :: subst in
314 (* CicMetaSubst.apply_subst_metasenv [n,(context, t'')] metasenv *)
315 CicMetaSubst.apply_subst_metasenv subst metasenv
318 (* (n,t'')::subst, metasenv *)
320 | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
321 | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
322 if UriManager.eq uri1 uri2 then
323 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
324 exp_named_subst1 exp_named_subst2
326 raise (UnificationFailure (sprintf
327 "Can't unify %s with %s due to different constants"
328 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
329 | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
330 if UriManager.eq uri1 uri2 && i1 = i2 then
331 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
332 exp_named_subst1 exp_named_subst2
334 raise (UnificationFailure (sprintf
335 "Can't unify %s with %s due to different inductive principles"
336 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
337 | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
338 C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
339 if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
340 fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
341 exp_named_subst1 exp_named_subst2
343 raise (UnificationFailure (sprintf
344 "Can't unify %s with %s due to different inductive constructors"
345 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
346 | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
347 | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
348 subst context metasenv te t2
349 | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
350 subst context metasenv t1 te
351 | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
352 (* TASSI: this is the only case in which we want == *)
353 let subst',metasenv' = fo_unif_subst true
354 subst context metasenv s1 s2 in
355 fo_unif_subst test_equality_only
356 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
357 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
358 (* TASSI: ask someone a reason for not putting true here *)
359 let subst',metasenv' = fo_unif_subst test_equality_only
360 subst context metasenv s1 s2 in
361 fo_unif_subst test_equality_only
362 subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
363 | (C.LetIn (_,s1,t1), t2)
364 | (t2, C.LetIn (_,s1,t1)) ->
366 test_equality_only subst context metasenv t2 (S.subst s1 t1)
367 | (C.Appl l1, C.Appl l2) ->
368 let subst,metasenv,t1',t2' =
370 C.Meta (i,_)::_, C.Meta (j,_)::_ when i = j ->
372 (* In the first two cases when we reach the next begin ... end
373 section useless work is done since, by construction, the list
374 of arguments will be equal.
376 | C.Meta (i,l)::args, _ ->
377 let subst,metasenv,t2' =
378 beta_expand_many test_equality_only metasenv subst context t2 args
380 subst,metasenv,t1,t2'
381 | _, C.Meta (i,l)::args ->
382 let subst,metasenv,t1' =
383 beta_expand_many test_equality_only metasenv subst context t1 args
385 subst,metasenv,t1',t2
391 C.Appl l1, C.Appl l2 ->
392 let lr1 = List.rev l1 in
393 let lr2 = List.rev l2 in
394 let rec fo_unif_l test_equality_only subst metasenv =
397 | _,[] -> assert false
399 fo_unif_subst test_equality_only subst context metasenv h1 h2
402 fo_unif_subst test_equality_only subst context metasenv
403 h (C.Appl (List.rev l))
404 | ((h1::l1),(h2::l2)) ->
405 let subst', metasenv' =
406 fo_unif_subst test_equality_only subst context metasenv h1 h2
408 fo_unif_l test_equality_only subst' metasenv' (l1,l2)
410 fo_unif_l test_equality_only subst metasenv (lr1, lr2)
413 | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
414 let subst', metasenv' =
415 fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in
416 let subst'',metasenv'' =
417 fo_unif_subst test_equality_only subst' context metasenv' t1' t2' in
420 (function (subst,metasenv) ->
421 fo_unif_subst test_equality_only subst context metasenv
422 ) (subst'',metasenv'') pl1 pl2
424 Invalid_argument _ ->
425 raise (UnificationFailure (sprintf
426 "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))
427 | (C.Rel _, _) | (_, C.Rel _) ->
431 raise (UnificationFailure (sprintf
432 "Can't unify %s with %s because they are not convertible"
433 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
434 | (C.Sort _ ,_) | (_, C.Sort _)
435 | (C.Const _, _) | (_, C.Const _)
436 | (C.MutInd _, _) | (_, C.MutInd _)
437 | (C.MutConstruct _, _) | (_, C.MutConstruct _)
438 | (C.Fix _, _) | (_, C.Fix _)
439 | (C.CoFix _, _) | (_, C.CoFix _) ->
440 if t1 = t2 || R.are_convertible subst context t1 t2 then
443 raise (UnificationFailure (sprintf
444 "Can't unify %s with %s because they are not convertible"
445 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
447 if R.are_convertible subst context t1 t2 then
450 raise (UnificationFailure (sprintf
451 "Can't unify %s with %s because they are not convertible"
452 (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
454 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
455 exp_named_subst1 exp_named_subst2
459 (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
461 fo_unif_subst test_equality_only subst context metasenv t1 t2
462 ) (subst,metasenv) exp_named_subst1 exp_named_subst2
464 Invalid_argument _ ->
469 UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
472 raise (UnificationFailure (sprintf
473 "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2)))
475 (* A substitution is a (int * Cic.term) list that associates a *)
476 (* metavariable i with its body. *)
477 (* metasenv is of type Cic.metasenv *)
478 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *)
479 (* a new substitution which is already unwinded and ready to be applied and *)
480 (* a new metasenv in which some hypothesis in the contexts of the *)
481 (* metavariables may have been restricted. *)
482 let fo_unif metasenv context t1 t2 =
483 fo_unif_subst false [] context metasenv t1 t2 ;;
485 let fo_unif_subst subst context metasenv t1 t2 =
487 sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
488 (CicMetaSubst.ppterm subst t1)
490 CicPp.ppterm (type_of_aux' metasenv subst context t1)
491 with _ -> "MALFORMED")
492 (CicMetaSubst.ppterm subst t2)
494 CicPp.ppterm (type_of_aux' metasenv subst context t2)
495 with _ -> "MALFORMED")
496 (CicMetaSubst.ppcontext subst context)
497 (CicMetaSubst.ppmetasenv metasenv subst) msg
500 fo_unif_subst false subst context metasenv t1 t2
502 | AssertFailure msg -> raise (AssertFailure (enrich_msg msg))
503 | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))