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