X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=b3525d3182bcec3737d02c2883cd7402d1acf730;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=54fde9a45a6d49c4d8e8d33ce88e98af2282f552;hpb=04ca589d65bcef6bd46cf4d277a748a12e09234b;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 54fde9a45..b3525d318 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -25,37 +25,25 @@
 
 open Printf
 
-exception Impossible of int;;
-exception NotRefinable of string;;
+exception RefineFailure of string;;
 exception Uncertain of string;;
-exception WrongUriToConstant of string;;
-exception WrongUriToVariable of string;;
-exception ListTooShort;;
-exception WrongUriToMutualInductiveDefinitions of string;;
-exception RelToHiddenHypothesis;;
-exception MetasenvInconsistency;;
-exception MutCaseFixAndCofixRefineNotImplemented;;
-exception WrongArgumentNumber;;
-
-let fdebug = ref 0;;
-let debug t context =
- let rec debug_aux t i =
-  let module C = Cic in
-  let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
- in
-  if !fdebug = 0 then
-   raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
-   (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
-;;
+exception AssertFailure of string;;
 
 let debug_print = prerr_endline
 
+let fo_unif_subst subst context metasenv t1 t2 =
+ try
+  CicUnification.fo_unif_subst subst context metasenv t1 t2
+ with
+    (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
+  | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
+;;
+
 let rec split l n =
  match (l,n) with
     (l,0) -> ([], l)
   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
-  | (_,_) -> raise ListTooShort
+  | (_,_) -> raise (AssertFailure "split: list too short")
 ;;
 
 let rec type_of_constant uri =
@@ -65,7 +53,9 @@ let rec type_of_constant uri =
   match CicEnvironment.get_cooked_obj uri with
      C.Constant (_,_,ty,_) -> ty
    | C.CurrentProof (_,_,_,ty,_) -> ty
-   | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
+   | _ ->
+     raise
+      (RefineFailure ("Unknown constant definition " ^  U.string_of_uri uri))
 
 and type_of_variable uri =
  let module C = Cic in
@@ -73,7 +63,10 @@ and type_of_variable uri =
  let module U = UriManager in
   match CicEnvironment.get_cooked_obj uri with
      C.Variable (_,_,ty,_) -> ty
-   |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+   |  _ ->
+      raise
+       (RefineFailure
+         ("Unknown variable definition " ^ UriManager.string_of_uri uri))
 
 and type_of_mutual_inductive_defs uri i =
  let module C = Cic in
@@ -83,7 +76,10 @@ and type_of_mutual_inductive_defs uri i =
      C.InductiveDefinition (dl,_,_) ->
       let (_,_,arity,_) = List.nth dl i in
        arity
-   | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+   | _ ->
+     raise
+      (RefineFailure
+        ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
 
 and type_of_mutual_inductive_constr uri i j =
  let module C = Cic in
@@ -94,7 +90,10 @@ and type_of_mutual_inductive_constr uri i j =
        let (_,_,_,cl) = List.nth dl i in
         let (_,ty) = List.nth cl (j-1) in
          ty
-   | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
+   | _ ->
+     raise
+      (RefineFailure
+        ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
 
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 
@@ -109,8 +108,7 @@ and type_of_mutual_inductive_constr uri i j =
 and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
   let module C = Cic in
   let module R = CicMetaSubst in
-  let module Un = CicUnification in 
-  match R.whd metasenv subst context expectedtype with
+  match R.whd subst context expectedtype with
      C.MutInd (_,_,_) ->
        (n,context,actualtype, [term]), subst, metasenv
    | C.Appl (C.MutInd (_,_,_)::tl) ->
@@ -119,10 +117,10 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
    | C.Prod (name,so,de) ->
       (* we expect that the actual type of the branch has the due 
          number of Prod *)
-      (match R.whd metasenv subst context actualtype with
+      (match R.whd subst context actualtype with
            C.Prod (name',so',de') ->
              let subst, metasenv = 
-                Un.fo_unif_subst subst context metasenv so so' in
+               fo_unif_subst subst context metasenv so so' in
              let term' =
                (match CicSubstitution.lift 1 term with
                    C.Appl l -> C.Appl (l@[C.Rel 1])
@@ -130,15 +128,14 @@ 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) metasenv subst left_args_no de' term' de 
-	 | _ -> raise WrongArgumentNumber)
-  | _ -> raise (NotRefinable "Prod or MutInd expected")
+        | _ -> raise (AssertFailure "Wrong number of arguments"))
+   | _ -> raise (AssertFailure "Prod or MutInd expected")
 
 and type_of_aux' metasenv context t =
  let rec type_of_aux subst metasenv context =
   let module C = Cic in
   let module S = CicSubstitution in
   let module U = UriManager in
-  let module Un = CicUnification in
    function
       C.Rel n ->
        (try
@@ -147,42 +144,46 @@ and type_of_aux' metasenv context t =
           | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
           | Some (_,C.Def (bo,None)) ->
              type_of_aux subst metasenv context (S.lift n bo)
-	  | None -> raise RelToHiddenHypothesis
+          | None -> raise (RefineFailure "Rel to hidden hypothesis")
         with
-         _ -> raise (NotRefinable "Not a close term")
+         _ -> raise (RefineFailure "Not a close term")
        )
     | C.Var (uri,exp_named_subst) ->
-      incr fdebug ;
       let subst',metasenv' =
        check_exp_named_subst subst metasenv context exp_named_subst in
       let ty =
        CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
       in
-       decr fdebug ;
        ty,subst',metasenv'
     | C.Meta (n,l) -> 
        let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
         let subst',metasenv' =
-         check_metasenv_consistency subst metasenv context canonical_context l
+         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
-    | C.Implicit -> raise (Impossible 21)
+        CicSubstitution.lift_meta l ty, 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' =
         type_of_aux subst metasenv context ty in
        let inferredty,subst'',metasenv'' =
-        type_of_aux subst' metasenv' context ty
+        type_of_aux subst' metasenv' context te
        in
         (try
           let subst''',metasenv''' =
-           Un.fo_unif_subst subst'' context metasenv'' inferredty ty
+           fo_unif_subst subst'' context metasenv'' inferredty ty
           in
            ty,subst''',metasenv'''
          with
-          _ -> raise (NotRefinable "Cast"))
+          _ -> raise (RefineFailure "Cast"))
     | C.Prod (name,s,t) ->
        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
        let sort2,subst'',metasenv'' =
@@ -191,17 +192,19 @@ and type_of_aux' metasenv context t =
         sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
    | C.Lambda (n,s,t) ->
        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
+       (match CicMetaSubst.whd subst' context sort1 with
+           C.Meta _
+         | C.Sort _ -> ()
+         | _ ->
+           raise (RefineFailure (sprintf
+            "Not well-typed lambda-abstraction: the source %s should be a type;
+             instead it is a term of type %s" (CicPp.ppterm s)
+            (CicPp.ppterm sort1)))
+       ) ;
        let type2,subst'',metasenv'' =
         type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
        in
-        let sort2,subst''',metasenv''' =
-         type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
-        in
-         (* only to check if the product is well-typed *)
-         let _,subst'''',metasenv'''' =
-          sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
-         in
-          C.Prod (n,s,type2),subst'''',metasenv''''
+          C.Prod (n,s,type2),subst'',metasenv''
    | C.LetIn (n,s,t) ->
       (* only to check if s is well-typed *)
       let ty,subst',metasenv' = type_of_aux subst metasenv context s in
@@ -223,25 +226,21 @@ and type_of_aux' metasenv context t =
         ) tl ([],subst',metasenv')
       in
        eat_prods subst'' metasenv'' context hetype tlbody_and_type
-   | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
+   | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
    | C.Const (uri,exp_named_subst) ->
-      incr fdebug ;
       let subst',metasenv' =
        check_exp_named_subst subst metasenv context exp_named_subst in
       let cty =
        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
       in
-       decr fdebug ;
        cty,subst',metasenv'
    | C.MutInd (uri,i,exp_named_subst) ->
-      incr fdebug ;
       let subst',metasenv' =
        check_exp_named_subst subst metasenv context exp_named_subst in
       let cty =
        CicSubstitution.subst_vars exp_named_subst
         (type_of_mutual_inductive_defs uri i)
       in
-       decr fdebug ;
        cty,subst',metasenv'
    | C.MutConstruct (uri,i,j,exp_named_subst) ->
       let subst',metasenv' =
@@ -259,9 +258,10 @@ and type_of_aux' metasenv context t =
               List.nth l i , expl_params, parsno
           | _ ->
             raise
-             (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
+             (RefineFailure
+              ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
        let rec count_prod t =
-         match CicMetaSubst.whd metasenv subst context t with
+         match CicMetaSubst.whd subst context t with
              C.Prod (_, _, t) -> 1 + (count_prod t)
            | _ -> 0 in 
        let no_args = count_prod arity in
@@ -286,9 +286,9 @@ and type_of_aux' metasenv context t =
        let _, subst, metasenv =
          type_of_aux subst metasenv context expected_type
        in
-       let actual_type = CicMetaSubst.whd metasenv subst context actual_type in
+       let actual_type = CicMetaSubst.whd subst context actual_type in
        let subst,metasenv =
-         Un.fo_unif_subst subst context metasenv expected_type actual_type
+         fo_unif_subst subst context metasenv expected_type actual_type
        in
        (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
        let (_,outtypeinstances,subst,metasenv) =
@@ -314,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
@@ -336,19 +337,62 @@ and type_of_aux' metasenv context t =
                   type_of_aux subst metasenv context appl
                 in
 *)
-                CicMetaSubst.whd metasenv subst context appl
+                CicMetaSubst.whd subst context appl
               in
-               Un.fo_unif_subst subst context metasenv instance instance')
+               fo_unif_subst subst context metasenv instance instance')
              (subst,metasenv) outtypeinstances in
-        CicMetaSubst.whd metasenv subst
+        CicMetaSubst.whd subst
           context (C.Appl(outtype::right_args@[term])),subst,metasenv
-   | C.Fix _
-   | C.CoFix _ -> raise MutCaseFixAndCofixRefineNotImplemented
+   | C.Fix (i,fl) ->
+      let subst,metasenv,types =
+       List.fold_left
+        (fun (subst,metasenv,types) (n,_,ty,_) ->
+          let _,subst',metasenv' = type_of_aux subst metasenv context ty in
+           subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
+        ) (subst,metasenv,[]) fl
+      in
+       let len = List.length types in
+       let context' = types@context in
+       let subst,metasenv =
+        List.fold_left
+         (fun (subst,metasenv) (name,x,ty,bo) ->
+           let ty_of_bo,subst,metasenv =
+            type_of_aux subst metasenv context' bo
+           in
+            fo_unif_subst subst context' metasenv
+              ty_of_bo (CicMetaSubst.lift subst len ty)
+         ) (subst,metasenv) fl in
+        let (_,_,ty,_) = List.nth fl i in
+         ty,subst,metasenv
+   | C.CoFix (i,fl) ->
+      let subst,metasenv,types =
+       List.fold_left
+        (fun (subst,metasenv,types) (n,ty,_) ->
+          let _,subst',metasenv' = type_of_aux subst metasenv context ty in
+           subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
+        ) (subst,metasenv,[]) fl
+      in
+       let len = List.length types in
+       let context' = types@context in
+       let subst,metasenv =
+        List.fold_left
+         (fun (subst,metasenv) (name,ty,bo) ->
+           let ty_of_bo,subst,metasenv =
+            type_of_aux subst metasenv context' bo
+           in
+            fo_unif_subst subst context' metasenv
+              ty_of_bo (CicMetaSubst.lift subst len ty)
+         ) (subst,metasenv) fl in
+      
+        let (_,ty,_) = List.nth fl i in
+         ty,subst,metasenv
 
  (* check_metasenv_consistency checks that the "canonical" context of a
  metavariable is consitent - up to relocation via the relocation list l -
  with the actual context *)
- and check_metasenv_consistency subst metasenv context canonical_context l =
+ and check_metasenv_consistency
+  metano subst metasenv context canonical_context l
+ =
    let module C = Cic in
    let module R = CicReduction in
    let module S = CicSubstitution in
@@ -361,10 +405,14 @@ and type_of_aux' metasenv context t =
        | (Some (n,C.Def (t,None)))::tl ->
           (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
        | None::tl -> None::(aux (i+1) tl)
-       | (Some (_,C.Def (_,Some _)))::_ -> assert false
+       | (Some (n,C.Def (t,Some ty)))::tl ->
+           (Some (n,
+            C.Def ((S.lift_meta l (S.lift i t)),
+              Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
      in
       aux 1 canonical_context
     in
+    try
      List.fold_left2 
       (fun (subst,metasenv) t ct -> 
         match (t,ct) with
@@ -372,19 +420,30 @@ and type_of_aux' metasenv context t =
              subst,metasenv
          | Some t,Some (_,C.Def (ct,_)) ->
             (try
-              CicUnification.fo_unif_subst subst context metasenv t ct
-             with _ -> raise MetasenvInconsistency)
+              fo_unif_subst subst context metasenv t ct
+             with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
          | Some t,Some (_,C.Decl ct) ->
             let inferredty,subst',metasenv' =
              type_of_aux subst metasenv context t
             in
              (try
-               CicUnification.fo_unif_subst
+               fo_unif_subst
                 subst' context metasenv' inferredty ct
-             with _ -> raise MetasenvInconsistency)
-         | _, _  ->
-             raise MetasenvInconsistency
+             with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))
+         | None, Some _  ->
+             raise (RefineFailure (sprintf
+              "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s"
+              (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
+              (CicMetaSubst.ppcontext subst canonical_context)))
       ) (subst,metasenv) l lifted_canonical_context 
+    with
+     Invalid_argument _ ->
+      raise
+       (RefineFailure
+         (sprintf
+           "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
+             (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
+             (CicMetaSubst.ppcontext subst canonical_context)))
 
  and check_exp_named_subst metasubst metasenv context =
   let rec check_exp_named_subst_aux metasubst metasenv substs =
@@ -396,119 +455,229 @@ and type_of_aux' metasenv context t =
        (match CicEnvironment.get_cooked_obj ~trust:false uri with
            Cic.Variable (_,Some bo,_,_) ->
             raise
-             (NotRefinable
+             (RefineFailure
                "A variable with a body can not be explicit substituted")
          | Cic.Variable (_,None,_,_) -> ()
-         | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+         | _ ->
+           raise
+            (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'' =
-          CicUnification.fo_unif_subst
-           metasubst' context metasenv' typeoft typeofvar
+          fo_unif_subst metasubst' context metasenv' typeoft typeofvar
          in
           check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
         with _ ->
-         raise (NotRefinable "Wrong Explicit Named Substitution")
+         raise (RefineFailure "Wrong Explicit Named Substitution")
   in
    check_exp_named_subst_aux metasubst metasenv []
 
  and sort_of_prod subst metasenv context (name,s) (t1, t2) =
   let module C = Cic in
-   (* ti could be a metavariable in the domain of the substitution *)
-   let subst',metasenv' = CicMetaSubst.unwind_subst metasenv subst in
-   let t1' = CicMetaSubst.apply_subst subst' t1 in
-   let t2' = CicMetaSubst.apply_subst subst' t2 in
-    let t1'' = CicMetaSubst.whd metasenv subst' context t1' in
-    let t2'' =
-      CicMetaSubst.whd metasenv subst' ((Some (name,C.Decl s))::context) t2'
-    in
+    let context_for_t2 = (Some (name,C.Decl s))::context in
+    let t1'' = CicMetaSubst.whd subst context t1 in
+    let t2'' = CicMetaSubst.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) -> (* different from 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.Meta _,_) | (_,C.Meta _) ->
-         let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv context in
-         let irl =
-           CicMkImplicit.identity_relocation_list_for_metavariable context
+         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
+          C.Sort s2,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
+          * brake the invariant that refine produce only well typed terms *)
+         (* TODO if we check the non meta term and if it is a sort then we are
+          * likely to know the exact value of the result e.g. if the rhs is a
+          * Sort (Prop | Set | CProp) then the result is the rhs *)
+         let (metasenv,idx) =
+          CicMkImplicit.mk_implicit_sort metasenv in
+         let (subst, metasenv) =
+           fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
          in
-         C.Meta (idx, irl), subst, metasenv'
+          t2'',subst,metasenv
      | (_,_) ->
-         raise (NotRefinable (sprintf
-          "Two types were expected, found %s of type %s and %s of type %s"
+         raise (RefineFailure (sprintf
+          "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
           (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
           (CicPp.ppterm t2'')))
 
- and eat_prods subst metasenv context hetype =
+ and eat_prods subst metasenv context hetype tlbody_and_type =
+ let rec mk_prod metasenv context =
   function
-     [] -> hetype,subst,metasenv
-   | (hete, hety)::tl ->
-    (match (CicMetaSubst.whd metasenv subst context hetype) with
-        Cic.Prod (n,s,t) ->
-         let subst',metasenv' =
-           CicUnification.fo_unif_subst subst context metasenv s hety
-         in
-          CicReduction.fdebug := -1 ;
-          eat_prods subst' metasenv' context (CicSubstitution.subst hete t) tl
-      | Cic.Meta _ as t ->
-         raise
-          (Uncertain
-            ("Prod expected, " ^ CicPp.ppterm t ^ " found"))
-      | _ -> raise (NotRefinable "Appl: wrong Prod-type")
-    )
+     [] ->
+       let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
+       let irl =
+        CicMkImplicit.identity_relocation_list_for_metavariable context
+       in
+        metasenv,Cic.Meta (idx, irl)
+   | (_,argty)::tl ->
+      let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
+      let irl =
+       CicMkImplicit.identity_relocation_list_for_metavariable context
+      in
+       let meta = Cic.Meta (idx,irl) in
+       let name =
+        (* The name must be fresh for context.                 *)
+        (* Nevertheless, argty is well-typed only in context.  *)
+        (* Thus I generate a name (name_hint) in context and   *)
+        (* then I generate a name --- using the hint name_hint *)
+        (* --- that is fresh in (context'@context).            *)
+        let name_hint =
+         FreshNamesGenerator.mk_fresh_name
+          (CicMetaSubst.apply_subst_metasenv subst metasenv)
+          (CicMetaSubst.apply_subst_context subst context)
+          Cic.Anonymous
+          (CicMetaSubst.apply_subst subst argty)
+        in
+         (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
+         FreshNamesGenerator.mk_fresh_name
+          [] context name_hint (Cic.Sort Cic.Prop)
+       in
+       let metasenv,target =
+        mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
+       in
+        metasenv,Cic.Prod (name,meta,target)
+ in
+  let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
+  let (subst, metasenv) =
+   fo_unif_subst subst context metasenv hetype hetype'
+  in
+   let rec eat_prods metasenv subst context hetype =
+      function
+         [] -> metasenv,subst,hetype
+       | (hete, hety)::tl ->
+        (match hetype with
+            Cic.Prod (n,s,t) ->
+              let subst,metasenv =
+               fo_unif_subst subst context metasenv hety s
+              in
+               eat_prods metasenv subst context
+                (CicMetaSubst.subst subst hete t) tl
+          | _ -> assert false
+        )
+   in
+    let metasenv,subst,t =
+     eat_prods metasenv subst context hetype' tlbody_and_type
+    in
+     t,subst,metasenv
+(*
+  let rec aux context' args (resty,subst,metasenv) =
+   function
+      [] -> resty,subst,metasenv
+    | (arg,argty)::tl ->
+       let args' =
+        List.map
+         (function
+             None -> assert false
+           | Some t -> Some (CicMetaSubst.lift subst 1 t)
+         ) args in
+       let argty' = CicMetaSubst.lift subst (List.length args) argty in
+       let name =
+        (* The name must be fresh for (context'@context).      *)
+        (* Nevertheless, argty is well-typed only in context.  *)
+        (* Thus I generate a name (name_hint) in context and   *)
+        (* then I generate a name --- using the hint name_hint *)
+        (* --- that is fresh in (context'@context).            *)
+        let name_hint =
+         FreshNamesGenerator.mk_fresh_name
+          (CicMetaSubst.apply_subst_metasenv subst metasenv)
+          (CicMetaSubst.apply_subst_context subst context)
+          Cic.Anonymous
+          (CicMetaSubst.apply_subst subst argty)
+        in
+         (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
+         FreshNamesGenerator.mk_fresh_name
+          [] (context'@context) name_hint (Cic.Sort Cic.Prop)
+       in
+       let context'' = Some (name, Cic.Decl argty') :: context' in
+       let (metasenv, idx) =
+        CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
+       let irl =
+         (Some (Cic.Rel 1))::args' @
+          (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
+            context)
+       in
+       let newmeta = Cic.Meta (idx, irl) in
+       let prod = Cic.Prod (name, argty, newmeta) in
+       let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
+       let (subst, metasenv) =
+         fo_unif_subst subst context metasenv resty prod
+       in
+        aux context'' (Some arg :: args)
+         (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
+  in
+   aux [] [] (hetype,subst,metasenv) tlbody_and_type
+*)
  in
   let ty,subst',metasenv' =
    type_of_aux [] metasenv context t
   in
-   let subst'',metasenv'' = CicMetaSubst.unwind_subst metasenv' subst' in
-   (* we get rid of the metavariables that have been instantiated *)
-   let metasenv''' =
-    List.filter
-     (function (i,_,_) -> not (List.exists (function (j,_) -> j=i) subst''))
-     metasenv''
+   let substituted_t = CicMetaSubst.apply_subst subst' t in
+   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
+   let substituted_metasenv =
+    CicMetaSubst.apply_subst_metasenv subst' metasenv'
    in
-    CicMetaSubst.apply_subst subst'' t,
-     CicMetaSubst.apply_subst subst'' ty,
-      subst'', metasenv'''
+    let cleaned_t =
+     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
+    let cleaned_ty =
+     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
+    let cleaned_metasenv =
+     List.map
+      (function (n,context,ty) ->
+        let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
+        let context' =
+         List.map
+          (function
+              None -> None
+            | Some (n, Cic.Decl t) ->
+               Some (n,
+                Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
+            | Some (n, Cic.Def (bo,ty)) ->
+               let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
+               let ty' =
+                match ty with
+                   None -> None
+                 | Some ty ->
+                    Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
+               in
+                Some (n, Cic.Def (bo',ty'))
+          ) context
+        in
+         (n,context',ty')
+      ) substituted_metasenv
+    in
+     (cleaned_t,cleaned_ty,cleaned_metasenv)
+
 ;;
 
 (* DEBUGGING ONLY *)
 let type_of_aux' metasenv context term =
  try
-  let (t,ty,s,m) = type_of_aux' metasenv context term in
+  let (t,ty,m) = type_of_aux' metasenv context term in
+   debug_print
+    ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
 (*
-   List.iter
-    (function (i,t) ->
-      debug_print ("+ ?" ^ string_of_int i ^ " := " ^ CicPp.ppterm t)) s ;
-   List.iter
-    (function (i,_,t) ->
-      debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t)) m ;
-*)
    debug_print
-    ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty) ;
-   (t,ty,s,m)
+    ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
+*)
+   (t,ty,m)
  with
- | CicUnification.AssertFailure msg as e ->
-     debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
-     debug_print msg;
+ | RefineFailure msg as e ->
+     debug_print ("@@@ REFINE FAILED: " ^ msg);
      raise e
- | CicUnification.UnificationFailure msg as e ->
-     debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
-     debug_print msg;
+ | Uncertain msg as e ->
+     debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
      raise e
- | e ->
-(*
-   List.iter
-    (function (i,_,t) ->
-      debug_print ("+ ?" ^ string_of_int i ^ " : " ^ CicPp.ppterm t))
-    metasenv ;
-*)
-   debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
-   raise e
 ;;
-