X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=87b3f7f42a319f227f06ce9d9c7b3db5bfc85e53;hb=790eccfa6b94dc82826d919691f8d4bfadb04573;hp=065dbc33d9cd8a3e2d6a6a175962809e63a9997e;hpb=97b18234921aec71a8b89ec2c1b058e12e5e043c;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 065dbc33d..87b3f7f42 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -295,7 +295,6 @@ and type_of_mutual_inductive_constr uri i j ugraph =
  
 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
   let module C = Cic in
-    (* let module R = CicMetaSubst in *)
   let module R = CicReduction in
     match R.whd ~subst context expectedtype with
         C.MutInd (_,_,_) ->
@@ -303,7 +302,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
       | C.Appl (C.MutInd (_,_,_)::tl) ->
           let (_,arguments) = split tl left_args_no in
             (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph 
-      | C.Prod (name,so,de) ->
+      | C.Prod (_,so,de) ->
           (* we expect that the actual type of the branch has the due 
              number of Prod *)
           (match R.whd ~subst context actualtype with
@@ -317,12 +316,12 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
                    (* we should also check that the name variable is anonymous in
                       the actual type de' ?? *)
                    check_branch (n+1) 
-                     ((Some (name,(C.Decl so)))::context) 
+                     ((Some (name',(C.Decl so)))::context) 
                        metasenv subst left_args_no de' term' de ugraph1
              | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
       | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
 
-and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
+and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
      ugraph
 =
   let rec type_of_aux subst metasenv context t ugraph =
@@ -583,7 +582,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                    context ^ " has type " ^
                   CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
                    context ^ " but is here used with type " ^
-                  CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
+                  CicMetaSubst.ppterm_in_context ~metasenv subst expected_type'
+                  context))
            in
            let rec instantiate_prod t =
             function
@@ -632,7 +632,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                           context)) exn
                   in
                     (p'::pl,j-1,
-                     outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
+                     outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
                pl ([],List.length pl,[],subst,metasenv,ugraph3)
            in
            
@@ -649,7 +649,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                (let candidate,ugraph5,metasenv,subst = 
                  let exp_name_subst, metasenv = 
                     let o,_ = 
-                      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri 
+                      CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri 
                     in
                     let uris = CicUtil.params_of_obj o in
                     List.fold_right (
@@ -801,7 +801,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                         in
                           C.Appl (outtype'::args)
                       in
-                        CicReduction.whd ~subst context appl
+                        CicReduction.head_beta_reduce ~delta:false 
+                          ~upto:(List.length args) appl 
                     in
                      try
                       fo_unif_subst subst context metasenv instance instance'
@@ -817,12 +818,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                             context ^ " but is here used with type " ^
                            CicMetaSubst.ppterm_in_context ~metasenv subst instance
                             context)))
-                 (subst,metasenv,ugraph5) pl' outtypeinstances 
+                 (subst,metasenv,ugraph5) pl' outtypeinstances
              in
                C.MutCase (uri, i, outtype, term', pl'),
                  CicReduction.head_beta_reduce
                   (CicMetaSubst.apply_subst subst
-                   (C.Appl(outtype::right_args@[term]))),
+                   (C.Appl(outtype::right_args@[term']))),
                  subst,metasenv,ugraph6)
         | C.Fix (i,fl) ->
             let fl_ty',subst,metasenv,types,ugraph1,len =
@@ -857,7 +858,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
                            context' ^ " but is here used with type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
-                           context))
+                           context'))
                    in 
                      fl @ [bo'] , subst',metasenv',ugraph'
                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty') 
@@ -1064,8 +1065,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
     let t1'' = CicReduction.whd ~subst context t1 in
     let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
       match (t1'', t2'') with
-          (C.Sort s1, C.Sort s2)
-            when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> 
+        | (C.Sort s1, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) -> 
               (* different than Coq manual!!! *)
               C.Sort s2,subst,metasenv,ugraph
         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
@@ -1076,8 +1076,34 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                 C.Sort (C.Type t'),subst,metasenv,ugraph2
               with
                CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+        | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) -> 
+            let t' = CicUniv.fresh() in 
+             (try
+              let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+              let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+                C.Sort (C.CProp t'),subst,metasenv,ugraph2
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+        | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) -> 
+            let t' = CicUniv.fresh() in 
+             (try
+              let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+              let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+                C.Sort (C.CProp t'),subst,metasenv,ugraph2
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+        | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) -> 
+            let t' = CicUniv.fresh() in 
+             (try
+              let ugraph1 = CicUniv.add_gt t' t1 ugraph in
+              let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+                C.Sort (C.Type t'),subst,metasenv,ugraph2
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
         | (C.Sort _,C.Sort (C.Type t1)) -> 
             C.Sort (C.Type t1),subst,metasenv,ugraph
+        | (C.Sort _,C.Sort (C.CProp t1)) -> 
+            C.Sort (C.CProp t1),subst,metasenv,ugraph
         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph
         | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
             (* TODO how can we force the meta to become a sort? If we don't we
@@ -1597,11 +1623,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                      CicTypeChecker.type_of_aux' ~subst metasenv context m
                        CicUniv.oblivion_ugraph 
                    with
-                   | Cic.MutInd _ as mty,_ -> [], mty
-                   | Cic.Appl (Cic.MutInd _::args) as mty,_ ->
+                   | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty
+                   | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
                        snd (HExtlib.split_nth leftno args), mty
                    | _ -> assert false
-                 with CicTypeChecker.TypeCheckerFailure _ -> assert false
+                 with CicTypeChecker.TypeCheckerFailure _ -> 
+                    raise (AssertFailure(lazy "already ill-typed matched term"))
                in
                let new_outty =
                 keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
@@ -1745,10 +1772,15 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
     (*  substituted_t,substituted_ty,substituted_metasenv *)
     (* ANDREA: spostare tutta questa robaccia da un altra parte *)
   let cleaned_t =
-    FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
+   if clean_dummy_dependent_types then
+    FreshNamesGenerator.clean_dummy_dependent_types substituted_t
+   else substituted_t in
   let cleaned_ty =
-    FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
+   if clean_dummy_dependent_types then
+    FreshNamesGenerator.clean_dummy_dependent_types substituted_ty
+   else substituted_ty in
   let cleaned_metasenv =
+   if clean_dummy_dependent_types then
     List.map
       (function (n,context,ty) ->
          let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
@@ -1768,6 +1800,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
          in
            (n,context',ty')
       ) substituted_metasenv
+   else
+    substituted_metasenv
   in
     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) 
 ;;
@@ -1847,7 +1881,7 @@ let are_all_occurrences_positive metasenv ugraph uri tys leftno =
   metasenv,ugraph,substituted_tys
     
 let typecheck metasenv uri obj ~localization_tbl =
- let ugraph = CicUniv.empty_ugraph in
+ let ugraph = CicUniv.oblivion_ugraph in
  match obj with
     Cic.Constant (name,Some bo,ty,args,attrs) ->
      (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
@@ -1926,7 +1960,12 @@ let typecheck metasenv uri obj ~localization_tbl =
       List.fold_right
        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
          let ty',_,metasenv,ugraph =
-          type_of_aux' ~localization_tbl metasenv [] ty ugraph
+          (* clean_dummy_dependent_types: false to avoid cleaning the names
+             of the left products, that must be identical to those of the
+             constructors; however, non-left products should probably be
+             cleaned *)
+          type_of_aux' ~clean_dummy_dependent_types:false ~localization_tbl
+           metasenv [] ty ugraph
          in
           metasenv,ugraph,(name,b,ty',cl)::res
        ) tys (metasenv,ugraph,[]) in