helm/ocaml/cic_unification/cicRefine.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 open Printf
  27
  28 exception RefineFailure of string;;
  29 exception Uncertain of string;;
  30 exception AssertFailure of string;;
  31
  32 let debug_print = prerr_endline
  33
  34 let fo_unif_subst subst context metasenv t1 t2 =
  35  try
  36   CicUnification.fo_unif_subst subst context metasenv t1 t2
  37  with
  38     (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg)
  39   | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
  40 ;;
  41
  42 let rec split l n =
  43  match (l,n) with
  44     (l,0) -> ([], l)
  45   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  46   | (_,_) -> raise (AssertFailure "split: list too short")
  47 ;;
  48
  49 let rec type_of_constant uri =
  50  let module C = Cic in
  51  let module R = CicReduction in
  52  let module U = UriManager in
  53   match CicEnvironment.get_cooked_obj uri with
  54      C.Constant (_,_,ty,_) -> ty
  55    | C.CurrentProof (_,_,_,ty,_) -> ty
  56    | _ ->
  57      raise
  58       (RefineFailure ("Unknown constant definition " ^  U.string_of_uri uri))
  59
  60 and type_of_variable uri =
  61  let module C = Cic in
  62  let module R = CicReduction in
  63  let module U = UriManager in
  64   match CicEnvironment.get_cooked_obj uri with
  65      C.Variable (_,_,ty,_) -> ty
  66    |  _ ->
  67       raise
  68        (RefineFailure
  69          ("Unknown variable definition " ^ UriManager.string_of_uri uri))
  70
  71 and type_of_mutual_inductive_defs uri i =
  72  let module C = Cic in
  73  let module R = CicReduction in
  74  let module U = UriManager in
  75   match CicEnvironment.get_cooked_obj uri with
  76      C.InductiveDefinition (dl,_,_) ->
  77       let (_,_,arity,_) = List.nth dl i in
  78        arity
  79    | _ ->
  80      raise
  81       (RefineFailure
  82         ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
  83
  84 and type_of_mutual_inductive_constr uri i j =
  85  let module C = Cic in
  86  let module R = CicReduction in
  87  let module U = UriManager in
  88   match CicEnvironment.get_cooked_obj uri with
  89       C.InductiveDefinition (dl,_,_) ->
  90        let (_,_,_,cl) = List.nth dl i in
  91         let (_,ty) = List.nth cl (j-1) in
  92          ty
  93    | _ ->
  94      raise
  95       (RefineFailure
  96         ("Unkown mutual inductive definition " ^ U.string_of_uri uri))
  97
  98 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
  99
 100 (* the check_branch function checks if a branch of a case is refinable.
 101    It returns a pair (outype_instance,args), a subst and a metasenv.
 102    outype_instance is the expected result of applying the case outtype
 103    to args.
 104    The problem is that outype is in general unknown, and we should
 105    try to synthesize it from the above information, that is in general
 106    a second order unification problem. *)
 107
 108 and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
 109   let module C = Cic in
 110   let module R = CicMetaSubst in
 111   match R.whd subst context expectedtype with
 112      C.MutInd (_,_,_) ->
 113        (n,context,actualtype, [term]), subst, metasenv
 114    | C.Appl (C.MutInd (_,_,_)::tl) ->
 115        let (_,arguments) = split tl left_args_no in
 116        (n,context,actualtype, arguments@[term]), subst, metasenv
 117    | C.Prod (name,so,de) ->
 118       (* we expect that the actual type of the branch has the due
 119          number of Prod *)
 120       (match R.whd subst context actualtype with
 121            C.Prod (name',so',de') ->
 122              let subst, metasenv =
 123                fo_unif_subst subst context metasenv so so' in
 124              let term' =
 125                (match CicSubstitution.lift 1 term with
 126                    C.Appl l -> C.Appl (l@[C.Rel 1])
 127                  | t -> C.Appl [t ; C.Rel 1]) in
 128              (* we should also check that the name variable is anonymous in
 129              the actual type de' ?? *)
 130              check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de
 131         | _ -> raise (AssertFailure "Wrong number of arguments"))
 132    | _ -> raise (AssertFailure "Prod or MutInd expected")
 133
 134 and type_of_aux' metasenv context t =
 135  let rec type_of_aux subst metasenv context =
 136   let module C = Cic in
 137   let module S = CicSubstitution in
 138   let module U = UriManager in
 139    function
 140       C.Rel n ->
 141        (try
 142          match List.nth context (n - 1) with
 143             Some (_,C.Decl t) -> S.lift n t,subst,metasenv
 144           | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
 145           | Some (_,C.Def (bo,None)) ->
 146              type_of_aux subst metasenv context (S.lift n bo)
 147           | None -> raise (RefineFailure "Rel to hidden hypothesis")
 148         with
 149          _ -> raise (RefineFailure "Not a close term")
 150        )
 151     | C.Var (uri,exp_named_subst) ->
 152       let subst',metasenv' =
 153        check_exp_named_subst subst metasenv context exp_named_subst in
 154       let ty =
 155        CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
 156       in
 157        ty,subst',metasenv'
 158     | C.Meta (n,l) ->
 159        let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
 160         let subst',metasenv' =
 161          check_metasenv_consistency n subst metasenv context canonical_context l
 162         in
 163         CicSubstitution.lift_meta l ty, subst', metasenv'
 164     | C.Sort s ->
 165        C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
 166         subst,metasenv
 167     | C.Implicit _ -> raise (AssertFailure "21")
 168     | C.Cast (te,ty) ->
 169        let _,subst',metasenv' =
 170         type_of_aux subst metasenv context ty in
 171        let inferredty,subst'',metasenv'' =
 172         type_of_aux subst' metasenv' context te
 173        in
 174         (try
 175           let subst''',metasenv''' =
 176            fo_unif_subst subst'' context metasenv'' inferredty ty
 177           in
 178            ty,subst''',metasenv'''
 179          with
 180           _ -> raise (RefineFailure "Cast"))
 181     | C.Prod (name,s,t) ->
 182        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
 183        let sort2,subst'',metasenv'' =
 184         type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
 185        in
 186         sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
 187    | C.Lambda (n,s,t) ->
 188        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
 189        (match CicMetaSubst.whd subst' context sort1 with
 190            C.Meta _
 191          | C.Sort _ -> ()
 192          | _ ->
 193            raise (RefineFailure (sprintf
 194             "Not well-typed lambda-abstraction: the source %s should be a type;
 195              instead it is a term of type %s" (CicPp.ppterm s)
 196             (CicPp.ppterm sort1)))
 197        ) ;
 198        let type2,subst'',metasenv'' =
 199         type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
 200        in
 201           C.Prod (n,s,type2),subst'',metasenv''
 202    | C.LetIn (n,s,t) ->
 203       (* only to check if s is well-typed *)
 204       let ty,subst',metasenv' = type_of_aux subst metasenv context s in
 205       let inferredty,subst'',metasenv'' =
 206        type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
 207       in
 208        (* One-step LetIn reduction. Even faster than the previous solution.
 209           Moreover the inferred type is closer to the expected one. *)
 210        CicSubstitution.subst s inferredty,subst',metasenv'
 211    | C.Appl (he::tl) when List.length tl > 0 ->
 212       let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
 213       let tlbody_and_type,subst'',metasenv'' =
 214        List.fold_right
 215         (fun x (res,subst,metasenv) ->
 216           let ty,subst',metasenv' =
 217            type_of_aux subst metasenv context x
 218           in
 219            (x, ty)::res,subst',metasenv'
 220         ) tl ([],subst',metasenv')
 221       in
 222        eat_prods subst'' metasenv'' context hetype tlbody_and_type
 223    | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
 224    | C.Const (uri,exp_named_subst) ->
 225       let subst',metasenv' =
 226        check_exp_named_subst subst metasenv context exp_named_subst in
 227       let cty =
 228        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
 229       in
 230        cty,subst',metasenv'
 231    | C.MutInd (uri,i,exp_named_subst) ->
 232       let subst',metasenv' =
 233        check_exp_named_subst subst metasenv context exp_named_subst in
 234       let cty =
 235        CicSubstitution.subst_vars exp_named_subst
 236         (type_of_mutual_inductive_defs uri i)
 237       in
 238        cty,subst',metasenv'
 239    | C.MutConstruct (uri,i,j,exp_named_subst) ->
 240       let subst',metasenv' =
 241        check_exp_named_subst subst metasenv context exp_named_subst in
 242       let cty =
 243        CicSubstitution.subst_vars exp_named_subst
 244         (type_of_mutual_inductive_constr uri i j)
 245       in
 246        cty,subst',metasenv'
 247    | C.MutCase (uri, i, outtype, term, pl) ->
 248        (* first, get the inductive type (and noparams) in the environment  *)
 249        let (_,b,arity,constructors), expl_params, no_left_params =
 250          match CicEnvironment.get_cooked_obj ~trust:true uri with
 251             C.InductiveDefinition (l,expl_params,parsno) ->
 252               List.nth l i , expl_params, parsno
 253           | _ ->
 254             raise
 255              (RefineFailure
 256               ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
 257        let rec count_prod t =
 258          match CicMetaSubst.whd subst context t with
 259              C.Prod (_, _, t) -> 1 + (count_prod t)
 260            | _ -> 0 in
 261        let no_args = count_prod arity in
 262        (* now, create a "generic" MutInd *)
 263        let metasenv,left_args =
 264          CicMkImplicit.n_fresh_metas metasenv context no_left_params in
 265        let metasenv,right_args =
 266          let no_right_params = no_args - no_left_params in
 267          if no_right_params < 0 then assert false
 268          else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
 269        let metasenv,exp_named_subst =
 270          CicMkImplicit.fresh_subst metasenv context expl_params in
 271        let expected_type =
 272          if no_args = 0 then
 273            C.MutInd (uri,i,exp_named_subst)
 274          else
 275            C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 276        in
 277        (* check consistency with the actual type of term *)
 278        let actual_type,subst,metasenv =
 279          type_of_aux subst metasenv context term in
 280        let _, subst, metasenv =
 281          type_of_aux subst metasenv context expected_type
 282        in
 283        let actual_type = CicMetaSubst.whd subst context actual_type in
 284        let subst,metasenv =
 285          fo_unif_subst subst context metasenv expected_type actual_type
 286        in
 287        (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
 288        let (_,outtypeinstances,subst,metasenv) =
 289           List.fold_left
 290            (fun (j,outtypeinstances,subst,metasenv) p ->
 291              let constructor =
 292               if left_args = [] then
 293                (C.MutConstruct (uri,i,j,exp_named_subst))
 294               else
 295                (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 296              in
 297              let actual_type,subst,metasenv =
 298                type_of_aux subst metasenv context p in
 299              let expected_type, subst, metasenv =
 300                type_of_aux subst metasenv context constructor in
 301              let outtypeinstance,subst,metasenv =
 302                check_branch
 303                 0 context metasenv subst
 304                 no_left_params actual_type constructor expected_type in
 305              (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
 306             (1,[],subst,metasenv) pl in
 307         (* we are left to check that the outype matches his instances.
 308            The easy case is when the outype is specified, that amount
 309            to a trivial check. Otherwise, we should guess a type from
 310            its instances *)
 311
 312         (* easy case *)
 313         let _, subst, metasenv =
 314           type_of_aux subst metasenv context
 315             (C.Appl ((outtype :: right_args) @ [term]))
 316         in
 317         let (subst,metasenv) =
 318           List.fold_left
 319             (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
 320               let instance' =
 321                 let appl =
 322                   let outtype' =
 323                     CicSubstitution.lift constructor_args_no outtype
 324                   in
 325                   C.Appl (outtype'::args)
 326                 in
 327 (*
 328                 (* if appl is not well typed then the type_of below solves the
 329                  * problem *)
 330                 let (_, subst, metasenv) =
 331                   type_of_aux subst metasenv context appl
 332                 in
 333 *)
 334                 CicMetaSubst.whd subst context appl
 335               in
 336                fo_unif_subst subst context metasenv instance instance')
 337              (subst,metasenv) outtypeinstances in
 338         CicMetaSubst.whd subst
 339           context (C.Appl(outtype::right_args@[term])),subst,metasenv
 340    | C.Fix (i,fl) ->
 341       let subst,metasenv,types =
 342        List.fold_left
 343         (fun (subst,metasenv,types) (n,_,ty,_) ->
 344           let _,subst',metasenv' = type_of_aux subst metasenv context ty in
 345            subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
 346         ) (subst,metasenv,[]) fl
 347       in
 348        let len = List.length types in
 349        let context' = types@context in
 350        let subst,metasenv =
 351         List.fold_left
 352          (fun (subst,metasenv) (name,x,ty,bo) ->
 353            let ty_of_bo,subst,metasenv =
 354             type_of_aux subst metasenv context' bo
 355            in
 356             fo_unif_subst subst context' metasenv
 357               ty_of_bo (CicMetaSubst.lift subst len ty)
 358          ) (subst,metasenv) fl in
 359         let (_,_,ty,_) = List.nth fl i in
 360          ty,subst,metasenv
 361    | C.CoFix (i,fl) ->
 362       let subst,metasenv,types =
 363        List.fold_left
 364         (fun (subst,metasenv,types) (n,ty,_) ->
 365           let _,subst',metasenv' = type_of_aux subst metasenv context ty in
 366            subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
 367         ) (subst,metasenv,[]) fl
 368       in
 369        let len = List.length types in
 370        let context' = types@context in
 371        let subst,metasenv =
 372         List.fold_left
 373          (fun (subst,metasenv) (name,ty,bo) ->
 374            let ty_of_bo,subst,metasenv =
 375             type_of_aux subst metasenv context' bo
 376            in
 377             fo_unif_subst subst context' metasenv
 378               ty_of_bo (CicMetaSubst.lift subst len ty)
 379          ) (subst,metasenv) fl in
 380
 381         let (_,ty,_) = List.nth fl i in
 382          ty,subst,metasenv
 383
 384  (* check_metasenv_consistency checks that the "canonical" context of a
 385  metavariable is consitent - up to relocation via the relocation list l -
 386  with the actual context *)
 387  and check_metasenv_consistency
 388   metano subst metasenv context canonical_context l
 389  =
 390    let module C = Cic in
 391    let module R = CicReduction in
 392    let module S = CicSubstitution in
 393     let lifted_canonical_context =
 394      let rec aux i =
 395       function
 396          [] -> []
 397        | (Some (n,C.Decl t))::tl ->
 398           (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
 399        | (Some (n,C.Def (t,None)))::tl ->
 400           (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 401        | None::tl -> None::(aux (i+1) tl)
 402        | (Some (n,C.Def (t,Some ty)))::tl ->
 403            (Some (n,
 404             C.Def ((S.lift_meta l (S.lift i t)),
 405               Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
 406      in
 407       aux 1 canonical_context
 408     in
 409     try
 410      List.fold_left2
 411       (fun (subst,metasenv) t ct ->
 412         match (t,ct) with
 413            _,None ->
 414              subst,metasenv
 415          | Some t,Some (_,C.Def (ct,_)) ->
 416             (try
 417               fo_unif_subst subst context metasenv t ct
 418              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)))))
 419          | Some t,Some (_,C.Decl ct) ->
 420             let inferredty,subst',metasenv' =
 421              type_of_aux subst metasenv context t
 422             in
 423              (try
 424                fo_unif_subst
 425                 subst' context metasenv' inferredty ct
 426              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)))))
 427          | None, Some _  ->
 428              raise (RefineFailure (sprintf
 429               "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"
 430               (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 431               (CicMetaSubst.ppcontext subst canonical_context)))
 432       ) (subst,metasenv) l lifted_canonical_context
 433     with
 434      Invalid_argument _ ->
 435       raise
 436        (RefineFailure
 437          (sprintf
 438            "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
 439              (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 440              (CicMetaSubst.ppcontext subst canonical_context)))
 441
 442  and check_exp_named_subst metasubst metasenv context =
 443   let rec check_exp_named_subst_aux metasubst metasenv substs =
 444    function
 445       [] -> metasubst,metasenv
 446     | ((uri,t) as subst)::tl ->
 447        let typeofvar =
 448         CicSubstitution.subst_vars substs (type_of_variable uri) in
 449        (match CicEnvironment.get_cooked_obj ~trust:false uri with
 450            Cic.Variable (_,Some bo,_,_) ->
 451             raise
 452              (RefineFailure
 453                "A variable with a body can not be explicit substituted")
 454          | Cic.Variable (_,None,_,_) -> ()
 455          | _ ->
 456            raise
 457             (RefineFailure
 458              ("Unkown variable definition " ^ UriManager.string_of_uri uri))
 459        ) ;
 460        let typeoft,metasubst',metasenv' =
 461         type_of_aux metasubst metasenv context t
 462        in
 463         try
 464          let metasubst'',metasenv'' =
 465           fo_unif_subst metasubst' context metasenv' typeoft typeofvar
 466          in
 467           check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
 468         with _ ->
 469          raise (RefineFailure "Wrong Explicit Named Substitution")
 470   in
 471    check_exp_named_subst_aux metasubst metasenv []
 472
 473  and sort_of_prod subst metasenv context (name,s) (t1, t2) =
 474   let module C = Cic in
 475     let context_for_t2 = (Some (name,C.Decl s))::context in
 476     let t1'' = CicMetaSubst.whd subst context t1 in
 477     let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in
 478     match (t1'', t2'') with
 479        (C.Sort s1, C.Sort s2)
 480          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
 481           C.Sort s2,subst,metasenv
 482      | (C.Sort s1, C.Sort s2) ->
 483          (*CSC manca la gestione degli universi!!! *)
 484          C.Sort C.Type,subst,metasenv
 485      | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
 486      | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
 487          (* TODO how can we force the meta to become a sort? If we don't we
 488           * brake the invariant that refine produce only well typed terms *)
 489          (* TODO if we check the non meta term and if it is a sort then we are
 490           * likely to know the exact value of the result e.g. if the rhs is a
 491           * Sort (Prop | Set | CProp) then the result is the rhs *)
 492          let (metasenv,idx) =
 493           CicMkImplicit.mk_implicit_sort metasenv in
 494          let (subst, metasenv) =
 495            fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
 496          in
 497           t2'',subst,metasenv
 498      | (_,_) ->
 499          raise (RefineFailure (sprintf
 500           "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
 501           (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
 502           (CicPp.ppterm t2'')))
 503
 504  and eat_prods subst metasenv context hetype tlbody_and_type =
 505  let rec mk_prod metasenv context =
 506   function
 507      [] ->
 508        let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
 509        let irl =
 510         CicMkImplicit.identity_relocation_list_for_metavariable context
 511        in
 512         metasenv,Cic.Meta (idx, irl)
 513    | (_,argty)::tl ->
 514       let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
 515       let irl =
 516        CicMkImplicit.identity_relocation_list_for_metavariable context
 517       in
 518        let meta = Cic.Meta (idx,irl) in
 519        let name =
 520         (* The name must be fresh for context.                 *)
 521         (* Nevertheless, argty is well-typed only in context.  *)
 522         (* Thus I generate a name (name_hint) in context and   *)
 523         (* then I generate a name --- using the hint name_hint *)
 524         (* --- that is fresh in (context'@context).            *)
 525         let name_hint =
 526          FreshNamesGenerator.mk_fresh_name
 527           (CicMetaSubst.apply_subst_metasenv subst metasenv)
 528           (CicMetaSubst.apply_subst_context subst context)
 529           Cic.Anonymous
 530           (CicMetaSubst.apply_subst subst argty)
 531         in
 532          (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
 533          FreshNamesGenerator.mk_fresh_name
 534           [] context name_hint (Cic.Sort Cic.Prop)
 535        in
 536        let metasenv,target =
 537         mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
 538        in
 539         metasenv,Cic.Prod (name,meta,target)
 540  in
 541   let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
 542   let (subst, metasenv) =
 543    fo_unif_subst subst context metasenv hetype hetype'
 544   in
 545    let rec eat_prods metasenv subst context hetype =
 546       function
 547          [] -> metasenv,subst,hetype
 548        | (hete, hety)::tl ->
 549         (match hetype with
 550             Cic.Prod (n,s,t) ->
 551               let subst,metasenv =
 552                fo_unif_subst subst context metasenv hety s
 553               in
 554                eat_prods metasenv subst context
 555                 (CicMetaSubst.subst subst hete t) tl
 556           | _ -> assert false
 557         )
 558    in
 559     let metasenv,subst,t =
 560      eat_prods metasenv subst context hetype' tlbody_and_type
 561     in
 562      t,subst,metasenv
 563 (*
 564   let rec aux context' args (resty,subst,metasenv) =
 565    function
 566       [] -> resty,subst,metasenv
 567     | (arg,argty)::tl ->
 568        let args' =
 569         List.map
 570          (function
 571              None -> assert false
 572            | Some t -> Some (CicMetaSubst.lift subst 1 t)
 573          ) args in
 574        let argty' = CicMetaSubst.lift subst (List.length args) argty in
 575        let name =
 576         (* The name must be fresh for (context'@context).      *)
 577         (* Nevertheless, argty is well-typed only in context.  *)
 578         (* Thus I generate a name (name_hint) in context and   *)
 579         (* then I generate a name --- using the hint name_hint *)
 580         (* --- that is fresh in (context'@context).            *)
 581         let name_hint =
 582          FreshNamesGenerator.mk_fresh_name
 583           (CicMetaSubst.apply_subst_metasenv subst metasenv)
 584           (CicMetaSubst.apply_subst_context subst context)
 585           Cic.Anonymous
 586           (CicMetaSubst.apply_subst subst argty)
 587         in
 588          (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
 589          FreshNamesGenerator.mk_fresh_name
 590           [] (context'@context) name_hint (Cic.Sort Cic.Prop)
 591        in
 592        let context'' = Some (name, Cic.Decl argty') :: context' in
 593        let (metasenv, idx) =
 594         CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
 595        let irl =
 596          (Some (Cic.Rel 1))::args' @
 597           (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
 598             context)
 599        in
 600        let newmeta = Cic.Meta (idx, irl) in
 601        let prod = Cic.Prod (name, argty, newmeta) in
 602        let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
 603        let (subst, metasenv) =
 604          fo_unif_subst subst context metasenv resty prod
 605        in
 606         aux context'' (Some arg :: args)
 607          (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
 608   in
 609    aux [] [] (hetype,subst,metasenv) tlbody_and_type
 610 *)
 611  in
 612   let ty,subst',metasenv' =
 613    type_of_aux [] metasenv context t
 614   in
 615    let substituted_t = CicMetaSubst.apply_subst subst' t in
 616    let substituted_ty = CicMetaSubst.apply_subst subst' ty in
 617    let substituted_metasenv =
 618     CicMetaSubst.apply_subst_metasenv subst' metasenv'
 619    in
 620     let cleaned_t =
 621      FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
 622     let cleaned_ty =
 623      FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
 624     let cleaned_metasenv =
 625      List.map
 626       (function (n,context,ty) ->
 627         let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
 628         let context' =
 629          List.map
 630           (function
 631               None -> None
 632             | Some (n, Cic.Decl t) ->
 633                Some (n,
 634                 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
 635             | Some (n, Cic.Def (bo,ty)) ->
 636                let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
 637                let ty' =
 638                 match ty with
 639                    None -> None
 640                  | Some ty ->
 641                     Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
 642                in
 643                 Some (n, Cic.Def (bo',ty'))
 644           ) context
 645         in
 646          (n,context',ty')
 647       ) substituted_metasenv
 648     in
 649      (cleaned_t,cleaned_ty,cleaned_metasenv)
 650
 651 ;;
 652
 653 (* DEBUGGING ONLY *)
 654 let type_of_aux' metasenv context term =
 655  try
 656   let (t,ty,m) = type_of_aux' metasenv context term in
 657    debug_print
 658     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
 659 (*
 660    debug_print
 661     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
 662 *)
 663    (t,ty,m)
 664  with
 665  | RefineFailure msg as e ->
 666      debug_print ("@@@ REFINE FAILED: " ^ msg);
 667      raise e
 668  | Uncertain msg as e ->
 669      debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
 670      raise e
 671 ;;