aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/extend.mli
blob: 086d1b2ebcbb75e6ea3a7a7dc0790ab373353e54 (plain)
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

(*i $Id$ i*)

(*i*)
open Pp
open Pcoq
(*i*)

(* Parsing. *)

type nonterm =
  | NtShort of string
  | NtQual of string * string

val qualified_nterm : (string * gram_universe) -> nonterm ->
  (string * gram_universe) * string

type prod_item =
  | Term of Token.pattern
  | NonTerm of nonterm * entry_type * string option

type grammar_rule = { 
  gr_name : string; 
  gr_production : prod_item list; 
  gr_action : Ast.act }

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

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

val gram_assoc : Coqast.t -> Gramext.g_assoc option

val interp_grammar_command : string -> Coqast.t list -> grammar_command


(*s Pretty-print. *)

(* Dealing with precedences *)

type precedence = int * int * int

type parenRelation = L | E | Any

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

type tolerability = (string * precedence) * parenRelation

val tolerable_prec : tolerability option -> (string * precedence) -> bool

(* unparsing objects *)

type ppbox =
  | PpHB of int
  | PpHOVB of int
  | PpHVB of int
  | PpVB of int
  | PpTB

type unparsing_hunk = 
  | PH of Ast.pat * (string * tolerability option) option * parenRelation
  | RO of string
  | UNP_BOX of ppbox * unparsing_hunk list
  | UNP_BRK of int * int
  | UNP_TBRK of int * int
  | UNP_TAB
  | UNP_FNL

val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds

val unparsing_of_ast : Ast.entry_env -> Coqast.t -> unparsing_hunk list

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

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

val interp_syntax_entry : string -> Coqast.t list -> syntax_command