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 fdebug = ref 0;;
  41 let debug t context =
  42  let rec debug_aux t i =
  43   let module C = Cic in
  44   let module U = UriManager in
  45    CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
  46  in
  47   if !fdebug = 0 then
  48    raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
  49    (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
  50 ;;
  51
  52 let debug_print = prerr_endline
  53
  54 let rec split l n =
  55  match (l,n) with
  56     (l,0) -> ([], l)
  57   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  58   | (_,_) -> raise ListTooShort
  59 ;;
  60
  61 let rec type_of_constant uri =
  62  let module C = Cic in
  63  let module R = CicReduction in
  64  let module U = UriManager in
  65   match CicEnvironment.get_cooked_obj uri with
  66      C.Constant (_,_,ty,_) -> ty
  67    | C.CurrentProof (_,_,_,ty,_) -> ty
  68    | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
  69
  70 and type_of_variable uri =
  71  let module C = Cic in
  72  let module R = CicReduction in
  73  let module U = UriManager in
  74   match CicEnvironment.get_cooked_obj uri with
  75      C.Variable (_,_,ty,_) -> ty
  76    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
  77
  78 and type_of_mutual_inductive_defs uri i =
  79  let module C = Cic in
  80  let module R = CicReduction in
  81  let module U = UriManager in
  82   match CicEnvironment.get_cooked_obj uri with
  83      C.InductiveDefinition (dl,_,_) ->
  84       let (_,_,arity,_) = List.nth dl i in
  85        arity
  86    | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
  87
  88 and type_of_mutual_inductive_constr uri i j =
  89  let module C = Cic in
  90  let module R = CicReduction in
  91  let module U = UriManager in
  92   match CicEnvironment.get_cooked_obj uri with
  93       C.InductiveDefinition (dl,_,_) ->
  94        let (_,_,_,cl) = List.nth dl i in
  95         let (_,ty) = List.nth cl (j-1) in
  96          ty
  97    | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
  98
  99 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 100
 101 (* the check_branch function checks if a branch of a case is refinable.
 102    It returns a pair (outype_instance,args), a subst and a metasenv.
 103    outype_instance is the expected result of applying the case outtype
 104    to args.
 105    The problem is that outype is in general unknown, and we should
 106    try to synthesize it from the above information, that is in general
 107    a second order unification problem. *)
 108
 109 and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
 110   let module C = Cic in
 111   let module R = CicMetaSubst in
 112   let module Un = CicUnification in
 113   match R.whd subst context expectedtype with
 114      C.MutInd (_,_,_) ->
 115        (n,context,actualtype, [term]), subst, metasenv
 116    | C.Appl (C.MutInd (_,_,_)::tl) ->
 117        let (_,arguments) = split tl left_args_no in
 118        (n,context,actualtype, arguments@[term]), subst, metasenv
 119    | C.Prod (name,so,de) ->
 120       (* we expect that the actual type of the branch has the due
 121          number of Prod *)
 122       (match R.whd subst context actualtype with
 123            C.Prod (name',so',de') ->
 124              let subst, metasenv =
 125                 Un.fo_unif_subst subst context metasenv so so' in
 126              let term' =
 127                (match CicSubstitution.lift 1 term with
 128                    C.Appl l -> C.Appl (l@[C.Rel 1])
 129                  | t -> C.Appl [t ; C.Rel 1]) in
 130              (* we should also check that the name variable is anonymous in
 131              the actual type de' ?? *)
 132              check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de
 133          | _ -> raise WrongArgumentNumber)
 134   | _ -> raise (NotRefinable "Prod or MutInd expected")
 135
 136 and type_of_aux' metasenv context t =
 137  let rec type_of_aux subst metasenv context =
 138   let module C = Cic in
 139   let module S = CicSubstitution in
 140   let module U = UriManager in
 141   let module Un = CicUnification in
 142    function
 143       C.Rel n ->
 144        (try
 145          match List.nth context (n - 1) with
 146             Some (_,C.Decl t) -> S.lift n t,subst,metasenv
 147           | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
 148           | Some (_,C.Def (bo,None)) ->
 149              type_of_aux subst metasenv context (S.lift n bo)
 150           | None -> raise RelToHiddenHypothesis
 151         with
 152          _ -> raise (NotRefinable "Not a close term")
 153        )
 154     | C.Var (uri,exp_named_subst) ->
 155       incr fdebug ;
 156       let subst',metasenv' =
 157        check_exp_named_subst subst metasenv context exp_named_subst in
 158       let ty =
 159        CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
 160       in
 161        decr fdebug ;
 162        ty,subst',metasenv'
 163     | C.Meta (n,l) ->
 164        let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
 165         let subst',metasenv' =
 166          check_metasenv_consistency n subst metasenv context canonical_context l
 167         in
 168         CicSubstitution.lift_meta l ty, subst', metasenv'
 169     | C.Sort s ->
 170        C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
 171         subst,metasenv
 172     | C.Implicit -> raise (Impossible 21)
 173     | C.Cast (te,ty) ->
 174        let _,subst',metasenv' =
 175         type_of_aux subst metasenv context ty in
 176        let inferredty,subst'',metasenv'' =
 177         type_of_aux subst' metasenv' context te
 178        in
 179         (try
 180           let subst''',metasenv''' =
 181            Un.fo_unif_subst subst'' context metasenv'' inferredty ty
 182           in
 183            ty,subst''',metasenv'''
 184          with
 185           _ -> raise (NotRefinable "Cast"))
 186     | C.Prod (name,s,t) ->
 187        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
 188        let sort2,subst'',metasenv'' =
 189         type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
 190        in
 191         sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2),
 192          subst'',metasenv''
 193    | C.Lambda (n,s,t) ->
 194        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
 195        let type2,subst'',metasenv'' =
 196         type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
 197        in
 198         let sort2,subst''',metasenv''' =
 199          type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
 200         in
 201          (* only to check if the product is well-typed *)
 202          let _ =
 203           sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
 204          in
 205           C.Prod (n,s,type2),subst''',metasenv'''
 206    | C.LetIn (n,s,t) ->
 207       (* only to check if s is well-typed *)
 208       let ty,subst',metasenv' = type_of_aux subst metasenv context s in
 209       let inferredty,subst'',metasenv'' =
 210        type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
 211       in
 212        (* One-step LetIn reduction. Even faster than the previous solution.
 213           Moreover the inferred type is closer to the expected one. *)
 214        CicSubstitution.subst s inferredty,subst',metasenv'
 215    | C.Appl (he::tl) when List.length tl > 0 ->
 216       let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
 217       let tlbody_and_type,subst'',metasenv'' =
 218        List.fold_right
 219         (fun x (res,subst,metasenv) ->
 220           let ty,subst',metasenv' =
 221            type_of_aux subst metasenv context x
 222           in
 223            (x, ty)::res,subst',metasenv'
 224         ) tl ([],subst',metasenv')
 225       in
 226        eat_prods subst'' metasenv'' context hetype tlbody_and_type
 227    | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
 228    | C.Const (uri,exp_named_subst) ->
 229       incr fdebug ;
 230       let subst',metasenv' =
 231        check_exp_named_subst subst metasenv context exp_named_subst in
 232       let cty =
 233        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
 234       in
 235        decr fdebug ;
 236        cty,subst',metasenv'
 237    | C.MutInd (uri,i,exp_named_subst) ->
 238       incr fdebug ;
 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_defs uri i)
 244       in
 245        decr fdebug ;
 246        cty,subst',metasenv'
 247    | C.MutConstruct (uri,i,j,exp_named_subst) ->
 248       let subst',metasenv' =
 249        check_exp_named_subst subst metasenv context exp_named_subst in
 250       let cty =
 251        CicSubstitution.subst_vars exp_named_subst
 252         (type_of_mutual_inductive_constr uri i j)
 253       in
 254        cty,subst',metasenv'
 255    | C.MutCase (uri, i, outtype, term, pl) ->
 256        (* first, get the inductive type (and noparams) in the environment  *)
 257        let (_,b,arity,constructors), expl_params, no_left_params =
 258          match CicEnvironment.get_cooked_obj ~trust:true uri with
 259             C.InductiveDefinition (l,expl_params,parsno) ->
 260               List.nth l i , expl_params, parsno
 261           | _ ->
 262             raise
 263              (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
 264        let rec count_prod t =
 265          match CicMetaSubst.whd subst context t with
 266              C.Prod (_, _, t) -> 1 + (count_prod t)
 267            | _ -> 0 in
 268        let no_args = count_prod arity in
 269        (* now, create a "generic" MutInd *)
 270        let metasenv,left_args =
 271          CicMkImplicit.n_fresh_metas metasenv context no_left_params in
 272        let metasenv,right_args =
 273          let no_right_params = no_args - no_left_params in
 274          if no_right_params < 0 then assert false
 275          else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
 276        let metasenv,exp_named_subst =
 277          CicMkImplicit.fresh_subst metasenv context expl_params in
 278        let expected_type =
 279          if no_args = 0 then
 280            C.MutInd (uri,i,exp_named_subst)
 281          else
 282            C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
 283        in
 284        (* check consistency with the actual type of term *)
 285        let actual_type,subst,metasenv =
 286          type_of_aux subst metasenv context term in
 287        let _, subst, metasenv =
 288          type_of_aux subst metasenv context expected_type
 289        in
 290        let actual_type = CicMetaSubst.whd subst context actual_type in
 291        let subst,metasenv =
 292          Un.fo_unif_subst subst context metasenv expected_type actual_type
 293        in
 294        (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
 295        let (_,outtypeinstances,subst,metasenv) =
 296           List.fold_left
 297            (fun (j,outtypeinstances,subst,metasenv) p ->
 298              let constructor =
 299               if left_args = [] then
 300                (C.MutConstruct (uri,i,j,exp_named_subst))
 301               else
 302                (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
 303              in
 304              let actual_type,subst,metasenv =
 305                type_of_aux subst metasenv context p in
 306              let expected_type, subst, metasenv =
 307                type_of_aux subst metasenv context constructor in
 308              let outtypeinstance,subst,metasenv =
 309                check_branch
 310                 0 context metasenv subst
 311                 no_left_params actual_type constructor expected_type in
 312              (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
 313             (1,[],subst,metasenv) pl in
 314         (* we are left to check that the outype matches his instances.
 315            The easy case is when the outype is specified, that amount
 316            to a trivial check. Otherwise, we should guess a type from
 317            its instances *)
 318         (* easy case *)
 319         let _, subst, metasenv =
 320           type_of_aux subst metasenv context
 321             (C.Appl ((outtype :: right_args) @ [term]))
 322         in
 323         let (subst,metasenv) =
 324           List.fold_left
 325             (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
 326               let instance' =
 327                 let appl =
 328                   let outtype' =
 329                     CicSubstitution.lift constructor_args_no outtype
 330                   in
 331                   C.Appl (outtype'::args)
 332                 in
 333 (*
 334                 (* if appl is not well typed then the type_of below solves the
 335                  * problem *)
 336                 let (_, subst, metasenv) =
 337                   type_of_aux subst metasenv context appl
 338                 in
 339 *)
 340                 CicMetaSubst.whd subst context appl
 341               in
 342                Un.fo_unif_subst subst context metasenv instance instance')
 343              (subst,metasenv) outtypeinstances in
 344         CicMetaSubst.whd subst
 345           context (C.Appl(outtype::right_args@[term])),subst,metasenv
 346    | C.Fix (i,fl) ->
 347       let subst,metasenv,types =
 348        List.fold_left
 349         (fun (subst,metasenv,types) (n,_,ty,_) ->
 350           let _,subst',metasenv' = type_of_aux subst metasenv context ty in
 351            subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
 352         ) (subst,metasenv,[]) fl
 353       in
 354        let len = List.length types in
 355        let context' = types@context in
 356        let subst,metasenv =
 357         List.fold_left
 358          (fun (subst,metasenv) (name,x,ty,bo) ->
 359            let ty_of_bo,subst,metasenv =
 360             type_of_aux subst metasenv context' bo
 361            in
 362             Un.fo_unif_subst subst context' metasenv
 363               ty_of_bo (CicMetaSubst.lift subst len ty)
 364          ) (subst,metasenv) fl in
 365         let (_,_,ty,_) = List.nth fl i in
 366          ty,subst,metasenv
 367    | C.CoFix (i,fl) ->
 368       let subst,metasenv,types =
 369        List.fold_left
 370         (fun (subst,metasenv,types) (n,ty,_) ->
 371           let _,subst',metasenv' = type_of_aux subst metasenv context ty in
 372            subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
 373         ) (subst,metasenv,[]) fl
 374       in
 375        let len = List.length types in
 376        let context' = types@context in
 377        let subst,metasenv =
 378         List.fold_left
 379          (fun (subst,metasenv) (name,ty,bo) ->
 380            let ty_of_bo,subst,metasenv =
 381             type_of_aux subst metasenv context' bo
 382            in
 383             Un.fo_unif_subst subst context' metasenv
 384               ty_of_bo (CicMetaSubst.lift subst len ty)
 385          ) (subst,metasenv) fl in
 386
 387         let (_,ty,_) = List.nth fl i in
 388          ty,subst,metasenv
 389
 390  (* check_metasenv_consistency checks that the "canonical" context of a
 391  metavariable is consitent - up to relocation via the relocation list l -
 392  with the actual context *)
 393  and check_metasenv_consistency
 394   metano subst metasenv context canonical_context l
 395  =
 396    let module C = Cic in
 397    let module R = CicReduction in
 398    let module S = CicSubstitution in
 399     let lifted_canonical_context =
 400      let rec aux i =
 401       function
 402          [] -> []
 403        | (Some (n,C.Decl t))::tl ->
 404           (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
 405        | (Some (n,C.Def (t,None)))::tl ->
 406           (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
 407        | None::tl -> None::(aux (i+1) tl)
 408        | (Some (n,C.Def (t,Some ty)))::tl ->
 409            (Some (n,
 410             C.Def ((S.lift_meta l (S.lift i t)),
 411               Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
 412      in
 413       aux 1 canonical_context
 414     in
 415      List.fold_left2
 416       (fun (subst,metasenv) t ct ->
 417         match (t,ct) with
 418            _,None ->
 419              subst,metasenv
 420          | Some t,Some (_,C.Def (ct,_)) ->
 421             (try
 422               CicUnification.fo_unif_subst subst context metasenv t ct
 423              with _ -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct))))
 424          | Some t,Some (_,C.Decl ct) ->
 425             let inferredty,subst',metasenv' =
 426              type_of_aux subst metasenv context t
 427             in
 428              (try
 429                CicUnification.fo_unif_subst
 430                 subst' context metasenv' inferredty ct
 431              with _ -> 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" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct))))
 432          | None, Some _  ->
 433              raise (NotRefinable (sprintf
 434               "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"
 435               (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
 436               (CicMetaSubst.ppcontext subst canonical_context)))
 437       ) (subst,metasenv) l lifted_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           CicUnification.fo_unif_subst
 460            metasubst' context metasenv' typeoft typeofvar
 461          in
 462           check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
 463         with _ ->
 464          raise (NotRefinable "Wrong Explicit Named Substitution")
 465   in
 466    check_exp_named_subst_aux metasubst metasenv []
 467
 468  and sort_of_prod subst metasenv context (name,s) (t1, t2) =
 469   let module C = Cic in
 470     let t1'' = CicMetaSubst.whd subst context t1 in
 471     let t2'' = CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) 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
 476      | (C.Sort s1, C.Sort s2) ->
 477          (*CSC manca la gestione degli universi!!! *)
 478          C.Sort C.Type
 479      | (C.Meta _,_) | (_,C.Meta _) ->
 480          (* TODO how can we force the meta to become a sort? If we don't we
 481           * brake the invariant that refine produce only well typed terms *)
 482          (* TODO if we check the non meta term and if it is a sort then we are
 483           * likely to know the exact value of the result e.g. if the rhs is a
 484           * Sort (Prop | Set | CProp) then the result is the rhs *)
 485          (C.Sort C.Type)
 486 (*           t2'' *)
 487      | (_,_) ->
 488          raise (NotRefinable (sprintf
 489           "Two types were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
 490           (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
 491           (CicPp.ppterm t2'')))
 492
 493  and eat_prods subst metasenv context hetype tlbody_and_type =
 494   let rec aux context' args (resty,subst,metasenv) =
 495    function
 496       [] -> resty,subst,metasenv
 497     | (arg,argty)::tl ->
 498        let args' =
 499         List.map
 500          (function
 501              None -> assert false
 502            | Some t -> Some (CicMetaSubst.lift subst 1 t)
 503          ) args in
 504        let argty' = CicMetaSubst.lift subst (List.length args) argty in
 505        let context'' = Some (Cic.Anonymous, Cic.Decl argty') :: context' in
 506        let (metasenv, idx) =
 507         CicMkImplicit.mk_implicit metasenv (context'' @ context) in
 508        let irl =
 509          (Some (Cic.Rel 1))::args' @
 510           (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
 511             context)
 512        in
 513        let newmeta = Cic.Meta (idx, irl) in
 514        let prod =
 515         Cic.Prod
 516          (FreshNamesGenerator.mk_fresh_name
 517            (CicMetaSubst.apply_subst_metasenv subst metasenv)
 518            (CicMetaSubst.apply_subst_context subst context)
 519            Cic.Anonymous
 520            (CicMetaSubst.apply_subst subst argty),
 521           argty, newmeta) in
 522        let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
 523        let (subst, metasenv) =
 524          CicUnification.fo_unif_subst subst context metasenv resty prod
 525        in
 526         aux context'' (Some arg :: args)
 527          (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
 528   in
 529    aux [] [] (hetype,subst,metasenv) tlbody_and_type
 530
 531  in
 532   let ty,subst',metasenv' =
 533    type_of_aux [] metasenv context t
 534   in
 535    (FreshNamesGenerator.clean_dummy_dependent_types
 536      (CicMetaSubst.apply_subst subst' t),
 537     FreshNamesGenerator.clean_dummy_dependent_types
 538      (CicMetaSubst.apply_subst subst' ty),
 539     CicMetaSubst.apply_subst_metasenv subst' metasenv')
 540 ;;
 541
 542 (* DEBUGGING ONLY *)
 543 let type_of_aux' metasenv context term =
 544  try
 545   let (t,ty,m) = type_of_aux' metasenv context term in
 546    debug_print
 547     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
 548 (*
 549    debug_print
 550     ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
 551 *)
 552    (t,ty,m)
 553  with
 554  | CicUnification.AssertFailure msg as e ->
 555      debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
 556      debug_print msg;
 557      raise e
 558  | CicUnification.UnificationFailure msg as e ->
 559      debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
 560      debug_print msg;
 561      raise e
 562  | e ->
 563    debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
 564    raise e
 565 ;;
 566