From 0191fb3768820da9287c3bd401593664f40aec7b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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.2