(* 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;;

type substitution = (int * Cic.term) list

(*CSC: Hhhmmm. Forse dovremmo spostarla in CicSubstitution dove si trova la *)
(*CSC: lift? O creare una proofEngineSubstitution?                          *)
(* the function delift n m un-lifts a lambda term m of n level of abstractions.
   It returns an exception Free if M contains a free variable in the range 1--n *)
let delift n =
 let rec deliftaux k =
  let module C = Cic in
   function
      C.Rel m ->
       if m < k then C.Rel m else
       if m < k+n then raise Free
       else C.Rel (m - n)
    | C.Var _  as t -> t
    | C.Meta _ as t -> t
    | 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 _ as t -> t
    | C.Abst _  as t -> t
    | C.MutInd _ as t -> t
    | C.MutConstruct _ as t -> t
    | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
       C.MutCase (sp, cookingsno, 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
  if n = 0 then
   (function t -> t)
  else
   deliftaux 1
;;

(* 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 fo_unif_new metasenv context t1 t2 =
    let module C = Cic in
    let module R = CicReduction in
    let module S = CicSubstitution in
    let rec fo_unif_aux subst k t1 t2 =  
    match (t1, t2) with
      (C.Meta n, C.Meta m) -> if n == m then subst 
                       else let subst'= 
			 let tn = try List.assoc n subst
                                  with Not_found -> C.Meta n in
			 let tm = try List.assoc m subst
                                  with Not_found -> C.Meta m in
			 (match (tn, tm) with 
			   (C.Meta n, C.Meta m) -> if n==m then subst
		                                 else if n<m 
						 then (m, C.Meta n)::subst
                                                 else (n, C.Meta m)::subst
		         | (C.Meta n, tm) -> (n, tm)::subst
		         | (tn, C.Meta m) -> (m, tn)::subst	
		         | (tn,tm) -> fo_unif_aux subst 0 tn tm) in
                         (* unify types first *)
                         let tyn = List.assoc n metasenv in
                         let tym = List.assoc m metasenv in
                         fo_unif_aux subst' 0 tyn tym
       | (C.Meta n, t)   
       | (t, C.Meta n) ->   (* unify types first *)
                            let t' = delift k t in
                            let subst' =
			    (try fo_unif_aux subst 0 (List.assoc n subst) t'
			     with Not_found -> (n, t')::subst) in
                            let tyn = List.assoc n metasenv in
                            let tyt = CicTypeChecker.type_of_aux' metasenv context t' in
                            fo_unif_aux subst' 0 tyn tyt
       | (C.Rel _, _)
       | (_,  C.Rel _) 
       | (C.Var _, _)
       | (_, C.Var _) 
       | (C.Sort _ ,_)
       | (_, C.Sort _)
       | (C.Implicit, _)
       | (_, C.Implicit) -> if R.are_convertible t1 t2 then subst
                            else raise UnificationFailed
       | (C.Cast (te,ty), t2) -> fo_unif_aux subst k te t2
       | (t1, C.Cast (te,ty)) -> fo_unif_aux subst k t1 te
       | (C.Prod (_,s1,t1), C.Prod (_,s2,t2)) -> 
	                   let subst' = fo_unif_aux subst k s1 s2 in
                           fo_unif_aux subst' (k+1) t1 t2
       | (C.Lambda (_,s1,t1), C.Lambda (_,s2,t2)) -> 
                                let subst' = fo_unif_aux subst k s1 s2 in
                                fo_unif_aux subst' (k+1) t1 t2
       | (C.LetIn (_,s1,t1), t2) -> fo_unif_aux subst k (S.subst s1 t1) t2
       | (t1, C.LetIn (_,s2,t2)) -> fo_unif_aux subst k t1 (S.subst s2 t2)
       | (C.Appl l1, C.Appl l2) -> 
                          let lr1 = List.rev l1 in
                          let lr2 = List.rev l2 in
                          let rec fo_unif_l subst = function
                              [],_
                            | _,[] -> assert false
                            | ([h1],[h2]) -> fo_unif_aux subst k h1 h2
                            | ([h],l) 
                            | (l,[h]) -> fo_unif_aux subst k h (C.Appl l)
                            | ((h1::l1),(h2::l2)) -> 
				let subst' = fo_unif_aux subst k h1 h2 in 
                                fo_unif_l subst' (l1,l2)
                          in
			  fo_unif_l subst (lr1, lr2) 
       | (C.Const _, _) 
       | (_, C.Const _)
       | (C.Abst _, _) 
       | (_, C.Abst _) 
       | (C.MutInd  _, _) 
       | (_, C.MutInd _)
       | (C.MutConstruct _, _)
       | (_, C.MutConstruct _) -> if R.are_convertible t1 t2 then subst
                                   else raise UnificationFailed
       | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))->
                      let subst' = fo_unif_aux subst k outt1 outt2 in
                      let subst'' = fo_unif_aux subst' k t1 t2 in
                      List.fold_left2 (function subst -> fo_unif_aux subst k) subst'' pl1 pl2 
       | (C.Fix _, _)
       | (_, C.Fix _) 
       | (C.CoFix _, _)
       | (_, C.CoFix _) -> if R.are_convertible t1 t2 then subst
                           else raise UnificationFailed
       | (_,_) -> raise UnificationFailed
   in fo_unif_aux [] 0 t1 t2;;

(* unwind mgu mark m applies mgu to the term m; mark is an array of integers
mark.(n) = 0 if the term has not been unwinded, is 2 if it is under uwinding, 
and is 1 if it has been succesfully unwinded. Meeting the value 2 during
the computation is an error: occur-check *) 

let unwind subst unwinded t =
 let unwinded = ref unwinded in
 let frozen = ref [] in
 let rec um_aux k =
  let module C = Cic in
  let module S = CicSubstitution in 
   function
      C.Rel _ as t -> t 
    | C.Var _  as t -> t
    | C.Meta i as t ->(try S.lift k (List.assoc i !unwinded)
                       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' = um_aux 0 t in
                                unwinded := (i,t')::!unwinded ;
                                S.lift k t'
                             with
                              Not_found ->
                               (* not constrained variable, i.e. free in subst*)
                               C.Meta i
                            in
                             frozen := saved_frozen ;
                             res
                      ) 
    | C.Sort _ as t -> t
    | C.Implicit as t -> t
    | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
    | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
    | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
    | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
    | C.Appl (he::tl) ->
       let tl' = List.map (um_aux k) tl in
        begin
         match um_aux k he with
            C.Appl l -> C.Appl (l@tl')
          | _ as he' -> C.Appl (he'::tl')
        end
    | C.Appl _ -> assert false
    | C.Const _ as t -> t
    | C.Abst _  as t -> t
    | C.MutInd _ as t -> t
    | C.MutConstruct _ as t -> t
    | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
       C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
        List.map (um_aux k) pl)
    | C.Fix (i, fl) ->
       let len = List.length fl in
       let liftedfl =
        List.map
         (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (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, um_aux k ty, um_aux (k+len) bo))
          fl
       in
        C.CoFix (i, liftedfl)
 in
   um_aux 0 t,!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 k =
  let module C = Cic in
  let module S = CicSubstitution in 
   function
      C.Rel _ as t -> t 
    | C.Var _  as t -> t
    | C.Meta i as t ->
       (try
         S.lift k (List.assoc i !unwinded)
        with Not_found ->
          C.Meta i)
    | C.Sort _ as t -> t
    | C.Implicit as t -> t
    | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty)
    | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t)
    | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t)
    | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t)
    | C.Appl (he::tl) ->
       let tl' = List.map (um_aux k) tl in
        let t' =
         match um_aux k he with
            C.Appl l -> C.Appl (l@tl')
          | _ as he' -> C.Appl (he'::tl')
        in
         begin
          match meta_to_reduce with
             Some (mtr,reductions_no) when he = C.Meta 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 _ as t -> t
    | C.Abst _  as t -> t
    | C.MutInd _ as t -> t
    | C.MutConstruct _ as t -> t
    | C.MutCase (sp,cookingsno,i,outty,t,pl) ->
       C.MutCase (sp, cookingsno, i, um_aux k outty, um_aux k t,
        List.map (um_aux k) pl)
    | C.Fix (i, fl) ->
       let len = List.length fl in
       let liftedfl =
        List.map
         (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (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, um_aux k ty, um_aux (k+len) bo))
          fl
       in
        C.CoFix (i, liftedfl)
 in
   um_aux 0 t
;;

(* UNWIND THE MGU INSIDE THE MGU *)
let unwind_subst subst =
  List.fold_left
   (fun unwinded (i,_) -> snd (unwind subst unwinded (Cic.Meta i))) [] subst
;;

let apply_subst subst t = 
    fst (unwind [] subst t)
;;

(* 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 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. *)
let fo_unif metasenv context t1 t2 =
 let subst_to_unwind = fo_unif_new metasenv context t1 t2 in
  unwind_subst subst_to_unwind
;;