(* 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 Rf   = CicRefine
module Un   = CicUniv
module Pp   = CicPp
module TC   = CicTypeChecker
module PEH  = ProofEngineHelpers
module E    = CicEnvironment
module UM   = UriManager
module D    = Deannotate
module PER  = ProofEngineReduction
module Ut   = CicUtil

(* raw cic prettyprinter ****************************************************)

let xiter out so ss sc map l =
   let rec aux = function
      | hd :: tl when tl <> [] -> map hd; out ss; aux tl
      | hd :: tl               -> map hd; aux tl
      | []                     -> ()
   in
   out so; aux l; out sc

let abst s w = Some (s, C.Decl w)

let abbr s v w = Some (s, C.Def (v, w))

let pp_sort out = function
   | C.Type _  -> out "\Type"
   | C.Prop    -> out "\Prop"
   | C.CProp _ -> out "\CProp"
   | C.Set     -> out "\Set"

let pp_name out = function
   | C.Name s    -> out s
   | C.Anonymous -> out "_"

let pp_rel out c i =
   try match List.nth c (pred i) with
      | None           -> out (Printf.sprintf "%u[?]" i)
      | Some (s, _)    -> out (Printf.sprintf "%u[" i); pp_name out s; out "]"
   with Failure "nth" -> out (Printf.sprintf "%u[%u]" i (List.length c - i))

let pp_implict out = function
   | None         -> out "?"
   | Some `Closed -> out "?[Closed]" 
   | Some `Type   -> out "?[Type]"
   | Some `Hole   -> out "?[Hole]"

let pp_uri out a =
   out (Printf.sprintf "%s<%s>" (UM.name_of_uri a) (UM.string_of_uri a)) 

let rec pp_term out e c = function
   | C.Sort h                      -> pp_sort out h
   | C.Rel i                       -> pp_rel out c i
   | C.Implicit x                  -> pp_implict out x
   | C.Meta (i, iss)               ->
      let map = function None   -> out "_" | Some v -> pp_term out e c v in
      out (Printf.sprintf "?%u" i); xiter out "[" "; " "]" map iss
   | C.Var (a, xss)              ->
      pp_uri out a; pp_xss out e c xss
   | C.Const (a, xss)              ->
      pp_uri out a; pp_xss out e c xss
   | C.MutInd (a, m, xss)          ->
      pp_uri out a; out (Printf.sprintf "/%u" m);
      pp_xss out e c xss
   | C.MutConstruct (a, m, n, xss) ->
      pp_uri out a; out (Printf.sprintf "/%u/%u" m n);
      pp_xss out e c xss
   | C.Cast (v, w)                 ->
      out "type "; pp_term out e c w; out " contains "; pp_term out e c v
   | C.Appl vs                     ->
      xiter out "(" " @ " ")" (pp_term out e c) vs
   | C.MutCase (a, m, w, v, vs)    ->
      out "match "; pp_term out e c v;
      out " of "; pp_uri out a; out (Printf.sprintf "/%u" m);
      out " to "; pp_term out e c w;
      xiter out " cases " " | " "" (pp_term out e c) vs
   | C.Prod (s, w, t)             ->
      out "forall "; pp_name out s; out " of "; pp_term out e c w;
      out " in "; pp_term out e (abst s w :: c) t
   | C.Lambda (s, w, t)            ->
      out "fun "; pp_name out s; out " of "; pp_term out e c w;
      out " in "; pp_term out e (abst s w :: c) t
   | C.LetIn (s, v, w, t)          ->
      out "let "; pp_name out s; 
      out " def "; pp_term out e c v; out " of "; pp_term out e c w;
      out " in "; pp_term out e (abbr s v w :: c) t
   | C.Fix (i, fs)                 ->
      let map c (s, _, w, v) = abbr (C.Name s) v w :: c in
      let c' = List.fold_left map c fs in
      let map (s, i, w, v) =
         out (Printf.sprintf "%s[%u] def " s i); pp_term out e c' v; 
	 out " of "; pp_term out e c w;
      in
      xiter out "let rec " " and " " in " map fs; pp_rel out c' (succ i)
   | C.CoFix (i, fs)                 ->
      let map c (s, w, v) = abbr (C.Name s) v w :: c in
      let c' = List.fold_left map c fs in
      let map (s, w, v) =
         out s; pp_term out e c' v; 
	 out " of "; pp_term out e c w;
      in
      xiter out "let corec " " and " " in " map fs; pp_rel out c' (succ i)

and pp_xss out e c xss = 
   let map (a, v) = pp_uri out a; out " <- "; pp_term out e c v in
   xiter out "[" "; " "]" map xss 

(* fresh name generator *****************************************************)

let split name =
   let rec aux i =
      if i <= 0 then assert false else
      let c = name.[pred i] in
      if c >= '0' && c <= '9' then aux (pred i) 
      else Str.string_before name i, Str.string_after name i
   in
   let before, after = aux (String.length name) in
   let i = if after = "" then -1 else int_of_string after in
   before, i

let join (s, i) =
   C.Name (if i < 0 then s else s ^ string_of_int i)

let mk_fresh_name context (name, k) = 
   let rec aux i = function
      | []                            -> name, i
      | Some (C.Name s, _) :: entries ->
         let m, j = split s in
	 if m = name && j >= i then aux (succ j) entries else aux i entries
      | _ :: entries                  -> aux i entries
   in
   join (aux k context)

let mk_fresh_name context = function
   | C.Anonymous -> C.Anonymous
   | C.Name s    -> mk_fresh_name context (split s)

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

let rec list_map_cps g map = function
   | []       -> g []
   | hd :: tl -> 
      let h hd =
         let g tl = g (hd :: tl) in
         list_map_cps g map tl	 
      in
      map h hd

let identity x = x

let compose f g x = f (g x)

let fst3 (x, _, _) = x

let refine c t =
   try let t, _, _, _ = Rf.type_of_aux' [] c t Un.default_ugraph in t
   with e -> 
      Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
      Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
      Printf.eprintf "Ref: term   : %s\n" (Pp.ppterm t);
      raise e

let get_type msg c t =
   let log s =
      prerr_endline ("TC: " ^ s); 
      prerr_endline ("TC: context: " ^ Pp.ppcontext c);
      prerr_string "TC: term   : "; pp_term prerr_string [] c t;
      prerr_newline (); prerr_endline ("TC: location: " ^ msg)
   in   
   try let ty, _ = TC.type_of_aux' [] c t Un.default_ugraph in ty with
      | TC.TypeCheckerFailure s as e ->
        log ("failure: " ^ Lazy.force s); raise e        
      | TC.AssertFailure s as e      -> 
        log ("assert : " ^ Lazy.force s); raise e

let get_tail c t =
   match PEH.split_with_whd (c, t) with
      | (_, hd) :: _, _ -> hd
      | _               -> assert false

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

let is_sort = function
   | C.Sort _ -> true
   | _        -> false 

let is_unsafe h (c, t) = true

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

let is_atomic t = not (is_not_atomic t)

let get_ind_type uri tyno =
   match E.get_obj Un.default_ugraph uri with
      | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
      | _                                           -> assert false

let get_ind_names uri tno =
try   
   let ts = match E.get_obj Un.default_ugraph uri with
      | C.InductiveDefinition (ts, _, _, _), _ -> ts 
      | _                                      -> assert false
   in
   match List.nth ts tno with
      | (_, _, _, cs) -> List.map fst cs  
with Invalid_argument _ -> failwith "get_ind_names"

let get_default_eliminator context uri tyno ty =
   let _, (name, _, _, _) = get_ind_type uri tyno in
   let ext = match get_tail context (get_type "get_def_elim" context ty) with
      | C.Sort C.Prop      -> "_ind"
      | C.Sort C.Set       -> "_rec"
      | C.Sort (C.CProp _) -> "_rect"
      | C.Sort (C.Type _)  -> "_rect"
      | t                  -> 
         Printf.eprintf "CicPPP get_default_eliminator: %s\n" (Pp.ppterm t);
         assert false
   in
   let buri = UM.buri_of_uri uri in
   let uri = UM.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in
   C.Const (uri, [])

let get_ind_parameters c t =
   let ty = get_type "get_ind_pars 1" c t in
   let ps = match get_tail c ty with
      | C.MutInd _                  -> []
      | C.Appl (C.MutInd _ :: args) -> args
      | _                           -> assert false
   in
   let disp = match get_tail c (get_type "get_ind_pars 2" c ty) with
      | C.Sort C.Prop -> 0
      | C.Sort _      -> 1
      | _             -> assert false
   in
   ps, disp

let cic = D.deannotate_term

let occurs c ~what ~where =
   let result = ref false in
   let equality c t1 t2 =
      let r = Ut.alpha_equivalence t1 t2 in
      result := !result || r; r
   in
   let context, what, with_what = c, [what], [C.Rel 0] in
   let _ = PER.replace_lifting ~equality ~context ~what ~with_what ~where in
   !result

let name_of_uri uri tyno cno =
   let get_ind_type tys tyno =
      let s, _, _, cs = List.nth tys tyno in s, cs
   in
   match (fst (E.get_obj Un.default_ugraph uri)), tyno, cno with
      | C.Variable (s, _, _, _, _), _, _                     -> s
      | C.Constant (s, _, _, _, _), _, _                     -> s
      | C.InductiveDefinition (tys, _, _, _), Some i, None   ->
         let s, _ = get_ind_type tys i in s
      | C.InductiveDefinition (tys, _, _, _), Some i, Some j ->
         let _, cs = get_ind_type tys i in
	 let s, _ = List.nth cs (pred j) in s
      | _                                                    -> assert false

(* Ensuring Barendregt convenction ******************************************)

let rec add_entries map c = function
   | []       -> c
   | hd :: tl ->
      let sname, w = map hd in
      let entry = Some (Cic.Name sname, C.Decl w) in
      add_entries map (entry :: c) tl

let get_sname c i =
   try match List.nth c (pred i) with
      | Some (Cic.Name sname, _) -> sname
      | _                        -> assert false
   with 
      | Failure _          -> assert false
      | Invalid_argument _ -> assert false

let cic_bc c t =
   let get_fix_decl (sname, i, w, v) = sname, w in
   let get_cofix_decl (sname, w, v) = sname, w in
   let rec bc c = function
      | C.LetIn (name, v, ty, t) ->
         let name = mk_fresh_name c name in
         let entry = Some (name, C.Def (v, ty)) in
         let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
	 C.LetIn (name, v, ty, t)
      | C.Lambda (name, w, t) ->
         let name = mk_fresh_name c name in
         let entry = Some (name, C.Decl w) in
         let w, t = bc c w, bc (entry :: c) t in
	 C.Lambda (name, w, t)
      | C.Prod (name, w, t) ->
         let name = mk_fresh_name c name in
         let entry = Some (name, C.Decl w) in
         let w, t = bc c w, bc (entry :: c) t in
	 C.Prod (name, w, t)
      | C.Appl vs -> 
         let vs = List.map (bc c) vs in
	 C.Appl vs
      | C.MutCase (uri, tyno, u, v, ts) ->
         let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
	 C.MutCase (uri, tyno, u, v, ts)
      | C.Cast (t, u) ->  
         let t, u = bc c t, bc c u in
         C.Cast (t, u)
      | C.Fix (i, fixes) ->
         let d = add_entries get_fix_decl c fixes in
	 let bc_fix (sname, i, w, v) = (sname, i, bc c w, bc d v) in
	 let fixes = List.map bc_fix fixes in
	 C.Fix (i, fixes)
      | C.CoFix (i, cofixes) ->
         let d = add_entries get_cofix_decl c cofixes in
	 let bc_cofix (sname, w, v) = (sname, bc c w, bc d v) in
	 let cofixes = List.map bc_cofix cofixes in
	 C.CoFix (i, cofixes)
      | t -> t
   in 
   bc c t

let acic_bc c t =
   let get_fix_decl (id, sname, i, w, v) = sname, cic w in
   let get_cofix_decl (id, sname, w, v) = sname, cic w in
   let rec bc c = function
      | C.ALetIn (id, name, v, ty, t) ->
         let name = mk_fresh_name c name in
         let entry = Some (name, C.Def (cic v, cic ty)) in
         let v, ty, t = bc c v, bc c ty, bc (entry :: c) t in
	 C.ALetIn (id, name, v, ty, t)
      | C.ALambda (id, name, w, t) ->
         let name = mk_fresh_name c name in
         let entry = Some (name, C.Decl (cic w)) in
         let w, t = bc c w, bc (entry :: c) t in
	 C.ALambda (id, name, w, t)
      | C.AProd (id, name, w, t) ->
         let name = mk_fresh_name c name in
         let entry = Some (name, C.Decl (cic w)) in
         let w, t = bc c w, bc (entry :: c) t in
	 C.AProd (id, name, w, t)
      | C.AAppl (id, vs) -> 
         let vs = List.map (bc c) vs in
	 C.AAppl (id, vs)
      | C.AMutCase (id, uri, tyno, u, v, ts) ->
         let u, v, ts = bc c u, bc c v, List.map (bc c) ts in
	 C.AMutCase (id, uri, tyno, u, v, ts)
      | C.ACast (id, t, u) ->  
         let t, u = bc c t, bc c u in
         C.ACast (id, t, u)
      | C.AFix (id, i, fixes) ->
         let d = add_entries get_fix_decl c fixes in
	 let bc_fix (id, sname, i, w, v) = (id, sname, i, bc c w, bc d v) in
	 let fixes = List.map bc_fix fixes in
	 C.AFix (id, i, fixes)
      | C.ACoFix (id, i, cofixes) ->
         let d = add_entries get_cofix_decl c cofixes in
	 let bc_cofix (id, sname, w, v) = (id, sname, bc c w, bc d v) in
	 let cofixes = List.map bc_cofix cofixes in
	 C.ACoFix (id, i, cofixes)
      | C.ARel (id1, id2, i, sname) ->
         let sname = get_sname c i in
	 C.ARel (id1, id2, i, sname)
      | t -> t
   in 
   bc c t