path: root/language/l2.ott

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

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

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

embed
{{ ocaml

type text = string

type l = Parse_ast.l

type 'a annot = l * 'a

}}

embed
{{ lem
open import Map
open import Maybe
open import Set_extra

type l =
  | Unknown
  | Int of string * maybe l (*Internally generated*)
  | Range of string * nat * nat * nat * nat

type annot 'a = l * 'a

val duplicates : forall 'a. list 'a -> list 'a

val set_from_list : forall 'a. list 'a -> set 'a

val subst : forall 'a. list 'a -> list 'a -> bool

}}

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 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
  | ( deinfix x )                       :: :: deIid {{ com remove infix status }}
  | bool      		   	 :: M :: bool {{ com Built in type identifiers }} {{ ichlo (Id "bool") }}
  | bit				 :: M :: bit {{ ichlo (Id "bit") }} 
  | unit			 :: M :: unit {{ ichlo (Id "unit") }}
  | nat				 :: M :: nat  {{ ichlo (Id "nat") }}
  | string                       :: M :: string {{ tex \ottkw{string} }} {{ ichlo (Id "string") }}
  | range                        :: M :: range {{ ichlo (Id "range") }}
  | atom			 :: M :: atom {{ ichlo (Id "atom") }}
  | vector			 :: M :: vector {{ ichlo (Id "vector") }}
  | list			 :: M :: list {{ ichlo (Id "list") }}
  | set                          :: M :: set {{ ichlo (Id "set") }}
  | reg                          :: M :: reg {{ ichlo (Id "reg") }}
  | to_num			 :: M :: tonum {{ com Built in function identifiers }} {{ ichlo (Id "to_num") }}
  | to_vec			 :: M :: tovec {{ ichlo (Id "to_vec") }}
% Note: we have just a single namespace. We don't want the same
% identifier to be reused as a type name or variable, expression
% variable, and field name.  We don't enforce any lexical convention
% on type variables (or variables of other kinds)
% We don't enforce a lexical convention on infix operators, as some of the 
% targets use alphabetical infix operators. 

kid :: '' ::=
  {{ com variables with kind, ticked to differntiate from program variables }}
  {{ aux _ l }}
  | ' x                       :: :: var
 

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


grammar

base_kind :: 'BK_' ::=  
  {{ com base kind}}
  {{ aux _ l }}
  | Type                                       :: :: type    {{ com kind of types  }} 
  | Nat                                        :: :: nat     {{ com kind of natural number size expressions  }} 
  | Order                                     :: :: order  {{ com kind of vector order specifications  }} 
  | Effect                                    :: :: effect {{ com kind of effect sets  }} 

kind :: 'K_' ::=  
  {{ com kinds}}
  {{ aux _ l }}
  | base_kind1 -> ... -> base_kindn            :: :: kind 
% we'll never use  ...-> Nat , .. Order , .. or Effects
    
nexp :: 'Nexp_' ::=  
  {{ com expression of kind Nat, for vector sizes and origins }}
  {{ aux _ l }}
  | kid                                 :: :: var         {{ com variable }}
  | num                                 :: :: constant     {{ com constant }}
  | nexp1 * nexp2                       :: :: times        {{ com product }}
  | nexp1 + nexp2                       :: :: sum          {{ com sum }}
  | 2** nexp                            :: :: exp         {{ com exponential }}
  | neg nexp				:: :: neg	  {{ com For internal use. Not M as a dataconstructor is required }}
  | ( nexp )                            :: S :: paren  {{ ichlo [[nexp]] }}

order :: 'Ord_' ::=  
  {{ com vector order specifications, of kind Order}}
  {{ aux _ l }} 
  | kid                                 :: :: var {{ com variable }} 
  | inc                                 :: :: inc  {{ com increasing (little-endian) }}
  | dec                                 :: :: dec  {{ com decreasing (big-endian) }}
  | ( 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 }}
  | wmem                                :: :: wmem {{ com write memory }}
  | barr                                :: :: barr {{ com memory barrier }}
  | undef                               :: :: undef {{ com undefined-instruction exception }}
  | unspec                              :: :: unspec {{ com unspecified values }}
  | nondet                              :: :: nondet {{ com nondeterminism from intra-instruction parallelism }}


