summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--editors/sail2-mode.el2
-rw-r--r--language/Makefile2
-rw-r--r--language/l2.ml471
-rw-r--r--language/l2.ott575
-rw-r--r--language/l2_rules.ott1565
-rw-r--r--lib/ocaml_rts/sail_lib.ml88
-rw-r--r--src/gen_lib/prompt.lem8
-rw-r--r--src/gen_lib/sail_operators.lem2
-rw-r--r--src/gen_lib/sail_values.lem9
-rw-r--r--src/gen_lib/state.lem13
-rw-r--r--src/ocaml_backend.ml90
-rw-r--r--src/pretty_print_lem.ml28
-rw-r--r--src/pretty_print_lem_ast.ml15
-rw-r--r--src/process_file.ml1
-rw-r--r--src/process_file.mli1
-rw-r--r--src/rewriter.ml330
-rw-r--r--src/rewriter.mli3
-rw-r--r--src/sail.ml6
-rw-r--r--src/spec_analysis.ml1
-rw-r--r--src/type_check.ml37
-rw-r--r--src/type_check.mli1
21 files changed, 984 insertions, 2264 deletions
diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el
index c2f77801..2958af21 100644
--- a/editors/sail2-mode.el
+++ b/editors/sail2-mode.el
@@ -8,7 +8,7 @@
"else" "match" "in" "return" "register" "forall" "operator" "effect"
"overload" "cast" "sizeof" "constraint" "default" "assert"
"pure" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and"
- "throw" "clause" "as"))
+ "throw" "clause" "as" "repeat" "until" "while" "do"))
(defconst sail2-kinds
'("Int" "Type" "Order" "inc" "dec"
diff --git a/language/Makefile b/language/Makefile
index 77aa5607..081d90a7 100644
--- a/language/Makefile
+++ b/language/Makefile
@@ -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
diff --git a/language/l2.ml b/language/l2.ml
index 13cb2567..8f041dc7 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,13 +265,23 @@ 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
@@ -299,165 +304,11 @@ type
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 reg_id_aux =
RI_id of id
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 +319,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 +337,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 +352,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 +390,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 +414,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 +444,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,6 +473,22 @@ type
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
+'a val_spec_aux = VS_val_spec of typschm * id * string option * bool
+
+
+type
+'a fundef_aux = (* function definition *)
+ FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
+
+
+type
'a default_spec_aux = (* default kinding or typing assumption *)
DT_order of order
| DT_kind of base_kind * kid
@@ -641,35 +496,35 @@ type
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
+prec =
+ Infix
+ | InfixL
+ | InfixR
type
-'a val_spec =
- VS_aux of 'a val_spec_aux * 'a annot
+'a scattered_def =
+ SD_aux of 'a scattered_def_aux * 'a annot
type
-'a fundef =
- FD_aux of 'a fundef_aux * 'a annot
+'a dec_spec =
+ DEC_aux of 'a dec_spec_aux * 'a annot
type
-'a scattered_def =
- SD_aux of 'a scattered_def_aux * 'a annot
+'a val_spec =
+ VS_aux of 'a val_spec_aux * 'a annot
type
-'a default_spec =
- DT_aux of 'a default_spec_aux * Parse_ast.l
+'a fundef =
+ FD_aux of 'a fundef_aux * 'a annot
type
-'a dec_spec =
- DEC_aux of 'a dec_spec_aux * 'a annot
+'a default_spec =
+ DT_aux of 'a default_spec_aux * Parse_ast.l
type
@@ -683,6 +538,8 @@ 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_fixity of prec * int * id (* fixity declaration *)
+ | DEF_overload of id * (id) list (* operator overload specification *)
| DEF_default of 'a 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 *)
diff --git a/language/l2.ott b/language/l2.ott
index c78c66f8..e8d8a9b7 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 }}
@@ -43,11 +47,24 @@ 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
+type text = string
+
+type l = Parse_ast.l
+
type 'a annot = l * 'a
+type loop = While | Until
+
}}
embed
@@ -75,7 +92,7 @@ val subst : forall 'a. list 'a -> list 'a -> bool
}}
metavar x , y , z ::=
- {{ ocaml string }}
+ {{ ocaml text }}
{{ lem string }}
{{ hol string }}
{{ com identifier }}
@@ -84,7 +101,7 @@ metavar x , y , z ::=
metavar ix ::=
{{ lex alphanum }}
- {{ ocaml string }}
+ {{ ocaml text }}
{{ lem string }}
{{ hol string }}
{{ com infix identifier }}
@@ -112,7 +129,7 @@ annot :: '' ::=
{{ hol unit }}
id :: '' ::=
- {{ com identifier }}
+ {{ com Identifier }}
{{ aux _ l }}
| x :: :: id
| ( deinfix x ) :: D :: deIid {{ com remove infix status }}
@@ -120,6 +137,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 +153,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 +184,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}}
@@ -243,6 +274,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 +290,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 +304,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 +339,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
@@ -412,17 +449,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 +504,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 +541,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 +562,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 +574,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_' ::=
@@ -583,355 +620,6 @@ 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" }}
-
-optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }}
- | x :: :: optx_x
- {{ lem (Just [[x]]) }} {{ ocaml (Some [[x]]) }}
- | :: :: optx_none
- {{ lem Nothing }} {{ ocaml None }}
-
-
-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 }}
- | 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 }}
- | Spec :: :: spec
- | Enum num :: :: enum
- | 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)))
-
-}}
-
-grammar
-
- 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
-
-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*)
-
-}}
-
-grammar
-
- 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]]) }}
-
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Expressions %
@@ -949,7 +637,9 @@ tannot :: '' ::=
{{ phantom }}
{{ ocaml tannot }}
{{ lem tannot }}
-
+loop :: loop ::= {{ phantom }}
+ | while :: :: while
+ | until :: :: until
exp :: 'E_' ::=
@@ -987,7 +677,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 ]] }}
@@ -1069,15 +761,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 +782,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 }}
- | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }}
-
-i_direction :: 'I' ::=
- | IInc :: :: Inc
- | IDec :: :: Dec
-
-ctor_kind :: 'C_' ::=
- | C_Enum nat :: :: Enum
- | C_Union :: :: Union
-
-reg_form :: 'Form_' ::=
- | Reg id tannot i_direction :: :: Reg
- | SubReg id reg_form index_range :: :: SubReg
-
-reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }}
-
-alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }}
-
-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
+ | return_int ( exp ) :: :: internal_return {{ com For internal use to embed into monad definition }}
+% | value :: I :: internal_value {{ com For internal use in interpreter to wrap pre-evaluated values when returning an action }}
+ | constraint n_constraint :: :: constraint
+
+%i_direction :: 'I' ::=
+% | IInc :: :: Inc
+% | IDec :: :: Dec
+
+%ctor_kind :: 'C_' ::=
+% | C_Enum nat :: :: Enum
+% | C_Union :: :: Union
+
+%reg_form :: 'Form_' ::=
+% | Reg id tannot i_direction :: :: Reg
+% | SubReg id reg_form index_range :: :: SubReg
+
+%reg_form_set :: '' ::= {{ phantom }} {{ lem set reg_form }}
+
+%alias_spec_tannot :: '' ::= {{ phantom }} {{ lem alias_spec tannot }} {{ ocaml tannot alias_spec }}
+
lexp :: 'LEXP_' ::= {{ com lvalue expression }}
{{ aux _ annot }} {{ auxparam 'a }}
@@ -1127,7 +809,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 +838,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 +916,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,22 +953,27 @@ 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)}}
+% | 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)}}
-
+ | let pat = exp :: :: val
+ {{ com let, implicit type ($[[pat]]$ must be total)}}
val_spec :: 'VS_' ::=
{{ com value type specification }}
{{ aux _ annot }} {{ auxparam 'a }}
- | val typschm id :: :: val_spec
+ {{ ocaml VS_val_spec of typschm * id * string option * 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) }}
+ | val cast typschm id :: S :: cast
+ {{ ocaml (VS_val_spec [[typschm]] [[id]] None true) }}
+ | val extern typschm id :: S :: extern_no_rename
{{ com specify the type of an external function }}
- | val extern typschm id = string :: :: extern_spec
+ {{ ocaml (VS_val_spec [[typschm]] [[id]] (Some [[id]]) false) }}
+ | val extern typschm id = string :: S :: extern_spec
{{ com specify the type of a function from Lem }}
+ {{ ocaml (VS_val_spec [[typschm]] [[id]] (Some [[string]]) false) }}
%where the string must provide an explicit path to the required function but will not be checked
default_spec :: 'DT_' ::=
@@ -1346,6 +1034,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 +1052,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
@@ -1379,16 +1076,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 +1112,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 < }}
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/lib/ocaml_rts/sail_lib.ml b/lib/ocaml_rts/sail_lib.ml
index a0d6bc5f..88217ddf 100644
--- a/lib/ocaml_rts/sail_lib.ml
+++ b/lib/ocaml_rts/sail_lib.ml
@@ -2,12 +2,26 @@ open Big_int
type 'a return = { return : 'b . 'a -> 'b }
+let trace_depth = ref 0
+let random = ref false
+
let with_return (type t) (f : _ -> t) =
let module M =
struct exception Return of t end
in
- let return = { return = (fun x -> raise (M.Return x)); } in
- try f return with M.Return x -> x
+ let return = { return = (fun x -> decr trace_depth; raise (M.Return x)); } in
+ try
+ let result = f return in
+ decr trace_depth;
+ result
+ with M.Return x -> x
+
+let trace str =
+ if !trace_depth < 0 then trace_depth := 0 else ();
+ prerr_endline (String.make (!trace_depth * 2) ' ' ^ str)
+
+let trace_call str =
+ trace str; incr trace_depth
type bit = B0 | B1
@@ -19,6 +33,11 @@ let or_bit = function
| B0, B0 -> B0
| _, _ -> B1
+let xor_bit = function
+ | B1, B0 -> B1
+ | B0, B1 -> B1
+ | _, _ -> B0
+
let and_vec (xs, ys) =
assert (List.length xs = List.length ys);
List.map2 (fun x y -> and_bit (x, y)) xs ys
@@ -31,10 +50,19 @@ let or_vec (xs, ys) =
let or_bool (b1, b2) = b1 || b2
+let xor_vec (xs, ys) =
+ assert (List.length xs = List.length ys);
+ List.map2 (fun x y -> xor_bit (x, y)) xs ys
+
+let xor_bool (b1, b2) = (b1 || b2) && (b1 != b2)
+
let undefined_bit () =
- if Random.bool () then B0 else B1
+ if !random
+ then (if Random.bool () then B0 else B1)
+ else B0
-let undefined_bool () = Random.bool ()
+let undefined_bool () =
+ if !random then Random.bool () else false
let rec undefined_vector (start_index, len, item) =
if eq_big_int len zero_big_int
@@ -46,10 +74,16 @@ let undefined_string () = ""
let undefined_unit () = ()
let undefined_int () =
- big_int_of_int (Random.int 0xFFFF)
+ if !random then big_int_of_int (Random.int 0xFFFF) else zero_big_int
+
+let undefined_nat () = zero_big_int
+
+let undefined_range (lo, hi) = lo
let internal_pick list =
- List.nth list (Random.int (List.length list))
+ if !random
+ then List.nth list (Random.int (List.length list))
+ else List.nth list 0
let eq_int (n, m) = eq_big_int n m
@@ -70,6 +104,11 @@ let subrange (list, n, m) =
let m = int_of_big_int m in
List.rev (take (n - (m - 1)) (drop m (List.rev list)))
+let slice (list, n, m) =
+ let n = int_of_big_int n in
+ let m = int_of_big_int m in
+ List.rev (take m (drop n (List.rev list)))
+
let eq_list (xs, ys) = List.for_all2 (fun x y -> x == y) xs ys
let access (xs, n) = List.nth (List.rev xs) (int_of_big_int n)
@@ -319,3 +358,40 @@ let debug (str1, n, str2, v) = prerr_endline (str1 ^ string_of_big_int n ^ str2
let eq_string (str1, str2) = String.compare str1 str2 == 0
let lt_int (x, y) = lt_big_int x y
+
+let set_slice (out_len, slice_len, out, n, slice) =
+ update_subrange(out, n, sub_big_int n (big_int_of_int (List.length slice - 1)), slice)
+
+let set_slice_int (_, _, _, _) = assert false
+
+let eq_real (x, y) = Num.eq_num x y
+let lt_real (x, y) = Num.lt_num x y
+let gt_real (x, y) = Num.gt_num x y
+let lteq_real (x, y) = Num.le_num x y
+let gteq_real (x, y) = Num.ge_num x y
+
+let round_down x = Num.big_int_of_num (Num.floor_num x)
+let round_up x = Num.big_int_of_num (Num.ceiling_num x)
+let quotient_real (x, y) = Num.div_num x y
+let mult_real (x, y) = Num.mult_num x y
+let real_power (x, y) = Num.power_num x (Num.num_of_big_int y)
+let add_real (x, y) = Num.add_num x y
+let sub_real (x, y) = Num.sub_num x y
+
+let lt (x, y) = lt_big_int x y
+let gt (x, y) = gt_big_int x y
+let lteq (x, y) = le_big_int x y
+let gteq (x, y) = gt_big_int x y
+
+let pow2 x = power_big_int_positive_int x 2
+
+let max_int (x, y) = max_big_int x y
+let min_int (x, y) = min_big_int x y
+
+let undefined_real () = Num.num_of_int 0
+
+(* Not a very good sqrt implementation *)
+let sqrt_real x = Num.num_of_string (string_of_float (sqrt (Num.float_of_num x)))
+
+let print_int (str, x) =
+ prerr_endline (str ^ string_of_big_int x)
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index f5ac8fc5..23f81f0e 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -158,7 +158,7 @@ let footprint = Footprint (Done (),Nothing)
val foreachM_inc : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
let rec foreachM_inc (i,stop,by) vars body =
- if i <= stop
+ if (by > 0 && i <= stop) || (by < 0 && stop <= i)
then
body i vars >>= fun vars ->
foreachM_inc (i + by,stop,by) vars body
@@ -167,11 +167,11 @@ let rec foreachM_inc (i,stop,by) vars body =
val foreachM_dec : forall 'vars 'r. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> MR 'vars 'r) -> MR 'vars 'r
-let rec foreachM_dec (i,stop,by) vars body =
- if i >= stop
+let rec foreachM_dec (stop,i,by) vars body =
+ if (by > 0 && i >= stop) || (by < 0 && stop >= i)
then
body i vars >>= fun vars ->
- foreachM_dec (i - by,stop,by) vars body
+ foreachM_dec (stop,i - by,by) vars body
else return vars
val while_PP : forall 'vars. bool -> 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 30c7325e..d9bf8454 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -144,7 +144,7 @@ let to_bin n = List.reverse (to_bin_aux n)
val pad_zero : list bitU -> integer -> list bitU
let rec pad_zero bits n =
- if n = 0 then bits else pad_zero (B0 :: bits) (n -1)
+ if n <= 0 then bits else pad_zero (B0 :: bits) (n -1)
let rec add_one_bit_ignore_overflow_aux bits = match bits with
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 906b35a8..45b73ab5 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -167,6 +167,7 @@ let get_dir (Vector _ _ ord) = ord
let get_start (Vector _ s _) = s
let get_elems (Vector elems _ _) = elems
let length (Vector bs _ _) = integerFromNat (length bs)
+let vector_length = length
instance forall 'a. Show 'a => (Show (vector 'a))
let show = showVector
@@ -565,17 +566,17 @@ let internal_mem_value direction bytes =
val foreach_inc : forall 'vars. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> 'vars) -> 'vars
let rec foreach_inc (i,stop,by) vars body =
- if i <= stop
+ if (by > 0 && i <= stop) || (by < 0 && stop <= i)
then let vars = body i vars in
foreach_inc (i + by,stop,by) vars body
else vars
val foreach_dec : forall 'vars. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> 'vars) -> 'vars
-let rec foreach_dec (i,stop,by) vars body =
- if i >= stop
+let rec foreach_dec (stop,i,by) vars body =
+ if (by > 0 && i >= stop) || (by < 0 && stop >= i)
then let vars = body i vars in
- foreach_dec (i - by,stop,by) vars body
+ foreach_dec (stop,i - by,by) vars body
else vars
let assert' b msg_opt =
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 1b03c81e..1ca25b74 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -63,8 +63,9 @@ let catch_early_return m s =
end) (m s)
val range : integer -> integer -> list integer
-let rec range i j =
- if i = j then [i]
+let rec range i j =
+ if j < i then []
+ else if i = j then [i]
else i :: range (i+1) j
val get_reg : forall 'regs 'a. sequential_state 'regs -> register_ref 'regs 'a -> 'a
@@ -218,7 +219,7 @@ let footprint s = return () s
val foreachM_inc : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e
let rec foreachM_inc (i,stop,by) vars body =
- if i <= stop
+ if (by > 0 && i <= stop) || (by < 0 && stop <= i)
then
body i vars >>= fun vars ->
foreachM_inc (i + by,stop,by) vars body
@@ -227,11 +228,11 @@ let rec foreachM_inc (i,stop,by) vars body =
val foreachM_dec : forall 'regs 'vars 'e. (integer * integer * integer) -> 'vars ->
(integer -> 'vars -> ME 'regs 'vars 'e) -> ME 'regs 'vars 'e
-let rec foreachM_dec (i,stop,by) vars body =
- if i >= stop
+let rec foreachM_dec (stop,i,by) vars body =
+ if (by > 0 && i >= stop) || (by < 0 && stop >= i)
then
body i vars >>= fun vars ->
- foreachM_dec (i - by,stop,by) vars body
+ foreachM_dec (stop,i - by,by) vars body
else return vars
val while_PP : forall 'vars. bool -> 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index dc8c056e..74fb6e4c 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -5,12 +5,14 @@ open Type_check
type ctx =
{ register_inits : tannot exp list;
- externs : id Bindings.t
+ externs : id Bindings.t;
+ val_specs : typ Bindings.t
}
let empty_ctx =
{ register_inits = [];
- externs = Bindings.empty
+ externs = Bindings.empty;
+ val_specs = Bindings.empty
}
let zchar c =
@@ -47,7 +49,10 @@ let ocaml_typ_id ctx = function
| id when Id.compare id (mk_id "list") = 0 -> string "list"
| id when Id.compare id (mk_id "bit") = 0 -> string "bit"
| id when Id.compare id (mk_id "int") = 0 -> string "big_int"
+ | id when Id.compare id (mk_id "nat") = 0 -> string "big_int"
| id when Id.compare id (mk_id "bool") = 0 -> string "bool"
+ | id when Id.compare id (mk_id "unit") = 0 -> string "unit"
+ | id when Id.compare id (mk_id "real") = 0 -> string "Num.num"
| id -> zencode ctx id
let rec ocaml_typ ctx (Typ_aux (typ_aux, _)) =
@@ -84,6 +89,7 @@ let ocaml_lit (L_aux (lit_aux, _)) =
| L_num n -> parens (string "big_int_of_int" ^^ space ^^ string (string_of_int n))
| L_undef -> failwith "undefined should have been re-written prior to ocaml backend"
| L_string str -> dquotes (string (String.escaped str))
+ | L_real str -> parens (string "Num.num_of_string" ^^ space ^^ dquotes (string (String.escaped str)))
| _ -> string "LIT"
let rec ocaml_pat ctx (P_aux (pat_aux, _) as pat) =
@@ -110,10 +116,10 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
| E_app (f, [x]) when Env.is_union_constructor f (env_of exp) -> zencode_upper ctx f ^^ space ^^ ocaml_atomic_exp ctx x
| E_app (f, [x]) -> zencode ctx f ^^ space ^^ ocaml_atomic_exp ctx x
| E_app (f, xs) when Env.is_union_constructor f (env_of exp) ->
- zencode_upper ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs)
+ zencode_upper ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_atomic_exp ctx) xs)
| E_app (f, xs) ->
- zencode ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) xs)
- | E_vector_subrange (exp1, exp2, exp3) -> string "subrange" ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_exp ctx) [exp1; exp2; exp3])
+ zencode ctx f ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_atomic_exp ctx) xs)
+ | E_vector_subrange (exp1, exp2, exp3) -> string "subrange" ^^ space ^^ parens (separate_map (comma ^^ space) (ocaml_atomic_exp ctx) [exp1; exp2; exp3])
| E_return exp -> separate space [string "r.return"; ocaml_atomic_exp ctx exp]
| E_assert (exp, _) -> separate space [string "assert"; ocaml_atomic_exp ctx exp]
| E_cast (_, exp) -> ocaml_exp ctx exp
@@ -140,8 +146,19 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
^/^ ocaml_exp ctx exp
| E_internal_let (lexp, exp1, exp2) ->
separate space [string "let"; ocaml_atomic_lexp ctx lexp;
- equals; string "ref"; ocaml_atomic_exp ctx exp1; string "in"]
+ equals; string "ref"; parens (ocaml_atomic_exp ctx exp1 ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (Rewriter.simple_typ (typ_of exp1))); string "in"]
^/^ ocaml_exp ctx exp2
+ | E_loop (Until, cond, body) ->
+ let loop_body =
+ (ocaml_atomic_exp ctx body ^^ semi)
+ ^/^
+ separate space [string "if"; ocaml_atomic_exp ctx cond;
+ string "then loop ()";
+ string "else ()"]
+ in
+ (string "let rec loop () =" ^//^ loop_body)
+ ^/^ string "in"
+ ^/^ string "loop ()"
| E_loop (While, cond, body) ->
let loop_body =
separate space [string "if"; ocaml_atomic_exp ctx cond;
@@ -152,11 +169,22 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
^/^ string "in"
^/^ string "loop ()"
| E_lit _ | E_list _ | E_id _ | E_tuple _ -> ocaml_atomic_exp ctx exp
+ | E_for (id, exp_from, exp_to, exp_step, _, exp_body) ->
+ let loop_var = separate space [string "let"; zencode ctx id; equals; string "ref"; ocaml_atomic_exp ctx exp_from; string "in"] in
+ let loop_mod = string "add_big_int" ^^ space ^^ zencode ctx id ^^ space ^^ ocaml_atomic_exp ctx exp_step in
+ let loop_body =
+ separate space [string "if"; zencode ctx id; string "<="; ocaml_atomic_exp ctx exp_to]
+ ^/^ separate space [string "then";
+ parens (ocaml_atomic_exp ctx exp_body ^^ semi ^^ space ^^ string "loop" ^^ space ^^ parens loop_mod)]
+ ^/^ string "else ()"
+ in
+ (string ("let rec loop " ^ zencode_string (string_of_id id) ^ " =") ^//^ loop_body)
+ ^/^ string "in"
+ ^/^ (string "loop" ^^ space ^^ ocaml_atomic_exp ctx exp_from)
| _ -> string ("EXP(" ^ string_of_exp exp ^ ")")
and ocaml_letbind ctx (LB_aux (lb_aux, _)) =
match lb_aux with
| LB_val (pat, exp) -> separate space [ocaml_pat ctx pat; equals; ocaml_atomic_exp ctx exp]
- | _ -> failwith "Ocaml: Explicit letbind found"
and ocaml_pexps ctx = function
| [pexp] -> ocaml_pexp ctx pexp
| pexp :: pexps -> ocaml_pexp ctx pexp ^/^ ocaml_pexps ctx pexps
@@ -166,7 +194,7 @@ and ocaml_pexp ctx = function
separate space [bar; ocaml_pat ctx pat; string "->"]
^//^ group (ocaml_exp ctx exp)
| Pat_aux (Pat_when (pat, wh, exp), _) ->
- separate space [bar; ocaml_pat ctx pat; string "when"; ocaml_atomic_exp ctx exp; string "->"]
+ separate space [bar; ocaml_pat ctx pat; string "when"; ocaml_atomic_exp ctx wh; string "->"]
^//^ group (ocaml_exp ctx exp)
and ocaml_block ctx = function
| [exp] -> ocaml_exp ctx exp
@@ -182,7 +210,8 @@ and ocaml_atomic_exp ctx (E_aux (exp_aux, _) as exp) =
match Env.lookup_id id (env_of exp) with
| Local (Immutable, _) | Unbound -> zencode ctx id
| Enum _ | Union _ -> zencode_upper ctx id
- | Register _ | Local (Mutable, _) -> bang ^^ zencode ctx id
+ | Register _ -> parens (string ("trace \"REG: " ^ string_of_id id ^ "\";") ^^ space ^^ bang ^^ zencode ctx id)
+ | Local (Mutable, _) -> bang ^^ zencode ctx id
end
| E_list exps -> enclose lbracket rbracket (separate_map (semi ^^ space) (ocaml_exp ctx) exps)
| E_tuple exps -> parens (separate_map (comma ^^ space) (ocaml_exp ctx) exps)
@@ -234,15 +263,25 @@ let rec ocaml_funcl_matches ctx = function
| [clause] -> ocaml_funcl_match ctx clause
| (clause :: clauses) -> ocaml_funcl_match ctx clause ^/^ ocaml_funcl_matches ctx clauses
+let first_function = ref true
+
+let function_header () =
+ if !first_function
+ then (first_function := false; string "let rec")
+ else string "and"
+
let ocaml_funcls ctx = function
| [] -> failwith "Ocaml: empty function"
| [FCL_aux (FCL_Funcl (id, pat, exp),_)] ->
- separate space [string "let rec"; zencode ctx id; ocaml_pat ctx pat; equals; string "with_return (fun r ->"]
+ let Typ_aux (Typ_fn (typ1, typ2, _), _) = Bindings.find id ctx.val_specs in
+ let annot_pat = parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx typ1) in
+ let dbg = string ("trace_call \"Calling: " ^ string_of_id id ^ "\";") in
+ separate space [function_header (); zencode ctx id; annot_pat; colon; ocaml_typ ctx typ2; equals; dbg; string "with_return (fun r ->"]
^//^ ocaml_exp ctx exp
^^ rparen
| funcls ->
let id = funcls_id funcls in
- separate space [string "let rec"; zencode ctx id; equals; string "function"]
+ separate space [function_header (); zencode ctx id; equals; string "function"]
^//^ ocaml_funcl_matches ctx funcls
let ocaml_fundef ctx (FD_aux (FD_function (_, _, _, funcls), _)) =
@@ -303,15 +342,35 @@ let get_externs (Defs defs) =
let ocaml_def_end = string ";;" ^^ twice hardline
+let nf_group doc =
+ first_function := true;
+ group doc
+
let ocaml_def ctx def = match def with
- | DEF_reg_dec ds -> group (ocaml_dec_spec ctx ds) ^^ ocaml_def_end
- | DEF_fundef fd -> group (ocaml_fundef ctx fd) ^^ ocaml_def_end
- | DEF_type td -> group (ocaml_typedef ctx td) ^^ ocaml_def_end
+ | DEF_reg_dec ds -> nf_group (ocaml_dec_spec ctx ds) ^^ ocaml_def_end
+ | DEF_fundef fd -> group (ocaml_fundef ctx fd) ^^ twice hardline
+ | DEF_type td -> nf_group (ocaml_typedef ctx td) ^^ ocaml_def_end
+ | DEF_val lb -> nf_group (string "let" ^^ space ^^ ocaml_letbind ctx lb) ^^ ocaml_def_end
| _ -> empty
+let val_spec_typs (Defs defs) =
+ let typs = ref (Bindings.empty) in
+ let val_spec_typ (VS_aux (vs_aux, _)) =
+ match vs_aux with
+ | VS_val_spec (TypSchm_aux (TypSchm_ts (_, typ), _), id, _, _) -> typs := Bindings.add id typ !typs
+ in
+ let rec vs_typs = function
+ | DEF_spec vs :: defs -> val_spec_typ vs; vs_typs defs
+ | _ :: defs -> vs_typs defs
+ | [] -> []
+ in
+ vs_typs defs;
+ !typs
+
let ocaml_defs (Defs defs) =
let ctx = { register_inits = get_initialize_registers defs;
- externs = get_externs (Defs defs)
+ externs = get_externs (Defs defs);
+ val_specs = val_spec_typs (Defs defs)
}
in
let empty_reg_init =
@@ -333,6 +392,7 @@ let ocaml_main spec =
^//^ (string "Random.self_init ();"
^/^ string "load_elf ();"
^/^ string "initialize_registers ();"
+ ^/^ string "Printexc.record_backtrace true;"
^/^ string "zmain ()")
]
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index a890e039..0cb95db1 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -62,7 +62,7 @@ let is_number_char c =
c = '0' || c = '1' || c = '2' || c = '3' || c = '4' || c = '5' ||
c = '6' || c = '7' || c = '8' || c = '9'
-let fix_id remove_tick name = match name with
+let rec fix_id remove_tick name = match name with
| "assert"
| "lsl"
| "lsr"
@@ -82,7 +82,9 @@ let fix_id remove_tick name = match name with
| "integer"
-> name ^ "'"
| _ ->
- if name.[0] = '\'' then
+ if String.contains name '#' then
+ fix_id remove_tick (String.concat "_" (Util.split_on_char '#' name))
+ else if name.[0] = '\'' then
let var = String.sub name 1 (String.length name - 1) in
if remove_tick then var else (var ^ "'")
else if is_number_char(name.[0]) then
@@ -285,9 +287,9 @@ let doc_lit_lem sequential mwords in_pat (L_aux(lit,l)) a =
| Typ_app (Id_aux (Id "register", _),_) -> utf8string "UndefinedRegister 0"
| Typ_id (Id_aux (Id "string", _)) -> utf8string "\"\""
| _ ->
+ let ta = if contains_t_pp_var typ then empty else doc_tannot_lem sequential mwords false typ in
parens
- ((utf8string "(failwith \"undefined value of unsupported type\")") ^^
- (doc_tannot_lem sequential mwords false typ)))
+ ((utf8string "(failwith \"undefined value of unsupported type\")") ^^ ta))
| _ -> utf8string "(failwith \"undefined value of unsupported type\")")
| L_string s -> utf8string ("\"" ^ s ^ "\"")
| L_real s ->
@@ -1058,7 +1060,15 @@ let doc_exp_lem, doc_let_lem =
raise (Reporting_basic.err_unreachable l
"pretty-printing non-constant sizeof expressions to Lem not supported"))
| E_return r ->
- align (string "early_return" ^//^ expV true r)
+ let ret_monad = if sequential then " : MR regstate" else " : MR" in
+ let ta =
+ if contains_t_pp_var (typ_of full_exp) || contains_t_pp_var (typ_of r)
+ then empty
+ else separate space
+ [string ret_monad;
+ parens (doc_typ_lem sequential mwords (typ_of full_exp));
+ parens (doc_typ_lem sequential mwords (typ_of r))] in
+ align (parens (string "early_return" ^//^ expV true r ^//^ ta))
| E_constraint _ | E_comment _ | E_comment_struc _ -> empty
| E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _ | E_internal_exp_user _ ->
raise (Reporting_basic.err_unreachable l
@@ -1110,9 +1120,10 @@ let rec doc_range_lem (BF_aux(r,_)) = match r with
| BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2)
let doc_typdef_lem sequential mwords (TD_aux(td, (l, annot))) = match td with
- | TD_abbrev(id,nm,typschm) ->
- doc_op equals (concat [string "type"; space; doc_id_lem_type id])
- (doc_typschm_lem sequential mwords false typschm)
+ | TD_abbrev(id,nm,(TypSchm_aux (TypSchm_ts (typq, _), _) as typschm)) ->
+ doc_op equals
+ (separate space [string "type"; doc_id_lem_type id; doc_typquant_items_lem typq])
+ (doc_typschm_lem sequential mwords false typschm)
| TD_record(id,nm,typq,fs,_) ->
let fname fid = if prefix_recordtype
then concat [doc_id_lem id;string "_";doc_id_lem_type fid;]
@@ -1575,6 +1586,7 @@ let rec doc_def_lem sequential mwords def =
(* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *)
match def with
| DEF_spec v_spec -> (empty,doc_spec_lem sequential mwords v_spec)
+ | DEF_fixity _ -> (empty,empty)
| DEF_overload _ -> (empty,empty)
| DEF_type t_def -> (group (doc_typdef_lem sequential mwords t_def) ^/^ hardline,empty)
| DEF_reg_dec dec -> (group (doc_dec_lem sequential dec),empty)
diff --git a/src/pretty_print_lem_ast.ml b/src/pretty_print_lem_ast.ml
index 2e464a08..2232b4de 100644
--- a/src/pretty_print_lem_ast.ml
+++ b/src/pretty_print_lem_ast.ml
@@ -234,6 +234,17 @@ let pp_lem_nexp ppf n = base ppf (pp_format_nexp_lem n)
let pp_lem_ord ppf o = base ppf (pp_format_ord_lem o)
let pp_lem_effects ppf e = base ppf (pp_format_effects_lem e)
let pp_lem_beffect ppf be = base ppf (pp_format_base_effect_lem be)
+let pp_lem_loop ppf l =
+ let l_str = match l with
+ | While -> "While"
+ | Until -> "Until" in
+ base ppf l_str
+let pp_lem_prec ppf p =
+ let p_str = match p with
+ | Infix -> "Infix"
+ | InfixL -> "InfixL"
+ | InfixR -> "InfixR" in
+ base ppf p_str
let pp_lem_nexp_constraint ppf nc = base ppf (pp_format_nexp_constraint_lem nc)
@@ -380,6 +391,9 @@ and pp_lem_exp ppf (E_aux(e,(l,annot))) =
fprintf ppf "@[<0>(E_aux (E_for %a %a %a %a %a @ @[<1> %a @]) (%a, %a))@]"
pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3
pp_lem_ord order pp_lem_exp exp4 pp_lem_l l pp_annot annot
+ | E_loop(loop,cond,body) ->
+ fprintf ppf "@[<0>(E_aux (E_loop %a %a @ @[<1> %a @]) (%a, %a))@]"
+ pp_lem_loop loop pp_lem_exp cond pp_lem_exp body pp_lem_l l pp_annot annot
| E_vector(exps) -> fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]"
kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot
| E_vector_access(v,e) ->
@@ -634,6 +648,7 @@ let pp_lem_def ppf d =
| DEF_val(lbind) -> fprintf ppf "(DEF_val %a);@\n" pp_lem_let lbind
| DEF_reg_dec(dec) -> fprintf ppf "(DEF_reg_dec %a);@\n" pp_lem_dec dec
| DEF_comm d -> fprintf ppf ""
+ | DEF_fixity (prec, n, id) -> fprintf ppf "(DEF_fixity %a %s %a);@\n" pp_lem_prec prec (lemnum string_of_int n) pp_lem_id id
| _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs")
let pp_lem_defs ppf (Defs(defs)) =
diff --git a/src/process_file.ml b/src/process_file.ml
index d35ccf5e..18df5047 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -259,5 +259,6 @@ let rewrite rewriters defs =
exit 1
let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
+let rewrite_undefined = rewrite [("undefined", Rewriter.rewrite_undefined)]
let rewrite_ast_lem = rewrite Rewriter.rewrite_defs_lem
let rewrite_ast_ocaml = rewrite Rewriter.rewrite_defs_ocaml
diff --git a/src/process_file.mli b/src/process_file.mli
index c477d185..fae38100 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -45,6 +45,7 @@ val convert_ast : Ast.order -> Parse_ast.defs -> unit Ast.defs
val check_ast: unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
val monomorphise_ast : ((string * int) * string) list -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_undefined: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
val rewrite_ast_ocaml : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
diff --git a/src/rewriter.ml b/src/rewriter.ml
index bcc4e60a..60beadac 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -76,12 +76,18 @@ let effect_of_pexp (Pat_aux (pexp,(_,a))) = match a with
let effect_of_lb (LB_aux (_,(_,a))) = effect_of_annot a
let get_loc_exp (E_aux (_,(l,_))) = l
+let gen_loc l = Parse_ast.Generated l
-let simple_annot l typ = (Parse_ast.Generated l, Some (Env.empty, typ, no_effect))
+let simple_annot l typ = (gen_loc l, Some (Env.empty, typ, no_effect))
let simple_num l n = E_aux (
- E_lit (L_aux (L_num n, Parse_ast.Generated l)),
- simple_annot (Parse_ast.Generated l)
- (atom_typ (Nexp_aux (Nexp_constant n, Parse_ast.Generated l))))
+ E_lit (L_aux (L_num n, gen_loc l)),
+ simple_annot (gen_loc l)
+ (atom_typ (Nexp_aux (Nexp_constant n, gen_loc l))))
+let annot_exp_effect e_aux l env typ effect = E_aux (e_aux, (l, Some (env, typ, effect)))
+let annot_exp e_aux l env typ = annot_exp_effect e_aux l env typ no_effect
+let annot_pat p_aux l env typ = P_aux (p_aux, (l, Some (env, typ, no_effect)))
+let annot_letbind (p_aux, exp) l env typ =
+ LB_aux (LB_val (annot_pat p_aux l env typ, exp), (l, Some (env, typ, effect_of exp)))
let rec small (E_aux (exp,_)) = match exp with
| E_id _
@@ -103,15 +109,15 @@ let reset_fresh_name_counter () =
let fresh_id pre l =
let current = fresh_name () in
- Id_aux (Id (pre ^ string_of_int current), Parse_ast.Generated l)
+ Id_aux (Id (pre ^ string_of_int current), gen_loc l)
let fresh_id_exp pre ((l,annot)) =
let id = fresh_id pre l in
- E_aux (E_id id, (Parse_ast.Generated l, annot))
+ E_aux (E_id id, (gen_loc l, annot))
let fresh_id_pat pre ((l,annot)) =
let id = fresh_id pre l in
- P_aux (P_id id, (Parse_ast.Generated l, annot))
+ P_aux (P_id id, (gen_loc l, annot))
let union_eff_exps es =
List.fold_left union_effects no_effect (List.map effect_of es)
@@ -237,7 +243,8 @@ let effectful_effs = function
) effs
| _ -> true
-let effectful eaux = effectful_effs (effect_of eaux)
+let effectful eaux = effectful_effs (effect_of (propagate_exp_effect eaux))
+let effectful_pexp pexp = effectful_effs (snd (propagate_pexp_effect pexp))
let updates_vars_effs = function
| Effect_aux (Effect_set effs, _) ->
@@ -349,9 +356,9 @@ let vector_string_to_bit_list l lit =
| L_bin s_bin -> explode s_bin
| _ -> raise (Reporting_basic.err_unreachable l "s_bin given non vector literal") in
- List.map (function '0' -> L_aux (L_zero, Parse_ast.Generated l)
- | '1' -> L_aux (L_one,Parse_ast.Generated l)
- | _ -> raise (Reporting_basic.err_unreachable (Parse_ast.Generated l) "binary had non-zero or one")) s_bin
+ List.map (function '0' -> L_aux (L_zero, gen_loc l)
+ | '1' -> L_aux (L_one,gen_loc l)
+ | _ -> raise (Reporting_basic.err_unreachable (gen_loc l) "binary had non-zero or one")) s_bin
let rewrite_pat rewriters (P_aux (pat,(l,annot))) =
let rewrap p = P_aux (p,(l,annot)) in
@@ -1079,7 +1086,7 @@ let rewrite_sizeof (Defs defs) =
when string_of_id atom = "atom" ->
[nexp, E_id id]
| Typ_app (vector, _) when string_of_id vector = "vector" ->
- let id_length = Id_aux (Id "length", Parse_ast.Generated l) in
+ let id_length = Id_aux (Id "length", gen_loc l) in
(try
(match Env.get_val_spec id_length (env_of_annot annot) with
| _ ->
@@ -1115,7 +1122,8 @@ let rewrite_sizeof (Defs defs) =
(* Rewrite calls to functions which have had parameters added to pass values
of type-level variables; these are added as sizeof expressions first, and
then further rewritten as above. *)
- let e_app_aux param_map ((exp, exp_orig), ((l, Some (env, _, _)) as annot)) =
+ let e_app_aux param_map ((exp, exp_orig), ((l, _) as annot)) =
+ let env = env_of_annot annot in
let full_exp = E_aux (exp, annot) in
let orig_exp = E_aux (exp_orig, annot) in
match exp with
@@ -1143,7 +1151,7 @@ let rewrite_sizeof (Defs defs) =
(* If the type variable is Not_found then it was probably
introduced by a P_var pattern, so it likely exists as
a variable in scope. It can't be an existential because the assert rules that out. *)
- | None -> E_aux (E_id (id_of_kid (orig_kid kid)), simple_annot l (atom_typ (nvar (orig_kid kid))))
+ | None -> annot_exp (E_id (id_of_kid (orig_kid kid))) l env (atom_typ (nvar (orig_kid kid)))
| _ ->
raise (Reporting_basic.err_unreachable l
("failed to infer nexp for type variable " ^ string_of_kid kid ^
@@ -1415,6 +1423,7 @@ let remove_vector_concat_pat pat =
(* build a let-expression of the form "let child = root[i..j] in body" *)
let letbind_vec typ_opt (rootid,rannot) (child,cannot) (i,j) =
let (l,_) = cannot in
+ let env = env_of_annot rannot in
let rootname = string_of_id rootid in
let childname = string_of_id child in
@@ -1434,7 +1443,7 @@ let remove_vector_concat_pat pat =
| None -> P_aux (P_id child,cannot) in
let letbind = fix_eff_lb (LB_aux (LB_val (id_pat,subv),cannot)) in
(letbind,
- (fun body -> fix_eff_exp (E_aux (E_let (letbind,body), simple_annot l (typ_of body)))),
+ (fun body -> fix_eff_exp (annot_exp (E_let (letbind,body)) l env (typ_of body))),
(rootname,childname)) in
let p_aux = function
@@ -1562,7 +1571,7 @@ let remove_vector_concat_pat pat =
let typ = Env.base_typ_of env (typ_of_annot annot) in
let eff = effect_of_annot (snd annot) in
let (l,_) = annot in
- let wild _ = P_aux (P_wild,(Parse_ast.Generated l, Some (env, bit_typ, eff))) in
+ let wild _ = P_aux (P_wild,(gen_loc l, Some (env, bit_typ, eff))) in
if is_vector_typ typ then
match p, vector_typ_args_of typ with
| P_vector ps,_ -> acc @ ps
@@ -1751,10 +1760,17 @@ and fpat_to_fexp (FP_aux (FP_Fpat (id,pat),(l,annot))) =
FE_aux (FE_Fexp (id, pat_to_exp pat),(l,annot))
let case_exp e t cs =
- let pexp (pat,body,annot) = Pat_aux (Pat_exp (pat,body),annot) in
- let ps = List.map pexp cs in
- (* let efr = union_effs (List.map effect_of_pexp ps) in *)
- fix_eff_exp (E_aux (E_case (e,ps), (get_loc_exp e, Some (env_of e, t, no_effect))))
+ let l = get_loc_exp e in
+ let env = env_of e in
+ let annot = (get_loc_exp e, Some (env_of e, t, no_effect)) in
+ match cs with
+ | [(P_aux (P_id id, pannot) as pat, body, _)] ->
+ fix_eff_exp (annot_exp (E_let (LB_aux (LB_val (pat, e), pannot), body)) l env t)
+ | _ ->
+ let pexp (pat,body,annot) = Pat_aux (Pat_exp (pat,body),annot) in
+ let ps = List.map pexp cs in
+ (* let efr = union_effs (List.map effect_of_pexp ps) in *)
+ fix_eff_exp (annot_exp (E_case (e,ps)) l env t)
let rewrite_guarded_clauses l cs =
let rec group clauses =
@@ -1800,7 +1816,7 @@ let rewrite_guarded_clauses l cs =
if equiv_pats current_pat pat'
then if_exp current_pat (c' :: cs)
else case_exp (pat_to_exp current_pat) (typ_of body') (group (c' :: cs)) in
- fix_eff_exp (E_aux (E_if (exp,body,else_exp), simple_annot (fst annot) (typ_of body)))
+ fix_eff_exp (annot_exp (E_if (exp,body,else_exp)) (fst annot) (env_of exp) (typ_of body))
| None -> body)
| [(pat,guard,body,annot)] -> body
| [] ->
@@ -1810,8 +1826,8 @@ let rewrite_guarded_clauses l cs =
let bitwise_and_exp exp1 exp2 =
let (E_aux (_,(l,_))) = exp1 in
- let andid = Id_aux (Id "bool_and", Parse_ast.Generated l) in
- E_aux (E_app(andid,[exp1;exp2]), simple_annot l bool_typ)
+ let andid = Id_aux (Id "bool_and", gen_loc l) in
+ annot_exp (E_app(andid,[exp1;exp2])) l (env_of exp1) bool_typ
let rec contains_bitvector_pat (P_aux (pat,annot)) = match pat with
| P_lit _ | P_wild | P_id _ -> false
@@ -1833,6 +1849,8 @@ let contains_bitvector_pexp = function
let remove_bitvector_pat pat =
+ let env = try pat_env_of pat with _ -> Env.empty in
+
(* first introduce names for bitvector patterns *)
let name_bitvector_roots =
{ p_lit = (fun lit -> P_lit lit)
@@ -1868,23 +1886,20 @@ let remove_bitvector_pat pat =
bindings for the bits bound by P_id or P_as patterns *)
(* Helper functions for generating guard expressions *)
- let access_bit_exp (rootid,rannot) l idx =
- let root : tannot exp = E_aux (E_id rootid,rannot) in
+ let access_bit_exp rootid l typ idx =
+ let root = annot_exp (E_id rootid) l env typ in
(* FIXME *)
- E_aux (E_vector_access (root,simple_num l idx), simple_annot l bit_typ) in
+ annot_exp (E_vector_access (root, simple_num l idx)) l env bit_typ in
(*let env = env_of_annot rannot in
let t = Env.base_typ_of env (typ_of_annot rannot) in
let (_, _, ord, _) = vector_typ_args_of t in
let access_id = if is_order_inc ord then "bitvector_access_inc" else "bitvector_access_dec" in
E_aux (E_app (mk_id access_id, [root; simple_num l idx]), simple_annot l bit_typ) in*)
- let test_bit_exp rootid l t idx exp =
- let rannot = simple_annot l t in
- let elem = access_bit_exp (rootid,rannot) l idx in
- let eqid = Id_aux (Id "eq", Parse_ast.Generated l) in
- let eqannot = simple_annot l bool_typ in
- let eqexp : tannot exp = E_aux (E_app(eqid,[elem;exp]), eqannot) in
- Some (eqexp) in
+ let test_bit_exp rootid l typ idx exp =
+ let rannot = (l, Some (env_of exp, typ, no_effect)) in
+ let elem = access_bit_exp rootid l typ idx in
+ Some (annot_exp (E_app (mk_id "eq", [elem; exp])) l env bool_typ) in
let test_subvec_exp rootid l typ i j lits =
let (start, length, ord, _) = vector_typ_args_of typ in
@@ -1903,25 +1918,24 @@ let remove_bitvector_pat pat =
then E_id rootid
else*)
E_vector_subrange (
- E_aux (E_id rootid, simple_annot l typ),
+ annot_exp (E_id rootid) l env typ,
simple_num l i,
simple_num l j) in
(* let subrange_id = if is_order_inc ord then "bitvector_subrange_inc" else "bitvector_subrange_dec" in
E_app (mk_id subrange_id, [E_aux (E_id rootid, simple_annot l typ); simple_num l i; simple_num l j]) in *)
- E_aux (E_app(
- Id_aux (Id "eq_vec", Parse_ast.Generated l),
- [E_aux (subvec_exp, simple_annot l typ');
- E_aux (E_vector lits, simple_annot l typ')]),
- simple_annot l bool_typ) in
+ annot_exp (E_app(
+ Id_aux (Id "eq_vec", gen_loc l),
+ [annot_exp subvec_exp l env typ';
+ annot_exp (E_vector lits) l env typ'])) l env bool_typ in
let letbind_bit_exp rootid l typ idx id =
let rannot = simple_annot l typ in
- let elem = access_bit_exp (rootid,rannot) l idx in
- let e = P_aux (P_id id, simple_annot l bit_typ) in
- let letbind = LB_aux (LB_val (e,elem), simple_annot l bit_typ) in
+ let elem = access_bit_exp rootid l typ idx in
+ let e = annot_pat (P_id id) l env bit_typ in
+ let letbind = LB_aux (LB_val (e,elem), (l, Some (env, bit_typ, no_effect))) in
let letexp = (fun body ->
let (E_aux (_,(_,bannot))) = body in
- E_aux (E_let (letbind,body), (Parse_ast.Generated l, bannot))) in
+ annot_exp (E_let (letbind,body)) l env (typ_of body)) in
(letexp, letbind) in
let compose_guards guards =
@@ -1946,7 +1960,7 @@ let remove_bitvector_pat pat =
| pat :: ps' ->
(match pat with
| P_aux (P_lit lit, (l,annot)) ->
- let e = E_aux (E_lit lit, (Parse_ast.Generated l, annot)) in
+ let e = E_aux (E_lit lit, (gen_loc l, annot)) in
let current' = (match current with
| Some (l,i,j,lits) -> Some (l,i,idx,lits @ [e])
| None -> Some (l,idx,idx,[e])) in
@@ -2243,7 +2257,7 @@ let rewrite_exp_lift_assign_intro rewriters ((E_aux (exp,((l,_) as annot))) as f
when lexp_is_local_intro le (env_of full_exp) && not (lexp_is_effectful le) ->
let (le', re') = rewrite_local_lexp le in
let e' = re' (rewrite_base e) in
- let block = E_aux (E_block [], simple_annot l unit_typ) in
+ let block = annot_exp (E_block []) l (env_of full_exp) unit_typ in
fix_eff_exp (E_aux (E_internal_let(le', e', block), annot))
| _ -> rewrite_base full_exp
@@ -2328,13 +2342,13 @@ let rewrite_defs_early_return =
match es with
| [E_aux (e, _)] -> e
| _ :: _ when is_return (Util.last es) ->
- let (E_aux (_, annot) as e) = Util.last es in
+ let (E_aux (_, annot) as e) = get_return (Util.last es) in
E_return (E_aux (E_block (Util.butlast es @ [get_return e]), annot))
| _ -> E_block es in
let e_if (e1, e2, e3) =
if is_return e2 && is_return e3 then
- let (E_aux (_, annot)) = e2 in
+ let (E_aux (_, annot)) = get_return e2 in
E_return (E_aux (E_if (e1, get_return e2, get_return e3), annot))
else E_if (e1, e2, e3) in
@@ -2344,7 +2358,7 @@ let rewrite_defs_early_return =
let get_return_pexp (Pat_aux (pexp, a)) = match pexp with
| Pat_exp (p, e) -> Pat_aux (Pat_exp (p, get_return e), a)
| Pat_when (p, g, e) -> Pat_aux (Pat_when (p, g, get_return e), a) in
- let annot = match pes with
+ let annot = match List.map get_return_pexp pes with
| Pat_aux (Pat_exp (_, E_aux (_, annot)), _) :: _ -> annot
| Pat_aux (Pat_when (_, _, E_aux (_, annot)), _) :: _ -> annot
| [] -> (Parse_ast.Unknown, None) in
@@ -2526,6 +2540,26 @@ let rewrite_undefined =
let rewrite_exp_undefined = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in
rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp_undefined) }
+let rec simple_typ (Typ_aux (typ_aux, l) as typ) = Typ_aux (simple_typ_aux typ_aux, l)
+and simple_typ_aux = function
+ | Typ_wild -> Typ_wild
+ | Typ_id id -> Typ_id id
+ | Typ_app (id, [_; _; _; Typ_arg_aux (Typ_arg_typ typ, l)]) when Id.compare id (mk_id "vector") = 0 ->
+ Typ_app (mk_id "list", [Typ_arg_aux (Typ_arg_typ (simple_typ typ), l)])
+ | Typ_app (id, [_]) when Id.compare id (mk_id "atom") = 0 ->
+ Typ_id (mk_id "int")
+ | Typ_app (id, [_; _]) when Id.compare id (mk_id "range") = 0 ->
+ Typ_id (mk_id "int")
+ | Typ_app (id, args) -> Typ_app (id, List.concat (List.map simple_typ_arg args))
+ | Typ_fn (typ1, typ2, effs) -> Typ_fn (simple_typ typ1, simple_typ typ2, effs)
+ | Typ_tup typs -> Typ_tup (List.map simple_typ typs)
+ | Typ_exist (_, _, Typ_aux (typ, l)) -> simple_typ_aux typ
+ | typ_aux -> typ_aux
+and simple_typ_arg (Typ_arg_aux (typ_arg_aux, l)) =
+ match typ_arg_aux with
+ | Typ_arg_typ typ -> [Typ_arg_aux (Typ_arg_typ (simple_typ typ), l)]
+ | _ -> []
+
(* This pass aims to remove all the Num quantifiers from the specification. *)
let rewrite_simple_types (Defs defs) =
let is_simple = function
@@ -2537,26 +2571,6 @@ let rewrite_simple_types (Defs defs) =
| TypQ_no_forall -> TypQ_aux (TypQ_no_forall, annot)
| TypQ_tq quants -> TypQ_aux (TypQ_tq (List.filter (fun q -> is_simple q) quants), annot)
in
- let rec simple_typ (Typ_aux (typ_aux, l) as typ) = Typ_aux (simple_typ_aux typ_aux, l)
- and simple_typ_aux = function
- | Typ_wild -> Typ_wild
- | Typ_id id -> Typ_id id
- | Typ_app (id, [_; _; _; Typ_arg_aux (Typ_arg_typ typ, l)]) when Id.compare id (mk_id "vector") = 0 ->
- Typ_app (mk_id "list", [Typ_arg_aux (Typ_arg_typ (simple_typ typ), l)])
- | Typ_app (id, [_]) when Id.compare id (mk_id "atom") = 0 ->
- Typ_id (mk_id "int")
- | Typ_app (id, [_; _]) when Id.compare id (mk_id "range") = 0 ->
- Typ_id (mk_id "int")
- | Typ_app (id, args) -> Typ_app (id, List.concat (List.map simple_typ_arg args))
- | Typ_fn (typ1, typ2, effs) -> Typ_fn (simple_typ typ1, simple_typ typ2, effs)
- | Typ_tup typs -> Typ_tup (List.map simple_typ typs)
- | Typ_exist (_, _, Typ_aux (typ, l)) -> simple_typ_aux typ
- | typ_aux -> typ_aux
- and simple_typ_arg (Typ_arg_aux (typ_arg_aux, l)) =
- match typ_arg_aux with
- | Typ_arg_typ typ -> [Typ_arg_aux (Typ_arg_typ (simple_typ typ), l)]
- | _ -> []
- in
let simple_typschm (TypSchm_aux (TypSchm_ts (typq, typ), annot)) =
TypSchm_aux (TypSchm_ts (simple_typquant typq, simple_typ typ), annot)
in
@@ -2621,7 +2635,7 @@ let rewrite_tuple_vector_assignments defs =
let i = match simplify_nexp start with
| (Nexp_aux (Nexp_constant i, _)) -> i
| _ -> if is_order_inc ord then 0 else List.length lexps - 1 in
- let l = Parse_ast.Generated (fst annot) in
+ let l = gen_loc (fst annot) in
let exp' =
if small exp then strip_exp exp
else mk_exp (E_id (mk_id "split_vec")) in
@@ -2699,14 +2713,19 @@ let rewrite_simple_assignments defs =
let rewrite_defs_remove_blocks =
let letbind_wild v body =
+ let l = get_loc_exp v in
+ let env = env_of v in
+ let typ = typ_of v in
+ annot_exp (E_let (annot_letbind (P_wild, v) l env typ, body)) l env (typ_of body) in
+ (* let pat = annot_pat P_wild l env typ in
let (E_aux (_,(l,tannot))) = v in
let annot_pat = (simple_annot l (typ_of v)) in
- let annot_lb = (Parse_ast.Generated l, tannot) in
- let annot_let = (Parse_ast.Generated l, Some (env_of body, typ_of body, union_eff_exps [v;body])) in
- E_aux (E_let (LB_aux (LB_val (P_aux (P_wild,annot_pat),v),annot_lb),body),annot_let) in
+ let annot_lb = (gen_loc l, tannot) in
+ let annot_let = (gen_loc l, Some (env_of body, typ_of body, union_eff_exps [v;body])) in
+ E_aux (E_let (LB_aux (LB_val (P_aux (P_wild,annot_pat),v),annot_lb),body),annot_let) in *)
let rec f l = function
- | [] -> E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)), (simple_annot l unit_typ))
+ | [] -> E_aux (E_lit (L_aux (L_unit,gen_loc l)), (simple_annot l unit_typ))
| [e] -> e (* check with Kathy if that annotation is fine *)
| e :: es -> letbind_wild e (f l es) in
@@ -2733,27 +2752,15 @@ let letbind (v : 'a exp) (body : 'a exp -> 'a exp) : 'a exp =
let (E_aux (_,(l,annot))) = v in
match annot with
| Some (env, Typ_aux (Typ_id tid, _), eff) when string_of_id tid = "unit" ->
- let e = E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)),(simple_annot l unit_typ)) in
- let body = body e in
+ let body = body (annot_exp (E_lit (mk_lit L_unit)) l env unit_typ) in
let body_typ = try typ_of body with _ -> unit_typ in
- let annot_pat = simple_annot l unit_typ in
- let annot_lb = annot_pat in
- let annot_let = (Parse_ast.Generated l, Some (env, body_typ, union_eff_exps [v;body])) in
- let pat = P_aux (P_wild,annot_pat) in
-
- E_aux (E_let (LB_aux (LB_val (pat,v),annot_lb),body),annot_let)
+ let lb = annot_letbind (P_wild, v) l env unit_typ in
+ propagate_exp_effect (annot_exp (E_let (lb, body)) l env body_typ)
| Some (env, typ, eff) ->
let id = fresh_id "w__" l in
- let annot_pat = simple_annot l typ in
- let e_id = E_aux (E_id id, (Parse_ast.Generated l, Some (env, typ, no_effect))) in
- let body = body e_id in
- let body_typ = try typ_of body with _ -> unit_typ in
-
- let annot_lb = annot_pat in
- let annot_let = (Parse_ast.Generated l, Some (env, body_typ, union_eff_exps [v;body])) in
- let pat = P_aux (P_id id,annot_pat) in
-
- E_aux (E_let (LB_aux (LB_val (pat,v),annot_lb),body),annot_let)
+ let lb = annot_letbind (P_id id, v) l env typ in
+ let body = body (annot_exp (E_id id) l env typ) in
+ propagate_exp_effect (annot_exp (E_let (lb, body)) l env (typ_of body))
| None ->
raise (Reporting_basic.err_unreachable l "no type information")
@@ -2853,8 +2860,8 @@ let rewrite_defs_letbind_effects =
let (E_aux (_,(l,tannot))) = exp in
let exp =
if newreturn then
- let typ = try typ_of exp with _ -> unit_typ in
- E_aux (E_internal_return exp, simple_annot l typ)
+ (* let typ = try typ_of exp with _ -> unit_typ in *)
+ annot_exp (E_internal_return exp) l (env_of exp) (typ_of exp)
else
exp in
(* n_exp_term forces an expression to be translated into a form
@@ -2947,10 +2954,7 @@ let rewrite_defs_letbind_effects =
n_exp_name exp1 (fun exp1 ->
k (rewrap (E_field (exp1,id))))
| E_case (exp1,pexps) ->
- let newreturn =
- List.fold_left
- (fun b pexp -> b || (try effectful_effs (effect_of_pexp pexp) with _ -> false))
- false pexps in
+ let newreturn = List.exists effectful_pexp pexps in
n_exp_name exp1 (fun exp1 ->
n_pexpL newreturn pexps (fun pexps ->
k (rewrap (E_case (exp1,pexps)))))
@@ -2995,10 +2999,8 @@ let rewrite_defs_letbind_effects =
| E_internal_plet _ -> failwith "E_internal_plet should not be here yet" in
let rewrite_fun _ (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),fdannot)) =
- let newreturn =
- List.fold_left
- (fun b (FCL_aux (FCL_Funcl(id,pat,exp),(_,annot))) ->
- b || (try effectful exp with _ -> false)) false funcls in
+ let effectful_funcl (FCL_aux (FCL_Funcl(_, _, exp), _)) = effectful exp in
+ let newreturn = List.exists effectful_funcl funcls in
let rewrite_funcl (FCL_aux (FCL_Funcl(id,pat,exp),annot)) =
let _ = reset_fresh_name_counter () in
FCL_aux (FCL_Funcl (id,pat,n_exp_term newreturn exp),annot)
@@ -3110,27 +3112,25 @@ let swaptyp typ (l,tannot) = match tannot with
let mktup l es =
match es with
- | [] -> E_aux (E_lit (L_aux (L_unit,Parse_ast.Generated l)),(simple_annot l unit_typ))
+ | [] -> annot_exp (E_lit (mk_lit L_unit)) (gen_loc l) Env.empty unit_typ
| [e] -> e
- | e :: _ ->
- let effs =
- List.fold_left (fun acc e -> union_effects acc (effect_of e)) no_effect es in
+ | e :: _ ->
let typ = mk_typ (Typ_tup (List.map typ_of es)) in
- E_aux (E_tuple es,(Parse_ast.Generated l, Some (env_of e, typ, effs)))
+ propagate_exp_effect (annot_exp (E_tuple es) (gen_loc l) (env_of e) typ)
let mktup_pat l es =
match es with
- | [] -> P_aux (P_wild,(simple_annot l unit_typ))
+ | [] -> annot_pat P_wild (gen_loc l) Env.empty unit_typ
| [E_aux (E_id id,_) as exp] ->
- P_aux (P_id id,(simple_annot l (typ_of exp)))
- | _ ->
+ annot_pat (P_id id) (gen_loc l) (env_of exp) (typ_of exp)
+ | exp :: _ ->
let typ = mk_typ (Typ_tup (List.map typ_of es)) in
let pats = List.map (function
| (E_aux (E_id id,_) as exp) ->
- P_aux (P_id id,(simple_annot l (typ_of exp)))
+ annot_pat (P_id id) (gen_loc l) (env_of exp) (typ_of exp)
| exp ->
- P_aux (P_wild,(simple_annot l (typ_of exp)))) es in
- P_aux (P_tup pats,(simple_annot l typ))
+ annot_pat P_wild (gen_loc l) (env_of exp) (typ_of exp)) es in
+ annot_pat (P_tup pats) (gen_loc l) (env_of exp) typ
type 'a updated_term =
@@ -3139,6 +3139,8 @@ type 'a updated_term =
let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
+ let env = env_of exp in
+
let rec add_vars overwrite ((E_aux (expaux,annot)) as exp) vars =
match expaux with
| E_let (lb,exp) ->
@@ -3163,7 +3165,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
| _ -> raise (Reporting_basic.err_unreachable l
"add_vars: trying to overwrite a non-unit expression in tail-position")
else
- let typ' = Typ_aux (Typ_tup [typ_of exp;typ_of vars], Parse_ast.Generated l) in
+ let typ' = Typ_aux (Typ_tup [typ_of exp;typ_of vars], gen_loc l) in
E_aux (E_tuple [exp;vars],swaptyp typ' annot) in
let rewrite (E_aux (expaux,((el,_) as annot))) (P_aux (_,(pl,pannot)) as pat) =
@@ -3192,7 +3194,7 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
| true, Ord_aux (Ord_dec,_) -> "foreachM_dec"
| _ -> raise (Reporting_basic.err_unreachable el
"Could not determine foreach combinator") in
- let funcl = Id_aux (Id fname,Parse_ast.Generated el) in
+ let funcl = Id_aux (Id fname,gen_loc el) in
let loopvar =
(* Don't bother with creating a range type annotation, since the
Lem pretty-printing does not use it. *)
@@ -3211,13 +3213,12 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let t = {t = Tapp ("range",match order with
| Ord_aux (Ord_inc,_) -> [bf;tt]
| Ord_aux (Ord_dec,_) -> [tf;bt])} in *)
- E_aux (E_id id, simple_annot l int_typ) in
+ annot_exp (E_id id) l env int_typ in
let v = E_aux (E_app (funcl,[loopvar;mktup el [exp1;exp2;exp3];exp4;vartuple]),
- (Parse_ast.Generated el, annot4)) in
+ (gen_loc el, annot4)) in
let pat =
if overwrite then mktup_pat el vars
- else P_aux (P_tup [pat; mktup_pat pl vars],
- simple_annot pl (typ_of v)) in
+ else annot_pat (P_tup [pat; mktup_pat pl vars]) pl env (typ_of v) in
Added_vars (v,pat)
| E_loop(loop,cond,body) ->
let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t))) (find_updated_vars body) in
@@ -3230,17 +3231,15 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
| false, true -> "while_PM"
| true, false -> "while_MP"
| true, true -> "while_MM" in
- let funcl = Id_aux (Id fname,Parse_ast.Generated el) in
+ let funcl = Id_aux (Id fname,gen_loc el) in
let is_while =
match loop with
- | While -> E_aux (E_lit (mk_lit L_true), simple_annot el bool_typ)
- | Until -> E_aux (E_lit (mk_lit L_false), simple_annot el bool_typ) in
- let v = E_aux (E_app (funcl,[is_while;cond;body;vartuple]),
- (Parse_ast.Generated el, bannot)) in
+ | While -> annot_exp (E_lit (mk_lit L_true)) (gen_loc el) env bool_typ
+ | Until -> annot_exp (E_lit (mk_lit L_false)) (gen_loc el) env bool_typ in
+ let v = E_aux (E_app (funcl,[is_while;cond;body;vartuple]), (gen_loc el, bannot)) in
let pat =
if overwrite then mktup_pat el vars
- else P_aux (P_tup [pat; mktup_pat pl vars],
- simple_annot pl (typ_of v)) in
+ else annot_pat (P_tup [pat; mktup_pat pl vars]) pl env (typ_of v) in
Added_vars (v,pat)
| E_if (c,e1,e2) ->
let vars = List.map (fun (var,(l,t)) -> E_aux (E_id var,(l,t)))
@@ -3255,11 +3254,10 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let env = env_of_annot annot in
let typ = typ_of e1 in
let eff = union_eff_exps [e1;e2] in
- let v = E_aux (E_if (c,e1,e2), (Parse_ast.Generated el, Some (env, typ, eff))) in
+ let v = E_aux (E_if (c,e1,e2), (gen_loc el, Some (env, typ, eff))) in
let pat =
if overwrite then mktup_pat el vars
- else P_aux (P_tup [pat; mktup_pat pl vars],
- (simple_annot pl (typ_of v))) in
+ else annot_pat (P_tup [pat; mktup_pat pl vars]) pl env (typ_of v) in
Added_vars (v,pat)
| E_case (e1,ps) ->
(* after rewrite_defs_letbind_effects e1 needs no rewriting *)
@@ -3277,10 +3275,19 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
Same_vars (E_aux (E_case (e1,ps),annot))
else
let vartuple = mktup el vars in
- let typ =
- let (Pat_aux ((Pat_exp (_,first)|Pat_when (_,_,first)),_)) = List.hd ps in
- typ_of first in
- let (ps,typ,effs) =
+ let rewrite_pexp (Pat_aux (pexp, (l, _))) = match pexp with
+ | Pat_exp (pat, exp) ->
+ let exp = rewrite_var_updates (add_vars overwrite exp vartuple) in
+ let pannot = (l, Some (env_of exp, typ_of exp, effect_of exp)) in
+ Pat_aux (Pat_exp (pat, exp), pannot)
+ | Pat_when _ ->
+ raise (Reporting_basic.err_unreachable l
+ "Guarded patterns should have been rewritten already") in
+ let typ = match ps with
+ | Pat_aux ((Pat_exp (_,first)|Pat_when (_,_,first)),_) :: _ -> typ_of first
+ | _ -> unit_typ in
+ let v = propagate_exp_effect (annot_exp (E_case (e1, List.map rewrite_pexp ps)) pl env typ) in
+ (* let (ps,typ,effs) =
let f (acc,typ,effs) (Pat_aux (Pat_exp (p,e),pannot)) =
let etyp = typ_of e in
let () = assert (string_of_typ etyp = string_of_typ typ) in
@@ -3290,11 +3297,10 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
let pat' = Pat_aux (Pat_exp (p,e),pannot) in
(acc @ [pat'],typ,effs) in
List.fold_left f ([],typ,no_effect) ps in
- let v = E_aux (E_case (e1,ps), (Parse_ast.Generated pl, Some (env_of_annot annot, typ, effs))) in
+ let v = E_aux (E_case (e1,ps), (gen_loc pl, Some (env_of_annot annot, typ, effs))) in *)
let pat =
if overwrite then mktup_pat el vars
- else P_aux (P_tup [pat; mktup_pat pl vars],
- (simple_annot pl (typ_of v))) in
+ else annot_pat (P_tup [pat; mktup_pat pl vars]) pl env (typ_of v) in
Added_vars (v,pat)
| E_assign (lexp,vexp) ->
let effs = match effect_of_annot (snd annot) with
@@ -3307,23 +3313,21 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
else
(match lexp with
| LEXP_aux (LEXP_id id,annot) ->
- let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in
+ let pat = annot_pat (P_id id) pl env (typ_of vexp) in
Added_vars (vexp,pat)
| LEXP_aux (LEXP_cast (_,id),annot) ->
- let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in
+ let pat = annot_pat (P_id id) pl env (typ_of vexp) in
Added_vars (vexp,pat)
| LEXP_aux (LEXP_vector (LEXP_aux (LEXP_id id,((l2,_) as annot2)),i),((l1,_) as annot)) ->
- let eid = E_aux (E_id id, simple_annot l2 (typ_of_annot annot2)) in
- let vexp = E_aux (E_vector_update (eid,i,vexp),
- simple_annot l1 (typ_of_annot annot)) in
- let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in
+ let eid = annot_exp (E_id id) l2 env (typ_of_annot annot2) in
+ let vexp = annot_exp (E_vector_update (eid,i,vexp)) l1 env (typ_of_annot annot) in
+ let pat = annot_pat (P_id id) pl env (typ_of vexp) in
Added_vars (vexp,pat)
| LEXP_aux (LEXP_vector_range (LEXP_aux (LEXP_id id,((l2,_) as annot2)),i,j),
((l,_) as annot)) ->
- let eid = E_aux (E_id id, simple_annot l2 (typ_of_annot annot2)) in
- let vexp = E_aux (E_vector_update_subrange (eid,i,j,vexp),
- simple_annot l (typ_of_annot annot)) in
- let pat = P_aux (P_id id, simple_annot pl (typ_of vexp)) in
+ let eid = annot_exp (E_id id) l2 env (typ_of_annot annot2) in
+ let vexp = annot_exp (E_vector_update_subrange (eid,i,j,vexp)) l env (typ_of_annot annot) in
+ let pat = annot_pat (P_id id) pl env (typ_of vexp) in
Added_vars (vexp,pat)
| _ -> Same_vars (E_aux (E_assign (lexp,vexp),annot)))
| _ ->
@@ -3334,32 +3338,35 @@ let rec rewrite_var_updates ((E_aux (expaux,((l,_) as annot))) as exp) =
match expaux with
| E_let (lb,body) ->
let body = rewrite_var_updates body in
- let (eff,lb) = match lb with
- | LB_aux (LB_val (pat,v),lbannot) ->
- (match rewrite v pat with
- | Added_vars (v,pat) ->
- let (E_aux (_,(l,_))) = v in
- let lbannot = (simple_annot l (typ_of v)) in
- (effect_of v,LB_aux (LB_val (pat,v),lbannot))
- | Same_vars v -> (effect_of v,LB_aux (LB_val (pat,v),lbannot))) in
- let tannot = Some (env_of_annot annot, typ_of body, union_effects eff (effect_of body)) in
- E_aux (E_let (lb,body),(Parse_ast.Generated l,tannot))
+ let (LB_aux (LB_val (pat, v), lbannot)) = lb in
+ let lb = match rewrite v pat with
+ | Added_vars (v, P_aux (pat, _)) ->
+ annot_letbind (pat, v) (get_loc_exp v) env (typ_of v)
+ | Same_vars v -> LB_aux (LB_val (pat, v),lbannot) in
+ propagate_exp_effect (annot_exp (E_let (lb, body)) l env (typ_of body))
| E_internal_let (lexp,v,body) ->
(* Rewrite E_internal_let into E_let and call recursively *)
let id = match lexp with
| LEXP_aux (LEXP_id id,_) -> id
- | LEXP_aux (LEXP_cast (_,id),_) -> id in
- let env = env_of_annot annot in
+ | LEXP_aux (LEXP_cast (_,id),_) -> id
+ | _ ->
+ raise (Reporting_basic.err_unreachable l
+ "E_internal_let with a lexp that is not a variable") in
+ let pat = annot_pat (P_id id) l env (typ_of v) in
+ let lb = annot_letbind (P_id id, v) l env (typ_of v) in
+ let exp = propagate_exp_effect (annot_exp (E_let (lb, body)) l env (typ_of body)) in
+ rewrite_var_updates exp
+ (* let env = env_of_annot annot in
let vtyp = typ_of v in
let veff = effect_of v in
let bodyenv = env_of body in
let bodytyp = typ_of body in
let bodyeff = effect_of body in
let pat = P_aux (P_id id, (simple_annot l vtyp)) in
- let lbannot = (Parse_ast.Generated l, Some (env, vtyp, veff)) in
+ let lbannot = (gen_loc l, Some (env, vtyp, veff)) in
let lb = LB_aux (LB_val (pat,v),lbannot) in
- let exp = E_aux (E_let (lb,body),(Parse_ast.Generated l, Some (bodyenv, bodytyp, union_effects veff bodyeff))) in
- rewrite_var_updates exp
+ let exp = E_aux (E_let (lb,body),(gen_loc l, Some (bodyenv, bodytyp, union_effects veff bodyeff))) in
+ rewrite_var_updates exp *)
| E_internal_plet (pat,v,body) ->
failwith "rewrite_var_updates: E_internal_plet shouldn't be introduced yet"
(* There are no expressions that have effects or variable updates in
@@ -3509,7 +3516,8 @@ let rewrite_defs_lem = [
let rewrite_defs_ocaml = [
(* ("top_sort_defs", top_sort_defs); *)
- ("undefined", rewrite_undefined);
+ (* ("undefined", rewrite_undefined); *)
+ ("tuple_vector_assignments", rewrite_tuple_vector_assignments);
("tuple_assignments", rewrite_tuple_assignments);
("simple_assignments", rewrite_simple_assignments);
("remove_vector_concat", rewrite_defs_remove_vector_concat);
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 1c3e8fae..73337de4 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -56,9 +56,12 @@ type 'a rewriters = { rewrite_exp : 'a rewriters -> 'a exp -> 'a exp;
val rewrite_exp : tannot rewriters -> tannot exp -> tannot exp
val rewrite_defs : tannot defs -> tannot defs
+val rewrite_undefined : tannot defs -> tannot defs
val rewrite_defs_ocaml : (string * (tannot defs -> tannot defs)) list (*Perform rewrites to exclude AST nodes not supported for ocaml out*)
val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list (*Perform rewrites to exclude AST nodes not supported for lem out*)
+val simple_typ : typ -> typ
+
(* the type of interpretations of pattern-matching expressions *)
type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
{ p_lit : lit -> 'pat_aux
diff --git a/src/sail.ml b/src/sail.ml
index ca121a79..9c447f36 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -170,7 +170,11 @@ let main() =
| locs -> monomorphise_ast locs ast
in
- let ast = rewrite_ast ast in
+ let ast =
+ if !Initial_check.opt_undefined_gen then
+ rewrite_undefined (rewrite_ast ast)
+ else rewrite_ast ast in
+
let out_name = match !opt_file_out with
| None -> fst (List.hd parsed)
| Some f -> f ^ ".sail" in
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 2e368c53..c896f07a 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -534,6 +534,7 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function
| DEF_fundef fdef -> fv_of_fun consider_var fdef
| DEF_val lebind -> ((fun (b,u,_) -> (b,u)) (fv_of_let consider_var mt mt mt lebind))
| DEF_spec vspec -> fv_of_vspec consider_var vspec
+ | DEF_fixity _ -> mt,mt
| DEF_overload (id,ids) -> init_env (string_of_id id), List.fold_left (fun ns id -> Nameset.add (string_of_id id) ns) mt ids
| DEF_default def -> mt,mt
| DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef
diff --git a/src/type_check.ml b/src/type_check.ml
index 3b13abb8..58de77e1 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2027,16 +2027,15 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
| E_throw exp, _ ->
let checked_exp = crule check_exp env exp exc_typ in
annot_exp_effect (E_throw checked_exp) typ (mk_effect [BE_escape])
+ | E_internal_let (lexp, bind, exp), _ ->
+ let E_aux (E_assign (lexp, bind), _), env = bind_assignment env lexp bind in
+ let checked_exp = crule check_exp env exp typ in
+ annot_exp (E_internal_let (lexp, bind, checked_exp)) typ
| E_vector vec, _ ->
- begin
- let (start, len, ord, vtyp) = destruct_vec_typ l env typ in
- let checked_items = List.map (fun i -> crule check_exp env i vtyp) vec in
- match nexp_simp len with
- | Nexp_aux (Nexp_constant lenc, _) ->
- if List.length vec = lenc then annot_exp (E_vector checked_items) typ
- else typ_error l "List length didn't match" (* FIXME: improve error message *)
- | _ -> typ_error l "Cannot check list constant against non-constant length vector type"
- end
+ let (start, len, ord, vtyp) = destruct_vec_typ l env typ in
+ let checked_items = List.map (fun i -> crule check_exp env i vtyp) vec in
+ if prove env (nc_eq (nconstant (List.length vec)) (nexp_simp len)) then annot_exp (E_vector checked_items) typ
+ else typ_error l "List length didn't match" (* FIXME: improve error message *)
| E_lit (L_aux (L_undef, _) as lit), _ ->
annot_exp_effect (E_lit lit) typ (mk_effect [BE_undef])
(* This rule allows registers of type t to be passed by name with type register<t>*)
@@ -2981,6 +2980,11 @@ and propagate_exp_effect_aux = function
let p_lexp = propagate_lexp_effect lexp in
let p_exp = propagate_exp_effect exp in
E_assign (p_lexp, p_exp), union_effects (effect_of p_exp) (effect_of_lexp p_lexp)
+ | E_internal_let (lexp, bind, exp) ->
+ let p_lexp = propagate_lexp_effect lexp in
+ let p_bind = propagate_exp_effect bind in
+ let p_exp = propagate_exp_effect exp in
+ E_internal_let (p_lexp, p_bind, p_exp), union_effects (effect_of_lexp p_lexp) (collect_effects [p_bind; p_exp])
| E_sizeof nexp -> E_sizeof nexp, no_effect
| E_constraint nc -> E_constraint nc, no_effect
| E_exit exp ->
@@ -2999,6 +3003,21 @@ and propagate_exp_effect_aux = function
| E_field (exp, id) ->
let p_exp = propagate_exp_effect exp in
E_field (p_exp, id), effect_of p_exp
+ | E_internal_let (lexp, exp, body) ->
+ let p_lexp = propagate_lexp_effect lexp in
+ let p_exp = propagate_exp_effect exp in
+ let p_body = propagate_exp_effect body in
+ E_internal_let (p_lexp, p_exp, p_body),
+ union_effects (effect_of_lexp p_lexp) (collect_effects [p_exp; p_body])
+ | E_internal_plet (pat, exp, body) ->
+ let p_pat = propagate_pat_effect pat in
+ let p_exp = propagate_exp_effect exp in
+ let p_body = propagate_exp_effect body in
+ E_internal_plet (p_pat, p_exp, p_body),
+ union_effects (effect_of_pat p_pat) (collect_effects [p_exp; p_body])
+ | E_internal_return exp ->
+ let p_exp = propagate_exp_effect exp in
+ E_internal_return p_exp, effect_of p_exp
| exp_aux -> typ_error Parse_ast.Unknown ("Unimplemented: Cannot propagate effect in expression "
^ string_of_exp (E_aux (exp_aux, (Parse_ast.Unknown, None))))
diff --git a/src/type_check.mli b/src/type_check.mli
index b6b5e75e..ff9eb74e 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -241,6 +241,7 @@ val unify : l -> Env.t -> typ -> typ -> uvar KBindings.t * kid list * n_constrai
val instantiation_of : tannot exp -> uvar KBindings.t
val propagate_exp_effect : tannot exp -> tannot exp
+val propagate_pexp_effect : tannot pexp -> tannot pexp * effect
(* Fully type-check an AST
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 16:14:22 +0000