path: root/language/sail.ott

%
%% 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 }}
  {{ com Numeric literals }}

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

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

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

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

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

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

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

embed
{{ ocaml

open Big_int
open Value

type text = string

type l = Parse_ast.l

type 'a annot = l * 'a

type loop = While | Until

}}

embed
{{ lem

type l = | Unknown

type value = | Val

type loop = While | Until

type annot 'a = l * 'a

}}

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

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

grammar

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 Order 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  }}
  | Order :: :: order {{ com kind of vector order specifications  }}
  | 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 }}
  | 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 }}
  | kid                                 :: :: var {{ com variable }} 
  | inc                                 :: :: inc {{ com increasing }}
  | dec                                 :: :: dec {{ com decreasing }}
  | ( order )                           :: S :: paren {{ ichlo [[order]] }}

base_effect :: 'BE_' ::=
  {{ com effect }}
  {{ aux _ l }}
  | rreg                                :: :: rreg {{ com read register }}
  | wreg                                :: :: wreg {{ com write register }}
  | rmem                                :: :: rmem {{ com read memory }}
  | rmemt                               :: :: rmemt {{ com read memory and tag }}
  | wmem                                :: :: wmem {{ com write memory }}
  | wmea                                :: :: eamem {{ com signal effective address for writing memory }}
  | exmem                               :: :: exmem {{ com determine if a store-exclusive (ARM) is going to succeed }}
  | wmv                                 :: :: wmv {{ com write memory, sending only value }}
  | wmvt                                :: :: wmvt {{ com write memory, sending only value and tag }}
  | barr                                :: :: barr {{ com memory barrier }}
  | depend                              :: :: depend {{ com dynamic footprint }}
  | undef                               :: :: undef {{ com undefined-instruction exception }}
  | unspec                              :: :: unspec {{ com unspecified values }}
  | nondet                              :: :: nondet {{ com nondeterminism, from $[[nondet]]$ }}
  | escape                              :: :: escape {{ com potential exception }}
  | config                              :: :: config {{ com configuration option }}

effect :: 'Effect_' ::=
  {{ aux _ l }}
  | { base_effect1 , .. , base_effectn } :: :: set {{ com effect set }}
  | pure                                 :: M :: pure {{ com sugar for empty effect set }}
    {{ lem (Effect_set []) }}

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 effectkw effect :: :: fn {{ com Function (first-order only) }}
  | typ1 <-> typ2                                 :: :: bidir {{ com Mapping }}
  | ( typ1 , .... , typn )                        :: :: tup {{ 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
  | order        :: :: order
  | n_constraint :: :: bool

n_constraint :: 'NC_' ::=
  {{ com constraint over kind Int }}
  {{ aux _ l }}
  | nexp == nexp'                    :: :: equal
  | nexp >= nexp'                    :: :: bounded_ge
  | nexp '<=' nexp'                  :: :: bounded_le
  | nexp != nexp'                    :: :: not_equal
  | kid 'IN' { num1 , ... , numn }   :: :: set
  | n_constraint & n_constraint'     :: :: or
  | n_constraint | n_constraint'     :: :: and
  | id ( typ_arg0 , ... , typ_argn ) :: :: app
  | 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 [[kinded_id]] }}

quant_item :: 'QI_' ::=
  {{ com kinded identifier or Int constraint }}
  {{ aux _ l }}
  | kinded_id 	  	 	       	      :: :: id {{ com optionally kinded identifier }}
  | n_constraint			      :: :: const {{ com Int 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

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 }}
  | 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 _ l }}
  | 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 }}
  {{ com optional semi-colon }}
  |                                                     :: :: no
    {{ hol F }}
    {{ ocaml false }}
    {{ lem false }}
  | ';'                                                 :: :: yes
    {{ hol T }}
    {{ ocaml true }}
    {{ lem true }}

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

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

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 }}

% OR?  do we invent something ghastly including a union keyword?  Perhaps not...

