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 (* CSC: why was this code here? it is wrong
 456        (match CicEnvironment.get_cooked_obj ~trust:false uri with
 457            Cic.Variable (_,Some bo,_,_) ->
 458             raise
 459              (RefineFailure
 460                "A variable with a body can not be explicit substituted")
 461          | Cic.Variable (_,None,_,_) -> ()
 462          | _ ->
 463            raise
 464             (RefineFailure
 465              ("Unkown variable definition " ^ UriManager.string_of_uri uri))
 466        ) ;
 467 *)
 468        let typeoft,metasubst',metasenv' =
 469         type_of_aux metasubst metasenv context t
 470        in
 471         let metasubst'',metasenv'' =
 472          try
 473           fo_unif_subst metasubst' context metasenv' typeoft typeofvar
 474          with _ ->
 475           raise (RefineFailure
 476            ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^
 477             " not unifiable with " ^ CicMetaSubst.ppterm metasubst' typeofvar))
 478         in
 479          check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
 480   in
 481    check_exp_named_subst_aux metasubst metasenv []
 482
 483  and sort_of_prod subst metasenv context (name,s) (t1, t2) =
 484   let module C = Cic in
 485     let context_for_t2 = (Some (name,C.Decl s))::context in
 486     let t1'' = CicMetaSubst.whd subst context t1 in
 487     let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in
 488     match (t1'', t2'') with
 489        (C.Sort s1, C.Sort s2)
 490          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
 491           C.Sort s2,subst,metasenv
 492      | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
 493        (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
 494        let t' = CicUniv.fresh() in
 495        if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
 496          assert false ; (* not possible, error in CicUniv *)
 497        C.Sort (C.Type t'),subst,metasenv
 498      | (C.Sort _,C.Sort (C.Type t1)) ->
 499        (* TASSI: CONSRTAINTS: the same in cictypechecker, doubletypeinference *)
 500         C.Sort (C.Type t1),subst,metasenv
 501      | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
 502      | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
 503          (* TODO how can we force the meta to become a sort? If we don't we
 504           * brake the invariant that refine produce only well typed terms *)
 505          (* TODO if we check the non meta term and if it is a sort then we are
 506           * likely to know the exact value of the result e.g. if the rhs is a
 507           * Sort (Prop | Set | CProp) then the result is the rhs *)
 508          let (metasenv,idx) =
 509           CicMkImplicit.mk_implicit_sort metasenv in
 510          let (subst, metasenv) =
 511            fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
 512          in
 513           t2'',subst,metasenv
 514      | (_,_) ->
 515          raise (RefineFailure (sprintf
 516           "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
 517           (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
 518           (CicPp.ppterm t2'')))
 519
 520  and eat_prods subst metasenv context hetype tlbody_and_type =
 521  let rec mk_prod metasenv context =
 522   function
 523      [] ->
 524        let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
 525        let irl =
 526         CicMkImplicit.identity_relocation_list_for_metavariable context
 527        in
 528         metasenv,Cic.Meta (idx, irl)
 529    | (_,argty)::tl ->
 530       let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
 531       let irl =
 532        CicMkImplicit.identity_relocation_list_for_metavariable context
 533       in
 534        let meta = Cic.Meta (idx,irl) in
 535        let name =
 536         (* The name must be fresh for context.                 *)
 537         (* Nevertheless, argty is well-typed only in context.  *)
 538         (* Thus I generate a name (name_hint) in context and   *)
 539         (* then I generate a name --- using the hint name_hint *)
 540         (* --- that is fresh in (context'@context).            *)
 541         let name_hint =
 542          FreshNamesGenerator.mk_fresh_name
 543           (CicMetaSubst.apply_subst_metasenv subst metasenv)
 544           (CicMetaSubst.apply_subst_context subst context)
 545           Cic.Anonymous
 546           (CicMetaSubst.apply_subst subst argty)
 547         in
 548          (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
 549          FreshNamesGenerator.mk_fresh_name
 550           [] context name_hint (Cic.Sort Cic.Prop)
 551        in
 552        let metasenv,target =
 553         mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
 554        in
 555         metasenv,Cic.Prod (name,meta,target)
 556  in
 557   let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
 558   let (subst, metasenv) =
 559    fo_unif_subst subst context metasenv hetype hetype'
 560   in
 561    let rec eat_prods metasenv subst context hetype =
 562       function
 563          [] -> metasenv,subst,hetype
 564        | (hete, hety)::tl ->
 565         (match hetype with
 566             Cic.Prod (n,s,t) ->
 567               let subst,metasenv =
 568                fo_unif_subst subst context metasenv hety s
 569               in
 570                eat_prods metasenv subst context
 571                 (CicMetaSubst.subst subst hete t) tl
 572           | _ -> assert false
 573         )
 574    in
 575     let metasenv,subst,t =
 576      eat_prods metasenv subst context hetype' tlbody_and_type
 577     in
 578      t,subst,metasenv
 579 (*
 580   let rec aux context' args (resty,subst,metasenv) =
 581    function
 582       [] -> resty,subst,metasenv
 583     | (arg,argty)::tl ->
 584        let args' =
 585         List.map
 586          (function
 587              None -> assert false
 588            | Some t -> Some (CicMetaSubst.lift subst 1 t)
 589          ) args in
 590        let argty' = CicMetaSubst.lift subst (List.length args) argty in
 591        let name =
 592         (* The name must be fresh for (context'@context).      *)
 593         (* Nevertheless, argty is well-typed only in context.  *)
 594         (* Thus I generate a name (name_hint) in context and   *)
 595         (* then I generate a name --- using the hint name_hint *)
 596         (* --- that is fresh in (context'@context).            *)
 597         let name_hint =
 598          FreshNamesGenerator.mk_fresh_name
 599           (CicMetaSubst.apply_subst_metasenv subst metasenv)
 600           (CicMetaSubst.apply_subst_context subst context)
 601           Cic.Anonymous
 602           (CicMetaSubst.apply_subst subst argty)
 603         in
 604          (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
 605          FreshNamesGenerator.mk_fresh_name
 606           [] (context'@context) name_hint (Cic.Sort Cic.Prop)
 607        in
 608        let context'' = Some (name, Cic.Decl argty') :: context' in
 609        let (metasenv, idx) =
 610         CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
 611        let irl =
 612          (Some (Cic.Rel 1))::args' @
 613           (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
 614             context)
 615        in
 616        let newmeta = Cic.Meta (idx, irl) in
 617        let prod = Cic.Prod (name, argty, newmeta) in
 618        let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
 619        let (subst, metasenv) =
 620          fo_unif_subst subst context metasenv resty prod
 621        in
 622         aux context'' (Some arg :: args)
 623          (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
 624   in
 625    aux [] [] (hetype,subst,metasenv) tlbody_and_type
 626 *)
 627  in
 628   let ty,subst',metasenv' =
 629    type_of_aux [] metasenv context t
 630   in
 631    let substituted_t = CicMetaSubst.apply_subst subst' t in
 632    let substituted_ty = CicMetaSubst.apply_subst subst' ty in
 633    let substituted_metasenv =
 634     CicMetaSubst.apply_subst_metasenv subst' metasenv'
 635    in
 636     let cleaned_t =
 637      FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
 638     let cleaned_ty =
 639      FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
 640     let cleaned_metasenv =
 641      List.map
 642       (function (n,context,ty) ->
 643         let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
 644         let context' =
 645          List.map
 646           (function
 647               None -> None
 648             | Some (n, Cic.Decl t) ->
 649                Some (n,
 650                 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
 651             | Some (n, Cic.Def (bo,ty)) ->
 652                let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
 653                let ty' =
 654                 match ty with
 655                    None -> None
 656                  | Some ty ->
 657                     Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
 658                in
 659                 Some (n, Cic.Def (bo',ty'))
 660           ) context
 661         in
 662          (n,context',ty')
 663       ) substituted_metasenv
 664     in
 665      (cleaned_t,cleaned_ty,cleaned_metasenv)
 666
 667 ;;
 668
 669 (* DEBUGGING ONLY *)
 670 let type_of_aux' metasenv context term =
 671  try
 672   let (t,ty,m) = type_of_aux' metasenv context term in
 673    debug_print
 674     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
 675 (*
 676    debug_print
 677     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
 678 *)
 679    (t,ty,m)
 680  with
 681  | RefineFailure msg as e ->
 682      debug_print ("@@@ REFINE FAILED: " ^ msg);
 683      raise e
 684  | Uncertain msg as e ->
 685      debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
 686      raise e
 687 ;;