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