%  | <| fpat1 ; ... ; fpatn semi_opt |>                  :: :: record
%    {{ com Record patterns }}
% OR
  | { fpat1 ; ... ; fpatn semi_opt }                  :: :: record
    {{ com struct pattern }}

%Patterns for vectors
%Should these be the same since vector syntax has changed, and lists have also changed?

  | [ pat1 , .. , patn  ]                     :: :: vector
   {{ com vector pattern }}

%  | [ num1 = pat1 , .. , numn = patn ]                     :: :: vector_indexed
%   {{ com vector pattern (with explicit indices) }}

% cf ntoes for this
  |  pat1 : .... : patn                                   :: :: vector_concat
  {{ com concatenated vector pattern }}

  | ( pat1 , .... , patn )                              :: :: tup
    {{ 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 }}

% XXX Is this still useful?
fpat :: 'FP_' ::=
  {{ com field pattern }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | id = pat                                            :: :: Fpat

mfpat  :: 'MFP_' ::=
  {{ com Mapping field pattern, why does this have to exist }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | id = mpat                                           :: :: mpat

parsing
P_app <= P_app
P_app <= P_as

grammar

% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% % Interpreter specific things                                  %
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }}
%   | x                                            ::  :: optx_x
%   {{ lem (Just [[x]]) }} {{ ocaml (Some [[x]]) }}
%   |                                              :: :: optx_none
%   {{ lem Nothing }} {{ ocaml None }}

% tag :: 'Tag_' ::=
% {{ com Data indicating where the identifier arises and thus information necessary in compilation }}
%    | None                                 :: :: empty
%    | Intro                                :: :: intro {{ com Denotes an assignment and lexp that introduces a binding }}
%    | Set                                  :: :: set {{ com Denotes an expression that mutates a local variable }}
%    | Tuple                                :: :: tuple_assign {{ com Denotes an assignment with a tuple lexp }}
%    | Global				  :: :: global {{ com Globally let-bound or enumeration based value/variable }}
%    | Ctor                                 :: :: ctor {{ com Data constructor from a type union }}
%    | Extern optx                          :: :: extern {{ com External function, specied only with a val statement }}
%    | Default                              :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }}
%    | Spec				  :: :: spec
%    | Enum num				  :: :: enum
%    | Alias				  :: :: alias
%    | Unknown_path optx			  :: :: unknown {{ com Tag to distinguish an unknown path from a non-analysis non deterministic path}}

% embed
% {{ lem

% type tannot = maybe (typ * tag * list unit * effect * effect)

% }}

% embed
% {{ ocaml

% (* Interpreter specific things are just set to unit here *)
% type tannot = unit

% type reg_form_set = unit

% }}

% grammar
% tannot :: '' ::=
%   {{ phantom }}
%   {{ ocaml unit }}
%   {{ lem tannot }}

% i_direction :: 'I' ::=
%   | IInc :: :: Inc
%   | IDec :: :: Dec

% ctor_kind :: 'C_' ::=
%   | C_Enum nat :: :: Enum
%   | C_Union    :: :: Union

% reg_form :: 'Form_' ::=
%   | Reg id tannot i_direction :: :: Reg
%   | SubReg id reg_form index_range :: :: SubReg

% reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }}

% alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }}