effect :: 'Effect_' ::=
  {{ com effect set, of kind Effects }}
  {{ aux _ l }}
 | kid                                 :: :: var
 | { base_effect1 , .. , base_effectn }           :: :: set {{ com effect set }}
 | pure                                 :: M :: pure {{ com sugar for empty effect set }} 
   {{ lem (Effect_set [])  }} {{icho [[{}]] }}
 | effect1 u+ .. u+ effectn                   :: M :: union {{ com meta operation for combining sets of effects }} {{ icho [] }}
   {{ lem (List.foldr effect_union (Effect_aux (Effect_set []) Unknown) [[effect1..effectn]]) }}

embed
{{ lem
let effect_union e1 e2 = 
  match (e1,e2) with
  | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l
  end
}}

grammar

% TODO: are we going to need any effect polymorphism?  Conceivably for built-in maps and folds.  Yes.  But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. 

typ :: 'Typ_' ::=
  {{ com Type expressions, of kind $[[Type]]$ }}
  {{ aux _ l }}
  | _                                           :: :: wild
    {{ com Unspecified type }}
  | id                                         :: :: id
    {{ com Defined type }}
  | kid                                         :: :: var
    {{ com Type variable }}
  | typ1 -> typ2 effectkw effect                        :: :: fn
    {{ com Function type (first-order only in user code) }}
% TODO: build first-order restriction into AST or just into type rules? neither - see note
% TODO: concrete syntax for effects in a function type?  needed only for pp, not in user syntax.
  | ( typ1 , .... , typn )                          :: :: tup
    {{ com Tuple type }}
% TODO union in the other kind grammars?  or make a syntax of argument? or glom together the grammars and leave o the typechecker
  | id < typ_arg1 , .. , typ_argn >                    :: :: app
  {{ com type constructor application }}
  | ( typ )                            :: S :: paren {{ ichlo [[typ]] }} 
%  | range < nexp1, nexp2> :: :: range  {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1 }}
  | [| nexp |]             :: S :: range1 {{ichlo range <[[nexp]], 0> }} {{ com sugar for \texttt{range<0, nexp>} }}
  | [| nexp : nexp' |]  :: S :: range2 {{ichlo range <[[nexp]],[[nexp']]> }} {{ com sugar for \texttt{range< nexp, nexp'>} }}
% | atom < nexp > :: :: atom {{ com equivalent to range<nexp,nexp> }}
  | [: nexp :]            :: S :: atom1 {{ichlo atom <[[nexp]]> }} {{ com sugar for \texttt{atom<nexp>} which is special case of \texttt{range<nexp,nexp>} }}
% use .. not - to avoid ambiguity with nexp -
% total maps and vectors indexed by finite subranges of nat
%  | vector nexp1 nexp2 order typ :: :: vector {{ com vector of [[typ]], indexed by natural range }}
% probably some sugar for vector types, using [ ] similarly to enums:
% (but with .. not : in the former, to avoid confusion...)
  | typ [ nexp ]  :: S :: vector2 {{ichlo vector < [[nexp]],0,inc,[[typ]] > }} {{ com sugar for vector indexed by [ [[nexp]] ] }}
  | typ [ nexp : nexp' ] :: S :: vector3 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} {{ com sugar for vector indexed by [ [[nexp]]..[[nexp']] ] }}
  | typ [ nexp <: nexp' ] :: S :: vector4 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} {{ com sugar for increasing vector indexed as above }}
  | typ [ nexp :> nexp' ] :: S :: vector5 {{ ichlo vector < [[nexp]],[[nexp']],dec,[[typ]] }} {{ com sugar for decreasing vector indexed as above }}
% ...so bit [ nexp ] etc is just an instance of that
%  | List < typ > :: :: list {{ com list of [[typ]] }}
%  | Set < typ >  :: :: set  {{ com finite set of [[typ]] }}
%  | Reg < typ > :: :: reg  {{ com mutable register components holding [[typ]] }}
% "reg t" is basically the ML "t ref" 
% not sure how first-class it should be, though
% use "reg word32" etc for the types of vanilla registers 


typ_arg :: 'Typ_arg_' ::=
  {{ com Type constructor arguments of all kinds }}
  {{ aux _ l }} 
  | nexp       :: :: nexp
  | typ        :: :: typ
  | order     :: :: order
  | effect    :: :: effect

% plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations   ... ref typ

