open Sign;;
open Classops;;
open Names;;
open Nameops
open Coqast;;
open Ast;;
open Termast;;
open Term;;
open Impargs;;
open Reduction;;
open Libnames;;
open Libobject;;
open Environ;;
open Declarations;;
open Prettyp;;
open Inductive;;
open Util;;
open Pp;;
open Declare;;
open Nametab
open Vernacexpr;;
open Decl_kinds;;
open Constrextern;;
open Topconstr;;

(* This function converts the parameter binders of an inductive definition,
   in particular you have to be careful to handle each element in the
   context containing all previously defined variables.  This squeleton
   of this procedure is taken from the function print_env in pretty.ml *)
let convert_env =
    let convert_binder env (na, b, c) =
      match b with 
       | Some b -> LocalRawDef ((dummy_loc,na), extern_constr true env b)
       | None -> LocalRawAssum ([dummy_loc,na], extern_constr true env c) in
    let rec cvrec env = function
       [] -> []
     | b::rest -> (convert_binder env b)::(cvrec (push_rel b env) rest) in
    cvrec (Global.env());;

(* let mib string = 
     let sp = Nametab.sp_of_id CCI (id_of_string string) in
     let lobj = Lib.map_leaf (objsp_of sp) in
     let (cmap, _) = outMutualInductive lobj in
     Listmap.map cmap CCI;; *)

(* This function is directly inspired by print_impl_args in pretty.ml *)

let impl_args_to_string_by_pos = function
    [] -> None
  | [i] -> Some(" position " ^ (string_of_int i) ^ " is implicit.")
  | l -> Some (" positions " ^
                (List.fold_right (fun i s -> (string_of_int i) ^ " " ^ s)
                     l
                     " are implicit."));;

(* This function is directly inspired by implicit_args_id in pretty.ml *)

let impl_args_to_string l = 
  impl_args_to_string_by_pos (positions_of_implicits l)

let implicit_args_id_to_ast_list id l ast_list = 
    (match impl_args_to_string l with
           None -> ast_list
         | Some(s) -> CommentString s::
                      CommentString ("For " ^ (string_of_id id))::
                      ast_list);;

(* This function construct an ast to enumerate the implicit positions for an
   inductive type and its constructors. It is obtained directly from
   implicit_args_msg in pretty.ml.  *)

let implicit_args_to_ast_list sp mipv =
    let implicit_args_descriptions = 
      let ast_list = ref [] in
       	(Array.iteri
           (fun i mip  ->
	      let imps = implicits_of_global (IndRef (sp, i)) in
		      (ast_list :=
	      	implicit_args_id_to_ast_list mip.mind_typename imps !ast_list;
	      	Array.iteri
		  (fun j idc ->
		     let impls = implicits_of_global
		       (ConstructRef ((sp,i),j+1)) in
		       ast_list := 
		       implicit_args_id_to_ast_list idc impls !ast_list)
		  mip.mind_consnames))
	  mipv;
	 !ast_list) in
      match implicit_args_descriptions with
	  [] -> []
	| _ -> [VernacComments (List.rev implicit_args_descriptions)];;
	      
let convert_qualid qid =
  let d, id = Libnames.repr_qualid qid in
    match repr_dirpath d with
	[] -> nvar id
      | d -> ope("QUALID", List.fold_left (fun l s -> (nvar s)::l)
		   [nvar id] d);;

(* This function converts constructors for an inductive definition to a
   Coqast.t.  It is obtained directly from print_constructors in pretty.ml *)

let convert_constructors envpar names types =
  let array_idC = 
    array_map2 
      (fun n t -> 
	let coercion_flag = false (* arbitrary *) in
	(coercion_flag, ((dummy_loc,n), extern_constr true envpar t)))
      names types in
  Array.to_list array_idC;;
  
(* this function converts one inductive type in a possibly multiple inductive
   definition *)

let convert_one_inductive sp tyi =
  let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
  let env = Global.env () in
  let envpar = push_rel_context params env in
  let sp = sp_of_global (IndRef (sp, tyi)) in
  ((dummy_loc,basename sp), None,
   convert_env(List.rev params),
   (extern_constr true envpar arity),
   convert_constructors envpar cstrnames cstrtypes);;

(* This function converts a Mutual inductive definition to a Coqast.t.
   It is obtained directly from print_mutual in pretty.ml.  However, all
   references to kinds have been removed and it treats only CCI stuff. *)

