From b1ccdc07a945d47a0ef5ca9bdec575f6b831cd27 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 15 Aug 2018 17:39:49 +0100 Subject: Various cleanups to ott grammar Add additional well-formedness check when calling typing rules --- language/sail.ott | 206 ++++++++++++++---------------------------------------- 1 file changed, 52 insertions(+), 154 deletions(-) (limited to 'language') diff --git a/language/sail.ott b/language/sail.ott index 4116013e..7ec736c5 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -151,30 +151,22 @@ id :: '' ::= % We don't enforce a lexical convention on infix operators, as some of the % targets use alphabetical infix operators. -% Vector builtins +% Vector builtins | vector_access :: M :: vector_access {{ ichlo (Id "vector_access") }} | vector_update :: M :: vector_update {{ ichlo (Id "vector_update") }} | vector_update_subrange :: M :: vector_update_subrange {{ ichlo (Id "vector_update_subrange") }} | vector_subrange :: M :: vector_subrange {{ ichlo (Id "vector_subrange") }} - | vector_append :: M :: vector_append {{ ichlo (Id "vector_append") }} - -% Comparison builtins - | lteq_atom_atom :: M :: lteq_atom_atom {{ ichlo (Id "lteq_atom_atom") }} - | gteq_atom_atom :: M :: gteq_atom_atom {{ ichlo (Id "gteq_atom_atom") }} - | lt_atom_atom :: M :: lt_atom_atom {{ ichlo (Id "lt_atom_atom") }} - | gt_atom_atom :: M :: gt_atom_atom {{ ichlo (Id "gt_atom_atom") }} - + | vector_append :: M :: vector_append {{ ichlo (Id "vector_append") }} + kid :: '' ::= - {{ com kinded IDs: $[[Type]]$, $[[Nat]]$, $[[Order]]$, and $[[Effect]]$ variables }} + {{ com kinded IDs: Type, Int, and Order variables }} {{ aux _ l }} - | ' x :: :: var - + | ' x :: :: var %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Kinds and Types % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - grammar base_kind :: 'BK_' ::= @@ -191,7 +183,7 @@ kind :: 'K_' ::= % we'll never use ...-> Nat , .. Order , .. or Effects nexp :: 'Nexp_' ::= - {{ com numeric expression, of kind $[[Nat]]$ }} + {{ com numeric expression, of kind Int }} {{ aux _ l }} | id :: :: id {{ com abbreviation identifier }} | kid :: :: var {{ com variable }} @@ -199,33 +191,33 @@ nexp :: 'Nexp_' ::= | id ( nexp1 , ... , nexpn ) :: :: app {{ com app }} | nexp1 * nexp2 :: :: times {{ com product }} | nexp1 + nexp2 :: :: sum {{ com sum }} - | nexp1 - nexp2 :: :: minus {{ com subtraction }} + | nexp1 - nexp2 :: :: minus {{ com subtraction }} | 2** nexp :: :: exp {{ com exponential }} - | neg nexp :: I :: neg {{ com for internal use only}} + | neg nexp :: I :: neg {{ com for internal use only}} | ( nexp ) :: S :: paren {{ ichlo [[nexp]] }} -order :: 'Ord_' ::= - {{ com vector order specifications, of kind $[[Order]]$}} - {{ aux _ l }} +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]] }} + | ( order ) :: S :: paren {{ ichlo [[order]] }} base_effect :: 'BE_' ::= {{ com effect }} - {{ aux _ l }} + {{ 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 }} + | 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 }} + | 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 }} + | depend :: :: depend {{ com dynamic footprint }} | undef :: :: undef {{ com undefined-instruction exception }} | unspec :: :: unspec {{ com unspecified values }} | nondet :: :: nondet {{ com nondeterminism, from $[[nondet]]$ }} @@ -233,18 +225,13 @@ base_effect :: 'BE_' ::= | config :: :: config {{ com configuration option }} effect :: 'Effect_' ::= - {{ com effect set, of kind $[[Effect]]$ }} {{ aux _ l }} - | { 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 union of sets of effects }} {{ icho [] }} - {{ lem (List.foldr effect_union (Effect_aux (Effect_set []) Unknown) [[effect1..effectn]]) }} - -% 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}. + | { 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]]$ }} + {{ com type expressions, of kind Type }} {{ aux _ l }} | :: :: internal_unknown | id :: :: id @@ -289,40 +276,15 @@ typ :: 'Typ_' ::= % 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 }} + {{ aux _ l }} | nexp :: :: nexp | typ :: :: typ | order :: :: order -% 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]]$ }} + {{ com constraint over kind Int }} {{ aux _ l }} | nexp = nexp' :: :: equal | nexp >= nexp' :: :: bounded_ge @@ -344,24 +306,21 @@ kinded_id :: 'KOpt_' ::= | kind kid :: :: kind {{ com kind-annotated variable }} quant_item :: 'QI_' ::= - {{ com kinded identifier or $[[Nat]]$ constraint }} + {{ com kinded identifier or Int constraint }} {{ aux _ l }} | kinded_id :: :: id {{ com optionally kinded identifier }} - | n_constraint :: :: const {{ com $[[Nat]]$ constraint }} + | n_constraint :: :: const {{ com Int constraint }} -typquant :: 'TypQ_' ::= +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 empty }} + | :: :: no_forall {{ com empty }} typschm :: 'TypSchm_' ::= {{ com type scheme }} {{ aux _ l }} - | typquant typ :: :: ts - - + | typquant typ :: :: ts %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Type definitions % @@ -431,21 +390,6 @@ kind_def :: 'KD_' ::= {{ aux _ annot }} {{ auxparam 'a }} | Def kind id name_scm_opt = nexp :: :: nabbrev {{ com $[[Nat]]$-expression abbreviation }} -% | Def kind id name_scm_opt = typschm :: D :: abbrev -% {{ com type abbreviation }} {{ texlong }} -% | Def kind id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: D :: record -% {{ com struct type definition }} {{ texlong }} -% | Def kind id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: D :: variant -% {{ com union type definition}} {{ texlong }} -% | Def kind id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: D :: enum -% {{ com enumeration type definition}} {{ texlong }} -% -% | Def kind id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } -%:: D :: register {{ com register mutable bitfield type definition }} {{ texlong }} - - - -% also sugar [ nexp ] type_union :: 'Tu_' ::= {{ com type union constructors }} @@ -458,41 +402,31 @@ index_range :: 'BF_' ::= {{ com index specification, for bitfields in register t | 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? - | string :: :: string {{ com string constant }} - | undefined :: :: undef {{ com undefined-value constant }} - | real :: :: real - + | ( ) :: :: 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 + | :: :: no {{ hol F }} {{ ocaml false }} {{ lem false }} @@ -501,7 +435,6 @@ semi_opt {{ tex \ottnt{;}^{?} }} :: 'semi_' ::= {{ phantom }} {{ ocaml true }} {{ lem true }} - %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Patterns % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -513,32 +446,26 @@ typ_pat :: 'TP_' ::= | kid :: :: var | id ( typ_pat1 , .. , typ_patn ) :: :: app - - -pat :: 'P_' ::= +pat :: 'P_' ::= {{ com pattern }} {{ aux _ annot }} {{ auxparam 'a }} - | lit :: :: lit + | lit :: :: lit {{ com literal constant pattern }} - | _ :: :: wild + | _ :: :: wild {{ com wildcard }} - | pat1 | pat2 :: :: or + | pat1 | pat2 :: :: or {{ com pattern disjunction }} - | ~ pat :: :: not + | ~ pat :: :: not {{ com pattern negation }} - | ( pat as id ) :: :: as + | ( pat as id ) :: :: as {{ com named pattern }} -% ML-style -% | ( pat : typ ) :: :: typ -% {{ com Typed patterns }} -% C-style - | ( typ ) pat :: :: typ + | ( typ ) pat :: :: typ {{ com typed pattern }} | id :: :: id {{ com identifier }} | pat typ_pat :: :: var {{ com bind pattern to type variable }} - | id ( pat1 , .. , patn ) :: :: app + | id ( pat1 , .. , patn ) :: :: app {{ com union constructor pattern }} % OR? do we invent something ghastly including a union keyword? Perhaps not... @@ -813,29 +740,10 @@ exp :: 'E_' ::= | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }} | constraint n_constraint :: :: constraint -%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 }} - - lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ aux _ annot }} {{ auxparam 'a }} - | id :: :: id -% | ref id :: :: ref + | id :: :: id {{ com identifier }} | deref exp :: :: deref - {{ com identifier }} | 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]]$ }} @@ -843,11 +751,9 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ 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 }} - % maybe comma-sep such lists too - | lexp . id :: :: field {{ com struct field }} - + | lexp [ exp ] :: :: vector {{ com vector element }} + | lexp [ exp1 '..' exp2 ] :: :: vector_range {{ com subvector }} + | lexp . id :: :: field {{ com struct field }} fexp :: 'FE_' ::= {{ com field expression }} @@ -1052,14 +958,6 @@ default_spec :: 'DT_' ::= {{ com default kinding or typing assumption }} {{ aux _ l }} | default Order order :: :: order - | default base_kind kid :: :: kind - | 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 scattered function and union type definitions }} -- cgit v1.2.3