(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id: extend.mli,v 1.19.2.1 2004/07/16 19:30:37 herbelin Exp $ i*)

(*i*)
open Pp
open Util
open Names
open Ast
open Coqast
open Ppextend
open Topconstr
open Genarg
(*i*)

type entry_type = argument_type

type production_position =
  | BorderProd of bool * Gramext.g_assoc option  (* true=left; false=right *)
  | InternalProd

type production_level =
  | NextLevel
  | NumLevel of int

type ('lev,'pos) constr_entry_key =
  | ETIdent | ETReference | ETBigint
  | ETConstr of ('lev * 'pos)
  | ETPattern
  | ETOther of string * string
  | ETConstrList of ('lev * 'pos) * Token.pattern list

type constr_production_entry =
    (production_level,production_position) constr_entry_key
type constr_entry = (int,unit) constr_entry_key
type simple_constr_production_entry = (production_level,unit) constr_entry_key

type nonterm_prod =
  | ProdList0 of nonterm_prod
  | ProdList1 of nonterm_prod * Token.pattern list
  | ProdOpt of nonterm_prod
  | ProdPrimitive of constr_production_entry

type prod_item =
  | Term of Token.pattern
  | NonTerm of constr_production_entry * 
      (Names.identifier * constr_production_entry) option

type grammar_rule = {
  gr_name : string; 
  gr_production : prod_item list; 
  gr_action : constr_expr }

type grammar_entry = { 
  ge_name : constr_entry;
  gl_assoc : Gramext.g_assoc option;
  gl_rules : grammar_rule list }

type grammar_command = { 
  gc_univ : string; 
  gc_entries : grammar_entry list }

type grammar_associativity = Gramext.g_assoc option

(* Globalisation and type-checking of Grammar actions *)
type entry_context = identifier list

val set_constr_globalizer : 
  (entry_context -> constr_expr -> constr_expr) -> unit

type syntax_modifier =
  | SetItemLevel of string list * production_level
  | SetLevel of int
  | SetAssoc of Gramext.g_assoc
  | SetEntryType of string * simple_constr_production_entry
  | SetOnlyParsing
  | SetFormat of string located

type nonterm =
  | NtShort of string
  | NtQual of string * string
type grammar_production =
  | VTerm of string
  | VNonTerm of loc * nonterm * Names.identifier option
type raw_grammar_rule = string * grammar_production list * grammar_action
type raw_grammar_entry = string * grammar_associativity * raw_grammar_rule list

val terminal : string -> string * string

val rename_command_entry : string -> string

val explicitize_entry : string -> string -> constr_entry

val subst_grammar_command : 
  Names.substitution -> grammar_command -> grammar_command

(* unparsing objects *)

type 'pat unparsing_hunk = 
  | PH of 'pat * string option * parenRelation
  | RO of string
  | UNP_BOX of ppbox * 'pat unparsing_hunk list
  | UNP_BRK of int * int
  | UNP_TBRK of int * int
  | UNP_TAB
  | UNP_FNL
  | UNP_SYMBOLIC of string option * string * 'pat unparsing_hunk

(*val subst_unparsing_hunk : 
  Names.substitution -> (Names.substitution -> 'pat -> 'pat) -> 
  'pat unparsing_hunk -> 'pat unparsing_hunk
*)

(* Checks if the precedence of the parent printer (None means the
   highest precedence), and the child's one, follow the given
   relation. *)

val tolerable_prec : tolerability option -> precedence -> bool

type 'pat syntax_entry = {
  syn_id : string;
  syn_prec: precedence;
  syn_astpat : 'pat;
  syn_hunks : 'pat unparsing_hunk list }

val subst_syntax_entry : 
  (Names.substitution -> 'pat -> 'pat) -> 
  Names.substitution -> 'pat syntax_entry -> 'pat syntax_entry


type 'pat syntax_command = { 
  sc_univ : string; 
  sc_entries : 'pat syntax_entry list }

val subst_syntax_command : 
  (Names.substitution -> 'pat -> 'pat) -> 
  Names.substitution -> 'pat syntax_command -> 'pat syntax_command

type syntax_rule = string * Coqast.t * Coqast.t unparsing_hunk list
type raw_syntax_entry = precedence * syntax_rule list

val interp_grammar_command :
  string -> (string * string -> unit) -> 
      raw_grammar_entry list -> grammar_command

val interp_syntax_entry :
  string -> raw_syntax_entry list -> Ast.astpat syntax_command