Codebase list coq / 22a9921b-8439-4643-b89f-f8d6f2bc9c55/main interp / notation_term.ml
22a9921b-8439-4643-b89f-f8d6f2bc9c55/main

Tree @22a9921b-8439-4643-b89f-f8d6f2bc9c55/main (Download .tar.gz)

notation_term.ml @22a9921b-8439-4643-b89f-f8d6f2bc9c55/main — 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
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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 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 GlobRef.t * glob_level list option
  | NVar of Id.t
  | NApp of notation_constr * notation_constr list
  | NProj of (Constant.t * glob_level list option) * notation_constr list * notation_constr
  | NHole of Evar_kinds.t * Namegen.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 option * notation_constr
  | NProd of Name.t * notation_constr option * 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 glob_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 * Constr.cast_kind * notation_constr
  | NInt of Uint63.t
  | NFloat of Float64.t
  | NArray of notation_constr array * notation_constr * 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 extended_subscopes = Constrexpr.notation_entry_level * subscopes

(** 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 constr_as_binder_kind =
  | AsIdent
  | AsName
  | AsNameOrPattern
  | AsStrictPattern

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 only name *)
  | NtnParsedAsName
  (* This accepts ident, or pattern, or both *)
  | NtnBinderParsedAsConstr of constr_as_binder_kind
  (* This accepts ident, _, and quoted pattern *)
  | NtnParsedAsBinder

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 of scope_name option
  | NtnInternTypeOnlyBinder

(** This characterizes to what a notation is interpreted to *)
type interpretation =
    (Id.t * (extended_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;
}