X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=35eb18f450974d61fc238b77d3f985203b249d6b;hb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;hp=b9f87cf9a14a4f4b3e27ecb9d2524cc90fb25471;hpb=7af6bb6e640a44489bdab79a38300cf103e45bd4;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index b9f87cf9a..35eb18f45 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -52,7 +52,7 @@ let type_of_aux' metasenv subst context term = a new substitution which is _NOT_ unwinded. It must be unwinded before applying it. *) -let rec fo_unif_subst subst context metasenv t1 t2 = +let rec fo_unif_subst test_equality_only subst context metasenv t1 t2 = let module C = Cic in let module R = CicMetaSubst in let module S = CicSubstitution in @@ -75,7 +75,8 @@ let rec fo_unif_subst subst context metasenv t1 t2 = else (try let subst,metasenv = - fo_unif_subst subst context metasenv t1' t2' + fo_unif_subst + test_equality_only subst context metasenv t1' t2' in true,subst,metasenv with @@ -93,7 +94,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 = "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." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) | (C.Meta (n,_), C.Meta (m,_)) when n>m -> - fo_unif_subst subst context metasenv t2 t1 + fo_unif_subst test_equality_only subst context metasenv t2 t1 | (C.Meta (n,l), t) | (t, C.Meta (n,l)) -> let swap = @@ -104,14 +105,17 @@ let rec fo_unif_subst subst context metasenv t1 t2 = in let lower = fun x y -> if swap then y else x in let upper = fun x y -> if swap then x else y in - let fo_unif_subst_ordered subst context metasenv m1 m2 = - fo_unif_subst subst context metasenv (lower m1 m2) (upper m1 m2) + let fo_unif_subst_ordered + test_equality_only subst context metasenv m1 m2 = + fo_unif_subst test_equality_only subst context metasenv + (lower m1 m2) (upper m1 m2) in let subst'',metasenv' = try let oldt = (List.assoc n subst) in let lifted_oldt = S.lift_meta l oldt in - fo_unif_subst_ordered subst context metasenv t lifted_oldt + fo_unif_subst_ordered + test_equality_only subst context metasenv t lifted_oldt with Not_found -> let t',metasenv',subst' = try @@ -120,14 +124,25 @@ let rec fo_unif_subst subst context metasenv t1 t2 = (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg) | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) in - (n, t')::subst', metasenv' + let t'' = + match t' with + C.Sort (C.Type u) when not test_equality_only -> + let u' = CicUniv.fresh () in + let s = C.Sort (C.Type u') in + ignore (CicUniv.add_ge (upper u u') (lower u u')) ; + s + | _ -> t' + in + (n, t'')::subst', metasenv' in let (_,_,meta_type) = CicUtil.lookup_meta n metasenv' in (try let tyt = type_of_aux' metasenv' subst'' context t in - fo_unif_subst subst'' context metasenv' tyt (S.lift_meta l meta_type) + fo_unif_subst + test_equality_only + subst'' context metasenv' tyt (S.lift_meta l meta_type) with AssertFailure _ -> (* TODO huge hack!!!! * we keep on unifying/refining in the hope that the problem will be @@ -143,7 +158,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; | (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 - fo_unif_subst_exp_named_subst subst context metasenv + fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 else raise (UnificationFailure (sprintf @@ -151,7 +166,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst 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 + fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 else raise (UnificationFailure (sprintf @@ -160,52 +175,62 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; | C.MutConstruct (uri1,i1,j1,exp_named_subst1), C.MutConstruct (uri2,i2,j2,exp_named_subst2) -> if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then - fo_unif_subst_exp_named_subst subst context metasenv + fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 else raise (UnificationFailure (sprintf "Can't unify %s with %s due to different inductive constructors" (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) | (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.Cast (te,ty), t2) -> fo_unif_subst test_equality_only + subst context metasenv te t2 + | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only + subst context metasenv t1 te | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> - let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in - fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 + (* TASSI: this is the only case in which we want == *) + let subst',metasenv' = fo_unif_subst true + subst context metasenv s1 s2 in + fo_unif_subst test_equality_only + subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> - let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in - fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 + (* TASSI: ask someone a reason for not putting true here *) + let subst',metasenv' = fo_unif_subst test_equality_only + subst context metasenv s1 s2 in + fo_unif_subst test_equality_only + subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 | (C.LetIn (_,s1,t1), t2) | (t2, C.LetIn (_,s1,t1)) -> - fo_unif_subst subst context metasenv t2 (S.subst s1 t1) + fo_unif_subst + test_equality_only subst context metasenv t2 (S.subst s1 t1) | (C.Appl l1, C.Appl l2) -> let lr1 = List.rev l1 in let lr2 = List.rev l2 in - let rec fo_unif_l subst metasenv = + let rec fo_unif_l test_equality_only subst metasenv = function [],_ | _,[] -> assert false | ([h1],[h2]) -> - fo_unif_subst subst context metasenv h1 h2 + fo_unif_subst test_equality_only subst context metasenv h1 h2 | ([h],l) | (l,[h]) -> - fo_unif_subst subst context metasenv h (C.Appl (List.rev l)) + fo_unif_subst + test_equality_only subst context metasenv h (C.Appl (List.rev l)) | ((h1::l1),(h2::l2)) -> let subst', metasenv' = - fo_unif_subst subst context metasenv h1 h2 + fo_unif_subst test_equality_only subst context metasenv h1 h2 in - fo_unif_l subst' metasenv' (l1,l2) + fo_unif_l test_equality_only subst' metasenv' (l1,l2) in - fo_unif_l subst metasenv (lr1, lr2) + fo_unif_l test_equality_only subst metasenv (lr1, lr2) | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> let subst', metasenv' = - fo_unif_subst subst context metasenv outt1 outt2 in + fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in let subst'',metasenv'' = - fo_unif_subst subst' context metasenv' t1' t2' in + fo_unif_subst test_equality_only subst' context metasenv' t1' t2' in (try List.fold_left2 (function (subst,metasenv) -> - fo_unif_subst subst context metasenv + fo_unif_subst test_equality_only subst context metasenv ) (subst'',metasenv'') pl1 pl2 with Invalid_argument _ -> @@ -232,14 +257,14 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; "Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) -and fo_unif_subst_exp_named_subst subst context metasenv +and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 = try List.fold_left2 (fun (subst,metasenv) (uri1,t1) (uri2,t2) -> assert (uri1=uri2) ; - fo_unif_subst subst context metasenv t1 t2 + fo_unif_subst test_equality_only subst context metasenv t1 t2 ) (subst,metasenv) exp_named_subst1 exp_named_subst2 with Invalid_argument _ -> @@ -260,7 +285,8 @@ and fo_unif_subst_exp_named_subst subst context metasenv (* 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 = fo_unif_subst [] context metasenv t1 t2 ;; +let fo_unif metasenv context t1 t2 = + fo_unif_subst false [] context metasenv t1 t2 ;; let fo_unif_subst subst context metasenv t1 t2 = let enrich_msg msg = @@ -277,7 +303,7 @@ let fo_unif_subst subst context metasenv t1 t2 = (CicMetaSubst.ppmetasenv metasenv subst) msg in try - fo_unif_subst subst context metasenv t1 t2 + fo_unif_subst false subst context metasenv t1 t2 with | AssertFailure msg -> raise (AssertFailure (enrich_msg msg)) | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))