(* 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/.
 *)

exception UnificationFailed;;
exception Free;;
exception OccurCheck;;
exception RelToHiddenHypothesis;;
exception OpenTerm;;

(**** DELIFT ****)

(* the delift function takes in input an ordered list of integers [n1,...,nk]
   and a term t, and relocates rel(nk) to k. Typically, the list of integers 
   is a parameter of a metavariable occurrence. *)

exception NotInTheList;;

let position n =
  let rec aux k =
   function 
       [] -> raise NotInTheList
     | (Some (Cic.Rel m))::_ when m=n -> k
     | _::tl -> aux (k+1) tl in
  aux 1
;;
 
let restrict to_be_restricted =
  let rec erase i n = 
    function
        [] -> []
      |        _::tl when List.mem (n,i) to_be_restricted ->
          None::(erase (i+1) n tl) 
      | he::tl -> he::(erase (i+1) n tl) in
  let rec aux =
    function 
        [] -> []
      |        (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
  aux
;;


let delift context metasenv l t =
 let module S = CicSubstitution in
  let to_be_restricted = ref [] in
  let rec deliftaux k =
   let module C = Cic in
    function
       C.Rel m -> 
         if m <=k then
          C.Rel m   (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
                    (*CSC: deliftato la regola per il LetIn                 *)
         else
          (match List.nth context (m-k-1) with
            Some (_,C.Def (t,_)) -> deliftaux k (S.lift m t)
          | Some (_,C.Decl t) ->
             (* It may augment to_be_restricted *)
             ignore (deliftaux k (S.lift m t)) ;
             C.Rel ((position (m-k) l) + k)
          | None -> raise RelToHiddenHypothesis)
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst' =
         List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
        in
         C.Var (uri,exp_named_subst')
     | C.Meta (i, l1) as t -> 
        let rec deliftl j =
         function
            [] -> []
          | None::tl -> None::(deliftl (j+1) tl)
          | (Some t)::tl ->
             let l1' = (deliftl (j+1) tl) in
              try
               Some (deliftaux k t)::l1'
              with
                 RelToHiddenHypothesis
               | NotInTheList ->
                  to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
        in
         let l' = deliftl 1 l1 in
          C.Meta(i,l')
     | C.Sort _ as t -> t
     | C.Implicit as t -> t
     | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
     | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
     | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
     | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
     | C.Appl l -> C.Appl (List.map (deliftaux k) l)
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' =
         List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
        in
         C.Const (uri,exp_named_subst')
     | C.MutInd (uri,typeno,exp_named_subst) ->
        let exp_named_subst' =
         List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
        in
         C.MutInd (uri,typeno,exp_named_subst')
     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
        let exp_named_subst' =
         List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
        in
         C.MutConstruct (uri,typeno,consno,exp_named_subst')
     | C.MutCase (sp,i,outty,t,pl) ->
        C.MutCase (sp, i, deliftaux k outty, deliftaux k t,
         List.map (deliftaux k) pl)
     | C.Fix (i, fl) ->
        let len = List.length fl in
        let liftedfl =
         List.map
          (fun (name, i, ty, bo) ->
           (name, i, deliftaux k ty, deliftaux (k+len) bo))
           fl
        in
         C.Fix (i, liftedfl)
     | C.CoFix (i, fl) ->
        let len = List.length fl in
        let liftedfl =
         List.map
          (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
           fl
        in
         C.CoFix (i, liftedfl)
  in
    let res = deliftaux 0 t in
    res, restrict !to_be_restricted metasenv
;;

(**** END OF DELIFT ****)

type substitution = (int * Cic.term) list

(* 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. *)
 
let rec fo_unif_subst subst context metasenv t1 t2 =  
 let module C = Cic in
 let module R = CicReduction in
 let module S = CicSubstitution in
  match (t1, t2) with
     (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
       let ok =
        List.fold_left2
         (fun b t1 t2 ->
           b &&
            match t1,t2 with
               None,_
             | _,None -> true
             | Some t1', Some t2' ->
                (* First possibility:  restriction    *)
                (* Second possibility: unification    *)
                (* Third possibility:  convertibility *)
                R.are_convertible context t1' t2'
         ) true ln lm
       in
        if ok then subst,metasenv else raise UnificationFailed
   | (C.Meta (n,l), C.Meta (m,_)) when n>m ->
       fo_unif_subst subst context metasenv t2 t1
   | (C.Meta (n,l), t)   
   | (t, C.Meta (n,l)) ->
       let subst',metasenv' =
        try
         let oldt = (List.assoc n subst) in
         let lifted_oldt = S.lift_meta l oldt in
          fo_unif_subst subst context metasenv lifted_oldt t
        with Not_found ->
         let t',metasenv' = delift context metasenv l t in
          (n, t')::subst, metasenv'
       in
        let (_,_,meta_type) = 
         List.find (function (m,_,_) -> m=n) metasenv' in
        let tyt = CicTypeChecker.type_of_aux' metasenv' context t in
         fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
   | (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 subst context metasenv
        exp_named_subst1 exp_named_subst2
      else
       raise UnificationFailed
   | 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 subst context metasenv
        exp_named_subst1 exp_named_subst2
      else
       raise UnificationFailed
   | 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 subst context metasenv
        exp_named_subst1 exp_named_subst2
      else
       raise UnificationFailed
   | (C.Rel _, _)
   | (_,  C.Rel _) 
   | (C.Var _, _)
   | (_, C.Var _) 
   | (C.Sort _ ,_)
   | (_, C.Sort _)
   | (C.Implicit, _)
   | (_, C.Implicit) -> 
       if R.are_convertible context t1 t2 then
        subst, metasenv
       else
        raise UnificationFailed
   | (C.Cast (te,ty), t2) -> fo_unif_subst subst context metasenv te t2
   | (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te
   | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> 
       let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in
        fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
   | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> 
       let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in
        fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2
   | (C.LetIn (_,s1,t1), t2)  
   | (t2, C.LetIn (_,s1,t1)) -> 
       fo_unif_subst subst context metasenv t2 (S.subst s1 t1)
   | (C.Appl l1, C.Appl l2) -> 
       let lr1 = List.rev l1 in
       let lr2 = List.rev l2 in
       let rec fo_unif_l subst metasenv =
        function
           [],_
         | _,[] -> assert false
         | ([h1],[h2]) ->
             fo_unif_subst subst context metasenv h1 h2
         | ([h],l) 
         | (l,[h]) ->
             fo_unif_subst subst context metasenv h (C.Appl (List.rev l))
         | ((h1::l1),(h2::l2)) -> 
            let subst', metasenv' = 
             fo_unif_subst subst context metasenv h1 h2
            in 
             fo_unif_l subst' metasenv' (l1,l2)
       in
        fo_unif_l subst metasenv (lr1, lr2) 
   | (C.Const _, _) 
   | (_, C.Const _)
   | (C.MutInd  _, _) 
   | (_, C.MutInd _)
   | (C.MutConstruct _, _)
   | (_, C.MutConstruct _) -> 
      if R.are_convertible context t1 t2 then
       subst, metasenv
      else
       raise UnificationFailed
   | (C.MutCase (_,_,outt1,t1,pl1), C.MutCase (_,_,outt2,t2,pl2))->
       let subst', metasenv' = 
        fo_unif_subst subst context metasenv outt1 outt2 in
       let subst'',metasenv'' = 
        fo_unif_subst subst' context metasenv' t1 t2 in
       List.fold_left2 
        (function (subst,metasenv) ->
          fo_unif_subst subst context metasenv
        ) (subst'',metasenv'') pl1 pl2 
   | (C.Fix _, _)
   | (_, C.Fix _) 
   | (C.CoFix _, _)
   | (_, C.CoFix _) -> 
       if R.are_convertible context t1 t2 then
        subst, metasenv
       else
        raise UnificationFailed
   | (_,_) ->
       if R.are_convertible context t1 t2 then
        subst, metasenv
       else
        raise UnificationFailed

and fo_unif_subst_exp_named_subst subst context metasenv
 exp_named_subst1 exp_named_subst2
=
try
 List.fold_left2
  (fun (subst,metasenv) (uri1,t1) (uri2,t2) ->
    assert (uri1=uri2) ;
    fo_unif_subst subst context metasenv t1 t2
  ) (subst,metasenv) exp_named_subst1 exp_named_subst2
with
e ->
let uri = UriManager.uri_of_string "cic:/dummy.var" in
prerr_endline ("@@@: " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst1)) ^
" <==> " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst2))) ; raise e
;;

(*CSC: ???????????????
(* m is the index of a metavariable to restrict, k is nesting depth
of the occurrence m, and l is its relocation list. canonical_context
is the context of the metavariable we are instantiating - containing
m - Only rel in the domain of canonical_context are accessible.
This function takes in input a metasenv and gives back a metasenv.
A rel(j) in the canonical context of m, is rel(List.nth l j) for the 
instance of m under consideration, that is rel (List.nth l j) - k 
in canonical_context. *)

let restrict canonical_context m k l =
  let rec erase i = 
    function
        [] -> []
      |        None::tl -> None::(erase (i+1) tl)
      |        he::tl -> 
          let i' = (List.nth l (i-1)) in
          if i' <= k 
           then he::(erase (i+1) tl) (* local variable *) 
           else 
            let acc = 
              (try List.nth canonical_context (i'-k-1)
               with Failure _ -> None) in
            if acc = None 
             then None::(erase (i+1) tl)
             else he::(erase (i+1) tl) in
  let rec aux =
    function 
        [] -> []
      |        (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl
      |        hd::tl -> hd::(aux tl)
  in
   aux
;;


let check_accessibility metasenv i =
  let module C = Cic in
  let module S = CicSubstitution in
  let (_,canonical_context,_) = 
    List.find (function (m,_,_) -> m=i) metasenv in
   List.map
    (function t ->
      let =
       delift canonical_context metasenv ? t
    ) canonical_context
CSCSCS



  let rec aux metasenv k =
    function
      C.Rel i -> 
       if i <= k then
        metasenv
       else 
        (try
          match List.nth canonical_context (i-k-1) with
            Some (_,C.Decl t) 
          | Some (_,C.Def t) -> aux metasenv k (S.lift i t)
          | None -> raise RelToHiddenHypothesis
          with
           Failure _ -> raise OpenTerm
        )
    | C.Var _  -> metasenv
    | C.Meta (i,l) -> restrict canonical_context i k l metasenv 
    | C.Sort _ -> metasenv
    | C.Implicit -> metasenv
    | C.Cast (te,ty) -> 
        let metasenv' = aux metasenv k te in
        aux metasenv' k ty
    | C.Prod (_,s,t) 
    | C.Lambda (_,s,t) 
    | C.LetIn (_,s,t) ->
        let metasenv' = aux metasenv k s in
        aux metasenv' (k+1) t
    | C.Appl l ->
        List.fold_left
          (function metasenv -> aux metasenv k) metasenv l
    | C.Const _
    | C.MutInd _ 
    | C.MutConstruct _ -> metasenv
    | C.MutCase (_,_,_,outty,t,pl) ->
        let metasenv' = aux metasenv k outty in
        let metasenv'' = aux metasenv' k t in
        List.fold_left
          (function metasenv -> aux metasenv k) metasenv'' pl
    | C.Fix (i, fl) ->
       let len = List.length fl in
       List.fold_left
         (fun metasenv f ->
           let (_,_,ty,bo) = f in
           let metasenv' = aux metasenv k ty in
           aux metasenv' (k+len) bo
         ) metasenv fl
    | C.CoFix (i, fl) ->
        let len = List.length fl in
        List.fold_left
         (fun metasenv f ->
           let (_,ty,bo) = f in
           let metasenv' = aux metasenv k ty in
           aux metasenv' (k+len) bo
         ) metasenv fl
  in aux metasenv 0
;;
*)


let unwind metasenv subst unwinded t =
 let unwinded = ref unwinded in
 let frozen = ref [] in
 let rec um_aux metasenv =
  let module C = Cic in
  let module S = CicSubstitution in 
   function
      C.Rel _ as t -> t,metasenv
    | C.Var _  as t -> t,metasenv
    | C.Meta (i,l) -> 
        (try
          S.lift_meta l (List.assoc i !unwinded), metasenv
         with Not_found ->
           if List.mem i !frozen then raise OccurCheck
           else
            let saved_frozen = !frozen in 
            frozen := i::!frozen ;
            let res =
             try
              let t = List.assoc i subst in
              let t',metasenv' = um_aux metasenv t in
              let _,metasenv'' =
               let (_,canonical_context,_) = 
                List.find (function (m,_,_) -> m=i) metasenv
               in
                delift canonical_context metasenv' l t'
              in
               unwinded := (i,t')::!unwinded ;
               S.lift_meta l t', metasenv'
             with
              Not_found ->
               (* not constrained variable, i.e. free in subst*)
               let l',metasenv' =
                List.fold_right
                 (fun t (tl,metasenv) ->
                   match t with
                      None -> None::tl,metasenv
                    | Some t -> 
                       let t',metasenv' = um_aux metasenv t in
                        (Some t')::tl, metasenv'
                 ) l ([],metasenv)
               in
                C.Meta (i,l'), metasenv'
            in
            frozen := saved_frozen ;
            res
        ) 
    | C.Sort _
    | C.Implicit as t -> t,metasenv
    | C.Cast (te,ty) ->
       let te',metasenv' = um_aux metasenv te in
       let ty',metasenv'' = um_aux metasenv' ty in
       C.Cast (te',ty'),metasenv''
    | C.Prod (n,s,t) ->
       let s',metasenv' = um_aux metasenv s in
       let t',metasenv'' = um_aux metasenv' t in
       C.Prod (n, s', t'), metasenv''
    | C.Lambda (n,s,t) ->
       let s',metasenv' = um_aux metasenv s in
       let t',metasenv'' = um_aux metasenv' t in
       C.Lambda (n, s', t'), metasenv''
    | C.LetIn (n,s,t) ->
       let s',metasenv' = um_aux metasenv s in
       let t',metasenv'' = um_aux metasenv' t in
       C.LetIn (n, s', t'), metasenv''
    | C.Appl (he::tl) ->
       let tl',metasenv' =
        List.fold_right
         (fun t (tl,metasenv) ->
           let t',metasenv' = um_aux metasenv t in
            t'::tl, metasenv'
         ) tl ([],metasenv)
       in
        begin
         match um_aux metasenv' he with
            (C.Appl l, metasenv'') -> C.Appl (l@tl'),metasenv''
          | (he', metasenv'') -> C.Appl (he'::tl'),metasenv''
        end
    | C.Appl _ -> assert false
    | C.Const (uri,exp_named_subst) ->
       let exp_named_subst', metasenv' =
        List.fold_right
         (fun (uri,t) (tl,metasenv) ->
           let t',metasenv' = um_aux metasenv t in
            (uri,t')::tl, metasenv'
         ) exp_named_subst ([],metasenv)
       in
        C.Const (uri,exp_named_subst'),metasenv'
    | C.MutInd (uri,typeno,exp_named_subst) ->
       let exp_named_subst', metasenv' =
        List.fold_right
         (fun (uri,t) (tl,metasenv) ->
           let t',metasenv' = um_aux metasenv t in
            (uri,t')::tl, metasenv'
         ) exp_named_subst ([],metasenv)
       in
        C.MutInd (uri,typeno,exp_named_subst'),metasenv'
    | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
       let exp_named_subst', metasenv' =
        List.fold_right
         (fun (uri,t) (tl,metasenv) ->
           let t',metasenv' = um_aux metasenv t in
            (uri,t')::tl, metasenv'
         ) exp_named_subst ([],metasenv)
       in
        C.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv'
    | C.MutCase (sp,i,outty,t,pl) ->
       let outty',metasenv' = um_aux metasenv outty in
       let t',metasenv'' = um_aux metasenv' t in
       let pl',metasenv''' =
        List.fold_right
         (fun p (pl,metasenv) ->
           let p',metasenv' = um_aux metasenv p in
            p'::pl, metasenv'
         ) pl ([],metasenv'')
       in
        C.MutCase (sp, i, outty', t', pl'),metasenv'''
    | C.Fix (i, fl) ->
       let len = List.length fl in
       let liftedfl,metasenv' =
        List.fold_right
         (fun (name, i, ty, bo) (fl,metasenv) ->
           let ty',metasenv' = um_aux metasenv ty in
           let bo',metasenv'' = um_aux metasenv' bo in
            (name, i, ty', bo')::fl,metasenv''
         ) fl ([],metasenv)
       in
        C.Fix (i, liftedfl),metasenv'
    | C.CoFix (i, fl) ->
       let len = List.length fl in
       let liftedfl,metasenv' =
        List.fold_right
         (fun (name, ty, bo) (fl,metasenv) ->
           let ty',metasenv' = um_aux metasenv ty in
           let bo',metasenv'' = um_aux metasenv' bo in
            (name, ty', bo')::fl,metasenv''
         ) fl ([],metasenv)
       in
        C.CoFix (i, liftedfl),metasenv'
 in
  let t',metasenv' = um_aux metasenv t in
   t',metasenv',!unwinded 
;;

(* apply_subst_reducing subst (Some (mtr,reductions_no)) t              *)
(* performs as (apply_subst subst t) until it finds an application of   *)
(* (META [meta_to_reduce]) that, once unwinding is performed, creates   *)
(* a new beta-redex; in this case up to [reductions_no] consecutive     *)
(* beta-reductions are performed.                                       *)
(* Hint: this function is usually called when [reductions_no]           *)
(*  eta-expansions have been performed and the head of the new          *)
(*  application has been unified with (META [meta_to_reduce]):          *)
(*  during the unwinding the eta-expansions are undone.                 *)

let apply_subst_reducing subst meta_to_reduce t =
 let unwinded = ref subst in
 let rec um_aux =
  let module C = Cic in
  let module S = CicSubstitution in 
   function
      C.Rel _
    | C.Var _  as t -> t
    | C.Meta (i,l) as t ->
       (try
         S.lift_meta l (List.assoc i !unwinded)
        with Not_found ->
          C.Meta (i,l))
    | C.Sort _ as t -> t
    | C.Implicit as t -> t
    | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
    | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
    | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
    | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
    | C.Appl (he::tl) ->
       let tl' = List.map um_aux tl in
        let t' =
         match um_aux he with
            C.Appl l -> C.Appl (l@tl')
          | _ as he' -> C.Appl (he'::tl')
        in
         begin
          match meta_to_reduce,he with
             Some (mtr,reductions_no), C.Meta (m,_) when m = mtr ->
              let rec beta_reduce =
               function
                  (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 ->
                    let he'' = CicSubstitution.subst he' t in
                     if tl' = [] then
                      he''
                     else
                      beta_reduce (n-1,C.Appl(he''::tl'))
                | (_,t) -> t
              in
               beta_reduce (reductions_no,t')
           | _,_ -> t'
         end
    | C.Appl _ -> assert false
    | C.Const (uri,exp_named_subst) ->
       let exp_named_subst' =
        List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
       in
        C.Const (uri,exp_named_subst')
    | C.MutInd (uri,typeno,exp_named_subst) ->
       let exp_named_subst' =
        List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
       in
        C.MutInd (uri,typeno,exp_named_subst')
    | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
       let exp_named_subst' =
        List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst
       in
        C.MutConstruct (uri,typeno,consno,exp_named_subst')
    | C.MutCase (sp,i,outty,t,pl) ->
       C.MutCase (sp, i, um_aux outty, um_aux t,
        List.map um_aux pl)
    | C.Fix (i, fl) ->
       let len = List.length fl in
       let liftedfl =
        List.map
         (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo))
          fl
       in
        C.Fix (i, liftedfl)
    | C.CoFix (i, fl) ->
       let len = List.length fl in
       let liftedfl =
        List.map
         (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo))
          fl
       in
        C.CoFix (i, liftedfl)
 in
   um_aux t
;;

(* UNWIND THE MGU INSIDE THE MGU *)
let unwind_subst metasenv subst =
 let identity_relocation_list_for_metavariable i =
  let (_,canonical_context,_) =
   List.find (function (m,_,_) -> m=i) metasenv
  in
   let canonical_context_length = List.length canonical_context in
    let rec aux =
     function
        n when n > canonical_context_length -> []
      | n -> (Some (Cic.Rel n))::(aux (n+1))
    in
     aux 1
 in
  List.fold_left
   (fun (unwinded,metasenv) (i,_) ->
     let identity_relocation_list =
      identity_relocation_list_for_metavariable i
     in
      let (_,metasenv',subst') =
       unwind metasenv subst unwinded (Cic.Meta (i,identity_relocation_list))
      in
       subst',metasenv'
   ) ([],metasenv) subst
;;

let apply_subst subst t = 
 (* metasenv will not be used nor modified. So, let's use a dummy empty one *)
 let metasenv = [] in
  let (t',_,_) = unwind metasenv [] subst t in
   t'
;;

(* 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 =
prerr_endline "INIZIO FASE 1" ; flush stderr ;
 let subst_to_unwind,metasenv' = fo_unif_subst [] context metasenv t1 t2 in
prerr_endline "FINE FASE 1" ; flush stderr ;
let res =
  unwind_subst metasenv' subst_to_unwind
in
prerr_endline "FINE FASE 2" ; flush stderr ; res
;;