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      List.fold_left2
 407       (fun (subst,metasenv) t ct ->
 408         match (t,ct) with
 409            _,None ->
 410              subst,metasenv
 411          | Some t,Some (_,C.Def (ct,_)) ->
 412             (try
 413               fo_unif_subst subst context metasenv t ct
 414              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)))))
 415          | Some t,Some (_,C.Decl ct) ->
 416             let inferredty,subst',metasenv' =
 417              type_of_aux subst metasenv context t
 418             in
 419              (try
 420                fo_unif_subst
 421                 subst' context metasenv' inferredty ct
 422              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)))))
 423          | None, Some _  ->
 424              raise (NotRefinable (sprintf
 425               "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"
 426               (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 427               (CicMetaSubst.ppcontext subst canonical_context)))
 428       ) (subst,metasenv) l lifted_canonical_context
 429
 430  and check_exp_named_subst metasubst metasenv context =
 431   let rec check_exp_named_subst_aux metasubst metasenv substs =
 432    function
 433       [] -> metasubst,metasenv
 434     | ((uri,t) as subst)::tl ->
 435        let typeofvar =
 436         CicSubstitution.subst_vars substs (type_of_variable uri) in
 437        (match CicEnvironment.get_cooked_obj ~trust:false uri with
 438            Cic.Variable (_,Some bo,_,_) ->
 439             raise
 440              (NotRefinable
 441                "A variable with a body can not be explicit substituted")
 442          | Cic.Variable (_,None,_,_) -> ()
 443          | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 444        ) ;
 445        let typeoft,metasubst',metasenv' =
 446         type_of_aux metasubst metasenv context t
 447        in
 448         try
 449          let metasubst'',metasenv'' =
 450           fo_unif_subst metasubst' context metasenv' typeoft typeofvar
 451          in
 452           check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
 453         with _ ->
 454          raise (NotRefinable "Wrong Explicit Named Substitution")
 455   in
 456    check_exp_named_subst_aux metasubst metasenv []
 457
 458  and sort_of_prod subst metasenv context (name,s) (t1, t2) =
 459   let module C = Cic in
 460     let context_for_t2 = (Some (name,C.Decl s))::context in
 461     let t1'' = CicMetaSubst.whd subst context t1 in
 462     let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in
 463     match (t1'', t2'') with
 464        (C.Sort s1, C.Sort s2)
 465          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
 466           C.Sort s2,subst,metasenv
 467      | (C.Sort s1, C.Sort s2) ->
 468          (*CSC manca la gestione degli universi!!! *)
 469          C.Sort C.Type,subst,metasenv
 470      | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
 471      | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
 472          (* TODO how can we force the meta to become a sort? If we don't we
 473           * brake the invariant that refine produce only well typed terms *)
 474          (* TODO if we check the non meta term and if it is a sort then we are
 475           * likely to know the exact value of the result e.g. if the rhs is a
 476           * Sort (Prop | Set | CProp) then the result is the rhs *)
 477          let (metasenv,idx) =
 478           CicMkImplicit.mk_implicit_sort metasenv in
 479          let (subst, metasenv) =
 480            fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
 481          in
 482           t2'',subst,metasenv
 483      | (_,_) ->
 484          raise (NotRefinable (sprintf
 485           "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
 486           (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
 487           (CicPp.ppterm t2'')))
 488
 489  and eat_prods subst metasenv context hetype tlbody_and_type =
 490  let rec mk_prod metasenv context =
 491   function
 492      [] ->
 493        let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
 494        let irl =
 495         CicMkImplicit.identity_relocation_list_for_metavariable context
 496        in
 497         metasenv,Cic.Meta (idx, irl)
 498    | (_,argty)::tl ->
 499       let (metasenv, idx) = CicMkImplicit.mk_implicit_type metasenv context in
 500       let irl =
 501        CicMkImplicit.identity_relocation_list_for_metavariable context
 502       in
 503        let meta = Cic.Meta (idx,irl) in
 504        let name =
 505         (* The name must be fresh for context.                 *)
 506         (* Nevertheless, argty is well-typed only in context.  *)
 507         (* Thus I generate a name (name_hint) in context and   *)
 508         (* then I generate a name --- using the hint name_hint *)
 509         (* --- that is fresh in (context'@context).            *)
 510         let name_hint =
 511          FreshNamesGenerator.mk_fresh_name
 512           (CicMetaSubst.apply_subst_metasenv subst metasenv)
 513           (CicMetaSubst.apply_subst_context subst context)
 514           Cic.Anonymous
 515           (CicMetaSubst.apply_subst subst argty)
 516         in
 517          (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
 518          FreshNamesGenerator.mk_fresh_name
 519           [] context name_hint (Cic.Sort Cic.Prop)
 520        in
 521        let metasenv,target =
 522         mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
 523        in
 524         metasenv,Cic.Prod (name,meta,target)
 525  in
 526   let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
 527   let (subst, metasenv) =
 528    CicUnification.fo_unif_subst subst context metasenv hetype hetype'
 529   in
 530    let rec eat_prods metasenv subst context hetype =
 531       function
 532          [] -> metasenv,subst,hetype
 533        | (hete, hety)::tl ->
 534         (match hetype with
 535             Cic.Prod (n,s,t) ->
 536              (try
 537               let subst,metasenv =
 538                CicUnification.fo_unif_subst subst context metasenv s hety
 539               in
 540                eat_prods metasenv subst context
 541                 (CicMetaSubst.subst subst hete t) tl
 542              with
 543               e -> raise (RefineFailure ("XXX " ^ Printexc.to_string e)))
 544           | _ -> assert false
 545         )
 546    in
 547     let metasenv,subst,t =
 548      eat_prods metasenv subst context hetype' tlbody_and_type
 549     in
 550      t,subst,metasenv
 551
 552 (*
 553   let rec aux context' args (resty,subst,metasenv) =
 554    function
 555       [] -> resty,subst,metasenv
 556     | (arg,argty)::tl ->
 557        let args' =
 558         List.map
 559          (function
 560              None -> assert false
 561            | Some t -> Some (CicMetaSubst.lift subst 1 t)
 562          ) args in
 563        let argty' = CicMetaSubst.lift subst (List.length args) argty in
 564        let name =
 565         (* The name must be fresh for (context'@context).      *)
 566         (* Nevertheless, argty is well-typed only in context.  *)
 567         (* Thus I generate a name (name_hint) in context and   *)
 568         (* then I generate a name --- using the hint name_hint *)
 569         (* --- that is fresh in (context'@context).            *)
 570         let name_hint =
 571          FreshNamesGenerator.mk_fresh_name
 572           (CicMetaSubst.apply_subst_metasenv subst metasenv)
 573           (CicMetaSubst.apply_subst_context subst context)
 574           Cic.Anonymous
 575           (CicMetaSubst.apply_subst subst argty)
 576         in
 577          (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
 578          FreshNamesGenerator.mk_fresh_name
 579           [] (context'@context) name_hint (Cic.Sort Cic.Prop)
 580        in
 581        let context'' = Some (name, Cic.Decl argty') :: context' in
 582        let (metasenv, idx) =
 583         CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
 584        let irl =
 585          (Some (Cic.Rel 1))::args' @
 586           (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
 587             context)
 588        in
 589        let newmeta = Cic.Meta (idx, irl) in
 590        let prod = Cic.Prod (name, argty, newmeta) in
 591        let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
 592        let (subst, metasenv) =
 593          fo_unif_subst subst context metasenv resty prod
 594        in
 595         aux context'' (Some arg :: args)
 596          (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
 597   in
 598    aux [] [] (hetype,subst,metasenv) tlbody_and_type
 599 *)
 600
 601  in
 602   let ty,subst',metasenv' =
 603    type_of_aux [] metasenv context t
 604   in
 605    let substituted_t = CicMetaSubst.apply_subst subst' t in
 606    let substituted_ty = CicMetaSubst.apply_subst subst' ty in
 607    let substituted_metasenv =
 608     CicMetaSubst.apply_subst_metasenv subst' metasenv'
 609    in
 610     let cleaned_t =
 611      FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
 612     let cleaned_ty =
 613      FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
 614     let cleaned_metasenv =
 615      List.map
 616       (function (n,context,ty) ->
 617         let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
 618         let context' =
 619          List.map
 620           (function
 621               None -> None
 622             | Some (n, Cic.Decl t) ->
 623                Some (n,
 624                 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
 625             | Some (n, Cic.Def (bo,ty)) ->
 626                let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
 627                let ty' =
 628                 match ty with
 629                    None -> None
 630                  | Some ty ->
 631                     Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
 632                in
 633                 Some (n, Cic.Def (bo',ty'))
 634           ) context
 635         in
 636          (n,context',ty')
 637       ) substituted_metasenv
 638     in
 639      (cleaned_t,cleaned_ty,cleaned_metasenv)
 640
 641 ;;
 642
 643 (* DEBUGGING ONLY *)
 644 let type_of_aux' metasenv context term =
 645  try
 646   let (t,ty,m) = type_of_aux' metasenv context term in
 647    debug_print
 648     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
 649 (*
 650    debug_print
 651     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
 652 *)
 653    (t,ty,m)
 654  with
 655  | CicUnification.AssertFailure msg as e ->
 656      debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
 657      debug_print msg;
 658      raise e
 659  | e ->
 660    debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
 661    raise e
 662 ;;
 663