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