From 12a55c7dd3cb44f7a4586524d5e342966bcfae60 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 16 Mar 2004 17:47:06 +0000 Subject: [PATCH] Sorts are no longer all convertible. To be completed once that universes are implemented. --- .../cic_proof_checking/cicReductionMachine.ml | 2 +- .../cic_proof_checking/cicTypeChecker.ml | 2 +- helm/ocaml/cic_unification/cicUnification.ml | 19 ++++++++++++++++--- 3 files changed, 18 insertions(+), 5 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml index dbe22fb3e..4aee1b2b9 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml @@ -802,7 +802,7 @@ let are_convertible = | _,None -> true | Some t1',Some t2' -> aux context t1' t2' ) true l1 l2 - | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *) + | (C.Sort s1, C.Sort s2) when s1 = s2 || s2 = C.Type -> true | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2 diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 431449e43..04b769b5c 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -1665,7 +1665,7 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ | (hete, hety)::tl -> (match (CicReduction.whd context hetype) with Cic.Prod (n,s,t) -> - if CicReduction.are_convertible context s hety then + if CicReduction.are_convertible context hety s then (CicReduction.fdebug := -1 ; eat_prods context (CicSubstitution.subst hete t) tl ) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 9c2dde84b..c56fb0874 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -92,15 +92,28 @@ let rec fo_unif_subst subst context metasenv t1 t2 = raise (UnificationFailure (sprintf "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,l), C.Meta (m,_)) when n>m -> + | (C.Meta (n,_), 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 fo_unif_subst = + let (lower,upper) = + match t1,t2 with + C.Meta (n,_), C.Meta (m,_) when n < m -> + (fun t1 t2 -> t1), (fun t1 t2 -> t2) + | _, C.Meta _ -> + (fun t1 t2 -> t1), (fun t1 t2 -> t2) + | _,_ -> + (fun t1 t2 -> t2), (fun t1 t2 -> t1) + in + fun subst context metasenv m1 m2 -> + fo_unif_subst 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 subst context metasenv lifted_oldt t + fo_unif_subst subst context metasenv t lifted_oldt with Not_found -> let t',metasenv',subst' = try @@ -116,7 +129,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 = let tyt = type_of_aux' metasenv' subst'' context t in - fo_unif_subst subst'' context metasenv' (S.lift_meta l meta_type) tyt + fo_unif_subst 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 -- 2.39.2