Module SyntaxDef

module SyntaxDef: sig .. end
Contains the type of syntax elements and definitions, basic functions for syntax definitions and printing with names generated from syntax definitions and a few basic syntax definitions of types and constructors.

type syntax_elem = 
| Str of string
| Tp of Term.term
Elements of the "right hand side" of a grammar rule.
type syntax_def = 
| SDterm of syntax_elem list * Term.term list
| SDvar of syntax_elem list * Term.term
| SDtvar of string * Term.term option
Grammar rules for functor terms (functions/constants/classes), for (sharing) variables and for type variables. Type variable has an optional supertype, i.e. its upper bound.
type sdef_result = 
| SD_Term of Term.term array
| SD_SVar of Term.term
| SD_TVar of Term.term option
Supertypes and whether we define a variable. Minor current and perhaps bigger future use.

Basic functions on Syntax Definitions, generating names

val syntax_elems_of_sd : syntax_def -> syntax_elem list
val result_of_sd : syntax_def -> sdef_result
val name_of_sd : syntax_def -> string
val unique_name_of_sd : syntax_def -> string list -> string
val term_of_sd : ?used_names:string list -> ?name:string -> syntax_def -> Term.term
A helper function returning type with level indication, or ?t.
val type_with_level_of_sd : syntax_def -> Term.term

Functions for printing based on Syntax Definitions

val split_sd_name : string -> string option list
val put_space : string -> string -> string
val display_sd : string option list -> string list -> string
val display_sd_bracketed : string option list -> string list -> string

Pretty printing Types and Syntax Definitions

Simple conversion to EBNF grammar

exception NONLEXICAL
val flat_grammar_of_sd_list : syntax_def list -> (string * string list list) list
val print_grammar : (string * string list list) list -> string

XSLT output for Syntax Definitions with names

val make_xml_compatible : string -> string
val print_xslt : string -> (string * syntax_def) list -> string