%typ_lib :: 'Typ_lib_' ::=
%  {{ com library types and syntactic sugar for them }}
%  {{ aux _ l }} {{ auxparam 'a }}
% boring base types:
%%  | unit :: :: unit {{ com unit type with value $()$ }}
%  | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }}
%  | bit :: :: bit  {{ com pure bit values (not mutable bits) }}
% experimentally trying with two distinct types of bool and bit ...
%  | nat :: :: nat {{ com natural numbers 0,1,2,... }}
%  | string :: :: string {{ com UTF8 strings }}
% finite subranges of nat

parsing

Typ_tup <= Typ_tup
Typ_fn right Typ_fn
Typ_fn <= Typ_tup
%Typ_fn right Typ_app1
%Typ_tup right Typ_app1

grammar

n_constraint :: 'NC_' ::=
  {{ com constraint over kind $[[Nat]]$ }}
  {{ aux _ l }}
  | nexp = nexp'                                :: :: fixed
  | nexp >= nexp'                               :: :: bounded_ge
  | nexp '<=' nexp'                             :: :: bounded_le
  | kid 'IN' { num1 , ... , numn }               :: :: nat_set_bounded

% Note only id on the left and constants on the right in a
% finite-set-bound, as we don't think we need anything more

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

quant_item :: 'QI_' ::=
  {{ com Either a kinded identifier or a nexp constraint for a typquant }}
  {{ aux _ l }}
  | kinded_id 	  	 	       	      :: :: id {{ com An optionally kinded identifier }}
  | n_constraint			              :: :: const {{ com A constraint for this type }}

typquant :: 'TypQ_' ::= 
  {{ com type quantifiers and constraints}}
  {{ aux _ l }}
  | forall quant_item1 , ... , quant_itemn . :: :: tq {{ texlong }}
% WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE
  |                           ::  ::  no_forall     {{ com sugar, omitting quantifier and constraints }}

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



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

grammar
%ctor_def :: 'CT_' ::=
%  {{ com Datatype constructor definition clause }}
%  {{ aux _ annot }} {{ auxparam 'a }}
%  | id : typschm                                       :: :: ct
% but we could get away with disallowing constraints in typschm, we
% think - if it's useful to do that

%enum_opt :: 'EnumOpt_' ::=
%  |      :: :: empty
%  | enum :: :: enum

%% tdefbody :: 'TD_' ::=
%%   {{ com Type definition bodies }}
%%   | typschm                                                     :: :: abbrev
%%     {{ com Type abbreviations }}
%%   | typquant <| id1 : typ1 ; ... ; idn : typn semi_opt |>     :: :: record
%%     {{ com Record types }}
%%   | enumeration_flag_opt '|' ctor_def1 '|' ... '|' ctor_defn            :: :: variant
%%     {{ com Variant types }}
%% 
 name_scm_opt :: 'Name_sect_' ::=
   {{ com Optional variable-naming-scheme specification for variables of defined type }} 
   {{ aux _ l }}
   |                                                   :: :: none
   | [ name = regexp ]                                 :: :: some
%% 
%% type_def :: '' ::=
%%   {{ com Type definitions }}
%%   | type id : kind naming_scheme_opt = tdefbody                                :: :: Td
%% %  | enumeration id naming_scheme_opt = tdefbody                               ::   :: Td2
%% % the enumeration is sugar for something that uses an enum flag, where the type system will restrict the tdefbody to be a simple enum...
%% 

% TODO: do we need mutually recursive type definitions?  


%%% OR, IN C STYLE

type_def :: 'TD_' ::=
  {{ com Type definition body }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | typedef id name_scm_opt = typschm                                        :: :: abbrev
    {{ com type abbreviation }} {{ texlong }}
  | typedef id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt }     :: :: record
    {{ com struct type definition }} {{ texlong }}
% for specifying constructor result types of nat-indexed GADTs, we can
%  let the typi be function types (as constructors are not allowed to
%  take parameters of function types)
% concrete syntax: to be even closer to C, could have a postfix id rather than prefix id = 
  | typedef id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt }   :: :: variant
    {{ com union type definition}} {{ texlong }}

  | typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt }   :: :: enum
    {{ com enumeration type definition}} {{ texlong }}

  | typedef  id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } 
:: :: register {{ com register mutable bitfield type definition }} {{ texlong }}

