From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 16 Mar 2004 17:47:06 +0000 (+0000)
Subject: Sorts are no longer all convertible. To be completed once that universes
X-Git-Tag: v0_0_4~14
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=12a55c7dd3cb44f7a4586524d5e342966bcfae60;p=helm.git

Sorts are no longer all convertible. To be completed once that universes
are implemented.
---

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