let mutual_to_ast_list sp mib =
  let mipv = (Global.lookup_mind sp).mind_packets in
  let _, l =
    Array.fold_right
      (fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in
  VernacInductive (mib.mind_finite, l)
  :: (implicit_args_to_ast_list sp mipv);;

let constr_to_ast v = 
  extern_constr true (Global.env()) v;;

let implicits_to_ast_list implicits =
  match (impl_args_to_string implicits) with
    | None -> []
    | Some s -> [VernacComments [CommentString s]];;

(*
let make_variable_ast name typ implicits =
   (ope("VARIABLE",
    [string "VARIABLE";
     ope("BINDERLIST",
         [ope("BINDER",
            [(constr_to_ast (body_of_type typ));
             nvar name])])]))::(implicits_to_ast_list implicits)
    ;;
*)
let make_variable_ast name typ implicits =
  (VernacAssumption
    ((Local,Definitional),
     [false,([dummy_loc,name], constr_to_ast (body_of_type typ))]))
  ::(implicits_to_ast_list implicits);;
    

let make_definition_ast name c typ implicits =
  VernacDefinition ((Global,Definition), (dummy_loc,name), DefineBody ([], None,
    (constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
    (fun _ _ -> ()))
  ::(implicits_to_ast_list implicits);;

(* This function is inspired by print_constant *)
let constant_to_ast_list kn =
  let cb = Global.lookup_constant kn in
  let c = cb.const_body in
  let typ = cb.const_type in
  let l = implicits_of_global (ConstRef kn) in
  (match c with
      None -> 
	make_variable_ast (id_of_label (label kn)) typ l
    | Some c1 ->
	make_definition_ast (id_of_label (label kn)) (Declarations.force c1) typ l)

let variable_to_ast_list sp =
  let (id, c, v) = get_variable sp in
  let l = implicits_of_global (VarRef sp) in
    (match c with
	 None -> 
	   make_variable_ast id v l
       | Some c1 ->
	   make_definition_ast id c1 v l);;

(* this function is taken from print_inductive in file pretty.ml *)

let inductive_to_ast_list sp =
  let mib = Global.lookup_mind sp in
  mutual_to_ast_list sp mib

(* this function is inspired by print_leaf_entry from pretty.ml *)

let leaf_entry_to_ast_list ((sp,kn),lobj) =
  let tag = object_tag lobj in
  match tag with
  | "VARIABLE" -> variable_to_ast_list (basename sp)
  | "CONSTANT" -> constant_to_ast_list kn
  | "INDUCTIVE" -> inductive_to_ast_list kn
  | s -> 
      errorlabstrm 
      	"print" (str ("printing of unrecognized object " ^
		      s ^ " has been required"));;




(* this function is inspired by print_name *)
let name_to_ast ref =
  let (loc,qid) = qualid_of_reference ref in
  let l = 
    try
      let sp = Nametab.locate_obj qid in
      let (sp,lobj) = 
      	let (sp,entry) =
          List.find (fun en -> (fst (fst en)) = sp) (Lib.contents_after None)
      	in
	  match entry with
            | Lib.Leaf obj -> (sp,obj)
            | _ -> raise Not_found
      in
    	leaf_entry_to_ast_list (sp,lobj)
    with Not_found -> 
      try 
    	match Nametab.locate qid with
	  | ConstRef sp -> constant_to_ast_list sp
	  | IndRef (sp,_) -> inductive_to_ast_list sp
	  | ConstructRef ((sp,_),_) -> inductive_to_ast_list sp
	  | VarRef sp -> variable_to_ast_list sp
  	with Not_found -> 
	  try  (* Var locale de but, pas var de section... donc pas d'implicits *)
	    let dir,name = repr_qualid qid in 
	      if (repr_dirpath dir) <> [] then raise Not_found;
	      let (_,c,typ) = Global.lookup_named name in 
		(match c with
		     None -> make_variable_ast name typ []
		   | Some c1 -> make_definition_ast name c1 typ [])
	  with Not_found ->
	    try
	      let sp = Nametab.locate_syntactic_definition qid in
		errorlabstrm "print"
      		  (str "printing of syntax definitions not implemented")
	    with Not_found ->
	      errorlabstrm "print"
		(pr_qualid qid ++
		 spc () ++ str "not a defined object")
  in
  VernacList (List.map (fun x -> (dummy_loc,x)) l)