diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | src/Makefile | 4 | ||||
| -rw-r--r-- | src/ast.ott | 1180 |
3 files changed, 3 insertions, 1182 deletions
@@ -1,3 +1,4 @@ +*~ *.native *.byte src/_build/ diff --git a/src/Makefile b/src/Makefile index d1e29d06..68ad408f 100644 --- a/src/Makefile +++ b/src/Makefile @@ -49,8 +49,8 @@ all: sail lib doc full: sail lib power doc test -ast.ml: ast.ott - ott -sort false -generate_aux_rules true -o ast.ml -picky_multiple_parses true ast.ott +ast.ml: ../language/l2.ott + ott -sort false -generate_aux_rules true -o ast.ml -picky_multiple_parses true ../language/l2.ott sail: ast.ml ocamlbuild sail.native diff --git a/src/ast.ott b/src/ast.ott deleted file mode 100644 index f08b089b..00000000 --- a/src/ast.ott +++ /dev/null @@ -1,1180 +0,0 @@ -%% -%% 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 int }} - {{ hol num }} - {{ lem integer }} - {{ com Numeric literals }} - -metavar nat ::= - {{ phantom }} - {{ 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 }} - -embed -{{ ocaml - -type text = string - -type l = Parse_ast.l - -type 'a annot = l * 'a - -type loop = While | Until - -}} - -embed -{{ lem -open import Pervasives -open import Pervasives_extra -open import Map -open import Maybe -open import Set_extra - -type l = - | Unknown - | Int of string * maybe l (*internal types, functions*) - | Range of string * nat * nat * nat * nat - | Generated of l (*location for a generated node, where l is the location of the closest original source*) - -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 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 - | ( deinfix x ) :: D :: 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") }} - | int :: M :: int {{ ichlo (Id "int") }} - | 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") }} - | msb :: M :: msb {{ ichlo (Id "msb") }} -% 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. - -% 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") }} - -kid :: '' ::= - {{ com kinded IDs: $[[Type]]$, $[[Nat]]$, $[[Order]]$, and $[[Effect]]$ 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 }} - - -kind :: 'K_' ::= - {{ com kinds}} - {{ aux _ l }} - | base_kind1 -> ... -> base_kindn :: :: kind -% we'll never use ...-> Nat , .. Order , .. or Effects - -nexp :: 'Nexp_' ::= - {{ com numeric expression, of kind $[[Nat]]$ }} - {{ aux _ l }} - | id :: :: id {{ com abbreviation identifier }} - | kid :: :: var {{ com variable }} - | num :: :: constant {{ com constant }} - | nexp1 * nexp2 :: :: times {{ com product }} - | nexp1 + nexp2 :: :: sum {{ com sum }} - | nexp1 - nexp2 :: :: minus {{ com subtraction }} - | 2** nexp :: :: exp {{ com exponential }} - | 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 }} - | 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 call of $[[exit]]$ }} - | lset :: :: lset {{ com local mutation; not user-writable }} - | lret :: :: lret {{ com local return; not user-writable }} - -effect :: 'Effect_' ::= - {{ com effect set, of kind $[[Effect]]$ }} - {{ 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 union of 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 (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 }} - | 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_' ::= - {{ com type constructor arguments of all kinds }} - {{ 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]]$ }} - {{ 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 - | 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 }} - | kid :: :: none {{ com identifier }} - | kind kid :: :: kind {{ com kind-annotated variable }} - -quant_item :: 'QI_' ::= - {{ com kinded identifier or $[[Nat]]$ constraint }} - {{ aux _ l }} - | kinded_id :: :: id {{ com optionally kinded identifier }} - | n_constraint :: :: const {{ com $[[Nat]]$ constraint }} - -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 }} - -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 constraint}} - {{ 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 {{ ocaml 'a type_def }} :: 'TD_' ::= - {{ ocaml TD_aux of type_def_aux * 'a annot }} - | type_def_aux :: :: aux - -type_def_aux :: 'TD_' ::= - {{ com type definition body }} - | 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 tagged 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 }} - - -% the D(eprecated) forms here should be removed; they add complexity for no purpose. The nexp abbreviation form should have better syntax. -% ; many are shorthands for type\_defs -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 = 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 }} - {{ 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? - | 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 % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - - -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 }} - | pat kid :: :: 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 }} - -% 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 - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Machinery for typing rules % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -embed -{{ lem - -let rec remove_one i l = - match l with - | [] -> [] - | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2) -end - -let rec remove_from l l2 = - match l2 with - | [] -> l - | i::l2' -> remove_from (remove_one i l) l2' -end - -let disjoint s1 s2 = Set.null (s1 inter s2) - -let rec disjoint_all sets = - match sets with - | [] -> true - | s1::[] -> true - | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets)) -end -}} - - -grammar - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Expressions % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -embed -{{ lem - -type tannot = maybe (t * tag * list nec * effect * effect) - -}} - -grammar -tannot :: '' ::= - {{ phantom }} - {{ ocaml tannot }} - {{ lem tannot }} -loop :: loop ::= {{ phantom }} - | while :: :: while - | until :: :: until - - -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 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 ]] }} - | 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 }} - - | 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 }} - | 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]] }} - | ( annot ) exp :: I :: internal_cast {{ com This is an internal cast, generated during type checking that will resolve into a syntactic cast after }} - | annot :: I :: internal_exp {{ com This is an internal use for passing nexp information to library functions, postponed for constraint solving }} - | sizeof annot :: I :: sizeof_internal {{ com For sizeof during type checking, to replace nexp with internal n}} - | annot , annot' :: I :: internal_exp_user {{ com This is like the above but the user has specified an implicit parameter for the current function }} - | comment string :: I :: comment {{ com For generated unstructured comments }} - | comment exp :: I :: comment_struc {{ com For generated structured comments }} - | let lexp = exp in exp' :: I :: internal_let {{ 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 - -%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 - {{ 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]]$ }} - | ( typ ) id :: :: cast -{{ com cast }} - | ( lexp0 , .. , lexpn ) :: :: tup {{ com multiple (non-memory) assignment }} - | 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 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 }} - {{ 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 let, 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 - {{ com let, implicit type ($[[pat]]$ must be total)}} - -val_spec {{ ocaml 'a val_spec }} :: 'VS_' ::= - {{ ocaml VS_aux of val_spec_aux * 'a annot }} - | val_spec_aux :: :: aux - - -val_spec_aux :: 'VS_' ::= - {{ com value type specification }} - {{ ocaml VS_val_spec of typschm * id * string option * bool }} - | val typschm id :: S :: val_spec - {{ com specify the type of an upcoming definition }} - {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} - | val cast typschm id :: S :: cast - {{ ocaml (VS_val_spec [[typschm]] [[id]] None true) }} - | 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) }} - | 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) }} -%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 - | 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 }} - {{ 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 -{{ texlong }} {{ 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 -{{ texlong }} {{ com scattered union definition member }} - | end id :: :: scattered_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 typ id :: :: reg - | register alias id = alias_spec :: :: alias - | register alias typ id = alias_spec :: :: typ_alias - -dec_comm :: 'DC_' ::= {{ com top-level generated comments }} {{auxparam 'a}} - | comment string :: :: comm {{ com generated unstructured comment }} - | comment def :: :: comm_struct {{ com generated structured comment }} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Top-level definitions % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -prec :: '' ::= - | infix :: :: Infix - | infixl :: :: InfixL - | infixr :: :: InfixR - -def :: 'DEF_' ::= - {{ com top-level definition }} - {{ auxparam 'a }} - | kind_def :: :: kind - {{ com definition of named kind identifiers }} - | type_def :: :: type - {{ com type definition }} - | fundef :: :: fundef - {{ com function 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 }} - | dec_spec :: :: reg_dec - {{ com register declaration }} - | dec_comm :: I :: comm - {{ com generated comments }} - -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} }} -% {{ 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]}$} }} - - |