%
%% Grammar for user language. Generates ./src/ast.ml
%%

indexvar n , m , i , j ::=
  {{ phantom }}
  {{ com Index variables for meta-lists }}

metavar num,numZero,numOne ::=
  {{ phantom }}
  {{ lex numeric }}
  {{ ocaml big_int }}
  {{ hol num }}
  {{ lem integer }}
  {{ isa int }}
  {{ com Numeric literals }}

metavar nat ::=
  {{ phantom }}
  {{ ocaml int }}
  {{ lex numeric }}
  {{ lem nat }}
  {{ isa nat }}

metavar hex ::=
  {{ phantom }}
  {{ lex numeric }}
  {{ ocaml string }}
  {{ lem string }}
  {{ isa string }}
  {{ com Bit vector literal, specified by C-style hex number }}

metavar bin ::=
  {{ phantom }}
  {{ lex numeric }}
  {{ ocaml string }}
  {{ lem string }}
  {{ isa string }}
  {{ com Bit vector literal, specified by C-style binary number }}

metavar string ::=
  {{ phantom }}
  {{ ocaml string }}
  {{ lem string }}
  {{ hol string }}
  {{ isa string }}
  {{ com String literals }}

metavar regexp ::=
  {{ phantom }}
  {{ ocaml string }}
  {{ lem string }}
  {{ hol string }}
  {{ isa string }}
  {{ com Regular expressions, as a string literal }}

metavar real ::=
   {{ phantom }}
  {{ ocaml string }}
  {{ lem string }}
  {{ hol string }}
  {{ isa string }}
  {{ com Real number literal }}

metavar value ::=
  {{ phantom }}
  {{ ocaml value }}
  {{ lem value }}
  {{ isa value }}

metavar attribute_data ::=
  {{ phantom }}
  {{ ocaml attribute_data }}
  {{ lem attribute_data }}

embed
{{ ocaml

open Big_int
open Value

type text = string

type l = Parse_ast.l
type attribute_data = Parse_ast.Attribute_data.attribute_data

type 'a annot = l * 'a

type loop = While | Until

type extern = { pure : bool; bindings : (string * string) list } option

type visibility = Public | Private of  l

type 'a def_annot = {
    doc_comment : string option;
    attrs : (l * string * config) list;
    visibility : visibility;
    loc : l;
    env : 'a
}

type 'a clause_annot = unit def_annot * 'a

}}

embed
{{ lem

type ocaml_l
declare ocaml target_rep type ocaml_l = `Parse_ast.l`

type l = ocaml_l

type ocaml_attribute_data
declare ocaml target_rep type ocaml_attribute_data = `Parse_ast.Attribute_data.attribute_data`

type attribute_data = ocaml_attribute_data

type value
declare ocaml target_rep type value = `Value.value`

type loop = While | Until

type annot 'a = l * 'a

type extern = <| pure : bool; bindings : list (string * string) |>

type visibility = Public | Private of l

type def_annot 'a = <|
    doc_comment : maybe string;
    attrs : list (l * string * maybe attribute_data);
    visibility : visibility;
    loc : l;
    env : 'a
|>

type clause_annot 'a = def_annot unit * 'a

}}

embed
{{ isa

datatype "l" = Unknown

datatype "value" = Val

datatype "loop" = While | Until

type_synonym "annot" = l

}}

metavar x , y , z ::=
  {{ ocaml text }}
  {{ lem string }}
  {{ hol string }}
  {{ isa string }}
  {{ com identifier }}
  {{ ocamlvar "[[x]]" }}
  {{ lemvar "[[x]]" }}


metavar ix ::=
  {{ lex alphanum }}
  {{ ocaml text }}
  {{ lem string }}
  {{ hol string }}
  {{ isa string }}
  {{ com infix identifier }}
  {{ ocamlvar "[[ix]]" }}
  {{ lemvar "[[ix]]" }}


grammar

external :: '' ::=
  {{ phantom }}
  {{ lem maybe extern }}
  {{ ocaml extern option }}

