(* 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 H = HExtlib
module C = Content
module G = GrafiteAst

(* grafite ast constructors *************************************************)

let floc = H.dummy_floc

let mk_note str = G.Comment (floc, G.Note (floc, str))
   
(* interface functions ******************************************************)

let out_arg = function
   | C.Aux _       -> "aux"
   | C.Premise _   -> "premise"
   | C.Lemma _     -> "lemma"
   | C.Term _      -> "term"
   | C.ArgProof _  -> "proof"
   | C.ArgMethod _ -> "method"

let out_args args = String.concat " " (List.map out_arg args) 

let out_name = function
   | None     -> ""
   | Some str -> str

let content2procedural ~ids_to_inner_sorts prefix (_, params, xmenv, obj) = 
   if List.length params > 0 || xmenv <> None then assert false;
   match obj with
      | `Def (C.Const, t, `Proof {
           C.proof_name = Some name; C.proof_context = []; 
	   C.proof_apply_context = []; C.proof_conclude = {
	      C.conclude_conclusion = Some b
	   }
        }) -> 	
	[mk_note (Printf.sprintf "%s" name)]
      | _ -> assert false