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

(* 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.empty_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 c t =
   try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
   with e -> 
      Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
      Printf.eprintf "TC: term   : %s\n" (Pp.ppterm t);
      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 c (get_type c t)) with
      | C.Sort C.Prop -> true
      | C.Sort _      -> false
      | _             -> assert 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 get_ind_type uri tyno =
   match E.get_obj Un.empty_ugraph uri with
      | C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
      | _                                           -> assert false

let get_default_eliminator context uri tyno ty =
   let _, (name, _, _, _) = get_ind_type uri tyno in
   let ext = match get_tail context (get_type context ty) with
      | C.Sort C.Prop     -> "_ind"
      | C.Sort C.Set      -> "_rec"
      | C.Sort C.CProp    -> "_rec"
      | 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 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 c ty) with
      | C.Sort C.Prop -> 0
      | C.Sort _      -> 1
      | _             -> assert false
   in
   ps, disp