aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation_term.ml
blob: a9c2e2a53294e6f3902efa2a170383412833ef3f (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
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
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Names
open Globnames
open Misctypes
open Glob_term

(** [notation_constr] *)

(** [notation_constr] is the subtype of [glob_constr] allowed in syntactic
    extensions (i.e. notations).
    No location since intended to be substituted at any place of a text.
    Complex expressions such as fixpoints and cofixpoints are excluded,
    as well as non global expressions such as existential variables. *)

type notation_constr =
  (** Part common to [glob_constr] and [cases_pattern] *)
  | NRef of global_reference
  | NVar of Id.t
  | NApp of notation_constr * notation_constr list
  | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option
  | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
  (** Part only in [glob_constr] *)
  | NLambda of Name.t * notation_constr * notation_constr
  | NProd of Name.t * notation_constr * notation_constr
  | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
  | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr
  | NCases of Constr.case_style * notation_constr option *
      (notation_constr * (Name.t * (inductive * Name.t list) option)) list *
      (cases_pattern list * notation_constr) list
  | NLetTuple of Name.t list * (Name.t * notation_constr option) *
      notation_constr * notation_constr
  | NIf of notation_constr * (Name.t * notation_constr option) *
      notation_constr * notation_constr
  | NRec of fix_kind * Id.t array *
      (Name.t * notation_constr option * notation_constr) list array *
      notation_constr array * notation_constr array
  | NSort of glob_sort
  | NCast of notation_constr * notation_constr cast_type
  | NProj of Projection.t * notation_constr

(** Note concerning NList: first constr is iterator, second is terminator;
    first id is where each argument of the list has to be substituted
    in iterator and snd id is alternative name just for printing;
    boolean is associativity *)

(** Types concerning notations *)

type scope_name = string

type tmp_scope_name = scope_name

type subscopes = tmp_scope_name option * scope_name list

(** Type of the meta-variables of an notation_constr: in a recursive pattern x..y,
    x carries the sequence of objects bound to the list x..y  *)

type notation_binder_source =
  (* This accepts only pattern *)
  (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *)
  | NtnParsedAsPattern of bool
  (* This accepts only ident *)
  | NtnParsedAsIdent
  (* This accepts ident, or pattern, or both *)
  | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind

type notation_var_instance_type =
  | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList

(** Type of variables when interpreting a constr_expr as a notation_constr:
    in a recursive pattern x..y, both x and y carry the individual type
    of each element of the list x..y *)
type notation_var_internalization_type =
  | NtnInternTypeAny | NtnInternTypeOnlyBinder

(** This characterizes to what a notation is interpreted to *)
type interpretation =
    (Id.t * (subscopes * notation_var_instance_type)) list *
    notation_constr

type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list

type notation_interp_env = {
  ninterp_var_type : notation_var_internalization_type Id.Map.t;
  ninterp_rec_vars : Id.t Id.Map.t;
}

type grammar_constr_prod_item =
  | GramConstrTerminal of Tok.t
  | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option
  | GramConstrListMark of int * bool * int
    (* tells action rule to make a list of the n previous parsed items;
       concat with last parsed list when true; additionally release
       the p last items as if they were parsed autonomously *)

(** Dealing with precedences *)

type precedence = int
type parenRelation = L | E | Any | Prec of precedence
type tolerability = precedence * parenRelation

type level = precedence * tolerability list * Extend.constr_entry_key list

(** Grammar rules for a notation *)

type one_notation_grammar = {
  notgram_level : level;
  notgram_assoc : Extend.gram_assoc option;
  notgram_notation : Constrexpr.notation;
  notgram_prods : grammar_constr_prod_item list list;
}

type notation_grammar = {
  notgram_onlyprinting : bool;
  notgram_rules : one_notation_grammar list
}