(* 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 UnificationFailure of string Lazy.t;;
exception Uncertain of string Lazy.t;;
exception AssertFailure of string Lazy.t;;

let verbose = false;;
let debug_print = fun _ -> () 

let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"

let type_of_aux' metasenv subst context term ugraph =
let foo () =
  try 
    CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph 
  with
      CicTypeChecker.TypeCheckerFailure msg ->
        let msg =
         lazy
          (sprintf
           "Kernel Type checking error: 
%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
             (CicMetaSubst.ppterm subst term)
             (CicMetaSubst.ppterm [] term)
             (CicMetaSubst.ppcontext subst context)
             (CicMetaSubst.ppmetasenv subst metasenv) 
             (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
        raise (AssertFailure msg)
    | CicTypeChecker.AssertFailure msg ->
        let msg = lazy
         (sprintf
           "Kernel Type checking assertion failure: 
%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
             (CicMetaSubst.ppterm subst term)
             (CicMetaSubst.ppterm [] term)
             (CicMetaSubst.ppcontext subst context)
             (CicMetaSubst.ppmetasenv subst metasenv) 
             (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in
        raise (AssertFailure msg)
in profiler_toa.HExtlib.profile foo ()
;;

let exists_a_meta l = 
  List.exists (function Cic.Meta _ -> true | _ -> false) l

let rec deref subst t =
  let snd (_,a,_) = a in
  match t with
      Cic.Meta(n,l) -> 
        (try 
           deref subst
             (CicSubstitution.subst_meta 
                l (snd (CicUtil.lookup_subst n subst))) 
         with 
             CicUtil.Subst_not_found _ -> t)
    | Cic.Appl(Cic.Meta(n,l)::args) ->
        (match deref subst (Cic.Meta(n,l)) with
           | Cic.Lambda _ as t -> 
               deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
           | r -> Cic.Appl(r::args))
    | Cic.Appl(((Cic.Lambda _) as t)::args) ->
           deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
    | t -> t
;; 

let deref subst t =
 let foo () = deref subst t
 in profiler_deref.HExtlib.profile foo ()

exception WrongShape;;
let eta_reduce after_beta_expansion after_beta_expansion_body
     before_beta_expansion
 =
 try
  match before_beta_expansion,after_beta_expansion_body with
     Cic.Appl l, Cic.Appl l' ->
      let rec all_but_last check_last =
       function
          [] -> assert false
        | [Cic.Rel 1] -> []
        | [_] -> if check_last then raise WrongShape else []
        | he::tl -> he::(all_but_last check_last tl)
      in
       let all_but_last check_last l =
        match all_but_last check_last l with
           [] -> assert false
         | [he] -> he
         | l -> Cic.Appl l
       in
       let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
       let all_but_last = all_but_last false l in
        (* here we should test alpha-equivalence; however we know by
           construction that here alpha_equivalence is equivalent to = *)
        if t = all_but_last then
         all_but_last
        else
         after_beta_expansion
   | _,_ -> after_beta_expansion
 with
  WrongShape -> after_beta_expansion

let rec beta_expand test_equality_only metasenv subst context t arg ugraph =
 let module S = CicSubstitution in
 let module C = Cic in
let foo () =
  let rec aux metasenv subst n context t' ugraph =
   try

    let subst,metasenv,ugraph1 =
     fo_unif_subst test_equality_only subst context metasenv 
      (CicSubstitution.lift n arg) t' ugraph

    in
     subst,metasenv,C.Rel (1 + n),ugraph1
   with
      Uncertain _
    | UnificationFailure _ ->
       match t' with
        | C.Rel m  -> subst,metasenv, 
           (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
        | C.Var (uri,exp_named_subst) ->
           let subst,metasenv,exp_named_subst',ugraph1 =
            aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
           in
            subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
        | C.Meta (i,l) ->
            (* andrea: in general, beta_expand can create badly typed
             terms. This happens quite seldom in practice, UNLESS we
             iterate on the local context. For this reason, we renounce
             to iterate and just lift *)
            let l = 
              List.map 
                (function
                     Some t -> Some (CicSubstitution.lift 1 t)
                   | None -> None) l in
            subst, metasenv, C.Meta (i,l), ugraph
        | C.Sort _
        | C.Implicit _ as t -> subst,metasenv,t,ugraph
        | C.Cast (te,ty) ->
            let subst,metasenv,te',ugraph1 = 
              aux metasenv subst n context te ugraph in
            let subst,metasenv,ty',ugraph2 = 
              aux metasenv subst n context ty ugraph1 in 
            (* TASSI: sure this is in serial? *)
            subst,metasenv,(C.Cast (te', ty')),ugraph2
        | C.Prod (nn,s,t) ->
           let subst,metasenv,s',ugraph1 = 
             aux metasenv subst n context s ugraph in
           let subst,metasenv,t',ugraph2 =
             aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t 
               ugraph1
           in
           (* TASSI: sure this is in serial? *)
           subst,metasenv,(C.Prod (nn, s', t')),ugraph2
        | C.Lambda (nn,s,t) ->
           let subst,metasenv,s',ugraph1 = 
             aux metasenv subst n context s ugraph in
           let subst,metasenv,t',ugraph2 =
            aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
           in
           (* TASSI: sure this is in serial? *)
            subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
        | C.LetIn (nn,s,t) ->
           let subst,metasenv,s',ugraph1 = 
             aux metasenv subst n context s ugraph in
           let subst,metasenv,t',ugraph2 =
            aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
              ugraph1
           in
           (* TASSI: sure this is in serial? *)
            subst,metasenv,(C.LetIn (nn, s', t')),ugraph2
        | C.Appl l ->
           let subst,metasenv,revl',ugraph1 =
            List.fold_left
             (fun (subst,metasenv,appl,ugraph) t ->
               let subst,metasenv,t',ugraph1 = 
                 aux metasenv subst n context t ugraph in
                subst,metasenv,(t'::appl),ugraph1
             ) (subst,metasenv,[],ugraph) l
           in
            subst,metasenv,(C.Appl (List.rev revl')),ugraph1
        | C.Const (uri,exp_named_subst) ->
           let subst,metasenv,exp_named_subst',ugraph1 =
            aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
           in
            subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
        | C.MutInd (uri,i,exp_named_subst) ->
           let subst,metasenv,exp_named_subst',ugraph1 =
            aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
           in
            subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
        | C.MutConstruct (uri,i,j,exp_named_subst) ->
           let subst,metasenv,exp_named_subst',ugraph1 =
            aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
           in
            subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
        | C.MutCase (sp,i,outt,t,pl) ->
           let subst,metasenv,outt',ugraph1 = 
             aux metasenv subst n context outt ugraph in
           let subst,metasenv,t',ugraph2 = 
             aux metasenv subst n context t ugraph1 in
           let subst,metasenv,revpl',ugraph3 =
            List.fold_left
             (fun (subst,metasenv,pl,ugraph) t ->
               let subst,metasenv,t',ugraph1 = 
                 aux metasenv subst n context t ugraph in
               subst,metasenv,(t'::pl),ugraph1
             ) (subst,metasenv,[],ugraph2) pl
           in
           subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
           (* TASSI: not sure this is serial *)
        | C.Fix (i,fl) ->
(*CSC: not implemented
           let tylen = List.length fl in
            let substitutedfl =
             List.map
              (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
               fl
            in
             C.Fix (i, substitutedfl)
*)
            subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
        | C.CoFix (i,fl) ->
(*CSC: not implemented
           let tylen = List.length fl in
            let substitutedfl =
             List.map
              (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
               fl
            in
             C.CoFix (i, substitutedfl)

*) 
            subst,metasenv,(CicSubstitution.lift 1 t'), ugraph

  and aux_exp_named_subst metasenv subst n context ens ugraph =
   List.fold_right
    (fun (uri,t) (subst,metasenv,l,ugraph) ->
      let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
       subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
  in
  let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
  let fresh_name =
   FreshNamesGenerator.mk_fresh_name ~subst
    metasenv context (Cic.Name "Hbeta") ~typ:argty
  in
   let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
   let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
   subst, metasenv, t'', ugraph2
in profiler_beta_expand.HExtlib.profile foo ()


and beta_expand_many test_equality_only metasenv subst context t args ugraph =
  let subst,metasenv,hd,ugraph =
    List.fold_right
      (fun arg (subst,metasenv,t,ugraph) ->
         let subst,metasenv,t,ugraph1 =
           beta_expand test_equality_only 
             metasenv subst context t arg ugraph 
         in
           subst,metasenv,t,ugraph1 
      ) args (subst,metasenv,t,ugraph) 
  in
    subst,metasenv,hd,ugraph


(* NUOVA UNIFICAZIONE *)
(* A substitution is a (int * Cic.term) list that associates a
   metavariable i with its body.
   A metaenv is a (int * Cic.term) list that associate a metavariable
   i with is type. 
   fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
   a new substitution which is _NOT_ unwinded. It must be unwinded before
   applying it. *)

and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =  
 let module C = Cic in
 let module R = CicReduction in
 let module S = CicSubstitution in
 let t1 = deref subst t1 in
 let t2 = deref subst t2 in
 let b,ugraph  = 
let foo () =
   R.are_convertible ~subst ~metasenv context t1 t2 ugraph 
in profiler_are_convertible.HExtlib.profile foo ()
 in
   if b then
     subst, metasenv, ugraph 
   else
   match (t1, t2) with
     | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
         let _,subst,metasenv,ugraph1 =
           (try
              List.fold_left2
                (fun (j,subst,metasenv,ugraph) t1 t2 ->
                   match t1,t2 with
                       None,_
                     | _,None -> j+1,subst,metasenv,ugraph
                     | Some t1', Some t2' ->
                         (* First possibility:  restriction    *)
                         (* Second possibility: unification    *)
                         (* Third possibility:  convertibility *)
                         let b, ugraph1 = 
                         R.are_convertible 
                           ~subst ~metasenv context t1' t2' ugraph
                         in
                         if b then
                           j+1,subst,metasenv, ugraph1 
                         else
                           (try
                              let subst,metasenv,ugraph2 =
                                fo_unif_subst 
                                  test_equality_only 
                                  subst context metasenv t1' t2' ugraph
                              in
                                j+1,subst,metasenv,ugraph2
                            with
                                Uncertain _
                              | UnificationFailure _ ->
debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j))); 
                                  let metasenv, subst = 
                                    CicMetaSubst.restrict 
                                      subst [(n,j)] metasenv in
                                    j+1,subst,metasenv,ugraph1)
                ) (1,subst,metasenv,ugraph) ln lm
            with
                Exit ->
                  raise 
                    (UnificationFailure (lazy "1"))
                    (*
                    (sprintf
                      "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
                      (CicMetaSubst.ppterm subst t1) 
                      (CicMetaSubst.ppterm subst t2))) *)
              | Invalid_argument _ ->
                  raise 
                    (UnificationFailure (lazy "2")))
                    (*
                    (sprintf
                      "Error trying to unify %s with %s: the lengths of the two local contexts do not match." 
                      (CicMetaSubst.ppterm subst t1) 
                      (CicMetaSubst.ppterm subst t2)))) *)
         in subst,metasenv,ugraph1
     | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
         fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
     | (C.Meta (n,l), t)   
     | (t, C.Meta (n,l)) ->
         let swap =
           match t1,t2 with
               C.Meta (n,_), C.Meta (m,_) when n < m -> false
             | _, C.Meta _ -> false
             | _,_ -> true
         in
         let lower = fun x y -> if swap then y else x in
         let upper = fun x y -> if swap then x else y in
         let fo_unif_subst_ordered 
             test_equality_only subst context metasenv m1 m2 ugraph =
           fo_unif_subst test_equality_only subst context metasenv 
             (lower m1 m2) (upper m1 m2) ugraph
         in
         begin
         let subst,metasenv,ugraph1 =
           let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
           (try
              let tyt,ugraph1 = 
                type_of_aux' metasenv subst context t ugraph 
              in
                fo_unif_subst 
                  test_equality_only 
                  subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
            with 
                UnificationFailure _ as e -> raise e
              | Uncertain msg -> raise (UnificationFailure msg)
              | AssertFailure _ ->
                  debug_print (lazy "siamo allo huge hack");
                  (* TODO huge hack!!!!
                   * we keep on unifying/refining in the hope that 
                   * the problem will be eventually solved. 
                   * In the meantime we're breaking a big invariant:
                   * the terms that we are unifying are no longer well 
                   * typed in the current context (in the worst case 
                   * we could even diverge) *)
                  (subst, metasenv,ugraph)) in
         let t',metasenv,subst =
           try 
             CicMetaSubst.delift n subst context metasenv l t
           with
               (CicMetaSubst.MetaSubstFailure msg)-> 
                 raise (UnificationFailure msg)
             | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
         in
         let t'',ugraph2 =
           match t' with
               C.Sort (C.Type u) when not test_equality_only ->
                 let u' = CicUniv.fresh () in
                 let s = C.Sort (C.Type u') in
                 let ugraph2 =   
                   CicUniv.add_ge (upper u u') (lower u u') ugraph1
                 in
                   s,ugraph2
             | _ -> t',ugraph1
         in
         (* Unifying the types may have already instantiated n. Let's check *)
         try
           let (_, oldt,_) = CicUtil.lookup_subst n subst in
           let lifted_oldt = S.subst_meta l oldt in
             fo_unif_subst_ordered 
               test_equality_only subst context metasenv t lifted_oldt ugraph2
         with
             CicUtil.Subst_not_found _ -> 
               let (_, context, ty) = CicUtil.lookup_meta n metasenv in
               let subst = (n, (context, t'',ty)) :: subst in
               let metasenv =
                 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
               subst, metasenv, ugraph2
         end
   | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
   | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
      if UriManager.eq uri1 uri2 then
       fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
        exp_named_subst1 exp_named_subst2 ugraph
      else
       raise (UnificationFailure (lazy 
          (sprintf
            "Can't unify %s with %s due to different constants"
            (CicMetaSubst.ppterm subst t1) 
            (CicMetaSubst.ppterm subst t2)))) 
   | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
       if UriManager.eq uri1 uri2 && i1 = i2 then
         fo_unif_subst_exp_named_subst 
           test_equality_only 
           subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
       else
         raise (UnificationFailure (lazy "4"))
           (* (sprintf
              "Can't unify %s with %s due to different inductive principles"
              (CicMetaSubst.ppterm subst t1) 
              (CicMetaSubst.ppterm subst t2))) *)
   | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
       C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
       if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
         fo_unif_subst_exp_named_subst
           test_equality_only 
           subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
       else
         raise (UnificationFailure (lazy "5"))
           (* (sprintf
              "Can't unify %s with %s due to different inductive constructors"
              (CicMetaSubst.ppterm subst t1) 
              (CicMetaSubst.ppterm subst t2))) *)
   | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
   | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only 
                              subst context metasenv te t2 ugraph
   | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only 
                              subst context metasenv t1 te ugraph
   | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> 
       let subst',metasenv',ugraph1 = 
         fo_unif_subst true subst context metasenv s1 s2 ugraph 
       in
         fo_unif_subst test_equality_only 
           subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
   | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> 
       let subst',metasenv',ugraph1 = 
         fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph 
       in
         fo_unif_subst test_equality_only 
           subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
   | (C.LetIn (_,s1,t1), t2)  
   | (t2, C.LetIn (_,s1,t1)) -> 
       fo_unif_subst 
        test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
   | (C.Appl l1, C.Appl l2) -> 
       (* andrea: this case should be probably rewritten in the 
          spirit of deref *)
       (match l1,l2 with
          | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
              (try 
                 List.fold_left2 
                   (fun (subst,metasenv,ugraph) t1 t2 ->
                      fo_unif_subst 
                        test_equality_only subst context metasenv t1 t2 ugraph)
                   (subst,metasenv,ugraph) l1 l2 
               with (Invalid_argument msg) -> 
                 raise (UnificationFailure (lazy msg)))
          | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
              (* we verify that none of the args is a Meta, 
                since beta expanding with respoect to a metavariable 
                makes no sense  *)
 (*
              (try 
                 let (_,t,_) = CicUtil.lookup_subst i subst in
                 let lifted = S.subst_meta l t in
                 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
                   fo_unif_subst 
                    test_equality_only 
                     subst context metasenv reduced t2 ugraph
               with CicUtil.Subst_not_found _ -> *)
              let subst,metasenv,beta_expanded,ugraph1 =
                beta_expand_many 
                  test_equality_only metasenv subst context t2 args ugraph 
              in
                fo_unif_subst test_equality_only subst context metasenv 
                  (C.Meta (i,l)) beta_expanded ugraph1
          | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
              (* (try 
                 let (_,t,_) = CicUtil.lookup_subst i subst in
                 let lifted = S.subst_meta l t in
                 let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
                   fo_unif_subst 
                     test_equality_only 
                     subst context metasenv t1 reduced ugraph
               with CicUtil.Subst_not_found _ -> *)
                 let subst,metasenv,beta_expanded,ugraph1 =
                   beta_expand_many 
                     test_equality_only 
                     metasenv subst context t1 args ugraph 
                 in
                   fo_unif_subst test_equality_only subst context metasenv 
                     (C.Meta (i,l)) beta_expanded ugraph1
          | _,_ ->
              let lr1 = List.rev l1 in
              let lr2 = List.rev l2 in
              let rec 
                  fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
                match (l1,l2) with
                    [],_
                  | _,[] -> assert false
                  | ([h1],[h2]) ->
                      fo_unif_subst 
                        test_equality_only subst context metasenv h1 h2 ugraph
                  | ([h],l) 
                  | (l,[h]) ->
                      fo_unif_subst test_equality_only subst context metasenv
                        h (C.Appl (List.rev l)) ugraph
                  | ((h1::l1),(h2::l2)) -> 
                      let subst', metasenv',ugraph1 = 
                        fo_unif_subst 
                          test_equality_only 
                          subst context metasenv h1 h2 ugraph
                      in 
                        fo_unif_l 
                          test_equality_only subst' metasenv' (l1,l2) ugraph1
              in
                fo_unif_l 
                  test_equality_only subst metasenv (lr1, lr2)  ugraph)
   | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
       let subst', metasenv',ugraph1 = 
        fo_unif_subst test_equality_only subst context metasenv outt1 outt2
          ugraph in
       let subst'',metasenv'',ugraph2 = 
        fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
          ugraph1 in
       (try
         List.fold_left2 
          (fun (subst,metasenv,ugraph) t1 t2 ->
            fo_unif_subst 
             test_equality_only subst context metasenv t1 t2 ugraph
          ) (subst'',metasenv'',ugraph2) pl1 pl2 
        with
         Invalid_argument _ ->
          raise (UnificationFailure (lazy "6.1")))
           (* (sprintf
              "Error trying to unify %s with %s: the number of branches is not the same." 
              (CicMetaSubst.ppterm subst t1) 
              (CicMetaSubst.ppterm subst t2)))) *)
   | (C.Rel _, _) | (_,  C.Rel _) ->
       if t1 = t2 then
         subst, metasenv,ugraph
       else
        raise (UnificationFailure (lazy 
           (sprintf
             "Can't unify %s with %s because they are not convertible"
             (CicMetaSubst.ppterm subst t1) 
             (CicMetaSubst.ppterm subst t2))))
   | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
       let subst,metasenv,beta_expanded,ugraph1 =
         beta_expand_many 
           test_equality_only metasenv subst context t2 args ugraph 
       in
         fo_unif_subst test_equality_only subst context metasenv 
           (C.Meta (i,l)) beta_expanded ugraph1
   | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
       let subst,metasenv,beta_expanded,ugraph1 =
         beta_expand_many 
           test_equality_only metasenv subst context t1 args ugraph 
       in
         fo_unif_subst test_equality_only subst context metasenv 
           beta_expanded (C.Meta (i,l)) ugraph1
   | (C.Sort _ ,_) | (_, C.Sort _)
   | (C.Const _, _) | (_, C.Const _)
   | (C.MutInd  _, _) | (_, C.MutInd _)
   | (C.MutConstruct _, _) | (_, C.MutConstruct _)
   | (C.Fix _, _) | (_, C.Fix _) 
   | (C.CoFix _, _) | (_, C.CoFix _) -> 
       if t1 = t2 then
         subst, metasenv, ugraph
       else 
         let b,ugraph1 = 
           R.are_convertible ~subst ~metasenv context t1 t2 ugraph 
         in
           if b then 
             subst, metasenv, ugraph1
           else
             raise
                (UnificationFailure (lazy (sprintf
                  "Can't unify %s with %s because they are not convertible"
                  (CicMetaSubst.ppterm subst t1) 
                  (CicMetaSubst.ppterm subst t2))))
   | (C.Prod _, t2) ->
       let t2' = R.whd ~subst context t2 in
       (match t2' with
            C.Prod _ -> 
              fo_unif_subst test_equality_only 
                subst context metasenv t1 t2' ugraph         
          | _ -> raise (UnificationFailure (lazy "8")))
   | (t1, C.Prod _) ->
       let t1' = R.whd ~subst context t1 in
       (match t1' with
            C.Prod _ -> 
              fo_unif_subst test_equality_only 
                subst context metasenv t1' t2 ugraph         
          | _ -> (* raise (UnificationFailure "9")) *)
             raise 
                (UnificationFailure (lazy (sprintf
                   "Can't unify %s with %s because they are not convertible"
                   (CicMetaSubst.ppterm subst t1) 
                   (CicMetaSubst.ppterm subst t2)))))
   | (_,_) ->
       raise (UnificationFailure (lazy "10"))
         (* (sprintf
            "Can't unify %s with %s because they are not convertible"
            (CicMetaSubst.ppterm subst t1) 
            (CicMetaSubst.ppterm subst t2))) *)

and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 exp_named_subst1 exp_named_subst2 ugraph
=
 try
  List.fold_left2
   (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
     assert (uri1=uri2) ;
     fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
   ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
 with
  Invalid_argument _ ->
   let print_ens ens =
    String.concat " ; "
     (List.map
       (fun (uri,t) ->
         UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t)
       ) ens) 
   in
    raise (UnificationFailure (lazy (sprintf
     "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2))))

(* A substitution is a (int * Cic.term) list that associates a               *)
(* metavariable i with its body.                                             *)
(* metasenv is of type Cic.metasenv                                          *)
(* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
(* a new substitution which is already unwinded and ready to be applied and  *)
(* a new metasenv in which some hypothesis in the contexts of the            *)
(* metavariables may have been restricted.                                   *)
let fo_unif metasenv context t1 t2 ugraph = 
 fo_unif_subst false [] context metasenv t1 t2 ugraph ;;

let enrich_msg msg subst context metasenv t1 t2 ugraph =
 lazy (
  if verbose then
   sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
    (CicMetaSubst.ppterm subst t1)
    (try
      let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
      CicPp.ppterm ty_t1
    with 
    | UnificationFailure s
    | Uncertain s
    | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
    (CicMetaSubst.ppterm subst t2)
    (try
      let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
      CicPp.ppterm ty_t2
    with
    | UnificationFailure s
    | Uncertain s
    | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
    (CicMetaSubst.ppcontext subst context)
    (CicMetaSubst.ppmetasenv subst metasenv)
    (CicMetaSubst.ppsubst subst) (Lazy.force msg)
 else
   sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
    (CicMetaSubst.ppterm_in_context subst t1 context)
    (try
      let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
      CicMetaSubst.ppterm_in_context subst ty_t1 context
    with 
    | UnificationFailure s
    | Uncertain s
    | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
    (CicMetaSubst.ppterm_in_context subst t2 context)
    (try
      let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
      CicMetaSubst.ppterm_in_context subst ty_t2 context
    with
    | UnificationFailure s
    | Uncertain s
    | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
    (CicMetaSubst.ppcontext subst context)
    (CicMetaSubst.ppmetasenv subst metasenv)
    (Lazy.force msg)
 )

let fo_unif_subst subst context metasenv t1 t2 ugraph =
  try
    fo_unif_subst false subst context metasenv t1 t2 ugraph
  with
  | AssertFailure msg ->
     raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
  | UnificationFailure msg ->
     raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
;;