prod moved under lambda-prolog unification case

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 065dbc33d9cd8a3e2d6a6a175962809e63a9997e..a1a7bdea8ebe9f5861bb602d61fd13cf7e390abe 100644 (file)
--- 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') 
@@ -1745,10 +1746,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 +1774,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 +1855,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 +1934,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