From 0191fb3768820da9287c3bd401593664f40aec7b Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 3 Feb 2004 14:07:43 +0000
Subject: [PATCH] Meta vs same Meta now tries unification when convertibility
of the two substitutions fails.
---
helm/ocaml/cic_unification/cicUnification.ml | 29 ++++++++++++++------
1 file changed, 21 insertions(+), 8 deletions(-)
diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index c23aada3d..70c7aa9cb 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -56,25 +56,34 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
let module S = CicSubstitution in
match (t1, t2) with
(C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
- let ok =
+ let ok,subst,metasenv =
List.fold_left2
- (fun b t1 t2 ->
- b &&
+ (fun (b,subst,metasenv) t1 t2 ->
+ if b then true,subst,metasenv else
match t1,t2 with
None,_
- | _,None -> true
+ | _,None -> true,subst,metasenv
| Some t1', Some t2' ->
(* First possibility: restriction *)
(* Second possibility: unification *)
(* Third possibility: convertibility *)
- R.are_convertible subst context t1' t2'
- ) true ln lm
+ if R.are_convertible subst context t1' t2' then
+ true,subst,metasenv
+ else
+ (try
+ let subst,metasenv =
+ fo_unif_subst subst context metasenv t1' t2'
+ in
+ true,subst,metasenv
+ with
+ Not_found -> false,subst,metasenv)
+ ) (true,subst,metasenv) ln lm
in
if ok then
subst,metasenv
else
raise (UnificationFailure (sprintf
- "Error trying to unify %s with %s: the algorithm only tried to check convertibility of the two substitutions"
+ "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."
(CicPp.ppterm t1) (CicPp.ppterm t2)))
| (C.Meta (n,l), C.Meta (m,_)) when n>m ->
fo_unif_subst subst context metasenv t2 t1
@@ -97,13 +106,17 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
type_of_aux' metasenv' subst'' context t
in
fo_unif_subst subst'' context metasenv' (S.lift_meta l meta_type) tyt
- with CicTypeChecker.SortExpectedMetaFound _ ->
+ with _ ->
(* TODO huge hack!!!!
* we keep on unifying/refining in the hope that the problem will be
* eventually solved. In the meantime we're breaking a big invariant:
* the terms that we are unifying are no longer well typed in the
* current context (in the worst case we could even diverge)
*)
+(*
+prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
+prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
+*)
(subst'', metasenv'))
| (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
| (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
--
2.39.5