% also sugar [  nexp ] 

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

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

% 



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


grammar

lit :: 'L_' ::=
  {{ com Literal constant }}
  {{ aux _ l }}
  | ( )                                                 :: :: unit  {{ com $() : [[unit]]$ }}
%Presumably we want to remove bitzero and bitone ?
  | bitzero                                             :: :: zero {{ com $[[bitzero]] : [[bit]]$ }}
  | bitone                                              :: :: one {{ com $[[bitone]] : [[bit]]$ }}
  | true                                                :: :: true  {{ com $[[true]] : [[bool]]$ }}
  | false                                               :: :: false {{ com $[[false]] : [[bool]]$ }}
  | num                                         :: :: num  {{ com natural number constant }}
  | hex                                         :: :: hex  {{ com bit vector constant, C-style }}
  {{ com hex and bin are constant bit vectors, C-style }}
  | bin                                         :: :: bin  {{ com bit vector constant, C-style }}
% Should undefined be of type bit[alpha] or alpha[beta] or just alpha?
  | undefined					:: :: undef {{ com constant representing undefined values }}
  | string                                              :: :: string {{ com string constant }}

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


pat :: 'P_' ::= 
  {{ com Pattern }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | lit                                                 :: :: lit
    {{ com literal constant pattern }}
  | _                                                   :: :: wild  
    {{ com wildcard }}
  | ( pat as id )                                      :: :: as
    {{ com named pattern }}
% ML-style
%  | ( pat : typ )                                       :: :: typ
%    {{ com Typed patterns }}
% C-style
  | ( typ ) pat                                       :: :: typ
    {{ com typed pattern }}

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

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

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

parsing
P_app <= P_app
P_app <= P_as

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



grammar

exp :: 'E_' ::=
  {{ com Expression }}
  {{ aux _ annot }} {{ auxparam 'a }}  

  | { exp1 ; ... ; expn }                               :: :: block {{ com block }}
% maybe we really should have indentation-sensitive syntax :-)  (given that some of the targets do)

  | nondet { exp1 ; ... ; expn }                        :: :: nondet {{ com nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently}}

  | 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 No extra parens needed when exp is a 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 ( ) ]] }}

  | foreach ( id from exp1 to exp2 by exp3 in order ) exp4  ::   :: for {{ com loop }}
  | foreach ( id from exp1 to exp2 by exp3 ) exp4           :: S :: forup {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in inc exp4 ]] }}
  | foreach ( id from exp1 to exp2 ) exp3                   :: S :: forupbyone  {{ ichlo [[ foreach id from exp1 to exp2 by 1 in inc exp4 ]] }}
  | foreach ( id from exp1 downto exp2 by exp3 ) exp4       :: S :: fordown {{ ichlo [[ foreach id from exp1 to exp2 by exp3 in dec exp4 ]] }}
  | foreach ( id from exp1 downto exp2 ) exp3               :: S :: fordownbyone  {{ ichlo [[ foreach id from exp1 downto exp2 by 1 in dec exp4 ]] }}

% 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 

  | [ num1 = exp1 , ... , numn = expn opt_default ]               :: :: vector_indexed {{ com vector (indexed consecutively) }}
% num1 .. numn must be a consecutive list of naturals

% 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

  | { fexps }                                         :: :: record
    {{ com struct }}
  | { exp with fexps }                                :: :: 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 }}

  | exit exp						:: :: exit
    {{ com expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp }}

  | ( exp )                                             :: S :: paren {{ ichlo [[exp]] }}
  | ( annot ) exp                                   :: :: internal_cast {{ com This is an internal cast, generated during type checking that will resolve into a syntactic cast after }}
  | annot                       :: :: internal_exp {{ com This is an internal use for passing nexp information  to library functions, postponed for constraint solving }}
  | annot , annot'           :: :: internal_exp_user {{ com This is like the above but the user has specified an implicit parameter for the current function }} 
 


