diff options
| -rw-r--r-- | language/l2.ott | 81 | ||||
| -rw-r--r-- | src/ast.ml | 53 |
2 files changed, 75 insertions, 59 deletions
diff --git a/language/l2.ott b/language/l2.ott index 0e0e3ce6..50c14c9c 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -170,6 +170,13 @@ id :: '' ::= {{ aux _ l }} | x :: :: id | ( x ) :: :: deIid {{ com remove infix status }} +% 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. + %% %% x_l {{ tex \ottnt{x}^{l} }} , y_l {{ tex \ottnt{y}^{l} }} , z_l {{ tex \ottnt{z}^{l} }} , name :: '' ::= @@ -288,7 +295,7 @@ base_kind :: 'BK_' ::= {{ aux _ l }} | Type :: :: type {{ com kind of types }} | Nat :: :: nat {{ com kind of natural number size expressions }} - | Endian :: :: endian {{ com kind of endianness specifications }} + | Order :: :: order {{ com kind of vector order specifications }} | Effects :: :: effects {{ com kind of effect sets }} kind :: 'K_' ::= @@ -299,7 +306,7 @@ kind :: 'K_' ::= nexp :: 'Nexp_' ::= - {{ com expression of kind Nat, for vector sizes and origins }} + {{ com expression of kind $[[Nat]]$, for vector sizes and origins }} {{ aux _ l }} | id :: :: id {{ com identifier }} | num :: :: constant {{ com constant }} @@ -309,13 +316,13 @@ nexp :: 'Nexp_' ::= | 2 ** nexp :: :: exp {{ com exponential }} | ( nexp ) :: S :: paren {{ icho [[nexp]] }} -endian :: 'End_' ::= - {{ com endianness specifications}} +order :: 'Ord_' ::= + {{ com vector order specifications, of kind $[[Order]]$}} {{ aux _ l }} | id :: :: id {{ com identifier }} | inc :: :: inc {{ com increasing (little-endian) }} | dec :: :: dec {{ com decreasing (big-endian) }} - | ( endian ) :: S :: paren {{ icho [[endian]] }} + | ( order ) :: S :: paren {{ icho [[order]] }} effect :: 'Effect_' ::= {{ com effect }} @@ -330,7 +337,7 @@ effect :: 'Effect_' ::= effects :: 'Effects_' ::= - {{ com effect set }} + {{ com effect set, of kind $[[Effects]]$ }} {{ aux _ l }} | id :: :: var | { effect1 , .. , effectn } :: :: set {{ com effect set }} @@ -340,7 +347,7 @@ effects :: 'Effects_' ::= typ :: 'Typ_' ::= - {{ com Constructor of kind Type }} + {{ com Type expressions, of kind $[[Type]]$ }} | _ :: :: wild {{ com Unspecified type }} | id :: :: var @@ -360,7 +367,7 @@ typ_arg :: 'Typ_arg_' ::= {{ com Type constructor arguments of all kinds }} | nexp :: :: nexp | typ :: :: typ - | endian :: :: endian + | order :: :: order | effects :: :: effects % plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations ... ref typ @@ -376,16 +383,16 @@ typ_lib :: 'Typ_lib_' ::= | nat :: :: nat {{ com natural numbers 0,1,2,... }} | string :: :: string {{ com UTF8 strings }} % finite subranges of nat - | enum nexp1 nexp2 endian :: :: enum {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1, ordered by [[endian]] }} + | enum nexp1 nexp2 order :: :: enum {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1, ordered by [[order]] }} | [ nexp ] :: :: enum1 {{ com sugar for \texttt{enum nexp 0 inc} }} | [ nexp '..' nexp' ] :: :: enum2 {{ com sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} }} % use .. not - to avoid ambiguity with nexp - % total maps and vectors indexed by finite subranges of nat - | vector nexp1 nexp2 endian typ :: :: vector {{ com vector of [[typ]], indexed by natural range }} + | 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 ] :: :: vector2 {{ com sugar for vector indexed by [ [[nexp]] ] }} - | typ [ nexp : nexp' ] :: :: vector3 {{ com sugar for vector indexed by [ [[nexp]]:[[nexp']] ] }} + | typ [ nexp : nexp' ] :: :: vector3 {{ com sugar for vector indexed by [ [[nexp]]..[[nexp']] ] }} % ...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]] }} @@ -405,7 +412,7 @@ Typ_fn <= Typ_tup grammar nexp_constraint :: 'NC_' ::= - {{ com contraint over kind Nat }} + {{ com constraint over kind $[[Nat]]$ }} {{ aux _ l }} | nexp = nexp' :: :: fixed | nexp >= nexp' :: :: bounded_ge @@ -422,16 +429,16 @@ kinded_id :: 'KOpt_' ::= | ( kinded_id ) :: S :: paren {{ icho [[kinded_id]] }} typquant :: 'TypQ_' ::= - {{ aux _ l }} + {{ aux _ l }} {{ com type quantifiers and constraints}} | forall kinded_id1 ... kinded_idn . nexp_constraint1 , ... , nexp_constrainti . :: :: tq {{ texlong }} % WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE - | forall kinded_id1 ... kinded_idn . :: :: no_constraint {{ com sugar }} - | :: :: no_forall {{ com sugar }} + | forall kinded_id1 ... kinded_idn . :: :: no_constraint {{ com sugar, omitting constraints}} + | :: :: no_forall {{ com sugar, omitting quantifier and constraints }} typschm :: 'TypSchm_' ::= - {{ com Type schemes }} + {{ com type scheme }} {{ aux _ l }} | typquant typ :: :: ts @@ -626,7 +633,8 @@ exp :: 'E_' ::= {{ com Expression }} {{ aux _ l }} - | { exp1 ; ... ; expn } :: :: block {{ com block (parsing conflict with structs?) }} + | { exp1 ; ... ; expn } :: :: block {{ com block (parsing conflict with structs?) }} +% maybe we really should have indentation-sensitive syntax :-) (given that some of the targets do) | id :: :: id {{ com identifier }} @@ -634,22 +642,29 @@ exp :: 'E_' ::= | lit :: :: lit {{ com literal constant }} - | exp1 exp2 :: :: app + | ( typ ) exp :: :: cast + {{ com cast }} + + | exp exp1 ... expn :: :: app {{ com function application }} - | exp1 id exp2 :: :: infix +% Note: fully applied function application only +% We might restrict exp to be an identifier +% We might require expn to have outermost parentheses (but not two sets if it's a tuple) + + | exp1 id exp2 :: :: app_infix {{ com infix function application }} - | ( exp1 , .... , expn ) :: :: tup + | ( exp1 , .... , expn ) :: :: tuple {{ com tuple }} | if exp1 then exp2 else exp3 :: :: if {{ com conditional }} - - % vectors | [ exp1 , ... , expn ] :: :: vector {{ com vector (indexed from 0) }} -% endianness comes from global command-line option??? +% 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 ] :: :: vector_indexed {{ com vector (indexed consecutively) }} % num1 .. numn must be a consecutive list of naturals @@ -662,22 +677,22 @@ exp :: 'E_' ::= | exp [ exp' ] :: :: vector_access {{ com vector access }} - | exp [ exp1 : exp2 ] :: :: vector_subrange + | 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_range + | [ 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? % lists - | [| exp1 , .. , expn |] :: :: list + | [| exp1 , .. , expn |] :: :: list {{ com list }} - | exp1 '::' exp2 :: :: cons + | exp1 '::' exp2 :: :: cons {{ com cons }} @@ -689,9 +704,9 @@ exp :: 'E_' ::= | { fexps } :: :: record {{ com struct }} - | { exp with fexps } :: :: recup + | { exp with fexps } :: :: record_update {{ com functional update of struct }} - | exp . id :: :: field + | exp . id :: :: field {{ com field projection from struct }} %Expressions for creating and accessing vectors @@ -852,10 +867,10 @@ fundef :: 'FD_' ::= letbind :: 'LB_' ::= {{ com Let binding }} {{ aux _ l }} - | typschm id = exp :: :: val_explicit - {{ com value binding with explicit type }} - | let id = exp :: :: val_implicit - {{ com value binding with implicit type }} + | typschm pat = exp :: :: val_explicit + {{ com value binding, explicit type ([[pat]] must be total)}} + | let pat = exp :: :: val_implicit + {{ com value binding, implicit type ([[pat]] must be total)}} val_spec :: 'VS_' ::= @@ -58,7 +58,7 @@ type base_kind_aux = (* base kind *) BK_type of terminal (* kind of types *) | BK_nat of terminal (* kind of natural number size expressions *) - | BK_endian of terminal (* kind of endianness specifications *) + | BK_order of terminal (* kind of vector order specifications *) | BK_effects of terminal (* kind of effect sets *) @@ -84,7 +84,7 @@ effect_aux = (* effect *) type -nexp_aux = (* expression of kind Nat, for vector sizes and origins *) +nexp_aux = (* expression of kind $_$, for vector sizes and origins *) Nexp_id of id (* identifier *) | Nexp_constant of terminal * int (* constant *) | Nexp_times of nexp * terminal * nexp (* product *) @@ -106,7 +106,7 @@ effect = type -nexp_constraint_aux = (* contraint over kind Nat *) +nexp_constraint_aux = (* constraint over kind $_$ *) NC_fixed of nexp * terminal * nexp | NC_bounded_ge of nexp * terminal * nexp | NC_bounded_le of nexp * terminal * nexp @@ -119,16 +119,16 @@ kind = type -effects_aux = (* effect set *) +effects_aux = (* effect set, of kind $_$ *) Effects_var of id | Effects_set of terminal * (effect * terminal) list * terminal (* effect set *) type -endian_aux = (* endianness specifications *) - End_id of id (* identifier *) - | End_inc of terminal (* increasing (little-endian) *) - | End_dec of terminal (* decreasing (big-endian) *) +order_aux = (* vector order specifications, of kind $_$ *) + Ord_id of id (* identifier *) + | Ord_inc of terminal (* increasing (little-endian) *) + | Ord_dec of terminal (* decreasing (big-endian) *) type @@ -148,19 +148,19 @@ effects = type -endian = - End_aux of endian_aux * l +order = + Ord_aux of order_aux * l type -typquant_aux = +typquant_aux = (* type quantifiers and constraints *) TypQ_tq of terminal * (kinded_id) list * terminal * (nexp_constraint * terminal) list * terminal - | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar *) - | TypQ_no_forall (* sugar *) + | TypQ_no_constraint of terminal * (kinded_id) list * terminal (* sugar, omitting constraints *) + | TypQ_no_forall (* sugar, omitting quantifier and constraints *) type -typ = (* Constructor of kind Type *) +typ = (* Type expressions, of kind $_$ *) Typ_wild of terminal (* Unspecified type *) | Typ_var of id (* Type variable *) | Typ_fn of typ * terminal * typ * effects (* Function type (first-order only in user code) *) @@ -170,7 +170,7 @@ typ = (* Constructor of kind Type *) and typ_arg = (* Type constructor arguments of all kinds *) Typ_arg_nexp of nexp | Typ_arg_typ of typ - | Typ_arg_endian of endian + | Typ_arg_order of order | Typ_arg_effects of effects @@ -180,7 +180,7 @@ typquant = type -typschm_aux = (* Type schemes *) +typschm_aux = (* type scheme *) TypSchm_ts of typquant * typ @@ -232,20 +232,21 @@ exp_aux = (* Expression *) E_block of terminal * (exp * terminal) list * terminal (* block (parsing conflict with structs?) *) | E_id of id (* identifier *) | E_lit of lit (* literal constant *) - | E_app of exp * exp (* function application *) - | E_infix of exp * id * exp (* infix function application *) - | E_tup of terminal * (exp * terminal) list * terminal (* tuple *) + | E_cast of terminal * typ * terminal * exp (* cast *) + | E_app of exp * (exp) list (* function application *) + | E_app_infix of exp * id * exp (* infix function application *) + | E_tuple of terminal * (exp * terminal) list * terminal (* tuple *) | E_if of terminal * exp * terminal * exp * terminal * exp (* conditional *) | E_vector of terminal * (exp * terminal) list * terminal (* vector (indexed from 0) *) | E_vector_indexed of terminal * ((terminal * int * terminal * exp) * terminal) list * terminal (* vector (indexed consecutively) *) | E_vector_access of exp * terminal * exp * terminal (* vector access *) | E_vector_subrange of exp * terminal * exp * terminal * exp * terminal (* subvector extraction *) | E_vector_update of terminal * exp * terminal * exp * terminal * exp * terminal (* vector functional update *) - | E_vector_update_range of terminal * exp * terminal * exp * terminal * exp * terminal * exp * terminal (* vector subrange update (with vector) *) + | E_vector_update_subrange of terminal * exp * terminal * exp * terminal * exp * terminal * exp * terminal (* vector subrange update (with vector) *) | E_list of terminal * (exp * terminal) list * terminal (* list *) | E_cons of exp * terminal * exp (* cons *) | E_record of terminal * fexps * terminal (* struct *) - | E_recup of terminal * exp * terminal * fexps * terminal (* functional update of struct *) + | E_record_update of terminal * exp * terminal * fexps * terminal (* functional update of struct *) | E_field of exp * terminal * id (* field projection from struct *) | E_case of terminal * exp * terminal * ((terminal * pexp)) list * terminal (* pattern matching *) | E_let of letbind * terminal * exp (* let expression *) @@ -279,8 +280,8 @@ and pexp = Pat_aux of pexp_aux * l and letbind_aux = (* Let binding *) - LB_val_explicit of typschm * id * terminal * exp (* value binding with explicit type *) - | LB_val_implicit of terminal * id * terminal * exp (* value binding with implicit type *) + LB_val_explicit of typschm * pat * terminal * exp (* value binding, explicit type (pat must be total) *) + | LB_val_implicit of terminal * pat * terminal * exp (* value binding, implicit type (pat must be total) *) and letbind = LB_aux of letbind_aux * l @@ -382,12 +383,12 @@ typ_lib_aux = (* library types and syntactic sugar for them *) | Typ_lib_bit of terminal (* pure bit values (not mutable bits) *) | Typ_lib_nat of terminal (* natural numbers 0,1,2,... *) | Typ_lib_string of terminal * Ulib.UTF8.t (* UTF8 strings *) - | Typ_lib_enum of terminal * nexp * nexp * endian (* natural numbers nexp .. nexp+nexp-1, ordered by endian *) + | Typ_lib_enum of terminal * nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *) | Typ_lib_enum1 of terminal * nexp * terminal (* sugar for \texttt{enum nexp 0 inc} *) | Typ_lib_enum2 of terminal * nexp * terminal * nexp * terminal (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) - | Typ_lib_vector of terminal * nexp * nexp * endian * typ (* vector of typ, indexed by natural range *) + | Typ_lib_vector of terminal * nexp * nexp * order * typ (* vector of typ, indexed by natural range *) | Typ_lib_vector2 of typ * terminal * nexp * terminal (* sugar for vector indexed by [ nexp ] *) - | Typ_lib_vector3 of typ * terminal * nexp * terminal * nexp * terminal (* sugar for vector indexed by [ nexp:nexp ] *) + | Typ_lib_vector3 of typ * terminal * nexp * terminal * nexp * terminal (* sugar for vector indexed by [ nexp..nexp ] *) | Typ_lib_list of terminal * typ (* list of typ *) | Typ_lib_set of terminal * typ (* finite set of typ *) | Typ_lib_reg of terminal * typ (* mutable register components holding typ *) |