(* Copyright (C) 2000, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 *)

open Printf

exception RefineFailure of string;;

exception Impossible of int;;
exception NotRefinable of string;;
exception Uncertain of string;;
exception WrongUriToConstant of string;;
exception WrongUriToVariable of string;;
exception ListTooShort;;
exception WrongUriToMutualInductiveDefinitions of string;;
exception RelToHiddenHypothesis;;
exception WrongArgumentNumber;;

let fdebug = ref 0;;
let debug t context =
 let rec debug_aux t i =
  let module C = Cic in
  let module U = UriManager in
   CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
 in
  if !fdebug = 0 then
   raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) ""))
   (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
;;

let debug_print = prerr_endline

let rec split l n =
 match (l,n) with
    (l,0) -> ([], l)
  | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  | (_,_) -> raise ListTooShort
;;

let rec type_of_constant uri =
 let module C = Cic in
 let module R = CicReduction in
 let module U = UriManager in
  match CicEnvironment.get_cooked_obj uri with
     C.Constant (_,_,ty,_) -> ty
   | C.CurrentProof (_,_,_,ty,_) -> ty
   | _ -> raise (WrongUriToConstant (U.string_of_uri uri))

and type_of_variable uri =
 let module C = Cic in
 let module R = CicReduction in
 let module U = UriManager in
  match CicEnvironment.get_cooked_obj uri with
     C.Variable (_,_,ty,_) -> ty
   |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))

and type_of_mutual_inductive_defs uri i =
 let module C = Cic in
 let module R = CicReduction in
 let module U = UriManager in
  match CicEnvironment.get_cooked_obj uri with
     C.InductiveDefinition (dl,_,_) ->
      let (_,_,arity,_) = List.nth dl i in
       arity
   | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))

and type_of_mutual_inductive_constr uri i j =
 let module C = Cic in
 let module R = CicReduction in
 let module U = UriManager in
  match CicEnvironment.get_cooked_obj uri with
      C.InductiveDefinition (dl,_,_) ->
       let (_,_,_,cl) = List.nth dl i in
        let (_,ty) = List.nth cl (j-1) in
         ty
   | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))