lexp :: 'LEXP_' ::= {{ com lvalue expression }}
    {{ aux _ annot }} {{ auxparam 'a }}
    | id                                                  :: :: id
    {{ com identifier }}
    | id ( exp1 , .. , expn )				  :: :: memory {{ com memory write via function call }}
    | id exp	       	    				  :: S :: mem_tup {{ ichlo [[id (exp)]] }}
    | ( typ ) id					  :: :: cast
    | lexp [ exp ]  :: ::                                 vector  {{ com vector element }}
    | lexp [ exp1 '..' exp2 ]  :: ::                         vector_range {{ com subvector }}
    % maybe comma-sep such lists too
    | lexp . id :: :: field                        {{ com struct field }}


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

fexps :: 'FES_' ::=
  {{ com Field-expression list }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | fexp1 ; ... ; fexpn semi_opt                        :: :: Fexps

opt_default :: 'Def_val_' ::=
  {{ com Optional default value for indexed vectors, to define a defualt 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
% 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 }}
  {{ aux _ l }}
  |                                             :: :: nonrec {{ com non-recursive }}
  | rec                                         :: :: rec {{ com recursive }}

effect_opt :: 'Effect_opt_' ::=
  {{ com Optional effect annotation for functions }}
  {{ aux _ l }}
  |                                             :: :: pure {{ com sugar for empty effect set }}
  | effectkw effect                              :: :: effect

funcl :: 'FCL_' ::=
  {{ com Function clause }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | id pat = exp                   :: :: 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

letbind :: 'LB_' ::=
  {{ com Let binding }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | let typschm pat = exp                                :: :: val_explicit
    {{ com value binding, explicit type ([[pat]] must be total)}}
% at the moment, we cannot parse the following, so perhaps we shouldn't keep this form here 
  | let pat = exp                                    :: :: val_implicit
    {{ com value binding, implicit type ([[pat]] must be total)}}


val_spec :: 'VS_' ::=
  {{ com Value type specification }} 
  {{ aux _ annot }} {{ auxparam 'a }}
  | val typschm id                                  :: :: val_spec
  | val extern typschm id                           :: :: extern_no_rename
  | val extern typschm id = string                  :: :: extern_spec
    {{ com Specify the type and id of a function from 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 }} {{ auxparam 'a }}
  | default base_kind kid    :: :: kind
  | default Order order      :: :: order
  | default typschm id      :: :: typ
% The intended semantics of these is that if an id in binding position
% doesn't have a kind or type annotation, then we look through the
% default regexps (in order from the beginning) and pick the first
% assumption for which id matches the regexp, if there is one.
% Otherwise we try to infer.  Perhaps warn if there are multiple matches.
% For example, we might often have default Type ['alphanum]

scattered_def :: 'SD_' ::=
  {{ com Function and type union definitions that can be spread across
         a file. Each one must end in $[[end id]]$ }}
  {{ aux _ annot }} {{ auxparam 'a }}
  | scattered function rec_opt tannot_opt effect_opt id   :: :: scattered_function {{ texlong }} {{ com scattered function definition header }}

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

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

  | union id member type_union  :: :: scattered_unioncl {{ com scattered union definition member }}
  | end id  :: :: scattered_end
{{ 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 typ id                                             :: :: reg
  | register alias id = alias_spec				:: :: alias
  | register alias typ id = alias_spec				:: :: typ_alias

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

def :: 'DEF_' ::=
  {{ com Top-level definition }}
  {{ auxparam 'a }}
  | type_def                                                    :: :: type
    {{ com type definition }}
  | fundef                                                   :: :: fundef
    {{ com function definition }}
  | letbind                                                   :: :: val
    {{ com value definition }}
  | val_spec                                                    :: :: spec
    {{ com top-level type constraint }}
  | default_spec                                         :: :: default
    {{ com default kind and type assumptions }}
  | scattered_def                                        :: :: scattered
    {{ com scattered function and type definition }}
  | dec_spec                                            :: :: reg_dec
    {{ com register declaration }}


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



terminals :: '' ::=
  | **                                  :: :: starstar
    {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }}
    {{ com \texttt{**} }}
  | >=                                  :: :: geq
    {{ tex \ensuremath{\geq} }}
    {{ com \texttt{>=} }}
  | '<='                                        :: :: leq
    {{ tex \ensuremath{\leq} }}
    {{ com \texttt{<=} }}
  | ->                                  :: :: arrow
    {{ tex \ensuremath{\rightarrow} }}
    {{ 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} }}
  | >                                   :: :: gt
    {{ tex \ensuremath{\rangle} }}
  | 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} }}
  | '                                   :: :: quote
    {{ tex \mbox{'} }}
  | |->                                 :: :: 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 }}