% value :: 'V_' ::= {{ com interpreter evaluated value }}
%   | Boxref nat typ                                                                  :: :: boxref
%   | Lit lit                                                                         :: :: lit
%   | Tuple ( value1 , ... , valuen )                                                 :: :: tuple
%   | List ( value1 , ... , valuen )                                                  :: :: list
%   | Vector nat i_direction ( value1 , ... , valuen )                                :: :: vector
%   | Vector_sparse nat' nat'' i_direction ( nat1 value1 , ... , natn valuen ) value' :: :: vector_sparse
%   | Record typ ( id1 value1 , ... , idn valuen )                                    :: :: record
%   | V_ctor id typ ctor_kind value1                                                  :: :: ctor
%   | Unknown                                                                         :: :: unknown
%   | Register reg_form                                                               :: :: register
%   | Register_alias alias_spec_tannot tannot                                         :: :: register_alias
%   | Track value reg_form_set                                                        :: :: track

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 }}
% maybe we really should have indentation-sensitive syntax :-)  (given that some of the targets do)

  | nondet { exp1 ; ... ; expn }                        :: :: nondet {{ com nondeterministic block }}

  | id                                                  :: :: id
    {{ com identifier }}

  | lit                                                 :: :: lit
    {{ com literal constant }}

  | ( typ ) exp                                         :: :: cast
    {{ com cast }}

  | id ( exp1 , .. , expn )                                   :: :: app
    {{ com function application }}
  | id exp                                               :: S :: tup_app {{ ichlo [[id ( exp ) ]] }} 
   {{ com funtion application to tuple }}

% Note: fully applied function application only

  | exp1 id exp2                                        :: :: app_infix
    {{ com infix function application }}
 
  | ( exp1 , .... , expn )                              :: :: tuple
    {{ com tuple }}

  | if exp1 then exp2 else exp3                         :: :: if
    {{ com conditional }}

  | if exp1 then exp2                                   :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }}
  | loop internal_loop_measure exp1 exp2                    :: :: loop
  | while internal_loop_measure exp1 do exp2                :: S :: while {{ ichlo [[ loop internal_loop_measure while exp1 exp2 ]] }}
  | repeat internal_loop_measure exp1 until exp2            :: S :: until {{ ichlo [[ loop internal_loop_measure until exp2 exp1 ]] }}
  | foreach ( id from exp1 to exp2 by exp3 in order ) exp4  ::   :: for   {{ com loop }}

% vectors
  | [ exp1 , ... , expn ]                             :: :: vector {{ com vector (indexed from 0) }}
% order comes from global command-line option???
% here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn 
% the expi and the result are both of type vector of 'a 

