diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/Makefile | 10 | ||||
| -rw-r--r-- | language/l2.ml | 481 | ||||
| -rw-r--r-- | language/l2.ott | 645 | ||||
| -rw-r--r-- | language/l2_parse2.ott | 1424 | ||||
| -rw-r--r-- | language/l2_rules.ott | 1565 | ||||
| -rw-r--r-- | language/sil.ott | 451 |
6 files changed, 2521 insertions, 2055 deletions
diff --git a/language/Makefile b/language/Makefile index 9167d65f..081d90a7 100644 --- a/language/Makefile +++ b/language/Makefile @@ -4,7 +4,7 @@ OTT=../../../github/ott/src/ott OTTLIB=$(dir $(shell which ott))../hol .PHONY: all -all: l2.ml l2_parse.ml l2.lem +all: l2.ml l2_parse.ml l2.lem l2_parse2.ml l2_parse2_parser.mly docs: l2.pdf l2_parse.pdf @@ -18,7 +18,7 @@ type_system.pdf: doc_in.tex type_system.tex pdflatex type_system.tex pdflatex type_system.tex -l2.tex: l2.ott l2_terminals_non_tt.ott l2_typ.ott l2_rules.ott +l2.tex: l2.ott l2_rules.ott # l2_terminals_non_tt.ott l2_typ.ott l2_rules.ott $(OTT) -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^ doc_in.tex: l2.ott primitive_doc.ott l2_terminals_tt.ott l2_typ.ott l2_rules.ott @@ -36,6 +36,12 @@ doc_in.tex: l2.ott primitive_doc.ott l2_terminals_tt.ott l2_typ.ott l2_rules.ott l2.lem: l2.ott $(OTT) -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^ +ROOT=l2_parse2 +# generate the ocaml AST type, ocamllex lexer, menhir parser, and ocaml pretty printers for the AST, all from the Ott soruce +$(ROOT)_ast.ml $(ROOT)_lexer.mll $(ROOT)_parser.mly $(ROOT)_parser_pp.ml $(ROOT)_ast.tex : $(ROOT).ott Makefile + $(OTT) -quotient_rules false -generate_aux_rules false -i $(ROOT).ott -o $(ROOT)_parser.mly -o $(ROOT)_lexer.mll -o $(ROOT)_ast.ml -o $(ROOT).tex + + clean: rm -rf *~ rm -rf *.uo *.ui *.sig *.sml .HOLMK diff --git a/language/l2.ml b/language/l2.ml index 13cb2567..c59ce838 100644 --- a/language/l2.ml +++ b/language/l2.ml @@ -1,18 +1,33 @@ -(* generated by Ott 0.25 from: l2.ott *) +(* generated by Ott 0.26 from: l2.ott *) +type text = string + +type l = Parse_ast.l + type 'a annot = l * 'a +type loop = While | Until + -type x = string (* identifier *) -type ix = string (* infix identifier *) +type x = text (* identifier *) +type ix = text (* infix identifier *) type base_kind_aux = (* base kind *) BK_type (* kind of types *) | BK_nat (* kind of natural number size expressions *) | BK_order (* kind of vector order specifications *) - | BK_effect (* kind of effect sets *) + + +type +base_kind = + BK_aux of base_kind_aux * Parse_ast.l + + +type +kind_aux = (* kinds *) + K_kind of (base_kind) list type @@ -21,14 +36,14 @@ kid_aux = (* kinded IDs: $_$, $_$, $_$, and $_$ variables *) type -id_aux = (* identifier *) +id_aux = (* Identifier *) Id of x | DeIid of x (* remove infix status *) type -base_kind = - BK_aux of base_kind_aux * Parse_ast.l +kind = + K_aux of kind_aux * Parse_ast.l type @@ -42,31 +57,6 @@ id = type -kind_aux = (* kinds *) - K_kind of (base_kind) list - - -type -nexp_aux = (* numeric expression, of kind $_$ *) - Nexp_id of id (* abbreviation identifier *) - | Nexp_var of kid (* variable *) - | Nexp_constant of int (* constant *) - | Nexp_times of nexp * nexp (* product *) - | Nexp_sum of nexp * nexp (* sum *) - | Nexp_minus of nexp * nexp (* subtraction *) - | Nexp_exp of nexp (* exponential *) - | Nexp_neg of nexp (* for internal use only *) - -and nexp = - Nexp_aux of nexp_aux * Parse_ast.l - - -type -kind = - K_aux of kind_aux * Parse_ast.l - - -type base_effect_aux = (* effect *) BE_rreg (* read register *) | BE_wreg (* write register *) @@ -88,6 +78,21 @@ base_effect_aux = (* effect *) type +nexp_aux = (* numeric expression, of kind $_$ *) + Nexp_id of id (* abbreviation identifier *) + | Nexp_var of kid (* variable *) + | Nexp_constant of int (* constant *) + | Nexp_times of nexp * nexp (* product *) + | Nexp_sum of nexp * nexp (* sum *) + | Nexp_minus of nexp * nexp (* subtraction *) + | Nexp_exp of nexp (* exponential *) + | Nexp_neg of nexp (* for internal use only *) + +and nexp = + Nexp_aux of nexp_aux * Parse_ast.l + + +type base_effect = BE_aux of base_effect_aux * Parse_ast.l @@ -116,27 +121,30 @@ effect = type -n_constraint_aux = (* constraint over kind $_$ *) - NC_fixed of nexp * nexp - | NC_bounded_ge of nexp * nexp - | NC_bounded_le of nexp * nexp - | NC_nat_set_bounded of kid * (int) list - - -type kinded_id_aux = (* optionally kind-annotated identifier *) KOpt_none of kid (* identifier *) | KOpt_kind of kind * kid (* kind-annotated variable *) type -n_constraint = - NC_aux of n_constraint_aux * Parse_ast.l +kinded_id = + KOpt_aux of kinded_id_aux * Parse_ast.l type -kinded_id = - KOpt_aux of kinded_id_aux * Parse_ast.l +n_constraint_aux = (* constraint over kind $_$ *) + NC_equal of nexp * nexp + | NC_bounded_ge of nexp * nexp + | NC_bounded_le of nexp * nexp + | NC_not_equal of nexp * nexp + | NC_set of kid * (int) list + | NC_or of n_constraint * n_constraint + | NC_and of n_constraint * n_constraint + | NC_true + | NC_false + +and n_constraint = + NC_aux of n_constraint_aux * Parse_ast.l type @@ -146,19 +154,23 @@ quant_item_aux = (* kinded identifier or $_$ constraint *) type -quant_item = - QI_aux of quant_item_aux * Parse_ast.l - - -type -typquant_aux = (* type quantifiers and constraints *) - TypQ_tq of (quant_item) list - | TypQ_no_forall (* empty *) +lit_aux = (* literal constant *) + L_unit (* $() : _$ *) + | L_zero (* $_ : _$ *) + | L_one (* $_ : _$ *) + | L_true (* $_ : _$ *) + | L_false (* $_ : _$ *) + | L_num of int (* natural number constant *) + | L_hex of string (* bit vector constant, C-style *) + | L_bin of string (* bit vector constant, C-style *) + | L_string of string (* string constant *) + | L_undef (* undefined-value constant *) + | L_real of string type -typquant = - TypQ_aux of typquant_aux * Parse_ast.l +quant_item = + QI_aux of quant_item_aux * Parse_ast.l type @@ -168,6 +180,7 @@ typ_aux = (* type expressions, of kind $_$ *) | Typ_var of kid (* type variable *) | Typ_fn of typ * typ * effect (* Function (first-order only in user code) *) | Typ_tup of (typ) list (* Tuple *) + | Typ_exist of (kid) list * n_constraint * typ | Typ_app of id * (typ_arg) list (* type constructor application *) and typ = @@ -177,49 +190,20 @@ and typ_arg_aux = (* type constructor arguments of all kinds *) Typ_arg_nexp of nexp | Typ_arg_typ of typ | Typ_arg_order of order - | Typ_arg_effect of effect and typ_arg = Typ_arg_aux of typ_arg_aux * Parse_ast.l type -lit_aux = (* literal constant *) - L_unit (* $() : _$ *) - | L_zero (* $_ : _$ *) - | L_one (* $_ : _$ *) - | L_true (* $_ : _$ *) - | L_false (* $_ : _$ *) - | L_num of int (* natural number constant *) - | L_hex of string (* bit vector constant, C-style *) - | L_bin of string (* bit vector constant, C-style *) - | L_string of string (* string constant *) - | L_undef (* undefined-value constant *) - - -type -typschm_aux = (* type scheme *) - TypSchm_ts of typquant * typ - - -type -index_range_aux = (* index specification, for bitfields in register types *) - BF_single of int (* single index *) - | BF_range of int * int (* index range *) - | BF_concat of index_range * index_range (* concatenation of index ranges *) - -and index_range = - BF_aux of index_range_aux * Parse_ast.l - - -type lit = L_aux of lit_aux * Parse_ast.l type -typschm = - TypSchm_aux of typschm_aux * Parse_ast.l +typquant_aux = (* type quantifiers and constraints *) + TypQ_tq of (quant_item) list + | TypQ_no_forall (* empty *) type @@ -229,13 +213,14 @@ type | P_as of 'a pat * id (* named pattern *) | P_typ of typ * 'a pat (* typed pattern *) | P_id of id (* identifier *) + | P_var of 'a pat * kid (* bind pattern to type variable *) | P_app of id * ('a pat) list (* union constructor pattern *) | P_record of ('a fpat) list * bool (* struct pattern *) | P_vector of ('a pat) list (* vector pattern *) - | P_vector_indexed of ((int * 'a pat)) list (* vector pattern (with explicit indices) *) | P_vector_concat of ('a pat) list (* concatenated vector pattern *) | P_tup of ('a pat) list (* tuple pattern *) | P_list of ('a pat) list (* list pattern *) + | P_cons of 'a pat * 'a pat (* Cons patterns *) and 'a pat = P_aux of 'a pat_aux * 'a annot @@ -248,6 +233,11 @@ and 'a fpat = type +typquant = + TypQ_aux of typquant_aux * Parse_ast.l + + +type name_scm_opt_aux = (* optional variable naming-scheme constraint *) Name_sect_none | Name_sect_some of string @@ -260,6 +250,11 @@ type_union_aux = (* type union constructors *) type +typschm_aux = (* type scheme *) + TypSchm_ts of typquant * typ + + +type name_scm_opt = Name_sect_aux of name_scm_opt_aux * Parse_ast.l @@ -270,17 +265,27 @@ type_union = type +typschm = + TypSchm_aux of typschm_aux * Parse_ast.l + + +type +index_range_aux = (* index specification, for bitfields in register types *) + BF_single of int (* single index *) + | BF_range of int * int (* index range *) + | BF_concat of index_range * index_range (* concatenation of index ranges *) + +and index_range = + BF_aux of index_range_aux * Parse_ast.l + + +type 'a kind_def_aux = (* Definition body for elements of kind *) KD_nabbrev of kind * id * name_scm_opt * nexp (* $_$-expression abbreviation *) - | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *) - | KD_record of kind * id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *) - | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *) - | KD_enum of kind * id * name_scm_opt * (id) list * bool (* enumeration type definition *) - | KD_register of kind * id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *) type -'a type_def_aux = (* type definition body *) +type_def_aux = (* type definition body *) TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *) | TD_record of id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *) | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* tagged union type definition *) @@ -293,146 +298,8 @@ type KD_aux of 'a kind_def_aux * 'a annot -type -'a type_def = - TD_aux of 'a type_def_aux * 'a annot - - -type -ne = (* internal numeric expressions *) - Ne_id of x - | Ne_var of x - | Ne_const of int - | Ne_inf - | Ne_mult of ne * ne - | Ne_add of (ne) list - | Ne_minus of ne * ne - | Ne_exp of ne - | Ne_unary of ne - - -type -t = (* Internal types *) - T_id of x - | T_var of x - | T_fn of t * t * effect - | T_tup of (t) list - | T_app of x * t_args - | T_abbrev of t * t - -and t_arg = (* Argument to type constructors *) - T_arg_typ of t - | T_arg_nexp of ne - | T_arg_effect of effect - | T_arg_order of order - -and t_args = (* Arguments to type constructors *) - T_args of (t_arg) list - - -type -k = (* Internal kinds *) - Ki_typ - | Ki_nat - | Ki_ord - | Ki_efct - | Ki_ctor of (k) list * k - | Ki_infer (* Representing an unknown kind, inferred by context *) - - -type -tid = (* A type identifier or type variable *) - Tid_id of id - | Tid_var of kid - - -type -kinf = (* Whether a kind is default or from a local binding *) - Kinf_k of k - | Kinf_def of k - - -type -nec = (* Numeric expression constraints *) - Nec_lteq of ne * ne - | Nec_eq of ne * ne - | Nec_gteq of ne * ne - | Nec_in of x * (int) list - | Nec_cond of (nec) list * (nec) list - | Nec_branch of (nec) list - - -type -tag = (* Data indicating where the identifier arises and thus information necessary in compilation *) - Tag_empty - | Tag_intro (* Denotes an assignment and lexp that introduces a binding *) - | Tag_set (* Denotes an expression that mutates a local variable *) - | Tag_tuple_assign (* Denotes an assignment with a tuple lexp *) - | Tag_global (* Globally let-bound or enumeration based value/variable *) - | Tag_ctor (* Data constructor from a type union *) - | Tag_extern of string option (* External function, specied only with a val statement *) - | Tag_default (* Type has come from default declaration, identifier may not be bound locally *) - | Tag_spec - | Tag_enum of int - | Tag_alias - | Tag_unknown of string option (* Tag to distinguish an unknown path from a non-analysis non deterministic path *) - - -type -tinf = (* Type variables, type, and constraints, bound to an identifier *) - Tinf_typ of t - | Tinf_quant_typ of e_k * s_N * tag * t - - -type -conformsto = (* how much conformance does overloading need *) - Conformsto_full - | Conformsto_parm - - -type -widennum = - Widennum_widen - | Widennum_dont - | Widennum_dontcare - - -type -widenvec = - Widenvec_widen - | Widenvec_dont - | Widenvec_dontcare - - -type -widening = (* Should we widen vector start locations, should we widen atoms and ranges *) - Widening_w of widennum * widenvec - - -type -tinflist = (* In place so that a list of tinfs can be referred to without the dot form *) - Tinfs_empty - | Tinfs_ls of (tinf) list - - -type -i = (* Information given by type checking an expression *) - I of s_N * effect - | Iempty (* Empty constraints, effect *) - | Singleunion of i * i - | Iunion of (i) list (* Unions the constraints and effect *) - - -type -e = (* Definition environment and lexical environment *) - E of e_t * e_d - | E_union of e * e - - -type -i_direction = - IInc - | IDec +type +'a type_def = TD_aux of type_def_aux * 'a annot type @@ -441,23 +308,6 @@ type type -ctor_kind = - C_Enum of nat - | C_Union - - -type -reg_form = - Form_Reg of id * tannot * i_direction - | Form_SubReg of id * reg_form * index_range - - -type -'a reg_id = - RI_aux of 'a reg_id_aux * 'a annot - - -type 'a exp_aux = (* expression *) E_block of ('a exp) list (* sequential block *) | E_nondet of ('a exp) list (* nondeterministic block *) @@ -468,6 +318,8 @@ type | E_app_infix of 'a exp * id * 'a exp (* infix function application *) | E_tuple of ('a exp) list (* tuple *) | E_if of 'a exp * 'a exp * 'a exp (* conditional *) + | E_loop of loop * 'a exp * 'a exp + | E_until of 'a exp * 'a exp | E_for of id * 'a exp * 'a exp * 'a exp * order * 'a exp (* loop *) | E_vector of ('a exp) list (* vector (indexed from 0) *) | E_vector_indexed of ((int * 'a exp)) list * 'a opt_default (* vector (indexed consecutively) *) @@ -484,10 +336,12 @@ type | E_case of 'a exp * ('a pexp) list (* pattern matching *) | E_let of 'a letbind * 'a exp (* let expression *) | E_assign of 'a lexp * 'a exp (* imperative assignment *) - | E_sizeof of nexp (* the value of nexp at run time *) - | E_return of 'a exp (* return 'a exp from current function *) + | E_sizeof of nexp (* the value of $nexp$ at run time *) + | E_return of 'a exp (* return $'a exp$ from current function *) | E_exit of 'a exp (* halt all current execution *) - | E_assert of 'a exp * 'a exp (* halt with error 'a exp when not 'a exp *) + | E_throw of 'a exp + | E_try of 'a exp * ('a pexp) list + | E_assert of 'a exp * 'a exp (* halt with error $'a exp$ when not $'a exp$ *) | E_internal_cast of 'a annot * 'a exp (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *) | E_internal_exp of 'a annot (* This is an internal use for passing nexp information to library functions, postponed for constraint solving *) | E_sizeof_internal of 'a annot (* For sizeof during type checking, to replace nexp with internal n *) @@ -497,25 +351,11 @@ type | E_internal_let of 'a lexp * 'a exp * 'a exp (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *) | E_internal_plet of 'a pat * 'a exp * 'a exp (* This is an internal node, used to distinguised some introduced lets during processing from original ones *) | E_internal_return of 'a exp (* For internal use to embed into monad definition *) - | E_internal_value of value (* For internal use in interpreter to wrap pre-evaluated values when returning an action *) + | E_constraint of n_constraint and 'a exp = E_aux of 'a exp_aux * 'a annot -and value = (* interpreter evaluated value *) - V_boxref of nat * t - | V_lit of lit - | V_tuple of (value) list - | V_list of (value) list - | V_vector of nat * i_direction * (value) list - | V_vector_sparse of nat * nat * i_direction * ((nat * value)) list * value - | V_record of t * ((id * value)) list - | V_ctor of id * t * ctor_kind * value - | V_unknown - | V_register of reg_form - | V_register_alias of tannot alias_spec * tannot - | V_track of value * reg_form_set - and 'a lexp_aux = (* lvalue expression *) LEXP_id of id (* identifier *) | LEXP_memory of id * ('a exp) list (* memory or register write via function call *) @@ -549,30 +389,21 @@ and 'a opt_default = and 'a pexp_aux = (* pattern match *) Pat_exp of 'a pat * 'a exp + | Pat_when of 'a pat * 'a exp * '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 (* let, explicit type ('a pat must be total) *) - | LB_val_implicit of 'a pat * 'a exp (* let, implicit type ('a pat must be total) *) + LB_val of 'a pat * 'a exp (* let, implicit type ($'a pat$ must be total) *) and 'a letbind = LB_aux of 'a letbind_aux * 'a annot -and 'a alias_spec_aux = (* register alias expression forms *) - AL_subreg of 'a reg_id * id - | AL_bit of 'a reg_id * 'a exp - | AL_slice of 'a reg_id * 'a exp * 'a exp - | AL_concat of 'a reg_id * 'a reg_id - -and 'a alias_spec = - AL_aux of 'a alias_spec_aux * 'a annot - type -'a funcl_aux = (* function clause *) - FCL_Funcl of id * 'a pat * 'a exp +'a reg_id = + RI_aux of 'a reg_id_aux * 'a annot type @@ -582,19 +413,28 @@ rec_opt_aux = (* optional recursive annotation for functions *) type +effect_opt_aux = (* optional effect annotation for functions *) + Effect_opt_pure (* sugar for empty effect set *) + | Effect_opt_effect of effect + + +type tannot_opt_aux = (* optional type annotation for functions *) - Typ_annot_opt_some of typquant * typ + Typ_annot_opt_none + | Typ_annot_opt_some of typquant * typ type -effect_opt_aux = (* optional effect annotation for functions *) - Effect_opt_pure (* sugar for empty effect set *) - | Effect_opt_effect of effect +'a funcl_aux = (* function clause *) + FCL_Funcl of id * 'a pat * 'a exp type -'a funcl = - FCL_aux of 'a funcl_aux * 'a annot +'a alias_spec_aux = (* register alias expression forms *) + AL_subreg of 'a reg_id * id + | AL_bit of 'a reg_id * 'a exp + | AL_slice of 'a reg_id * 'a exp * 'a exp + | AL_concat of 'a reg_id * 'a reg_id type @@ -603,25 +443,23 @@ rec_opt = type -tannot_opt = - Typ_annot_opt_aux of tannot_opt_aux * Parse_ast.l +effect_opt = + Effect_opt_aux of effect_opt_aux * Parse_ast.l type -effect_opt = - Effect_opt_aux of effect_opt_aux * Parse_ast.l +tannot_opt = + Typ_annot_opt_aux of tannot_opt_aux * Parse_ast.l type -'a val_spec_aux = (* value type specification *) - VS_val_spec of typschm * id (* specify the type of an upcoming definition *) - | VS_extern_no_rename of typschm * id (* specify the type of an external function *) - | VS_extern_spec of typschm * id * string (* specify the type of a function from Lem *) +'a funcl = + FCL_aux of 'a funcl_aux * 'a annot type -'a fundef_aux = (* function definition *) - FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list +'a alias_spec = + AL_aux of 'a alias_spec_aux * 'a annot type @@ -634,37 +472,38 @@ type type -'a default_spec_aux = (* default kinding or typing assumption *) - DT_order of order - | DT_kind of base_kind * kid - | DT_typ of typschm * id - - -type 'a dec_spec_aux = (* register declarations *) DEC_reg of typ * id | DEC_alias of id * 'a alias_spec | DEC_typ_alias of typ * id * 'a alias_spec +type +val_spec_aux = VS_val_spec of typschm * id * string option * bool + + type -'a val_spec = - VS_aux of 'a val_spec_aux * 'a annot +'a fundef_aux = (* function definition *) + FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list type -'a fundef = - FD_aux of 'a fundef_aux * 'a annot +default_spec_aux = (* default kinding or typing assumption *) + DT_order of order + | DT_kind of base_kind * kid + | DT_typ of typschm * id type -'a scattered_def = - SD_aux of 'a scattered_def_aux * 'a annot +prec = + Infix + | InfixL + | InfixR type -'a default_spec = - DT_aux of 'a default_spec_aux * Parse_ast.l +'a scattered_def = + SD_aux of 'a scattered_def_aux * 'a annot type @@ -672,6 +511,20 @@ type DEC_aux of 'a dec_spec_aux * 'a annot +type +'a val_spec = VS_aux of val_spec_aux * 'a annot + + +type +'a fundef = + FD_aux of 'a fundef_aux * 'a annot + + +type +default_spec = + DT_aux of default_spec_aux * Parse_ast.l + + type 'a dec_comm = (* top-level generated comments *) DC_comm of string (* generated unstructured comment *) @@ -683,7 +536,9 @@ and 'a def = (* top-level definition *) | DEF_fundef of 'a fundef (* function definition *) | DEF_val of 'a letbind (* value definition *) | DEF_spec of 'a val_spec (* top-level type constraint *) - | DEF_default of 'a default_spec (* default kind and type assumptions *) + | DEF_fixity of prec * int * id (* fixity declaration *) + | DEF_overload of id * (id) list (* operator overload specification *) + | DEF_default of default_spec (* default kind and type assumptions *) | DEF_scattered of 'a scattered_def (* scattered function and type definition *) | DEF_reg_dec of 'a dec_spec (* register declaration *) | DEF_comm of 'a dec_comm (* generated comments *) diff --git a/language/l2.ott b/language/l2.ott index c78c66f8..76fc0c77 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -1,3 +1,7 @@ +%% +%% Grammar for user language. Generates ./src/ast.ml +%% + indexvar n , m , i , j ::= {{ phantom }} {{ com Index variables for meta-lists }} @@ -5,13 +9,14 @@ indexvar n , m , i , j ::= metavar num,numZero,numOne ::= {{ phantom }} {{ lex numeric }} - {{ ocaml int }} + {{ ocaml big_int }} {{ hol num }} {{ lem integer }} {{ com Numeric literals }} metavar nat ::= {{ phantom }} + {{ ocaml int }} {{ lex numeric }} {{ lem nat }} @@ -27,7 +32,7 @@ metavar bin ::= {{ lex numeric }} {{ ocaml string }} {{ lem string }} - {{ com Bit vector literal, specified by C-style binary number }} + {{ com Bit vector literal, specified by C-style binary number }} metavar string ::= {{ phantom }} @@ -43,11 +48,26 @@ metavar regexp ::= {{ hol string }} {{ com Regular expresions, as a string literal }} +metavar real ::= + {{ phantom }} + {{ ocaml string }} + {{ lem string }} + {{ hol string }} + {{ com Real number literal }} + embed {{ ocaml +open Big_int + +type text = string + +type l = Parse_ast.l + type 'a annot = l * 'a +type loop = While | Until + }} embed @@ -72,10 +92,12 @@ val set_from_list : forall 'a. list 'a -> set 'a val subst : forall 'a. list 'a -> list 'a -> bool +type loop = While | Until + }} metavar x , y , z ::= - {{ ocaml string }} + {{ ocaml text }} {{ lem string }} {{ hol string }} {{ com identifier }} @@ -84,7 +106,7 @@ metavar x , y , z ::= metavar ix ::= {{ lex alphanum }} - {{ ocaml string }} + {{ ocaml text }} {{ lem string }} {{ hol string }} {{ com infix identifier }} @@ -112,7 +134,7 @@ annot :: '' ::= {{ hol unit }} id :: '' ::= - {{ com identifier }} + {{ com Identifier }} {{ aux _ l }} | x :: :: id | ( deinfix x ) :: D :: deIid {{ com remove infix status }} @@ -120,6 +142,7 @@ id :: '' ::= | 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") }} @@ -135,8 +158,21 @@ id :: '' ::= % 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. - +% 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 }} @@ -153,10 +189,10 @@ grammar base_kind :: 'BK_' ::= {{ com base kind}} {{ aux _ l }} - | Type :: :: type {{ com kind of types }} - | Nat :: :: nat {{ com kind of natural number size expressions }} + | Type :: :: type {{ com kind of types }} + | Nat :: :: nat {{ com kind of natural number size expressions }} | Order :: :: order {{ com kind of vector order specifications }} - | Effect :: :: effect {{ com kind of effect sets }} + kind :: 'K_' ::= {{ com kinds}} @@ -167,14 +203,15 @@ kind :: 'K_' ::= 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}} + | id :: :: id {{ com abbreviation identifier }} + | kid :: :: var {{ com variable }} + | num :: :: constant {{ com constant }} + | id ( nexp1 , ... , nexpn ) :: :: app {{ com app }} + | 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_' ::= @@ -231,8 +268,6 @@ grammar typ :: 'Typ_' ::= {{ com type expressions, of kind $[[Type]]$ }} {{ aux _ l }} - | _ :: :: wild - {{ com unspecified type }} | id :: :: id {{ com defined type }} | kid :: :: var @@ -243,6 +278,7 @@ typ :: 'Typ_' ::= % 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 }} @@ -258,11 +294,12 @@ typ :: 'Typ_' ::= % 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{|]} }} +{{ 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{|]} }} +{{ 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]] }} @@ -271,14 +308,13 @@ typ :: 'Typ_' ::= % not sure how first-class it should be, though % use "reg word32" etc for the types of vanilla registers - + typ_arg :: 'Typ_arg_' ::= {{ com type constructor arguments of all kinds }} {{ aux _ l }} | nexp :: :: nexp | typ :: :: typ | order :: :: order - | effect :: :: effect % plus more for l-value/r-value pairs, as introduced by the L3 'compound' declarations ... ref typ @@ -307,10 +343,15 @@ grammar n_constraint :: 'NC_' ::= {{ com constraint over kind $[[Nat]]$ }} {{ aux _ l }} - | nexp = nexp' :: :: fixed + | nexp = nexp' :: :: equal | nexp >= nexp' :: :: bounded_ge | nexp '<=' nexp' :: :: bounded_le - | kid 'IN' { num1 , ... , numn } :: :: nat_set_bounded + | 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 @@ -384,9 +425,13 @@ grammar %%% OR, IN C STYLE -type_def :: 'TD_' ::= +type_def {{ ocaml 'a type_def }} {{ lem type_def 'a }} :: 'TD_' ::= + {{ ocaml TD_aux of type_def_aux * 'a annot }} + {{ lem TD_aux of type_def_aux * annot 'a }} + | type_def_aux :: :: aux + +type_def_aux :: 'TD_' ::= {{ com type definition body }} - {{ aux _ annot }} {{ auxparam 'a }} | 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 @@ -412,17 +457,17 @@ kind_def :: 'KD_' ::= {{ aux _ annot }} {{ auxparam 'a }} | Def kind id name_scm_opt = nexp :: :: nabbrev {{ com $[[Nat]]$-expression abbreviation }} - | Def kind id name_scm_opt = typschm :: D :: abbrev - {{ com type abbreviation }} {{ texlong }} - | Def kind id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: D :: record - {{ com struct type definition }} {{ texlong }} - | Def kind id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: D :: variant - {{ com union type definition}} {{ texlong }} - | Def kind id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: D :: enum - {{ com enumeration type definition}} {{ texlong }} - - | Def kind id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn } -:: D :: register {{ com register mutable bitfield type definition }} {{ texlong }} +% | 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 }} @@ -467,7 +512,8 @@ lit :: 'L_' ::= % 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 }} @@ -503,11 +549,10 @@ pat :: 'P_' ::= % 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 }} @@ -525,8 +570,8 @@ pat :: 'P_' ::= | [ pat1 , .. , patn ] :: :: vector {{ com vector pattern }} - | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed - {{ com vector pattern (with explicit indices) }} +% | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed +% {{ com vector pattern (with explicit indices) }} % cf ntoes for this | pat1 : .... : patn :: :: vector_concat @@ -537,9 +582,9 @@ pat :: 'P_' ::= | [|| pat1 , .. , patn ||] :: :: list {{ com list pattern }} | ( pat ) :: S :: paren -{{ ichlo [[pat]] }} -% | pat1 '::' pat2 :: :: cons -% {{ com Cons patterns }} + {{ ichlo [[pat]] }} + | pat1 '::' pat2 :: :: cons + {{ com Cons patterns }} % XXX Is this still useful? fpat :: 'FP_' ::= @@ -580,37 +625,11 @@ let rec disjoint_all sets = end }} - -grammar - -k :: 'Ki_' ::= -{{ com Internal kinds }} - | K_Typ :: :: typ - | K_Nat :: :: nat - | K_Ord :: :: ord - | K_Efct :: :: efct - | K_Lam ( k0 .. kn -> k' ) :: :: ctor - | K_infer :: :: infer {{ com Representing an unknown kind, inferred by context }} - -t , u :: 'T_' ::= -{{ com Internal types }} - | x :: :: id - | ' x :: :: var - | t1 -> t2 effect :: :: fn - | ( t1 , .... , tn ) :: :: tup - | x < t_args > :: :: app - | t |-> t1 :: :: abbrev - | register < t_arg > :: S :: reg_app {{ ichlo T_app "register" [[t_arg]] }} - | range < ne ne' > :: S :: range_app {{ ichlo T_app "range" [[ [ ne ; ne' ] ]] }} - | atom < ne > :: S :: atom_app {{ ichlo T_app "atom" [ [[ne]] ] }} - | vector < ne ne' order t > :: S :: vector_app {{ ichlo T_app "vector" [[ [ ne; ne'; ord; t ] ]] }} - | list < t > :: S :: list_app {{ ichlo T_app "list" [[t]] }} - | reg < t > :: S :: box_app {{ ichlo T_app "reg" [[t]] }} - | implicit < ne > :: S :: implicit_app {{ ichlo T_app "implicit" [[ne]] }} - | bit :: S :: bit_typ {{ ichlo T_id "bit" }} - | string :: S :: string_typ {{ ichlo T_id "string" }} - | unit :: S :: unit_typ {{ ichlo T_id "unit" }} - | t [ t_arg1 / tid1 .. t_argn / tidn ] :: M :: subst {{ ichlo "todo" }} +grammar + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Interpreter specific things % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }} | x :: :: optx_x @@ -618,14 +637,13 @@ optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }} | :: :: optx_none {{ lem Nothing }} {{ ocaml None }} - -tag :: 'Tag_' ::= +tag :: 'Tag_' ::= {{ com Data indicating where the identifier arises and thus information necessary in compilation }} | None :: :: empty | Intro :: :: intro {{ com Denotes an assignment and lexp that introduces a binding }} | Set :: :: set {{ com Denotes an expression that mutates a local variable }} | Tuple :: :: tuple_assign {{ com Denotes an assignment with a tuple lexp }} - | Global :: :: global {{ com Globally let-bound or enumeration based value/variable }} + | Global :: :: global {{ com Globally let-bound or enumeration based value/variable }} | Ctor :: :: ctor {{ com Data constructor from a type union }} | Extern optx :: :: extern {{ com External function, specied only with a val statement }} | Default :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }} @@ -634,323 +652,66 @@ tag :: 'Tag_' ::= | Alias :: :: alias | Unknown_path optx :: :: unknown {{ com Tag to distinguish an unknown path from a non-analysis non deterministic path}} -ne :: 'Ne_' ::= - {{ com internal numeric expressions }} - | x :: :: id - | ' x :: :: var - | num :: :: const - | infinity :: :: inf - | ne1 * ne2 :: :: mult - | ne1 + ... + nen :: :: add - | ne1 - ne2 :: :: minus - | 2 ** ne :: :: exp - | ( - ne ) :: :: unary - | zero :: S :: zero - {{ ichlo (Ne_const 0) }} - | one :: S :: one - {{ ichlo (Ne_const 1) }} - | bitlength ( bin ) :: M :: cbin - {{ ocaml (asssert false) }} - {{ hol ARB }} - {{ lem (blength [[bin]]) }} - | bitlength ( hex ) :: M :: chex - {{ ocaml (assert false) }} - {{ hol ARB }} - {{ lem (hlength [[hex]]) }} - | count ( num0 ... numi ) :: M :: length {{ichlo "todo" }} - | length ( pat1 ... patn ) :: M :: cpat - {{ ocaml (assert false) }} - {{ hol ARB }} - {{ lem (Ne_const (List.length [[pat1...patn]])) }} - | length ( exp1 ... expn ) :: M :: cexp - {{ hol ARB }} - {{ ocaml (assert false) }} - {{ lem (Ne_const (List.length [[exp1...expn]])) }} - - t_arg :: 't_arg_' ::= - {{ com Argument to type constructors }} - | t :: :: typ - | ne :: :: nexp - | effect :: :: effect - | order :: :: order - | fresh :: M :: freshvar {{ ichlo T_arg (T_var "fresh") }} - - t_args :: '' ::= {{ lem list t_arg }} - {{ com Arguments to type constructors }} - | t_arg1 ... t_argn :: :: T_args - - nec :: 'Nec_' ::= - {{ com Numeric expression constraints }} - | ne <= ne' :: :: lteq - | ne = ne' :: :: eq - | ne >= ne' :: :: gteq - | ' x 'IN' { num1 , ... , numn } :: :: in - | nec0 .. necn -> nec'0 ... nec'm :: :: cond - | nec0 ... necn :: :: branch - -S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }} - {{ hol nec list }} - {{ lem list nec }} - {{ com nexp constraint lists }} - | { nec1 , .. , necn } :: :: Sn_concrete - {{ hol [[nec1 .. necn]] }} - {{ lem [[nec1 .. necn]] }} - | S_N1 u+ .. u+ S_Nn :: M :: SN_union - {{ hol (FOLDR FUNION FEMPTY [[S_N1..S_Nn]]) }} - {{ lem (List.foldr (++) [] [[S_N1..S_Nn]]) }} - {{ ocaml (assert false) }} - | consistent_increase ne1 ne'1 ... nen ne'n :: M :: SN_increasing - {{ com Generates constraints from pairs of constraints, where the first of each pair is always larger than the sum of the previous pair }} - {{ ocaml (assert false) }} - {{ ichl todo }} - | consistent_decrease ne1 ne'1 ... nen ne'n :: M :: SN_decreasing - {{ com Generates constraints from pairs of constraints, where the first of each pair is always smaller than the difference of the previous pair }} - {{ ocaml assert false }} - {{ ichl todo }} - | resolve ( S_N ) :: :: resolution - {{ lem [[S_N]] (* Write constraint solver *) }} - - - E_d {{ tex {\ottnt{E}^{\textsc{d} } } }} :: 'E_d_' ::= {{ phantom }} - {{ lem definition_env }} - {{ com Environments storing top level information, such as defined abbreviations, records, enumerations, and kinds }} - | < E_k , E_a , E_r , E_e > :: :: base - {{ hol arb }} - {{ lem (Denv [[E_k]] [[E_r]] [[E_e]]) }} - | empty :: :: empty - {{ hol arb }} - {{ lem DenvEmp }} - | E_d u+ E_d' :: :: union - {{ hol arb }} - {{ lem (denv_union [[E_d]] [[E_d']]) }} - - kinf :: 'kinf_' ::= - {{ com Whether a kind is default or from a local binding }} - | k :: :: k - | k default :: :: def - - tid :: 'tid_' ::= - {{ com A type identifier or type variable }} - | id :: :: id - | kid :: :: var - - E_k {{ tex {\ottnt{E}^{\textsc{k} } } }} :: 'E_k_' ::= {{ phantom }} - {{ hol (tid-> kinf) }} - {{ lem (map tid kinf) }} - {{ com Kind environments }} - | { tid1 |-> kinf1 , .. , tidn |-> kinfn } :: :: concrete - {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[tid1 kinf1 .. tidn kinfn]]) }} - {{ lem (List.foldr (fun (x,v) m -> Map.insert x v m) Map.empty [[tid1 kinf1 .. tidn kinfn]]) }} - | E_k1 u+ .. u+ E_kn :: M :: union - {{ com In a unioning kinf, {k default} u {k} results in {k} (i.e. the default is locally forgotten) }} - {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }} - {{ lem (List.foldr (union) Map.empty [[E_k1..E_kn]]) }} - {{ ocaml (assert false) }} - | E_k u- E_k1 .. E_kn :: M :: multi_set_minus - {{ hol arb }} - {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_k]])) - (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_k1..E_kn]]))))) }} - {{ ocaml assert false }} - - tinf :: 'tinf_' ::= - {{ com Type variables, type, and constraints, bound to an identifier }} - | t :: :: typ - | E_k , S_N , tag , t :: :: quant_typ - -tinflist :: 'tinfs_' ::= - {{ com In place so that a list of tinfs can be referred to without the dot form }} - | empty :: :: empty - | tinf1 ... tinfn :: :: ls - -conformsto :: 'conformsto_' ::= - {{ com how much conformance does overloading need }} - | full :: :: full - | parm :: :: parm - -widenvec :: 'widenvec_' ::= - | vectors :: :: widen - | none :: :: dont - | _ :: :: dontcare - -widennum :: 'widennum_' ::= - | nums :: :: widen - | none :: :: dont - | _ :: :: dontcare - -widening :: 'widening_' ::= - {{ com Should we widen vector start locations, should we widen atoms and ranges }} - | ( widennum , widenvec ) :: :: w - - E_a {{ tex \ottnt{E}^{\textsc{a} } }} :: 'E_a_' ::= {{ phantom }} - {{ hol tid |-> tinf}} - {{ lem map tid tinf }} - | { tid1 |-> tinf1 , .. , tidn |-> tinfn } :: :: concrete - | E_a1 u+ .. u+ E_an :: :: union - - field_typs :: 'FT_' ::= {{ phantom }} - {{ lem list (id * t) }} - {{ com Record fields }} - | id1 : t1 , .. , idn : tn :: :: fields - {{ lem [[id1 t1..idn tn]] }} - - E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::= {{ phantom }} - {{ hol (id*t) |-> tinf) }} - {{ lem map (list (id*t)) tinf }} - {{ com Record environments }} - | { { field_typs1 } |-> tinf1 , .. , { field_typsn } |-> tinfn } :: :: concrete - {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }} - {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[field_typs1 tinf1..field_typsn tinfn]]) }} - | E_r1 u+ .. u+ E_rn :: M :: union - {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }} - {{ lem (List.foldr (union) Map.empty [[E_r1..E_rn]]) }} - {{ ocaml (assert false) }} - - enumerate_map :: '' ::= {{ phantom }} - {{ lem (list (nat*id)) }} - | { num1 |-> id1 ... numn |-> idn } :: :: enum_map - {{ lem [[num1 id1...numn idn]] }} - - E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::= {{ phantom }} - {{ lem (map t (list (nat*id))) }} - {{ com Enumeration environments }} - | { t1 |-> enumerate_map1 , .. , tn |-> enumerate_mapn } :: :: base - {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[t1 enumerate_map1..tn enumerate_mapn]]) }} - | E_e1 u+ .. u+ E_en :: :: union - {{ lem (List.foldr (union) Map.empty [[E_e1..E_en]]) }} - - embed {{ lem - type definition_env = - | DenvEmp - | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id))) + +type tannot = maybe (typ * tag * list unit * effect * effect) }} -grammar +embed +{{ ocaml - E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::= {{ phantom }} - {{ hol (id |-> tinf) }} - {{ lem map id tinf }} - {{ com Type environments }} - | { id1 |-> tinf1 , .. , idn |-> tinfn } :: :: base - {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }} - {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[id1 tinf1 .. idn tinfn]]) }} - | { id |-> overload tinf conformsto : tinf1 , ... , tinfn } :: :: overload - | ( E_t1 u+ .... u+ E_tn ) :: M :: union - {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }} - {{ lem (List.foldr (union) Map.empty [[E_t1....E_tn]]) }} - {{ ocaml (assert false) }} - | u+ E_t1 .. E_tn :: M :: multi_union - {{ hol arb }} - {{ lem (List.foldr (union) Map.empty [[E_t1..E_tn]]) }} - {{ ocaml assert false }} - | E_t u- id1 .. idn :: M :: multi_set_minus - {{ hol arb }} - {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_t]])) - (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[id1..idn]]))))) }} - {{ ocaml assert false }} - | ( E_t1 inter .... inter E_tn ) :: M :: intersect - {{ hol arb }} - {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1....E_tn]]) }} - {{ ocaml (assert false) }} - | inter E_t1 .. E_tn :: M :: multi_inter - {{ hol arb }} - {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1..E_tn]]) }} - {{ ocaml assert false }} - - -ts :: ts_ ::= {{ phantom }} - {{ lem list t }} - | t1 , .. , tn :: :: lst +(* Interpreter specific things are just set to unit here *) +type tannot = unit -embed -{{ lem -let blength (bit) = Ne_const 8 -let hlength (bit) = Ne_const 8 - - type env = - | EnvEmp - | Env of (map id tinf) * definition_env - - type inf = - | Iemp - | Inf of (list nec) * effect - - val denv_union : definition_env -> definition_env -> definition_env - let denv_union de1 de2 = - match (de1,de2) with - | (DenvEmp,de2) -> de2 - | (de1,DenvEmp) -> de1 - | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) -> - Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2) - end - - val env_union : env -> env -> env - let env_union e1 e2 = - match (e1,e2) with - | (EnvEmp,e2) -> e2 - | (e1,EnvEmp) -> e1 - | ((Env te1 de1),(Env te2 de2)) -> - Env (te1 union te2) (denv_union de1 de2) - end - -let inf_union i1 i2 = - match (i1,i2) with - | (Iemp,i2) -> i2 - | (i1,Iemp) -> i1 - | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2)) - end - -let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*) +type reg_form_set = unit }} grammar +tannot :: '' ::= + {{ phantom }} + {{ ocaml unit }} + {{ lem tannot }} - E :: '' ::= - {{ hol ((string,env_body) fmaptree) }} - {{ lem env }} - {{ com Definition environment and lexical environment }} - | < E_t , E_d > :: :: E - {{ hol arb }} - {{ lem (Env [[E_t]] [[E_d]]) }} - | empty :: M :: E_empty - {{ hol arb }} - {{ lem EnvEmp }} - {{ ocaml assert false }} - | E u+ E' :: :: E_union - {{ lem (env_union [[E]] [[E']]) }} - - I :: '' ::= {{ lem inf }} - {{ com Information given by type checking an expression }} - | < S_N , effect > :: :: I - {{ lem (Inf [[S_N]] [[effect]]) }} - | Ie :: :: Iempty {{ com Empty constraints, effect }} {{ tex {\ottnt{I}_{\epsilon} } }} - {{ lem Iemp }} - | ( I1 u+ I2 ) :: :: singleunion {{ tex [[I1]] [[u+]] [[I2]] }} - | I1 u+ .. u+ In :: :: Iunion {{ com Unions the constraints and effect }} - {{ lem (List.foldr inf_union Iemp [[I1..In]]) }} - +i_direction :: 'I' ::= + | IInc :: :: Inc + | IDec :: :: Dec -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Expressions % -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +ctor_kind :: 'C_' ::= + | C_Enum nat :: :: Enum + | C_Union :: :: Union -embed -{{ lem +reg_form :: 'Form_' ::= + | Reg id tannot i_direction :: :: Reg + | SubReg id reg_form index_range :: :: SubReg -type tannot = maybe (t * tag * list nec * effect * effect) +reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }} -}} +alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }} -grammar -tannot :: '' ::= - {{ phantom }} - {{ ocaml tannot }} - {{ lem tannot }} +value :: 'V_' ::= {{ com interpreter evaluated value }} + | Boxref nat typ :: :: boxref + | Lit lit :: :: lit + | Tuple ( value1 , ... , valuen ) :: :: tuple + | List ( value1 , ... , valuen ) :: :: list + | Vector nat i_direction ( value1 , ... , valuen ) :: :: vector + | Vector_sparse nat' nat'' i_direction ( nat1 value1 , ... , natn valuen ) value' :: :: vector_sparse + | Record typ ( id1 value1 , ... , idn valuen ) :: :: record + | V_ctor id typ ctor_kind value1 :: :: ctor + | Unknown :: :: unknown + | Register reg_form :: :: register + | Register_alias alias_spec_tannot tannot :: :: register_alias + | Track value reg_form_set :: :: track +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Expressions % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +loop :: loop ::= {{ phantom }} + | while :: :: while + | until :: :: until exp :: 'E_' ::= {{ com expression }} @@ -987,7 +748,9 @@ exp :: 'E_' ::= {{ 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 ]] }} @@ -1000,9 +763,6 @@ exp :: 'E_' ::= % 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 @@ -1069,15 +829,17 @@ exp :: 'E_' ::= {{ com imperative assignment }} | sizeof nexp :: :: sizeof - {{ com the value of [[nexp]] at run time }} + {{ com the value of $[[nexp]]$ at run time }} - | return exp :: :: return {{ com return [[exp]] from current function }} + | 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]] }} + {{ 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 }} @@ -1088,38 +850,26 @@ exp :: 'E_' ::= | 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 ) :: I :: internal_return {{ com For internal use to embed into monad definition }} + | 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 +%i_direction :: 'I' ::= +% | IInc :: :: Inc +% | IDec :: :: Dec -ctor_kind :: 'C_' ::= - | C_Enum nat :: :: Enum - | C_Union :: :: Union +%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 :: 'Form_' ::= +% | Reg id tannot i_direction :: :: Reg +% | SubReg id reg_form index_range :: :: SubReg -reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }} +%reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }} -alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }} +%alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }} -value :: 'V_' ::= {{ com interpreter evaluated value }} - | Boxref nat t :: :: boxref - | Lit lit :: :: lit - | Tuple ( value1 , ... , valuen ) :: :: tuple - | List ( value1 , ... , valuen ) :: :: list - | Vector nat i_direction ( value1 , ... , valuen ) :: :: vector - | Vector_sparse nat' nat'' i_direction ( nat1 value1 , ... , natn valuen ) value' :: :: vector_sparse - | Record t ( id1 value1 , ... , idn valuen ) :: :: record - | V_ctor id t ctor_kind value1 :: :: ctor - | Unknown :: :: unknown - | Register reg_form :: :: register - | Register_alias alias_spec_tannot tannot :: :: register_alias - | Track value reg_form_set :: :: track lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ aux _ annot }} {{ auxparam 'a }} @@ -1127,7 +877,7 @@ lexp :: 'LEXP_' ::= {{ com lvalue expression }} {{ 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]] }} +{{ com sugared form of above for explicit tuple $[[exp]]$ }} | ( typ ) id :: :: cast {{ com cast }} | ( lexp0 , .. , lexpn ) :: :: tup {{ com multiple (non-memory) assignment }} @@ -1156,7 +906,8 @@ opt_default :: 'Def_val_' ::= pexp :: 'Pat_' ::= {{ com pattern match }} {{ aux _ annot }} {{ auxparam 'a }} - | pat -> exp :: :: exp + | pat -> exp :: :: exp + | pat when exp1 -> exp :: :: when % apparently could use -> or => for this. %% % psexp :: 'Pats' ::= @@ -1233,7 +984,7 @@ grammar tannot_opt :: 'Typ_annot_opt_' ::= {{ com optional type annotation for functions}} {{ aux _ l }} -% | :: :: none + | :: :: 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 @@ -1270,27 +1021,34 @@ fundef :: 'FD_' ::= 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_implicit - {{ com let, implicit type ([[pat]] must be total)}} - - -val_spec :: 'VS_' ::= - {{ com value type specification }} - {{ aux _ annot }} {{ auxparam 'a }} - | val typschm id :: :: val_spec + | let pat = exp :: :: val + {{ com let, implicit type ($[[pat]]$ must be total)}} + +val_spec {{ ocaml 'a val_spec }} {{ lem val_spec 'a }} :: 'VS_' ::= + {{ ocaml VS_aux of val_spec_aux * 'a annot }} + {{ lem VS_aux of val_spec_aux * annot 'a }} + | val_spec_aux :: :: aux + +val_spec_aux :: 'VS_' ::= + {{ com value type specification }} + {{ ocaml VS_val_spec of typschm * id * (string -> string option) * bool }} + {{ lem VS_val_spec of typschm * id * maybe string * bool }} + | val typschm id :: S :: val_spec {{ com specify the type of an upcoming definition }} - | val extern typschm id :: :: extern_no_rename + {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} {{ lem }} + | val cast typschm id :: S :: cast + {{ ocaml (VS_val_spec [[typschm]] [[id]] None true) }} {{ lem }} + | val extern typschm id :: S :: extern_no_rename {{ com specify the type of an external function }} - | val extern typschm id = string :: :: extern_spec + {{ ocaml (VS_val_spec [[typschm]] [[id]] ([[Some id]]) false) }} {{ lem }} + | 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) }} {{ lem }} %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 }} {{ auxparam 'a }} + {{ aux _ l }} | default Order order :: :: order | default base_kind kid :: :: kind | default typschm id :: :: typ @@ -1346,6 +1104,11 @@ dec_comm :: 'DC_' ::= {{ com top-level generated comments }} {{auxparam 'a}} % Top-level definitions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +prec :: '' ::= + | infix :: :: Infix + | infixl :: :: InfixL + | infixr :: :: InfixR + def :: 'DEF_' ::= {{ com top-level definition }} {{ auxparam 'a }} @@ -1359,6 +1122,10 @@ def :: 'DEF_' ::= {{ 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 @@ -1367,6 +1134,8 @@ def :: 'DEF_' ::= {{ com register declaration }} | dec_comm :: I :: comm {{ com generated comments }} + | fundef1 .. fundefn :: I :: internal_mutrec + {{ com internal representation of mutually recursive functions }} defs :: '' ::= {{ com definition sequence }} @@ -1379,16 +1148,16 @@ terminals :: '' ::= | ** :: :: starstar {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} {{ com \texttt{**} }} -% | >= :: :: geq -% % {{ tex \ensuremath{\geq} }} + | >= :: :: geq + {{ tex \ensuremath{\geq} }} % {{ tex \ottsym{\textgreater=} }} % {{ com \texttt{>=} }} -% | '<=' :: :: leq -% % {{ tex \ensuremath{\leq} }} + | '<=' :: :: leq + {{ tex \ensuremath{\leq} }} % {{ tex \ottsym{\textless=} }} % {{ com \texttt{<=} }} -% | -> :: :: arrow -% % {{ tex \ensuremath{\rightarrow} }} + | -> :: :: arrow + {{ tex \ensuremath{\rightarrow} }} % {{ tex \ottsym{-\textgreater} }} % {{ com \texttt{->} }} | ==> :: :: Longrightarrow @@ -1415,10 +1184,10 @@ terminals :: '' ::= | emptyset :: :: emptyset {{ tex \ensuremath{\emptyset} }} % | < :: :: lt -% % {{ tex \ensuremath{\langle} }} + {{ tex \ensuremath{\langle} }} % {{ tex \ottsym{<} }} % | > :: :: gt -% % {{ tex \ensuremath{\rangle} }} + {{ tex \ensuremath{\rangle} }} % {{ tex \ottsym{>} }} | lt :: :: mathlt {{ tex < }} @@ -1472,5 +1241,3 @@ terminals :: '' ::= % {{ tex \mbox{$\ottsym{[\textbar\textbar}$} }} % | ||] :: :: list_end % {{ tex \mbox{$\ottsym{\textbar\textbar]}$} }} - - diff --git a/language/l2_parse2.ott b/language/l2_parse2.ott new file mode 100644 index 00000000..0f8dc8e7 --- /dev/null +++ b/language/l2_parse2.ott @@ -0,0 +1,1424 @@ +indexvar n , i , j , k ::= + {{ phantom }} + {{ com Index variables for meta-lists }} + +metavar num ::= + {{ phantom }} + {{ lex numeric }} + {{ ocaml int }} + {{ hol num }} + {{ lem integer }} + {{ com Numeric literals }} + {{ ocamllex ['0'-'9']+ }} + +metavar hex ::= + {{ phantom }} + {{ lex numeric }} + {{ ocaml string }} + {{ lem string }} +{{ ocamllex '0''x'['0'-'9' 'A' - 'F' 'a'-'f' '_']+ }} + {{ com Bit vector literal, specified by C-style hex number }} + +metavar bin ::= + {{ phantom }} + {{ lex numeric }} + {{ ocaml string }} + {{ lem string }} +{{ ocamllex '\'' ['0' '1' ' ']* '\'' }} + {{ com Bit vector literal, specified by C-style binary number }} + +metavar string ::= + {{ phantom }} + {{ ocaml string }} + {{ lem string }} + {{ hol string }} + {{ ocamllex "a" }} {{ phantom }} + {{ com String literals }} + +metavar regexp ::= + {{ phantom }} + {{ ocaml string }} + {{ lem string }} + {{ hol string }} + {{ ocamllex "a" }} {{ phantom }} + {{ com Regular expresions, as a string literal }} + +embed +{{ ocaml + +type l = + | Unknown + | Int of string * l option + | Generated of l + | Range of Lexing.position * Lexing.position + +type 'a annot = l * 'a + +exception Parse_error_locn of l * string + +}} + +embed +{{ lem +open import Map +open import Maybe +open import Pervasives + +type l = + | Unknown + | Trans of string * maybe l + | Range of nat * nat + +val duplicates : forall 'a. list 'a -> list 'a + +val union_map : forall 'a 'b. map 'a 'b -> map 'a 'b -> map 'a 'b + +val set_from_list : forall 'a. list 'a -> set 'a + +val subst : forall 'a. list 'a -> list 'a -> bool + +}} + +metavar x , y , z ::= + {{ ocaml string }} + {{ lem string }} + {{ hol string }} + {{ com identifier }} + {{ ocamlvar "[[x]]" }} + {{ lemvar "[[x]]" }} + {{ ocamllex "a" }} {{ phantom }} + +metavar ix ::= + {{ lex alphanum }} + {{ ocaml string }} + {{ lem string }} + {{ hol string }} + {{ com infix identifier }} + {{ ocamlvar "[[ix]]" }} + {{ lemvar "[[ix]]" }} + {{ ocamllex "a" }} {{ phantom }} + + +grammar + +l :: '' ::= {{ phantom }} + {{ ocaml l }} + {{ lem l }} + {{ hol unit }} + {{ com Source location }} + | :: :: Unknown + {{ ocaml Unknown }} + {{ lem Unknown }} + {{ hol () }} + + +id :: '' ::= + {{ com Identifier }} + {{ aux _ l }} + | x :: :: id + | op x :: :: deIid {{ com remove infix status }} + + +kid :: '' ::= + {{ com identifiers 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 +% 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. + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% 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 }} + | Effect :: :: effect {{ com kind of effect sets }} + +kind :: 'K_' ::= + {{ com kinds}} + {{ aux _ l }} + | base_kind1 -> ... -> base_kindn :: :: kind +% we'll never use ...-> Nat + +base_effect :: 'BE_' ::= + {{ com effect }} + {{ aux _ l }} + | rreg :: :: rreg {{ com read register }} + | wreg :: :: wreg {{ com write register }} + | rmem :: :: rmem {{ com read memory }} + | wmem :: :: wmem {{ com write memory }} + | wmv :: :: wmv {{ com write memory value }} + | eamem :: :: eamem {{ com address for write signaled }} + | barr :: :: barr {{ com memory barrier }} + | depend :: :: depend {{ com dynmically dependent footprint }} + | undef :: :: undef {{ com undefined-instruction exception }} + | unspec :: :: unspec {{ com unspecified values }} + | nondet :: :: nondet {{ com nondeterminism from intra-instruction parallelism }} + | escape :: :: escape + + + +atomic_typ :: 'ATyp_' ::= + {{ quotient-with atyp }} + | id :: :: id + | kid :: :: var + | num :: :: constant + | dec :: :: dec + | inc :: :: inc + | id ( atyp1 , ... , atypn ) :: :: app + | ( atyp ) :: S :: paren {{ ocaml [[atyp]] }} + | ( atyp1 , .... , atypn ) :: :: tup + | {| num_list |} :: S :: existential_set {{ ocaml + { let v = mk_kid "n" $startpos $endpos in + let atom_id = mk_id (Id "atom") $startpos $endpos in + let atom_of_v = mk_typ (ATyp_app (atom_id, [mk_typ (ATyp_var v) $startpos $endpos])) $startpos $endpos in + mk_typ (ATyp_exist ([v], NC_aux (NC_set (v, [[num_list]]), loc $startpos($2) $endpos($2)), atom_of_v)) $startpos $endpos } }} + | { kid_list . atyp } :: S :: existential_true {{ ocaml + { mk_typ (ATyp_exist ([[kid_list]], NC_aux (NC_true, loc $startpos $endpos), [[atyp]])) $startpos $endpos } }} + | { kid_list , nc . atyp } :: :: exist + | { base_effect1 , .. , base_effectn } :: :: set {{ com effect set }} + | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }} + + +atyp :: 'ATyp_' ::= + {{ com expressions of all kinds, to be translated to types, nats, orders, and effects after parsing }} + {{ aux _ l }} + | atomic_typ :: S :: atomic {{ ocaml [[atomic_typ]] }} {{ quotient-remove }} + | atyp1 * atyp2 :: :: times {{ com product }} + | atyp1 + atyp2 :: :: sum {{ com sum }} + | atyp1 - atyp2 :: :: minus {{ com subtraction }} + | 2** atyp :: :: exp {{ com exponential }} + | neg atyp :: :: neg {{ com Internal (but not M as I want a datatype constructor) negative nexp }} + | atyp1 -> atyp2 effect atyp3 :: :: fn + {{ com Function type (first-order only in user code), last atyp is an effect }} + + +% 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 +% | enum nexp1 nexp2 order :: :: enum {{ com natural numbers [[atyp2]] .. [[atyp2]]+[[atyp1]]-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 order atyp :: :: vector {{ com vector of [[atyp]], indexed by natural range }} +% probably some sugar for vector types, using [ ] similarly to enums: +% (but with .. not : in the former, to avoid confusion...) +% | atyp [ nexp ] :: :: vector2 {{ com sugar for vector indexed by [ [[atyp]] ] }} +% | atyp [ nexp : nexp' ] :: :: vector3 {{ com sugar for vector indexed by [ [[atyp]]..[[atyp']] ] }} +% ...so bit [ nexp ] etc is just an instance of that +% | list atyp :: :: list {{ com list of [[atyp]] }} +% | set atyp :: :: set {{ com finite set of [[atyp]] }} +% | reg atyp :: :: reg {{ com mutable register components holding [[atyp]] }} +% "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 + +% parsing +% +% ATyp_tup <= ATyp_tup +% ATyp_fn right ATyp_fn +% ATyp_fn <= ATyp_tup + +grammar + +n_constraint :: 'NC_' ::= + {{ com constraint over kind $[[Nat]]$ }} + {{ aux _ l }} + | atyp = atyp' :: :: fixed + | atyp >= atyp' :: :: bounded_ge + | atyp '<=' atyp' :: :: bounded_le + | kid 'IN' { num1 , ... , numn } :: :: nat_set_bounded + +% 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 Either a kinded identifier or a nexp constraint for a typquant }} + {{ aux _ l }} + | kinded_id :: :: id {{ com An optionally kinded identifier }} + | n_constraint :: :: const {{ com A constraint for this type }} + +typquant :: 'TypQ_' ::= + {{ com type quantifiers and constraints}} + {{ aux _ l }} + | forall quant_item1 , ... , quant_itemn . :: :: tq {{ texlong }} + | :: :: no_forall {{ com sugar, omitting quantifier and constraints }} + +typschm :: 'TypSchm_' ::= + {{ com type scheme }} + {{ aux _ l }} + | typquant atyp :: :: ts + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Type definitions % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +grammar +%ctor_def :: 'CT_' ::= +% {{ com Datatype constructor definition clause }} +% {{ aux _ l }} +% | id : typschm :: :: ct +% but we could get away with disallowing constraints in typschm, we +% think - if it's useful to do that + + name_scm_opt :: 'Name_sect_' ::= + {{ com Optional variable-naming-scheme specification for variables of defined type }} + {{ aux _ l }} + | :: :: none + | [ name = regexp ] :: :: some + +type_union :: 'Tu_' ::= + {{ com Type union constructors }} + {{ aux _ l }} + | id :: :: id + | atyp id :: :: ty_id + +type_def :: 'TD_' ::= + {{ com Type definition body }} + {{ aux _ l }} + | typedef id name_scm_opt = typschm :: :: abbrev + {{ com type abbreviation }} {{ texlong }} + | typedef id name_scm_opt = const struct typquant { atyp1 id1 ; ... ; atypn idn semi_opt } :: :: record + {{ com struct type definition }} {{ texlong }} + | typedef id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: :: variant + {{ com union type definition}} {{ texlong }} + | typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum + {{ com enumeration type definition}} {{ texlong }} + + | typedef id = register bits [ atyp : atyp' ] { index_range1 : id1 ; ... ; index_rangen : idn } +:: :: register {{ com register mutable bitfield type definition }} {{ texlong }} + +kind_def :: 'KD_' ::= + {{ com Definition body for elements of kind; many are shorthands for type\_defs }} + {{ aux _ l }} + | Def kind id name_scm_opt = typschm :: :: abbrev + {{ com type abbreviation }} {{ texlong }} + | Def kind id name_scm_opt = const struct typquant { atyp1 id1 ; ... ; atypn idn semi_opt } :: :: record + {{ com struct type definition }} {{ texlong }} + | Def kind id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: :: variant + {{ com union type definition}} {{ texlong }} + | Def kind id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum + {{ com enumeration type definition}} {{ texlong }} + + | Def kind id = register bits [ atyp : atyp' ] { index_range1 : id1 ; ... ; index_rangen : idn } +:: :: register {{ com register mutable bitfield type definition }} {{ texlong }} + + +% also sugar [ nexp ] + + +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 }} + | undefined :: :: undef {{ com undefined value }} + | string :: :: string {{ com string constant }} + +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 _ l }} + | lit :: :: lit + {{ com literal constant pattern }} + | _ :: :: wild + {{ com wildcard }} + | ( pat as id ) :: :: as + {{ com named pattern }} + | ( atyp ) pat :: :: typ + {{ com typed pattern }} + + | id :: :: id + {{ com identifier }} + + | id ( pat1 , .. , patn ) :: :: app + {{ com union constructor pattern }} + + | { fpat1 ; ... ; fpatn semi_opt } :: :: record + {{ com struct pattern }} + + | [ pat1 , .. , patn ] :: :: vector + {{ com vector pattern }} + + | [ num1 = pat1 , .. , numn = patn ] :: :: vector_indexed + {{ com vector pattern (with explicit indices) }} + + | 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]] }} + +fpat :: 'FP_' ::= + {{ com Field pattern }} + {{ aux _ l }} + | id = pat :: :: Fpat + +parsing +P_app <= P_app +P_app <= P_as + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Expressions % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + + +grammar + +exp :: 'E_' ::= + {{ com Expression }} + {{ aux _ l }} + + | { exp1 ; ... ; expn } :: :: block {{ com block (parsing conflict with structs?) }} +% maybe we really should have indentation-sensitive syntax :-) (given that some of the targets do) + + | nondet { exp1 ; ... ; expn } :: :: nondet {{ com block that can evaluate the contained expressions in any ordering }} + + | id :: :: id + {{ com identifier }} + + | lit :: :: lit + {{ com literal constant }} + + | ( atyp ) exp :: :: cast + {{ com cast }} + + + | id exp :: S :: tup_app {{ ichlo [[id]] ( [[exp]] ) }} {{ com No extra parens needed when exp is a tuple }} + | id ( exp1 , .. , expn ) :: :: app + {{ com function application }} +% 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 {{ icho [[ if exp1 then exp2 else unit ]] }} + + | foreach id from exp1 to exp2 by exp3 in atyp 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 {{ icho [[ foreach id from exp1 to exp2 by 1 exp4 ]] }} + | foreach id from exp1 downto exp2 by exp3 exp4 :: S :: fordown {{ icho [[ foreach id from exp1 to exp2 by ( - exp3 ) exp4 ]] }} + | foreach id from exp1 downto exp2 exp3 :: S :: fordownbyone {{ icho [[ foreach id from exp1 downto exp2 by 1 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 + + | [ exp1 , ... , 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 exp1 ; .. ; expn } :: :: 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 }} + | letbind in exp :: :: let + {{ com let expression }} + + | exp := exp' :: :: assign + {{ com imperative assignment }} + + | sizeof atyp :: :: sizeof + | exit exp :: :: exit + | return exp :: :: return + | assert ( exp , exp' ) :: :: assert + + | ( exp ) :: S :: paren {{ ichlo [[exp]] }} + + +lexp :: 'LEXP_' ::= {{ com lvalue expression, can't occur out of the parser }} + {{ aux _ l }} +% {{ aux _ annot }} {{ auxparam 'a }} + | id :: :: id + {{ com identifier }} + | id ( exp1 , .. , expn ) :: :: mem + | id exp :: S :: mem_tup {{ ichlo [[id (exp)]] }} + | lexp [ exp ] :: :: vector {{ com vector element }} + | lexp [ exp1 : exp2 ] :: :: vector_range {{ com subvector }} + % maybe comma-sep such lists too + | lexp . id :: :: field {{ com struct field }} + + +fexp :: 'FE_' ::= + {{ com Field-expression }} + {{ aux _ l }} +% {{ aux _ annot }} {{ auxparam 'a }} + | id = exp :: :: Fexp + +fexps :: 'FES_' ::= + {{ com Field-expression list }} + {{ aux _ l }} +% {{ aux _ annot }} {{ auxparam 'a }} + | fexp1 ; ... ; fexpn semi_opt :: :: Fexps + +opt_default :: 'Def_val_' ::= + {{ com Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map }} + {{ aux _ l }} + | :: :: empty + | ; default = exp :: :: dec + +pexp :: 'Pat_' ::= + {{ com Pattern match }} + {{ aux _ l }} +% {{ aux _ annot }} {{ auxparam 'a }} + | pat -> exp :: :: exp +% 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 }} +% {{ aux _ annot }} {{ auxparam 'a }} + | :: :: none + | typquant atyp :: :: 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 }} +% {{ aux _ annot }} {{ auxparam 'a }} + | :: :: pure {{ com sugar for empty effect set }} + | effectkw atyp :: :: effect + +funcl :: 'FCL_' ::= + {{ com Function clause }} + {{ aux _ l }} +% {{ aux _ annot }} {{ auxparam 'a }} + | id pat = exp :: :: Funcl + + +fundef :: 'FD_' ::= + {{ com Function definition}} + {{ aux _ l }} +% {{ 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 _ l }} +% {{ aux _ annot }} {{ auxparam 'a }} + | let 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_' ::= + {{ com Value type specification }} + {{ aux _ l }} +% {{ aux _ annot }} {{ auxparam 'a }} + | val typschm id :: :: val_spec + | val extern typschm id :: :: extern_no_rename + | val extern typschm id = string :: :: extern_spec + +default_typing_spec :: 'DT_' ::= + {{ com Default kinding or typing assumption, and default order for literal vectors and vector shorthands }} + {{ aux _ l }} +% {{ aux _ annot }} {{ auxparam 'a }} + | default base_kind kid :: :: kind + | default base_kind atyp :: :: order + | 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 Function and type union definitions that can be spread across + a file. Each one must end in $[[end id]]$ }} + {{ aux _ l }} + | scattered function rec_opt tannot_opt effect_opt id :: :: scattered_function {{ texlong }} {{ com scattered function definition header }} + + | function clause funcl :: :: scattered_funcl +{{ 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 {{ com scattered union definition member }} + | end id :: :: scattered_end +{{ com scattered definition end }} + +dec_spec :: 'DEC_' ::= + {{ com Register declarations }} + {{ aux _ l }} + | register atyp id :: :: reg + | register alias id = exp :: :: alias + | register alias atyp id = exp :: :: typ_alias + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Top-level definitions % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +def :: 'DEF_' ::= + {{ com Top-level definition }} + | 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 }} + | default_typing_spec :: :: default + {{ com default kind and type assumptions }} + | scattered_def :: :: scattered + {{ com scattered definition }} + | dec_spec :: :: reg_dec + {{ com register declaration }} + +defs :: '' ::= + {{ com Definition sequence }} + | def1 .. defn :: :: Defs + + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Machinery for typing rules % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%% %% +%% %% +%% %% grammar +%% %% +%% %% +%% %% p :: 'Path_' ::= +%% %% {{ com Unique paths }} +%% %% | x1 . .. xn . x :: :: def +%% %% | __list :: :: list +%% %% {{ tex \ottkw{\_\_list} }} +%% %% | __bool :: :: bool +%% %% {{ tex \ottkw{\_\_bool} }} +%% %% | __num :: :: num +%% %% {{ tex \ottkw{\_\_num} }} +%% %% | __set :: :: set +%% %% {{ tex \ottkw{\_\_set} }} +%% %% | __string :: :: string +%% %% {{ tex \ottkw{\_\_string} }} +%% %% | __unit :: :: unit +%% %% {{ tex \ottkw{\_\_unit} }} +%% %% | __bit :: :: bit +%% %% {{ tex \ottkw{\_\_bit} }} +%% %% | __vector :: :: vector +%% %% {{ tex \ottkw{\_\_vector} }} +%% %% %TODO morally, delete the above - but what are the __ things for? +%% %% % cleaner to declare early in the library? +%% %% +%% %% t_subst {{ tex \ensuremath{\sigma} }} :: '' ::= {{ phantom }} +%% %% {{ hol (a # t) list }} +%% %% {{ lem list (tnvar * t) }} +%% %% {{ com Type variable substitutions }} +%% %% | { tnvar1 |-> t1 .. tnvarn |-> tn } :: :: T_subst +%% %% {{ ocaml (assert false) }} +%% %% {{ lem ([[tnvar1 t1 .. tnvarn tn]]) }} +%% %% {{ hol ([[tnvar1 t1 .. tnvarn tn]]) }} +%% %% +%% %% t , u :: 'T_' ::= +%% %% {{ com Internal types }} +%% %% | a :: :: var +%% %% | t1 -> t2 :: :: fn +%% %% | t1 * .... * tn :: :: tup +%% %% | p t_args :: :: app +%% %% | ne :: :: len +%% %% | t_subst ( t ) :: M :: subst_app +%% %% {{ com Multiple substitutions }} +%% %% {{ ocaml (assert false) }} +%% %% {{ hol (t_subst_t [[t_subst]] [[t]]) }} +%% %% {{ lem (t_subst_t [[t_subst]] [[t]]) }} +%% %% | t_subst ( tnv ) :: M :: var_subst_app +%% %% {{ com Single variable substitution }} +%% %% {{ ocaml (assert false) }} +%% %% {{ hol (t_subst_tnv [[t_subst]] [[tnv]]) }} +%% %% {{ lem (t_subst_tnv [[t_subst]] [[tnv]]) }} +%% %% | curry ( t_multi , t ) :: M :: multifn +%% %% {{ com Curried, multiple argument functions }} +%% %% {{ ocaml (assert false) }} +%% %% {{ hol (FOLDR T_fn [[t]] [[t_multi]]) }} +%% %% {{ lem (List.fold_right T_fn [[t_multi]] [[t]]) }} +%% %% +%% %% ne :: 'Ne_' ::= +%% %% {{ com internal numeric expressions }} +%% %% | N :: :: var +%% %% | nat :: :: const +%% %% | ne1 * ne2 :: :: mult +%% %% | ne1 + ne2 :: :: add +%% %% | ( - ne ) :: :: unary +%% %% | normalize ( ne ) :: M :: normalize +%% %% {{ ocaml (assert false) }} +%% %% {{ hol ARB }} +%% %% {{ lem (normalize [[ne]] ) }} +%% %% | ne1 + ... + nen :: M :: addmany +%% %% {{ ocaml (assert false) }} +%% %% {{ hol ARB }} +%% %% {{ lem (sumation_nes [[ne1...nen]]) }} +%% %% | bitlength ( bin ) :: M :: cbin +%% %% {{ ocaml (asssert false) }} +%% %% {{ hol ARB }} +%% %% {{ lem (blength [[bin]]) }} +%% %% | bitlength ( hex ) :: M :: chex +%% %% {{ ocaml (assert false) }} +%% %% {{ hol ARB }} +%% %% {{ lem (hlength [[hex]]) }} +%% %% | length ( pat1 ... patn ) :: M :: cpat +%% %% {{ ocaml (assert false) }} +%% %% {{ hol ARB }} +%% %% {{ lem (Ne_const (List.length [[pat1...patn]])) }} +%% %% | length ( exp1 ... expn ) :: M :: cexp +%% %% {{ hol ARB }} +%% %% {{ ocaml (assert false) }} +%% %% {{ lem (Ne_const (List.length [[exp1...expn]])) }} +%% %% +%% %% t_args :: '' ::= +%% %% {{ com Lists of types }} +%% %% | t1 .. tn :: :: T_args +%% %% | t_subst ( t_args ) :: M :: T_args_subst_app +%% %% {{ com Multiple substitutions }} +%% %% {{ ocaml (assert false) }} +%% %% {{ hol (t_subst_t_args [[t_subst]] [[t_args]]) }} +%% %% {{ lem (t_subst_t_args [[t_subst]] [[t_args]]) }} +%% %% +%% %% t_multi :: '' ::= {{ phantom }} +%% %% {{ hol t list }} +%% %% {{ ocaml t list }} +%% %% {{ lem list t }} +%% %% {{ com Lists of types }} +%% %% | ( t1 * .. * tn ) :: :: T_multi +%% %% {{ hol [[t1..tn]] }} +%% %% {{ lem [[t1..tn]] }} +%% %% | t_subst ( t_multi ) :: M :: T_multi_subst_app +%% %% {{ com Multiple substitutions }} +%% %% {{ ocaml (assert false) }} +%% %% {{ hol (MAP (t_subst_t [[t_subst]]) [[t_multi]]) }} +%% %% {{ lem (List.map (t_subst_t [[t_subst]]) [[t_multi]]) }} +%% %% +%% %% nec :: '' ::= +%% %% {{ com Numeric expression constraints }} +%% %% | ne < nec :: :: lessthan +%% %% | ne = nec :: :: eq +%% %% | ne <= nec :: :: lteq +%% %% | ne :: :: base +%% %% +%% %% parsing +%% %% T_fn right T_fn +%% %% T_tup <= T_multi +%% %% +%% %% embed +%% %% {{ lem +%% %% +%% %% val t_subst_t : list (tnv * t) -> t -> t +%% %% val t_subst_tnv : list (tnv * t) -> tnv -> t +%% %% val ftv_t : t -> list tnv +%% %% val ftv_tm : list t -> list tnv +%% %% val ftv_s : list (p*tnv) -> list tnv +%% %% val compatible_overlap : list (x*t) -> bool +%% %% +%% %% (*TODO Should this normalize following the implementation? And blength and hlength need a means of implementation*) +%% %% let normalize n = n +%% %% +%% %% let blength (_,bit) = Ne_const 8 +%% %% let hlength (_,bit) = Ne_const 8 +%% %% +%% %% let rec sumation_nes nes = match nes with +%% %% | [ a; b] -> Ne_add a b +%% %% | x :: y -> Ne_add x (sumation_nes y) +%% %% end +%% %% +%% %% }} +%% %% +%% %% grammar +%% %% +%% %% +%% %% names :: '' ::= {{ phantom }} +%% %% {{ hol x set }} +%% %% {{ lem set x }} +%% %% {{ ocaml Set.Make(String).t }} +%% %% {{ com Sets of names }} +%% %% | { x1 , .. , xn } :: :: Names +%% %% {{ hol (LIST_TO_SET [[x1..xn]]) }} +%% %% {{ lem (set_from_list [[x1..xn]]) }} +%% %% +%% %% semC {{ tex \ensuremath{\mathcal{C} } }} :: '' ::= +%% %% {{ hol (p#tnv) list }} +%% %% {{ lem list (p*tnv) }} +%% %% % {{ com Typeclass constraint lists }} +%% %% % | ( p1 tnv1 ) .. ( pn tnvn ) :: :: SemC_concrete +%% %% % {{ hol ([[p1 tnv1..pn tnvn]]) }} +%% %% % {{ lem ([[p1 tnv1..pn tnvn]]) }} +%% %% +%% %% env_tag :: '' ::= +%% %% {{ com Tags for the (non-constructor) value descriptions }} +%% %% % | method :: :: method +%% %% % {{ com Bound to a method }} +%% %% | val :: :: spec +%% %% {{ com Specified with val }} +%% %% | let :: :: def +%% %% {{ com Defined with let or indreln }} +%% %% +%% %% v_desc :: 'V_' ::= +%% %% {{ com Value descriptions }} +%% %% | < forall tnvs . t_multi -> p , ( x of names ) > :: :: constr +%% %% {{ com Constructors }} +%% %% | < forall tnvs . semC => t , env_tag > :: :: val +%% %% {{ com Values }} +%% %% +%% %% f_desc :: 'F_' ::= +%% %% | < forall tnvs . p -> t , ( x of names ) > :: :: field +%% %% {{ com Fields }} +%% %% +%% %% embed +%% %% {{ hol +%% %% load "fmaptreeTheory"; +%% %% val _ = +%% %% Hol_datatype +%% %% `env_body = <| env_p : x|->p; env_f : x|->f_desc; env_v : x|->v_desc |>`; +%% %% +%% %% val _ = Define ` +%% %% env_union e1 e2 = +%% %% let i1 = item e1 in +%% %% let m1 = map e1 in +%% %% let i2 = item e2 in +%% %% let m2 = map e2 in +%% %% FTNode <| env_p:=FUNION i1.env_p i2.env_p; +%% %% env_f:=FUNION i1.env_f i2.env_f; +%% %% env_v:=FUNION i1.env_v i2.env_v |> +%% %% (FUNION m1 m2)`; +%% %% }} +%% %% {{ lem +%% %% type env = +%% %% | EnvEmp +%% %% | Env of (map x env) * (map x p) * (map x f_desc) * (map x v_desc) +%% %% +%% %% val env_union : env -> env -> env +%% %% let env_union e1 e2 = +%% %% match (e1,e2) with +%% %% | (EnvEmp,e2) -> e2 +%% %% | (e1,EnvEmp) -> e1 +%% %% | ((Env Em1 Ep1 Ef1 Ev1),(Env Em2 Ep2 Ef2 Ev2)) -> +%% %% Env(union_map Em1 Em2) (union_map Ep1 Ep2) (union_map Ef1 Ef2) (union_map Ev1 Ev2) +%% %% end +%% %% +%% %% }} +%% %% +%% %% grammar +%% %% +%% %% xs :: '' ::= {{ phantom }} +%% %% {{ hol string list }} +%% %% {{ lem list string }} +%% %% | x1 .. xn :: :: Xs +%% %% {{ hol [[x1..xn]] }} +%% %% {{ lem [[x1..xn]] }} +%% %% +%% %% %TODO: no clue what the following are: +%% %% S_c {{ tex {\ensuremath{ {\Sigma}^{\mathcal{C} } } } }} :: '' ::= {{ phantom }} +%% %% {{ hol (p#t) list }} +%% %% {{ lem list (p*t) }} +%% %% {{ com Typeclass constraints }} +%% %% | { ( p1 t1 ) , .. , ( pn tn ) } :: :: S_concrete +%% %% {{ hol [[p1 t1 .. pn tn]] }} +%% %% {{ lem [[p1 t1 .. pn tn]] }} +%% %% | S_c1 union .. union S_cn :: M :: S_union +%% %% {{ hol (FLAT [[S_c1..S_cn]]) }} +%% %% {{ lem (List.flatten [[S_c1..S_cn]]) }} +%% %% {{ ocaml assert false }} +%% %% +%% %% S_N {{ tex { \ensuremath{ {\Sigma}^{\mathcal{N} } } } }} :: '' ::= {{ phantom }} +%% %% {{ hol nec list }} +%% %% {{ lem list nec }} +%% %% {{ com nexp constraint lists }} +%% %% | { nec1 , .. , necn } :: :: Sn_concrete +%% %% {{ hol [[nec1 .. necn]] }} +%% %% {{ lem [[nec1 .. necn]] }} +%% %% | S_N1 union .. union S_Nn :: M :: SN_union +%% %% {{ hol (FLAT [[S_N1..S_Nn]]) }} +%% %% {{ lem (List.flatten [[S_N1..S_Nn]]) }} +%% %% {{ ocaml assert false }} +%% %% +%% %% +%% %% E :: '' ::= {{ phantom }} +%% %% {{ hol ((string,env_body) fmaptree) }} +%% %% +%% %% +%% %% %TODO: simplify by removing E_m throughout? And E_p?? +%% %% {{ lem env }} +%% %% {{ com Environments }} +%% %% | < E_m , E_p , E_f , E_x > :: :: E +%% %% {{ hol (FTNode <|env_p:=[[E_p]]; env_f:=[[E_f]]; env_v:=[[E_x]]|> ([[E_m]])) }} +%% %% {{ lem (Env [[E_m]] [[E_p]] [[E_f]] [[E_x]]) }} +%% %% | E1 u+ E2 :: M :: E_union +%% %% {{ hol (env_union [[E1]] [[E2]]) }} +%% %% {{ lem (env_union [[E1]] [[E2]]) }} +%% %% {{ ocaml assert false }} +%% %% | empty :: M :: E_empty +%% %% {{ hol (FTNode <|env_p:=FEMPTY; env_f:=FEMPTY; env_v:=FEMPTY|> FEMPTY) }} +%% %% {{ lem EnvEmp }} +%% %% {{ ocaml assert false }} +%% %% +%% %% E_x {{ tex \ottnt{E}^{\textsc{x} } }} :: 'E_x_' ::= {{ phantom }} +%% %% {{ hol (x|-> v_desc) }} +%% %% {{ lem map x v_desc }} +%% %% {{ com Value environments }} +%% %% | { x1 |-> v_desc1 , .. , xn |-> v_descn } :: :: concrete +%% %% {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[x1 v_desc1 .. xn v_descn]]) }} +%% %% {{ lem (List.fold_right (fun (x,v) m -> Pmap.add x v m) [[x1 v_desc1 .. xn v_descn]] Pmap.empty) }} +%% %% | E_x1 u+ .. u+ E_xn :: M :: union +%% %% {{ hol (FOLDR FUNION FEMPTY [[E_x1..E_xn]]) }} +%% %% {{ lem (List.fold_right union_map [[E_x1..E_xn]] Pmap.empty) }} +%% %% {{ ocaml (assert false) }} +%% %% +%% %% E_f {{ tex \ottnt{E}^{\textsc{f} } }} :: 'E_f_' ::= {{ phantom }} +%% %% {{ hol (x |-> f_desc) }} +%% %% {{ lem map x f_desc }} +%% %% {{ com Field environments }} +%% %% | { x1 |-> f_desc1 , .. , xn |-> f_descn } :: :: concrete +%% %% {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 f_desc1 .. xn f_descn]]) }} +%% %% {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) [[x1 f_desc1 .. xn f_descn]] Pmap.empty) }} +%% %% | E_f1 u+ .. u+ E_fn :: M :: union +%% %% {{ hol (FOLDR FUNION FEMPTY [[E_f1..E_fn]]) }} +%% %% {{ lem (List.fold_right union_map [[E_f1..E_fn]] Pmap.empty) }} +%% %% {{ ocaml (assert false) }} +%% %% +%% %% E_m {{ tex \ottnt{E}^{\textsc{m} } }} :: 'E_m_' ::= {{ phantom }} +%% %% {{ hol (string |-> (string,env_body) fmaptree) }} +%% %% {{ lem map x env }} +%% %% % {{ com Module environments }} +%% %% % | { x1 |-> E1 , .. , xn |-> En } :: :: concrete +%% %% % {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 E1 .. xn En]]) }} +%% %% % {{ lem (List.fold_right (fun (x,e) m -> Pmap.add x e m) [[x1 E1 .. xn En]] Pmap.empty) }} +%% %% % +%% %% % _p {{ tex \ottnt{E}^{\textsc{p} } }} :: 'E_p_' ::= {{ phantom }} +%% %% % {{ hol (x |-> p) }} +%% %% % {{ lem map x p }} +%% %% % {{ com Path environments }} +%% %% % | { x1 |-> p1 , .. , xn |-> pn } :: :: concrete +%% %% % {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 p1 .. xn pn]]) }} +%% %% % {{ lem (List.fold_right (fun (x,p) m -> Pmap.add x p m) [[x1 p1 .. xn pn]] Pmap.empty) }} +%% %% % | E_p1 u+ .. u+ E_pn :: M :: union +%% %% % {{ hol (FOLDR FUNION FEMPTY [[E_p1..E_pn]]) }} +%% %% % {{ lem (List.fold_right union_map [[E_p1..E_pn]] Pmap.empty) }} +%% %% % +%% %% % {{ ocaml (assert false) }} +%% %% E_l {{ tex \ottnt{E}^{\textsc{l} } }} :: 'E_l_' ::= {{ phantom }} +%% %% {{ hol (x |-> t) }} +%% %% {{ lem map x t }} +%% %% {{ com Lexical bindings }} +%% %% | { x1 |-> t1 , .. , xn |-> tn } :: :: concrete +%% %% {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[x1 t1 .. xn tn]]) }} +%% %% {{ lem (List.fold_right (fun (x,t) m -> Pmap.add x t m) [[x1 t1 .. xn tn]] Pmap.empty) }} +%% %% | E_l1 u+ .. u+ E_ln :: M :: union +%% %% {{ hol (FOLDR FUNION FEMPTY [[E_l1..E_ln]]) }} +%% %% {{ lem (List.fold_right union_map [[E_l1..E_ln]] Pmap.empty) }} +%% %% {{ ocaml (assert false) }} +%% %% +%% %% tc_abbrev :: 'Tc_abbrev_' ::= {{ phantom }} +%% %% {{ hol t option }} +%% %% {{ lem option t }} +%% %% {{ ocaml t option }} +%% %% {{ com Type abbreviations }} +%% %% | . t :: :: some +%% %% {{ hol (SOME [[t]]) }} +%% %% {{ lem (Some [[t]]) }} +%% %% | :: :: none +%% %% {{ hol NONE }} +%% %% {{ lem None }} +%% %% +%% %% tc_def :: '' ::= +%% %% {{ com Type and class constructor definitions }} +%% %% | tnvs tc_abbrev :: :: Tc_def +%% %% {{ com Type constructors }} +%% %% +%% %% TD {{ tex \ensuremath{\Delta} }} :: 'TD_' ::= {{ phantom }} +%% %% {{ hol p |-> tc_def }} +%% %% {{ lem map p tc_def }} +%% %% {{ com Type constructor definitions }} +%% %% | { p1 |-> tc_def1 , .. , pn |-> tc_defn } :: :: concrete +%% %% {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[p1 tc_def1 .. pn tc_defn]]) }} +%% %% {{ lem (List.fold_right (fun (p,t) m -> Pmap.add p t m) [[p1 tc_def1 .. pn tc_defn]] Pmap.empty) }} +%% %% {{ ocaml (assert false) }} +%% %% | TD1 u+ TD2 :: M :: union +%% %% {{ hol (FUNION [[TD1]] [[TD2]]) }} +%% %% {{ lem (union_map [[TD1]] [[TD2]]) }} +%% %% {{ ocaml (assert false) }} +%% %% +%% %% +%% %% +%% %% D :: 'D_' ::= {{ phantom }} +%% %% {{ hol ((p |-> tc_def) # (p |-> x list) # (inst list)) }} +%% %% {{ lem tdefs}} +%% %% {{ com Global type definition store }} +%% %% | < TD , TC , I > :: :: concrete +%% %% {{ hol ([[TD]], [[TC]], [[I]]) }} +%% %% {{ lem (D [[TD]] [[TC]] [[I]]) }} +%% %% | D1 u+ D2 :: M :: union +%% %% {{ hol (case ([[D1]],[[D2]]) of ((x1,x2,x3),(y1,y2,y3)) => (FUNION x1 y1, FUNION x2 y2, x3 ++ y3)) }} +%% %% {{ lem (union_tcdefs [[D1]] [[D2]]) }} +%% %% {{ ocaml (assert false) }} +%% %% | empty :: M :: empty +%% %% {{ hol (FEMPTY, FEMPTY, []) }} +%% %% {{ lem DEmp }} +%% %% {{ ocaml assert false }} +%% %% +%% %% parsing +%% %% E_union left E_union +%% %% +%% %% embed +%% %% {{ lem +%% %% type tdefs = +%% %% | DEmp +%% %% | D of (map p tc_def) * (map p (list x)) * (set inst) +%% %% +%% %% val union_tcdefs : tdefs -> tdefs -> tdefs +%% %% +%% %% }} + +grammar + +terminals :: '' ::= + | ** :: :: starstar + {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} + {{ com \texttt{**} }} + | >= :: :: geq + {{ tex \ensuremath{\geq} }} + {{ com \texttt{>=} }} + | '<=' :: :: leq + {{ tex \ensuremath{\leq} }} + {{ com \texttt{<=} }} + | -> :: :: arrow + {{ tex \ensuremath{\rightarrow} }} + {{ 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} }} +% | union :: :: union +% {{ tex \ensuremath{\cup} }} + | u+ :: :: uplus + {{ tex \ensuremath{\uplus} }} + | 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} }} + | > :: :: gt + {{ tex \ensuremath{\rangle} }} + | |- :: :: vdash + {{ tex \ensuremath{\vdash} }} + | ' :: :: quote + {{ tex \mbox{'} }} + | |-> :: :: mapsto + {{ tex \ensuremath{\mapsto} }} + | gives :: :: gives + {{ tex \ensuremath{\triangleright} }} + | ~> :: :: leadsto + {{ tex \ensuremath{\leadsto} }} + | => :: :: Rightarrow + {{ tex \ensuremath{\Rightarrow} }} + | -- :: :: dashdash + {{ tex \mbox{--} }} + | empty :: :: empty + {{ tex \ensuremath{\epsilon} }} + | effectkw :: :: effectkw + {{ tex \ottkw{effect} }} + + +formula :: formula_ ::= + | judgement :: :: judgement + + | formula1 .. formulan :: :: dots + +% | E_m ( x ) gives E :: :: lookup_m +% {{ com Module lookup }} +% {{ hol (FLOOKUP [[E_m]] [[x]] = SOME [[E]]) }} +% {{ lem (Pmap.find [[x]] [[E_m]]) = [[E]] }} +% +% | E_p ( x ) gives p :: :: lookup_p +% {{ com Path lookup }} +% {{ hol (FLOOKUP [[E_p]] [[x]] = SOME [[p]]) }} +% {{ lem Pmap.find [[x]] [[E_p]] = [[p]] }} + +%% %% | E_f ( x ) gives f_desc :: :: lookup_f +%% %% {{ com Field lookup }} +%% %% {{ hol (FLOOKUP [[E_f]] [[x]] = SOME [[f_desc]]) }} +%% %% {{ lem Pmap.find [[x]] [[E_f]] = [[f_desc]] }} +%% %% +%% %% | E_x ( x ) gives v_desc :: :: lookup_v +%% %% {{ com Value lookup }} +%% %% {{ hol (FLOOKUP [[E_x]] [[x]] = SOME [[v_desc]]) }} +%% %% {{ lem Pmap.find [[x]] [[E_x]] = [[v_desc]] }} +%% %% +%% %% | E_l ( x ) gives t :: :: lookup_l +%% %% {{ com Lexical binding lookup }} +%% %% {{ hol (FLOOKUP [[E_l]] [[x]] = SOME [[t]]) }} +%% %% {{ lem Pmap.find [[x]] [[E_l]] = [[t]] }} +%% %% +%% %% % | TD ( p ) gives tc_def :: :: lookup_tc +%% %% % {{ com Type constructor lookup }} +%% %% % {{ hol (FLOOKUP [[TD]] [[p]] = SOME [[tc_def]]) }} +%% %% % {{ lem Pmap.find [[p]] [[TD]] = [[tc_def]] }} +%% %% % +%% %% % | TC ( p ) gives xs :: :: lookup_class +%% %% % {{ com Type constructor lookup }} +%% %% % {{ hol (FLOOKUP [[TC]] [[p]] = SOME [[xs]]) }} +%% %% % {{ lem Pmap.find [[p]] [[TC]] = [[xs]] }} +%% %% +%% %% | dom ( E_m1 ) inter dom ( E_m2 ) = emptyset :: :: E_m_disjoint +%% %% {{ hol (DISJOINT (FDOM [[E_m1]]) (FDOM [[E_m2]])) }} +%% %% {{ lem disjoint (Pmap.domain [[E_m1]]) (Pmap.domain [[E_m2]]) }} +%% %% +%% %% | dom ( E_x1 ) inter dom ( E_x2 ) = emptyset :: :: E_x_disjoint +%% %% {{ hol (DISJOINT (FDOM [[E_x1]]) (FDOM [[E_x2]])) }} +%% %% {{ lem disjoint (Pmap.domain [[E_x1]]) (Pmap.domain [[E_x2]]) }} +%% %% +%% %% | dom ( E_f1 ) inter dom ( E_f2 ) = emptyset :: :: E_f_disjoint +%% %% {{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }} +%% %% {{ lem disjoint (Pmap.domain [[E_f1]]) (Pmap.domain [[E_f2]]) }} +%% %% +%% %% % | dom ( E_p1 ) inter dom ( E_p2 ) = emptyset :: :: E_p_disjoint +%% %% % {{ hol (DISJOINT (FDOM [[E_p1]]) (FDOM [[E_p2]])) }} +%% %% % {{ lem disjoint (Pmap.domain [[E_p1]]) (Pmap.domain [[E_p2]]) }} +%% %% % +%% %% | disjoint doms ( E_l1 , .... , E_ln ) :: :: E_l_disjoint +%% %% {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM +%% %% E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_l1....E_ln]] <> NONE) }} +%% %% {{ lem disjoint_all (List.map Pmap.domain [[E_l1 .... E_ln]]) }} +%% %% {{ com Pairwise disjoint domains }} +%% %% +%% %% | disjoint doms ( E_x1 , .... , E_xn ) :: :: E_x_disjoint_many +%% %% {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM +%% %% E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_x1....E_xn]] <> NONE) }} +%% %% {{ lem disjoint_all (List.map Pmap.domain [[E_x1 .... E_xn]]) }} +%% %% {{ com Pairwise disjoint domains }} +%% %% +%% %% | compatible overlap ( x1 |-> t1 , .. , xn |-> tn ) :: :: E_l_compat +%% %% {{ hol (!__n __m. MEM __m [[x1 t1 .. xn tn]] /\ MEM __n [[x1 t1..xn tn]] /\ (FST __m = FST __n) ==> (SND __m = SND __n)) }} +%% %% {{ lem (compatible_overlap [[x1 t1 .. xn tn]]) }} +%% %% {{ com $(\ottnt{x}_i = \ottnt{x}_j) \ensuremath{\Longrightarrow} (\ottnt{t}_i = \ottnt{t}_j)$ }} +%% %% +%% %% | duplicates ( tnvs ) = emptyset :: :: no_dups_tnvs +%% %% {{ hol (ALL_DISTINCT [[tnvs]]) }} +%% %% {{ lem (duplicates [[tnvs]]) = [ ] }} +%% %% +%% %% | duplicates ( x1 , .. , xn ) = emptyset :: :: no_dups +%% %% {{ hol (ALL_DISTINCT [[x1..xn]]) }} +%% %% {{ lem (duplicates [[x1..xn]]) = [ ] }} +%% %% +%% %% | x NOTIN dom ( E_l ) :: :: notin_dom_l +%% %% {{ hol ([[x]] NOTIN FDOM [[E_l]]) }} +%% %% {{ lem Pervasives.not (Pmap.mem [[x]] [[E_l]]) }} +%% %% +%% %% | x NOTIN dom ( E_x ) :: :: notin_dom_v +%% %% {{ hol ([[x]] NOTIN FDOM [[E_x]]) }} +%% %% {{ lem Pervasives.not (Pmap.mem [[x]] [[E_x]]) }} +%% %% +%% %% | x NOTIN dom ( E_f ) :: :: notin_dom_f +%% %% {{ hol ([[x]] NOTIN FDOM [[E_f]]) }} +%% %% {{ lem Pervasives.not (Pmap.mem [[x]] [[E_f]]) }} +%% %% +%% %% % | p NOTIN dom ( TC ) :: :: notin_dom_tc +%% %% % {{ hol ([[p]] NOTIN FDOM [[TC]]) }} +%% %% % {{ lem Pervasives.not (Pmap.mem [[p]] [[TC]]) }} +%% %% +%% %% | p NOTIN dom ( TD ) :: :: notin_dom_td +%% %% {{ hol ([[p]] NOTIN FDOM [[TD]]) }} +%% %% {{ lem Pervasives.not (Pmap.mem [[p]] [[TD]]) }} +%% %% +%% %% | FV ( t ) SUBSET tnvs :: :: FV_t +%% %% {{ com Free type variables }} +%% %% {{ hol (LIST_TO_SET (ftv_t [[t]]) SUBSET LIST_TO_SET [[tnvs]]) }} +%% %% {{ lem subst (ftv_t [[t]]) [[tnvs]] }} +%% %% +%% %% | FV ( t_multi ) SUBSET tnvs :: :: FV_t_multi +%% %% {{ com Free type variables }} +%% %% {{ hol (LIST_TO_SET (FLAT (MAP ftv_t [[t_multi]])) SUBSET LIST_TO_SET [[tnvs]]) }} +%% %% {{ lem subst (ftv_tm [[t_multi]]) [[tnvs]] }} +%% %% +%% %% | FV ( semC ) SUBSET tnvs :: :: FV_semC +%% %% {{ com Free type variables }} +%% %% {{ hol (LIST_TO_SET (MAP SND [[semC]]) SUBSET LIST_TO_SET [[tnvs]]) }} +%% %% {{ lem subst (ftv_s [[semC]]) [[tnvs]] }} +%% %% +%% %% | inst 'IN' I :: :: inst_in +%% %% {{ hol (MEM [[inst]] [[I]]) }} +%% %% {{ lem ([[inst]] IN [[I]]) }} +%% %% +%% %% | ( p t ) NOTIN I :: :: notin_I +%% %% {{ hol (~?__semC__. MEM (Inst __semC__ [[p]] [[t]]) [[I]]) }} +%% %% {{ lem (Pervasives.not ((Inst [] [[p]] [[t]]) IN [[I]])) }} +%% %% +%% %% | E_l1 = E_l2 :: :: E_l_eqn +%% %% {{ ichl ([[E_l1]] = [[E_l2]]) }} +%% %% +%% %% | E_x1 = E_x2 :: :: E_x_eqn +%% %% {{ ichl ([[E_x1]] = [[E_x2]]) }} +%% %% +%% %% | E_f1 = E_f2 :: :: E_f_eqn +%% %% {{ ichl ([[E_f1]] = [[E_f2]]) }} +%% %% +%% %% | E1 = E2 :: :: E_eqn +%% %% {{ ichl ([[E1]] = [[E2]]) }} +%% %% +%% %% | TD1 = TD2 :: :: TD_eqn +%% %% {{ ichl ([[TD1]] = [[TD2]]) }} +%% %% +%% %% | TC1 = TC2 :: :: TC_eqn +%% %% {{ ichl ([[TC1]] = [[TC2]]) }} +%% %% +%% %% | I1 = I2 :: :: I_eqn +%% %% {{ ichl ([[I1]] = [[I2]]) }} +%% %% +%% %% | names1 = names2 :: :: names_eq +%% %% {{ ichl ([[names1]] = [[names2]]) }} +%% %% +%% %% | t1 = t2 :: :: t_eq +%% %% {{ ichl ([[t1]] = [[t2]]) }} +%% %% +%% %% | t_subst1 = t_subst2 :: :: t_subst_eq +%% %% {{ ichl ([[t_subst1]] = [[t_subst2]]) }} +%% %% +%% %% | p1 = p2 :: :: p_eq +%% %% {{ ichl ([[p1]] = [[p2]]) }} +%% %% +%% %% | xs1 = xs2 :: :: xs_eq +%% %% {{ ichl ([[xs1]] = [[xs2]]) }} +%% %% +%% %% | tnvs1 = tnvs2 :: :: tnvs_eq +%% %% {{ ichl ([[tnvs1]] = [[tnvs2]]) }} + diff --git a/language/l2_rules.ott b/language/l2_rules.ott index 7fb54c9a..9e1b79fb 100644 --- a/language/l2_rules.ott +++ b/language/l2_rules.ott @@ -1,1461 +1,424 @@ -grammar - -formula :: formula_ ::= - | judgement :: :: judgement - - | formula1 .. formulan :: :: dots - - | E_k ( tid ) gives kinf :: :: lookup_k - {{ com Kind lookup }} - {{ hol (FLOOKUP [[E_k]] [[tid]] = SOME [[kinf]]) }} - {{ lem Map.lookup [[tid]] [[E_k]] = Just [[kinf]] }} - - | E_a ( tid ) gives tinf :: :: lookup_a_t - | E_a ( tid ) gives ne :: :: lookup_a_ne - - - | E_t ( id ) gives tinf :: :: lookup_t - {{ com Type lookup }} - {{ hol (FLOOKUP [[E_t]] [[id]] = SOME [[tinf]]) }} - {{ lem Map.lookup [[id]] [[E_t]] = Just [[tinf]] }} - | E_t ( id ) gives overload tinf : tinf1 ... tinfn :: :: lookup_over_t - {{ com Overloaded type lookup }} - - | E_k ( tid ) <-| k :: :: update_k - {{ com Update the kind associated with id to k }} - {{ lem [[true]] (*TODO: update_k needs to be rewritten*) }} - - | E_r ( id0 .. idn ) gives t , ts :: :: lookup_r - {{ com Record lookup }} - {{ lem [[true]] (*TODO write a proper lookup for E_r *) }} - - | E_r ( t ) gives id0 : t0 .. idn : tn :: :: lookup_rt - {{ com Record looup by type }} - {{ lem [[true]] (* write a proper lookup for E_r *) }} - - | E_e ( t ) gives enumerate_map :: :: lookup_e - {{ com Enumeration lookup by type }} - {{ lem Map.lookup [[t]] [[E_e]] = Just [[enumerate_map]] }} - - | dom ( E_t1 ) inter dom ( E_t2 ) = emptyset :: :: E_t_disjoint - {{ hol (DISJOINT (FDOM [[E_t1]]) (FDOM [[E_t2]])) }} - {{ lem disjoint (Map.domain [[E_t1]]) (Map.domain [[E_t2]]) }} - - | dom ( E_k1 ) inter dom ( E_k2 ) = emptyset :: :: E_k_disjoint - {{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }} - {{ lem disjoint (Map.domain [[E_f1]]) (Map.domain [[E_f2]]) }} - - | disjoint doms ( E_t1 , .... , E_tn ) :: :: E_x_disjoint_many - {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM - E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_t1....E_tn]] <> NONE) }} - {{ lem disjoint_all (List.map Map.domain [[E_t1 .... E_tn]]) }} - {{ com Pairwise disjoint domains }} - | id NOTIN dom ( E_k ) :: :: notin_dom_k - {{ hol ([[id]] NOTIN FDOM [[E_k]]) }} - {{ lem Pervasives.not (Map.member [[id]] [[E_k]]) }} - | id NOTIN dom ( E_t ) :: :: notin_dom_t - {{ hol ([[id]] NOTIN FDOM [[E_t]]) }} - {{ lem Pervasives.not (Map.member [[id]] [[E_t]]) }} - - | id0 : t0 .. idn : tn SUBSET id'0 : t'0 .. id'i : t'i :: :: subsetFields - {{ lem ((Set.fromList [[id0 t0..idn tn]]) subset (Set.fromList [[id'0 t'0..id'i t'i]])) }} - - | num1 lt ... lt numn :: :: increasing - - | num1 gt ... gt numn :: :: decreasing - - | exp1 == exp2 :: :: exp_eqn - {{ ichl ([[exp1]] = [[exp2]]) }} - - | E_k1 == E_k2 :: :: E_k_eqn - {{ ichl ([[E_k1]] = [[E_k2]]) }} +grammar - | E_k1 ~= E_k2 :: :: E_k_approx - {{ lem ([[E_k1]] = [[E_k2]]) (* Todo, not quite equality *) }} - {{ ich arb }} +mut :: 'mut_' ::= + | immutable :: :: immutable + | mutable :: :: mutable - | E_t1 == E_t2 :: :: E_t_eqn - {{ ichl ([[E_t1]] = [[E_t2]]) }} +lvar :: 'lvar_' ::= + | register typ :: :: register + | enum typ :: :: enum + | local mut typ :: :: local + | union typquant typ :: :: union + | unbound :: :: unbound + - | E_r1 == E_r2 :: :: E_r_eqn - {{ ichl ([[E_r1]] = [[E_r2]]) }} - | E_e1 == E_e2 :: :: E_e_eqn - {{ ichl ([[E_e1]] = [[E_e2]]) }} - - | E_d1 == E_d2 :: :: E_d_eqn - {{ ichl ([[E_d1]] = [[E_d2]]) }} +G {{ tex \Gamma }}, D {{ tex \Delta }} :: 'G_' ::= {{ com Type environment }} + | empty :: :: empty {{ tex \epsilon }} {{ com Empty context }} + | G , x1 : typ1 , .. , xn : typn :: :: type_list {{ com List of variables and their types }} +% | G , x1 : k1 , .. , xn : kn :: :: kind_list {{ com List of variables and their kinds }} + | G , kid1 , .. , kidn :: :: kid_list +% | G , quant_item1 , .. , quant_itemn :: :: quant_list +% | G , { nec1 , .. , necn } :: :: constraint_list {{ com Constraints }} + | G , G1 .. Gn :: :: merge {{ com Merge or disjoint union }} + | G , id : lvar :: :: add_local - | E1 == E2 :: :: E_eqn - {{ ichl ([[E1]] = [[E2]]) }} - | S_N1 == S_N2 :: :: S_N_eqn - {{ ichl ([[S_N1]] = [[S_N2]]) }} - - | id == 'id :: :: id_eq - | x1 NOTEQ x2 :: :: id_neq - | lit1 NOTEQ lit2 :: ::lit_neq - | I1 == I2 :: :: I_eqn - {{ ichl ([[I1]] = [[I2]]) }} - - | effect1 == effect2 :: :: Ef_eqn - {{ ichl ([[effect1]] = [[effect2]]) }} - - | t1 == t2 :: :: t_eq - {{ ichl ([[t1]] = [[t2]]) }} - | ne == ne' :: :: ne_eq - {{ ichl ([[ne]] = [[ne']]) }} - | kid == fresh_kid ( E_d ) :: :: kid_eq - {{ ichl ([[kid]] = fresh_kid [[E_d]]) }} +formula :: formula_ ::= + | judgement :: :: judgement + | formula1 .. formulan :: :: dots + | G ( id ) = lvar :: :: lookup_id + | G ( typ1 , id ) = typ2 :: :: lookup_record_field + | G ( typ1 ) = typ2 :: :: lookup_typ + | nexp = length [|| exp , exp1 , .. , expn ||] :: :: vector_length + | order_inc :: :: default_order_inc + | order_dec :: :: default_order_dec + | G |= nexp1 <= nexp2 :: :: prove_lteq defns -check_t :: '' ::= + declarative :: '' ::= defn -E_k |-t t ok :: :: check_t :: check_t_ -{{ lemwcf witness type check_t_witness; check check_t_w_check; }} -{{ com Well-formed types }} - by - - E_k('x) gives K_Typ - ------------------------------------------------------------ :: var - E_k |-t 'x ok - - E_k('x) gives K_infer - E_k('x) <-| K_Typ - ------------------------------------------------------------ :: varInfer - E_k |-t 'x ok - - E_k |-t t1 ok - E_k |-t t2 ok - E_k |-e effect ok - ------------------------------------------------------------ :: fn - E_k |-t t1 -> t2 effect ok - - E_k |-t t1 ok .... E_k |-t tn ok - ------------------------------------------------------------ :: tup - E_k |-t (t1 , .... , tn) ok - - E_k(x) gives K_Lam(k1..kn -> K_Typ) - E_k,k1 |- t_arg1 ok .. E_k,kn |- t_argn ok - ------------------------------------------------------------ :: app - E_k |-t x < t_arg1 .. t_argn > ok - -defn -E_k |-e effect ok :: :: check_ef :: check_ef_ -{{ com Well-formed effects }} -{{ lemwcf witness type check_ef_witness; check check_ef_w_check; }} -by - -E_k('x) gives K_Efct ------------------------------------------------------------ :: var -E_k |-e 'x ok - -E_k('x) gives K_infer -E_k('x) <-| K_Efct ------------------------------------------------------------- :: varInfer -E_k |-e 'x ok - -------------------------------------------------------------- :: set -E_k |-e { base_effect1 , .. , base_effectn } ok - -defn -E_k |-n ne ok :: :: check_n :: check_n_ -{{ com Well-formed numeric expressions }} -{{ lemwcf witness type check_n_witness; check check_n_w_check; }} -by - -E_k(x) gives K_Nat ------------------------------------------------------------ :: id -E_k |-n x ok - -E_k('x) gives K_Nat ------------------------------------------------------------ :: var -E_k |-n 'x ok - -E_k('x) gives K_infer -E_k('x) <-| K_Nat ------------------------------------------------------------- :: varInfer -E_k |-n 'x ok - ------------------------------------------------------------ :: num -E_k |-n num ok - -E_k |-n ne1 ok -E_k |-n ne2 ok ------------------------------------------------------------ :: sum -E_k |-n ne1 + ne2 ok - -E_k |-n ne1 ok -E_k |-n ne2 ok ------------------------------------------------------------ :: minus -E_k |-n ne1 - ne2 ok - -E_k |-n ne1 ok -E_k |-n ne2 ok ------------------------------------------------------------- :: mult -E_k |-n ne1 * ne2 ok - -E_k |-n ne ok ------------------------------------------------------------- :: exp -E_k |-n 2 ** ne ok - -defn -E_k |-o order ok :: :: check_ord :: check_ord_ -{{ com Well-formed numeric expressions }} -{{ lemwcf witness type check_ord_witness; check check_ord_w_check; }} + G |- typ1 ~< typ2 :: :: subtype :: subtype_ + {{ com $[[typ1]]$ is a subtype of $[[typ2]]$ }} + {{ tex [[G]] \vdash [[typ1]] \preccurlyeq [[typ2]] }} by -E_k('x) gives K_Ord ------------------------------------------------------------ :: var -E_k |-o 'x ok - -E_k('x) gives K_infer -E_k('x) <-| K_Ord ------------------------------------------------------------- :: varInfer -E_k |-o 'x ok +----------------- :: refl +G |- typ ~< typ ------------------------------------------------------------- :: inc -E_k |-o inc ok +--------------------- :: wild +G |- _ ~< _ ------------------------------------------------------------- :: dec -E_k |-o dec ok -defn -E_k , k |- t_arg ok :: :: check_targs :: check_targs_ -{{ com Well-formed type arguments kind check matching the application type variable }} -{{ lemwcf witness type check_targs_witness; check check_targs_w_check; }} -by -E_k |-t t ok ---------------------------------------------------------- :: typ -E_k , K_Typ |- t ok +------------- :: id +G |- id ~< id -E_k |-e effect ok ---------------------------------------------------------- :: eff -E_k , K_Efct |- effect ok +G |- typ1 ~< typ'1 .. G |- typn ~< typ'n +--------------------------------------------------- :: tuple +G |- (typ1 , .. , typn ) ~< (typ'1, .. , typ'n) -E_k |-n ne ok ---------------------------------------------------------- :: nat -E_k , K_Nat |- ne ok - -E_k |-o order ok ---------------------------------------------------------- :: ord -E_k, K_Ord |- order ok - -defns -convert_kind :: '' ::= defn -E_k |- kind ~> k :: :: convert_kind :: convert_kind_ -{{ lemwcf witness type convert_kind_witness; check convert_kind_w_check; }} +G |-l lit => typ :: :: infer_lit :: infer_lit_ +{{ com Infer that type of $[[lit]]$ is $[[typ]]$ }} +{{ tex [[G]] \vdash_l [[lit]] \Rightarrow [[typ]] }} by --------------------- :: Typ -E_k |- Type ~> K_Typ -defns -convert_typ :: '' ::= +----------------------------- :: unit +G |-l () => unit -defn -E_d |- quant_item ~> E_k1 , S_N :: :: convert_quants :: convert_quants_ -{{ com Convert source quantifiers to kind environments and constraints }} -{{ lemwcf witness type convert_quants_witness; check convert_quants_w_check; }} -by - -E_k |- kind ~> k ------------------------------------------------------------ :: kind -<E_k,E_a,E_r,E_e> |- kind 'x ~> {'x |-> k}, {} +-------------------- :: zero +G |-l bitzero => bit -E_k('x) gives k ------------------------------------------------------------ :: nokind -<E_k,E_a,E_r,E_e> |- 'x ~> {'x |-> k},{} +-------------------- :: one +G |-l bitone => bit -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------ :: eq -E_d |- nexp1 = nexp2 ~> {}, {ne1 = ne2} -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------ :: gteq -E_d |- nexp1 >= nexp2 ~> {}, {ne1 >= ne2} +---------------------- :: num +G |-l num => atom < num > -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------ :: lteq -E_d |- nexp1 <= nexp2 ~> {}, {ne1 <= ne2} ------------------------------------------------------------ :: in -E_d |- 'x IN {num1 , ... , numn} ~> {}, {'x IN {num1 , ..., numn}} +---------------------- :: true +G |-l true => bool -defn -E_d |- typschm ~> t , E_k , S_N :: :: convert_typschm :: convert_typschm_ -{{ com Convert source types with typeschemes to internal types and kind environments }} -{{ lemwcf witness type convert_typschm_witness; check convert_typschm_w_check; }} -by -E_d |- typ ~> t ------------------------------------------------------------ :: noquant -E_d |- typ ~> t,{},{} - -E_d |- quant_item1 ~> E_k1, S_N1 ... E_d |- quant_itemn ~> E_kn, S_Nn -E_k == E_k1 u+ ... u+ E_kn -E_d u+ <E_k,{},{},{}> |- typ ~> t ------------------------------------------------------------ :: quant -E_d |- forall quant_item1 , ... , quant_itemn . typ ~> t, E_k, S_N1 u+ ... u+ S_Nn +---------------------- :: false +G |-l false => bool defn -E_d |- typ ~> t :: :: convert_typ :: convert_typ_ -{{ com Convert source types to internal types }} -{{ lemwcf witness type convert_typ_witness; check convert_typ_w_check; }} +G |- lexp := exp => typ -| D :: :: bind_assignment :: bind_assignment_ +{{ com Bind assignment returning updated environment }} +{{ tex [[G]] \vdash [[lexp]] := [[exp]] \Rightarrow [[typ]] \dashv [[D]] }} by - -E_k('x) gives K_Typ ------------------------------------------------------------- :: var -<E_k,E_a,E_r,E_e> |- 'x ~> 'x - -E_k(x) gives K_Typ ------------------------------------------------------------- :: id -<E_k,E_a,E_r,E_e> |- x ~> x - -E_d |- typ1 ~> t1 -E_d |- typ2 ~> t2 ------------------------------------------------------------- :: fn -E_d |- typ1->typ2 effectkw effect ~> t1->t2 effect - -E_d |- typ1 ~> t1 .... E_d |- typn ~> tn ------------------------------------------------------------- :: tup -E_d |- ( typ1 , .... , typn ) ~> (t1 , .... , tn) -E_k(x) gives K_Lam (k1..kn -> K_Typ) -<E_k,E_a,E_r,E_e>,k1 |- typ_arg1 ~> t_arg1 .. <E_k,E_a,E_r,E_e>,kn |- typ_argn ~> t_argn ------------------------------------------------------------- :: app -<E_k,E_a,E_r,E_e> |- x <typ_arg1, .. ,typ_argn> ~> x <t_arg1 .. t_argn> + +G |- exp => typ +G |- id <= typ -| D +------------------------------- :: id +G |- id := exp => unit -| D defn -E_d , k |- typ_arg ~> t_arg :: :: convert_targ :: convert_targ_ -{{ com Convert source type arguments to internals }} -{{ lemwcf witness type convert_targ_witness; check convert_targ_w_check; }} +G |- pat <= typ -| D :: :: bind_pat :: bind_pat_ +{{ tex [[G]] \vdash [[pat]] \Leftarrow [[typ]] \dashv [[D]] }} by - -E_d |- typ ~> t -------------------------------------- :: typ -E_d, K_Typ |- typ ~> t - -defn -|- nexp ~> ne :: :: convert_nexp :: convert_nexp_ -{{ com Convert and normalize numeric expressions }} -{{ lemwcf witness type convert_nexp_witness; check convert_nexp_w_check; }} -by - -------------------------------------------------------------- :: id -|- x ~> x ------------------------------------------------------------- :: var -|- 'x ~> 'x +G |- lit <= typ +------------------- :: lit +G |- lit <= typ -| G ------------------------------------------------------------- :: num -|- num ~> num +%% FIXME do add_local +G(id) = local mutable typ' +---------------------- :: local +G |- id <= typ -| G -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------- :: mult -|- nexp1 * nexp2 ~> ne1 * ne2 +G(id) = unbound +---------------------- :: unbound +G |- id <= typ -| G -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------ :: add -|- nexp1 + nexp2 ~> ne1 + ne2 -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------ :: sub -|- nexp1 - nexp2 ~> ne1 - ne2 +G(id) = enum typ' +G |- typ' ~< typ +---------------------- :: enum +G |- id <= typ -| G -|- nexp ~> ne ------------------------------------------------------------- :: exp -|- 2** nexp ~> 2 ** ne -defn -E_d |-n ne ~= ne' :: :: conforms_to_ne :: conforms_to_ne_ -by - -E_k |-n ne ok ------------------------------------------------------------- :: refl -<E_k,E_a,E_r,E_e> |-n ne ~= ne - -E_d |-n ne1 ~= ne2 -E_d |-n ne2 ~= ne3 ------------------------------------------------------------- :: trans -E_d |-n ne1 ~= ne3 +---------------------- :: wild +G |- _ <= typ -| G -E_d |-n ne2 ~= ne1 -------------------------------------------------------------- :: assoc -E_d |-n ne1 ~= ne2 -E_a(x) gives ne -<E_k,E_a,E_r,E_e> |-n ne ~= ne' ------------------------------------------------------------- :: abbrev -<E_k,E_a,E_r,E_e> |-n x ~= ne' +%% FIXME Should be fold? +G |- pat1 <= typ1 -| G1 .. G |- patn <= typn -| Gn +------------------------------------------------------- :: tup +G |- (pat1 , .. , patn ) <= (typ1 , .. , typn ) -| G , G1 .. Gn -:formula_ne_eq: num == num' ------------------------------------------------------------ :: constants -E_d |-n num ~= num' ------------------------------------------------------------- :: rest -E_d |-n ne ~= ne' defn -E_d |- t ~= t' :: :: conforms_to :: conforms_to_ -{{ com Relate t and t' when t can be used where t' is expected without consideration for non-constant nats }} +G |- pat => typ -| D :: :: infer_pat :: infer_pat_ +{{ tex [[G]] \vdash [[pat]] \Leftarrow [[typ]] \dashv [[D]] }} by -E_k |-t t ok ------------------------------------------------------------- :: refl -<E_k,E_a,E_r,E_e> |- t ~= t - -E_d |- t1 ~= t2 -E_d |- t2 ~= t3 ------------------------------------------------------------- :: trans -E_d |- t1 ~= t3 +G(id) = enum typ +-------------------- :: id +G |- id => typ -| G ------------------------------------------------------------- :: var -E_d |- 'x ~= t ------------------------------------------------------------- :: var2 -E_d |- t ~= 'x +G |- pat <= typ -| D +------------------------------- :: typ +G |- (typ) pat => typ -| D -E_a(x) gives u -<E_k,E_a,E_r,E_e> |- u ~= t ------------------------------------------------------------- :: abbrev -<E_k,E_a,E_r,E_e> |- x ~= t -E_a(x) gives u -<E_k,E_a,E_r,E_e> |- t ~= u ------------------------------------------------------------- :: abbrev2 -<E_k,E_a,E_r,E_e> |- t ~= x +G |-l lit => typ +----------------------- :: lit +G |- lit => typ -| G - -E_d |- t1 ~= u1 .... E_d |- tn ~= un ------------------------------------------------------------- :: tup -E_d |- (t1,....,tn) ~= (u1,....,un) -E_k(x) gives K_Lam (k1 .. kn -> K_Typ) -<E_k,E_a,E_r,E_e>,k1 |- t_arg1 ~= t_arg'1 .. <E_k,E_a,E_r,E_e>,kn |- t_argn ~= t_arg'n ------------------------------------------------------------- :: app -<E_k,E_a,E_r,E_e> |- x <t_arg1 .. t_argn> ~= x <t_arg'1 .. t_arg'n> +defn +G |-i id => typ :: :: infer_id :: infer_id_ +{{ com Infer type of indentifier }} +{{ tex [[G]] \vdash_i [[id]] \Rightarrow [[typ]] }} +by ------------------------------------------------------------- :: atom -E_d |- atom<ne> ~= range<ne1 ne2> +G(id) = local mut typ +---------------------- :: local +G |-i id => typ ------------------------------------------------------------- :: atom2 -E_d |- range<ne1 ne2> ~= atom<ne> -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u -<E_k,E_a,E_r,E_e> |- x <t_arg1 .. t_argn> ~= u [ t_arg'1/tid1 .. t_arg'm/tidm ] ------------------------------------------------------------- :: appAbbrev -<E_k,E_a,E_r,E_e> |- x < t_arg1 .. t_argn> ~= x' <t_arg'1 .. t_arg'm> +G(id) = enum typ +---------------------- :: enum +G |-i id => typ -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidn|->kinfn}, S_N, tag, u -<E_k,E_a,E_r,E_e> |- u [ t_arg1/tid1 .. t_argn/tidn ] ~= x <t_arg'1 .. t_arg'm> ------------------------------------------------------------- :: appAbbrev2 -<E_k,E_a,E_r,E_e> |- x' < t_arg1 .. t_argn> ~= x <t_arg'1 .. t_arg'm> -E_d |- t ~= u ------------------------------------------------------------- :: register -E_d |- register<t> ~= u +G(id) = register typ +---------------------- :: register +G |-i id => typ -E_d |- t ~= u ------------------------------------------------------------- :: reg -E_d |- reg<t> ~= u +G(id) = union typquant typ +------------------------------------- :: union +G |-i id => typ defn -E_d , k |- t_arg ~= t_arg' :: :: targconforms :: targconforms_ -{{ lemwcf witness type check_targeq_witness; check check_targeq_w_check; }} +G |-f exp . id => typ :: :: infer_field :: infer_field_ +{{ tex [[G]] \vdash_f [[exp]] . [[id]] \Rightarrow [[typ]] }} by -E_d |- t ~= t' ------------------------------------------------------------- :: typ -E_d, K_Typ |- t ~= t' - -E_d |-n ne ~= ne' ------------------------------------------------------------ :: nexp -E_d, K_Nat |- ne ~= ne' -defn -E_d |-c t ~= t' :: :: conforms_to_upto_coerce :: conforms_to_upto_coerce_ -{{ com Relate t and t' when t can be used where t' is expected upto applying coercions to t }} -by +G |- exp => typ1 +G ( typ1 ) = register [ id2 ] +G ( id2 ) = (base,top,ranges) +ranges ( id ) = vec_typ +---------------------------- :: register +G |-f exp . id => vec_typ -E_d |- t ~= t' -------------------------------------------------------------- :: base -E_d |-c t ~= t' -E_d |-n ne2 ~= one -------------------------------------------------------------- :: bitToVec -E_d |-c bit ~= vector<ne ne2 order bit> -E_d |-n ne2 ~= one -------------------------------------------------------------- :: vecToBit -E_d |-c vector<ne ne2 order bit> ~= bit +G |- exp => typ1 +G ( typ1 , id ) = typ +---------------------------- :: record +G |-f exp . id => typ -------------------------------------------------------------- :: vecToAtom -E_d |-c vector<ne ne2 order bit> ~= atom<ne3> -------------------------------------------------------------- :: vecToRange -E_d |-c vector<ne ne2 order bit> ~= range<ne3 ne4> +defn +G |- exp1 => n_constraint :: :: infer_flow :: infer_flow_ +by -E_e(x) gives enumerate_map -------------------------------------------------------------- :: enumToRange -<E_k,E_a,E_r,E_e> |-c x ~= range<ne1 ne2> -E_e(x) gives enumerate_map -------------------------------------------------------------- :: rangeToEnum -<E_k,E_a,E_r,E_e> |-c range<ne1 ne2> ~= x +G |- x => atom < nexp1 > +G |- y => atom < nexp2 > +---------------------------- :: lteq +G |- :E_app: lteq_atom_atom ( x , y ) => nexp1 <= nexp2 -E_e(x) gives enumerate_map -------------------------------------------------------------- :: enumToAtom -<E_k,E_a,E_r,E_e> |-c x ~= atom<ne> -E_e(x) gives enumerate_map -------------------------------------------------------------- :: atomToEnum -<E_k,E_a,E_r,E_e> |-c atom<ne> ~= x +G |- x => atom < nexp1 > +G |- y => atom < nexp2 > +---------------------------- :: gteq +G |- :E_app: gteq_atom_atom ( x , y ) => nexp1 >= nexp2 -E_d |-c t1 ~= u1 .... E_d |-c tn ~= un ------------------------------------------------------------- :: tup -E_d |-c (t1,....,tn) ~= (u1,....,un) +G |- x => atom < nexp1 > +G |- y => atom < nexp2 > +---------------------------- :: lt +G |- :E_app: lt_atom_atom ( x , y ) => nexp1 + numOne <= nexp2 -E_k(x) gives K_Lam (k1 .. kn -> K_Typ) -<E_k,E_a,E_r,E_e>,k1 |-c t_arg1 ~= t_arg'1 .. <E_k,E_a,E_r,E_e>,kn |-c t_argn ~= t_arg'n ------------------------------------------------------------- :: app -<E_k,E_a,E_r,E_e> |-c x <t_arg1 .. t_argn> ~= x <t_arg'1 .. t_arg'n> +G |- x => atom < nexp1 > +G |- y => atom < nexp2 > +---------------------------- :: gt +G |- :E_app: lteq_atom_atom ( x , y ) => nexp1 >= nexp2 + numOne -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u -<E_k,E_a,E_r,E_e> |-c x <t_arg1 .. t_argn> ~= u [ t_arg'1/tid1 .. t_arg'm/tidm ] ------------------------------------------------------------- :: appAbbrev -<E_k,E_a,E_r,E_e> |-c x < t_arg1 .. t_argn> ~= x' <t_arg'1 .. t_arg'm> +G |- id => range <nexp1 , nexp2 > +G |- y => atom < nexp > +------------------------------------------------------------------------------- :: lt_range_atom +G |- :E_app: lt_range_atom ( id , y ) => range < nexp1 , min (nexp - 1 , nexp2 ) > -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidn|->kinfn}, S_N, tag, u -<E_k,E_a,E_r,E_e> |-c u [ t_arg1/tid1 .. t_argn/tidn ] ~= x <t_arg'1 .. t_arg'm> ------------------------------------------------------------- :: appAbbrev2 -<E_k,E_a,E_r,E_e> |-c x' < t_arg1 .. t_argn> ~= x <t_arg'1 .. t_arg'm> -E_d |-c t ~= u ------------------------------------------------------------- :: register -E_d |-c register<t> ~= u -E_d |-c t ~= u ------------------------------------------------------------- :: reg -E_d |-c reg<t> ~= u defn -E_d , k |-c t_arg ~= t_arg' :: :: targconforms_coerce :: targconforms_coerce_ + G |- exp => typ :: :: infer_exp :: infer_exp_ +{{ com Infer that type of $[[exp]]$ is $[[typ]]$ }} +{{ tex [[G]] \vdash [[exp]] \Rightarrow [[typ]] }} by -E_d |-c t ~= t' ------------------------------------------------------------- :: typ -E_d, K_Typ |-c t ~= t' -E_d |-n ne ~= ne' ------------------------------------------------------------ :: nexp -E_d, K_Nat |-c ne ~= ne' +G |- exp1 <= unit ... G |- expn <= unit +------------------------------------------ :: nondet +G |- nondet { exp1 ; ... ; expn } => unit -defn -E_d |- select ( conformsto ( t , t' ) ) of tinflist gives tinflist' :: :: selectoverload :: so_ -{{ tex [[select]]_{[[conformsto]] ([[t]],[[t']])} ([[tinflist]]) [[gives]] [[tinflist']] }} -by +G |-i id => typ +---------------- :: id +G |- id => typ -E_d |- ti ~= ti' -E_d |- tj' ~= tj -E_d |- select (full(ti,tj)) of tinf0 .. tinfm tinf'0 .. tinf'n gives empty ---------------------------------------------------------- :: full -E_d |- select (full( ti, tj)) of tinf0 .. tinfm E_k,S_N,tag, ti' -> tj' effect tinf'0 .. tinf'n gives E_k,S_N,tag,ti' -> tj' -E_d |- ti ~= ti' -E_d |- select (parm(ti,tj)) of tinf0 .. tinfm gives empty --------------------------------------------------------- :: parm -E_d |- select (parm( ti, tj)) of tinf0 .. tinfm E_k,S_N,tag,ti' -> t effect tinf'0 .. tinf'n gives E_k,S_N,tag,ti' -> t +G |-l lit => typ +---------------- :: lit +G |- lit => typ -defn -E_d , widening |- t ~< t' : t'' , S_N :: :: consistent_typ :: consistent_typ_ -{{ com t is consistent with t' if they match if t can be used where t' is needed after the constraints are solved, with no coercions needed. t'' is the consistent type when widening is required }} -by -E_k |-t t ok ------------------------------------------------------------- :: refl -<E_k,E_a,E_r,E_e>,widening |- t ~< t:t,{} - -E_d,widening |- t1 ~< t3:t4, S_N1 -E_d,widening |- t4 ~< t2: t5, S_N2 ------------------------------------------------------------- :: trans -E_d,widening |- t1 ~< t2: t5, S_N1 u+ S_N2 - -E_a(x) gives {},S_N1,tag,u -<E_k,E_a,E_r,E_e>,widening |- u ~< t:t', S_N ------------------------------------------------------------- :: abbrev -<E_k,E_a,E_r,E_e>,widening |- x ~< t : t', S_N u+ S_N1 - -E_a(x) gives {},S_N1,tag,u -<E_k,E_a,E_r,E_e>,widening |- t ~< u: t', S_N' ------------------------------------------------------------- :: abbrev2 -<E_k,E_a,E_r,E_e>,widening |- t ~< x : t', S_N u+ S_N1 - ------------------------------------------------------------- :: var -E_d,widening |- 'x ~< t:t, {} - ------------------------------------------------------------- :: var2 -E_d,widening |- t ~< 'x: t, {} - -E_d,widening |- t1 ~< u1:u'1, S_N1 .... E_d,widening |- tn ~< un:u'n, S_Nn ------------------------------------------------------------- :: tup -E_d,widening |- (t1,....,tn) ~< (u1,....,un): (u'1,....,u'n), S_N1 u+ .... u+ S_Nn +----------------------------------- :: sizeof +G |- sizeof nexp => atom < nexp > ------------------------------------------------------------ :: range -E_d,widening |- range <ne1 ne2> ~< range<ne3 ne4>: range<ne3 ne4>, { ne3 <= ne1, ne2 <= ne4 } +-------------------------------------------- :: constraint +G |- constraint n_constraint => bool ----------------------------------------------------------- :: atomRange -E_d,(nums,_) |- atom <ne> ~< range<ne1 ne2>: atom<ne>, { ne1 <= ne, ne <= ne2 } +G |-f exp . id => typ +------------------------ :: field +G |- exp . id => typ ----------------------------------------------------------- :: atom -E_d,(none,_) |- atom <ne1> ~< atom<ne2>: atom<ne2>, { ne1 = ne2 } +G |- exp1 => typ1 .... G |- expn => typn +---------------------------------------------------------- :: tuple +G |- ( exp1 , .... , expn ) => (typ1 , .... , typn ) -num1 lt num2 ----------------------------------------------------------- :: atomWidenConst -E_d,(nums,_) |- atom <num1> ~< atom<num2>: range<num1 num2>, {} -num2 lt num1 ---------------------------------------------------------- :: atomWidenConst2 -E_d,(nums,_) |- atom <num1> ~< atom<num2>: range<num2 num1>, {} ----------------------------------------------------------- :: rangeAtom -E_d,widening |- range<ne1 ne2> ~< atom<'x>: atom<'x>, { ne1 <= 'x, 'x <= ne2 } -E_d,(nums,none) |- t ~< t': t'', S_N ----------------------------------------------------------- :: vector -E_d,(_,none) |- vector <ne1 ne2 order t> ~< vector <ne3 ne4 order t'>: vector<ne3 ne4 order t''>, {ne2=ne4, ne1=ne3} u+ S_N +G |- lexp := exp => typ -| D +-------------------- :: assign +G |- lexp := exp => typ -E_d,(nums,none) |- t ~< t': t'', S_N ----------------------------------------------------------- :: vectorWiden -E_d,(_,vectors) |- vector <ne1 ne2 order t> ~< vector <ne3 ne4 order t'>: vector<ne3 ne4 order t''>, {ne2=ne4} u+ S_N -E_k(x) gives K_Lam (k1 .. kn -> K_Typ) -<E_k,E_a,E_r,E_e>,widening,k1 |- t_arg1 ~< t_arg'1,S_N1 .. <E_k,E_a,E_r,E_e>,widening,kn |- t_argn ~< t_arg'n,S_Nn ------------------------------------------------------------- :: app -<E_k,E_a,E_r,E_e>,widening |- x <t_arg1 .. t_argn> ~< x <t_arg'1 .. t_arg'n>:x<t_arg'1 .. t_arg'n>, S_N1 u+ .. u+ S_Nn -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u -<E_k,E_a,E_r,E_e>,widening |- x <t_arg1 .. t_argn> ~< u [ t_arg'1/tid1 .. t_arg'm/tidm ]: t ,S_N2 ------------------------------------------------------------- :: appAbbrev -<E_k,E_a,E_r,E_e>,widening |- x < t_arg1 .. t_argn> ~< x' <t_arg'1 .. t_arg'm>: x'<t_arg'1 .. t_arg'm>, S_N u+ S_N2 +---------------------------- :: record_update +G |- lexp . id := exp => typ -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u -<E_k,E_a,E_r,E_e>,widening |- u [ t_arg'1/tid1 .. t_arg'm/tidm ] ~< x <t_arg1 .. t_argn>: t ,S_N2 ------------------------------------------------------------- :: appAbbrev2 -<E_k,E_a,E_r,E_e>,widening |- x' <t_arg'1 .. t_arg'm> ~< x < t_arg1 .. t_argn> :x<t_arg1 .. t_argn>, S_N u+ S_N2 -defn -E_d , widening , k |- t_arg ~< t_arg' , S_N :: :: targ_consistent :: targ_consistent_ -by +G |- exp <= typ +----------------------- :: cast +G |- ( typ ) exp => typ -E_d,widening |- t ~< t': t'', S_N ------------------------------------------------------------- :: typ -E_d,widening, K_Typ |- t ~< t',S_N ------------------------------------------------------------ :: nexp -E_d,widening, K_Nat |- ne ~< ne',{ne=ne'} -defn -E_d , widening, t' |- exp : t gives t'' , exp' , S_N , effect :: :: coerce_typ :: coerce_typ_ -{{ lemwcf witness type coerce_typ_witness; check coerce_typ_w_check; }} -by +G |- :E_app: id ( exp1 , exp2 ) => typ +-------------------------------- :: app_infix +G |- exp1 id exp2 => typ -E_d, widening, u1 |- id1 : t1 gives u1, exp1, S_N1,effect1 .. E_d,widening, un|- idn: tn gives un,expn, S_Nn,effectn -exp' == switch exp { case (id1, .., idn) -> (exp1,..,expn) } --------------------------------------- :: tuple -E_d, widening, (u1 , .. , un) |- exp : (t1 , .. , tn) gives (u1 , .. , un), exp', S_N1 u+ .. u+ S_Nn, pure - -E_d,(nums,vectors) |- u ~< t: t',S_N -exp' == (annot) exp -------------------------------------------------- :: vectorUpdateStart -E_d, widening, vector< ne1 ne2 order t > |- exp : vector <ne3 ne4 order u> gives vector <ne3 ne4 order t'>, exp', S_N u+ {ne2=ne4}, pure - -E_d, (none,none) |- u ~< bit:bit, S_N -exp' == to_num exp --------------------------------------------------- :: toNum -E_d,widening, range<ne1 ne2> |- exp : vector <ne3 ne4 order u> gives range<ne1 ne2>, exp', S_N u+ {ne1=zero, ne2 >= 2**ne4}, pure - -exp' == to_vec exp --------------------------------------- :: fromNum -E_d,widening, vector<ne1 ne2 order bit> |- exp: range<ne3 ne4> gives vector<ne1 ne2 order bit>,exp', {ne3 = zero, ne4 <= 2** ne2}, pure - -E_d |- typ ~> t -exp' == (typ) exp -E_d,widening, u |- exp':t gives t',exp'', S_N, pure --------------------------------------- :: readReg -E_d,widening, u |- exp : register<t> gives t', exp'', S_N, {rreg} - -exp' == :E_tup_app: msb(exp) --------------------------------------- :: accessVecBit -E_d,widening, bit |- exp : vector<ne1 ne2 order bit> gives bit,exp', { ne1=one},pure - -E_d,widening |- range<zero one> ~< range<ne1 ne2>: t,S_N -exp' == switch exp { case bitzero -> numZero case bitone -> numOne} --------------------------------------- :: bitToNum -E_d,widening, range<ne1 ne2> |- exp : bit gives range<ne1 ne2>, exp',S_N,pure - -E_d,widening |- range<ne1 ne2> ~< range<zero one>: t,S_N -exp' == switch exp { case numZero -> bitzero case numOne -> bitone } -------------------------------------- :: numToBit -E_d, widening, bit |- exp : range<ne1 ne2> gives bit, exp',S_N,pure - -E_d,(nums,none) |- atom<ne> ~< range<zero one>: t,S_N -exp' == switch exp { case numZero -> bitzero case numOne -> bitone } -------------------------------------- :: numToBitAtom -E_d,widening, bit |- exp : atom<ne> gives bit, exp',S_N,pure - -E_e(x) gives { </numi |-> idi//i/> } -exp' == switch exp { </case numi -> idi//i/> } -ne3 == count( </numi//i/>) ------------------------------------------------- :: toEnumerate -<E_k,E_a,E_r,E_e>,widening, x |- exp : range<ne1 ne2> gives x,exp', {ne1<=zero,ne2<=ne3},pure - -E_e(x) gives { </numi |-> idi//i/> } -exp' == switch exp { </case idi -> numi//i/> } -ne3 == count( </numi//i/>) -<E_k,E_a,E_r,E_e>,(nums,none) |- range<zero ne3> ~< range<ne1 ne2>:t, S_N ------------------------------------------------- :: fromEnumerate -<E_k,E_a,E_r,E_e>,widening,range<ne1 ne2> |- exp: x gives range<zero ne3>, exp', S_N,pure - -E_d,widening |- t ~< u: u', S_N --------------------------------------- :: eq -E_d,widening, u |- exp: t gives u', exp, S_N,pure +--------------------------------------- :: app +G |- :E_app: id (exp1 , .. , expn ) => typ -defns -check_lit :: '' ::= - -defn -widening , t |- lit : t' => exp , S_N :: :: check_lit :: check_lit_ -{{ com Typing literal constants, coercing to expected type t }} -by - - ------------------------------------------------------------ :: num -widening, range <ne ne'> |- num : atom < num > => num , { ne <= num, num <= ne' } - ------------------------------------------------------------ :: numToVec -widening, vector <ne ne' order bit> |- num : atom < num > => to_vec num , { num + one <= 2**ne' } +G |- exp1 => bool +G |- exp2 => unit +------------------------------- :: while_loop +G |- while exp1 do exp2 => unit - ------------------------------------------------------------ :: numbitzero -widening, bit |- numZero : atom < zero > => bitzero, {} +G |- exp1 => unit +G |- exp2 => bool +------------------------------- :: until_loop +G |- repeat exp1 until exp2 => unit - ------------------------------------------------------------ :: numbitone -widening, bit |- numOne : atom < one > => bitone, {} - - ------------------------------------------------------------- :: string -widening, string |- :L_string: string : :T_string_typ: string => :E_lit: string, {} +G |- exp1 => range <nexp1,nexp1'> +G |- exp2 => range <nexp2,nexp2'> +G |= nexp1' <= nexp2 +G |- exp3 <= int +G |- exp4 => unit +----------------------------------------------------------------------- :: for_inc +G |- foreach ( id from exp1 to exp2 by exp3 in inc ) exp4 => unit - ne == bitlength(hex) - ------------------------------------------------------------ :: hex -widening, vector<ne1 ne2 order bit> |- hex : vector< ne1 ne order bit> => hex, {ne=ne2} +G |- exp1 => range <nexp1,nexp1'> +G |- exp2 => range <nexp2,nexp2'> +G |= nexp2' <= nexp1 +G |- exp3 <= int +G |- exp4 => unit +----------------------------------------------------------------------- :: for_dec +G |- foreach ( id from exp1 to exp2 by exp3 in dec ) exp4 => unit -ne == bitlength(bin) - ------------------------------------------------------------ :: bin -widening,vector<ne1 ne2 order bit> |- bin : vector< ne1 ne order bit> => bin, {ne=ne2} - ------------------------------------------------------------ :: unit -widening, unit |- () : unit => unit, {} +G |- foreach ( id from exp1 to exp2 by exp3 in inc) exp4 => typ +----------------------------------------------------------------------- :: forup +G |- foreach ( id from exp1 to exp2 by exp3 ) exp4 => typ - ------------------------------------------------------------ :: bitzero -widening, bit |- bitzero : bit => bitzero, {} - ------------------------------------------------------------ :: bitone -widening, bit |- bitone : bit => bitzero, {} +G |- foreach ( id from exp1 to exp2 by numOne in inc) exp3 => typ +----------------------------------------------------------------------- :: forupbyone +G |- foreach ( id from exp1 to exp2 ) exp3 => typ ------------------------------------------------------------- :: undef -widening, t |- undefined : t => undefined, {} -defns -check_pat :: '' ::= - -defn -E , t |- pat : t' gives pat' , E_t , S_N :: :: check_pat :: check_pat_ -{{ com Typing patterns, building their binding environment }} -by +G |- foreach ( id from exp1 to exp2 by exp3 in dec) exp4 => typ +--------------------------------------------------------------------------- :: fordown +G |- foreach ( id from exp1 downto exp2 by exp3 ) exp4 => typ -lit NOTEQ undefined -(none,none),t |- lit : u => lit',S_N -E_d,(nums,none) |- u ~< t: t', S_N' ------------------------------------------------------------- :: lit -<E_t,E_d>, t |- lit : t' gives lit', {}, S_N u+ S_N' - ------------------------------------------------------------- :: wild -E, t |- _ : t gives _, {}, {} - -E,t |- pat : u gives pat',E_t1,S_N -id NOTIN dom(E_t1) ------------------------------------------------------------- :: as -E,t |- (pat as id) : u gives (pat' as id), (E_t1 u+ {id|->t}),S_N - -E_t(id) gives {}, {}, Default, t' -<E_t,E_d>,t' |- pat : t gives pat', E_t1,S_N -E_d,(none,none) |- t' ~< u : u', S_N' ------------------------------------------------------------- :: asDefault -<E_t,E_d>,u |- (pat as id) : t gives (pat' as id), (E_t1 u+ {id|->t'}),S_N u+ S_N' - -E_d |- typ ~> t -<E_t,E_d>,t |- pat : t gives pat',E_t1,S_N ------------------------------------------------------------- :: typ -<E_t,E_d>,u |- (typ) pat : t gives pat',E_t1,S_N - -E_t(id) gives {tid1 |-> kinf1 , .. , tidm|-> kinfm}, S_N, Ctor, (u'1,..,u'n) -> x < t_arg1 .. t_argm > pure -(u1,..,un) -> x <t_args'> pure == (u'1,..,u'n) -> x <t_args> pure [t_arg1/tid1 .. t_argm/tidm] -<E_t,E_d>,u1 |- pat1 : t1 gives pat'1,E_t1,S_N1 .. <E_t,E_d>,un |- patn : tn gives pat'n,E_tn,S_Nn -disjoint doms(E_t1,..,E_tn) -E_d,(nums,vectors) |- x <t_args'> ~< t: t', S_N ------------------------------------------------------------- :: constr -<E_t,E_d>,t |- id(pat1, .., patn) : x<t_args'> gives id(pat'1, ..,pat'n), u+ E_t1 .. E_tn, S_N u+ S_N1 u+ .. u+ S_Nn - - -E_t(id) gives {tid1 |-> kinf1 , .. , tidm|-> kinfm}, S_N, Ctor, unit -> x < t_arg1 .. t_argm > pure -unit -> x <t_args'> pure == unit -> x <t_args> pure [t_arg1/tid1 .. t_argm/tidm] -E_d,(nums,vectors) |- x <t_args'> ~< t: t', S_N -------------------------------------------------------------- :: identConstr -<E_t,E_d>, t |- :P_id: id : t gives :P_id: id, {}, S_N - -E_t(id) gives {},{},Default,t -E_d,(nums,vectors) |- t ~< u: u', S_N ------------------------------------------------------------- :: varDefault -<E_t,E_d>,u |- :P_id: id : t gives :P_id: id, (E_t u+ {id|->t}),S_N - ------------------------------------------------------------- :: var -<E_t,E_d>,t |- :P_id: id : t gives :P_id: id, (E_t u+ {id|->t}),{} - -E_r(</idi//i/>) gives x< t_args>, (</ti//i/>) -</<E_t,<E_k,E_a,E_r,E_e>>,ti |- pati : ui gives pat'i, E_ti,S_Ni//i/> -disjoint doms(</E_ti//i/>) -<E_k,E_a,E_r,E_e>,(nums,vectors) |- x<t_args> ~< t: t', S_N ------------------------------------------------------------- :: record -<E_t,<E_k,E_a,E_r,E_e>>,t |- { </idi = pati//i/> semi_opt } : x<t_args> gives {</idi=pat'i//i/> semi_opt }, :E_t_multi_union: u+ </E_ti//i/>, S_N u+ </S_Ni//i/> - -<E_t,E_d>,t |- pat1 : u1 gives pat'1, E_t1,S_N1 ... <E_t,E_d>,t |- patn : un gives pat'n, E_tn,S_Nn -disjoint doms(E_t1, ... ,E_tn) -E_d,(nums,vectors) |- u1 ~< t:t',S_N'1 ... E_d,(nums,vectors) |- un ~< t:t',S_N'n -ne4==length(pat1 ... patn) -S_N ==S_N1 u+ ... u+ S_Nn -S_N' == S_N'1 u+ ... u+ S_N'n ------------------------------------------------------------ :: vector -<E_t,E_d>, vector<ne1 ne2 order t> |- [ pat1, ..., patn ] : vector< ne3 ne4 order u> gives [ pat'1, ..., pat'n ], (E_t1 u+ ... u+ E_tn), S_N u+ S_N' u+ {ne2=ne4} - -<E_t,E_d>,t |- pat1 : u1 gives pat'1, E_t1,S_N1 ... <E_t,E_d>,t |- patn : un gives pat'n, E_tn,S_Nn -E_d,(nums,vectors) |- u1 ~< t:t',S_N'1 ... E_d,(nums,vectors) |- un ~< t:t',S_N'n -ne4 == length(pat1 ... patn) -disjoint doms(E_t1 , ... , E_tn) -num1 lt ... lt numn -S_N == S_N1 u+ ... u+ S_Nn -S_N' == S_N'1 u+ ... u+ S_N'n ------------------------------------------------------------ :: indexedVectorInc -<E_t,E_d>, vector<ne1 ne2 inc t> |- [ num1 = pat1 , ... , numn = patn ] : vector< ne3 ne4 inc t> gives [num1 = pat'1 , ... , numn = pat'n], (E_t1 u+ ... u+ E_tn), {ne1<=num1, ne2 >= ne4} u+ S_N1 u+ ... u+ S_Nn - -<E_t,E_d>,t |- pat1 : u1 gives pat'1, E_t1,S_N1 ... <E_t,E_d>,t |- patn : un gives pat'n, E_tn,S_Nn -E_d,(nums,vectors) |- u1 ~< t:t',S_N'1 ... E_d,(nums,vectors) |- un ~< t:t',S_N'n -ne4 == length(pat1 ... patn) -disjoint doms(E_t1 , ... , E_tn) -num1 gt ... gt numn -S_N == S_N1 u+ ... u+ S_Nn -S_N' == S_N'1 u+ ... u+ S_N'n ------------------------------------------------------------ :: indexedVectorDec -<E_t,E_d>, vector<ne1 ne2 dec t> |- [ num1 = pat1 , ... , numn = patn ] : vector< ne3 ne4 dec t> gives [num1 = pat'1 , ... , numn = pat'n], (E_t1 u+ ... u+ E_tn), {ne1>=num1, ne2 >= ne4} u+ S_N1 u+ ... u+ S_Nn - -<E_t,E_d>, vector<ne''1 ne'''1 order t> |- pat1 : vector< ne''1 ne'1 order u1> gives pat'1, E_t1,S_N1 ... <E_t,E_d>, vector<ne''n ne'''n order t> |- pat1 : vector< ne''n ne'n order u1> gives pat'n, E_tn,S_Nn -E_d,(nums,vectors) |- u1 ~< t:t',S_N'1 ... E_d,(nums,vectors) |- un ~< t:t',S_N'n -disjoint doms(E_t1 , ... , E_tn) -S_N == S_N1 u+ ... u+ S_Nn -S_N' == S_N'1 u+ ... u+ S_N'n ------------------------------------------------------------ :: vectorConcat -<E_t,E_d>, vector<ne1 ne2 order t> |- pat1 : ... : patn : vector<ne1 ne4 order t> gives pat'1 : ... : pat'n, (E_t1 u+ ... u+ E_tn),{ne'1 + ... + ne'n <= ne2} u+ S_N u+ S_N' - -E,t1 |- pat1 : u1 gives pat'1,E_t1,S_N1 .... E,tn |- patn : un gives pat'n,E_tn,S_Nn -disjoint doms(E_t1,....,E_tn) ------------------------------------------------------------- :: tup -E,(t1, .... , tn) |- (pat1, ...., patn) : (u1 , .... , un) gives (pat'1, .... , pat'n), (E_t1 u+ .... u+ E_tn),S_N1 u+ .... u+ S_Nn - -<E_t,E_d>,t |- pat1 : u1 gives pat'1,E_t1,S_N1 .. <E_t,E_d>,t |- patn : un gives pat'n,E_tn,S_Nn -disjoint doms(E_t1,..,E_tn) -E_d,(nums,none) |- u1 ~< t:t',S_N'1 .. E_d,(nums,none) |- un ~< t:t',S_N'n -disjoint doms(E_t1 , .. , E_tn) -S_N == S_N1 u+ .. u+ S_Nn -S_N' == S_N'1 u+ .. u+ S_N'n ------------------------------------------------------------- :: list -<E_t,E_d>, list<t> |- [||pat1, .., patn ||] : list< t> gives [|| pat'1, .. , pat'n ||],(E_t1 u+ .. u+ E_tn),S_N u+ S_N' +G |- foreach ( id from exp1 to exp2 by numOne in dec) exp3 => typ +------------------------------------------------------------------------- :: fordownbyone +G |- foreach ( id from exp1 downto exp2 ) exp3 => typ -defns -check_exp :: '' ::= - -defn -E , t , widening |- exp : t' gives exp' , I , E_t :: :: check_exp :: check_exp_ -{{ com Typing expressions, collecting nexp constraints, effects, and new bindings }} -by - -E_t(id) gives {tid0|->kinf0, .., tidn |-> kinfn}, {},Ctor, unit -> x <t_args> pure -u == x<t_args> [ t_arg0/tid0 .. t_argn/tidn] -E_d,widening |- u ~< t:t',S_N ------------------------------------------------------------ :: unaryCtor -<E_t,E_d>,t,widening |- id : x gives id, <S_N,pure>,{} - -E_t(id) gives {}, {},tag,u -E_d,widening,t |- id : u gives t', exp, S_N, effect ------------------------------------------------------------- :: localVar -<E_t,E_d>,t,widening |- id : u gives id, <S_N,effect>,{} - -E_t(id) gives {tid1|->kinf1, .., tidn |-> kinfn}, S_N,tag,u' -u == u'[t_arg1/tid1 .. t_argn/tidn] -E_d,widening,t |- id : u gives t', exp, S_N', effect ------------------------------------------------------------- :: otherVar -<E_t,E_d>,t,widening |- id : u gives id,<S_N u+ S_N' ,effect>,{} - -E_t(id) gives {tid0|->kinf0, .., tidn |-> kinfn}, {},Ctor, t'' -> x <t_args> pure -t' -> u pure == t'' -> x<t_args> pure [ t_arg0/tid0 .. t_argn/tidn] -E_d,widening |- u ~< t:t',S_N -<E_t,E_d>,t,widening |- exp : u' gives exp, <S_N',effect>,E_t' ------------------------------------------------------------- :: ctor -<E_t,E_d>,t,widening |- :E_app: id(exp) : t gives :E_app: id(exp'), <S_N u+ S_N, effect>,{} - -E_t(id) gives {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u -u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect -ui == ( implicit<ne>, t0 , .. , tm ) -<E_t,E_d>,(t0,..,tm),widening |- (exp0,..,expm) : ui' gives (exp0',..,expm'),I,E_t' -E_d,widening,t |- :E_app: id (annot, exp'0, .., exp'm) : uj gives uj', exp'',S_N',effect' ------------------------------------------------------------- :: appImplicit -<E_t,E_d>,t,widening |- :E_app: id(exp0,..,expm) : uj gives exp'', I u+ <S_N,effect>u+ <S_N',effect'>, E_t - - -E_t(id) gives {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u -u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect -<E_t,E_d>,ui,widening |- exp : ui' gives exp',I,E_t' -E_d,widening,t |- :E_app: id (exp') : uj gives uj', exp'',S_N',effect' ------------------------------------------------------------- :: app -<E_t,E_d>,t,widening |- :E_app: id(exp) : uj gives exp'', I u+ <S_N,effect>u+ <S_N',effect'>, E_t - -E_t(id) gives overload {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u : tinf1 ... tinfn -u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect -<E_t,E_d>,ui,widening |- exp : ui' gives exp',I,E_t' -E_d |- select (full( ui', t)) of tinf1 ... tinfn gives tinf -<({id |-> tinf} u+ E_t), E_d>, t,widening |- :E_app: id (exp) : t' gives exp'',I', E_t'' ------------------------------------------------------------- :: appOverload -<E_t,E_d>,t,widening |- :E_app: id(exp) : uj gives exp'', I u+ I' u+ <S_N,effect>u+ <S_N',effect'>, E_t - -E_t(id) gives {tid0 |-> kinf0, .. ,tidn |-> kinfn}, S_N, tag, u -u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect -<E_t,E_d>,ui,widening |- (exp1,exp2) : ui' gives (exp1', exp2'), I,E_t' -E_d,widening,t |- :E_app_infix: exp1' id exp2' : uj gives uj', exp, S_N', effect' ------------------------------------------------------------- :: infix_app -<E_t,E_d>,t,widening |- :E_app_infix: exp1 id exp2 : t gives exp, I u+ <S_N, effect> u+ <S_N',effect'>, E_t - -E_t(id) gives overload {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u : tinf1 ... tinfn -u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect -<E_t,E_d>,ui,widening |- (exp1,exp2) : ui' gives (exp1', exp2'), I,E_t' -E_d |- select (full( ui', t)) of tinf1 ... tinfn gives tinf -<({id |-> tinf} u+ E_t), E_d>, t, widening |- :E_app_infix: exp1 id exp2 : t' gives exp, I',E_t'' ------------------------------------------------------------- :: infix_appOverload -<E_t,E_d>,t,widening |- :E_app_infix: exp1 id exp2 : t gives exp, I u+ I u+ <S_N, effect> u+ <S_N',effect'>, E_t - - -E_r(</idi//i/>) gives x<t_args>, </ti//i/> -</ <E_t,<E_k,E_a,E_r,E_e>>,ti,widening |- expi : ui gives exp'i,<S_Ni,effecti>,E_t//i/> -</<E_k,E_a,E_r,E_e>,widening |- ui ~< ti: t'i,S_N'i//i/> -S_N == u+ </S_Ni//i/> -S_N' == u+ </S_N'i//i/> ------------------------------------------------------------- :: record -<E_t,<E_k,E_a,E_r,E_e>>,t,widening |- { </idi = expi//i/> semi_opt} : x<t_args> gives{ </idi=exp'i//i/> semi_opt}, u+ <S_N u+ S_N', u+ </effecti//i/>>, {} - -<E_t,<E_k,E_a,E_r,E_e>>,t,widening |- exp : x<t_args> gives exp', I,E_t -E_r(x<t_args>) gives </ id'n:t'n//n/> -</ <E_t,<E_k,E_a,E_r,E_e>>,ti,widening |- expi : ui gives expi',Ii,E_t//i/> -</idi:ti//i/> SUBSET </id'n : t'n//n/> -</<E_k,E_a,E_r,E_e>,widening |- ui ~< ti: t''i,S_N'i//i/> ------------------------------------------------------------- :: recup -<E_t,<E_k,E_a,E_r,E_e>> ,t,widening |- { exp with </idi = expi//i/> semi_opt } : x<t_args> gives {exp' with </idi = exp'i//i/>}, I u+ </Ii//i/>, E_t - -<E_t,E_d>,t,(nums,none) |- exp1 : u1 gives exp'1,I1,E_t' ... <E_t,E_d>,t,(nums,none) |- expn : un gives exp'n,In,E_t' -E_d,(nums,none) |- u1 ~< t: t', S_N1 ... E_d,(nums,none) |- un ~< t: t', S_Nn -length(exp1 ... expn) == ne -S_N == {ne=ne2} u+ S_N1 u+ ... u+ S_Nn ------------------------------------------------------------- :: vector -E, vector<ne1 ne2 order t>, widening |- [ exp1 , ... , expn ] : vector<ne1 num order t> gives [exp'1,...,exp'n], <S_N,pure> u+ I1 u+ ... u+ In , E_t - -E, vector<ne ne' order t>,(nums,none) |- exp1 : vector<ne1 ne1' inc u> gives exp'1,I1,E_t -E, range<ne2 ne2'>,(none,vectors) |- exp2 : range<ne3 ne3'> gives exp'2, I2,E_t -------------------------------------------------------------- :: vectorgetInc -E, t,widening |- :E_vector_access: exp1 [ exp2 ] : u gives exp'1 [ exp'2], I1 u+ I2 u+ <{ne1<=ne3,ne3+ne3'<=ne1+ne1'},pure>,E_t - -E, vector<ne ne' order t>,(nums,none) |- exp1 : vector<ne1 ne1' dec u> gives exp'1,I1,E_t -E, range<ne2 ne2'>,(none,vectors) |- exp2 : range<ne3 ne3'> gives exp'2, I2,E_t -------------------------------------------------------------- :: vectorgetDec -E, t,widening |- :E_vector_access: exp1 [ exp2 ] : u gives exp'1 [ exp'2], I1 u+ I2 u+ <{ne1>=ne3,ne3+(-ne3')<=ne1+(-ne1')},pure>,E_t - -E, vector<ne1 ne'1 inc t>,(nums,none) |- exp1 : vector<ne2 ne'2 inc u> gives exp'1, I1,E_t -E, range<ne3 ne3'>,(none,vectors) |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t -E,range <ne5 ne5'>,(none,vectors) |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t -------------------------------------------------------------- :: vectorsubInc -E, vector<ne ne' inc t>,widening |- :E_vector_subrange: exp1[ exp2 .. exp3 ] : vector<ne7 ne'7 inc u> gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne >= ne4, ne <= ne'4,ne'<=ne4+ne'6,ne4 <= ne2, ne4+ne6' <= ne'2},pure>,E_t - -E, vector<ne1 ne'1 dec t>,(nums,none) |- exp1 : vector< ne2 ne'2 dec u> gives exp'1, I1,E_t -E, range<ne3 ne3'>,(none,vectors) |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t -E,range <ne5 ne5'>,(none,vectors) |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t -------------------------------------------------------------- :: vectorsubDec -E, vector<ne ne' dec t>,widening |- :E_vector_subrange: exp1[ exp2 .. exp3 ] : vector<ne7 ne'7 dec u> gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne <= ne4, ne >= ne'4,ne'<=ne'6+(-ne4),ne4' >= ne2, ne'6+(-ne4) <= ne'2},pure>,E_t - -E, vector<ne ne' inc t>,(nums,none) |- exp : vector< ne1 ne2 inc u> gives exp',I,E_t -E, range<ne'1 ne'2>,(none,vectors) |- exp1 : range<ne3 ne4> gives exp'1,I1,E_t -E,t,(nums,vectors) |- exp2 : u gives exp'2,I2,E_t ------------------------------------------------------------- :: vectorupInc -E, vector<ne ne' inc t>,widening |- [ exp with exp1 = exp2 ] : vector< ne1 ne2 inc u> gives [exp' with exp'1 = exp'2], I u+ I1 u+ I2 u+ <{ne1 <= ne3, ne2 >= ne4},pure>,E_t - -E, vector<ne ne' dec t>,(nums,none) |- exp : vector <ne1 ne2 dec u> gives exp',I,E_t -E, range<ne'1 ne'2>,(none,vectors) |- exp1 : range<ne3 ne4> gives exp'1,I1,E_t -E,t,(nums,vectors) |- exp2 : u gives exp'2,I2,E_t ------------------------------------------------------------- :: vectorupDec -E, vector<ne ne' dec t>,widening |- [ exp with exp1 = exp2 ] : vector< ne1 ne2 dec u> gives [exp' with exp'1 = exp'2], I u+ I1 u+ I2 u+ <{ne1 >= ne3, ne2 >= ne4},pure>,E_t - -E,vector<ne1 ne2 order t>,(nums,none) |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t -E,atom<ne5>,(none,vectors) |- exp1 : atom<ne6> gives exp1',I1,E_t -E,atom<ne7>,(none,vectors) |- exp2 : atom<ne8> gives exp2', I2,E_t -E,vector<ne9 ne10 inc t>,(nums,vectors) |- exp3 : vector <ne11 ne12 inc u> gives exp3',I3,E_t -I4 == <{ ne3 <= ne5, ne3+ne4 <= ne7, ne12 = ne8 + (-ne6) , ne6 + one <= ne8},pure> ------------------------------------------------------------- :: vecrangeupInc -E,vector<ne1 ne2 order t>,widening |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 inc u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t - -E,vector<ne1 ne2 order t>,(nums,none) |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t -E,atom<ne5>,(none,vectors) |- exp1 : atom<ne6> gives exp1',I1,E_t -E,atom<ne7>,(none,vectors) |- exp2 : atom<ne8> gives exp2', I2,E_t -E,u,(nums,vectors) |- exp3 : u' gives exp3',I3,E_t -I4 == <{ ne3 <= ne5, ne3+ne4 <= ne7 },pure> ------------------------------------------------------------- :: vecrangeupvalueInc -E,vector<ne1 ne2 order t>,widening |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 inc u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t - -E,vector<ne1 ne2 order t>,(nums,none) |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t -E,atom<ne5>,(none,vectors) |- exp1 : atom<ne6> gives exp1',I1,E_t -E,atom<ne7>,(none,vectors) |- exp2 : atom<ne8> gives exp2', I2,E_t -E,vector<ne9 ne10 dec t>,(nums,vectors) |- exp3 : vector <ne11 ne12 dec u> gives exp3',I3,E_t -I4 == <{ ne5 <= ne3, ne3+(-ne4) <= ne6+(-ne8), ne8+one<=ne6 },pure> ------------------------------------------------------------- :: vecrangeupDec -E,vector<ne1 ne2 order t>,widening |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 dec u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t - -E,vector<ne1 ne2 order t>,(nums,none) |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t -E,atom<ne5>,(none,vectors) |- exp1 : atom<ne6> gives exp1',I1,E_t -E,atom<ne7>,(none,vectors) |- exp2 : atom<ne8> gives exp2', I2,E_t -E,u,(nums,vectors) |- exp3 : u' gives exp3',I3,E_t -I4 == <{ ne5 <= ne3, ne3+(-ne4) <= ne6+(-ne8), ne8+one<=ne6 },pure> ------------------------------------------------------------- :: vecrangeupvalueDec -E,vector<ne1 ne2 order t>,widening |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 dec u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t - -E_r (x<t_args>) gives </idi : ti//i/> id : u </id'j : t'j//j/> -<E_t,<E_k,E_a,E_r,E_e>>,t'',widening |- exp : x< t_args> gives exp', I,E_t -E_d,widening,t |- exp'.id : u gives t', exp1', S_N', effect ------------------------------------------------------------- :: field -<E_t,<E_k,E_a,E_r,E_e>>,t,widening |- exp.id : u gives exp1',I u+ <S_N',effect>,E_t - -<E_t,E_d>,t'',widening |- exp : u gives exp',I,E_t -</<E_t,E_d>,u |- pati : u'i gives pat'i,E_ti,S_Ni//i/> -</<(E_t u+ E_ti),E_d>,t,widening |- expi : u''i gives exp'i,Ii,E_t'i//i/> ------------------------------------------------------------- :: case -<E_t,E_d>,t,widening |- switch exp { </case pati -> expi//i/> }: u gives switch exp' { </case pat'i -> exp'i//i/> }, I u+ </Ii u+ <S_Ni,pure>//i/>, E_t - -<E_t,E_d>,t'',widening |- exp : u gives exp',I,E_t -E_d |- typ ~> t' -E_d,widening,t' |- exp' : u gives u', exp'', S_N,effect -E_d,widening,t |- exp'' : t' gives u'', exp''', S_N', effect' ------------------------------------------------------------- :: typed -<E_t,E_d>,t,widening |- (typ) exp : t gives exp''',I u+ <S_N u+ S_N',effect u+ effect'>,E_t - -<E_t,E_d> |- letbind gives letbind', E_t1, S_N, effect, {} -<(E_t u+ E_t1),E_d>,t,widening |- exp : u gives exp', I2, E_t2 ------------------------------------------------------------- :: let -<E_t,E_d>,t,widening |- letbind in exp : t gives letbind' in exp', <S_N,effect> u+ I2, E_t - -E,t1,widening |- exp1 : u1 gives exp1',I1,E_t1 .... E,tn,widening |- expn : un gives expn',In,E_tn ------------------------------------------------------------- :: tup -E,(t1, ...., tn),widening |- (exp1, .... , expn) : (u1 , .... , un) gives (exp1', ...., expn'), I1 u+ .... u+ In,E_t - -<E_t,E_d>,t,(nums,none) |- exp1 : u1 gives exp1', I1,E_t1 .. <E_t,E_d>,t,(nums,none) |- expn : un gives expn', In,E_tn -E_d,(nums,none) |- u1 ~< t:t',S_N1 .. E_d,(nums,none) |- un ~< t:t',S_Nn ------------------------------------------------------------- :: list -<E_t,E_d>,list<t>,widening |- [||exp1, .., expn ||] : list<u> gives [|| exp1', .., expn' ||], <S_N1 u+ .. u+ S_Nn,pure> u+ I1 u+ .. u+ In, E_t - -E,bit,widening |- exp1 : bit gives exp1',I1,E_t' -E,t,widening |- exp2 : u1 gives exp2',I2,E_t2 -E,t,widening |- exp3 : u2 gives exp3',I3,E_t3 -E_d,widening |- u1 ~< t:t',S_N1 -E_d,widening |- u2 ~< t:t',S_N2 ------------------------------------------------------------- :: if -<E_t,E_d>,t,widening |- if exp1 then exp2 else exp3 : u gives if exp1' then exp2' else exp3', <S_N1 u+ S_N2,pure> u+ I1 u+ I2 u+ I3,(E_t2 inter E_t3) - -<E_t,E_d>,range<ne1 ne2>,widening |- exp1 : range< ne7 ne8> gives exp1', I1,E_t -<E_t,E_d>,range<ne3 ne4>,widening |- exp2 : range< ne9 ne10> gives exp2', I2,E_t -<E_t,E_d>,range<ne5 ne6>,widening |- exp3 : range< ne11 ne12> gives exp3',I3,E_t -<(E_t u+ {id |-> range< ne1 ne4>}),E_d>,unit,widening |- exp4 : t gives exp4',I4,E_t' ------------------------------------------------------------ :: for -<E_t,E_d>,unit,widening |- foreach (id from exp1 to exp2 by exp3) exp4 : t gives foreach (id from exp1' to exp2' by exp3') exp4', I1 u+ I2 u+ I3 u+ I4 u+ <{ne1 <= ne3+ne4},pure>,E_t - -E,t,widening |- exp1 : u gives exp1',I1,E_t -E,list<t>,widening |- exp2 : list<u> gives exp2',I2,E_t ------------------------------------------------------------- :: cons -E,list<t>,widening |- exp1 :: exp2 : list<u> gives exp1'::exp2', I1 u+ I2,E_t - -widening,t |- lit : u => exp,S_N ------------------------------------------------------------- :: lit -E,t,widening |- lit : u gives exp,<S_N,pure>,E_t - -<E_t,E_d>,unit,widening |- exp : unit gives exp', I, E_t1 ------------------------------------------------------------- :: blockbase -<E_t,E_d>,unit,widening |- { exp } : unit gives {exp'}, I, E_t - -<E_t,E_d>,unit,widening |- exp : unit gives exp', I1, E_t1 -<(E_t u+ E_t1),E_d>,unit,widening |- { </expi//i/> } : unit gives {</expi'//i/>}, I2, E_t2 ------------------------------------------------------------- :: blockrec -<E_t,E_d>,unit,widening |- { exp ; </expi//i/> } : unit gives {exp'; </expi'//i/>}, I1 u+ I2, E_t - -<E_t,E_d>,unit,widening |- exp : unit gives exp', I, E_t1 ------------------------------------------------------------- :: nondetbase -<E_t,E_d>,unit,widening |- nondet { exp } : unit gives {exp'}, I, E_t - -<E_t,E_d>,unit,widening |- exp : unit gives exp', I1, E_t1 -<(E_t u+ E_t1),E_d>,unit,widening |- nondet { </expi//i/> } : unit gives {</expi'//i/>}, I2, E_t2 ------------------------------------------------------------- :: nondetrec -<E_t,E_d>,unit,widening |- nondet { exp ; </expi//i/> } : unit gives {exp'; </expi'//i/>}, I1 u+ I2, E_t - -E,t,widening |- exp:u gives exp', I1, E_t1 -E,widening |- lexp:t gives lexp', I2, E_t2 ------------------------------------------------------------- :: assign -E,unit,widening |- lexp := exp : unit gives lexp' := exp', I u+ I2, E_t2 - -defn -E , widening |- lexp : t gives lexp' , I , E_t :: :: check_lexp :: check_lexp_ -{{ com Check the left hand side of an assignment }} -by +G |- exp1 => n_constraint +%G , flows , constrs |- exp2 => typ +%G , flows , negate constrs |- exp3 <= typ +-------------------------------------------- :: if +G |- if exp1 then exp2 else exp3 => typ -E_t(id) gives register<t> ----------------------------------------------------------- :: wreg -<E_t,E_d>,widening |- id : t gives id,<{},{ wreg }>, E_t - -E_t(id) gives reg<t> ----------------------------------------------------------- :: wlocl -<E_t,E_d>,widening |- id : t gives id,Ie, E_t - -E_t(id) gives t ----------------------------------------------------------- :: var -<E_t,E_d>,widening |- id : t gives id,Ie,E_t - -id NOTIN dom(E_t) ----------------------------------------------------------- :: wnew -<E_t,E_d>,widening |- id : t gives id,Ie, {id |-> reg<t>} - -E_t(id) gives register<t> -E_d |- typ ~> u -E_d,widening |- u ~< t : u, S_N ----------------------------------------------------------- :: wregCast -<E_t,E_d>,widening |- (typ) id : t gives id,<S_N,{ wreg }>, E_t - -E_t(id) gives reg<t> -E_d |- typ ~> u -E_d,widening |- u ~< t : u, S_N ----------------------------------------------------------- :: wloclCast -<E_t,E_d>,widening |- (typ) id : t gives id,<S_N,pure>, E_t - -E_t(id) gives t -E_d |- typ ~> u -E_d,widening |- u ~< t : u, S_N ----------------------------------------------------------- :: varCast -<E_t,E_d>,widening |- (typ) id : t gives id,<S_N,pure>,E_t - -id NOTIN dom(E_t) -E_d |- typ ~> t ----------------------------------------------------------- :: wnewCast -<E_t,E_d>, widening |- (typ) id : t gives id,Ie, {id |-> reg<t>} - - -E_t(id) gives E_k, S_N, Extern, (t1, .. ,tn, t) -> t' {</base_effecti//i/>, wmem, </base_effect'j//j/>} -<E_t,E_d>,(t1, .. , tn),widening |- exp : u1 gives exp',I,E_t1 ----------------------------------------------------------- :: wmem -<E_t,E_d>,widening |- :LEXP_memory: id(exp) : t gives :LEXP_memory: id(exp'),I u+ <S_N,{wmem}>,E_t - -E_t(id) gives E_k, S_N, Extern, (t1, ..,tn,t) -> t' {</base_effecti//i/>, wreg, </base_effect'j//j/>} -<E_t,E_d>,(t1,..,tn),widening |- exp : u1 gives exp',I,E_t1 ----------------------------------------------------------- :: wregCall -<E_t,E_d>,widening |- :LEXP_memory: id(exp) : t gives :LEXP_memory: id(exp'),I u+ <S_N,{wreg}>,E_t - -E,atom<ne>,(nums,none) |- exp : u gives exp',I1,E_t -E,(none,vectors) |- lexp : vector<ne1 ne2 inc t> gives lexp',I2,E_t ----------------------------------------------------------- :: wbitInc -E,widening |- lexp [exp] : t gives lexp'[exp'], I1 u+ I2 u+ <{ne1 <= ne, ne1 + ne2 >= ne},pure>,E_t - -E,atom<ne>,(nums,none) |- exp : u gives exp',I1,E_t -E,(none,vectors) |- lexp : vector<ne1 ne2 dec t> gives lexp',I2,E_t ----------------------------------------------------------- :: wbitDec -E,widening |- lexp [exp] : t gives lexp'[exp'], I1 u+ I2 u+ <{ne <= ne1, ne1 + (-ne2) <= ne},pure>,E_t - -E,atom<ne1>,(nums,none) |- exp1 : u1 gives exp1',I1,E_t -E,atom<ne2>,(nums,none) |- exp2 : u2 gives exp2',I2,E_t -E,(none,vectors) |- lexp : vector<ne3 ne4 inc t> gives lexp',I3,E_t ----------------------------------------------------------- :: wsliceInc -E,widening |- lexp [exp1 : exp2] : vector< ne1 ne2 + (-ne1) inc t> gives lexp'[exp1':exp2'],I1 u+ I2 u+ I3 u+ <{ne3<=ne1, ne3+ne4<= ne2 + (-ne1)},pure> ,E_t - -E,atom<ne1>,(nums,none) |- exp1 : u1 gives exp1',I1,E_t -E,atom<ne2>,(nums,none) |- exp2 : u2 gives exp2',I2,E_t -E,(none,vectors) |- lexp : vector<ne3 ne4 inc t> gives lexp',I3,E_t ----------------------------------------------------------- :: wsliceDec -E,widening |- lexp [exp1 : exp2] : vector< ne1 ne2 + (-ne1) inc t> gives lexp'[exp1':exp2'],I1 u+ I2 u+ I3 u+ <{ne1<=ne3, ne3 + (-ne4)<= ne1 + (-ne2)},pure> ,E_t - - -E_r (x<t_args>) gives </idi : ti//i/> id : t </id'j : t'j//j/> -<E_t,<E_k,E_a,E_r,E_e>>,widening |- lexp : x<t_args> gives lexp',I,E_t ----------------------------------------------------------- :: wrecord -<E_t,<E_k,E_a,E_r,E_e>>,widening |- lexp.id : t gives lexp'.id,I,E_t +G |- :E_app: vector_access ( exp , exp' ) => typ +------------------------------ :: vector_access +G |- exp [ exp' ] => typ -defn -E |- letbind gives letbind' , E_t , S_N , effect , E_k :: :: check_letbind :: check_letbind_ -{{ com Build the environment for a let binding, collecting index constraints }} -by -<E_k,E_a,E_r,E_e> |- typschm ~> t,E_k2,S_N -<E_t,<E_k u+ E_k2,E_a,E_r,E_e>>,t |- pat : u gives pat',E_t1, S_N1 -<E_t,<E_k u+ E_k2,E_a,E_r,E_e>>,t,(none,none) |- exp : u' gives exp', <S_N2,effect>,E_t2 -<E_k u+ E_k2,E_a,E_r,E_e>,(none,none) |- u' ~< u, S_N3 ------------------------------------------------------------- :: val_annot -<E_t,<E_k,E_a,E_r,E_e>> |- let typschm pat = exp gives let typschm pat' = exp', E_t1, S_N u+ S_N1 u+ S_N2 u+ S_N3, effect, E_k2 - -<E_t,E_d>,t |- pat : u gives pat',E_t1,S_N1 -<(E_t u+ E_t1),E_d>,u |- exp : u' gives exp',<S_N2,effect>,E_t2 ------------------------------------------------------------- :: val_noannot -<E_t,E_d> |- let pat = exp gives let pat' = exp', E_t1, S_N1 u+ S_N2, effect,{} +G |- :E_app: vector_subrange ( exp , exp1 , exp2 ) => typ +--------------------------- :: vector_subrange +G |- exp [ exp1 .. exp2 ] => typ -defns -check_defs :: '' ::= -defn -E_d |- type_def gives E :: :: check_td :: check_td_ -{{ com Check a type definition }} -by +G |- :E_app: vector_update ( exp , exp1 , exp2 ) => typ +---------------------------------- :: vector_update +G |- :E_vector_update: [ exp with exp1 = exp2] => typ -E_d |- typschm ~> t,E_k,S_N ------------------------------------------------------------ :: abbrev -E_d |- typedef id name_scm_opt = typschm gives <{},<{},{id |-> E_k, S_N, None,t},{},{}>> - -E_d |- typ1 ~> t1 .. E_d |- typn ~> tn -E_r == { {id1:t1, .., idn:tn} |-> x } ------------------------------------------------------------ :: unquant_record -E_d |- typedef x name_scm_opt = const struct { typ1 id1 ; .. ; typn idn semi_opt } gives <{},<{x |-> K_Typ},{},E_r,{}>> - -</ <E_k,E_a,E_r,E_e> |- quant_itemi ~>E_ki, S_Ni//i/> -<E_k u+ </E_ki//i/>,E_a,E_r,E_e> |- typ1 ~> t1 .. <E_k u+ </E_ki//i/>,E_a,E_r,E_e> |- typn ~> tn -{ x'1 |-> k1, .. ,x'm |-> km } == u+ </E_ki//i/> -E_r1 == { {id1:t1, .., idn:tn} |-> {x'1 |-> k1, ..,x'm |-> km}, u+</S_Ni//i/>, None, x< :t_arg_typ: x'1 .. :t_arg_typ: x'm> } -E_k1' == { x |-> K_Lam (k1 .. km -> K_Typ) } ------------------------------------------------------------ :: quant_record -<E_k,E_a,E_r,E_e> |- typedef x name_scm_opt = const struct forall </quant_itemi//i/> . { typ1 id1 ; .. ; typn idn semi_opt } gives <{},<E_k',{},E_r1,{}>> - -E_t == { id1 |-> {},{},Ctor,t1 -> x pure , ..., idn |-> {},{},Ctor, tn -> x pure } -E_k1 == { x |-> K_Typ } -<E_k u+ E_k1,E_a,E_r,E_e> |- typ1 ~> t1 ... <E_k u+ E_k1,E_a,E_r,E_e> |- typn ~> tn ------------------------------------------------------------- :: unquant_union -<E_k,E_a,E_r,E_e> |- typedef x name_scm_opt = const union { typ1 id1 ; ... ; typn idn semi_opt } gives <E_t,<E_k1,{},{},{}>> - -</ <E_k,E_a,E_r,E_e> |- quant_itemi ~> E_ki, S_Ni//i/> -{ x'1 |-> k1, ... , x'm |-> km } == u+ </E_ki//i/> -E_k' == { x |-> K_Lam (k1 ... km -> K_Typ) } u+ </E_ki//i/> -<E_k u+ E_k',E_a,E_r,E_e> |- typ1 ~> t1 ... <E_k u+ E_k',E_a,E_r,E_e> |- typn ~> tn -t == x < :t_arg_typ: x'1 ... :t_arg_typ: x'm> -E_t == { id1 |-> E_k', u+</S_Ni//i/>, Ctor, t1 -> t pure, ... , idn |-> E_k', u+</S_Ni//i/>, Ctor, tn -> t pure } ------------------------------------------------------------- :: quant_union -<E_k,E_a,E_r,E_e> |- typedef id name_scm_opt = const union forall </quant_itemi//i/> . { typ1 id1 ; ... ; typn idn semi_opt } gives <E_t,<E_k',{},{},{}>> - -% Save these as enumerations for coercion -E_t == {id1 |-> x, ..., idn |-> x} -E_e == { x |-> { num1 |-> id1 ... numn |-> idn} } -------------------------------------------------------------- :: enumerate -E_d |- typedef x name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } gives <E_t,<{id |-> K_Typ},{},{},E_e>> -defn -E |- fundef gives fundef' , E_t , S_N :: :: check_fd :: check_fd_ -{{ com Check a function definition }} -by +G |- :E_app: vector_update_subrange ( exp , exp1 , exp2 , exp3 ) => typ +------------------------------------------ :: vector_update_subrange +G |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] => typ -E_t(id) gives E_k',S_N',Global, t1 -> t effect -</E_d |- quant_itemi ~> E_ki,S_Ni//i/> -S_N'' == u+ </S_Ni//i/> -E_k' == </E_ki//i/> -E_d1 == <E_k',{},{},{}> u+ E_d -E_d1 |- typ ~> u -E_d1 |- u ~< t, S_N2 -</<E_t,E_d1>,t1 |- patj : uj gives patj',E_tj,S_N'''j//j/> -</<(E_t u+ E_tj),E_d1>,u |- expj : u' gives expj',<S_N''''j,effect'j>,E_t'j//j/> -S_N''''' == S_N2 u+ </S_N'''j u+ S_N''''j//j/> -effect == u+ </effect'j//j/> -S_N == resolve ( S_N' u+ S_N'' u+ S_N''''') -------------------------------------------------------------- :: rec_function -<E_t,E_d> |- function rec forall </quant_itemi//i/> . typ effectkw effect </id patj = expj//j/> gives function rec forall </quant_itemi//i/>. typ effectkw effect </id patj' = expj'//j/>,E_t, S_N - -E_t(id) gives E_k', S_N', Global, t1 -> t effect -E_d |- typ ~> u -E_d |- u ~< t, S_N2 -</<E_t,E_d>,t1 |- patj : uj gives pat',E_tj,S_N''j//j/> -</<(E_t u+ E_tj),E_d>,u |- expj : uj' gives expj',<S_N'''j,effect'j>,E_t'j//j/> -effect == u+ </effect'j//j/> -S_N == resolve (S_N2 u+ S_N' u+ </S_N''j u+ S_N'''j//j/>) -------------------------------------------------------------- :: rec_function2 -<E_t,E_d> |- function rec typ effectkw effect </id patj = expj//j/> gives function rec typ effectkw effect </id patj'=expj'//j/>,E_t, S_N - -</<E_k,E_a,E_r,E_e> |- quant_itemi ~> E_ki,S_Ni//i/> -S_N' == u+ </S_Ni//i/> -E_k' == E_k u+ </E_ki//i/> -<E_k',E_a,E_r,E_e> |- typ ~> t -</<E_t,<E_k',E_a,E_r,E_e>>, t1 |- patj : uj gives patj', E_tj,S_N''j//j/> -E_t' == (E_t u+ {id |-> E_k', S_N', Global, t1 -> t effect}) -</<(E_t' u+ E_tj),<E_k',E_a,E_r,E_e>>,t |- expj : u'j gives expj', <S_N'''j,effect'j>,E_t'j//j/> -effect == u+ </effect'j//j/> -S_N == resolve (S_N' u+ </S_N''j u+ S_N'''j//j/>) -------------------------------------------------------------- :: rec_function_no_spec -<E_t,<E_k,E_a,E_r,E_e>> |- function rec forall </quant_itemi//i/> . typ effectkw effect </id patj = expj//j/> gives function rec forall </quant_itemi//i/> . typ effectkw effect </id patj' = expj'//j/>, E_t', S_N - -E_d |- typ ~> t -</<E_t,E_d>, t1 |- patj : uj gives patj', E_tj,S_N'j//j/> -E_t' == (E_t u+ {id |-> {}, {}, Global, t1 -> t effect}) -</<(E_t' u+ E_tj),E_d>,t |- expj : uj' gives expj', <S_N'j,effect'j>,E_t'j//j/> -effect == u+ </effect'j//j/> -S_N == resolve (u+ </S_N'j u+ S_N''j//j/>) -------------------------------------------------------------- :: rec_function_no_spec2 -<E_t,E_d> |- function rec typ effectkw effect </id patj = expj//j/> gives function rec typ effectkw effect </id patj' = expj'//j/>, E_t', S_N - -E_t(id) gives E_k',S_N',Global, t1 -> t effect -</<E_k,E_a,E_r,E_e> |- quant_itemi ~> E_ki,S_Ni//i/> -S_N'' == u+ </S_Ni//i/> -E_k'' == </E_ki//i/> -<E_k'' u+ E_k,E_a,E_r,E_e> |- typ ~> u -<E_k'' u+ E_k, E_a,E_r,E_e> |- u ~< t, S_N2 -</<E_t,<E_k u+ E_k'',E_a,E_r,E_e>>, t1 |- patj : uj gives patj', E_tj,S_N''j//j/> -</<(E_t u- id u+ E_tj),<E_k u+ E_k'',E_a,E_r,E_e>>,t |- expj : uj' gives expj', <S_N'''j,effect'j>,E_t'j//j/> -S_N'''' == u+ </S_N''j u+ S_N'''j//j/> -effect == u+ </effect'j//j/> -S_N == resolve ( S_N' u+ S_N'' u+ S_N'''') -------------------------------------------------------------- :: function -<E_t,<E_k,E_a,E_r,E_e>> |- function forall </quant_itemi//i/> . typ effectkw effect </id patj = expj//j/> gives function forall </quant_itemi//i/> . typ effectkw effect </id patj' = expj'//j/>, E_t, S_N - -E_t(id) gives {}, S_N1, Global, t1 -> t effect -E_d |- typ ~> u -E_d |- u ~< t, S_N2 -</<E_t,E_d>,t1 |- patj : uj gives patj,E_tj,S_N'j//j/> -</<(E_t u- id u+ E_tj),E_d>, u |- expj : uj' gives expj', <S_N''j,effect'j>,E_t'j//j/> -effect == u+ </effect'j//j/> -S_N == resolve (S_N1 u+ S_N2 u+ </S_N'j u+ S_N''j//j/>) -------------------------------------------------------------- :: function2 -<E_t,E_d> |- function typ effectkw effect </id patj = expj//j/> gives function typ effectkw effect </id patj' = expj'//j/>, E_t, S_N - -</<E_k,E_a,E_r,E_e> |- quant_itemi ~> E_ki,S_Ni//i/> -S_N' == u+ </S_Ni//i/> -E_k'' == E_k u+ </E_ki//i/> -<E_k'',E_a,E_r,E_e> |- typ ~> t -</<E_t,<E_k'',E_a,E_r,E_e>>,t1 |- patj : uj gives patj,E_tj,S_N''j//j/> -E_t' == (E_t u+ {id |-> E_k'', S_N', Global, t1 -> t effect}) -</<(E_t u+ E_tj),<E_k'',E_a,E_r,E_e>>,t |- expj : uj' gives expj', <S_N''j,effect'j>,E_t'j//j/> -effect == u+ </effect'j//j/> -S_N == resolve (S_N' u+ </S_N'j u+ S_N''j//j/>) -------------------------------------------------------------- :: function_no_spec -<E_t,<E_k,E_a,E_r,E_e>> |- function forall </quant_itemi//i/> . typ effectkw effect </id patj = expj//j/> gives function forall </quant_itemi//i/>. typ effectkw effect </id patj' = expj'//j/>, E_t', S_N - -E_d |- typ ~> t -</<E_t,E_d>,t1 |- patj : uj gives patj', E_tj,S_N'j//j/> -E_t' == (E_t u+ {id |-> {},S_N, Global, t1 -> t effect}) -</<(E_t u+ E_tj),E_d>,t |- expj : uj' gives exp', <S_N'j,effect'j>,E_t'j//j/> -effect == u+ </effect'j//j/> -S_N == resolve (u+ </S_N'j u+ S_N''j//j/>) -------------------------------------------------------------- :: function_no_spec2 -<E_t,E_d> |- function typ effectkw effect </id patj = expj//j/> gives function typ effectkw effect </id patj' = expj'//j/>, E_t', S_N +G |- :E_app: vector_append ( exp1 , exp2 ) => typ +----------------------------------- :: vector_append +G |- exp1 : exp2 => typ -defn -E |- val_spec gives E_t :: :: check_spec :: check_spec_ -{{ com Check a value specification }} -by -E_d |- typschm ~> t, E_k1, S_N --------------------------------------------------------- :: val_spec -<E_t,E_d> |- val typschm id gives {id |-> E_k1,S_N,Global,t } +order_inc +G |- exp => typ +G |- exp1 <= typ .. G |- expn <= typ +nexp = length [|| exp , exp1 , .. , expn ||] +-------------------------------------------- :: vector_inc +G |- [|| exp , exp1 , .. , expn ||] => typ [ numZero <: nexp ] -E_d |- typschm ~> t, E_k1, S_N --------------------------------------------------------- :: extern -<E_t,E_d> |- val extern typschm id = string gives {id |-> E_k1,S_N,Extern,t} +order_dec +G |- exp => typ +G |- exp1 <= typ .. G |- expn <= typ +nexp = length [|| exp , exp1 , .. , expn ||] +-------------------------------------------- :: vector_dec +G |- [|| exp , exp1 , .. , expn ||] => typ [ nexp :> numZero ] -defn -E_d |- default_spec gives E_t , E_k1 :: :: check_default :: check_default_ -{{ com Check a default typing specification }} -by -E_k |- base_kind ~> k ------------------------------------------------------------- :: kind -<E_k,E_a,E_r,E_e> |- default base_kind 'x gives {}, {'x |-> k default } +G |- exp1 <= bool +G |- exp2 <= string +----------------------------------- :: assert +G |- assert (exp1, exp2 ) => unit -E_d |- typschm ~> t,E_k1,S_N ------------------------------------------------------------- :: typ -E_d |- default typschm id gives {id |-> E_k1,S_N,Default,t},{} defn - -E |- def gives def' , E' :: :: check_def :: check_def_ -{{ com Check a definition }} + G |- exp <= typ :: :: check_exp :: check_exp_ +{{ com Check that type of $[[exp]]$ is $[[typ]]$ }} +{{ tex [[G]] \vdash [[exp]] \Leftarrow [[typ]] }} by -E_d |- type_def gives E ---------------------------------------------------------- :: tdef -<E_t,E_d>|- type_def gives type_def, <E_t,E_d> u+ E -E |- fundef gives fundef', E_t,S_N ---------------------------------------------------------- :: fdef -E |- fundef gives fundef', E u+ <E_t,empty> +G |- exp1 <= unit ... G |- expn <= unit +G |- exp <= typ +----------------------------------- :: block +G |- { exp1; ... ; expn ; exp } <= typ -E |- letbind gives letbind', {id1 |-> t1 , .. , idn |-> tn},S_N,pure,E_k -S_N1 == resolve(S_N) ---------------------------------------------------------- :: vdef -E |- letbind gives letbind', E u+ <{id1 |-> E_k,S_N,None,t1 , .. , idn |-> E_k,S_N,None,tn},empty> -E |- val_spec gives E_t ---------------------------------------------------------- :: vspec -E |- val_spec gives val_spec, E u+ <E_t,empty> -E_d |- default_spec gives E_t1, E_k1 ---------------------------------------------------------- :: default -<E_t,E_d> |- default_spec gives default_spec, <(E_t u+ E_t1),E_d u+ <E_k1,{},{},{}>> - -E_d |- typ ~> t ----------------------------------------------------------- :: register -<E_t,E_d> |- register typ id gives register typ id, <(E_t u+ {id |-> register<t>}),E_d> - -%TODO Add alias checking - -defn -E |- defs gives defs' , E' :: :: check_defs :: check_defs_ -{{ com Check definitions, potentially given default environment of built-in library }} -by - -:check_def: E |- def gives def', E1 -E u+ E1 |- </defi// i/> gives </defi'//i/>, E2 ------------------------------------------------------------- :: defs -E |- def </defi// i/> gives def' </defi'//i/>, E2 + diff --git a/language/sil.ott b/language/sil.ott new file mode 100644 index 00000000..40adfc4d --- /dev/null +++ b/language/sil.ott @@ -0,0 +1,451 @@ +%%% Sail Intermediate Language %%% + +% An attempt to precisely document the subset of sail that the +% rewriter is capable of re-writing sail into. It is intended to be a +% strict subset of the Sail AST, and be typecheckable with the full +% typechecker. +% +% Notably, it lacks: +% - Special (bit)vector syntax. +% - Complex l-values. +% - Existential types. +% - Polymorphism, of any kind. + +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 }} + {{ ocaml int }} + {{ lex numeric }} + {{ lem nat }} + +metavar string ::= + {{ phantom }} + {{ ocaml string }} + {{ lem string }} + {{ hol string }} + {{ com String literals }} + +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 + +type loop = While | Until + +}} + +metavar x , y , z ::= + {{ ocaml text }} + {{ lem string }} + {{ hol string }} + {{ com identifier }} + {{ ocamlvar "[[x]]" }} + {{ lemvar "[[x]]" }} + +grammar + +l :: '' ::= {{ phantom }} + {{ ocaml Parse_ast.l }} + {{ lem l }} + {{ hol unit }} + {{ com source location }} + | :: :: Unknown + {{ ocaml Unknown }} + {{ lem Unknown }} + {{ hol () }} + + +id :: '' ::= + {{ com Identifier }} + {{ aux _ l }} + | x :: :: id + | ( deinfix x ) :: D :: deIid {{ com remove infix status }} + +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 }} + | { 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]]) }} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Types % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +typ :: 'Typ_' ::= + {{ com type expressions, of kind $[[Type]]$ }} + {{ aux _ l }} + | id :: :: id + {{ com defined type }} + | typ1 -> typ2 effectkw effect :: :: fn + {{ com Function (first-order only in user code) }} + | ( typ1 , .... , typn ) :: :: tup + {{ com Tuple }} + | id < typ_arg1 , .. , typ_argn > :: :: app + {{ com type constructor application }} + +typ_arg :: 'Typ_arg_' ::= + {{ com type constructor arguments of all kinds }} + {{ aux _ l }} + | typ :: :: typ + +typquant :: 'TypQ_' ::= + {{ com type quantifiers and constraints}} + {{ aux _ l }} + | :: :: no_forall {{ com empty }} + +typschm :: 'TypSchm_' ::= + {{ com type scheme }} + {{ aux _ l }} + | typquant typ :: :: ts + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Type definitions % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +type_def {{ ocaml 'a type_def }} {{ lem type_def 'a }} :: 'TD_' ::= + {{ ocaml TD_aux of type_def_aux * 'a annot }} + {{ lem TD_aux of type_def_aux * annot 'a }} + | type_def_aux :: :: aux + +type_def_aux :: 'TD_' ::= + {{ com type definition body }} + | typedef id = typschm :: :: abbrev + {{ com type abbreviation }} {{ texlong }} + | typedef id = const struct typquant { typ1 id1 ; ... ; typn idn } :: :: record + {{ com struct type definition }} {{ texlong }} + | typedef id = const union typquant { type_union1 ; ... ; type_unionn } :: :: variant + {{ com tagged union type definition}} {{ texlong }} + | typedef id = enumerate { id1 ; ... ; idn } :: :: enum + {{ com enumeration type definition}} {{ texlong }} + +% This one is a bit unusual - I think all nexps here must be constant, so replace with num. + | typedef id = register bits [ num : num' ] { index_range1 : id1 ; ... ; index_rangen : idn } + :: :: register {{ com register mutable bitfield type definition }} {{ texlong }} + +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 % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +lit :: 'L_' ::= + {{ com literal constant }} + {{ aux _ l }} + | ( ) :: :: unit {{ com $() : [[unit]]$ }} + | 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 }} +% Need to represent as a function call, e.g. sil#hex_string "0xFFFF". +% | hex :: :: hex {{ com bit vector constant, C-style }} +% | bin :: :: bin {{ com bit vector constant, C-style }} + | string :: :: string {{ com string constant }} + | undefined :: :: undef {{ com undefined-value constant }} + | real :: :: real {{ com real number }} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Patterns % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +pat :: 'P_' ::= + {{ com pattern }} + {{ aux _ annot }} {{ auxparam 'a }} + | _ :: :: wild + {{ com wildcard }} + | ( pat as id ) :: :: as + {{ com named pattern }} + | ( typ ) pat :: :: typ + {{ com typed pattern }} + | id :: :: id + {{ com identifier }} + | id ( pat1 , .. , patn ) :: :: app + {{ com union constructor pattern }} + | { fpat1 ; ... ; fpatn } :: :: record + {{ com struct pattern }} + | ( pat1 , .... , patn ) :: :: tup + {{ com tuple pattern }} + | [|| pat1 , .. , patn ||] :: :: list + {{ com list pattern }} + | ( pat ) :: S :: paren + {{ ichlo [[pat]] }} + | pat1 '::' pat2 :: :: cons + {{ com Cons patterns }} + +fpat :: 'FP_' ::= + {{ com field pattern }} + {{ aux _ annot }} {{ auxparam 'a }} + | id = pat :: :: Fpat + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Expressions % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +loop :: loop ::= {{ phantom }} + | while :: :: while + | until :: :: until + +exp :: 'E_' ::= + {{ com expression }} + {{ aux _ annot }} {{ auxparam 'a }} + | { exp1 ; ... ; expn } :: :: block {{ com sequential block }} + | nondet { exp1 ; ... ; expn } :: :: nondet {{ com nondeterministic block }} + | id :: :: id + {{ com identifier }} + | lit :: :: lit + {{ com literal constant }} +% Purely an annotation as all casting is resolved by type checker, can +% be evaluated by simply dropping the type. + | ( typ ) exp :: :: cast + {{ com cast }} + | id ( exp1 , .. , expn ) :: :: app + {{ com function application }} + | ( exp1 , .... , expn ) :: :: tuple + {{ com tuple }} + | if exp1 then exp2 else exp3 :: :: if + {{ com conditional }} + | loop exp1 exp2 :: :: loop + {{ com while or until loop }} + | foreach ( id from exp1 to exp2 by exp3 in order ) exp4 :: :: for + {{ com for loop }} + | [|| exp1 , .. , expn ||] :: :: list + {{ com list }} + | exp1 '::' exp2 :: :: cons + {{ com cons }} + | { fexps } :: :: record + {{ com struct }} + | { exp with fexps } :: :: record_update + {{ com functional update of struct }} + | exp . id :: :: field + {{ com field projection from struct }} + | switch exp { case pexp1 ... case pexpn } :: :: case + {{ com pattern matching }} + | letbind in exp :: :: let + {{ com let expression }} + | lexp := exp :: :: assign + {{ com imperative assignment }} + | return exp :: :: return + {{ com return $[[exp]]$ from current function }} + | exit exp :: :: exit + {{ com halt all current execution }} + | value :: I :: value + {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }} + +lexp :: 'LEXP_' ::= {{ com lvalue expression }} + {{ aux _ annot }} {{ auxparam 'a }} + | id :: :: id + {{ com identifier }} + | ( typ ) id :: :: cast + {{ com cast }} + | ( lexp0 , .. , lexpn ) :: :: tup {{ com multiple (non-memory) assignment }} +% SIL: Not sure how much to rewrite L-expressions. +% | lexp [ exp ] :: :: vector {{ com vector element }} +% | lexp [ exp1 '..' exp2 ] :: :: vector_range {{ com subvector }} +% | lexp . id :: :: field {{ com struct field }} + +fexp :: 'FE_' ::= + {{ com field expression }} + {{ aux _ annot }} {{ auxparam 'a }} + | id = exp :: :: Fexp + +fexps :: 'FES_' ::= + {{ com field expression list }} + {{ aux _ annot }} {{ auxparam 'a }} + | fexp1 ; ... ; fexpn :: :: Fexps + +pexp :: 'Pat_' ::= + {{ com pattern match }} + {{ aux _ annot }} {{ auxparam 'a }} + | pat -> exp :: :: exp + | pat when exp1 -> exp :: :: when + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Function definitions % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +tannot_opt :: 'Typ_annot_opt_' ::= + {{ com optional type annotation for functions}} + {{ aux _ l }} + | :: :: none + | 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 }} + +letbind :: 'LB_' ::= + {{ com let binding }} + {{ aux _ annot }} {{ auxparam 'a }} + | let pat = exp :: :: val + {{ com let, implicit type ($[[pat]]$ must be total)}} + +val_spec {{ ocaml 'a val_spec }} {{ lem val_spec 'a }} :: 'VS_' ::= + {{ ocaml VS_aux of val_spec_aux * 'a annot }} + {{ lem VS_aux of val_spec_aux * annot 'a }} + | val_spec_aux :: :: aux + +val_spec_aux :: 'VS_' ::= + {{ com value type specification }} + {{ ocaml VS_val_spec of typschm * id * (string -> string option) * bool }} + {{ lem VS_val_spec of typschm * id * maybe string * bool }} + | val typschm id :: S :: val_spec + {{ com specify the type of an upcoming definition }} + {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} {{ lem }} + +default_spec :: 'DT_' ::= + {{ com default kinding or typing assumption }} + {{ aux _ l }} + | default Order order :: :: order + +reg_id :: 'RI_' ::= + {{ aux _ annot }} {{ auxparam 'a }} + | id :: :: id + +alias_spec :: 'AL_' ::= + {{ com register alias expression forms }} + {{ 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 + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Top-level definitions % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +prec :: '' ::= + | infix :: :: Infix + | infixl :: :: InfixL + | infixr :: :: InfixR + +def :: 'DEF_' ::= + {{ com top-level definition }} + {{ auxparam 'a }} + | 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 }} + | dec_spec :: :: reg_dec + {{ com register declaration }} + +defs :: '' ::= + {{ com definition sequence }} + {{ auxparam 'a }} + | def1 .. defn :: :: Defs |