diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/sail.ott | 111 |
1 files changed, 34 insertions, 77 deletions
diff --git a/language/sail.ott b/language/sail.ott index b35e64d3..585a2939 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -209,8 +209,8 @@ base_effect :: 'BE_' ::= | 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 }} + | 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 }} @@ -221,57 +221,24 @@ base_effect :: 'BE_' ::= effect :: 'Effect_' ::= {{ aux _ l }} - | { base_effect1 , .. , base_effectn } :: :: set {{ com effect set }} - | pure :: M :: pure {{ com sugar for empty effect set }} + | { 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 in user code) }} - | typ1 <-> typ2 :: :: bidir - {{ com Mapping }} -% 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 }} - | exist kid1 , .. , kidn , n_constraint . typ :: :: exist -% 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>}=\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 \texttt{[|} $[[nexp]]$ \texttt{|]} }} - | typ [ nexp : nexp' ] :: S :: vector3 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} -{{ com sugar for vector indexed by \texttt{[|} $[[nexp]]$..$[[nexp']]$ \texttt{|]} }} - | typ [ nexp <: nexp' ] :: S :: vector4 {{ ichlo vector < [[nexp]],[[nexp']],inc,[[typ]] }} {{ com sugar for increasing vector }} - | typ [ nexp :> nexp' ] :: S :: vector5 {{ ichlo vector < [[nexp]],[[nexp']],dec,[[typ]] }} {{ com sugar for decreasing vector }} -% | register [ id ] :: S :: register {{ ichlo (Typ_app Id "lteq_atom_atom") }} -% ...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_' ::= + | :: :: 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 }} + | { kid1 ... kidn , n_constraint . typ } :: :: exist + | id ( typ_arg1 , ... , typ_argn ) :: :: app {{ com type constructor application }} + | ( typ ) :: S :: paren {{ ichlo [[typ]] }} + +typ_arg :: 'A_' ::= {{ com type constructor arguments of all kinds }} {{ aux _ l }} | nexp :: :: nexp @@ -282,21 +249,18 @@ typ_arg :: 'Typ_arg_' ::= n_constraint :: 'NC_' ::= {{ com constraint over kind Int }} {{ aux _ l }} - | nexp = nexp' :: :: equal + | 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 + | n_constraint & n_constraint' :: :: or + | n_constraint | n_constraint' :: :: and | id ( typ_arg0 , ... , typ_argn ) :: :: app | kid :: :: var | true :: :: true | false :: :: false -% 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 }} @@ -386,8 +350,8 @@ type_def_aux :: 'TD_' ::= kind_def :: 'KD_' ::= {{ com Definition body for elements of kind }} {{ aux _ annot }} {{ auxparam 'a }} - | Def kind id name_scm_opt = nexp :: :: nabbrev - {{ com $[[Nat]]$-expression abbreviation }} + | Def kind id name_scm_opt = nexp :: :: nabbrev + {{ com Int-expression abbreviation }} type_union :: 'Tu_' ::= {{ com type union constructors }} @@ -638,13 +602,9 @@ exp :: 'E_' ::= | if exp1 then exp2 :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }} | loop exp1 exp2 :: :: loop - | while exp1 do exp2 :: S :: while {{ ichlo [[ loop while exp1 exp2 ]] }} - | repeat exp1 until exp2 :: S :: until {{ ichlo [[ loop until exp2 exp1 ]] }} + | while exp1 do exp2 :: S :: while {{ ichlo [[ loop while exp1 exp2 ]] }} + | repeat exp1 until exp2 :: S :: until {{ ichlo [[ loop until exp2 exp1 ]] }} | 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) }} @@ -740,29 +700,26 @@ exp :: 'E_' ::= 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 }} - | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }} -{{ com sugared form of above for explicit tuple $[[exp]]$ }} - | ( typ ) id :: :: cast -{{ com 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 }} + | 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 + | 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 + | :: :: empty + | ; default = exp :: :: dec pexp :: 'Pat_' ::= {{ com pattern match }} |