(* type_of_aux' is just another name (with a different scope) for type_of_aux *)

(* the check_branch function checks if a branch of a case is refinable. 
   It returns a pair (outype_instance,args), a subst and a metasenv.
   outype_instance is the expected result of applying the case outtype 
   to args. 
   The problem is that outype is in general unknown, and we should
   try to synthesize it from the above information, that is in general
   a second order unification problem. *)
 
and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
  let module C = Cic in
  let module R = CicMetaSubst in
  let module Un = CicUnification in 
  match R.whd subst context expectedtype with
     C.MutInd (_,_,_) ->
       (n,context,actualtype, [term]), subst, metasenv
   | C.Appl (C.MutInd (_,_,_)::tl) ->
       let (_,arguments) = split tl left_args_no in
       (n,context,actualtype, arguments@[term]), subst, metasenv
   | C.Prod (name,so,de) ->
      (* we expect that the actual type of the branch has the due 
         number of Prod *)
      (match R.whd subst context actualtype with
           C.Prod (name',so',de') ->
             let subst, metasenv = 
                Un.fo_unif_subst subst context metasenv so so' in
             let term' =
               (match CicSubstitution.lift 1 term with
                   C.Appl l -> C.Appl (l@[C.Rel 1])
                 | t -> C.Appl [t ; C.Rel 1]) in
             (* we should also check that the name variable is anonymous in
             the actual type de' ?? *)
             check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de 
	 | _ -> raise WrongArgumentNumber)
  | _ -> raise (NotRefinable "Prod or MutInd expected")

and type_of_aux' metasenv context t =
 let rec type_of_aux subst metasenv context =
  let module C = Cic in
  let module S = CicSubstitution in
  let module U = UriManager in
  let module Un = CicUnification in
   function
      C.Rel n ->
       (try
         match List.nth context (n - 1) with
            Some (_,C.Decl t) -> S.lift n t,subst,metasenv
          | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
          | Some (_,C.Def (bo,None)) ->
             type_of_aux subst metasenv context (S.lift n bo)
	  | None -> raise RelToHiddenHypothesis
        with
         _ -> raise (NotRefinable "Not a close term")
       )
    | C.Var (uri,exp_named_subst) ->
      incr fdebug ;
      let subst',metasenv' =
       check_exp_named_subst subst metasenv context exp_named_subst in
      let ty =
       CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
      in
       decr fdebug ;
       ty,subst',metasenv'
    | C.Meta (n,l) -> 
       let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
        let subst',metasenv' =
         check_metasenv_consistency n subst metasenv context canonical_context l
        in
        CicSubstitution.lift_meta l ty, subst', metasenv'
    | C.Sort s ->
       C.Sort C.Type, (*CSC manca la gestione degli universi!!! *)
        subst,metasenv
    | C.Implicit _ -> raise (Impossible 21)
    | C.Cast (te,ty) ->
       let _,subst',metasenv' =
        type_of_aux subst metasenv context ty in
       let inferredty,subst'',metasenv'' =
        type_of_aux subst' metasenv' context te
       in
        (try
          let subst''',metasenv''' =
           Un.fo_unif_subst subst'' context metasenv'' inferredty ty
          in
           ty,subst''',metasenv'''
         with
          _ -> raise (NotRefinable "Cast"))
    | C.Prod (name,s,t) ->
       let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
       let sort2,subst'',metasenv'' =
        type_of_aux subst' metasenv' ((Some (name,(C.Decl s)))::context) t
       in
        sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
   | C.Lambda (n,s,t) ->
       let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
       let type2,subst'',metasenv'' =
        type_of_aux subst' metasenv' ((Some (n,(C.Decl s)))::context) t
       in
        let sort2,subst''',metasenv''' =
         type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
        in
         (* only to check if the product is well-typed *)
         let _,subst'''',metasenv'''' =
          sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
         in
          C.Prod (n,s,type2),subst'''',metasenv''''
   | C.LetIn (n,s,t) ->
      (* only to check if s is well-typed *)
      let ty,subst',metasenv' = type_of_aux subst metasenv context s in
      let inferredty,subst'',metasenv'' =
       type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
      in
       (* One-step LetIn reduction. Even faster than the previous solution.
          Moreover the inferred type is closer to the expected one. *)
       CicSubstitution.subst s inferredty,subst',metasenv'
   | C.Appl (he::tl) when List.length tl > 0 ->
      let hetype,subst',metasenv' = type_of_aux subst metasenv context he in
      let tlbody_and_type,subst'',metasenv'' =
       List.fold_right
        (fun x (res,subst,metasenv) ->
          let ty,subst',metasenv' =
           type_of_aux subst metasenv context x
          in
           (x, ty)::res,subst',metasenv'
        ) tl ([],subst',metasenv')
      in
       eat_prods subst'' metasenv'' context hetype tlbody_and_type
   | C.Appl _ -> raise (NotRefinable "Appl: no arguments")
   | C.Const (uri,exp_named_subst) ->
      incr fdebug ;
      let subst',metasenv' =
       check_exp_named_subst subst metasenv context exp_named_subst in
      let cty =
       CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
      in
       decr fdebug ;
       cty,subst',metasenv'
   | C.MutInd (uri,i,exp_named_subst) ->
      incr fdebug ;
      let subst',metasenv' =
       check_exp_named_subst subst metasenv context exp_named_subst in
      let cty =
       CicSubstitution.subst_vars exp_named_subst
        (type_of_mutual_inductive_defs uri i)
      in
       decr fdebug ;
       cty,subst',metasenv'
   | C.MutConstruct (uri,i,j,exp_named_subst) ->
      let subst',metasenv' =
       check_exp_named_subst subst metasenv context exp_named_subst in
      let cty =
       CicSubstitution.subst_vars exp_named_subst
        (type_of_mutual_inductive_constr uri i j)
      in
       cty,subst',metasenv'
   | C.MutCase (uri, i, outtype, term, pl) ->
       (* first, get the inductive type (and noparams) in the environment  *)
       let (_,b,arity,constructors), expl_params, no_left_params =
         match CicEnvironment.get_cooked_obj ~trust:true uri with
            C.InductiveDefinition (l,expl_params,parsno) -> 
              List.nth l i , expl_params, parsno
          | _ ->
            raise
             (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in
       let rec count_prod t =
         match CicMetaSubst.whd subst context t with
             C.Prod (_, _, t) -> 1 + (count_prod t)
           | _ -> 0 in 
       let no_args = count_prod arity in
       (* now, create a "generic" MutInd *)
       let metasenv,left_args = 
         CicMkImplicit.n_fresh_metas metasenv context no_left_params in
       let metasenv,right_args = 
         let no_right_params = no_args - no_left_params in
         if no_right_params < 0 then assert false
         else CicMkImplicit.n_fresh_metas metasenv context no_right_params in
       let metasenv,exp_named_subst = 
         CicMkImplicit.fresh_subst metasenv context expl_params in
       let expected_type = 
         if no_args = 0 then 
           C.MutInd (uri,i,exp_named_subst)
         else
	   C.Appl (C.MutInd (uri,i,exp_named_subst)::(left_args @ right_args))
       in
       (* check consistency with the actual type of term *)
       let actual_type,subst,metasenv = 
         type_of_aux subst metasenv context term in
       let _, subst, metasenv =
         type_of_aux subst metasenv context expected_type
       in
       let actual_type = CicMetaSubst.whd subst context actual_type in
       let subst,metasenv =
         Un.fo_unif_subst subst context metasenv expected_type actual_type
       in
       (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *)
       let (_,outtypeinstances,subst,metasenv) =
          List.fold_left
           (fun (j,outtypeinstances,subst,metasenv) p ->
             let constructor =
              if left_args = [] then
               (C.MutConstruct (uri,i,j,exp_named_subst))
              else
               (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::left_args))
             in
             let actual_type,subst,metasenv = 
               type_of_aux subst metasenv context p in
             let expected_type, subst, metasenv = 
               type_of_aux subst metasenv context constructor in
             let outtypeinstance,subst,metasenv =
               check_branch 
                0 context metasenv subst 
                no_left_params actual_type constructor expected_type in
             (j+1,outtypeinstance::outtypeinstances,subst,metasenv))
            (1,[],subst,metasenv) pl in
        (* we are left to check that the outype matches his instances.
           The easy case is when the outype is specified, that amount
           to a trivial check. Otherwise, we should guess a type from
           its instances *)
        (* easy case *)
        let _, subst, metasenv =
          type_of_aux subst metasenv context
            (C.Appl ((outtype :: right_args) @ [term]))
        in
        let (subst,metasenv) = 
          List.fold_left
            (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
              let instance' = 
                let appl =
                  let outtype' =
                    CicSubstitution.lift constructor_args_no outtype
                  in
                  C.Appl (outtype'::args)
                in
(*
                (* if appl is not well typed then the type_of below solves the
                 * problem *)
                let (_, subst, metasenv) =
                  type_of_aux subst metasenv context appl
                in
*)
                CicMetaSubst.whd subst context appl
              in
               Un.fo_unif_subst subst context metasenv instance instance')
             (subst,metasenv) outtypeinstances in
        CicMetaSubst.whd subst
          context (C.Appl(outtype::right_args@[term])),subst,metasenv
   | C.Fix (i,fl) ->
      let subst,metasenv,types =
       List.fold_left
        (fun (subst,metasenv,types) (n,_,ty,_) ->
          let _,subst',metasenv' = type_of_aux subst metasenv context ty in
           subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
        ) (subst,metasenv,[]) fl
      in
       let len = List.length types in
       let context' = types@context in
       let subst,metasenv =
        List.fold_left
         (fun (subst,metasenv) (name,x,ty,bo) ->
           let ty_of_bo,subst,metasenv =
            type_of_aux subst metasenv context' bo
           in
            Un.fo_unif_subst subst context' metasenv
              ty_of_bo (CicMetaSubst.lift subst len ty)
         ) (subst,metasenv) fl in
        let (_,_,ty,_) = List.nth fl i in
         ty,subst,metasenv
   | C.CoFix (i,fl) ->
      let subst,metasenv,types =
       List.fold_left
        (fun (subst,metasenv,types) (n,ty,_) ->
          let _,subst',metasenv' = type_of_aux subst metasenv context ty in
           subst',metasenv', Some (C.Name n,(C.Decl ty)) :: types
        ) (subst,metasenv,[]) fl
      in
       let len = List.length types in
       let context' = types@context in
       let subst,metasenv =
        List.fold_left
         (fun (subst,metasenv) (name,ty,bo) ->
           let ty_of_bo,subst,metasenv =
            type_of_aux subst metasenv context' bo
           in
            Un.fo_unif_subst subst context' metasenv
              ty_of_bo (CicMetaSubst.lift subst len ty)
         ) (subst,metasenv) fl in
      
        let (_,ty,_) = List.nth fl i in
         ty,subst,metasenv

 (* check_metasenv_consistency checks that the "canonical" context of a
 metavariable is consitent - up to relocation via the relocation list l -
 with the actual context *)
 and check_metasenv_consistency
  metano subst metasenv context canonical_context l
 =
   let module C = Cic in
   let module R = CicReduction in
   let module S = CicSubstitution in
    let lifted_canonical_context = 
     let rec aux i =
      function
         [] -> []
       | (Some (n,C.Decl t))::tl ->
          (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
       | (Some (n,C.Def (t,None)))::tl ->
          (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
       | None::tl -> None::(aux (i+1) tl)
       | (Some (n,C.Def (t,Some ty)))::tl ->
           (Some (n,
            C.Def ((S.lift_meta l (S.lift i t)),
              Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
     in
      aux 1 canonical_context
    in
     List.fold_left2 
      (fun (subst,metasenv) t ct -> 
        match (t,ct) with
           _,None ->
             subst,metasenv
         | Some t,Some (_,C.Def (ct,_)) ->
            (try
              CicUnification.fo_unif_subst subst context metasenv t ct
             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)))))
         | Some t,Some (_,C.Decl ct) ->
            let inferredty,subst',metasenv' =
             type_of_aux subst metasenv context t
            in
             (try
               CicUnification.fo_unif_subst
                subst' context metasenv' inferredty ct
             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)))))
         | None, Some _  ->
             raise (NotRefinable (sprintf
              "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"
              (CicMetaSubst.ppterm subst (Cic.Meta (metano, l)))
              (CicMetaSubst.ppcontext subst canonical_context)))
      ) (subst,metasenv) l lifted_canonical_context 

 and check_exp_named_subst metasubst metasenv context =
  let rec check_exp_named_subst_aux metasubst metasenv substs =
   function
      [] -> metasubst,metasenv
    | ((uri,t) as subst)::tl ->
       let typeofvar =
        CicSubstitution.subst_vars substs (type_of_variable uri) in
       (match CicEnvironment.get_cooked_obj ~trust:false uri with
           Cic.Variable (_,Some bo,_,_) ->
            raise
             (NotRefinable
               "A variable with a body can not be explicit substituted")
         | Cic.Variable (_,None,_,_) -> ()
         | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
       ) ;
       let typeoft,metasubst',metasenv' =
        type_of_aux metasubst metasenv context t
       in
        try
         let metasubst'',metasenv'' =
          CicUnification.fo_unif_subst
           metasubst' context metasenv' typeoft typeofvar
         in
          check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl
        with _ ->
         raise (NotRefinable "Wrong Explicit Named Substitution")
  in
   check_exp_named_subst_aux metasubst metasenv []

 and sort_of_prod subst metasenv context (name,s) (t1, t2) =
  let module C = Cic in
    let context_for_t2 = (Some (name,C.Decl s))::context in
    let t1'' = CicMetaSubst.whd subst context t1 in
    let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in
    match (t1'', t2'') with
       (C.Sort s1, C.Sort s2)
         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
          C.Sort s2,subst,metasenv
     | (C.Sort s1, C.Sort s2) ->
         (*CSC manca la gestione degli universi!!! *)
         C.Sort C.Type,subst,metasenv
     | (C.Meta _, C.Sort _) -> t2'',subst,metasenv
     | (C.Sort _,C.Meta _) | (C.Meta _,C.Meta _) ->
         (* TODO how can we force the meta to become a sort? If we don't we
          * brake the invariant that refine produce only well typed terms *)
         (* TODO if we check the non meta term and if it is a sort then we are
          * likely to know the exact value of the result e.g. if the rhs is a
          * Sort (Prop | Set | CProp) then the result is the rhs *)
         let (metasenv,idx) =
          CicMkImplicit.mk_implicit_sort metasenv in
         let (subst, metasenv) =
          CicUnification.fo_unif_subst subst context_for_t2 metasenv
           (C.Meta (idx,[])) t2''
         in
          t2'',subst,metasenv
     | (_,_) ->
         raise (NotRefinable (sprintf
          "Two types were expected, found %s (that reduces to %s) and %s (that reduces to %s)"
          (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2)
          (CicPp.ppterm t2'')))

 and eat_prods subst metasenv context hetype tlbody_and_type =
  let rec aux context' args (resty,subst,metasenv) =
   function
      [] -> resty,subst,metasenv
    | (arg,argty)::tl ->
       let args' =
        List.map
         (function
             None -> assert false
           | Some t -> Some (CicMetaSubst.lift subst 1 t)
         ) args in
       let argty' = CicMetaSubst.lift subst (List.length args) argty in
       let name =
        (* The name must be fresh for (context'@context).      *)
        (* Nevertheless, argty is well-typed only in context.  *)
        (* Thus I generate a name (name_hint) in context and   *)
        (* then I generate a name --- using the hint name_hint *)
        (* --- that is fresh in (context'@context).            *)
        let name_hint =
         FreshNamesGenerator.mk_fresh_name
          (CicMetaSubst.apply_subst_metasenv subst metasenv)
          (CicMetaSubst.apply_subst_context subst context)
          Cic.Anonymous
          (CicMetaSubst.apply_subst subst argty)
        in
         (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
         FreshNamesGenerator.mk_fresh_name
          [] (context'@context) name_hint (Cic.Sort Cic.Prop)
       in
       let context'' = Some (name, Cic.Decl argty') :: context' in
       let (metasenv, idx) =
        CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
       let irl =
         (Some (Cic.Rel 1))::args' @
          (CicMkImplicit.identity_relocation_list_for_metavariable ~start:2
            context)
       in
       let newmeta = Cic.Meta (idx, irl) in
       let prod = Cic.Prod (name, argty, newmeta) in
       let (_, subst, metasenv) = type_of_aux subst metasenv context prod in
       let (subst, metasenv) =
         CicUnification.fo_unif_subst subst context metasenv resty prod
       in
        aux context'' (Some arg :: args)
         (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl
  in
   aux [] [] (hetype,subst,metasenv) tlbody_and_type

 in
  let ty,subst',metasenv' =
   type_of_aux [] metasenv context t
  in
   let substituted_t = CicMetaSubst.apply_subst subst' t in
   let substituted_ty = CicMetaSubst.apply_subst subst' ty in
   let substituted_metasenv =
    CicMetaSubst.apply_subst_metasenv subst' metasenv'
   in
    let cleaned_t =
     FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
    let cleaned_ty =
     FreshNamesGenerator.clean_dummy_dependent_types substituted_ty in
    let cleaned_metasenv =
     List.map
      (function (n,context,ty) ->
        let ty' = FreshNamesGenerator.clean_dummy_dependent_types ty in
        let context' =
         List.map
          (function
              None -> None
            | Some (n, Cic.Decl t) ->
               Some (n,
                Cic.Decl (FreshNamesGenerator.clean_dummy_dependent_types t))
            | Some (n, Cic.Def (bo,ty)) ->
               let bo' = FreshNamesGenerator.clean_dummy_dependent_types bo in
               let ty' =
                match ty with
                   None -> None
                 | Some ty ->
                    Some (FreshNamesGenerator.clean_dummy_dependent_types ty)
               in
                Some (n, Cic.Def (bo',ty'))
          ) context
        in
         (n,context',ty')
      ) substituted_metasenv
    in
     (cleaned_t,cleaned_ty,cleaned_metasenv)

;;

(* DEBUGGING ONLY *)
let type_of_aux' metasenv context term =
 try
  let (t,ty,m) = type_of_aux' metasenv context term in
   debug_print
    ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
(*
   debug_print
    ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
*)
   (t,ty,m)
 with
 | CicUnification.AssertFailure msg as e ->
     debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:";
     debug_print msg;
     raise e
 | CicUnification.UnificationFailure msg as e ->
     debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:";
     debug_print msg;
     raise e
 | e ->
   debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ;
   raise e
;;