def_annot :: '' ::=
  {{ phantom }}
  {{ lem def_annot 'b }}
  {{ ocaml 'b def_annot }}

clause_annot :: '' ::=
  {{ phantom }}
  {{ lem clause_annot 'a }}
  {{ ocaml 'a clause_annot }}

union_annot :: '' ::=
  {{ phantom }}
  {{ lem def_annot unit }}
  {{ ocaml unit def_annot }}

l :: '' ::=
  {{ phantom }}
  {{ ocaml Parse_ast.l }}
  {{ lem l }}
  {{ hol unit }}
  {{ com source location }}
  | :: :: Unknown
    {{ ocaml Unknown }}
    {{ lem Unknown }}
    {{ hol () }}

annot :: '' ::=
  {{ phantom }}
  {{ ocaml 'a annot }}
  {{ lem annot 'a }}
  {{ hol unit }}

id :: '' ::=
  {{ com Identifier }}
  {{ aux _ l }}
  | x              :: :: id
  | ( operator x ) :: D :: operator {{ com remove infix status }}

kid :: '' ::=
  {{ com kinded IDs: Type, Int, and Bool variables }}
  {{ aux _ l }}
  | ' x :: :: var

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Kinds and Types                                              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

grammar

kind :: 'K_' ::=
  {{ com base kind}}
  {{ aux _ l }}
  | Type  :: :: type  {{ com kind of types  }}
  | Int   :: :: int   {{ com kind of natural number size expressions  }}
  | Bool  :: :: bool  {{ com kind of constraints }}

nexp :: 'Nexp_' ::=
  {{ com numeric expression, of kind Int }}
  {{ aux _ l }}
  | id                                    :: :: id       {{ com abbreviation identifier }}
  | kid                                   :: :: var      {{ com variable }}
  | num                                   :: :: constant {{ com constant }}
  | id ( nexp1 , ... , nexpn )            :: :: app      {{ com app }}
  | if n_constraint then nexp1 else nexp2 :: :: if       {{ com if-then-else }}
  | nexp1 * nexp2                         :: :: times    {{ com product }}
  | nexp1 + nexp2                         :: :: sum      {{ com sum }}
  | nexp1 - nexp2                         :: :: minus    {{ com subtraction }}
  | 2 ^ nexp                              :: :: exp      {{ com exponential }}
  | - nexp                                :: :: neg      {{ com unary negation}}
  | ( nexp )                              :: S :: paren  {{ ichlo [[nexp]] }}

order :: 'Ord_' ::=
  {{ com vector order specifications, of kind Order }}
  {{ aux _ l }}
  | inc                                 :: :: inc {{ com increasing }}
  | dec                                 :: :: dec {{ com decreasing }}
  | ( order )                           :: S :: paren {{ ichlo [[order]] }}

typ :: 'Typ_' ::=
  {{ com type expressions, of kind Type }}
  {{ aux _ l }}
  |                                               :: :: internal_unknown
  | id                                            :: :: id {{ com defined type }}
  | kid                                           :: :: var {{ com type variable }}
  | ( typ1 , ... , typn ) -> typ2                 :: :: fn {{ com Function (first-order only) }}
  | typ1 <-> typ2                                 :: :: bidir {{ com Mapping }}
  | ( typ1 , .... , typn )                        :: :: tuple {{ com Tuple }}
  | id ( typ_arg1 , ... , typ_argn )              :: :: app {{ com type constructor application }}
  | ( typ )                                       :: S :: paren {{ ichlo [[typ]] }}
  | { kinded_id1 ...  kinded_idn , n_constraint . typ }
    :: :: exist

typ_arg :: 'A_' ::=
  {{ com type constructor arguments of all kinds }}
  {{ aux _ l }}
  | nexp         :: :: nexp
  | typ          :: :: typ
  | n_constraint :: :: bool

n_constraint :: 'NC_' ::=
  {{ com constraint over kind Int }}
  {{ aux _ l }}
  | typ_arg == typ_arg'              :: :: equal
  | typ_arg != typ_arg'              :: :: not_equal
  | nexp >= nexp'                    :: :: ge
  | nexp > nexp'                     :: :: gt
  | nexp '<=' nexp'                  :: :: le
  | nexp '<' nexp'                   :: :: lt
  | nexp 'IN' { num1 , ... , numn }  :: :: set
  | n_constraint & n_constraint'     :: :: and
  | n_constraint | n_constraint'     :: :: or
  | id ( typ_arg0 , ... , typ_argn ) :: :: app
  | id                               :: :: id
  | kid                              :: :: var
  | true                             :: :: true
  | false                            :: :: false

kinded_id :: 'KOpt_' ::=
  {{ com optionally kind-annotated identifier }}
  {{ aux _ l }}
  | kind kid       :: :: kind {{ com kind-annotated variable }}
  | kid            :: S :: none {{ ichlo [[kid]] }}

quant_item :: 'QI_' ::=
  {{ com kinded identifier or Int constraint }}
  {{ aux _ l }}
  | kinded_id 	  	 	       	      :: :: id {{ com optionally kinded identifier }}
  | n_constraint			      :: :: constraint {{ com constraint }}

typquant :: 'TypQ_' ::=
  {{ com type quantifiers and constraints}}
  {{ aux _ l }}
  | forall quant_item1 , ... , quant_itemn . :: :: tq %{{ texlong }}
  |                                          :: ::  no_forall     {{ com empty }}

typschm :: 'TypSchm_' ::=
  {{ com type scheme  }}
  {{ aux _ l }}
  |  typquant typ                            :: :: ts

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Type definitions                                             %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

grammar

opt_abstract_config :: 'TDC_' ::=
  | = config string1 . ... . string2 :: :: key
  |                                  :: :: none

type_def {{ ocaml 'a type_def }} {{ lem type_def 'a }} :: 'TD_' ::=
  {{ ocaml TD_aux of type_def_aux * 'a annot }}
  {{ lem TD_aux of type_def_aux * annot 'a }}
  | type_def_aux  :: :: aux

type_def_aux  :: 'TD_' ::=
  {{ com type definition body }}
  | type id typquant = typ_arg                                        :: :: abbrev
    {{ com type abbreviation }} {{ texlong }}
  | typedef id = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt }     :: :: record
    {{ com struct type definition }} {{ texlong }}
  | typedef id = const union typquant { type_union1 ; ... ; type_unionn semi_opt }   :: :: variant
    {{ com tagged union type definition}} {{ texlong }}
  | typedef id = enumerate { id1 ; ... ; idn semi_opt }   :: :: enum
    {{ com enumeration type definition}} {{ texlong }}
  | typedef id : kind opt_abstract_config :: :: abstract
    {{ com abstract type }}
  | bitfield id : typ = { id1 : index_range1 , ... , idn : index_rangen } :: :: bitfield
    {{ com register mutable bitfield type definition }} {{ texlong }}

type_union :: 'Tu_' ::=
  {{ com type union constructors }}
  {{ aux _ union_annot }}
  | typ id                                              :: :: ty_id

index_range :: 'BF_' ::= {{ com index specification, for bitfields in register types}}
  {{ aux _ l }}
  | nexp :: :: 'single'  {{ com single index }}
  | nexp1 '..' nexp2 :: :: range {{ com index range }}
  | index_range1 , index_range2 :: :: concat {{ com concatenation of index ranges }}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Literals                                                     %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

lit :: 'L_' ::=
  {{ com literal constant }}
  {{ aux _ l }}
  | ( )       :: :: unit
  | bitzero   :: :: zero
  | bitone    :: :: one
  | true      :: :: true
  | false     :: :: false
  | num       :: :: num {{ com natural number constant }}
  | hex       :: :: hex {{ com bit vector constant, C-style }}
  | bin       :: :: bin  {{ com bit vector constant, C-style }}
  | string    :: :: string {{ com string constant }}
  | undefined :: :: undef {{ com undefined-value constant }}
  | real      :: :: real

semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::=         {{ phantom }}
                                                        {{ ocaml bool }}
                                                        {{ lem bool }}
                                                        {{ hol bool }}
							{{ isa bool }}
  {{ com optional semi-colon }}
  |                                                     :: :: no
    {{ hol F }}
    {{ ocaml false }}
    {{ lem false }}
    {{ isa False }}
  | ';'                                                 :: :: yes
    {{ hol T }}
    {{ ocaml true }}
    {{ lem true }}
    {{ isa True }}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Patterns                                                     %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

typ_pat :: 'TP_' ::=
  {{ com type pattern }}
  {{ aux _ l }}
  | _                               :: :: wild
  | kid                             :: :: var
  | id ( typ_pat1 , .. , typ_patn ) :: :: app

field_pat_wildcard :: 'FP_' ::=
  | _ l :: :: wild
  |     :: :: no_wild

struct_name :: 'SN_' ::=
  | id :: :: id
  |    :: :: anon

pat :: 'P_' ::=
  {{ com pattern }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | lit                                      :: :: lit
    {{ com literal constant pattern }}
  | _                                        :: :: wild
    {{ com wildcard }}
  | pat1 | pat2                              :: :: or
    {{ com pattern disjunction }}
  | ~ pat                                    :: :: not
    {{ com pattern negation }}
  | ( pat as id )                            :: :: as
    {{ com named pattern }}
  | ( typ ) pat                              :: :: typ
    {{ com typed pattern }}
  | id                                       :: :: id
    {{ com identifier  }}
  | pat typ_pat                              :: :: var
    {{ com bind pattern to type variable }}
  | id ( pat1 , .. , patn )                  :: :: app
    {{ com union constructor pattern }}
  | [ pat1 , ... , patn  ]                   :: :: vector
    {{ com vector pattern }}
  | pat1 @ ... @ patn                        :: :: vector_concat
    {{ com concatenated vector pattern }}
  | id [ num1 '..' num2 ]                    :: :: vector_subrange
    {{ com vector subrange pattern }}
  | ( pat1 , .... , patn )                   :: :: tuple
    {{ com tuple pattern }}
  | [|| pat1 , .. , patn ||]                 :: :: list
    {{ com list pattern }}
  | ( pat )                                  :: S :: paren
    {{ ichlo [[pat]] }}
  | pat1 '::' pat2                           :: :: cons
    {{ com Cons patterns }}
  | pat1 ^^ ... ^^ patn                      :: :: string_append
    {{ com string append pattern, x ^^ y }}
  | struct struct_name { id1 = pat1 , ... , idn = patn , field_pat_wildcard } :: :: struct
    {{ com struct pattern }}

parsing
P_app <= P_app
P_app <= P_as

grammar

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Expressions                                                  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

loop :: loop ::= {{ phantom }}
  | while :: :: while
  | until :: :: until

internal_loop_measure :: 'Measure_' ::=
  {{ com internal syntax for an optional termination measure for a loop }}
  {{ auxparam 'a }}
  {{ aux _ l }}
  |                               :: :: none
  | 'termination_measure' { exp } :: :: some

exp :: 'E_' ::=
  {{ com expression }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | { exp1 ; ... ; expn }                               :: :: block
    {{ com sequential block }}
  | id                                                  :: :: id
    {{ com identifier }}
  | lit                                                 :: :: lit
    {{ com literal constant }}
  | ( typ ) exp                                         :: :: typ
    {{ com cast }}
  | id ( exp1 , .. , expn )                             :: :: app
    {{ com function application }}
  | exp1 id exp2                                        :: :: app_infix
    {{ com infix function application }}
  | ( exp1 , .... , expn )                              :: :: tuple
    {{ com tuple }}
  | if exp1 then exp2 else exp3                         :: :: if
    {{ com conditional }}
  | loop internal_loop_measure exp1 exp2                    :: :: loop
  | foreach ( id from exp1 to exp2 by exp3 in order ) exp4  :: :: for   {{ com for loop }}

  % vectors
  | [ exp1 , ... , expn ]                             :: :: vector {{ com vector (indexed from 0) }}
  | exp [ exp' ]                                      :: :: vector_access {{ com vector access }}
  | exp [ exp1 '..' exp2 ]                            :: :: vector_subrange {{ com subvector extraction }}
  | [ exp with exp1 = exp2 ]                          :: :: vector_update {{ com vector functional update }}
  | [ exp with exp1 '..' exp2 = exp3 ]                :: :: vector_update_subrange {{ com vector subrange update, with vector}}
  | exp1 @ exp2                                       :: :: vector_append {{ com vector concatenation }}

  % lists
  | [| exp1 , ..  , expn |]                           :: :: list {{ com list }}
  | exp1 '::' exp2                                    :: :: cons {{ com cons }}

  % structs
  | struct struct_name { fexp0 , ... , fexpn }        :: :: struct {{ com struct }}
  | { exp with fexp0 , ... , fexpn }                  :: :: struct_update {{ com functional update of struct }}
  | exp . id                                          :: :: field {{ com field projection from struct  }}

  | match exp { pexp1 , ... , pexpn }                 :: :: match {{ com pattern matching }}

  | letbind in exp                                    :: :: let
    {{ com let expression }}

  | lexp = exp                                        :: :: assign
    {{ com imperative assignment }}

  | sizeof nexp                                       :: :: sizeof
    {{ com the value of $[[nexp]]$ at run time }}

  | return exp                                        :: :: return {{ com  return $[[exp]]$ from current function }}
  | exit exp                                          :: :: exit {{ com halt all current execution }}

  | config string1 . ... . stringn                    :: :: config {{ com model configuration value }}

  | ref id                                            :: :: ref
  | throw exp                                         :: :: throw
  | try exp catch { pexp1 , ... , pexpn }             :: :: try
  | assert ( exp , exp' )                             :: :: assert
    {{ com halt with error message $[[exp']]$ when not $[[exp]]$. exp' is optional. }}
  | ( exp )                                           :: S :: paren {{ ichlo [[exp]] }}
  | var lexp = exp in exp'  :: I :: var {{ com This is an internal node for compilation that demonstrates the scope of a local mutable variable }}
  | let pat = exp in exp'   :: I :: internal_plet {{ com This is an internal node, used to distinguish some introduced lets during processing from original ones }}
  | return_int ( exp )      ::  :: internal_return {{ com For internal use to embed into monad definition }}
  | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }}
  | assume n_constraint in exp :: :: internal_assume {{ com Internal node for additional type checker assumptions }}
  | constraint n_constraint :: :: constraint

lexp :: 'LE_' ::= {{ com lvalue expression }}
    {{ aux _ annot }} {{ auxparam 'a }}
    | id                      :: :: id {{ com identifier }}
    | deref exp               :: :: deref
    | id ( exp1 , .. , expn ) :: :: app {{ com memory or register write via function call }}
    | ( typ ) id	      :: :: typ
    | ( lexp0 , .. , lexpn )  :: :: tuple {{ com multiple (non-memory) assignment }}
    | lexp1 @ ... @ lexpn     :: :: vector_concat {{ com vector concatenation L-exp }}
    | lexp [ exp ]            :: :: vector  {{ com vector element }}
    | lexp [ exp1 '..' exp2 ] :: :: vector_range {{ com subvector }}
    | lexp . id               :: :: field {{ com struct field }}

fexp :: 'FE_' ::=
  {{ com field expression }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | id = exp                  :: :: fexp

opt_default :: 'Def_val_' ::=
  {{ com optional default value for indexed vector expressions }} %, to define a default value for any unspecified positions in a sparse map
  {{ aux _ annot }} {{ auxparam 'a }}
  |                           :: :: empty
  | ; default = exp           :: :: dec

pexp :: 'Pat_' ::=
  {{ com pattern match }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | pat => exp                        :: :: exp
  | pat if exp1 => exp                :: :: when
% apparently could use -> or => for this.

%% % psexp :: 'Pats' ::=
%% %   {{ com Multi-pattern matches }}
%% %   {{ aux _ l }}
%% %   | pat1 ... patn -> exp                                :: :: exp


parsing

%P_app right LB_Let_val

%%P_app <= Fun

%%Fun right App
%%Function right App
E_match right E_app
E_let right E_app

%%Fun <= Field
%%Function <= Field
E_app <= E_field
E_match <= E_field
E_let <= E_field

E_app left E_app

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Function definitions                                         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%% C-ish style %%%%%%%%%%

grammar

tannot_opt :: 'Typ_annot_opt_' ::=
  {{ com optional type annotation for functions}}
  {{ aux _ l }}
  |                                             :: :: none
% Currently not optional; one issue, do the type parameters apply over the argument types, or should this be the type of the function and not just the return
  | typquant typ                                :: :: some

rec_opt :: 'Rec_' ::=
  {{ com optional recursive annotation for functions }}
  {{ auxparam 'a }}
  {{ aux _ l }}
  |                                             :: :: nonrec {{ com non-recursive }}
  | rec                                         :: :: rec {{ com recursive without termination measure }}
  | { pat -> exp }                              :: :: measure {{ com recursive with termination measure }}

% Generate a pexp, but from slightly different syntax (= rather than ->)
pexp_funcl :: 'Pat_funcl_' ::=
  {{ auxparam 'a }}
  {{ ocaml ('a pexp) }}
  {{ isa pexp }}
  {{ lem (pexp 'a) }}
  | pat = exp                       :: :: exp {{ ichlo (Pat_aux (Pat_exp [[pat]] [[exp]],Unknown)) }}
  | ( pat when exp1 ) = exp         :: :: when {{ ichlo (Pat_aux (Pat_when [[pat]] [[exp1]] [[exp]],Unknown)) }}

funcl :: 'FCL_' ::=
  {{ com function clause }}
  {{ aux _ clause_annot }} {{ auxparam 'a }}
  | id pexp_funcl                   :: :: funcl


fundef :: 'FD_' ::=
  {{ com function definition}}
  {{ aux _ annot }} {{ auxparam 'a }}
  | function rec_opt tannot_opt funcl1 and ... and funcln :: :: function {{ texlong }}
% Note that the typ in the tannot_opt is
% the *result* type, not the type of the whole function.  The argument
% type comes from the pattern in the funcl

impldef :: 'Impl_' ::=
  {{ com impl for target }}
  {{ aux _ l }} {{ auxparam 'a }}
  | impl funcl :: :: impl

mpat :: 'MP_' ::=
  {{ com Mapping pattern. Mostly the same as normal patterns but only constructible parts }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | lit                                ::   :: lit
  | id                                 ::   :: id
  | id ( mpat1 , ... , mpatn )         ::   :: app
  | [ mpat1 , ... , mpatn ]            ::   :: vector
  | mpat1 @ ... @ mpatn                ::   :: vector_concat
  | id [ num1 '..' num2 ]              ::   :: vector_subrange
  | ( mpat1 , ... , mpatn )            ::   :: tuple
  | [|| mpat1 , ... , mpatn ||]        ::   :: list
  | ( mpat )                           :: S :: paren {{ ichlo [[mpat]] }}
  | mpat1 '::' mpat2                   ::   :: cons
  | mpat1 ^^ ... ^^ mpatn              ::   :: string_append
  | mpat : typ                         ::   :: typ
  | mpat as id                         ::   :: as
  | struct struct_name { id1 = mpat1 , ... , idn = mpatn } :: :: struct

mpexp :: 'MPat_' ::=
  {{ aux _ annot }} {{ auxparam 'a }}
  | mpat          :: :: pat
  | mpat when exp :: :: when

mapcl :: 'MCL_' ::=
  {{ com mapping clause (bidirectional pattern-match) }}
  {{ aux _ clause_annot }} {{ auxparam 'a }}
  | mpexp1 <-> mpexp2 :: :: bidir
  | forwards pexp     :: :: forwards
  | backwards pexp    :: :: backwards


mapdef :: 'MD_' ::=
  {{ com mapping definition (bidirectional pattern-match function) }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | mapping id tannot_opt = { mapcl1 , ... , mapcln } :: :: mapping {{ texlong }}

letbind :: 'LB_' ::=
  {{ com let binding }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | let pat = exp                                    :: :: val
    {{ com let, implicit type ($[[pat]]$ must be total)}}

subst :: 'IS_' ::=
  {{ aux _ l }}
  {{ com instantiation substitution }}
  | kid = typ_arg :: :: typ
    {{ com instantiate a type variable with a type }}
  | id1 = id2     :: :: id
    {{ com instantiate an identifier with another identifier }}

outcome_spec :: 'OV_' ::=
  {{ com outcome declaration }}
  {{ aux _ l }}
  | outcome id : typschm with typquant :: :: outcome

instantiation_spec :: 'IN_' ::=
  {{ aux _ annot }} {{ auxparam 'a }}
  | id :: :: id

val_spec {{ ocaml 'a val_spec }} {{ lem val_spec 'a }} :: 'VS_' ::=
   {{ ocaml VS_aux of val_spec_aux * 'a annot }}
   {{ lem VS_aux of val_spec_aux * annot 'a }}
  | val_spec_aux ::  :: aux

val_spec_aux :: 'VS_' ::=
  {{ com value type specification }}
  {{ ocaml  VS_val_spec of typschm * id * extern option }}
  {{ lem VS_val_spec of typschm * id * maybe extern }}
  {{ isa  typschm * id  * (string => string option) }}
  | val id : typschm                           :: S :: val_spec
    {{ com specify the type of an upcoming definition }}
    {{ ocaml (VS_val_spec [[typschm]] [[id]] []) }} {{ lem }} {{ isa }}
  | val string : typschm       :: S :: extern_no_rename
    {{ com specify the type of an external function }}
    {{ ocaml  (VS_val_spec [[typschm]] [[string]] [ ( "_" , [[string]] ) ]) }} {{ lem }} {{ isa }}
  | val id = string : typschm      :: S :: extern_rename_all
    {{ com specify the type of an external function }}
    {{ ocaml  (VS_val_spec [[typschm]] [[id]] [ ( "_" , [[string]] ) ]) }} {{ lem }} {{ isa }}
  | val id = { string1 = string'1 , ... , stringn = string'n } : typschm :: S :: extern_rename_some
    {{ ichlo }}

default_spec :: 'DT_' ::=
  {{ com default kinding or typing assumption }}
  {{ aux _ l }}
  | default Order order      :: :: order

scattered_def :: 'SD_' ::=
  {{ com scattered function and union type definitions }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | scattered function id : tannot_opt effect_opt :: :: function
{{ texlong }} {{ com scattered function definition header }}

  | function clause funcl  :: :: funcl
{{ texlong }} {{ com scattered function definition clause }}

  | scattered typedef id = const union typquant :: :: variant
{{ texlong }} {{ com scattered union definition header }}

  | union id member type_union :: :: unioncl
{{ texlong }} {{ com scattered union definition member }}

  | internal_unioncl_record id1 id2 typquant { typ1 id1 , ... , typn idn } :: :: internal_unioncl_record

  | scattered mapping id : tannot_opt :: :: mapping

  | mapping clause id = mapcl :: :: mapcl

  | scattered enum id :: :: enum

  | enum clause id1 = id2 :: :: enumcl

  | end id  :: :: end
{{ texlong }} {{ com scattered definition end }}

opt_exp :: '' ::= {{ phantom }} {{ lem maybe (exp 'a) }} {{ ocaml 'a exp option }} {{ auxparam 'a }}
  | exp                                          :: :: opt_exp_some
  {{ lem (Just [[exp]]) }} {{ ocaml (Some [[exp]]) }}
  |                                              :: :: opt_exp_none
  {{ lem Nothing }} {{ ocaml None }}

dec_spec :: 'DEC_' ::=
  {{ com register declarations }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | register effect effect' typ id = opt_exp :: :: reg

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Top-level definitions                                        %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

prec :: '' ::=
   | infix :: :: Infix
   | infixl :: :: InfixL
   | infixr :: :: InfixR

% The measure expression will remain explicitly untyped until it is moved into the loop itself
loop_measure :: '' ::= {{ lem (loop * exp unit) }}
   {{ auxparam 'a }}
   | loop exp :: :: Loop

pragma :: 'Pragma_' ::=
  {{ com pragma contents }}
  | string l                                                    :: :: line
  | string1 = attribute_data1 , ... , stringn = attribute_datan :: :: structured

def :: 'DEF_' ::=
  {{ com top-level definition }}
  {{ aux _ def_annot }} {{ auxparam 'a 'b }}
  | type_def                                           :: :: type
    {{ com type definition }}
  | constraint n_constraint                            :: :: constraint
    {{ com top-level constraint }}
  | fundef                                             :: :: fundef
    {{ com function definition }}
  | mapdef                                             :: :: mapdef
    {{ com mapping definition }}
  | impl funcl                                         :: :: impl
    {{ com impl definition }}
  | letbind                                            :: :: let
    {{ com value definition }}
  | val_spec                                           :: :: val
    {{ com top-level type constraint }}
  | outcome_spec { def1 ... defn }                     :: :: outcome
    {{ com top-level outcome definition }}
  | instantiation instantiation_spec with subst1 , ... , substn :: :: instantiation
    {{ com instantiation }}
  | fix prec num id                                    :: :: fixity
    {{ com fixity declaration }}
  |  overload id [ id1 ; ... ; idn ]                   :: :: overload
    {{ com operator overload specification }}
  | default_spec                                       :: :: default
    {{ com default kind and type assumptions }}
  | scattered_def                                      :: :: scattered
    {{ com scattered function and type definition }}
  | 'termination_measure' id pat = exp                 :: :: measure
    {{ com separate termination measure declaration }}
  | 'termination_measure' id loop_measure1 , .. , loop_measuren :: :: loop_measures
    {{ com separate termination measure declaration }}
  | dec_spec                                           :: :: register
    {{ com register declaration }}
  | fundef1 .. fundefn                                 :: I :: internal_mutrec
    {{ com internal representation of mutually recursive functions }}
  | $ string pragma                                    :: :: pragma
    {{ com compiler directive }}

terminals :: '' ::=
  | **                                  :: :: starstar
    {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }}
    {{ com \texttt{**} }}
   | >=                                  :: :: geq
    {{ tex \ensuremath{\geq} }}
%     {{ tex \ottsym{\textgreater=} }}
%     {{ com \texttt{>=} }}
   | '<='                                        :: :: leq
    {{ tex \ensuremath{\leq} }}
%     {{ tex \ottsym{\textless=} }}
%     {{ com \texttt{<=} }}
   | ->                                  :: :: arrow
    {{ tex \ensuremath{\rightarrow} }}
   | <->                                 :: :: bidir
    {{ tex \ensuremath{\leftrightarrow} }}

%     {{ tex \ottsym{-\textgreater} }}
%     {{ com \texttt{->} }}
   | ==>                                 :: :: Longrightarrow
     {{ tex \ensuremath{\Longrightarrow} }}
     {{ com \texttt{==>} }}
%   | <|                                  :: :: startrec
%     {{ tex \ensuremath{\langle|} }}
%     {{ com \texttt{<|} }}
%   | |>                                  :: :: endrec
%     {{ tex \ensuremath{|\rangle} }}
%     {{ com \texttt{|>} }}
  | inter                               :: :: inter
    {{ tex \ensuremath{\cap} }}
  | u+                                  :: :: uplus
    {{ tex \ensuremath{\uplus} }}
  | u-                                  :: :: uminus
    {{ tex \ensuremath{\setminus} }}
  | NOTIN                               :: :: notin
    {{ tex \ensuremath{\not\in} }}
  | SUBSET                              :: :: subset
    {{ tex \ensuremath{\subset} }}
  | NOTEQ                               :: :: noteq
    {{ tex \ensuremath{\not=} }}
  | emptyset                            :: :: emptyset
    {{ tex \ensuremath{\emptyset} }}
%   | <                                   :: :: lt
    {{ tex \ensuremath{\langle} }}
%     {{ tex \ottsym{<} }}
%   | >                                   :: :: gt
    {{ tex \ensuremath{\rangle} }}
%    {{ tex \ottsym{>} }}
  | lt                                  :: :: mathlt
    {{ tex < }}
  | gt                                  :: :: mathgt
    {{ tex > }}
  | ~=                                  :: :: alphaeq
    {{ tex \ensuremath{\approx} }}
  | ~< 	   			:: :: consist
    {{ tex \ensuremath{\precapprox} }}
  | |-                                  :: :: vdash
    {{ tex \ensuremath{\vdash} }}
  | |-t					:: :: vdashT
    {{ tex \ensuremath{\vdash_t} }}
  | |-n					:: :: vdashN
    {{ tex \ensuremath{\vdash_n} }}
  | |-e					:: :: vdashE
    {{ tex \ensuremath{\vdash_e} }}
  | |-o					:: :: vdashO
    {{ tex \ensuremath{\vdash_o} }}
  | |-c                                 :: :: vdashC
    {{ tex \ensuremath{\vdash_c} }}
  | '                                   :: :: quote
    {{ tex \ottsym{'} }}
  | |->                                 :: :: mapsto
    {{ tex \ensuremath{\mapsto} }}
  | gives                               :: :: gives
    {{ tex \ensuremath{\triangleright} }}
  | ~>                                  :: :: leadsto
    {{ tex \ensuremath{\leadsto} }}
  | select				:: :: select
   {{ tex \ensuremath{\sigma} }}
  | =>                                  :: :: Rightarrow
    {{ tex \ensuremath{\Rightarrow} }}
  | --                                  :: :: dashdash
    {{ tex \mbox{--} }}
  | effectkw				:: :: effectkw
    {{ tex \ottkw{effect} }}
  | empty                               :: :: empty
    {{ tex \ensuremath{\epsilon} }}
  | consistent_increase                 :: :: ci
    {{ tex \ottkw{consistent\_increase}~ }}
  | consistent_decrease                 :: :: cd
    {{ tex \ottkw{consistent\_decrease}~ }}
  | == :: :: equiv
    {{ tex \equiv }}
%   | [| :: :: range_start
%     {{ tex \mbox{$\ottsym{[\textbar}$} }}
%   | |] :: :: range_end
%     {{ tex \mbox{$\ottsym{\textbar]}$} }}
%   | [|| :: :: list_start
%     {{ tex \mbox{$\ottsym{[\textbar\textbar}$} }}
%   | ||] :: :: list_end
%     {{ tex \mbox{$\ottsym{\textbar\textbar]}$} }}