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        let type2,subst'',metasenv'' =
 189         type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
 190        in
 191         let sort2,subst''',metasenv''' =
 192          type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
 193         in
 194          (* only to check if the product is well-typed *)
 195          let _,subst'''',metasenv'''' =
 196           sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
 197          in
 198           C.Prod (n,s,type2),subst'''',metasenv''''
 199    | C.LetIn (n,s,t) ->
 200       (* only to check if s is well-typed *)
 201       let ty,subst',metasenv' = type_of_aux subst metasenv context s in
 202       let inferredty,subst'',metasenv'' =
 203        type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
 204       in
 205        (* One-step LetIn reduction. Even faster than the previous solution.
 206           Moreover the inferred type is closer to the expected one. *)
 207        CicSubstitution.subst s inferredty,subst',metasenv'
 208    | C.Appl (he::tl) when List.length tl > 0 ->
 209       let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
 210       let tlbody_and_type,subst'',metasenv'' =
 211        List.fold_right
 212         (fun x (res,subst,metasenv) ->
 213           let ty,subst',metasenv' =
 214            type_of_aux subst metasenv context x
 215           in
 216            (x, ty)::res,subst',metasenv'
 217         ) tl ([],subst',metasenv')
 218       in
 219        eat_prods subst'' metasenv'' context hetype tlbody_and_type
 220    | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
 221    | C.Const (uri,exp_named_subst) ->
 222       let subst',metasenv' =
 223        check_exp_named_subst subst metasenv context exp_named_subst in
 224       let cty =
 225        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
 226       in
 227        cty,subst',metasenv'
 228    | C.MutInd (uri,i,exp_named_subst) ->
 229       let subst',metasenv' =
 230        check_exp_named_subst subst metasenv context exp_named_subst in
 231       let cty =
 232        CicSubstitution.subst_vars exp_named_subst
 233         (type_of_mutual_inductive_defs uri i)
 234       in
 235        cty,subst',metasenv'
 236    | C.MutConstruct (uri,i,j,exp_named_subst) ->
 237       let subst',metasenv' =
 238        check_exp_named_subst subst metasenv context exp_named_subst in
 239       let cty =
 240        CicSubstitution.subst_vars exp_named_subst
 241         (type_of_mutual_inductive_constr uri i j)
 242       in
 243        cty,subst',metasenv'
 244    | C.MutCase (uri, i, outtype, term, pl) ->
 245        (* first, get the inductive type (and noparams) in the environment  *)
 246        let (_,b,arity,constructors), expl_params, no_left_params =
 247          match CicEnvironment.get_cooked_obj ~trust:true uri with
 248             C.InductiveDefinition (l,expl_params,parsno) ->
 249               List.nth l i , expl_params, parsno
 250           | _ ->
 251             raise
 252              (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
 253        let rec count_prod t =
 254          match CicMetaSubst.whd subst context t with
 255              C.Prod (_, _, t) -> 1 + (count_prod t)
 256            | _ -> 0 in
 257        let no_args = count_prod arity in
 258        (* now, create a "generic" MutInd *)
 259        let metasenv,left_args =
 260          CicMkImplicit.n_fresh_metas metasenv context no_left_params in
 261        let metasenv,right_args =
 262          let no_right_params = no_args - no_left_params in
 263          if no_right_params < 0 then assert false
 264          else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
 265        let metasenv,exp_named_subst =
 266          CicMkImplicit.fresh_subst metasenv context expl_params in
 267        let expected_type =
 268          if no_args = 0 then
 269            C.MutInd (uri,i,exp_named_subst)
 270          else
 271            C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 272        in
 273        (* check consistency with the actual type of term *)
 274        let actual_type,subst,metasenv =
 275          type_of_aux subst metasenv context term in
 276        let _, subst, metasenv =
 277          type_of_aux subst metasenv context expected_type
 278        in
 279        let actual_type = CicMetaSubst.whd subst context actual_type in
 280        let subst,metasenv =
 281          fo_unif_subst subst context metasenv expected_type actual_type
 282        in
 283        (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
 284        let (_,outtypeinstances,subst,metasenv) =
 285           List.fold_left
 286            (fun (j,outtypeinstances,subst,metasenv) p ->
 287              let constructor =
 288               if left_args = [] then
 289                (C.MutConstruct (uri,i,j,exp_named_subst))
 290               else
 291                (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 292              in
 293              let actual_type,subst,metasenv =
 294                type_of_aux subst metasenv context p in
 295              let expected_type, subst, metasenv =
 296                type_of_aux subst metasenv context constructor in
 297              let outtypeinstance,subst,metasenv =
 298                check_branch
 299                 0 context metasenv subst
 300                 no_left_params actual_type constructor expected_type in
 301              (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
 302             (1,[],subst,metasenv) pl in
 303         (* we are left to check that the outype matches his instances.
 304            The easy case is when the outype is specified, that amount
 305            to a trivial check. Otherwise, we should guess a type from
 306            its instances *)
 307         (* easy case *)
 308         let _, subst, metasenv =
 309           type_of_aux subst metasenv context
 310             (C.Appl ((outtype :: right_args) @ [term]))
 311         in
 312         let (subst,metasenv) =
 313           List.fold_left
 314             (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
 315               let instance' =
 316                 let appl =
 317                   let outtype' =
 318                     CicSubstitution.lift constructor_args_no outtype
 319                   in
 320                   C.Appl (outtype'::args)
 321                 in
 322 (*
 323                 (* if appl is not well typed then the type_of below solves the
 324                  * problem *)
 325                 let (_, subst, metasenv) =
 326                   type_of_aux subst metasenv context appl
 327                 in
 328 *)
 329                 CicMetaSubst.whd subst context appl
 330               in
 331                fo_unif_subst subst context metasenv instance instance')
 332              (subst,metasenv) outtypeinstances in
 333         CicMetaSubst.whd subst
 334           context (C.Appl(outtype::right_args@[term])),subst,metasenv
 335    | C.Fix (i,fl) ->
 336       let subst,metasenv,types =
 337        List.fold_left
 338         (fun (subst,metasenv,types) (n,_,ty,_) ->
 339           let _,subst',metasenv' = type_of_aux subst metasenv context ty in
 340            subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
 341         ) (subst,metasenv,[]) fl
 342       in
 343        let len = List.length types in
 344        let context' = types@context in
 345        let subst,metasenv =
 346         List.fold_left
 347          (fun (subst,metasenv) (name,x,ty,bo) ->
 348            let ty_of_bo,subst,metasenv =
 349             type_of_aux subst metasenv context' bo
 350            in
 351             fo_unif_subst subst context' metasenv
 352               ty_of_bo (CicMetaSubst.lift subst len ty)
 353          ) (subst,metasenv) fl in
 354         let (_,_,ty,_) = List.nth fl i in
 355          ty,subst,metasenv
 356    | C.CoFix (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,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
 376         let (_,ty,_) = List.nth fl i in
 377          ty,subst,metasenv
 378
 379  (* check_metasenv_consistency checks that the "canonical" context of a
 380  metavariable is consitent - up to relocation via the relocation list l -
 381  with the actual context *)
 382  and check_metasenv_consistency
 383   metano subst metasenv context canonical_context l
 384  =
 385    let module C = Cic in
 386    let module R = CicReduction in
 387    let module S = CicSubstitution in
 388     let lifted_canonical_context =
 389      let rec aux i =
 390       function
 391          [] -> []
 392        | (Some (n,C.Decl t))::tl ->
 393           (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
 394        | (Some (n,C.Def (t,None)))::tl ->
 395           (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 396        | None::tl -> None::(aux (i+1) tl)
 397        | (Some (n,C.Def (t,Some ty)))::tl ->
 398            (Some (n,
 399             C.Def ((S.lift_meta l (S.lift i t)),
 400               Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
 401      in
 402       aux 1 canonical_context
 403     in
 404      List.fold_left2
 405       (fun (subst,metasenv) t ct ->
 406         match (t,ct) with
 407            _,None ->
 408              subst,metasenv
 409          | Some t,Some (_,C.Def (ct,_)) ->
 410             (try
 411               fo_unif_subst subst context metasenv t ct
 412              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)))))
 413          | Some t,Some (_,C.Decl ct) ->
 414             let inferredty,subst',metasenv' =
 415              type_of_aux subst metasenv context t
 416             in
 417              (try
 418                fo_unif_subst
 419                 subst' context metasenv' inferredty ct
 420              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)))))
 421          | None, Some _  ->
 422              raise (NotRefinable (sprintf
 423               "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"
 424               (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 425               (CicMetaSubst.ppcontext subst canonical_context)))
 426       ) (subst,metasenv) l lifted_canonical_context
 427
 428  and check_exp_named_subst metasubst metasenv context =
 429   let rec check_exp_named_subst_aux metasubst metasenv substs =
 430    function
 431       [] -> metasubst,metasenv
 432     | ((uri,t) as subst)::tl ->
 433        let typeofvar =
 434         CicSubstitution.subst_vars substs (type_of_variable uri) in
 435        (match CicEnvironment.get_cooked_obj ~trust:false uri with
 436            Cic.Variable (_,Some bo,_,_) ->
 437             raise
 438              (NotRefinable
 439                "A variable with a body can not be explicit substituted")
 440          | Cic.Variable (_,None,_,_) -> ()
 441          | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 442        ) ;
 443        let typeoft,metasubst',metasenv' =
 444         type_of_aux metasubst metasenv context t
 445        in
 446         try
 447          let metasubst'',metasenv'' =
 448           fo_unif_subst metasubst' context metasenv' typeoft typeofvar
 449          in
 450           check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
 451         with _ ->
 452          raise (NotRefinable "Wrong Explicit Named Substitution")
 453   in
 454    check_exp_named_subst_aux metasubst metasenv []
 455
 456  and sort_of_prod subst metasenv context (name,s) (t1, t2) =
 457   let module C = Cic in
 458     let context_for_t2 = (Some (name,C.Decl s))::context in
 459     let t1'' = CicMetaSubst.whd subst context t1 in
 460     let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in
 461     match (t1'', t2'') with
 462        (C.Sort s1, C.Sort s2)
 463          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
 464           C.Sort s2,subst,metasenv
 465      | (C.Sort s1, C.Sort s2) ->
 466          (*CSC manca la gestione degli universi!!! *)
 467          C.Sort C.Type,subst,metasenv
 468      | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
 469      | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
 470          (* TODO how can we force the meta to become a sort? If we don't we
 471           * brake the invariant that refine produce only well typed terms *)
 472          (* TODO if we check the non meta term and if it is a sort then we are
 473           * likely to know the exact value of the result e.g. if the rhs is a
 474           * Sort (Prop | Set | CProp) then the result is the rhs *)
 475          let (metasenv,idx) =
 476           CicMkImplicit.mk_implicit_sort metasenv in
 477          let (subst, metasenv) =
 478            fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2''
 479          in
 480           t2'',subst,metasenv
 481      | (_,_) ->
 482          raise (NotRefinable (sprintf
 483           "Two types were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
 484           (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
 485           (CicPp.ppterm t2'')))
 486
 487  and eat_prods subst metasenv context hetype tlbody_and_type =
 488   let rec aux context' args (resty,subst,metasenv) =
 489    function
 490       [] -> resty,subst,metasenv
 491     | (arg,argty)::tl ->
 492        let args' =
 493         List.map
 494          (function
 495              None -> assert false
 496            | Some t -> Some (CicMetaSubst.lift subst 1 t)
 497          ) args in
 498        let argty' = CicMetaSubst.lift subst (List.length args) argty in
 499        let name =
 500         (* The name must be fresh for (context'@context).      *)
 501         (* Nevertheless, argty is well-typed only in context.  *)
 502         (* Thus I generate a name (name_hint) in context and   *)
 503         (* then I generate a name --- using the hint name_hint *)
 504         (* --- that is fresh in (context'@context).            *)
 505         let name_hint =
 506          FreshNamesGenerator.mk_fresh_name
 507           (CicMetaSubst.apply_subst_metasenv subst metasenv)
 508           (CicMetaSubst.apply_subst_context subst context)
 509           Cic.Anonymous
 510           (CicMetaSubst.apply_subst subst argty)
 511         in
 512          (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
 513          FreshNamesGenerator.mk_fresh_name
 514           [] (context'@context) name_hint (Cic.Sort Cic.Prop)
 515        in
 516        let context'' = Some (name, Cic.Decl argty') :: context' in
 517        let (metasenv, idx) =
 518         CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
 519        let irl =
 520          (Some (Cic.Rel 1))::args' @
 521           (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
 522             context)
 523        in
 524        let newmeta = Cic.Meta (idx, irl) in
 525        let prod = Cic.Prod (name, argty, newmeta) in
 526        let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
 527        let (subst, metasenv) =
 528          fo_unif_subst subst context metasenv resty prod
 529        in
 530         aux context'' (Some arg :: args)
 531          (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
 532   in
 533    aux [] [] (hetype,subst,metasenv) tlbody_and_type
 534
 535  in
 536   let ty,subst',metasenv' =
 537    type_of_aux [] metasenv context t
 538   in
 539    let substituted_t = CicMetaSubst.apply_subst subst' t in
 540    let substituted_ty = CicMetaSubst.apply_subst subst' ty in
 541    let substituted_metasenv =
 542     CicMetaSubst.apply_subst_metasenv subst' metasenv'
 543    in
 544     let cleaned_t =
 545      FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
 546     let cleaned_ty =
 547      FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
 548     let cleaned_metasenv =
 549      List.map
 550       (function (n,context,ty) ->
 551         let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
 552         let context' =
 553          List.map
 554           (function
 555               None -> None
 556             | Some (n, Cic.Decl t) ->
 557                Some (n,
 558                 Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
 559             | Some (n, Cic.Def (bo,ty)) ->
 560                let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
 561                let ty' =
 562                 match ty with
 563                    None -> None
 564                  | Some ty ->
 565                     Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
 566                in
 567                 Some (n, Cic.Def (bo',ty'))
 568           ) context
 569         in
 570          (n,context',ty')
 571       ) substituted_metasenv
 572     in
 573      (cleaned_t,cleaned_ty,cleaned_metasenv)
 574
 575 ;;
 576
 577 (* DEBUGGING ONLY *)
 578 let type_of_aux' metasenv context term =
 579  try
 580   let (t,ty,m) = type_of_aux' metasenv context term in
 581    debug_print
 582     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
 583 (*
 584    debug_print
 585     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
 586 *)
 587    (t,ty,m)
 588  with
 589  | CicUnification.AssertFailure msg as e ->
 590      debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
 591      debug_print msg;
 592      raise e
 593  | e ->
 594    debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
 595    raise e
 596 ;;
 597