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