(************************************************************************)
(*         *      The Rocq Prover / The Rocq 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.
    Non global expressions such as existential variables are not allowed. *)

type notation_constr =
  (* Part common to [glob_constr] and [cases_pattern] *)
  | NRef of GlobRef.t * glob_instance option
  | NVar of Id.t
  | NApp of notation_constr * notation_constr list
  | NProj of (Constant.t * glob_instance option) * notation_constr list * notation_constr
  | NHole of glob_evar_kind
  | NGenarg of GenConstr.glb
  | 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 option * notation_constr
  | NInt of Uint63.t
  | NFloat of Float64.t
  | NString of Pstring.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 = Constrexpr.scope_delimiter list

type extended_subscopes = Constrexpr.notation_entry_relative_level * subscopes

(** The set of other notation variables that are bound to a binder or
    binder list and that bind the given notation variable, for
    instance, in ["{ x | P }" := (sigT (fun x => P)], "x" is under an
    empty set of binders and "P" is under the binders bound to "x",
    that is, its notation_var_binders set is "x" *)
type notation_var_binders = Id.Set.t

(** 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_kind =
  (* This accepts only ident *)
  | AsIdent
  (* This accepts only name *)
  | AsName
  (* This accepts pattern *)
  | AsAnyPattern
  (* This accepts only strict pattern (i.e. no single variable) at printing *)
  | AsStrictPattern

type notation_binder_source =
  (* Parsed as constr and constrained to be ident, name or pattern, depending on kind *)
  | NtnBinderParsedAsConstr of notation_binder_kind
  (* Parsed and interpreted as ident, name or pattern, depending on kind *)
  | NtnBinderParsedAsSomeBinderKind of notation_binder_kind
  (* Parsed as open or closed binder: This accepts ident, _, quoted pattern, etc. *)
  | NtnBinderParsedAsBinder

type notation_var_constr_kind =
  | NtnAlwaysConstr (* In anticipation of supporting PatCast in
      pattern, which is a case where a constr in a pattern should be
      kept as a constr and not interpreted by default as a pattern *)
  | NtnConstrForConstrAndPatternForPattern

(** Type of variables in notation interpretations, remembering how it is parsed;
    Note: when a notation variable appears both as term and as binder, its type is Pattern *)
type notation_var_kind =
  | NtnTypeVarConstr of notation_var_constr_kind
  | NtnTypeVarPattern of notation_binder_source
  | NtnTypeVarBinders of notation_binder_source

type notation_var_type =
  | NtnTypeVar of (extended_subscopes * notation_var_binders) * notation_var_kind
  | NtnTypeVarList of notation_var_type (* list A *)
  | NtnTypeVarTuple of notation_var_type list (* A1 * ... * An *)

(** 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 'a interpretation_gen = (Id.t * 'a) list * notation_constr
type interpretation = notation_var_type interpretation_gen
  (* (var_types, n) is a pair with a notation n and the type of its
     non terminals, var_types is a list giving a name and a type to
     each non terminal. Type invariant: the length of var_types is the
     number of non terminals appearing in n, as given by the function
     TODO *)

type forgetfulness = { forget_ltac : bool; forget_volatile_cast : bool }

type reversibility_status =
  | APrioriReversible
  | Forgetful of forgetfulness
  | NonInjective of Id.t list

type notation_interp_var_types = notation_var_internalization_type Names.Id.Map.t

type 'a notation_raw_type =
  | NtnRawTypeVar of 'a
  | NtnRawTypeVarList of ('a * 'a) notation_raw_type (* A .. A *)
      (* represented as a pattern pat(x) ... pat(y) in the declaration
         of the notation and we keep the names of the two ends (note
         that this may multiply in case of nested recursive patterns) *)
  | NtnRawTypeVarTuple of 'a notation_raw_type list (* A1 * ... * An *)

type notation_interp_env = {
  ninterp_var_type : notation_interp_var_types;
  ninterp_raw_types : Id.t notation_raw_type list;
}