- new implementation of the apply case in fo_unif using beta expansion

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 36a25a6c227928f4fddb099195cc508a078e42d8..7bd3de5c2a0f09aa92e0094d80f999dac7272276 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -161,9 +161,15 @@ and type_of_aux' metasenv context t =
          check_metasenv_consistency n subst metasenv context canonical_context l
         in
         CicSubstitution.lift_meta l ty, subst', metasenv'
-    | C.Sort s ->
-       C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
-        subst,metasenv
+     (* TASSI: CONSTRAINT *)
+    | C.Sort (C.Type t) -> 
+        let t' = CicUniv.fresh() in 
+        if not (CicUniv.add_gt t' t ) then
+         assert false (* t' is fresh! an error in CicUniv *)
+       else
+          C.Sort (C.Type t'),subst,metasenv
+     (* TASSI: CONSTRAINT *)
+    | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv
     | C.Implicit _ -> raise (AssertFailure "21")
     | C.Cast (te,ty) ->
        let _,subst',metasenv' =
@@ -308,6 +314,7 @@ and type_of_aux' metasenv context t =
            The easy case is when the outype is specified, that amount
            to a trivial check. Otherwise, we should guess a type from
            its instances *)
+
         (* easy case *)
         let _, subst, metasenv =
           type_of_aux subst metasenv context
@@ -445,6 +452,7 @@ and type_of_aux' metasenv context t =
     | ((uri,t) as subst)::tl ->
        let typeofvar =
         CicSubstitution.subst_vars substs (type_of_variable uri) in
+(* CSC: why was this code here? it is wrong
        (match CicEnvironment.get_cooked_obj ~trust:false uri with
            Cic.Variable (_,Some bo,_,_) ->
             raise
@@ -456,16 +464,19 @@ and type_of_aux' metasenv context t =
             (RefineFailure
              ("Unkown variable definition " ^ UriManager.string_of_uri uri))
        ) ;
+*)
        let typeoft,metasubst',metasenv' =
         type_of_aux metasubst metasenv context t
        in
-        try
-         let metasubst'',metasenv'' =
+        let metasubst'',metasenv'' =
+         try
           fo_unif_subst metasubst' context metasenv' typeoft typeofvar
-         in
-          check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
-        with _ ->
-         raise (RefineFailure "Wrong Explicit Named Substitution")
+         with _ ->
+          raise (RefineFailure
+           ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^
+            " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar))
+        in
+         check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
   in
    check_exp_named_subst_aux metasubst metasenv []
 
@@ -478,9 +489,15 @@ and type_of_aux' metasenv context t =
        (C.Sort s1, C.Sort s2)
          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
           C.Sort s2,subst,metasenv
-     | (C.Sort s1, C.Sort s2) ->
-         (*CSC manca la gestione degli universi!!! *)
-         C.Sort C.Type,subst,metasenv
+     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
+       (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
+       let t' = CicUniv.fresh() in 
+       if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
+         assert false ; (* not possible, error in CicUniv *)
+       C.Sort (C.Type t'),subst,metasenv
+     | (C.Sort _,C.Sort (C.Type t1)) -> 
+       (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
+       C.Sort (C.Type t1),subst,metasenv
      | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
      | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
          (* TODO how can we force the meta to become a sort? If we don't we
@@ -548,7 +565,7 @@ and type_of_aux' metasenv context t =
         (match hetype with
             Cic.Prod (n,s,t) ->
               let subst,metasenv =
-               fo_unif_subst subst context metasenv s hety
+               fo_unif_subst subst context metasenv hety s
               in
                eat_prods metasenv subst context
                 (CicMetaSubst.subst subst hete t) tl
@@ -559,7 +576,6 @@ and type_of_aux' metasenv context t =
      eat_prods metasenv subst context hetype' tlbody_and_type
     in
      t,subst,metasenv
-
 (*
   let rec aux context' args (resty,subst,metasenv) =
    function
@@ -608,7 +624,6 @@ and type_of_aux' metasenv context t =
   in
    aux [] [] (hetype,subst,metasenv) tlbody_and_type
 *)
-
  in
   let ty,subst',metasenv' =
    type_of_aux [] metasenv context t