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      (* TASSI: CONSTRAINT *)
 165     | C.Sort (C.Type t) ->
 166         let t' = CicUniv.fresh() in
 167         if not (CicUniv.add_gt t' t ) then
 168           assert false (* t' is fresh! an error in CicUniv *)
 169         else
 170           C.Sort (C.Type t'),subst,metasenv
 171      (* TASSI: CONSTRAINT *)
 172     | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())),subst,metasenv
 173     | C.Implicit _ -> raise (AssertFailure "21")
 174     | C.Cast (te,ty) ->
 175        let _,subst',metasenv' =
 176         type_of_aux subst metasenv context ty in
 177        let inferredty,subst'',metasenv'' =
 178         type_of_aux subst' metasenv' context te
 179        in
 180         (try
 181           let subst''',metasenv''' =
 182            fo_unif_subst subst'' context metasenv'' inferredty ty
 183           in
 184            ty,subst''',metasenv'''
 185          with
 186           _ -> raise (RefineFailure "Cast"))
 187     | C.Prod (name,s,t) ->
 188        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
 189        let sort2,subst'',metasenv'' =
 190         type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
 191        in
 192         sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
 193    | C.Lambda (n,s,t) ->
 194        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
 195        (match CicMetaSubst.whd subst' context sort1 with
 196            C.Meta _
 197          | C.Sort _ -> ()
 198          | _ ->
 199            raise (RefineFailure (sprintf
 200             "Not well-typed lambda-abstraction: the source %s should be a type;
 201              instead it is a term of type %s" (CicPp.ppterm s)
 202             (CicPp.ppterm sort1)))
 203        ) ;
 204        let type2,subst'',metasenv'' =
 205         type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
 206        in
 207           C.Prod (n,s,type2),subst'',metasenv''
 208    | C.LetIn (n,s,t) ->
 209       (* only to check if s is well-typed *)
 210       let ty,subst',metasenv' = type_of_aux subst metasenv context s in
 211       let inferredty,subst'',metasenv'' =
 212        type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
 213       in
 214        (* One-step LetIn reduction. Even faster than the previous solution.
 215           Moreover the inferred type is closer to the expected one. *)
 216        CicSubstitution.subst s inferredty,subst',metasenv'
 217    | C.Appl (he::tl) when List.length tl > 0 ->
 218       let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
 219       let tlbody_and_type,subst'',metasenv'' =
 220        List.fold_right
 221         (fun x (res,subst,metasenv) ->
 222           let ty,subst',metasenv' =
 223            type_of_aux subst metasenv context x
 224           in
 225            (x, ty)::res,subst',metasenv'
 226         ) tl ([],subst',metasenv')
 227       in
 228        eat_prods subst'' metasenv'' context hetype tlbody_and_type
 229    | C.Appl _ -> raise (RefineFailure "Appl: no arguments")
 230    | C.Const (uri,exp_named_subst) ->
 231       let subst',metasenv' =
 232        check_exp_named_subst subst metasenv context exp_named_subst in
 233       let cty =
 234        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
 235       in
 236        cty,subst',metasenv'
 237    | C.MutInd (uri,i,exp_named_subst) ->
 238       let subst',metasenv' =
 239        check_exp_named_subst subst metasenv context exp_named_subst in
 240       let cty =
 241        CicSubstitution.subst_vars exp_named_subst
 242         (type_of_mutual_inductive_defs uri i)
 243       in
 244        cty,subst',metasenv'
 245    | C.MutConstruct (uri,i,j,exp_named_subst) ->
 246       let subst',metasenv' =
 247        check_exp_named_subst subst metasenv context exp_named_subst in
 248       let cty =
 249        CicSubstitution.subst_vars exp_named_subst
 250         (type_of_mutual_inductive_constr uri i j)
 251       in
 252        cty,subst',metasenv'
 253    | C.MutCase (uri, i, outtype, term, pl) ->
 254        (* first, get the inductive type (and noparams) in the environment  *)
 255        let (_,b,arity,constructors), expl_params, no_left_params =
 256          match CicEnvironment.get_cooked_obj ~trust:true uri with
 257             C.InductiveDefinition (l,expl_params,parsno) ->
 258               List.nth l i , expl_params, parsno
 259           | _ ->
 260             raise
 261              (RefineFailure
 262               ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
 263        let rec count_prod t =
 264          match CicMetaSubst.whd subst context t with
 265              C.Prod (_, _, t) -> 1 + (count_prod t)
 266            | _ -> 0 in
 267        let no_args = count_prod arity in
 268        (* now, create a "generic" MutInd *)
 269        let metasenv,left_args =
 270          CicMkImplicit.n_fresh_metas metasenv context no_left_params in
 271        let metasenv,right_args =
 272          let no_right_params = no_args - no_left_params in
 273          if no_right_params < 0 then assert false
 274          else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
 275        let metasenv,exp_named_subst =
 276          CicMkImplicit.fresh_subst metasenv context expl_params in
 277        let expected_type =
 278          if no_args = 0 then
 279            C.MutInd (uri,i,exp_named_subst)
 280          else
 281            C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 282        in
 283        (* check consistency with the actual type of term *)
 284        let actual_type,subst,metasenv =
 285          type_of_aux subst metasenv context term in
 286        let _, subst, metasenv =
 287          type_of_aux subst metasenv context expected_type
 288        in
 289        let actual_type = CicMetaSubst.whd subst context actual_type in
 290        let subst,metasenv =
 291          fo_unif_subst subst context metasenv expected_type actual_type
 292        in
 293        (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
 294        let (_,outtypeinstances,subst,metasenv) =
 295           List.fold_left
 296            (fun (j,outtypeinstances,subst,metasenv) p ->
 297              let constructor =
 298               if left_args = [] then
 299                (C.MutConstruct (uri,i,j,exp_named_subst))
 300               else
 301                (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 302              in
 303              let actual_type,subst,metasenv =
 304                type_of_aux subst metasenv context p in
 305              let expected_type, subst, metasenv =
 306                type_of_aux subst metasenv context constructor in
 307              let outtypeinstance,subst,metasenv =
 308                check_branch
 309                 0 context metasenv subst
 310                 no_left_params actual_type constructor expected_type in
 311              (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
 312             (1,[],subst,metasenv) pl in
 313         (* we are left to check that the outype matches his instances.
 314            The easy case is when the outype is specified, that amount
 315            to a trivial check. Otherwise, we should guess a type from
 316            its instances *)
 317
 318         (* easy case *)
 319         let _, subst, metasenv =
 320           type_of_aux subst metasenv context
 321             (C.Appl ((outtype :: right_args) @ [term]))
 322         in
 323         let (subst,metasenv) =
 324           List.fold_left
 325             (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
 326               let instance' =
 327                 let appl =
 328                   let outtype' =
 329                     CicSubstitution.lift constructor_args_no outtype
 330                   in
 331                   C.Appl (outtype'::args)
 332                 in
 333 (*
 334                 (* if appl is not well typed then the type_of below solves the
 335                  * problem *)
 336                 let (_, subst, metasenv) =
 337                   type_of_aux subst metasenv context appl
 338                 in
 339 *)
 340                 CicMetaSubst.whd subst context appl
 341               in
 342                fo_unif_subst subst context metasenv instance instance')
 343              (subst,metasenv) outtypeinstances in
 344         CicMetaSubst.whd subst
 345           context (C.Appl(outtype::right_args@[term])),subst,metasenv
 346    | C.Fix (i,fl) ->
 347       let subst,metasenv,types =
 348        List.fold_left
 349         (fun (subst,metasenv,types) (n,_,ty,_) ->
 350           let _,subst',metasenv' = type_of_aux subst metasenv context ty in
 351            subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
 352         ) (subst,metasenv,[]) fl
 353       in
 354        let len = List.length types in
 355        let context' = types@context in
 356        let subst,metasenv =
 357         List.fold_left
 358          (fun (subst,metasenv) (name,x,ty,bo) ->
 359            let ty_of_bo,subst,metasenv =
 360             type_of_aux subst metasenv context' bo
 361            in
 362             fo_unif_subst subst context' metasenv
 363               ty_of_bo (CicMetaSubst.lift subst len ty)
 364          ) (subst,metasenv) fl in
 365         let (_,_,ty,_) = List.nth fl i in
 366          ty,subst,metasenv
 367    | C.CoFix (i,fl) ->
 368       let subst,metasenv,types =
 369        List.fold_left
 370         (fun (subst,metasenv,types) (n,ty,_) ->
 371           let _,subst',metasenv' = type_of_aux subst metasenv context ty in
 372            subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
 373         ) (subst,metasenv,[]) fl
 374       in
 375        let len = List.length types in
 376        let context' = types@context in
 377        let subst,metasenv =
 378         List.fold_left
 379          (fun (subst,metasenv) (name,ty,bo) ->
 380            let ty_of_bo,subst,metasenv =
 381             type_of_aux subst metasenv context' bo
 382            in
 383             fo_unif_subst subst context' metasenv
 384               ty_of_bo (CicMetaSubst.lift subst len ty)
 385          ) (subst,metasenv) fl in
 386
 387         let (_,ty,_) = List.nth fl i in
 388          ty,subst,metasenv
 389
 390  (* check_metasenv_consistency checks that the "canonical" context of a
 391  metavariable is consitent - up to relocation via the relocation list l -
 392  with the actual context *)
 393  and check_metasenv_consistency
 394   metano subst metasenv context canonical_context l
 395  =
 396    let module C = Cic in
 397    let module R = CicReduction in
 398    let module S = CicSubstitution in
 399     let lifted_canonical_context =
 400      let rec aux i =
 401       function
 402          [] -> []
 403        | (Some (n,C.Decl t))::tl ->
 404           (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
 405        | (Some (n,C.Def (t,None)))::tl ->
 406           (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 407        | None::tl -> None::(aux (i+1) tl)
 408        | (Some (n,C.Def (t,Some ty)))::tl ->
 409            (Some (n,
 410             C.Def ((S.lift_meta l (S.lift i t)),
 411               Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
 412      in
 413       aux 1 canonical_context
 414     in
 415     try
 416      List.fold_left2
 417       (fun (subst,metasenv) t ct ->
 418         match (t,ct) with
 419            _,None ->
 420              subst,metasenv
 421          | Some t,Some (_,C.Def (ct,_)) ->
 422             (try
 423               fo_unif_subst subst context metasenv t ct
 424              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)))))
 425          | Some t,Some (_,C.Decl ct) ->
 426             let inferredty,subst',metasenv' =
 427              type_of_aux subst metasenv context t
 428             in
 429              (try
 430                fo_unif_subst
 431                 subst' context metasenv' inferredty ct
 432              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)))))
 433          | None, Some _  ->
 434              raise (RefineFailure (sprintf
 435               "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"
 436               (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 437               (CicMetaSubst.ppcontext subst canonical_context)))
 438       ) (subst,metasenv) l lifted_canonical_context
 439     with
 440      Invalid_argument _ ->
 441       raise
 442        (RefineFailure
 443          (sprintf
 444            "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s"
 445              (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 446              (CicMetaSubst.ppcontext subst canonical_context)))
 447
 448  and check_exp_named_subst metasubst metasenv context =
 449   let rec check_exp_named_subst_aux metasubst metasenv substs =
 450    function
 451       [] -> metasubst,metasenv
 452     | ((uri,t) as subst)::tl ->
 453        let typeofvar =
 454         CicSubstitution.subst_vars substs (type_of_variable uri) in
 455        (match CicEnvironment.get_cooked_obj ~trust:false uri with
 456            Cic.Variable (_,Some bo,_,_) ->
 457             raise
 458              (RefineFailure
 459                "A variable with a body can not be explicit substituted")
 460          | Cic.Variable (_,None,_,_) -> ()
 461          | _ ->
 462            raise
 463             (RefineFailure
 464              ("Unkown variable definition " ^ UriManager.string_of_uri uri))
 465        ) ;
 466        let typeoft,metasubst',metasenv' =
 467         type_of_aux metasubst metasenv context t
 468        in
 469         try
 470          let metasubst'',metasenv'' =
 471           fo_unif_subst metasubst' context metasenv' typeoft typeofvar
 472          in
 473           check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
 474         with _ ->
 475          raise (RefineFailure "Wrong Explicit Named Substitution")
 476   in
 477    check_exp_named_subst_aux metasubst metasenv []
 478
 479  and sort_of_prod subst metasenv context (name,s) (t1, t2) =
 480   let module C = Cic in
 481     let context_for_t2 = (Some (name,C.Decl s))::context in
 482     let t1'' = CicMetaSubst.whd subst context t1 in
 483     let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in
 484     match (t1'', t2'') with
 485        (C.Sort s1, C.Sort s2)
 486          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
 487           C.Sort s2,subst,metasenv
 488      | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
 489        (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
 490        let t' = CicUniv.fresh() in
 491        if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
 492          assert false ; (* not possible, error in CicUniv *)
 493        C.Sort (C.Type t'),subst,metasenv
 494      | (C.Sort _,C.Sort (C.Type t1)) ->
 495        (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
 496         C.Sort (C.Type t1),subst,metasenv
 497      | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
 498      | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
 499          (* TODO how can we force the meta to become a sort? If we don't we
 500           * brake the invariant that refine produce only well typed terms *)
 501          (* TODO if we check the non meta term and if it is a sort then we are
 502           * likely to know the exact value of the result e.g. if the rhs is a
 503           * Sort (Prop | Set | CProp) then the result is the rhs *)
 504          let (metasenv,idx) =
 505           CicMkImplicit.mk_implicit_sort metasenv in
 506          let (subst, metasenv) =
 507            fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
 508          in
 509           t2'',subst,metasenv
 510      | (_,_) ->
 511          raise (RefineFailure (sprintf
 512           "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
 513           (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
 514           (CicPp.ppterm t2'')))
 515
 516  and eat_prods subst metasenv context hetype tlbody_and_type =
 517  let rec mk_prod metasenv context =
 518   function
 519      [] ->
 520        let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
 521        let irl =
 522         CicMkImplicit.identity_relocation_list_for_metavariable context
 523        in
 524         metasenv,Cic.Meta (idx, irl)
 525    | (_,argty)::tl ->
 526       let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
 527       let irl =
 528        CicMkImplicit.identity_relocation_list_for_metavariable context
 529       in
 530        let meta = Cic.Meta (idx,irl) in
 531        let name =
 532         (* The name must be fresh for context.                 *)
 533         (* Nevertheless, argty is well-typed only in context.  *)
 534         (* Thus I generate a name (name_hint) in context and   *)
 535         (* then I generate a name --- using the hint name_hint *)
 536         (* --- that is fresh in (context'@context).            *)
 537         let name_hint =
 538          FreshNamesGenerator.mk_fresh_name
 539           (CicMetaSubst.apply_subst_metasenv subst metasenv)
 540           (CicMetaSubst.apply_subst_context subst context)
 541           Cic.Anonymous
 542           (CicMetaSubst.apply_subst subst argty)
 543         in
 544          (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
 545          FreshNamesGenerator.mk_fresh_name
 546           [] context name_hint (Cic.Sort Cic.Prop)
 547        in
 548        let metasenv,target =
 549         mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
 550        in
 551         metasenv,Cic.Prod (name,meta,target)
 552  in
 553   let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
 554   let (subst, metasenv) =
 555    fo_unif_subst subst context metasenv hetype hetype'
 556   in
 557    let rec eat_prods metasenv subst context hetype =
 558       function
 559          [] -> metasenv,subst,hetype
 560        | (hete, hety)::tl ->
 561         (match hetype with
 562             Cic.Prod (n,s,t) ->
 563               let subst,metasenv =
 564                fo_unif_subst subst context metasenv hety s
 565               in
 566                eat_prods metasenv subst context
 567                 (CicMetaSubst.subst subst hete t) tl
 568           | _ -> assert false
 569         )
 570    in
 571     let metasenv,subst,t =
 572      eat_prods metasenv subst context hetype' tlbody_and_type
 573     in
 574      t,subst,metasenv
 575 (*
 576   let rec aux context' args (resty,subst,metasenv) =
 577    function
 578       [] -> resty,subst,metasenv
 579     | (arg,argty)::tl ->
 580        let args' =
 581         List.map
 582          (function
 583              None -> assert false
 584            | Some t -> Some (CicMetaSubst.lift subst 1 t)
 585          ) args in
 586        let argty' = CicMetaSubst.lift subst (List.length args) argty in
 587        let name =
 588         (* The name must be fresh for (context'@context).      *)
 589         (* Nevertheless, argty is well-typed only in context.  *)
 590         (* Thus I generate a name (name_hint) in context and   *)
 591         (* then I generate a name --- using the hint name_hint *)
 592         (* --- that is fresh in (context'@context).            *)
 593         let name_hint =
 594          FreshNamesGenerator.mk_fresh_name
 595           (CicMetaSubst.apply_subst_metasenv subst metasenv)
 596           (CicMetaSubst.apply_subst_context subst context)
 597           Cic.Anonymous
 598           (CicMetaSubst.apply_subst subst argty)
 599         in
 600          (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
 601          FreshNamesGenerator.mk_fresh_name
 602           [] (context'@context) name_hint (Cic.Sort Cic.Prop)
 603        in
 604        let context'' = Some (name, Cic.Decl argty') :: context' in
 605        let (metasenv, idx) =
 606         CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
 607        let irl =
 608          (Some (Cic.Rel 1))::args' @
 609           (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
 610             context)
 611        in
 612        let newmeta = Cic.Meta (idx, irl) in
 613        let prod = Cic.Prod (name, argty, newmeta) in
 614        let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
 615        let (subst, metasenv) =
 616          fo_unif_subst subst context metasenv resty prod
 617        in
 618         aux context'' (Some arg :: args)
 619          (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
 620   in
 621    aux [] [] (hetype,subst,metasenv) tlbody_and_type
 622 *)
 623  in
 624   let ty,subst',metasenv' =
 625    type_of_aux [] metasenv context t
 626   in
 627    let substituted_t = CicMetaSubst.apply_subst subst' t in
 628    let substituted_ty = CicMetaSubst.apply_subst subst' ty in
 629    let substituted_metasenv =
 630     CicMetaSubst.apply_subst_metasenv subst' metasenv'
 631    in
 632     let cleaned_t =
 633      FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
 634     let cleaned_ty =
 635      FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
 636     let cleaned_metasenv =
 637      List.map
 638       (function (n,context,ty) ->
 639         let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
 640         let context' =
 641          List.map
 642           (function
 643               None -> None
 644             | Some (n, Cic.Decl t) ->
 645                Some (n,
 646                 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
 647             | Some (n, Cic.Def (bo,ty)) ->
 648                let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
 649                let ty' =
 650                 match ty with
 651                    None -> None
 652                  | Some ty ->
 653                     Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
 654                in
 655                 Some (n, Cic.Def (bo',ty'))
 656           ) context
 657         in
 658          (n,context',ty')
 659       ) substituted_metasenv
 660     in
 661      (cleaned_t,cleaned_ty,cleaned_metasenv)
 662
 663 ;;
 664
 665 (* DEBUGGING ONLY *)
 666 let type_of_aux' metasenv context term =
 667  try
 668   let (t,ty,m) = type_of_aux' metasenv context term in
 669    debug_print
 670     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
 671 (*
 672    debug_print
 673     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
 674 *)
 675    (t,ty,m)
 676  with
 677  | RefineFailure msg as e ->
 678      debug_print ("@@@ REFINE FAILED: " ^ msg);
 679      raise e
 680  | Uncertain msg as e ->
 681      debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
 682      raise e
 683 ;;