helm/ocaml/cic_unification/cicRefine.ml

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