Codebase list coq / debian/8.0pl3-2 parsing / extend.mli
debian/8.0pl3-2

Tree @debian/8.0pl3-2 (Download .tar.gz)

extend.mli @debian/8.0pl3-2 — raw · history · blame 

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
(************************************************************************)
(*  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.2 2005/01/21 16:42: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

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

(* 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