(* Copyright (C) 2003-2005, 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/.
 *)

module C    = Cic
module Un   = CicUniv
module S    = CicSubstitution
module R    = CicReduction
module TC   = CicTypeChecker 
module DTI  = DoubleTypeInference
module HEL  = HExtlib

(* helper functions *********************************************************)

let identity x = x

let comp f g x = f (g x)

let get_type c t =
   let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty

let is_proof c t =
   match (get_type c (get_type c t)) with
      | C.Sort C.Prop -> true
      | _             -> false

let is_not_atomic = function
   | C.Sort _
   | C.Rel _
   | C.Const _
   | C.Var _
   | C.MutInd _ 
   | C.MutConstruct _ -> false
   | _                -> true

let split c t =
   let add s v c = Some (s, C.Decl v) :: c in
   let rec aux whd a n c = function
      | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
      | v when whd        -> v :: a, n
      | v                 -> aux true a n c (R.whd ~delta:true c v)
    in
    aux false [] 0 c t

let add g htbl t proof decurry =
   if proof then C.CicHash.add htbl t decurry; 
   g t proof decurry

let find g htbl t = 
   try 
      let decurry = C.CicHash.find htbl t in g t true decurry
   with Not_found -> g t false 0

(* term preprocessing *******************************************************)

let expanded_premise = "EXPANDED"

let defined_premise = "DEFINED"

let eta_expand n t =
   let ty = C.Implicit None in
   let name i = Printf.sprintf "%s%u" expanded_premise i in 
   let lambda i t = C.Lambda (C.Name (name i), ty, t) in
   let arg i n = C.Rel (n - i) in
   let rec aux i f a =
      if i >= n then f, a else aux (succ i) (comp f (lambda i)) (arg i n :: a)
   in
   let absts, args = aux 0 identity [] in
   absts (C.Appl (S.lift n t :: args))

let eta_fix t proof decurry =
   if proof && decurry > 0 then eta_expand decurry t else t

let rec pp_cast g ht es c t v =
   if es then pp_proof g ht es c t else find g ht t

and pp_lambda g ht es c name v t =
   let name = if DTI.does_not_occur 1 t then C.Anonymous else name in
   let entry = Some (name, C.Decl v) in
   let g t _ decurry = 
      let t = eta_fix t true decurry in
      g (C.Lambda (name, v, t)) true 0 in
   if es then pp_proof g ht es (entry :: c) t else find g ht t

and pp_letin g ht es c name v t =
   let entry = Some (name, C.Def (v, None)) in
   let g t _ decurry =
      if DTI.does_not_occur 1 t then g (S.lift (-1) t) true decurry else 
      let g v proof d = match v with
         | C.LetIn (mame, w, u) when proof ->
            let x = C.LetIn (mame, w, C.LetIn (name, u, S.lift_from 2 1 t)) in
	    pp_proof g ht false c x 
         | v                               -> 
            let v = eta_fix v proof d in
	    g (C.LetIn (name, v, t)) true decurry
      in
      if es then pp_term g ht es c v else find g ht v
   in
   if es then pp_proof g ht es (entry :: c) t else find g ht t

and pp_appl_one g ht es c t v =
   let g t _ decurry =
      let g v proof d =
         match t, v with
	    | t, C.LetIn (mame, w, u) when proof ->
               let x = C.LetIn (mame, w, C.Appl [S.lift 1 t; u]) in
	       pp_proof g ht false c x 
            | C.LetIn (mame, w, u), v            ->
               let x = C.LetIn (mame, w, C.Appl [u; S.lift 1 v]) in
	       pp_proof g ht false c x
	    | C.Appl ts, v when decurry > 0      ->
	       let v = eta_fix v proof d in
	       g (C.Appl (List.append ts [v])) true (pred decurry)
	    | t, v  when is_not_atomic t         ->
	       let mame = C.Name defined_premise in
	       let x = C.LetIn (mame, t, C.Appl [C.Rel 1; S.lift 1 v]) in
	       pp_proof g ht false c x
	    | t, v                               ->
               let _, premsno = split c (get_type c t) in
	       let v = eta_fix v proof d in
               g (C.Appl [t; v]) true (pred premsno)
      in
      if es then pp_term g ht es c v else find g ht v
   in
   if es then pp_proof g ht es c t else find g ht t

and pp_appl g ht es c t = function
   | []             -> pp_proof g ht es c t
   | [v]            -> pp_appl_one g ht es c t v
   | v1 :: v2 :: vs ->
      let x = C.Appl (C.Appl [t; v1] :: v2 :: vs) in 
      pp_proof g ht es c x

and pp_proof g ht es c t = 
   let g t proof decurry = add g ht t proof decurry in
   match t with
      | C.Cast (t, v)         -> pp_cast g ht es c t v
      | C.Lambda (name, v, t) -> pp_lambda g ht es c name v t
      | C.LetIn (name, v, t)  -> pp_letin g ht es c name v t
      | C.Appl (t :: vs)      -> pp_appl g ht es c t vs
      | t                     -> g t true 0

and pp_term g ht es c t =
   if is_proof c t then pp_proof g ht es c t else g t false 0

(* object preprocessing *****************************************************)

let pp_obj = function
   | C.Constant (name, Some bo, ty, pars, attrs) ->
      let g bo proof decurry = 
         let bo = eta_fix bo proof decurry in
         C.Constant (name, Some bo, ty, pars, attrs)
      in
      let ht = C.CicHash.create 1 in
      pp_term g ht true [] bo
   | obj                                         -> obj