X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=fb1ca113f23e7f3b40035b8c68f47cd74bf9048d;hb=9f60b3b0f4460aec52ec241037f6c475b421dd15;hp=59ccc9ae907b4912f9674f59f7b57e3d4cf1f155;hpb=2f4e2076f4b53f0c3e277bff67268cb80bfae967;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 59ccc9ae9..fb1ca113f 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -25,8 +25,9 @@ open Printf -exception AssertFailure of string;; exception UnificationFailure of string;; +exception Uncertain of string;; +exception AssertFailure of string;; let debug_print = prerr_endline @@ -37,9 +38,10 @@ let type_of_aux' metasenv subst context term = | CicMetaSubst.MetaSubstFailure msg -> raise (AssertFailure ((sprintf - "Type checking error: %s in context\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms" - (CicPp.ppterm (CicMetaSubst.apply_subst subst term)) - (CicMetaSubst.ppcontext subst context) msg))) + "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" + (CicMetaSubst.ppterm subst term) + (CicMetaSubst.ppcontext subst context) + (CicMetaSubst.ppmetasenv metasenv subst) msg))) (* NUOVA UNIFICAZIONE *) (* A substitution is a (int * Cic.term) list that associates a @@ -56,25 +58,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 @@ -87,7 +98,11 @@ let rec fo_unif_subst subst context metasenv t1 t2 = fo_unif_subst subst context metasenv lifted_oldt t with Not_found -> let t',metasenv',subst' = + try CicMetaSubst.delift n subst context metasenv l t + with + (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg) + | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) in (n, t')::subst', metasenv' in @@ -97,13 +112,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 AssertFailure _ -> (* 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)) -> @@ -113,7 +132,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 = else raise (UnificationFailure (sprintf "Can't unify %s with %s due to different constants" - (CicPp.ppterm t1) (CicPp.ppterm t1))) + (CicPp.ppterm t1) (CicPp.ppterm t2))) | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) -> if UriManager.eq uri1 uri2 && i1 = i2 then fo_unif_subst_exp_named_subst subst context metasenv @@ -131,7 +150,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 = raise (UnificationFailure (sprintf "Can't unify %s with %s due to different inductive constructors" (CicPp.ppterm t1) (CicPp.ppterm t1))) - | (C.Implicit, _) | (_, C.Implicit) -> assert false + | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2 | (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> @@ -219,11 +238,11 @@ let fo_unif metasenv context t1 t2 = fo_unif_subst [] context metasenv t1 t2 ;; let fo_unif_subst subst context metasenv t1 t2 = let enrich_msg msg = sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s" - (CicPp.ppterm (CicMetaSubst.apply_subst subst t1)) + (CicMetaSubst.ppterm subst t1) (try CicPp.ppterm (type_of_aux' metasenv subst context t1) with _ -> "MALFORMED") - (CicPp.ppterm (CicMetaSubst.apply_subst subst t2)) + (CicMetaSubst.ppterm subst t2) (try CicPp.ppterm (type_of_aux' metasenv subst context t2) with _ -> "MALFORMED")