From dcc2ec2e4e6a3fd9a393af64d45bdf659201da03 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Thu, 28 Nov 2013 17:07:32 +0000 Subject: Updated syntax with working examples --- language/l2.lem | 72 +++++++------ language/l2.ml | 236 +++++++++++++++++++++++-------------------- language/l2.ott | 31 ++++-- language/l2_parse.ml | 108 +++++++++++--------- language/l2_parse.ott | 14 ++- src/initial_check.ml | 172 ++++++++++++++++++++----------- src/lem_interp/run_interp.ml | 2 +- src/lexer.mll | 1 + src/parser.mly | 54 +++++----- src/pre_parser.mly | 26 +++-- src/pretty_print.ml | 44 +++++--- src/process_file.ml | 5 +- src/test/test1.sail | 14 +-- src/test/test3.sail | 4 +- 14 files changed, 458 insertions(+), 325 deletions(-) diff --git a/language/l2.lem b/language/l2.lem index 79cb82b3..da806b57 100644 --- a/language/l2.lem +++ b/language/l2.lem @@ -22,11 +22,6 @@ val subst : forall 'a. list 'a -> list 'a -> bool type x = string (* identifier *) type ix = string (* infix identifier *) -type id = (* Identifier *) - | Id of x - | DeIid of x (* remove infix status *) - - type base_kind = (* base kind *) | BK_type (* kind of types *) | BK_nat (* kind of natural number size expressions *) @@ -34,18 +29,28 @@ type base_kind = (* base kind *) | BK_effects (* kind of effect sets *) +type id = (* Identifier *) + | Id of x + | DeIid of x (* remove infix status *) + + +type var = (* variables with kind, ticked to differntiate from program variables *) + | Var of x + + +type kind = (* kinds *) + | K_kind of list base_kind + + type nexp = (* expression of kind $Nat$, for vector sizes and origins *) | Nexp_id of id (* identifier *) + | Nexp_var of var (* variable *) | Nexp_constant of nat (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) | Nexp_exp of nexp (* exponential *) -type kind = (* kinds *) - | K_kind of list base_kind - - type efct = (* effect *) | Effect_rreg (* read register *) | Effect_wreg (* write register *) @@ -56,6 +61,11 @@ type efct = (* effect *) | Effect_nondet (* nondeterminism from intra-instruction parallelism *) +type kinded_id = (* optionally kind-annotated identifier *) + | KOpt_none of var (* identifier *) + | KOpt_kind of kind * var (* kind-annotated variable *) + + type nexp_constraint = (* constraint over kind $Nat$ *) | NC_fixed of nexp * nexp | NC_bounded_ge of nexp * nexp @@ -63,22 +73,19 @@ type nexp_constraint = (* constraint over kind $Nat$ *) | NC_nat_set_bounded of id * list nat -type kinded_id = (* optionally kind-annotated identifier *) - | KOpt_none of id (* identifier *) - | KOpt_kind of kind * id (* kind-annotated variable *) - - -type effects = (* effect set, of kind $Effects$ *) - | Effects_var of id - | Effects_set of list efct (* effect set *) - - type order = (* vector order specifications, of kind $Order$ *) | Ord_id of id (* identifier *) + | Ord_var of var (* variable *) | Ord_inc (* increasing (little-endian) *) | Ord_dec (* decreasing (big-endian) *) +type effects = (* effect set, of kind $Effects$ *) + | Effects_id of id + | Effects_var of var + | Effects_set of list efct (* effect set *) + + type quant_item = (* Either a kinded identifier or a nexp constraint for a typquant *) | QI_id of kinded_id (* An optionally kinded identifier *) | QI_const of nexp_constraint (* A constraint for this type *) @@ -99,7 +106,8 @@ type lit = (* Literal constant *) type typ = (* Type expressions, of kind $Type$ *) | Typ_wild (* Unspecified type *) - | Typ_var of id (* Type variable *) + | Typ_id of id (* Defined type *) + | Typ_var of var (* Type variable *) | Typ_fn of typ * typ * effects (* Function type (first-order only in user code) *) | Typ_tup of list typ (* Tuple type *) | Typ_app of id * list typ_arg (* type constructor application *) @@ -184,15 +192,15 @@ and letbind = (* Let binding *) | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *) -type funcl = (* Function clause *) - | FCL_Funcl of id * pat * exp - - type effects_opt = (* Optional effect annotation for functions *) | Effects_opt_pure (* sugar for empty effect set *) | Effects_opt_effects of effects +type funcl = (* Function clause *) + | FCL_Funcl of id * pat * exp + + type rec_opt = (* Optional recursive annotation for functions *) | Rec_nonrec (* non-recursive *) | Rec_rec (* recursive *) @@ -218,21 +226,21 @@ type index_range = (* index specification, for bitfields in register types *) | BF_concat of index_range * index_range (* concatenation of index ranges *) -type val_spec = (* Value type specification *) - | VS_val_spec of typschm * id - | VS_extern_no_rename of typschm * id - | VS_extern_spec of typschm * id * string (* 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 *) - - type fundef = (* Function definition *) | FD_function of rec_opt * tannot_opt * effects_opt * list funcl type default_typing_spec = (* Default kinding or typing assumption *) - | DT_kind of base_kind * id + | DT_kind of base_kind * var | DT_typ of typschm * id +type val_spec = (* Value type specification *) + | VS_val_spec of typschm * id + | VS_extern_no_rename of typschm * id + | VS_extern_spec of typschm * id * string (* 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 *) + + type type_def = (* Type definition body *) | TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *) | TD_record of id * naming_scheme_opt * typquant * list (typ * id) * bool (* struct type definition *) @@ -264,7 +272,7 @@ type typ_lib = (* library types and syntactic sugar for them *) | Typ_lib_bool (* booleans $true$ and $false$ *) | Typ_lib_bit (* pure bit values (not mutable bits) *) | Typ_lib_nat (* natural numbers 0,1,2,... *) - | Typ_lib_string (* UTF8 strings *) + | Typ_lib_string of string (* UTF8 strings *) | Typ_lib_enum of nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *) | Typ_lib_enum1 of nexp (* sugar for \texttt{enum nexp 0 inc} *) | Typ_lib_enum2 of nexp * nexp (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) diff --git a/language/l2.ml b/language/l2.ml index 6ecf3411..00c59136 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -20,8 +20,8 @@ base_kind_aux = (* base kind *) type -base_kind = - BK_aux of base_kind_aux * l +var_aux = (* variables with kind, ticked to differntiate from program variables *) + Var of x type @@ -31,8 +31,13 @@ id_aux = (* Identifier *) type -kind_aux = (* kinds *) - K_kind of (base_kind) list +base_kind = + BK_aux of base_kind_aux * l + + +type +var = + Var_aux of var_aux * l type @@ -41,13 +46,14 @@ id = type -kind = - K_aux of kind_aux * l +kind_aux = (* kinds *) + K_kind of (base_kind) list type nexp_aux = (* expression of kind $_$, for vector sizes and origins *) Nexp_id of id (* identifier *) + | Nexp_var of var (* variable *) | Nexp_constant of int (* constant *) | Nexp_times of nexp * nexp (* product *) | Nexp_sum of nexp * nexp (* sum *) @@ -58,9 +64,8 @@ and nexp = type -kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of id (* identifier *) - | KOpt_kind of kind * id (* kind-annotated variable *) +kind = + K_aux of kind_aux * l type @@ -71,6 +76,22 @@ nexp_constraint_aux = (* constraint over kind $_$ *) | NC_nat_set_bounded of id * (int) list +type +kinded_id_aux = (* optionally kind-annotated identifier *) + KOpt_none of var (* identifier *) + | KOpt_kind of kind * var (* kind-annotated variable *) + + +type +nexp_constraint = + NC_aux of nexp_constraint_aux * l + + +type +kinded_id = + KOpt_aux of kinded_id_aux * l + + type efct_aux = (* effect *) Effect_rreg (* read register *) @@ -83,13 +104,9 @@ efct_aux = (* effect *) type -kinded_id = - KOpt_aux of kinded_id_aux * l - - -type -nexp_constraint = - NC_aux of nexp_constraint_aux * l +quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) + QI_id of kinded_id (* An optionally kinded identifier *) + | QI_const of nexp_constraint (* A constraint for this type *) type @@ -98,27 +115,29 @@ efct = type -quant_item_aux = (* Either a kinded identifier or a nexp constraint for a typquant *) - QI_id of kinded_id (* An optionally kinded identifier *) - | QI_const of nexp_constraint (* A constraint for this type *) +quant_item = + QI_aux of quant_item_aux * l type effects_aux = (* effect set, of kind $_$ *) - Effects_var of id + Effects_id of id + | Effects_var of var | Effects_set of (efct) list (* effect set *) type order_aux = (* vector order specifications, of kind $_$ *) Ord_id of id (* identifier *) + | Ord_var of var (* variable *) | Ord_inc (* increasing (little-endian) *) | Ord_dec (* decreasing (big-endian) *) type -quant_item = - QI_aux of quant_item_aux * l +typquant_aux = (* type quantifiers and constraints *) + TypQ_tq of (quant_item) list + | TypQ_no_forall (* sugar, omitting quantifier and constraints *) type @@ -131,12 +150,6 @@ order = Ord_aux of order_aux * l -type -typquant_aux = (* type quantifiers and constraints *) - TypQ_tq of (quant_item) list - | TypQ_no_forall (* sugar, omitting quantifier and constraints *) - - type lit_aux = (* Literal constant *) L_unit (* $() : _$ *) @@ -151,10 +164,16 @@ lit_aux = (* Literal constant *) | L_string of string (* string constant *) +type +typquant = + TypQ_aux of typquant_aux * l + + type typ_aux = (* Type expressions, of kind $_$ *) Typ_wild (* Unspecified type *) - | Typ_var of id (* Type variable *) + | Typ_id of id (* Defined type *) + | Typ_var of var (* Type variable *) | Typ_fn of typ * typ * effects (* Function type (first-order only in user code) *) | Typ_tup of (typ) list (* Tuple type *) | Typ_app of id * (typ_arg) list (* type constructor application *) @@ -172,11 +191,6 @@ and typ_arg = Typ_arg_aux of typ_arg_aux * l -type -typquant = - TypQ_aux of typquant_aux * l - - type lit = L_aux of lit_aux * l @@ -218,7 +232,38 @@ typschm = type -'a letbind_aux = (* Let binding *) +'a exp = + E_aux of 'a exp_aux * 'a annot + +and 'a lexp_aux = (* lvalue expression *) + LEXP_id of id (* identifier *) + | LEXP_memory of id * 'a exp (* memory write via function call *) + | LEXP_vector of 'a lexp * 'a exp (* vector element *) + | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *) + | LEXP_field of 'a lexp * id (* struct field *) + +and 'a lexp = + LEXP_aux of 'a lexp_aux * 'a annot + +and 'a fexp_aux = (* Field-expression *) + FE_Fexp of id * 'a exp + +and 'a fexp = + FE_aux of 'a fexp_aux * 'a annot + +and 'a fexps_aux = (* Field-expression list *) + FES_Fexps of ('a fexp) list * bool + +and 'a fexps = + FES_aux of 'a fexps_aux * 'a annot + +and 'a pexp_aux = (* Pattern match *) + Pat_exp of 'a pat * 'a exp + +and 'a pexp = + Pat_aux of 'a pexp_aux * 'a annot + +and 'a letbind_aux = (* Let binding *) LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *) | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *) @@ -250,42 +295,27 @@ and 'a exp_aux = (* Expression *) | E_let of 'a letbind * 'a exp (* let expression *) | E_assign of 'a lexp * 'a exp (* imperative assignment *) -and 'a exp = - E_aux of 'a exp_aux * 'a annot - -and 'a lexp_aux = (* lvalue expression *) - LEXP_id of id (* identifier *) - | LEXP_memory of id * 'a exp (* memory write via function call *) - | LEXP_vector of 'a lexp * 'a exp (* vector element *) - | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *) - | LEXP_field of 'a lexp * id (* struct field *) - -and 'a lexp = - LEXP_aux of 'a lexp_aux * 'a annot - -and 'a fexp_aux = (* Field-expression *) - FE_Fexp of id * 'a exp -and 'a fexp = - FE_aux of 'a fexp_aux * 'a annot +type +'a effects_opt_aux = (* Optional effect annotation for functions *) + Effects_opt_pure (* sugar for empty effect set *) + | Effects_opt_effects of effects -and 'a fexps_aux = (* Field-expression list *) - FES_Fexps of ('a fexp) list * bool -and 'a fexps = - FES_aux of 'a fexps_aux * 'a annot +type +'a tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_some of typquant * typ -and 'a pexp_aux = (* Pattern match *) - Pat_exp of 'a pat * 'a exp -and 'a pexp = - Pat_aux of 'a pexp_aux * 'a annot +type +rec_opt_aux = (* Optional recursive annotation for functions *) + Rec_nonrec (* non-recursive *) + | Rec_rec (* recursive *) type -type_union_aux = (* Type union constructors *) - Tu_id of id - | Tu_ty_id of typ * id +'a funcl_aux = (* Function clause *) + FCL_Funcl of id * 'a pat * 'a exp type @@ -295,25 +325,29 @@ naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for va type -'a funcl_aux = (* Function clause *) - FCL_Funcl of id * 'a pat * 'a exp +type_union_aux = (* Type union constructors *) + Tu_id of id + | Tu_ty_id of typ * id type -rec_opt_aux = (* Optional recursive annotation for functions *) - Rec_nonrec (* non-recursive *) - | Rec_rec (* recursive *) +'a effects_opt = + Effects_opt_aux of 'a effects_opt_aux * 'a annot type -'a tannot_opt_aux = (* Optional type annotation for functions *) - Typ_annot_opt_some of typquant * typ +'a tannot_opt = + Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot type -'a effects_opt_aux = (* Optional effect annotation for functions *) - Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of effects +rec_opt = + Rec_aux of rec_opt_aux * l + + +type +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot type @@ -326,41 +360,19 @@ and index_range = BF_aux of index_range_aux * l -type -type_union = - Tu_aux of type_union_aux * l - - type naming_scheme_opt = Name_sect_aux of naming_scheme_opt_aux * l type -'a funcl = - FCL_aux of 'a funcl_aux * 'a annot - - -type -rec_opt = - Rec_aux of rec_opt_aux * l - - -type -'a tannot_opt = - Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot - - -type -'a effects_opt = - Effects_opt_aux of 'a effects_opt_aux * 'a annot +type_union = + Tu_aux of type_union_aux * l type -'a val_spec_aux = (* Value type specification *) - VS_val_spec of typschm * id - | VS_extern_no_rename of typschm * id - | VS_extern_spec of typschm * id * string (* 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 *) +'a fundef_aux = (* Function definition *) + FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list type @@ -373,19 +385,21 @@ type type -'a fundef_aux = (* Function definition *) - FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list +'a default_typing_spec_aux = (* Default kinding or typing assumption *) + DT_kind of base_kind * var + | DT_typ of typschm * id type -'a default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of base_kind * id - | DT_typ of typschm * id +'a val_spec_aux = (* Value type specification *) + VS_val_spec of typschm * id + | VS_extern_no_rename of typschm * id + | VS_extern_spec of typschm * id * string (* 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 *) type -'a val_spec = - VS_aux of 'a val_spec_aux * 'a annot +'a fundef = + FD_aux of 'a fundef_aux * 'a annot type @@ -394,13 +408,13 @@ type type -'a fundef = - FD_aux of 'a fundef_aux * 'a annot +'a default_typing_spec = + DT_aux of 'a default_typing_spec_aux * 'a annot type -'a default_typing_spec = - DT_aux of 'a default_typing_spec_aux * 'a annot +'a val_spec = + VS_aux of 'a val_spec_aux * 'a annot type @@ -424,7 +438,7 @@ type | Typ_lib_bool (* booleans $_$ and $_$ *) | Typ_lib_bit (* pure bit values (not mutable bits) *) | Typ_lib_nat (* natural numbers 0,1,2,... *) - | Typ_lib_string (* UTF8 strings *) + | Typ_lib_string of string (* UTF8 strings *) | Typ_lib_enum of nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *) | Typ_lib_enum1 of nexp (* sugar for \texttt{enum nexp 0 inc} *) | Typ_lib_enum2 of nexp * nexp (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *) diff --git a/language/l2.ott b/language/l2.ott index e28e0271..9c801336 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -129,7 +129,11 @@ id :: '' ::= % We don't enforce a lexical convention on infix operators, as some of the % targets use alphabetical infix operators. - +var :: '' ::= + {{ com variables with kind, ticked to differntiate from program variables }} + {{ aux _ l }} + | ' x :: :: var + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Kinds and Types % @@ -157,6 +161,7 @@ nexp :: 'Nexp_' ::= {{ com expression of kind $[[Nat]]$, for vector sizes and origins }} {{ aux _ l }} | id :: :: id {{ com identifier }} + | var :: :: var {{ com variable }} | num :: :: constant {{ com constant }} | nexp1 * nexp2 :: :: times {{ com product }} %{{ com must be linear after normalisation... except for the type of *, ahem }} @@ -168,6 +173,7 @@ order :: 'Ord_' ::= {{ com vector order specifications, of kind $[[Order]]$}} {{ aux _ l }} | id :: :: id {{ com identifier }} + | var :: :: var {{ com variable }} | inc :: :: inc {{ com increasing (little-endian) }} | dec :: :: dec {{ com decreasing (big-endian) }} | ( order ) :: S :: paren {{ ichlo [[order]] }} @@ -187,7 +193,8 @@ efct :: 'Effect_' ::= effects :: 'Effects_' ::= {{ com effect set, of kind $[[Effects]]$ }} {{ aux _ l }} - | effect id :: :: var + | effect id :: :: id + | effect var :: :: var | effect { efct1 , .. , efctn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ ichlo [] }} | effects1 u+ .. u+ effectsn :: M :: union {{ com meta operation for combining sets of effects }} {{ ichlo [] }} @@ -199,7 +206,9 @@ typ :: 'Typ_' ::= {{ aux _ l }} | _ :: :: wild {{ com Unspecified type }} - | id :: :: var + | id :: :: id + {{ com Defined type }} + | var :: :: var {{ com Type variable }} | typ1 -> typ2 effects :: :: fn {{ com Function type (first-order only in user code) }} @@ -226,12 +235,12 @@ 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) }} + | 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 }} + | nat :: :: nat {{ com natural numbers 0,1,2,... }} + | string :: :: string {{ com UTF8 strings }} % finite subranges of nat | 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} }} @@ -275,8 +284,8 @@ nexp_constraint :: 'NC_' ::= kinded_id :: 'KOpt_' ::= {{ com optionally kind-annotated identifier }} {{ aux _ l }} - | id :: :: none {{ com identifier }} - | kind id :: :: kind {{ com kind-annotated variable }} + | var :: :: none {{ com identifier }} + | kind var :: :: kind {{ com kind-annotated variable }} quant_item :: 'QI_' ::= {{ com Either a kinded identifier or a nexp constraint for a typquant }} @@ -763,7 +772,7 @@ val_spec :: 'VS_' ::= default_typing_spec :: 'DT_' ::= {{ com Default kinding or typing assumption }} {{ aux _ annot }} {{ auxparam 'a }} - | default base_kind id :: :: kind + | default base_kind var :: :: 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 diff --git a/language/l2_parse.ml b/language/l2_parse.ml index 990166c4..b196f007 100644 --- a/language/l2_parse.ml +++ b/language/l2_parse.ml @@ -24,6 +24,17 @@ base_kind_aux = (* base kind *) | BK_effects (* kind of effect sets *) +type +id_aux = (* Identifier *) + Id of x + | DeIid of x (* remove infix status *) + + +type +var_aux = (* variables with kind, ticked to differntiate from program variables *) + Var of x + + type efct_aux = (* effect *) Effect_rreg (* read register *) @@ -36,24 +47,23 @@ efct_aux = (* effect *) type -id_aux = (* Identifier *) - Id of x - | DeIid of x (* remove infix status *) +base_kind = + BK_aux of base_kind_aux * l type -base_kind = - BK_aux of base_kind_aux * l +id = + Id_aux of id_aux * l type -efct = - Effect_aux of efct_aux * l +var = + Var_aux of var_aux * l type -id = - Id_aux of id_aux * l +efct = + Effect_aux of efct_aux * l type @@ -64,6 +74,7 @@ kind_aux = (* kinds *) type atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders, and effects after parsing *) ATyp_id of id (* identifier *) + | ATyp_var of var (* ticked variable *) | ATyp_constant of int (* constant *) | ATyp_times of atyp * atyp (* product *) | ATyp_sum of atyp * atyp (* sum *) @@ -71,6 +82,7 @@ atyp_aux = (* expressions of all kinds, to be translated to types, nats, orders | ATyp_inc (* increasing (little-endian) *) | ATyp_dec (* decreasing (big-endian) *) | ATyp_efid of id + | ATyp_efvar of var | ATyp_set of (efct) list (* effect set *) | ATyp_wild (* Unspecified type *) | ATyp_fn of atyp * atyp * atyp (* Function type (first-order only in user code), last atyp is an effect *) @@ -96,8 +108,8 @@ nexp_constraint_aux = (* constraint over kind $_$ *) type kinded_id_aux = (* optionally kind-annotated identifier *) - KOpt_none of id (* identifier *) - | KOpt_kind of kind * id (* kind-annotated variable *) + KOpt_none of var (* identifier *) + | KOpt_kind of kind * var (* kind-annotated variable *) type @@ -127,6 +139,11 @@ typquant_aux = (* type quantifiers and constraints *) | TypQ_no_forall (* sugar, omitting quantifier and constraints *) +type +typquant = + TypQ_aux of typquant_aux * l + + type lit_aux = (* Literal constant *) L_unit (* $() : _$ *) @@ -142,8 +159,8 @@ lit_aux = (* Literal constant *) type -typquant = - TypQ_aux of typquant_aux * l +typschm_aux = (* type scheme *) + TypSchm_ts of typquant * atyp type @@ -152,8 +169,8 @@ lit = type -typschm_aux = (* type scheme *) - TypSchm_ts of typquant * atyp +typschm = + TypSchm_aux of typschm_aux * l type @@ -181,11 +198,6 @@ and fpat = FP_aux of fpat_aux * l -type -typschm = - TypSchm_aux of typschm_aux * l - - type exp_aux = (* Expression *) E_block of (exp) list (* block (parsing conflict with structs?) *) @@ -241,12 +253,6 @@ and letbind = LB_aux of letbind_aux * l -type -naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) - Name_sect_none - | Name_sect_some of string - - type type_union_aux = (* Type union constructors *) Tu_id of id @@ -254,15 +260,15 @@ type_union_aux = (* Type union constructors *) type -tannot_opt_aux = (* Optional type annotation for functions *) - Typ_annot_opt_none - | Typ_annot_opt_some of typquant * atyp +naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *) + Name_sect_none + | Name_sect_some of string type -effects_opt_aux = (* Optional effect annotation for functions *) - Effects_opt_pure (* sugar for empty effect set *) - | Effects_opt_effects of atyp +tannot_opt_aux = (* Optional type annotation for functions *) + Typ_annot_opt_none + | Typ_annot_opt_some of typquant * atyp type @@ -277,8 +283,14 @@ funcl_aux = (* Function clause *) type -naming_scheme_opt = - Name_sect_aux of naming_scheme_opt_aux * l +effects_opt_aux = (* Optional effect annotation for functions *) + Effects_opt_pure (* sugar for empty effect set *) + | Effects_opt_effects of atyp + + +type +type_union = + Tu_aux of type_union_aux * l type @@ -292,8 +304,8 @@ and index_range = type -type_union = - Tu_aux of type_union_aux * l +naming_scheme_opt = + Name_sect_aux of naming_scheme_opt_aux * l type @@ -301,11 +313,6 @@ tannot_opt = Typ_annot_opt_aux of tannot_opt_aux * l -type -effects_opt = - Effects_opt_aux of effects_opt_aux * l - - type rec_opt = Rec_aux of rec_opt_aux * l @@ -317,10 +324,8 @@ funcl = type -val_spec_aux = (* Value type specification *) - VS_val_spec of typschm * id - | VS_extern_no_rename of typschm * id - | VS_extern_spec of typschm * id * string +effects_opt = + Effects_opt_aux of effects_opt_aux * l type @@ -334,7 +339,7 @@ type_def_aux = (* Type definition body *) type default_typing_spec_aux = (* Default kinding or typing assumption *) - DT_kind of base_kind * id + DT_kind of base_kind * var | DT_typ of typschm * id @@ -344,8 +349,10 @@ fundef_aux = (* Function definition *) type -val_spec = - VS_aux of val_spec_aux * l +val_spec_aux = (* Value type specification *) + VS_val_spec of typschm * id + | VS_extern_no_rename of typschm * id + | VS_extern_spec of typschm * id * string type @@ -363,6 +370,11 @@ fundef = FD_aux of fundef_aux * l +type +val_spec = + VS_aux of val_spec_aux * l + + type def_aux = (* Top-level definition *) DEF_type of type_def (* type definition *) diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 6876fcfa..f96c3f99 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -118,6 +118,12 @@ id :: '' ::= | x :: :: id | ( deinfix x ) :: :: deIid {{ com remove infix status }} + +var :: '' ::= + {{ com variables with kind, ticked to differntiate from program variables }} + {{ aux _ l }} + | ' x :: :: var + % 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 @@ -162,6 +168,7 @@ atyp :: 'ATyp_' ::= {{ com expressions of all kinds, to be translated to types, nats, orders, and effects after parsing }} {{ aux _ l }} | id :: :: id {{ com identifier }} + | var :: :: var {{ com ticked variable }} | num :: :: constant {{ com constant }} | atyp1 * atyp2 :: :: times {{ com product }} | atyp1 + atyp2 :: :: sum {{ com sum }} @@ -171,6 +178,7 @@ atyp :: 'ATyp_' ::= | inc :: :: inc {{ com increasing (little-endian) }} | dec :: :: dec {{ com decreasing (big-endian) }} | effect id :: :: efid + | effect var :: :: efvar | effect { efct1 , .. , efctn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }} @@ -237,8 +245,8 @@ nexp_constraint :: 'NC_' ::= kinded_id :: 'KOpt_' ::= {{ com optionally kind-annotated identifier }} {{ aux _ l }} - | id :: :: none {{ com identifier }} - | kind id :: :: kind {{ com kind-annotated variable }} + | var :: :: none {{ com identifier }} + | kind var :: :: kind {{ com kind-annotated variable }} quant_item :: 'QI_' ::= {{ com Either a kinded identifier or a nexp constraint for a typquant }} @@ -682,7 +690,7 @@ default_typing_spec :: 'DT_' ::= {{ com Default kinding or typing assumption }} {{ aux _ l }} % {{ aux _ annot }} {{ auxparam 'a }} - | default base_kind id :: :: kind + | default base_kind var :: :: 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 diff --git a/src/initial_check.ml b/src/initial_check.ml index 772df3e9..18a853d9 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -10,8 +10,15 @@ type 'a envs_out = 'a * envs let id_to_string (Id_aux(id,l)) = match id with | Id(x) | DeIid(x) -> x +let var_to_string (Var_aux(Var v,l)) = v + (*placeholder, write in type_internal*) -let kind_to_string _ = " kind pp place holder " +let kind_to_string kind = match kind.k with + | K_Nat -> "Nat" + | K_Typ -> "Type" + | K_Ord -> "Order" + | K_Efct -> "Effects" + | _ -> " kind pp place holder " let typquant_to_quantkinds k_env typquant = match typquant with @@ -25,29 +32,33 @@ let typquant_to_quantkinds k_env typquant = | QI_const _ -> rst | QI_id(ki) -> begin match ki with - | KOpt_aux(KOpt_none(id),l) | KOpt_aux(KOpt_kind(_,id),l) -> - (match Envmap.apply k_env (id_to_string id) with + | KOpt_aux(KOpt_none(v),l) | KOpt_aux(KOpt_kind(_,v),l) -> + (match Envmap.apply k_env (var_to_string v) with | Some(typ) -> typ::rst | None -> raise (Reporting_basic.err_unreachable l "Envmap didn't get an entry during typschm processing")) end) qlist []) -let typ_error l msg opt_id opt_kind = +let typ_error l msg opt_id opt_var opt_kind = raise (Reporting_basic.err_typ l (msg ^ - (match opt_id, opt_kind with - | Some(id),Some(kind) -> (id_to_string id) ^ " of " ^ (kind_to_string kind) - | Some(id),None -> ": " ^ (id_to_string id) - | None,Some(kind) -> " " ^ (kind_to_string kind) - | None,None -> ""))) + (match opt_id, opt_var, opt_kind with + | Some(id),None,Some(kind) -> (id_to_string id) ^ " of " ^ (kind_to_string kind) + | Some(id),None,None -> ": " ^ (id_to_string id) + | None,Some(v),Some(kind) -> "'" ^ (var_to_string v) ^ " of " ^ (kind_to_string kind) + | None,Some(v),None -> ": '" ^ (var_to_string v) + | None,None,Some(kind) -> " " ^ (kind_to_string kind) + | _ -> ""))) let to_ast_id (Parse_ast.Id_aux(id,l)) = Id_aux( (match id with | Parse_ast.Id(x) -> Id(x) | Parse_ast.DeIid(x) -> DeIid(x)) , l) +let to_ast_var (Parse_ast.Var_aux(Parse_ast.Var v,l)) = Var_aux(Var v,l) + let to_ast_base_kind (Parse_ast.BK_aux(k,l')) = match k with | Parse_ast.BK_type -> BK_aux(BK_type,l'), { k = K_Typ} @@ -65,7 +76,7 @@ let to_ast_kind (k_env : kind Envmap.t) (Parse_ast.K_aux(Parse_ast.K_kind(klst), let ret,args = List.hd reverse_typs, List.rev (List.tl reverse_typs) in match ret.k with | K_Typ -> K_aux(K_kind(List.map fst k_pairs), l), { k = K_Lam(args,ret) } - | _ -> typ_error l "Type constructor must have an -> kind ending in Type" None None + | _ -> typ_error l "Type constructor must have an -> kind ending in Type" None None None let rec to_ast_typ (k_env : kind Envmap.t) (t: Parse_ast.atyp) : Ast.typ = match t with @@ -76,10 +87,19 @@ let rec to_ast_typ (k_env : kind Envmap.t) (t: Parse_ast.atyp) : Ast.typ = let mk = Envmap.apply k_env (id_to_string id) in (match mk with | Some(k) -> (match k.k with - | K_Typ -> Typ_var id - | K_infer -> k.k <- K_Typ; Typ_var id - | _ -> typ_error l "Required a variable with kind Type, encountered " (Some id) (Some k)) - | None -> typ_error l "Encountered an unbound variable" (Some id) None) + | K_Typ -> Typ_id id + | K_infer -> k.k <- K_Typ; Typ_id id + | _ -> typ_error l "Required an identifier with kind Type, encountered " (Some id) None (Some k)) + | None -> typ_error l "Encountered an unbound identifier" (Some id) None None) + | Parse_ast.ATyp_var(v) -> + let v = to_ast_var v in + let mk = Envmap.apply k_env (var_to_string v) in + (match mk with + | Some(k) -> (match k.k with + | K_Typ -> Typ_var v + | K_infer -> k.k <- K_Typ; Typ_var v + | _ -> typ_error l "Required a variable with kind Type, encountered " None (Some v) (Some k)) + | None -> typ_error l "Encountered an unbound variable" None (Some v) None) | Parse_ast.ATyp_wild -> Typ_wild | Parse_ast.ATyp_fn(arg,ret,efct) -> Typ_fn( (to_ast_typ k_env arg), (to_ast_typ k_env ret), @@ -93,10 +113,10 @@ let rec to_ast_typ (k_env : kind Envmap.t) (t: Parse_ast.atyp) : Ast.typ = if ((List.length args) = (List.length typs)) then Typ_app(id,(List.map2 (fun k a -> (to_ast_typ_arg k_env k a)) args typs)) - else typ_error l "Type constructor given incorrect number of arguments" (Some id) None - | None -> typ_error l "Required a type constructor, encountered an unbound variable" (Some id) None - | _ -> typ_error l "Required a type constructor, encountered a base kind variable" (Some id) None) - | _ -> typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None + else typ_error l "Type constructor given incorrect number of arguments" (Some id) None None + | None -> typ_error l "Required a type constructor, encountered an unbound identifier" (Some id) None None + | _ -> typ_error l "Required a type constructor, encountered a base kind variable" (Some id) None None) + | _ -> typ_error l "Required an item of kind Type, encountered an illegal form for this kind" None None None ), l) and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp = @@ -110,8 +130,17 @@ and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp = | Some(k) -> Nexp_aux((match k.k with | K_Nat -> Nexp_id id | K_infer -> k.k <- K_Nat; Nexp_id id - | _ -> typ_error l "Required a variable with kind Nat, encountered " (Some id) (Some k)),l) - | None -> typ_error l "Encountered an unbound variable" (Some id) None) + | _ -> typ_error l "Required a variable with kind Nat, encountered " (Some id) None (Some k)),l) + | None -> typ_error l "Encountered an unbound variable" (Some id) None None) + | Parse_ast.ATyp_var(v) -> + let v = to_ast_var v in + let mk = Envmap.apply k_env (var_to_string v) in + (match mk with + | Some(k) -> Nexp_aux((match k.k with + | K_Nat -> Nexp_var v + | K_infer -> k.k <- K_Nat; Nexp_var v + | _ -> typ_error l "Required a variable with kind Nat, encountered " None (Some v) (Some k)),l) + | None -> typ_error l "Encountered an unbound variable" None (Some v) None) | Parse_ast.ATyp_constant(i) -> Nexp_aux(Nexp_constant(i),l) | Parse_ast.ATyp_sum(t1,t2) -> let n1 = to_ast_nexp k_env t1 in @@ -128,7 +157,7 @@ and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp = (Nexp_aux((Nexp_times(n1,n2)),l))) (*TODO This needs just a portion of the l, think about adding a way to split*) in times_loop typs false - | _ -> typ_error l "Requred an item of kind Nat, encountered an illegal form for this kind" None None) + | _ -> typ_error l "Requred an item of kind Nat, encountered an illegal form for this kind" None None None) and to_ast_order (k_env : kind Envmap.t) (o: Parse_ast.atyp) : Ast.order = match o with @@ -141,11 +170,20 @@ and to_ast_order (k_env : kind Envmap.t) (o: Parse_ast.atyp) : Ast.order = | Some(k) -> (match k.k with | K_Ord -> Ord_id id | K_infer -> k.k <- K_Ord; Ord_id id - | _ -> typ_error l "Required a variable with kind Order, encountered " (Some id) (Some k)) - | None -> typ_error l "Encountered an unbound variable" (Some id) None) + | _ -> typ_error l "Required an identifier with kind Order, encountered " (Some id) None (Some k)) + | None -> typ_error l "Encountered an unbound identifier" (Some id) None None) + | Parse_ast.ATyp_var(v) -> + let v = to_ast_var v in + let mk = Envmap.apply k_env (var_to_string v) in + (match mk with + | Some(k) -> (match k.k with + | K_Ord -> Ord_var v + | K_infer -> k.k <- K_Ord; Ord_var v + | _ -> typ_error l "Required a variable with kind Order, encountered " None (Some v) (Some k)) + | None -> typ_error l "Encountered an unbound variable" None (Some v) None) | Parse_ast.ATyp_inc -> Ord_inc | Parse_ast.ATyp_dec -> Ord_dec - | _ -> typ_error l "Requred an item of kind Order, encountered an illegal form for this kind" None None + | _ -> typ_error l "Requred an item of kind Order, encountered an illegal form for this kind" None None None ), l) and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effects = @@ -157,10 +195,19 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effects = let mk = Envmap.apply k_env (id_to_string id) in (match mk with | Some(k) -> (match k.k with - | K_Efct -> Effects_var id - | K_infer -> k.k <- K_Efct; Effects_var id - | _ -> typ_error l "Required a variable with kind Effect, encountered " (Some id) (Some k)) - | None -> typ_error l "Encountered an unbound variable" (Some id) None) + | K_Efct -> Effects_id id + | K_infer -> k.k <- K_Efct; Effects_id id + | _ -> typ_error l "Required a variable with kind Effect, encountered " (Some id) None (Some k)) + | None -> typ_error l "Encountered an unbound variable" (Some id) None None) + | Parse_ast.ATyp_efvar(v) -> + let v = to_ast_var v in + let mk = Envmap.apply k_env (var_to_string v) in + (match mk with + | Some(k) -> (match k.k with + | K_Efct -> Effects_var v + | K_infer -> k.k <- K_Efct; Effects_var v + | _ -> typ_error l "Required a variable with kind Effect, encountered " None (Some v) (Some k)) + | None -> typ_error l "Encountered an unbound variable" None (Some v) None) | Parse_ast.ATyp_set(effects) -> Effects_set( List.map (fun efct -> match efct with @@ -174,7 +221,7 @@ and to_ast_effects (k_env : kind Envmap.t) (e : Parse_ast.atyp) : Ast.effects = | Parse_ast.Effect_unspec -> Effect_unspec | Parse_ast.Effect_nondet -> Effect_nondet),l)) effects) - | _ -> typ_error l "Required an item of kind Effects, encountered an illegal form for this kind" None None + | _ -> typ_error l "Required an item of kind Effects, encountered an illegal form for this kind" None None None ), l) and to_ast_typ_arg (k_env : kind Envmap.t) (kind : kind) (arg : Parse_ast.atyp) : Ast.typ_arg = @@ -211,26 +258,26 @@ let to_ast_nexp_constraint (k_env : kind Envmap.t) (c : Parse_ast.nexp_constrain (* Transforms a typquant while building first the kind environment of declared variables, and also the kind environment in context *) let to_ast_typquant (k_env: kind Envmap.t) (tq : Parse_ast.typquant) : typquant * kind Envmap.t * kind Envmap.t = let opt_kind_to_ast k_env local_names local_env (Parse_ast.KOpt_aux(ki,l)) = - let id, key, kind, ktyp = + let v, key, kind, ktyp = match ki with - | Parse_ast.KOpt_none(id) -> - let id = to_ast_id id in - let key = id_to_string id in + | Parse_ast.KOpt_none(v) -> + let v = to_ast_var v in + let key = var_to_string v in let kind,ktyp = if (Envmap.in_dom key k_env) then None,(Envmap.apply k_env key) else None,(Some{ k = K_infer }) in - id,key,kind, ktyp - | Parse_ast.KOpt_kind(k,id) -> - let id = to_ast_id id in - let key = id_to_string id in + v,key,kind, ktyp + | Parse_ast.KOpt_kind(k,v) -> + let v = to_ast_var v in + let key = var_to_string v in let kind,ktyp = to_ast_kind k_env k in - id,key,Some(kind),Some(ktyp) + v,key,Some(kind),Some(ktyp) in if (Nameset.mem key local_names) - then typ_error l "Encountered duplicate name in type scheme" (Some id) None + then typ_error l "Encountered duplicate name in type scheme" None (Some v) None else let local_names = Nameset.add key local_names in let kopt,k_env,k_env_local = (match kind,ktyp with - | Some(k),Some(kt) -> KOpt_kind(k,id), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt)) - | None, Some(kt) -> KOpt_none(id), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt)) + | Some(k),Some(kt) -> KOpt_kind(k,v), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt)) + | None, Some(kt) -> KOpt_none(v), (Envmap.insert k_env (key,kt)), (Envmap.insert local_env (key,kt)) | _ -> raise (Reporting_basic.err_unreachable l "Envmap in dom is true but apply gives None")) in KOpt_aux(kopt,l),k_env,local_names,local_env in @@ -354,11 +401,11 @@ and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp) | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),[exp]) -> (match f with | Parse_ast.Id(id) -> LEXP_memory(to_ast_id f',to_ast_exp k_env exp) - | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None) + | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None) | Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env vexp, to_ast_exp k_env exp) | Parse_ast.E_vector_subrange(vexp,exp1,exp2) -> LEXP_vector_range(to_ast_lexp k_env vexp, to_ast_exp k_env exp1, to_ast_exp k_env exp2) | Parse_ast.E_field(fexp,id) -> LEXP_field(to_ast_lexp k_env fexp, to_ast_id id) - | _ -> typ_error l "Only identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None) + | _ -> typ_error l "Only identifiers, vector accesses, vector slices, and fields can be on the lefthand side of an assignment" None None None) , (l,None)) and to_ast_case (k_env : kind Envmap.t) (Parse_ast.Pat_aux(pex,l) : Parse_ast.pexp) : tannot pexp = @@ -376,7 +423,7 @@ and to_ast_fexps (fail_on_error : bool) (k_env : kind Envmap.t) (exps : Parse_as | _ -> None) | None,Some(l,msg) -> if fail_on_error - then typ_error l msg None None + then typ_error l msg None None None else None | _ -> None) @@ -399,11 +446,11 @@ let to_ast_default (names, k_env, t_env) (default : Parse_ast.default_typing_spe match default with | Parse_ast.DT_aux(df,l) -> (match df with - | Parse_ast.DT_kind(bk,id) -> + | Parse_ast.DT_kind(bk,v) -> let k,k_typ = to_ast_base_kind bk in - let id = to_ast_id id in - let key = id_to_string id in - DT_aux(DT_kind(k,id),(l,None)),(names,(Envmap.insert k_env (key,k_typ)),t_env) + let v = to_ast_var v in + let key = var_to_string v in + DT_aux(DT_kind(k,v),(l,None)),(names,(Envmap.insert k_env (key,k_typ)),t_env) | Parse_ast.DT_typ(typschm,id) -> let tps,_,_ = to_ast_typschm k_env typschm in DT_aux(DT_typ(tps,to_ast_id id),(l,None)),(names,k_env,t_env) (* Does t_env need to be updated here in this pass? *) @@ -418,7 +465,10 @@ let to_ast_spec (names,k_env,t_env) (val_:Parse_ast.val_spec) : (tannot val_spec VS_aux(VS_val_spec(typsch,to_ast_id id),(l,None)),(names,k_env,t_env) | Parse_ast.VS_extern_spec(ts,id,s) -> let typsch,_,_ = to_ast_typschm k_env ts in - VS_aux(VS_extern_spec(typsch,to_ast_id id,s),(l,None)),(names,k_env,t_env))(*Do names and t_env need updating this pass? *) + VS_aux(VS_extern_spec(typsch,to_ast_id id,s),(l,None)),(names,k_env,t_env) + | Parse_ast.VS_extern_no_rename(ts,id) -> + let typsch,_,_ = to_ast_typschm k_env ts in + VS_aux(VS_extern_no_rename(typsch,to_ast_id id),(l,None)),(names,k_env,t_env))(*Do names and t_env need updating this pass? *) let to_ast_namescm (Parse_ast.Name_sect_aux(ns,l)) = @@ -567,21 +617,21 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out * (match (def_in_progress id partial_defs) with | None -> let partial_def = ref ((DEF_aux(DEF_fundef(FD_aux(FD_function(rec_opt,tannot,effects_opt,[]),(l,None))),(l,None))),false) in (No_def,envs),((id,(partial_def,k_local))::partial_defs) - | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None) + | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None None) | Parse_ast.DEF_scattered_funcl(funcl) -> (match funcl with | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_,_),_) -> let id = to_ast_id id in (match (def_in_progress id partial_defs) with - | None -> typ_error l "Scattered function definition clause does not match any exisiting function definition headers" (Some id) None + | None -> typ_error l "Scattered function definition clause does not match any exisiting function definition headers" (Some id) None None | Some(d,k) -> (match !d with | DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),dl),false -> let funcl = to_ast_funcl (names,Envmap.union k k_env,t_env) funcl in d:= (DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[funcl]),fl)),dl),false); (No_def,envs),partial_defs - | _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None - | _ -> typ_error l "Scattered function definition clause matches an existing scattered type definition header" (Some id) None))) + | _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None None + | _ -> typ_error l "Scattered function definition clause matches an existing scattered type definition header" (Some id) None None))) | Parse_ast.DEF_scattered_variant(id,naming_scheme_opt,typquant) -> let id = to_ast_id id in let name = to_ast_namescm naming_scheme_opt in @@ -589,24 +639,24 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out * (match (def_in_progress id partial_defs) with | None -> let partial_def = ref ((DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,None))),(l,None))),false) in (Def_place_holder(id,l),envs),(id,(partial_def,k_env'))::partial_defs - | Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None) + | Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None) | Parse_ast.DEF_scattered_unioncl(id,typ,arm_id) -> let id = to_ast_id id in let arm_id = to_ast_id arm_id in (match (def_in_progress id partial_defs) with - | None -> typ_error l "Scattered type definition clause does not match any existing type definition headers" (Some id) None + | None -> typ_error l "Scattered type definition clause does not match any existing type definition headers" (Some id) None None | Some(d,k) -> (match !d with | (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)),dl), false) -> let typ = to_ast_typ k typ in d:= (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms@[Tu_aux(Tu_ty_id (typ,arm_id), l)],false),tl)),dl),false); (No_def,envs),partial_defs - | _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None - | _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None)) + | _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None + | _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None None)) | Parse_ast.DEF_scattered_end(id) -> let id = to_ast_id id in (match (def_in_progress id partial_defs) with - | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None + | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None None | Some(d,k) -> (match !d with | (DEF_aux(DEF_type(_),_) as def),false -> @@ -616,7 +666,7 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out * d:= (def,true); ((Finished def), envs),partial_defs | _, true -> - typ_error l "Scattered definition ended multiple times" (Some id) None + typ_error l "Scattered definition ended multiple times" (Some id) None None | _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type"))) ) @@ -633,14 +683,14 @@ let rec to_ast_defs_helper envs partial_defs = function | Some(d,k) -> if (snd !d) then (fst !d) :: defs, envs, partial_defs - else typ_error l "Scattered type definition never ended" (Some id) None)) + else typ_error l "Scattered type definition never ended" (Some id) None None)) let to_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (typ_env : t Envmap.t) (Parse_ast.Defs(defs)) = let defs,_,partial_defs = to_ast_defs_helper (default_names,kind_env,typ_env) [] defs in List.iter (fun (id,(d,k)) -> (match !d with - | (DEF_aux(_,(l,_)),false) -> typ_error l "Scattered definition never ended" (Some id) None + | (DEF_aux(_,(l,_)),false) -> typ_error l "Scattered definition never ended" (Some id) None None | (_, true) -> ())) partial_defs; (Defs defs) diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml index 940a43bb..622bdbaa 100644 --- a/src/lem_interp/run_interp.ml +++ b/src/lem_interp/run_interp.ml @@ -92,6 +92,6 @@ let run (name, test) = eprintf "%s: action returned %s\n" name (val_to_string return); loop env' (resume test s return) | Error e -> eprintf "%s: error: %s\n" name e in - let entry = E_app(E_id(Id "main"), [E_lit L_unit]) in + let entry = E_app((Id "main"), [E_lit L_unit]) in loop (Reg.empty, Mem.empty) (interp test entry) ;; diff --git a/src/lexer.mll b/src/lexer.mll index 52be6084..80fd06f4 100644 --- a/src/lexer.mll +++ b/src/lexer.mll @@ -66,6 +66,7 @@ let kw_table = ("clause", (fun _ -> Clause)); ("const", (fun _ -> Const)); ("default", (fun _ -> Default)); + ("deinfix", (fun _ -> Deinfix)); ("effect", (fun _ -> Effect)); ("Effects", (fun _ -> Effects)); ("end", (fun _ -> End)); diff --git a/src/parser.mly b/src/parser.mly index ba796347..572408ea 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -243,8 +243,10 @@ id: tid: | TyId { (idl (Id($1))) } + +tyvar: | TyVar - { (idl (Id($1))) } + { (Var_aux((Var($1)),loc ())) } atomic_kind: | TYPE @@ -299,6 +301,8 @@ effect_typ: atomic_typ: | tid { tloc (ATyp_id $1) } + | tyvar + { tloc (ATyp_var $1) } | effect_typ { $1 } | Inc @@ -319,6 +323,10 @@ vec_typ: { tloc (make_vector_sugar (ATyp_aux ((ATyp_id $1), locn 1 1)) $3) } | tid Lsquare nexp_typ Colon nexp_typ Rsquare { tloc (make_vector_sugar_bounded (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) } + | tyvar Lsquare nexp_typ Rsquare + { tloc (make_vector_sugar (ATyp_aux ((ATyp_var $1), locn 1 1)) $3) } + | tyvar Lsquare nexp_typ Colon nexp_typ Rsquare + { tloc (make_vector_sugar_bounded (ATyp_aux ((ATyp_var $1), locn 1 1)) $3 $5) } app_typs: | vec_typ @@ -397,8 +405,8 @@ atomic_pat: { ploc P_wild } | Lparen pat As id Rparen { ploc (P_as($2,$4)) } - | Lparen Lparen typ Rparen atomic_pat Rparen - { ploc (P_typ($3,$5)) } + | Lparen typ Rparen atomic_pat + { ploc (P_typ($2,$4)) } | id { ploc (P_app($1,[])) } | Lcurly fpats Rcurly @@ -844,13 +852,13 @@ funcl_ands: /* This causes ambiguity because without a type quantifier it's unclear whether the first id is a function name or a type name for the optional types.*/ fun_def: - | Function_ Rec typquant atomic_typ effect_typ funcl_ands + | Function_ Rec typquant typ effect_typ funcl_ands { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) } - | Function_ Rec typquant atomic_typ funcl_ands + | Function_ Rec typquant typ funcl_ands { funloc (FD_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) } - | Function_ Rec atomic_typ effect_typ funcl_ands + | Function_ Rec typ effect_typ funcl_ands { funloc (FD_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $4 4, $5)) } - | Function_ Rec atomic_typ funcl_ands + | Function_ Rec typ funcl_ands { match $3 with | ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) -> funloc (FD_function(mk_rec 2,mk_tannotn (), mk_eannot $3 3, $4)) @@ -860,9 +868,9 @@ fun_def: { funloc (FD_function(mk_rec 2, mk_tannotn (), mk_eannotn (), $3)) } */ | Function_ typquant atomic_typ effect_typ funcl_ands { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) } - | Function_ typquant atomic_typ funcl_ands + | Function_ typquant typ funcl_ands { funloc (FD_function(mk_recn (), mk_tannot $2 $3 2 2, mk_eannotn (), $4)) } - | Function_ atomic_typ funcl_ands + | Function_ typ funcl_ands { match $2 with | ATyp_aux(ATyp_efid _, _) | ATyp_aux(ATyp_set _, _) -> funloc (FD_function(mk_recn (),mk_tannotn (), mk_eannot $2 2, $3)) @@ -873,9 +881,9 @@ fun_def: */ val_spec: - | Val typquant atomic_typ id + | Val typquant typ id { vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4)) } - | Val atomic_typ id + | Val typ id { vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3)) } | Val Extern typquant atomic_typ id { vloc (VS_extern_no_rename (mk_typschm $3 $4 3 4,$5)) } @@ -887,9 +895,9 @@ val_spec: { vloc (VS_extern_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, $6)) } kinded_id: - | tid + | tyvar { kiloc (KOpt_none $1) } - | kind tid + | kind tyvar { kiloc (KOpt_kind($1,$2))} /*kinded_ids: @@ -1020,12 +1028,12 @@ type_def: { tdloc (TD_enum($2, mk_namesectn (), $6,false)) } | Typedef id name_sect Eq Enumerate Lcurly enum_body Rcurly { tdloc (TD_enum($2,$3,$7,false)) } - | Typedef id Eq Register Bits Lsquare typ Colon typ Rsquare Lcurly r_def_body Rcurly + | Typedef id Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly { tdloc (TD_register($2, $7, $9, $12)) } default_typ: - | Default atomic_kind id + | Default atomic_kind tyvar { defloc (DT_kind($2,$3)) } | Default typquant atomic_typ id { defloc (DT_typ((mk_typschm $2 $3 2 3),$4)) } @@ -1033,13 +1041,13 @@ default_typ: { defloc (DT_typ((mk_typschm (mk_typqn ()) $2 2 2),$3)) } scattered_def: - | Function_ Rec typquant atomic_typ effect_typ id + | Function_ Rec typquant typ effect_typ id { (DEF_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannot $5 5, $6)) } - | Function_ Rec atomic_typ effect_typ id + | Function_ Rec typ effect_typ id { (DEF_scattered_function(mk_rec 2, mk_tannot (mk_typqn ()) $3 3 3, mk_eannot $4 4, $5)) } - | Function_ Rec typquant atomic_typ id + | Function_ Rec typquant typ id { (DEF_scattered_function(mk_rec 2, mk_tannot $3 $4 3 4, mk_eannotn (), $5)) } - | Function_ Rec atomic_typ id + | Function_ Rec typ id { match $3 with | (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) -> (DEF_scattered_function(mk_rec 2, mk_tannotn (), mk_eannot $3 3, $4)) @@ -1047,13 +1055,13 @@ scattered_def: (DEF_scattered_function(mk_rec 2,mk_tannot (mk_typqn ()) $3 3 3, mk_eannotn (), $4)) } | Function_ Rec id { (DEF_scattered_function(mk_rec 2,mk_tannotn (), mk_eannotn (),$3)) } - | Function_ typquant atomic_typ effect_typ id + | Function_ typquant typ effect_typ id { (DEF_scattered_function(mk_recn (),mk_tannot $2 $3 2 3, mk_eannot $4 4, $5)) } - | Function_ atomic_typ effect_typ id + | Function_ typ effect_typ id { (DEF_scattered_function(mk_recn (), mk_tannot (mk_typqn ()) $2 2 2, mk_eannot $3 3, $4)) } - | Function_ typquant atomic_typ id + | Function_ typquant typ id { (DEF_scattered_function(mk_recn (), mk_tannot $2 $3 2 3, mk_eannotn (), $4)) } - | Function_ atomic_typ id + | Function_ typ id { match $2 with | (ATyp_aux(ATyp_efid _, _)) | (ATyp_aux(ATyp_set _, _)) -> (DEF_scattered_function(mk_recn (), mk_tannotn (), mk_eannot $2 2, $3)) diff --git a/src/pre_parser.mly b/src/pre_parser.mly index fe59603f..e9c38ebd 100644 --- a/src/pre_parser.mly +++ b/src/pre_parser.mly @@ -64,25 +64,29 @@ id: | Id { $1 } -scan: +id_found: | Typedef id { $2 } - | Scattered Typedef id - { $3 } - | id scan - { $2 } - | Other scan - { $2 } + +skip: + | Scattered + { () } + | id + { () } + | Other + { () } scan_file: - | scan + | id_found { [$1] } - | scan scan_file + | skip + { [] } + | id_found scan_file { $1::$2 } + | skip scan_file + { $2 } file: | scan_file Eof { $1 } - | Other Eof - { [] } diff --git a/src/pretty_print.ml b/src/pretty_print.ml index dd5a792b..083bd087 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -50,10 +50,14 @@ let pp_parens is_atomic format = let pp_format_id (Id_aux(i,_)) = match i with | Id(i) -> i - | DeIid(x) -> "(:" ^ x ^ ")" + | DeIid(x) -> "(deinfix " ^ x ^ ")" let pp_id ppf id = base ppf (pp_format_id id) +let pp_format_var (Var_aux(Var v,_)) = "'" ^ v + +let pp_var ppf var = base ppf (pp_format_var var) + let pp_format_bkind (BK_aux(k,_)) = match k with | BK_type -> "Type" @@ -70,7 +74,8 @@ let pp_kind ppf k = base ppf (pp_format_kind k) let rec pp_format_typ (Typ_aux(t,_)) = match t with - | Typ_var(id) -> pp_format_id id + | Typ_id(id) -> pp_format_id id + | Typ_var(var) -> pp_format_var var | Typ_wild -> "_" | Typ_fn(arg,ret,efct) -> "(" ^ (parens is_atomic_typ pp_format_typ arg) ^ " -> " ^ (parens is_atomic_typ pp_format_typ ret) ^ " " ^ @@ -80,6 +85,7 @@ let rec pp_format_typ (Typ_aux(t,_)) = and pp_format_nexp (Nexp_aux(n,_)) = match n with | Nexp_id(id) -> pp_format_id id + | Nexp_var(var) -> pp_format_var var | Nexp_constant(i) -> string_of_int i | Nexp_sum(n1,n2) -> "(" ^ (pp_format_nexp n1) ^ " + " ^ (pp_format_nexp n2) ^ ")" | Nexp_times(n1,n2) -> "(" ^ (pp_format_nexp n1) ^ " * " ^ (pp_format_nexp n2) ^ ")" @@ -87,11 +93,13 @@ and pp_format_nexp (Nexp_aux(n,_)) = and pp_format_ord (Ord_aux(o,_)) = match o with | Ord_id(id) -> pp_format_id id + | Ord_var(var) -> pp_format_var var | Ord_inc -> "inc" | Ord_dec -> "dec" and pp_format_effects (Effects_aux(e,_)) = match e with - | Effects_var(id) -> "effect " ^ pp_format_id id + | Effects_id(id) -> "effect " ^ pp_format_id id + | Effects_var(var) -> "effect " ^ pp_format_var var | Effects_set(efcts) -> if (efcts = []) then "pure" @@ -137,8 +145,8 @@ let pp_format_qi (QI_aux(qi,_)) = | QI_const(n_const) -> pp_format_nexp_constraint n_const | QI_id(KOpt_aux(ki,_)) -> (match ki with - | KOpt_none(id) -> pp_format_id id - | KOpt_kind(k,id) -> pp_format_kind k ^ " " ^ pp_format_id id) + | KOpt_none(var) -> pp_format_var var + | KOpt_kind(k,var) -> pp_format_kind k ^ " " ^ pp_format_var var) let pp_qi ppf qi = base ppf (pp_format_qi qi) @@ -259,13 +267,14 @@ and pp_lexp ppf (LEXP_aux(lexp,_)) = let pp_default ppf (DT_aux(df,_)) = match df with - | DT_kind(bk,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "default" pp_bkind bk pp_id id + | DT_kind(bk,var) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "default" pp_bkind bk pp_var var | DT_typ(ts,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "default" pp_typscm ts pp_id id let pp_spec ppf (VS_aux(v,_)) = match v with | VS_val_spec(ts,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "val" pp_typscm ts pp_id id | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>%a %a %a %a %a \"%s\"@]@\n" kwd "val" kwd "extern" pp_typscm ts pp_id id kwd "=" s + | VS_extern_no_rename(ts,id) -> fprintf ppf "@[<0>%a %a %a %a@]@\n" kwd "val" kwd "extern" pp_typscm ts pp_id id let pp_namescm ppf (Name_sect_aux(ns,_)) = match ns with @@ -352,6 +361,10 @@ let pp_format_id_lem (Id_aux(i,_)) = let pp_lem_id ppf id = base ppf (pp_format_id_lem id) +let pp_format_var_lem (Var_aux(Var v,_)) = "(Var \"" ^ v ^ "\")" + +let pp_lem_var ppf var = base ppf (pp_format_var_lem var) + let pp_format_bkind_lem (BK_aux(k,_)) = match k with | BK_type -> "BK_type" @@ -368,7 +381,8 @@ let pp_lem_kind ppf k = base ppf (pp_format_kind_lem k) let rec pp_format_typ_lem (Typ_aux(t,_)) = match t with - | Typ_var(id) -> "(Typ_var " ^ pp_format_id_lem id ^ ")" + | Typ_id(id) -> "(Typ_id " ^ pp_format_id_lem id ^ ")" + | Typ_var(var) -> "(Typ_var " ^ pp_format_var_lem var ^ ")" | Typ_fn(arg,ret,efct) -> "(Typ_fn " ^ pp_format_typ_lem arg ^ " " ^ pp_format_typ_lem ret ^ " " ^ (pp_format_effects_lem efct) ^ ")" @@ -378,6 +392,7 @@ let rec pp_format_typ_lem (Typ_aux(t,_)) = and pp_format_nexp_lem (Nexp_aux(n,_)) = match n with | Nexp_id(id) -> "(Nexp_id " ^ pp_format_id_lem id ^ ")" + | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")" | Nexp_constant(i) -> "(Nexp_constant " ^ string_of_int i ^ ")" | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")" | Nexp_times(n1,n2) -> "(Nexp_times " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")" @@ -385,11 +400,13 @@ and pp_format_nexp_lem (Nexp_aux(n,_)) = and pp_format_ord_lem (Ord_aux(o,_)) = match o with | Ord_id(id) -> "(Ord_id " ^ pp_format_id_lem id ^ ")" + | Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")" | Ord_inc -> "Ord_inc" | Ord_dec -> "Ord_dec" and pp_format_effects_lem (Effects_aux(e,_)) = match e with - | Effects_var(id) -> "(Effects_var " ^ pp_format_id id ^ ")" + | Effects_id(id) -> "(Effects_id " ^ pp_format_id id ^ ")" + | Effects_var(v) -> "(Effects_var " ^ pp_format_var v ^ ")" | Effects_set(efcts) -> "(Effects_set [" ^ (list_format "; " @@ -434,8 +451,8 @@ let pp_format_qi_lem (QI_aux(qi,_)) = | QI_id(KOpt_aux(ki,_)) -> "(QI_id " ^ (match ki with - | KOpt_none(id) -> "(KOpt_none " ^ pp_format_id_lem id ^ ")" - | KOpt_kind(k,id) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_id_lem id ^ ")") ^ ")" + | KOpt_none(var) -> "(KOpt_none " ^ pp_format_var_lem var ^ ")" + | KOpt_kind(k,var) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_var_lem var ^ ")") ^ ")" let pp_lem_qi ppf qi = base ppf (pp_format_qi_lem qi) @@ -558,13 +575,14 @@ and pp_lem_lexp ppf (LEXP_aux(lexp,_)) = let pp_lem_default ppf (DT_aux(df,_)) = match df with - | DT_kind(bk,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_id id + | DT_kind(bk,var) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_var var | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id let pp_lem_spec ppf (VS_aux(v,_)) = match v with | VS_val_spec(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>(%a %a %a \"%s\")@]@\n" kwd "VS_extern_spec" pp_lem_typscm ts pp_lem_id id s + | VS_extern_no_rename(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_extern_no_rename" pp_lem_typscm ts pp_lem_id id let pp_lem_namescm ppf (Name_sect_aux(ns,_)) = match ns with @@ -589,8 +607,8 @@ let pp_lem_typdef ppf (TD_aux(td,_)) = | TD_variant(id,nm,typq,ar,_) -> let a_pp ppf (Tu_aux(typ_u,_)) = match typ_u with - | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_ty_id %a %a)@]" pp_lem_typ typ pp_lem_id id - | Tu_id(id) -> fprintf ppf "@[<1>(Tu_id %a)@]" pp_id id + | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_ty_id %a %a);@]" pp_lem_typ typ pp_lem_id id + | Tu_id(id) -> fprintf ppf "@[<1>(Tu_id %a);@]" pp_lem_id id in fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar diff --git a/src/process_file.ml b/src/process_file.ml index 35a84b21..b07caca4 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -62,6 +62,7 @@ let get_lexbuf fn = let parse_file (f : string) : Parse_ast.defs = let scanbuf = get_lexbuf f in + let default_type_names = ["bool";"unit";"vector";"enum";"list";"bit";"nat"] in let type_names = try Pre_parser.file Pre_lexer.token scanbuf @@ -73,14 +74,14 @@ let parse_file (f : string) : Parse_ast.defs = raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m))) | Lexer.LexError(s,p) -> raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) in - let _ = Lexer.type_names != ref type_names in + let _ = Lexer.type_names := (default_type_names@type_names) in let lexbuf = get_lexbuf f in try Parser.file Lexer.token lexbuf with | Parsing.Parse_error -> let pos = Lexing.lexeme_start_p lexbuf in - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, ""))) + raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "main"))) | Parse_ast.Parse_error_locn(l,m) -> raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m))) | Lexer.LexError(s,p) -> diff --git a/src/test/test1.sail b/src/test/test1.sail index e7828483..dfb8ac8f 100644 --- a/src/test/test1.sail +++ b/src/test/test1.sail @@ -1,14 +1,14 @@ -(*default Nat i -default Order o +default Nat 'i +default Order 'o default bool b -default forall 'a. (list 'a) b +default forall 'a. (list<'a>) b val forall 'a, 'b . (('a * 'b) -> 'b pure) snd val forall Type 'i, 'b. (('i * 'b) -> 'i pure) fst -typedef int_list [name = "il"] = list nat +typedef int_list [name = "il"] = list typedef reco = const struct forall 'i, 'a, 'b. { ('a['i]) v; 'b w; } -typedef maybe = const union forall 'a. { unit None; a Some; } +typedef maybe = const union forall 'a. { Nne; 'a Sme; } typedef colors = enumerate { red; green; blue } -typedef creg = register bits [5:i] { 5 : h ; 6..7 : j} +typedef creg = register bits [5:'i] { 5 : h ; 6..7 : j} let bool e = true -function unit main _ = ()*) +function unit main _ = () \ No newline at end of file diff --git a/src/test/test3.sail b/src/test/test3.sail index 4a216467..30513bc9 100644 --- a/src/test/test3.sail +++ b/src/test/test3.sail @@ -8,9 +8,9 @@ val ( ( nat * nat ) -> nat effect { wmem , rmem } ) MEM_SIZE (* extern functions *) val extern ( ( nat * nat ) -> nat pure ) add = "add" -val extern ( ( nat * nat ) -> nat pure ) (: + ) = "add_infix" (* infix plus *) +val extern ( ( nat * nat ) -> nat pure ) (deinfix + ) = "add_infix" (* infix plus *) -function nat (: * ) ( < nat > x, < nat > y ) = 42 +function nat (deinfix * ) ( (nat) x, (nat) y ) = 42 function nat main _ = { (* left-hand side function call = memory write *) -- cgit v1.2.3