(* 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/.
 *)

(*****************************************************************************)
(*                                                                           *)
(*                               PROJECT HELM                                *)
(*                                                                           *)
(* This module implements a very simple Coq-like pretty printer that, given  *)
(* an object of cic (internal representation) returns a string describing    *)
(* the object in a syntax similar to that of coq                             *)
(*                                                                           *)
(* It also contains the utility functions to check a name w.r.t the Matita   *)
(* naming policy                                                             *)
(*                                                                           *)
(*****************************************************************************)

exception CicPpInternalError;;
exception NotEnoughElements;;

(* Utility functions *)

let ppname =
 function
    Cic.Name s     -> s
  | Cic.Anonymous  -> "_"
;;

(* get_nth l n   returns the nth element of the list l if it exists or *)
(* raises NotEnoughElements if l has less than n elements             *)
let rec get_nth l n =
 match (n,l) with
    (1, he::_) -> he
  | (n, he::tail) when n > 1 -> get_nth tail (n-1)
  | (_,_) -> raise NotEnoughElements
;;

(* pp t l                                                                  *)
(* pretty-prints a term t of cic in an environment l where l is a list of  *)
(* identifier names used to resolve DeBrujin indexes. The head of l is the *)
(* name associated to the greatest DeBrujin index in t                     *)
let rec pp t l =
 let module C = Cic in
   match t with
      C.Rel n ->
       begin
        try
         (match get_nth l n with
             Some (C.Name s) -> s
           | Some C.Anonymous -> "__" ^ string_of_int n
           | None -> "_hidden_" ^ string_of_int n
         )
        with
         NotEnoughElements -> string_of_int (List.length l - n)
       end
    | C.Var (uri,exp_named_subst) ->
       UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
    | C.Meta (n,l1) ->
       "?" ^ (string_of_int n) ^ "[" ^ 
        String.concat " ; "
         (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
        "]"
    | C.Sort s ->
       (match s with
           C.Prop  -> "Prop"
         | C.Set   -> "Set"
         | C.Type _ -> "Type"
         (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*)
	 | C.CProp -> "CProp" 
       )
    | C.Implicit (Some `Hole) -> "%"
    | C.Implicit _ -> "?"
    | C.Prod (b,s,t) ->
       (match b with
          C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
        | C.Anonymous -> "(" ^ pp s l ^ "->" ^ pp t ((Some b)::l) ^ ")"
       )
    | C.Cast (v,t) -> "(" ^ pp v l ^ ":" ^ pp t l ^ ")"
    | C.Lambda (b,s,t) ->
       "[" ^ ppname b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
    | C.LetIn (b,s,t) ->
       "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
    | C.Appl li ->
       "(" ^
       (List.fold_right
        (fun x i -> pp x l ^ (match i with "" -> "" | _ -> " ") ^ i)
        li ""
       ) ^ ")"
    | C.Const (uri,exp_named_subst) ->
       UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l
    | C.MutInd (uri,n,exp_named_subst) ->
       (try
         match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
            C.InductiveDefinition (dl,_,_,_) ->
             let (name,_,_,_) = get_nth dl (n+1) in
              name ^ pp_exp_named_subst exp_named_subst l
          | _ -> raise CicPpInternalError
        with
         _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
       )
    | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
       (try
         match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
            C.InductiveDefinition (dl,_,_,_) ->
             let (_,_,_,cons) = get_nth dl (n1+1) in
              let (id,_) = get_nth cons n2 in
               id ^ pp_exp_named_subst exp_named_subst l
          | _ -> raise CicPpInternalError
        with
         _ ->
          UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
           string_of_int n2
       )
    | C.MutCase (uri,n1,ty,te,patterns) ->
       let connames =
        (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
            C.InductiveDefinition (dl,_,_,_) ->
             let (_,_,_,cons) = get_nth dl (n1+1) in
              List.map (fun (id,_) -> id) cons
          | _ -> raise CicPpInternalError
        )
       in
        "\n<" ^ pp ty l ^ ">Cases " ^ pp te l ^ " of " ^
          List.fold_right (fun (x,y) i -> "\n " ^ x ^ " => " ^ pp y l ^ i)
           (List.combine connames patterns) "" ^
          "\nend"
    | C.Fix (no, funs) ->
       let snames = List.map (fun (name,_,_,_) -> name) funs in
        let names =
         List.rev (List.map (function name -> Some (C.Name name)) snames)
        in
         "\nFix " ^ get_nth snames (no + 1) ^ " {" ^
         List.fold_right
          (fun (name,ind,ty,bo) i -> "\n" ^ name ^ " / " ^ string_of_int ind ^
            " : " ^ pp ty l ^ " := \n" ^
            pp bo (names@l) ^ i)
          funs "" ^
         "}\n"
    | C.CoFix (no,funs) ->
       let snames = List.map (fun (name,_,_) -> name) funs in
        let names =
         List.rev (List.map (function name -> Some (C.Name name)) snames)
        in
         "\nCoFix " ^ get_nth snames (no + 1) ^ " {" ^
         List.fold_right
          (fun (name,ty,bo) i -> "\n" ^ name ^ 
            " : " ^ pp ty l ^ " := \n" ^
            pp bo (names@l) ^ i)
          funs "" ^
         "}\n"
and pp_exp_named_subst exp_named_subst l =
 if exp_named_subst = [] then "" else
  "{" ^
   String.concat " ; " (
    List.map
     (function (uri,t) -> UriManager.name_of_uri uri ^ ":=" ^ pp t l)
     exp_named_subst
   ) ^ "}"
;;

let ppterm t =
 pp t []
;;

(* ppinductiveType (typename, inductive, arity, cons)                       *)
(* pretty-prints a single inductive definition                              *)
(* (typename, inductive, arity, cons)                                       *)
let ppinductiveType (typename, inductive, arity, cons) =
  (if inductive then "\nInductive " else "\nCoInductive ") ^ typename ^ ": " ^
  pp arity [] ^ " =\n   " ^
  List.fold_right
   (fun (id,ty) i -> id ^ " : " ^ pp ty [] ^ 
    (if i = "" then "\n" else "\n | ") ^ i)
   cons ""
;;

let ppcontext ?(sep = "\n") context =
 let separate s = if s = "" then "" else s ^ sep in
 fst (List.fold_right 
   (fun context_entry (i,name_context) ->
     match context_entry with
        Some (n,Cic.Decl t) ->
         Printf.sprintf "%s%s : %s" (separate i) (ppname n)
          (pp t name_context), (Some n)::name_context
      | Some (n,Cic.Def (bo,ty)) ->
         Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
          (match ty with
              None -> "_"
            | Some ty -> pp ty name_context)
          (pp bo name_context), (Some n)::name_context
       | None ->
          Printf.sprintf "%s_ :? _" (separate i), None::name_context
    ) context ("",[]))

(* ppobj obj  returns a string with describing the cic object obj in a syntax *)
(* similar to the one used by Coq                                             *)
let ppobj obj =
 let module C = Cic in
 let module U = UriManager in
  match obj with
    C.Constant (name, Some t1, t2, params, _) ->
      "Definition of " ^ name ^
       "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
       ")" ^ ":\n" ^ pp t1 [] ^ " : " ^ pp t2 []
   | C.Constant (name, None, ty, params, _) ->
      "Axiom " ^ name ^
       "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
       "):\n" ^ pp ty []
   | C.Variable (name, bo, ty, params, _) ->
      "Variable " ^ name ^
       "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
       ")" ^ ":\n" ^
       pp ty [] ^ "\n" ^
       (match bo with None -> "" | Some bo -> ":= " ^ pp bo [])
   | C.CurrentProof (name, conjectures, value, ty, params, _) ->
      "Current Proof of " ^ name ^
       "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
       ")" ^ ":\n" ^
      let separate s = if s = "" then "" else s ^ " ; " in
       List.fold_right
        (fun (n, context, t) i -> 
          let conjectures',name_context =
	         List.fold_right 
	          (fun context_entry (i,name_context) ->
	            (match context_entry with
	                Some (n,C.Decl at) ->
                   (separate i) ^
                     ppname n ^ ":" ^ pp at name_context ^ " ",
                      (Some n)::name_context
	              | Some (n,C.Def (at,None)) ->
                   (separate i) ^
                     ppname n ^ ":= " ^ pp at name_context ^ " ",
                      (Some n)::name_context
                | None ->
                   (separate i) ^ "_ :? _ ", None::name_context
                | _ -> assert false)
            ) context ("",[])
          in
           conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
            pp t name_context ^ "\n" ^ i
        ) conjectures "" ^
        "\n" ^ pp value [] ^ " : " ^ pp ty [] 
   | C.InductiveDefinition (l, params, nparams, _) ->
      "Parameters = " ^
       String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^
       "NParams = " ^ string_of_int nparams ^ "\n" ^
        List.fold_right (fun x i -> ppinductiveType x ^ i) l ""
;;

let ppsort = function
  | Cic.Prop -> "Prop"
  | Cic.Set -> "Set"
  | Cic.Type _ -> "Type"
  | Cic.CProp -> "CProp"


(* MATITA NAMING CONVENTION *)

let is_prefix prefix string =
  let len = String.length prefix in
  let len1 = String.length string in
  if len <= len1 then
    begin
      let head = String.sub string 0 len in
      if ((String.compare head prefix)=0) ||
      ((String.compare head (String.lowercase prefix))=0) then 
	begin
	  let diff = len1-len in
	  let tail = String.sub string len diff in
	  if ((diff > 0) && (String.rcontains_from tail 0 '_')) then
	    Some (String.sub tail 1 (diff-1))
	    else Some tail
	  end
	else None
    end
  else None

let remove_prefix prefix (last,string) =
  if string = "" then (last,string)
  else 
    match is_prefix prefix string with
      None ->
	if last <> "" then 
	  match is_prefix last prefix with
	    None -> (last,string)
	  | Some _ ->
              (match is_prefix prefix (last^string) with
		None -> (last,string)
	      | Some tail -> (prefix,tail))
	else (last,string)
    | Some tail -> (prefix, tail)
	
let legal_suffix string = 
  if string = "" then true else
  begin
    let legal_s = Str.regexp "_?\\([0-9]+\\|r\\|l\\|'\\|\"\\)" in
    (Str.string_match legal_s string 0) && (Str.matched_string string = string)
  end

(** check if a prefix of string_name is legal for term and returns the tail.
    chec_rec cannot fail: at worst it return string_name.
    The algorithm is greedy, but last contains the last name matched, providing
    a one slot buffer. 
    string_name is here a pair (last,string_name).*)

let rec check_rec ctx string_name =
  function
    | Cic.Rel m -> 
	(match List.nth ctx (m-1) with
	  Cic.Name name ->
	    remove_prefix name string_name
	| Cic.Anonymous -> string_name)
    | Cic.Meta _ -> string_name
    | Cic.Sort sort -> remove_prefix (ppsort sort) string_name  
    | Cic.Implicit _ -> string_name
    | Cic.Cast (te,ty) -> check_rec ctx string_name te
    | Cic.Prod (name,so,dest) -> 
	let l_string_name = check_rec ctx string_name so in
	check_rec (name::ctx) string_name dest
    | Cic.Lambda (name,so,dest) -> 
        let string_name =
          match name with
            Cic.Anonymous -> string_name
          | Cic.Name name -> remove_prefix name string_name in
        let l_string_name = check_rec ctx string_name so in
	check_rec (name::ctx) l_string_name dest
    | Cic.LetIn (name,so,dest) -> 
        let string_name = check_rec ctx string_name so in
	check_rec (name::ctx) string_name dest
    | Cic.Appl l ->
	List.fold_left (check_rec ctx) string_name l
    | Cic.Var (uri,exp_named_subst) ->
	let name = UriManager.name_of_uri uri in
	remove_prefix name string_name
    | Cic.Const (uri,exp_named_subst) ->
	let name = UriManager.name_of_uri uri in
	remove_prefix name string_name
    | Cic.MutInd (uri,_,exp_named_subst) -> 
	let name = UriManager.name_of_uri uri in
	remove_prefix name string_name  
    | Cic.MutConstruct (uri,n,m,exp_named_subst) ->
	let name =
          (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
	    Cic.InductiveDefinition (dl,_,_,_) ->
	      let (_,_,_,cons) = get_nth dl (n+1) in
	      let (id,_) = get_nth cons m in
	      id 
	  | _ -> assert false) in
	remove_prefix name string_name  
    | Cic.MutCase (_,_,_,te,pl) ->
	let strig_name = remove_prefix "match" string_name in
	let string_name = check_rec ctx string_name te in
        List.fold_right (fun t s -> check_rec ctx s t) pl string_name
    | Cic.Fix (_,fl) ->
        let strig_name = remove_prefix "fix" string_name in
        let names = List.map (fun (name,_,_,_) -> name) fl in
        let onames =
          List.rev (List.map (function name -> Cic.Name name) names)
        in
        List.fold_right 
	  (fun (_,_,_,bo) s -> check_rec (onames@ctx) s bo) fl string_name
    | Cic.CoFix (_,fl) ->
	let strig_name = remove_prefix "cofix" string_name in
        let names = List.map (fun (name,_,_) -> name) fl in
        let onames =
          List.rev (List.map (function name -> Cic.Name name) names)
        in
        List.fold_right 
	  (fun (_,_,bo) s -> check_rec (onames@ctx) s bo) fl string_name

let check_name ?(allow_suffix=false) ctx name term =
  let (_,tail) = check_rec ctx ("",name) term in
  if (not allow_suffix) then (String.length tail = 0) 
  else legal_suffix tail

let check_elim ctx conclusion_name =
  let elim = Str.regexp "_elim\\|_case" in
  if (Str.string_match elim conclusion_name 0) then
    let len = String.length conclusion_name in
    let tail = String.sub conclusion_name 5 (len-5) in
    legal_suffix tail
  else false

let rec check_names ctx hyp_names conclusion_name t =
  match t with
    | Cic.Prod (name,s,t) -> 
	(match hyp_names with
	     [] -> check_names (name::ctx) hyp_names conclusion_name t
	   | hd::tl ->
	       if check_name ctx hd s then 
		 check_names (name::ctx) tl conclusion_name t
	       else 
		 check_names (name::ctx) hyp_names conclusion_name t)
    | Cic.Appl ((Cic.Rel n)::args) -> 
  	(match hyp_names with
 	  | [] ->
	      (check_name ~allow_suffix:true ctx conclusion_name t) ||
              (check_elim ctx conclusion_name)
	  | [what_to_elim] ->   
              (* what to elim could be an argument 
                 of the predicate: e.g. leb_elim *)
	      let (last,tail) = 
		List.fold_left (check_rec ctx) ("",what_to_elim) args in
              (tail = "" && check_elim ctx conclusion_name)
	  | _ -> false)
    | Cic.MutCase  (_,_,Cic.Lambda(name,so,ty),te,_) ->
	(match hyp_names with
 	  | [] ->
               (match is_prefix "match" conclusion_name with
		   None -> check_name ~allow_suffix:true ctx conclusion_name t
	       | Some tail -> check_name ~allow_suffix:true ctx tail t)
	  | [what_to_match] ->   
              (* what to match could be the term te or its type so; in this case the
                 conclusion name should match ty *)
	      check_name ~allow_suffix:true (name::ctx) conclusion_name ty &&
              (check_name ctx what_to_match te || check_name ctx what_to_match so)
	  | _ -> false)
    | _ -> 
	hyp_names=[] && check_name ~allow_suffix:true ctx conclusion_name t

let check name term =
  let names = Str.split (Str.regexp_string "_to_") name in
  let hyp_names,conclusion_name =
    match List.rev names with
	[] -> assert false
      | hd::tl -> 
          let elim = Str.regexp "_elim\\|_case" in
          let len = String.length hd in
          try 
	    let pos = Str.search_backward elim hd len in
	    let hyp = String.sub hd 0 pos in
	    let concl = String.sub hd pos (len-pos) in
	    List.rev (hyp::tl),concl
          with Not_found -> (List.rev tl),hd in
  check_names [] hyp_names conclusion_name term
;;