(* 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 ReferenceToVariable;;
exception RferenceToCurrentProof;;
exception ReferenceToInductiveDefinition;;

let rec fix_lambdas_wrt_type ty te =
 let module C = Cic in
 let module S = CicSubstitution in
(*  prerr_endline ("entering fix_lambdas: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); 
   flush stderr ; *)
   (* cast e altra porcheria ???? *)
   match ty,te with
     C.Prod (_,_,ty'), C.Lambda (n,s,te') ->
       C.Lambda (n,s,fix_lambdas_wrt_type ty' te')
   | C.Prod (_,s,ty'), C.Appl l ->
       prerr_endline ("******** fl - eta expansion 1: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); 
       flush stderr ;
       let l' = List.map (S.lift 1) l in
        C.Lambda (C.Name "x",s,
         fix_lambdas_wrt_type ty' (C.Appl (l'@[C.Rel 1])))
   | C.Prod (_,s,ty'), _ ->
       prerr_endline ("******** fl - eta expansion 2: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm te); 
       flush stderr ;
       let te' = S.lift 1 te in
        C.Lambda (C.Name "x",s,
          fix_lambdas_wrt_type ty' (C.Appl [te';C.Rel 1]))
   | _, _ -> te
;;

let fix_according_to_type ty hd tl =
 let module C = Cic in
 let module S = CicSubstitution in
  let rec aux ty tl res =
   (* prerr_endline ("entering aux_1 with type=" ^ CicPp.ppterm ty); 
   flush stderr ; *)
   match ty with
      C.Rel _
    | C.Var _
    | C.Meta _ 
    | C.Sort _ 
    | C.Implicit -> 
      (match tl with 
         [] -> C.Appl res
       |  _ ->
         prerr_endline ("******* fat - too many args: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); 
         flush stderr ;
         C.LetIn 
          (C.Name "H", C.Appl res, C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
    | C.Cast (v,t) -> aux v tl res
    | C.Prod (n,s,t) -> 
       (match tl with 
          [] ->
            prerr_endline ("******* fat - eta expansion: type=" ^ CicPp.ppterm ty ^ "term=" ^ CicPp.ppterm (C.Appl res)); 
         flush stderr ;
           let res' = List.map (S.lift 1) res 
           in 
           C.Lambda 
            (C.Name "x", (* Andrea: to do: generate a fresh name *)
             s, 
             aux t [] (res'@[C.Rel 1]))
        | hd::tl' -> 
           let hd' = fix_lambdas_wrt_type s hd
           in
            aux (S.subst hd' t) tl' (res@[hd']))
    | C.Lambda _ -> assert false
    | C.LetIn (n,s,t) -> aux (S.subst s t) tl res
    | C.Appl _
    | C.Const _
    | C.MutInd _ 
    | C.MutConstruct _
    | C.MutCase _
    | C.Fix _
    | C.CoFix _ -> (* ???? *)
       (match tl with 
         [] -> C.Appl res
       |  _ -> (* Andrea: to do: generate a fresh name *)
         C.LetIn 
          (C.Name "H",
           C.Appl res, 
           C.Appl (C.Rel 1::(List.map (S.lift 1) tl))))
  in
  aux ty tl [hd]
;;

let eta_fix metasenv t =
 let rec eta_fix' t = 
(*  prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t); 
  flush stderr ; *)
  let module C = Cic in
  match t with
     C.Rel n -> C.Rel n 
   | C.Var (uri,exp_named_subst) ->
      let exp_named_subst' =
       List.map
        (function i,t -> i, (eta_fix' t)) exp_named_subst
      in
      C.Var (uri,exp_named_subst')
   | C.Meta (n,l) ->
      let (_,canonical_context,_) =
       List.find (function (m,_,_) -> n = m) metasenv
       in
       let l' =
        List.map2
         (fun ct t ->
          match (ct, t) with
            None, _ -> None
          | _, Some t -> Some (eta_fix' t)
          | Some _, None -> assert false (* due to typing rules *))
        canonical_context l
       in
       C.Meta (n,l')
   | C.Sort s -> C.Sort s
   | C.Implicit -> C.Implicit
   | C.Cast (v,t) -> C.Cast (eta_fix' v, eta_fix' t)
   | C.Prod (n,s,t) -> C.Prod (n, eta_fix' s, eta_fix' t)
   | C.Lambda (n,s,t) -> C.Lambda (n, eta_fix' s, eta_fix' t)
   | C.LetIn (n,s,t) -> C.LetIn (n, eta_fix' s, eta_fix' t)
   | C.Appl l -> 
       let l' =  List.map eta_fix' l 
       in 
       (match l' with
         C.Const(uri,exp_named_subst)::l'' ->
           let constant_type =
             (match CicEnvironment.get_obj uri with
               C.Constant (_,_,ty,_) -> ty
             | C.Variable _ -> raise ReferenceToVariable
             | C.CurrentProof (_,_,_,_,params) -> raise RferenceToCurrentProof
             | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
             )
           in
           fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l''
        | _ -> C.Appl l' )
   | C.Const (uri,exp_named_subst) ->
       let exp_named_subst' =
       List.map
        (function i,t -> i, (eta_fix' t)) exp_named_subst
       in
       C.Const (uri,exp_named_subst')
   | C.MutInd (uri,tyno,exp_named_subst) ->
       let exp_named_subst' =
       List.map
        (function i,t -> i, (eta_fix' t)) exp_named_subst
       in
        C.MutInd (uri, tyno, exp_named_subst')
   | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
       let exp_named_subst' =
       List.map
        (function i,t -> i, (eta_fix' t)) exp_named_subst
       in
        C.MutConstruct (uri, tyno, consno, exp_named_subst')
   | C.MutCase (uri, tyno, outty, term, patterns) ->
       C.MutCase (uri, tyno, eta_fix' outty,
              eta_fix' term, List.map eta_fix' patterns)
   | C.Fix (funno, funs) ->
       C.Fix (funno,
        List.map
         (fun (name, no, ty, bo) ->
           (name, no, eta_fix' ty, eta_fix' bo)) funs)
   | C.CoFix (funno, funs) ->
       C.CoFix (funno,
        List.map
         (fun (name, ty, bo) ->
           (name, eta_fix' ty, eta_fix' bo)) funs)
   in
   eta_fix' t
;;