% we pick [ ] not { } for vector literals for consistency with their
% array-like access syntax, in contrast to the C which has funny
% syntax for array literals.  We don't have to preserve [ ] for lists
% as we don't expect to use lists very much. 

  | exp [ exp' ]                                      :: :: vector_access
  {{ com vector access }}

  | exp [ exp1 '..' exp2 ]                               :: :: vector_subrange
  {{ com subvector extraction }}
  % do we want to allow a comma-separated list of such thingies?  

  | [ exp with exp1 = exp2 ]                          :: :: vector_update 
  {{ com vector functional update }}

  | [ exp with exp1 : exp2 = exp3 ]                   :: :: vector_update_subrange
  {{ com vector subrange update, with vector}}
  % do we want a functional update form with a comma-separated list of such?

  | exp : exp2                                        :: :: vector_append
  {{ com vector concatenation }}

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


% const unions

% const structs

% TODO

  | { fexp0 , ... , fexpn }                    :: :: record
    {{ com struct }}
  | { exp with fexp0 , ... , fexpn }           :: :: record_update
    {{ com functional update of struct }}
  | exp . id                                   :: :: field
    {{ com field projection from struct  }}

%Expressions for creating and accessing vectors



%  map : forall 'x 'y ''N.  ('x -> 'y) -> vector ''N 'x -> vector ''N 'y
%  zip : forall 'x 'y ''N.  vector ''N 'x  -> vector ''N 'y -> vector ''N ('x*'y) 
%  foldl : forall 'x 'y ''N. ('x 'y -> 'y) -> vector ''N 'x -> 'y -> 'y
% foldr : forall 'x 'y ''N. ('x 'y -> 'y) -> 'y -> vector ''N 'x -> 'y
% foldmap : forall 'x 'y 'z ''N. ((x,y) -> (x,z)) -> x -> vector ''N y -> vector ''N z
%(or unzip)

%  and maybe with nice syntax

  | switch exp { case pexp1  ... case pexpn } :: :: case
    {{ com pattern matching }}
%  | ( typ ) exp                                      :: :: Typed
%    {{ com Type-annotated expressions }}
  | 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 }}
% this can be used to break out of for loops
  | exit exp						:: :: exit
    {{ com halt all current execution }}
  | ref id                                     :: :: ref
  | throw exp                                  :: :: throw
  | try exp catch pexp1 .. pexpn             :: :: try
%, potentially calling a system, trap, or interrupt handler with exp
  | assert ( exp , exp' )                            :: :: assert
    {{ com halt with error $[[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 distinguised 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 }}
  | constraint n_constraint :: :: constraint

lexp :: 'LEXP_' ::= {{ com lvalue expression }}
    {{ aux _ annot }} {{ auxparam 'a }}
    | id                      :: :: id {{ com identifier }}
    | deref exp               :: :: deref
    | id ( exp1 , .. , expn ) :: :: memory {{ com memory or register write via function call }}
    | ( typ ) id	      :: :: cast
    | ( lexp0 , .. , lexpn )  :: :: tup {{ 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 when 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_case right E_app
E_let right E_app

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

E_app left E_app


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

%%%% old Lem style %%%%%%
grammar
%% % lem_tannot_opt_aux :: 'LEM_Typ_annot_' ::=
%% %   {{ com Optional type annotations }}
%% %   |                                                     :: :: none
%% %   | : typ                                               :: :: some 
%% % 
%% % lem_tannot_opt {{ tex \ottnt{tannot}^? }} :: 'LEM_Typ_annot_' ::=
%% %   {{ com location-annotated optional type annotations }}
%% %   | tannot_opt_aux l                                    :: :: aux
%% % 
%% % lem_funcl :: 'LEM_FCL' ::=
%% %   {{ com Function clauses }}
%% %   {{ aux _ l }}
%% %   | id pat1 ... patn tannot_opt = exp                   :: :: Funcl
%% % 
%% % lem_letbind :: 'LEM_LB_' ::=
%% %   {{ com Let bindings }}
%% %   {{ aux _ l }}
%% %   | pat tannot_opt = exp                                :: :: Let_val
%% %     {{ com Value bindings }}
%% %   | lem_funcl                                           :: :: Let_fun
%% %     {{ com Function bindings }}
%% % 
%% % 
%% % grammar
%% % lem_val_def :: 'LEM_VD' ::= 
%% %   {{ com Value definitions }}
%% %   {{ aux _ l }}
%% %   | let lem_letbind                                     :: :: Let_def
%% %     {{ com Non-recursive value definitions }}
%% %   | let rec  lem_funcl1 and ... and lem_funcln          :: :: Let_rec
%% %     {{ com Recursive function definitions }}
%% % 
%% % lem_val_spec :: 'LEM_VS' ::=
%% %   {{ com Value type specifications }} 
%% %   {{ aux _ l }}
%% %   | val x_l : typschm                                           :: :: Val_spec

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

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 }}

effect_opt :: 'Effect_opt_' ::=
  {{ com optional effect annotation for functions }}
  {{ aux _ l }}
  |                                              :: :: none {{ com no effect annotation }}
  | effectkw effect                              :: :: effect

% Generate a pexp, but from slightly different syntax (= rather than ->)
pexp_funcl :: 'Pat_funcl_' ::=
  {{ auxparam 'a }}
  {{ icho ('a 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 _ annot }} {{ auxparam 'a }}
  | id pexp_funcl                   :: :: Funcl


fundef :: 'FD_' ::=
  {{ com function definition}}
  {{ aux _ annot }} {{ auxparam 'a }}
  | function rec_opt tannot_opt effect_opt funcl1 and ... and funcln :: :: function {{ texlong }}  
% {{ com function definition }}
% TODO 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
% TODO the above is ok for single functions, but not for mutually
%  recursive functions - the tannot_opt scopes over all the funcli,
%  which is ok for the typ_quant part but not for the typ part

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
  | { mfpat1 ; ... ; mfpatn semi_opt } ::   :: record
  | [ mpat1 , ... , mpatn ]            ::   :: vector
  | mpat1 @ ... @ mpatn                ::   :: vector_concat
  | ( mpat1 , ... , mpatn )            ::   :: tup
  | [|| mpat1 , ... , mpatn ||]        ::   :: list
  | ( mpat )                           :: S :: paren {{ ichlo [[mpat]] }}
  | mpat1 '::' mpat2                   ::   :: cons
  | mpat1 ^^ ... ^^ mpatn              ::   :: string_append
  | mpat : typ                         ::   :: typ
  | mpat as id                         ::   :: as

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

mapcl :: 'MCL_' ::=
  {{ com mapping clause (bidirectional pattern-match) }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | mpexp1 <-> mpexp2 :: :: bidir
  | mpexp   => exp    :: :: forwards
  | mpexp  <-  exp     :: :: 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)}}

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 * (string -> string option) * bool }}
  {{ lem VS_val_spec of typschm * id * (string -> maybe string) * bool }}
  | val typschm id                                  :: S :: val_spec
    {{ com specify the type of an upcoming definition }}
    {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} {{ lem }}
  | val cast typschm id                             :: S :: cast
    {{ ocaml  (VS_val_spec [[typschm]] [[id]] None true) }} {{ lem }}
  | val extern typschm id                           :: S :: extern_no_rename
    {{ com specify the type of an external function }}
    {{ ocaml  (VS_val_spec [[typschm]] [[id]] ([[Some id]]) false) }} {{ lem }}
  | val extern typschm id = string                  :: S :: extern_spec
    {{ com specify the type of a function from Lem }}
    {{ ocaml  (VS_val_spec [[typschm]] [[id]] ([[Some string]]) false) }} {{ lem }}
%where the string must provide an explicit path to the required function but will not be checked

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 rec_opt tannot_opt effect_opt id   :: :: 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 }}

  | scattered mapping id : tannot_opt :: :: mapping

  | mapping clause id = mapcl :: :: mapcl

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

reg_id :: 'RI_' ::=
  {{ aux _ annot }} {{ auxparam 'a }}
  | id								:: :: id

alias_spec :: 'AL_' ::=
  {{ com register alias expression forms }}
%. Other than where noted, each id must refer to an unaliased register of type vector
  {{ aux _ annot }} {{ auxparam 'a }}
  | reg_id . id							:: :: subreg
  | reg_id [ exp ] 						:: :: bit
  | reg_id [ exp '..' exp' ]					:: :: slice
  | reg_id : reg_id'  	    					:: :: concat

dec_spec :: 'DEC_' ::=
  {{ com register declarations }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | register effect effect' typ id                              :: :: reg
  | register configuration id : typ = exp                       :: :: config
  | register alias id = alias_spec				:: :: alias
  | register alias typ id = alias_spec				:: :: typ_alias

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

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

loop_measure :: '' ::=
   {{ auxparam 'a }}
   | loop exp :: :: Loop

def :: 'DEF_' ::=
  {{ com top-level definition }}
  {{ auxparam 'a }}
  | type_def                                           :: :: type
    {{ com type definition }}
  | fundef                                             :: :: fundef
    {{ com function definition }}
  | mapdef                                             :: :: mapdef
    {{ com mapping definition }}
  | letbind                                            :: :: val
    {{ com value definition }}
  | val_spec                                           :: :: spec
    {{ com top-level type constraint }}
  | 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                                           :: :: reg_dec
    {{ com register declaration }}
  | fundef1 .. fundefn                                 :: I :: internal_mutrec
    {{ com internal representation of mutually recursive functions }}
  | $ string1 string2 l                                :: :: pragma
    {{ com compiler directive }}

defs :: '' ::=
  {{ com definition sequence }}
  {{ auxparam 'a }}
  | def1  .. defn                 :: :: Defs



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]}$} }}