X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=fb1ca113f23e7f3b40035b8c68f47cd74bf9048d;hb=9f60b3b0f4460aec52ec241037f6c475b421dd15;hp=704eecb467135939170c631c373236c36c3ffb00;hpb=04ca589d65bcef6bd46cf4d277a748a12e09234b;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 704eecb46..fb1ca113f 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -25,20 +25,23 @@ open Printf -exception AssertFailure of string;; exception UnificationFailure of string;; +exception Uncertain of string;; +exception AssertFailure of string;; let debug_print = prerr_endline let type_of_aux' metasenv subst context term = try CicMetaSubst.type_of_aux' metasenv subst context term - with CicMetaSubst.MetaSubstFailure msg -> + with + | 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 @@ -55,42 +58,72 @@ 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 metasenv 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 | (C.Meta (n,l), t) | (t, C.Meta (n,l)) -> - let subst',metasenv' = + let subst'',metasenv' = try let oldt = (List.assoc n subst) in let lifted_oldt = S.lift_meta l oldt in fo_unif_subst subst context metasenv lifted_oldt t with Not_found -> - let t',metasenv' = CicMetaSubst.delift n subst context metasenv l t in - (n, t')::subst, metasenv' + 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 let (_,_,meta_type) = CicUtil.lookup_meta n metasenv' in - let tyt = type_of_aux' metasenv' subst' context t in - fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt + (try + let tyt = + type_of_aux' metasenv' subst'' context t + in + fo_unif_subst subst'' context metasenv' (S.lift_meta l meta_type) tyt + 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)) -> if UriManager.eq uri1 uri2 then @@ -99,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 @@ -117,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)) -> @@ -164,14 +197,14 @@ let rec fo_unif_subst subst context metasenv t1 t2 = | (C.MutConstruct _, _) | (_, C.MutConstruct _) | (C.Fix _, _) | (_, C.Fix _) | (C.CoFix _, _) | (_, C.CoFix _) -> - if R.are_convertible metasenv subst context t1 t2 then + if R.are_convertible subst context t1 t2 then subst, metasenv else raise (UnificationFailure (sprintf "Can't unify %s with %s because they are not convertible" (CicPp.ppterm t1) (CicPp.ppterm t2))) | (_,_) -> - if R.are_convertible metasenv subst context t1 t2 then + if R.are_convertible subst context t1 t2 then subst, metasenv else raise (UnificationFailure (sprintf @@ -200,24 +233,21 @@ debug_print ("@@@: " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst1)) ^ (* a new substitution which is already unwinded and ready to be applied and *) (* a new metasenv in which some hypothesis in the contexts of the *) (* metavariables may have been restricted. *) -let fo_unif metasenv context t1 t2 = - let subst_to_unwind,metasenv' = fo_unif_subst [] context metasenv t1 t2 in - CicMetaSubst.unwind_subst metasenv' subst_to_unwind -;; +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") (CicMetaSubst.ppcontext subst context) - (CicMetaSubst.ppmetasenv subst metasenv) msg + (CicMetaSubst.ppmetasenv metasenv subst) msg in try fo_unif_subst subst context metasenv t1 t2