summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKathy Gray2016-03-02 17:04:09 +0000
committerKathy Gray2016-03-02 17:04:31 +0000
commit9d6875ba4147e3f52b3251bab77e52df03257aa3 (patch)
tree9eb0e06cb82527ea7e20a686a307efa973d2be77
parente120d223a007587b1e741b69e0e46bfb4c2ea6c8 (diff)
Add new language feature to permit definitions of items of kind Nat, etc as well as items of kind Type.
Syntax for the feature is: def Nat id = nexp Note: some useful nexps may not parse properly. All typedef forms can also be used as def Type ... if desired, but this is not required.
Diffstat
-rw-r--r--language/l2.lem139
-rw-r--r--language/l2.ml151
-rw-r--r--language/l2.ott24
-rw-r--r--language/l2_parse.ml165
-rw-r--r--language/l2_parse.ott18
-rw-r--r--language/manual.pdfbin342551 -> 342588 bytes
-rw-r--r--language/manual.tex2
-rw-r--r--src/initial_check.ml106
-rw-r--r--src/initial_check_full_ast.ml89
-rw-r--r--src/parser.mly42
-rw-r--r--src/pre_lexer.mll1
-rw-r--r--src/pre_parser.mly6
-rw-r--r--src/pretty_print.ml174
-rw-r--r--src/process_file.ml3
-rw-r--r--src/rewriter.ml260
-rw-r--r--src/type_check.ml351
-rw-r--r--src/type_internal.ml98
-rw-r--r--src/type_internal.mli5
18 files changed, 1078 insertions, 556 deletions
diff --git a/language/l2.lem b/language/l2.lem
index 8f6144cb..a845f1f6 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -30,6 +30,11 @@ type base_kind_aux = (* base kind *)
| BK_effect (* kind of effect sets *)
+type id_aux = (* Identifier *)
+ | Id of x
+ | DeIid of x (* remove infix status *)
+
+
type kid_aux = (* variables with kind, ticked to differntiate from program variables *)
| Var of x
@@ -38,6 +43,10 @@ type base_kind =
| BK_aux of base_kind_aux * l
+type id =
+ | Id_aux of id_aux * l
+
+
type kid =
| Kid_aux of kid_aux * l
@@ -47,11 +56,12 @@ type kind_aux = (* kinds *)
type nexp_aux = (* expression of kind Nat, for vector sizes and origins *)
+ | Nexp_id of id (* identifier, bound by def Nat x = nexp *)
| Nexp_var of kid (* variable *)
| Nexp_constant of integer (* constant *)
| Nexp_times of nexp * nexp (* product *)
| Nexp_sum of nexp * nexp (* sum *)
- | Nexp_minus of nexp * nexp (* subtraction, error for nexp1 to be smaller than nexp2 *)
+ | Nexp_minus of nexp * nexp (* subtraction *)
| Nexp_exp of nexp (* exponential *)
| Nexp_neg of nexp (* For internal use *)
@@ -83,32 +93,23 @@ type base_effect =
| BE_aux of base_effect_aux * l
-type effect_aux = (* effect set, of kind Effects *)
- | Effect_var of kid
- | Effect_set of list base_effect (* effect set *)
-
-
type order_aux = (* vector order specifications, of kind Order *)
| Ord_var of kid (* variable *)
| Ord_inc (* increasing (little-endian) *)
| Ord_dec (* decreasing (big-endian) *)
-type id_aux = (* Identifier *)
- | Id of x
- | DeIid of x (* remove infix status *)
-
-
-type effect =
- | Effect_aux of effect_aux * l
+type effect_aux = (* effect set, of kind Effects *)
+ | Effect_var of kid
+ | Effect_set of list base_effect (* effect set *)
type order =
| Ord_aux of order_aux * l
-type id =
- | Id_aux of id_aux * l
+type effect =
+ | Effect_aux of effect_aux * l
let effect_union e1 e2 =
match (e1,e2) with
@@ -163,10 +164,6 @@ type lit_aux = (* Literal constant *)
| L_string of string (* string constant *)
-type typquant =
- | TypQ_aux of typquant_aux * l
-
-
type typ_aux = (* Type expressions, of kind $Type$ *)
| Typ_wild (* Unspecified type *)
| Typ_id of id (* Defined type *)
@@ -188,6 +185,10 @@ and typ_arg =
| Typ_arg_aux of typ_arg_aux * l
+type typquant =
+ | TypQ_aux of typquant_aux * l
+
+
type lit =
| L_aux of lit_aux * l
@@ -228,42 +229,7 @@ type reg_id_aux 'a =
| RI_id of id
-type lexp 'a =
- | LEXP_aux of (lexp_aux 'a) * annot 'a
-
-and fexp_aux 'a = (* Field-expression *)
- | FE_Fexp of id * (exp 'a)
-
-and fexp 'a =
- | FE_aux of (fexp_aux 'a) * annot 'a
-
-and fexps_aux 'a = (* Field-expression list *)
- | FES_Fexps of list (fexp 'a) * bool
-
-and fexps 'a =
- | FES_aux of (fexps_aux 'a) * annot 'a
-
-and opt_default_aux 'a = (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *)
- | Def_val_empty
- | Def_val_dec of (exp 'a)
-
-and opt_default 'a =
- | Def_val_aux of (opt_default_aux 'a) * annot 'a
-
-and pexp_aux 'a = (* Pattern match *)
- | Pat_exp of (pat 'a) * (exp 'a)
-
-and pexp 'a =
- | Pat_aux of (pexp_aux 'a) * annot 'a
-
-and letbind_aux 'a = (* Let binding *)
- | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *)
- | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *)
-
-and letbind 'a =
- | LB_aux of (letbind_aux 'a) * annot 'a
-
-and exp_aux 'a = (* Expression *)
+type exp_aux 'a = (* Expression *)
| E_block of list (exp 'a) (* block *)
| E_nondet of list (exp 'a) (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *)
| E_id of id (* identifier *)
@@ -311,6 +277,41 @@ and lexp_aux 'a = (* lvalue expression *)
| LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *)
| LEXP_field of (lexp 'a) * id (* struct field *)
+and lexp 'a =
+ | LEXP_aux of (lexp_aux 'a) * annot 'a
+
+and fexp_aux 'a = (* Field-expression *)
+ | FE_Fexp of id * (exp 'a)
+
+and fexp 'a =
+ | FE_aux of (fexp_aux 'a) * annot 'a
+
+and fexps_aux 'a = (* Field-expression list *)
+ | FES_Fexps of list (fexp 'a) * bool
+
+and fexps 'a =
+ | FES_aux of (fexps_aux 'a) * annot 'a
+
+and opt_default_aux 'a = (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *)
+ | Def_val_empty
+ | Def_val_dec of (exp 'a)
+
+and opt_default 'a =
+ | Def_val_aux of (opt_default_aux 'a) * annot 'a
+
+and pexp_aux 'a = (* Pattern match *)
+ | Pat_exp of (pat 'a) * (exp 'a)
+
+and pexp 'a =
+ | Pat_aux of (pexp_aux 'a) * annot 'a
+
+and letbind_aux 'a = (* Let binding *)
+ | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *)
+ | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *)
+
+and letbind 'a =
+ | LB_aux of (letbind_aux 'a) * annot 'a
+
type reg_id 'a =
| RI_aux of (reg_id_aux 'a) * annot 'a
@@ -421,6 +422,15 @@ type default_spec_aux 'a = (* Default kinding or typing assumption *)
| DT_typ of typschm * id
+type kind_def_aux 'a = (* Definition body for elements of kind; many are shorthands for type\_defs *)
+ | KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *)
+ | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *)
+ | KD_record of kind * id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
+ | KD_variant of kind * id * name_scm_opt * typquant * list type_union * bool (* union type definition *)
+ | KD_enum of kind * id * name_scm_opt * list id * bool (* enumeration type definition *)
+ | KD_register of kind * id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
+
+
type val_spec_aux 'a = (* Value type specification *)
| VS_val_spec of typschm * id
| VS_extern_no_rename of typschm * id
@@ -447,6 +457,10 @@ type default_spec 'a =
| DT_aux of (default_spec_aux 'a) * l
+type kind_def 'a =
+ | KD_aux of (kind_def_aux 'a) * annot 'a
+
+
type val_spec 'a =
| VS_aux of (val_spec_aux 'a) * annot 'a
@@ -456,6 +470,7 @@ type dec_comm 'a = (* Top-level generated comments *)
| DC_comm_struct of (def 'a) (* generated structured comment *)
and def 'a = (* Top-level definition *)
+ | DEF_kind of (kind_def 'a) (* definition of named kind identifiers *)
| DEF_type of (type_def 'a) (* type definition *)
| DEF_fundef of (fundef 'a) (* function definition *)
| DEF_val of (letbind 'a) (* value definition *)
@@ -521,16 +536,16 @@ type nec = (* Numeric expression constraints *)
| Nec_branch of list nec
-type kinf = (* Whether a kind is default or from a local binding *)
- | Kinf_k of k
- | Kinf_def of k
-
-
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 t = (* Internal types *)
| T_id of x
| T_var of x
@@ -622,10 +637,10 @@ let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should
-type E = env
+type I = inf
-type I = inf
+type E = env
diff --git a/language/l2.ml b/language/l2.ml
index b8e31514..fbc52b10 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -25,6 +25,12 @@ base_kind =
type
+id_aux = (* Identifier *)
+ Id of x
+ | DeIid of x (* remove infix status *)
+
+
+type
kid_aux = (* variables with kind, ticked to differntiate from program variables *)
Var of x
@@ -35,6 +41,11 @@ kind_aux = (* kinds *)
type
+id =
+ Id_aux of id_aux * l
+
+
+type
kid =
Kid_aux of kid_aux * l
@@ -46,11 +57,12 @@ kind =
type
nexp_aux = (* expression of kind Nat, for vector sizes and origins *)
- Nexp_var of kid (* variable *)
+ Nexp_id of id (* identifier, bound by def Nat x = nexp *)
+ | 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, error for nexp1 to be smaller than nexp2 *)
+ | Nexp_minus of nexp * nexp (* subtraction *)
| Nexp_exp of nexp (* exponential *)
| Nexp_neg of nexp (* For internal use *)
@@ -88,12 +100,6 @@ order_aux = (* vector order specifications, of kind Order *)
type
-id_aux = (* Identifier *)
- Id of x
- | DeIid of x (* remove infix status *)
-
-
-type
effect_aux = (* effect set, of kind Effects *)
Effect_var of kid
| Effect_set of (base_effect) list (* effect set *)
@@ -105,11 +111,6 @@ order =
type
-id =
- Id_aux of id_aux * l
-
-
-type
effect =
Effect_aux of effect_aux * l
@@ -175,10 +176,7 @@ typquant =
type
-typ_arg =
- Typ_arg_aux of typ_arg_aux * l
-
-and typ_aux = (* Type expressions, of kind $_$ *)
+typ_aux = (* Type expressions, of kind $_$ *)
Typ_wild (* Unspecified type *)
| Typ_id of id (* Defined type *)
| Typ_var of kid (* Type variable *)
@@ -195,6 +193,9 @@ and typ_arg_aux = (* Type constructor arguments of all kinds *)
| Typ_arg_order of order
| Typ_arg_effect of effect
+and typ_arg =
+ Typ_arg_aux of typ_arg_aux * l
+
type
lit =
@@ -338,13 +339,9 @@ type_union_aux = (* Type union constructors *)
type
-tannot_opt_aux = (* Optional type annotation for functions *)
- Typ_annot_opt_some of typquant * typ
-
-
-type
-'a funcl_aux = (* Function clause *)
- FCL_Funcl of id * 'a pat * 'a exp
+name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *)
+ Name_sect_none
+ | Name_sect_some of string
type
@@ -354,9 +351,8 @@ effect_opt_aux = (* Optional effect annotation for functions *)
type
-name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *)
- Name_sect_none
- | Name_sect_some of string
+'a funcl_aux = (* Function clause *)
+ FCL_Funcl of id * 'a pat * 'a exp
type
@@ -366,6 +362,11 @@ rec_opt_aux = (* Optional recursive annotation for functions *)
type
+tannot_opt_aux = (* Optional type annotation for functions *)
+ Typ_annot_opt_some of typquant * typ
+
+
+type
'a alias_spec_aux = (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
AL_subreg of 'a reg_id * id
| AL_bit of 'a reg_id * 'a exp
@@ -379,13 +380,18 @@ type_union =
type
-tannot_opt =
- Typ_annot_opt_aux of tannot_opt_aux * l
+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 * l
type
-'a funcl =
- FCL_aux of 'a funcl_aux * 'a annot
+name_scm_opt =
+ Name_sect_aux of name_scm_opt_aux * l
type
@@ -394,8 +400,8 @@ effect_opt =
type
-name_scm_opt =
- Name_sect_aux of name_scm_opt_aux * l
+'a funcl =
+ FCL_aux of 'a funcl_aux * 'a annot
type
@@ -404,13 +410,8 @@ rec_opt =
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 * l
+tannot_opt =
+ Typ_annot_opt_aux of tannot_opt_aux * l
type
@@ -419,13 +420,10 @@ type
type
-'a scattered_def_aux = (* Function and type union definitions that can be spread across
- a file. Each one must end in $_$ *)
- SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
- | SD_scattered_funcl of 'a funcl (* scattered function definition clause *)
- | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
- | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
- | SD_scattered_end of id (* scattered definition end *)
+'a default_spec_aux = (* Default kinding or typing assumption *)
+ DT_kind of base_kind * kid
+ | DT_order of order
+ | DT_typ of typschm * id
type
@@ -438,10 +436,30 @@ type
type
-'a default_spec_aux = (* Default kinding or typing assumption *)
- DT_kind of base_kind * kid
- | DT_order of order
- | DT_typ of typschm * id
+'a val_spec_aux = (* Value type specification *)
+ VS_val_spec of typschm * id
+ | VS_extern_no_rename of typschm * id
+ | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
+
+
+type
+'a kind_def_aux = (* Definition body for elements of kind; many are shorthands for type\_defs *)
+ KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *)
+ | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *)
+ | KD_record of kind * id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
+ | KD_variant of kind * id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
+ | KD_enum of kind * id * name_scm_opt * (id) list * bool (* enumeration type definition *)
+ | KD_register of kind * id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
+
+
+type
+'a scattered_def_aux = (* Function and type union definitions that can be spread across
+ a file. Each one must end in $_$ *)
+ SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
+ | SD_scattered_funcl of 'a funcl (* scattered function definition clause *)
+ | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
+ | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
+ | SD_scattered_end of id (* scattered definition end *)
type
@@ -457,25 +475,28 @@ type
type
-'a val_spec_aux = (* Value type specification *)
- VS_val_spec of typschm * id
- | VS_extern_no_rename of typschm * id
- | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
+'a default_spec =
+ DT_aux of 'a default_spec_aux * l
type
-'a scattered_def =
- SD_aux of 'a scattered_def_aux * 'a annot
+'a type_def =
+ TD_aux of 'a type_def_aux * 'a annot
type
-'a type_def =
- TD_aux of 'a type_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 * l
+'a kind_def =
+ KD_aux of 'a kind_def_aux * 'a annot
+
+
+type
+'a scattered_def =
+ SD_aux of 'a scattered_def_aux * 'a annot
type
@@ -489,17 +510,13 @@ type
type
-'a val_spec =
- VS_aux of 'a val_spec_aux * 'a annot
-
-
-type
'a dec_comm = (* Top-level generated comments *)
DC_comm of string (* generated unstructured comment *)
| DC_comm_struct of 'a def (* generated structured comment *)
and 'a def = (* Top-level definition *)
- DEF_type of 'a type_def (* type definition *)
+ DEF_kind of 'a kind_def (* definition of named kind identifiers *)
+ | DEF_type of 'a type_def (* type 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 *)
diff --git a/language/l2.ott b/language/l2.ott
index c6e1e470..f750832a 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -163,11 +163,12 @@ kind :: 'K_' ::=
nexp :: 'Nexp_' ::=
{{ com expression of kind Nat, for vector sizes and origins }}
{{ aux _ l }}
+ | id :: :: id {{ com identifier, bound by def Nat x = nexp }}
| kid :: :: var {{ com variable }}
| num :: :: constant {{ com constant }}
| nexp1 * nexp2 :: :: times {{ com product }}
| nexp1 + nexp2 :: :: sum {{ com sum }}
- | nexp1 - nexp2 :: :: minus {{ com subtraction, error for nexp1 to be smaller than nexp2 }}
+ | nexp1 - nexp2 :: :: minus {{ com subtraction }}
| 2** nexp :: :: exp {{ com exponential }}
| neg nexp :: :: neg {{ com For internal use }}
| ( nexp ) :: S :: paren {{ ichlo [[nexp]] }}
@@ -394,6 +395,25 @@ type_def :: 'TD_' ::=
| typedef id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn }
:: :: register {{ com register mutable bitfield type definition }} {{ texlong }}
+kind_def :: 'KD_' ::=
+ {{ com Definition body for elements of kind; many are shorthands for type\_defs }}
+ {{ aux _ annot }} {{ auxparam 'a }}
+ | Def kind id name_scm_opt = nexp :: :: nabbrev
+ {{ com nexp abbreviation }}
+ | Def kind id name_scm_opt = typschm :: :: abbrev
+ {{ com type abbreviation }} {{ texlong }}
+ | Def kind id name_scm_opt = const struct typquant { typ1 id1 ; ... ; typn idn semi_opt } :: :: record
+ {{ com struct type definition }} {{ texlong }}
+ | Def kind id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: :: variant
+ {{ com union type definition}} {{ texlong }}
+ | Def kind id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum
+ {{ com enumeration type definition}} {{ texlong }}
+
+ | Def kind id = register bits [ nexp : nexp' ] { index_range1 : id1 ; ... ; index_rangen : idn }
+:: :: register {{ com register mutable bitfield type definition }} {{ texlong }}
+
+
+
% also sugar [ nexp ]
type_union :: 'Tu_' ::=
@@ -876,6 +896,8 @@ dec_comm :: 'DC_' ::= {{ com Top-level generated comments }} {{auxparam 'a}}
def :: 'DEF_' ::=
{{ com Top-level definition }}
{{ auxparam 'a }}
+ | kind_def :: :: kind
+ {{ com definition of named kind identifiers }}
| type_def :: :: type
{{ com type definition }}
| fundef :: :: fundef
diff --git a/language/l2_parse.ml b/language/l2_parse.ml
index 1152cff9..d4d71cfe 100644
--- a/language/l2_parse.ml
+++ b/language/l2_parse.ml
@@ -31,17 +31,6 @@ base_kind =
type
-id_aux = (* Identifier *)
- Id of x
- | DeIid of x (* remove infix status *)
-
-
-type
-kid_aux = (* identifiers with kind, ticked to differntiate from program variables *)
- Var of x
-
-
-type
base_effect_aux = (* effect *)
BE_rreg (* read register *)
| BE_wreg (* write register *)
@@ -58,13 +47,24 @@ base_effect_aux = (* effect *)
type
+kid_aux = (* identifiers with kind, ticked to differntiate from program variables *)
+ Var of x
+
+
+type
+id_aux = (* Identifier *)
+ Id of x
+ | DeIid of x (* remove infix status *)
+
+
+type
kind_aux = (* kinds *)
K_kind of (base_kind) list
type
-id =
- Id_aux of id_aux * l
+base_effect =
+ BE_aux of base_effect_aux * l
type
@@ -73,8 +73,8 @@ kid =
type
-base_effect =
- BE_aux of base_effect_aux * l
+id =
+ Id_aux of id_aux * l
type
@@ -146,6 +146,11 @@ typquant_aux = (* type quantifiers and constraints *)
type
+typquant =
+ TypQ_aux of typquant_aux * l
+
+
+type
lit_aux = (* Literal constant *)
L_unit (* $() : _$ *)
| L_zero (* $_ : _$ *)
@@ -160,8 +165,8 @@ lit_aux = (* Literal constant *)
type
-typquant =
- TypQ_aux of typquant_aux * l
+typschm_aux = (* type scheme *)
+ TypSchm_ts of typquant * atyp
type
@@ -170,8 +175,8 @@ lit =
type
-typschm_aux = (* type scheme *)
- TypSchm_ts of typquant * atyp
+typschm =
+ TypSchm_aux of typschm_aux * l
type
@@ -200,11 +205,6 @@ and fpat =
type
-typschm =
- TypSchm_aux of typschm_aux * l
-
-
-type
exp_aux = (* Expression *)
E_block of (exp) list (* block (parsing conflict with structs?) *)
| E_nondet of (exp) list (* block that can evaluate the contained expressions in any ordering *)
@@ -271,15 +271,15 @@ and letbind =
type
-name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *)
- Name_sect_none
- | Name_sect_some of string
+tannot_opt_aux = (* Optional type annotation for functions *)
+ Typ_annot_opt_none
+ | Typ_annot_opt_some of typquant * atyp
type
-type_union_aux = (* Type union constructors *)
- Tu_id of id
- | Tu_ty_id of atyp * id
+effect_opt_aux = (* Optional effect annotation for functions *)
+ Effect_opt_pure (* sugar for empty effect set *)
+ | Effect_opt_effect of atyp
type
@@ -294,30 +294,35 @@ funcl_aux = (* Function clause *)
type
-tannot_opt_aux = (* Optional type annotation for functions *)
- Typ_annot_opt_none
- | Typ_annot_opt_some of typquant * atyp
+type_union_aux = (* Type union constructors *)
+ Tu_id of id
+ | Tu_ty_id of atyp * id
type
-effect_opt_aux = (* Optional effect annotation for functions *)
- Effect_opt_pure (* sugar for empty effect set *)
- | Effect_opt_effect of atyp
+name_scm_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *)
+ Name_sect_none
+ | Name_sect_some of string
type
-name_scm_opt =
- Name_sect_aux of name_scm_opt_aux * l
+tannot_opt =
+ Typ_annot_opt_aux of tannot_opt_aux * 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 *)
+effect_opt =
+ Effect_opt_aux of effect_opt_aux * l
-and index_range =
- BF_aux of index_range_aux * l
+
+type
+rec_opt =
+ Rec_aux of rec_opt_aux * l
+
+
+type
+funcl =
+ FCL_aux of funcl_aux * l
type
@@ -326,23 +331,30 @@ type_union =
type
-rec_opt =
- Rec_aux of rec_opt_aux * l
+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 * l
type
-funcl =
- FCL_aux of funcl_aux * l
+name_scm_opt =
+ Name_sect_aux of name_scm_opt_aux * l
type
-tannot_opt =
- Typ_annot_opt_aux of tannot_opt_aux * l
+default_typing_spec_aux = (* Default kinding or typing assumption, and default order for literal vectors and vector shorthands *)
+ DT_kind of base_kind * kid
+ | DT_order of base_kind * atyp
+ | DT_typ of typschm * id
type
-effect_opt =
- Effect_opt_aux of effect_opt_aux * l
+fundef_aux = (* Function definition *)
+ FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list
type
@@ -355,8 +367,19 @@ type_def_aux = (* Type definition body *)
type
-fundef_aux = (* Function definition *)
- FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list
+val_spec_aux = (* Value type specification *)
+ VS_val_spec of typschm * id
+ | VS_extern_no_rename of typschm * id
+ | VS_extern_spec of typschm * id * string
+
+
+type
+kind_def_aux = (* Definition body for elements of kind; many are shorthands for type\_defs *)
+ KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *)
+ | KD_record of kind * id * name_scm_opt * typquant * ((atyp * 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 * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *)
type
@@ -377,17 +400,13 @@ scattered_def_aux = (* Function and type union definitions that can be spread a
type
-val_spec_aux = (* Value type specification *)
- VS_val_spec of typschm * id
- | VS_extern_no_rename of typschm * id
- | VS_extern_spec of typschm * id * string
+default_typing_spec =
+ DT_aux of default_typing_spec_aux * l
type
-default_typing_spec_aux = (* Default kinding or typing assumption, and default order for literal vectors and vector shorthands *)
- DT_kind of base_kind * kid
- | DT_order of base_kind * atyp
- | DT_typ of typschm * id
+fundef =
+ FD_aux of fundef_aux * l
type
@@ -396,8 +415,13 @@ type_def =
type
-fundef =
- FD_aux of fundef_aux * l
+val_spec =
+ VS_aux of val_spec_aux * l
+
+
+type
+kind_def =
+ KD_aux of kind_def_aux * l
type
@@ -411,18 +435,9 @@ scattered_def =
type
-val_spec =
- VS_aux of val_spec_aux * l
-
-
-type
-default_typing_spec =
- DT_aux of default_typing_spec_aux * l
-
-
-type
def = (* Top-level definition *)
- DEF_type of type_def (* type definition *)
+ DEF_kind of kind_def (* definition of named kind identifiers *)
+ | DEF_type of type_def (* type definition *)
| DEF_fundef of fundef (* function definition *)
| DEF_val of letbind (* value definition *)
| DEF_spec of val_spec (* top-level type constraint *)
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index 00345c27..224fea06 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -305,6 +305,22 @@ type_def :: 'TD_' ::=
| typedef id = register bits [ atyp : atyp' ] { index_range1 : id1 ; ... ; index_rangen : idn }
:: :: register {{ com register mutable bitfield type definition }} {{ texlong }}
+kind_def :: 'KD_' ::=
+ {{ com Definition body for elements of kind; many are shorthands for type\_defs }}
+ {{ aux _ l }}
+ | Def kind id name_scm_opt = typschm :: :: abbrev
+ {{ com type abbreviation }} {{ texlong }}
+ | Def kind id name_scm_opt = const struct typquant { atyp1 id1 ; ... ; atypn idn semi_opt } :: :: record
+ {{ com struct type definition }} {{ texlong }}
+ | Def kind id name_scm_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: :: variant
+ {{ com union type definition}} {{ texlong }}
+ | Def kind id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum
+ {{ com enumeration type definition}} {{ texlong }}
+
+ | Def kind id = register bits [ atyp : atyp' ] { index_range1 : id1 ; ... ; index_rangen : idn }
+:: :: register {{ com register mutable bitfield type definition }} {{ texlong }}
+
+
% also sugar [ nexp ]
@@ -744,6 +760,8 @@ dec_spec :: 'DEC_' ::=
def :: 'DEF_' ::=
{{ com Top-level definition }}
+ | kind_def :: :: kind
+ {{ com definition of named kind identifiers }}
| type_def :: :: type
{{ com type definition }}
| fundef :: :: fundef
diff --git a/language/manual.pdf b/language/manual.pdf
index e5a8e457..6dfb546e 100644
--- a/language/manual.pdf
+++ b/language/manual.pdf
Binary files differ
diff --git a/language/manual.tex b/language/manual.tex
index 2052ea0e..69fd8e8b 100644
--- a/language/manual.tex
+++ b/language/manual.tex
@@ -89,7 +89,7 @@ any type. However, the Sail executable interpreter expects that it is
simulating a uni-processor machine where all registers are bit
vectors.
-A vector of length one, such as \emph{a} can read the element of a \emph{a}
+A vector of length one, such as \emph{a} can read the element of \emph{a}
either with {\tt a} or {\tt a[0]}.
\item Have functions named decode and execute to evaluate
diff --git a/src/initial_check.ml b/src/initial_check.ml
index df46b0cc..efa6b8e8 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -155,16 +155,28 @@ and to_ast_nexp (k_env : kind Envmap.t) (n: Parse_ast.atyp) : Ast.nexp =
match n with
| Parse_ast.ATyp_aux(t,l) ->
(match t with
- | Parse_ast.ATyp_var(v) ->
- let v = to_ast_var v in
- let mk = Envmap.apply k_env (var_to_string v) in
- (*let _ = Envmap.iter (fun v' k -> Printf.eprintf "%s -> %s, %s =? %b\n" v' (kind_to_string k) (var_to_string v) ((var_to_string v) = v') ) k_env in *)
- (match mk with
- | Some(k) -> Nexp_aux((match k.k with
- | K_Nat -> Nexp_var v
- | K_infer -> k.k <- K_Nat; Nexp_var v
- | _ -> typ_error l "Required a variable with kind Nat, encountered " None (Some v) (Some k)),l)
- | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
+ | Parse_ast.ATyp_id(i) ->
+ let i = to_ast_id i in
+ let v = id_to_string i in
+ let mk = Envmap.apply k_env v in
+ (match mk with
+ | Some(k) -> Nexp_aux((match k.k with
+ | K_Nat -> Nexp_id i
+ | K_infer -> k.k <- K_Nat; Nexp_id i
+ | _ -> typ_error l "Required an identifier with kind Nat, encountered " (Some i) None (Some k)),l)
+ | None -> typ_error l "Encountered an unbound variable" (Some i) None None)
+ | Parse_ast.ATyp_var(v) ->
+ let v = to_ast_var v in
+ let mk = Envmap.apply k_env (var_to_string v) in
+ (*let _ =
+ Envmap.iter (fun v' k -> Printf.eprintf "%s -> %s, %s =? %b\n"
+ v' (kind_to_string k) (var_to_string v) ((var_to_string v) = v') ) k_env in *)
+ (match mk with
+ | Some(k) -> Nexp_aux((match k.k with
+ | K_Nat -> Nexp_var v
+ | K_infer -> k.k <- K_Nat; Nexp_var v
+ | _ -> typ_error l "Required a variable with kind Nat, encountered " None (Some v) (Some k)),l)
+ | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
| Parse_ast.ATyp_constant(i) -> Nexp_aux(Nexp_constant(i),l)
| Parse_ast.ATyp_sum(t1,t2) ->
let n1 = to_ast_nexp k_env t1 in
@@ -624,6 +636,77 @@ let to_ast_typedef (names,k_env,def_ord) (td:Parse_ast.type_def) : (tannot type_
let ranges = List.map (fun (range,id) -> (to_ast_range range),to_ast_id id) ranges in
TD_aux(TD_register(id,n1,n2,ranges),(l,NoTyp)), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord))
+let to_ast_kdef (names,k_env,def_ord) (td:Parse_ast.kind_def) : (tannot kind_def) envs_out =
+ match td with
+ | Parse_ast.KD_aux(td,l) ->
+ (match td with
+ | Parse_ast.KD_abbrev(kind,id,name_scm_opt,typschm) ->
+ let id = to_ast_id id in
+ let key = id_to_string id in
+ let (kind,k) = to_ast_kind k_env kind in
+ (match k.k with
+ | K_Typ | K_Lam _ ->
+ let typschm,k_env,_ = to_ast_typschm k_env def_ord typschm in
+ let kd_abrv = KD_aux(KD_abbrev(kind,id,to_ast_namescm name_scm_opt,typschm),(l,NoTyp)) in
+ let typ = (match typschm with
+ | TypSchm_aux(TypSchm_ts(tq,typ), _) ->
+ begin match (typquant_to_quantkinds k_env tq) with
+ | [] -> {k = K_Typ}
+ | typs -> {k= K_Lam(typs,{k=K_Typ})}
+ end) in
+ kd_abrv,(names,Envmap.insert k_env (key,typ),def_ord)
+ | K_Nat ->
+ let kd_nabrv =
+ (match typschm with
+ | Parse_ast.TypSchm_aux(Parse_ast.TypSchm_ts(Parse_ast.TypQ_aux(tq,_),atyp),_) ->
+ (match tq with
+ | Parse_ast.TypQ_no_forall ->
+ KD_aux(KD_nabbrev(kind,id,to_ast_namescm name_scm_opt, to_ast_nexp k_env atyp), (l,NoTyp))
+ | _ -> typ_error l "Def with kind Nat cannot have universal quantification" None None None)) in
+ kd_nabrv,(names,Envmap.insert k_env (key, k),def_ord)
+ | _ -> assert false
+ )
+ | Parse_ast.KD_record(kind,id,name_scm_opt,typq,fields,_) ->
+ let id = to_ast_id id in
+ let key = id_to_string id in
+ let (kind,k) = to_ast_kind k_env kind in
+ let typq,k_env,_ = to_ast_typquant k_env typq in
+ let fields = List.map (fun (atyp,id) -> (to_ast_typ k_env def_ord atyp),(to_ast_id id)) fields in (* Add check that all arms have unique names locally *)
+ let kd_rec = KD_aux(KD_record(kind,id,to_ast_namescm name_scm_opt,typq,fields,false),(l,NoTyp)) in
+ let typ = (match (typquant_to_quantkinds k_env typq) with
+ | [ ] -> {k = K_Typ}
+ | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
+ kd_rec, (names,Envmap.insert k_env (key,typ), def_ord)
+ | Parse_ast.KD_variant(kind,id,name_scm_opt,typq,arms,_) ->
+ let id = to_ast_id id in
+ let key = id_to_string id in
+ let kind,k = to_ast_kind k_env kind in
+ let typq,k_env,_ = to_ast_typquant k_env typq in
+ let arms = List.map (to_ast_type_union k_env def_ord) arms in (* Add check that all arms have unique names *)
+ let kd_var = KD_aux(KD_variant(kind,id,to_ast_namescm name_scm_opt,typq,arms,false),(l,NoTyp)) in
+ let typ = (match (typquant_to_quantkinds k_env typq) with
+ | [ ] -> {k = K_Typ}
+ | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
+ kd_var, (names,Envmap.insert k_env (key,typ), def_ord)
+ | Parse_ast.KD_enum(kind,id,name_scm_opt,enums,_) ->
+ let id = to_ast_id id in
+ let key = id_to_string id in
+ let kind,k = to_ast_kind k_env kind in
+ let enums = List.map to_ast_id enums in
+ let keys = List.map id_to_string enums in
+ let kd_enum = KD_aux(KD_enum(kind,id,to_ast_namescm name_scm_opt,enums,false),(l,NoTyp)) in (* Add check that all enums have unique names *)
+ let k_env = List.fold_right (fun k k_env -> Envmap.insert k_env (k,{k=K_Nat})) keys (Envmap.insert k_env (key,{k=K_Typ})) in
+ kd_enum, (names,k_env,def_ord)
+ | Parse_ast.KD_register(kind,id,t1,t2,ranges) ->
+ let id = to_ast_id id in
+ let key = id_to_string id in
+ let kind,k = to_ast_kind k_env kind in
+ let n1 = to_ast_nexp k_env t1 in
+ let n2 = to_ast_nexp k_env t2 in
+ let ranges = List.map (fun (range,id) -> (to_ast_range range),to_ast_id id) ranges in
+ KD_aux(KD_register(kind,id,n1,n2,ranges),(l,NoTyp)), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord))
+
+
let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt =
Rec_aux((match r with
| Parse_ast.Rec_nonrec -> Rec_nonrec
@@ -700,6 +783,9 @@ let to_ast_dec (names,k_env,def_ord) (Parse_ast.DEC_aux(regdec,l)) =
let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out * (id * partial_def) list =
let envs = (names,k_env,def_ord) in
match def with
+ | Parse_ast.DEF_kind(k_def) ->
+ let kd,envs = to_ast_kdef envs k_def in
+ ((Finished(DEF_kind(kd))),envs),partial_defs
| Parse_ast.DEF_type(t_def) ->
let td,envs = to_ast_typedef envs t_def in
((Finished(DEF_type(td))),envs),partial_defs
diff --git a/src/initial_check_full_ast.ml b/src/initial_check_full_ast.ml
index 23a2f264..1d5a8c98 100644
--- a/src/initial_check_full_ast.ml
+++ b/src/initial_check_full_ast.ml
@@ -105,7 +105,15 @@ and to_nexp (k_env : kind Envmap.t) (n: Ast.nexp) : Ast.nexp =
match n with
| Nexp_aux(t,l) ->
(match t with
- | Nexp_var(v) ->
+ | Nexp_id i ->
+ let mk = Envmap.apply k_env (id_to_string i) in
+ (match mk with
+ | Some(k) -> Nexp_aux((match k.k with
+ | K_Nat -> Nexp_id i
+ | K_infer -> k.k <- K_Nat; Nexp_id i
+ | _ -> typ_error l "Required a variable with kind Nat, encountered " (Some i) None (Some k)),l)
+ | None -> typ_error l "Encountered an unbound variable" (Some i) None None)
+ | Nexp_var(v) ->
let mk = Envmap.apply k_env (var_to_string v) in
(match mk with
| Some(k) -> Nexp_aux((match k.k with
@@ -482,6 +490,82 @@ let to_typedef (names,k_env,def_ord) (td: tannot type_def) : (tannot type_def) e
let ranges = List.map (fun (range,id) -> (to_range range),id) ranges in
TD_aux(TD_register(id,n1,n2,ranges),(l,NoTyp)), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord))
+let to_kinddef (names,k_env,def_ord) (kd: tannot kind_def) : (tannot kind_def) envs_out =
+ match kd with
+ |KD_aux(td,(l,_)) ->
+ (match td with
+ | KD_abbrev(kind,id,name_scm_opt,typschm) ->
+ let key = id_to_string id in
+ let _,k = to_kind k_env kind in
+ (match k.k with
+ | K_Typ | K_Lam _ ->
+ let typschm,k_env,_ = to_typschm k_env def_ord typschm in
+ let kd_abrv = KD_aux(KD_abbrev(kind,id,to_namescm name_scm_opt,typschm),(l,NoTyp)) in
+ let typ = (match typschm with
+ | TypSchm_aux(TypSchm_ts(tq,typ), _) ->
+ begin match (typquant_to_quantkinds k_env tq) with
+ | [] -> {k = K_Typ}
+ | typs -> {k= K_Lam(typs,{k=K_Typ})}
+ end) in
+ kd_abrv,(names,Envmap.insert k_env (key,typ),def_ord)
+ | _ -> typ_error l "Def abbreviation with type scheme had declared kind other than Type" None None (Some k))
+ | KD_nabbrev(kind,id,name_scm_opt,nexp) ->
+ let key = id_to_string id in
+ let _,k = to_kind k_env kind in
+ (match k.k with
+ | K_Nat ->
+ let nexp = to_nexp k_env nexp in
+ let kd_nabrv = KD_aux(KD_nabbrev(kind,id,to_namescm name_scm_opt, nexp),(l,NoTyp)) in
+ kd_nabrv,(names,Envmap.insert k_env (key,k),def_ord)
+ | _ -> typ_error l "Def abbreviation binding a number declared with kind other than Nat" None None (Some k))
+ | KD_record(kind,id,name_scm_opt,typq,fields,_) ->
+ let key = id_to_string id in
+ let _,k = to_kind k_env kind in
+ let typq,k_env,_ = to_typquant k_env typq in
+ (match k.k with
+ | K_Typ | K_Lam _ ->
+ let fields = List.map (fun (atyp,id) -> (to_typ k_env def_ord atyp),id) fields in (* Add check that all arms have unique names locally *)
+ let kd_rec = KD_aux(KD_record(kind,id,to_namescm name_scm_opt,typq,fields,false),(l,NoTyp)) in
+ let typ = (match (typquant_to_quantkinds k_env typq) with
+ | [ ] -> {k = K_Typ}
+ | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
+ kd_rec, (names,Envmap.insert k_env (key,typ), def_ord)
+ | _ -> typ_error l "Def abbreviation binding a record has kind other than Type" None None (Some k))
+ | KD_variant(kind,id,name_scm_opt,typq,arms,_) ->
+ let key = id_to_string id in
+ let _,k = to_kind k_env kind in
+ let typq,k_env,_ = to_typquant k_env typq in
+ (match k.k with
+ | K_Typ | K_Lam _ ->
+ let arms = List.map (to_type_union k_env def_ord) arms in (* Add check that all arms have unique names *)
+ let kd_var = KD_aux(KD_variant(kind,id,to_namescm name_scm_opt,typq,arms,false),(l,NoTyp)) in
+ let typ = (match (typquant_to_quantkinds k_env typq) with
+ | [ ] -> {k = K_Typ}
+ | typs -> {k = K_Lam(typs,{k=K_Typ})}) in
+ kd_var, (names,Envmap.insert k_env (key,typ), def_ord)
+ | _ -> typ_error l "Def abbreviation binding a variant has kind other than Type" None None (Some k))
+ | KD_enum(kind,id,name_scm_opt,enums,_) ->
+ let key = id_to_string id in
+ let keys = List.map id_to_string enums in
+ let _,k= to_kind k_env kind in
+ (match k.k with
+ | K_Typ ->
+ let kd_enum = KD_aux(KD_enum(kind,id,to_namescm name_scm_opt,enums,false),(l,NoTyp)) in (* Add check that all enums have unique names *)
+ let k_env = List.fold_right (fun k k_env -> Envmap.insert k_env (k,{k=K_Nat})) keys (Envmap.insert k_env (key,{k=K_Typ})) in
+ kd_enum, (names,k_env,def_ord)
+ | _ -> typ_error l "Def abbreviation binding an enum has kind other than Type" None None (Some k))
+ | KD_register(kind,id,t1,t2,ranges) ->
+ let key = id_to_string id in
+ let n1 = to_nexp k_env t1 in
+ let n2 = to_nexp k_env t2 in
+ let _,k = to_kind k_env kind in
+ match k.k with
+ | K_Typ ->
+ let ranges = List.map (fun (range,id) -> (to_range range),id) ranges in
+ KD_aux(KD_register(kind,id,n1,n2,ranges),(l,NoTyp)), (names,Envmap.insert k_env (key, {k=K_Typ}),def_ord)
+ | _ -> typ_error l "Def abbreviation binding a register type has kind other than Type" None None (Some k))
+
+
let to_tannot_opt (k_env:kind Envmap.t) (def_ord:Ast.order) (Typ_annot_opt_aux(tp,l))
:tannot_opt * kind Envmap.t * kind Envmap.t=
match tp with
@@ -545,6 +629,9 @@ let to_dec (names,k_env,def_ord) (DEC_aux(regdec,(l,_))) =
let to_def (names, k_env, def_ord) partial_defs def : def_progress envs_out * (id * partial_def) list =
let envs = (names,k_env,def_ord) in
match def with
+ | DEF_kind(k_def) ->
+ let kd,envs = to_kinddef envs k_def in
+ ((Finished(DEF_kind(kd))),envs),partial_defs
| DEF_type(t_def) ->
let td,envs = to_typedef envs t_def in
((Finished(DEF_type(td))),envs),partial_defs
diff --git a/src/parser.mly b/src/parser.mly
index 3261551b..6ecffd68 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -77,6 +77,7 @@ let irloc r = BF_aux(r, loc())
let defloc df = DT_aux(df, loc())
let tdloc td = TD_aux(td, loc())
+let kdloc kd = KD_aux(kd, loc())
let funloc fn = FD_aux(fn, loc())
let vloc v = VS_aux(v, loc ())
let sdloc sd = SD_aux(sd, loc ())
@@ -131,7 +132,7 @@ let make_vector_sugar order_set is_inc typ typ1 =
/*Terminals with no content*/
-%token And Alias As Assert Bitzero Bitone Bits By Case Clause Const Dec Default Deinfix Effect EFFECT End
+%token And Alias As Assert Bitzero Bitone Bits By Case Clause Const Dec Def Default Deinfix Effect EFFECT End
%token Enumerate Else Exit Extern False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order
%token Pure Rec Register Scattered Struct Switch Then True TwoStarStar Type TYPE Typedef
%token Undefined Union With Val
@@ -1207,9 +1208,46 @@ scattered_def:
| Typedef tid Eq Const Union
{ sdloc (SD_scattered_variant($2,mk_namesectn (),mk_typqn ())) }
+ktype_def:
+ | Def kind tid name_sect Eq typquant typ
+ { kdloc (KD_abbrev($2,$3,$4,mk_typschm $6 $7 6 7)) }
+ | Def kind tid name_sect Eq typ
+ { kdloc (KD_abbrev($2,$3,$4,mk_typschm (mk_typqn ()) $6 6 6)) }
+ | Def kind tid Eq typquant typ
+ { kdloc (KD_abbrev($2,$3,mk_namesectn (), mk_typschm $5 $6 5 6)) }
+ | Def kind tid Eq typ
+ { kdloc (KD_abbrev($2,$3,mk_namesectn (),mk_typschm (mk_typqn ()) $5 5 5)) }
+ | Def kind tid Eq Num
+ { kdloc (KD_abbrev($2,$3,mk_namesectn (),mk_typschm (mk_typqn ()) (tlocl (ATyp_constant $5) 5 5) 5 5)) }
+ | Def kind tid name_sect Eq Const Struct typquant Lcurly c_def_body Rcurly
+ { kdloc (KD_record($2,$3,$4,$8,fst $10, snd $10)) }
+ | Def kind tid name_sect Eq Const Struct Lcurly c_def_body Rcurly
+ { kdloc (KD_record($2,$3,$4,(mk_typqn ()), fst $9, snd $9)) }
+ | Def kind tid Eq Const Struct typquant Lcurly c_def_body Rcurly
+ { kdloc (KD_record($2,$3,mk_namesectn (), $7, fst $9, snd $9)) }
+ | Def kind tid Eq Const Struct Lcurly c_def_body Rcurly
+ { kdloc (KD_record($2,$3, mk_namesectn (), mk_typqn (), fst $8, snd $8)) }
+ | Def kind tid name_sect Eq Const Union typquant Lcurly union_body Rcurly
+ { kdloc (KD_variant($2,$3,$4, $8, fst $10, snd $10)) }
+ | Def kind tid Eq Const Union typquant Lcurly union_body Rcurly
+ { kdloc (KD_variant($2,$3,mk_namesectn (), $7, fst $9, snd $9)) }
+ | Def kind tid name_sect Eq Const Union Lcurly union_body Rcurly
+ { kdloc (KD_variant($2, $3,$4, mk_typqn (), fst $9, snd $9)) }
+ | Def kind tid Eq Const Union Lcurly union_body Rcurly
+ { kdloc (KD_variant($2,$3, mk_namesectn (), mk_typqn (), fst $8, snd $8)) }
+ | Def kind tid Eq Enumerate Lcurly enum_body Rcurly
+ { kdloc (KD_enum($2,$3, mk_namesectn (), $7,false)) }
+ | Def kind tid name_sect Eq Enumerate Lcurly enum_body Rcurly
+ { kdloc (KD_enum($2,$3,$4,$8,false)) }
+ | Def kind tid Eq Register Bits Lsquare nexp_typ Colon nexp_typ Rsquare Lcurly r_def_body Rcurly
+ { kdloc (KD_register($2,$3, $8, $10, $13)) }
+
+
def:
| type_def
- { dloc (DEF_type($1)) }
+ { dloc (DEF_type($1)) }
+ | ktype_def
+ { assert false }
| fun_def
{ dloc (DEF_fundef($1)) }
| letbind
diff --git a/src/pre_lexer.mll b/src/pre_lexer.mll
index 8987c0fd..f6ccd3c2 100644
--- a/src/pre_lexer.mll
+++ b/src/pre_lexer.mll
@@ -96,6 +96,7 @@ let kw_table =
("true", (fun x -> Other));
("Type", (fun x -> Other));
("typedef", (fun x -> Typedef));
+ ("def", (fun x -> Def));
("undefined", (fun x -> Other));
("union", (fun x -> Other));
("with", (fun x -> Other));
diff --git a/src/pre_parser.mly b/src/pre_parser.mly
index 9aceb371..0b2c916f 100644
--- a/src/pre_parser.mly
+++ b/src/pre_parser.mly
@@ -52,7 +52,7 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *)
/*Terminals with no content*/
-%token Scattered Typedef Other Eof
+%token Scattered Typedef Def Other Eof
%token <string> Id
%start file
@@ -62,7 +62,9 @@ let r = fun x -> x (* Ulib.Text.of_latin1 *)
id_found:
| Typedef Id
- { $2 }
+ { $2 }
+ | Def Id Id
+ { $3 }
skip:
| Scattered
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 5f0990d1..ad6d02a7 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -120,14 +120,15 @@ let rec pp_format_typ_lem (Typ_aux(t,l)) =
and pp_format_nexp_lem (Nexp_aux(n,l)) =
"(Nexp_aux " ^
(match n with
- | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")"
- | Nexp_constant(i) -> "(Nexp_constant " ^ (lemnum string_of_int i) ^ ")"
- | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
- | Nexp_minus(n1,n2) -> "(Nexp_minus " ^ (pp_format_nexp_lem n1)^ " " ^ (pp_format_nexp_lem n2) ^ ")"
- | Nexp_times(n1,n2) -> "(Nexp_times " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
- | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")"
- | Nexp_neg(n1) -> "(Nexp_neg " ^ (pp_format_nexp_lem n1) ^ ")") ^ " " ^
- (pp_format_l_lem l) ^ ")"
+ | Nexp_id(i) -> "(Nexp_id " ^ pp_format_id_lem i ^ ")"
+ | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")"
+ | Nexp_constant(i) -> "(Nexp_constant " ^ (lemnum string_of_int i) ^ ")"
+ | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
+ | Nexp_minus(n1,n2) -> "(Nexp_minus " ^ (pp_format_nexp_lem n1)^ " " ^ (pp_format_nexp_lem n2) ^ ")"
+ | Nexp_times(n1,n2) -> "(Nexp_times " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
+ | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")"
+ | Nexp_neg(n1) -> "(Nexp_neg " ^ (pp_format_nexp_lem n1) ^ ")") ^ " " ^
+ (pp_format_l_lem l) ^ ")"
and pp_format_ord_lem (Ord_aux(o,l)) =
"(Ord_aux " ^
(match o with
@@ -257,19 +258,20 @@ and pp_format_targ = function
| TA_ord o -> "(T_arg_order " ^ pp_format_o o ^ ")"
and pp_format_n n =
match n.nexp with
- | Nvar i -> "(Ne_var \"" ^ i ^ "\")"
- | Nconst i -> "(Ne_const " ^ (lemnum string_of_int (int_of_big_int i)) ^ ")"
- | Npos_inf -> "Ne_inf"
- | Nadd(n1,n2) -> "(Ne_add [" ^ (pp_format_n n1) ^ "; " ^ (pp_format_n n2) ^ "])"
- | Nsub(n1,n2) -> "(Ne_minus "^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")"
- | Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")"
- | N2n(n,Some i) -> "(Ne_exp " ^ (pp_format_n n) ^ "(*" ^ string_of_big_int i ^ "*)" ^ ")"
- | N2n(n,None) -> "(Ne_exp " ^ (pp_format_n n) ^ ")"
- | Nneg n -> "(Ne_unary " ^ (pp_format_n n) ^ ")"
- | Nuvar _ -> "(Ne_var \"fresh_v_" ^ string_of_int (get_index n) ^ "\")"
- | Nneg_inf -> "(Ne_unary Ne_inf)"
- | Npow _ -> "power_not_implemented"
- | Ninexact -> "(Ne_add Ne_inf (Ne_unary Ne_inf)"
+ | Nid (i, n) -> "(Ne_id \"" ^ i ^ " " ^ "\")"
+ | Nvar i -> "(Ne_var \"" ^ i ^ "\")"
+ | Nconst i -> "(Ne_const " ^ (lemnum string_of_int (int_of_big_int i)) ^ ")"
+ | Npos_inf -> "Ne_inf"
+ | Nadd(n1,n2) -> "(Ne_add [" ^ (pp_format_n n1) ^ "; " ^ (pp_format_n n2) ^ "])"
+ | Nsub(n1,n2) -> "(Ne_minus "^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")"
+ | Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")"
+ | N2n(n,Some i) -> "(Ne_exp " ^ (pp_format_n n) ^ "(*" ^ string_of_big_int i ^ "*)" ^ ")"
+ | N2n(n,None) -> "(Ne_exp " ^ (pp_format_n n) ^ ")"
+ | Nneg n -> "(Ne_unary " ^ (pp_format_n n) ^ ")"
+ | Nuvar _ -> "(Ne_var \"fresh_v_" ^ string_of_int (get_index n) ^ "\")"
+ | Nneg_inf -> "(Ne_unary Ne_inf)"
+ | Npow _ -> "power_not_implemented"
+ | Ninexact -> "(Ne_add Ne_inf (Ne_unary Ne_inf)"
and pp_format_e e =
"(Effect_aux " ^
(match e.effect with
@@ -537,6 +539,41 @@ let pp_lem_typdef ppf (TD_aux(td,(l,annot))) =
in
fprintf ppf "@[<0>(TD_aux %a (%a, %a))@]" print_td td pp_lem_l l pp_annot annot
+let pp_lem_kindef ppf (KD_aux(kd,(l,annot))) =
+ let print_kd ppf kd =
+ match kd with
+ | KD_abbrev(kind,id,namescm,typschm) ->
+ fprintf ppf "@[<0>(KD_abbrev %a %a %a %a)@]"
+ pp_lem_kind kind pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm
+ | KD_nabbrev(kind,id,namescm,n) ->
+ fprintf ppf "@[<0>(KD_nabbrev %a %a %a %a)@]"
+ pp_lem_kind kind pp_lem_id id pp_lem_namescm namescm pp_lem_nexp n
+ | KD_record(kind,id,nm,typq,fs,_) ->
+ let f_pp ppf (typ,id) =
+ fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in
+ fprintf ppf "@[<0>(%a %a %a %a %a [%a] false)@]"
+ kwd "KD_record" pp_lem_kind kind pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs
+ | KD_variant(kind,id,nm,typq,ar,_) ->
+ let a_pp ppf (Tu_aux(typ_u,l)) =
+ match typ_u with
+ | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]"
+ pp_lem_typ typ pp_lem_id id pp_lem_l l
+ | Tu_id(id) -> fprintf ppf "@[<1>(Tu_aux (Tu_id %a) %a);@]" pp_lem_id id pp_lem_l l
+ in
+ fprintf ppf "@[<0>(%a %a %a %a %a [%a] false)@]"
+ kwd "KD_variant" pp_lem_kind kind pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar
+ | KD_enum(kind,id,ns,enums,_) ->
+ let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in
+ fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
+ kwd "KD_enum" pp_lem_kind kind pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums
+ | KD_register(kind,id,n1,n2,rs) ->
+ let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in
+ let pp_rids = (list_pp pp_rid pp_rid) in
+ fprintf ppf "@[<0>(%a %a %a %a %a [%a])@]"
+ kwd "KD_register" pp_lem_kind kind pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs
+ in
+ fprintf ppf "@[<0>(KD_aux %a (%a, %a))@]" print_kd kd pp_lem_l l pp_annot annot
+
let pp_lem_rec ppf (Rec_aux(r,l)) =
match r with
| Rec_nonrec -> fprintf ppf "(Rec_aux Rec_nonrec %a)" pp_lem_l l
@@ -589,9 +626,11 @@ let pp_lem_def ppf d =
| DEF_default(df) -> fprintf ppf "(DEF_default %a);" pp_lem_default df
| DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a);" pp_lem_spec v_spec
| DEF_type(t_def) -> fprintf ppf "(DEF_type %a);" pp_lem_typdef t_def
+ | DEF_kind(k_def) -> fprintf ppf "(DEF_kind %a);" pp_lem_kindef k_def
| DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a);" pp_lem_fundef f_def
| DEF_val(lbind) -> fprintf ppf "(DEF_val %a);" pp_lem_let lbind
| DEF_reg_dec(dec) -> fprintf ppf "(DEF_reg_dec %a);" pp_lem_dec dec
+ | DEF_comm d -> fprintf ppf ""
| _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs")
let pp_lem_defs ppf (Defs(defs)) =
@@ -757,9 +796,10 @@ let doc_typ, doc_atomic_typ, doc_nexp =
minus ^^ (atomic_nexp_typ n1)
| _ -> atomic_nexp_typ ne
and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with
- | Nexp_var v -> doc_var v
- | Nexp_constant i -> doc_int i
- | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _->
+ | Nexp_var v -> doc_var v
+ | Nexp_id i -> doc_id i
+ | Nexp_constant i -> doc_int i
+ | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _->
group (parens (nexp ne))
(* expose doc_typ, doc_atomic_typ and doc_nexp *)
@@ -936,6 +976,8 @@ let doc_exp, doc_let =
| E_nondet exps ->
let exps_doc = separate_map (semi ^^ hardline) exp exps in
string "nondet" ^^ space ^^ (surround 2 1 lbrace exps_doc rbrace)
+ | E_comment s -> string ("(*" ^ s ^ "*)")
+ | E_comment_struc e -> string "(*" ^^ exp e ^^ string "*)"
| E_id id -> doc_id id
| E_lit lit -> doc_lit lit
| E_cast(typ,e) -> prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp e))
@@ -1137,6 +1179,39 @@ let doc_typdef (TD_aux(td,_)) = match td with
braces doc_rids;
])
+let doc_kindef (KD_aux(kd,_)) = match kd with
+ | KD_abbrev(kind,id,nm,typschm) ->
+ doc_op equals (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm]) (doc_typscm typschm)
+ | KD_nabbrev(kind,id,nm,n) ->
+ doc_op equals (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm]) (doc_nexp n)
+ | KD_record(kind,id,nm,typq,fs,_) ->
+ let f_pp (typ,id) = concat [doc_typ typ; space; doc_id id; semi] in
+ let fs_doc = group (separate_map (break 1) f_pp fs) in
+ doc_op equals
+ (concat [string "def"; space;doc_kind kind; space; doc_id id; doc_namescm nm])
+ (string "const struct" ^^ space ^^ doc_typquant typq (braces fs_doc))
+ | KD_variant(kind,id,nm,typq,ar,_) ->
+ let ar_doc = group (separate_map (semi ^^ break 1) doc_type_union ar) in
+ doc_op equals
+ (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm])
+ (string "const union" ^^ space ^^ doc_typquant typq (braces ar_doc))
+ | KD_enum(kind,id,nm,enums,_) ->
+ let enums_doc = group (separate_map (semi ^^ break 1) doc_id enums) in
+ doc_op equals
+ (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm])
+ (string "enumerate" ^^ space ^^ braces enums_doc)
+ | KD_register(kind,id,n1,n2,rs) ->
+ let doc_rid (r,id) = separate space [doc_range r; colon; doc_id id] ^^ semi in
+ let doc_rids = group (separate_map (break 1) doc_rid rs) in
+ doc_op equals
+ (string "def" ^^ space ^^ doc_kind kind ^^ space ^^ doc_id id)
+ (separate space [
+ string "register bits";
+ brackets (doc_nexp n1 ^^ colon ^^ doc_nexp n2);
+ braces doc_rids;
+ ])
+
+
let doc_rec (Rec_aux(r,_)) = match r with
| Rec_nonrec -> empty
(* include trailing space because caller doesn't know if we return
@@ -1206,6 +1281,7 @@ let rec doc_def def = group (match def with
| DEF_default df -> doc_default df
| DEF_spec v_spec -> doc_spec v_spec
| DEF_type t_def -> doc_typdef t_def
+ | DEF_kind k_def -> doc_kindef k_def
| DEF_fundef f_def -> doc_fundef f_def
| DEF_val lbind -> doc_let lbind
| DEF_reg_dec dec -> doc_dec dec
@@ -1752,6 +1828,56 @@ let doc_typdef_ocaml (TD_aux(td,_)) = match td with
string (if dir then "true" else "false");
brackets doc_rids]))])
+let doc_kdef_ocaml (KD_aux(kd,_)) = match kd with
+ | KD_abbrev(_,id,nm,typschm) ->
+ doc_op equals (concat [string "type"; space; doc_id_ocaml_type id;]) (doc_typscm_ocaml typschm)
+ | KD_record(_,id,nm,typq,fs,_) ->
+ let f_pp (typ,id) = concat [doc_id_ocaml_type id; space; colon; doc_typ_ocaml typ; semi] in
+ let fs_doc = group (separate_map (break 1) f_pp fs) in
+ doc_op equals
+ (concat [string "type"; space; doc_id_ocaml_type id;]) (doc_typquant_ocaml typq (braces fs_doc))
+ | KD_variant(_,id,nm,typq,ar,_) ->
+ let n = List.length ar in
+ let ar_doc = group (separate_map (break 1) (doc_type_union_ocaml n) ar) in
+ doc_op equals
+ (concat [string "type"; space; doc_id_ocaml_type id;])
+ (if n > 246
+ then brackets (space ^^(doc_typquant_ocaml typq ar_doc))
+ else (doc_typquant_ocaml typq ar_doc))
+ | KD_enum(_,id,nm,enums,_) ->
+ let n = List.length enums in
+ let enums_doc = group (separate_map (break 1 ^^ pipe) (doc_id_ocaml_ctor n) enums) in
+ doc_op equals
+ (concat [string "type"; space; doc_id_ocaml_type id;])
+ (enums_doc)
+ | KD_register(_,id,n1,n2,rs) ->
+ let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id id); doc_range_ocaml r;]) in
+ let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in
+ match n1,n2 with
+ | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) ->
+ let dir = i1 < i2 in
+ let size = if dir then i2-i1 +1 else i1-i2 in
+ doc_op equals
+ ((string "let") ^^ space ^^ doc_id_ocaml id ^^ space ^^ (string "init_val"))
+ (separate space [string "Vregister";
+ (parens (separate comma_sp
+ [parens (separate space
+ [string "match init_val with";
+ pipe;
+ string "None";
+ arrow;
+ string "ref";
+ string "(Array.make";
+ doc_int size;
+ string "Vzero)";
+ pipe;
+ string "Some init_val";
+ arrow;
+ string "ref init_val";]);
+ doc_nexp n1;
+ string (if dir then "true" else "false");
+ brackets doc_rids]))])
+
let doc_rec_ocaml (Rec_aux(r,_)) = match r with
| Rec_nonrec -> empty
| Rec_rec -> string "rec" ^^ space
diff --git a/src/process_file.ml b/src/process_file.ml
index db064b83..ec0d8d08 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -95,7 +95,8 @@ let initi_check_ast (defs : Type_internal.tannot Ast.defs) : (Type_internal.tann
Initial_check_full_ast.to_checked_ast Nameset.empty Type_internal.initial_kind_env (Ast.Ord_aux(Ast.Ord_inc,Parse_ast.Unknown)) defs
let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.order) : Type_internal.tannot Ast.defs =
- let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env;
+ let d_env = { Type_internal.k_env = k; Type_internal.abbrevs = Type_internal.initial_abbrev_env;
+ Type_internal.nabbrevs = Envmap.empty;
Type_internal.namesch = Envmap.empty; Type_internal.enum_env = Envmap.empty;
Type_internal.rec_env = []; Type_internal.alias_env = Envmap.empty;
Type_internal.default_o =
diff --git a/src/rewriter.ml b/src/rewriter.ml
index d957ee6c..d9e3925b 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -90,6 +90,7 @@ let fix_effsum_exp (E_aux (e,(l,annot))) =
| E_assign (lexp,e) -> union_effs [get_effsum_lexp lexp;get_effsum_exp e]
| E_exit e -> get_effsum_exp e
| E_assert (c,m) -> pure_e
+ | E_comment _ | E_comment_struc _ -> pure_e
| E_internal_cast (_,e) -> get_effsum_exp e
| E_internal_exp _ -> pure_e
| E_internal_exp_user _ -> pure_e
@@ -278,139 +279,140 @@ let rewrite_exp rewriters nmap (E_aux (exp,(l,annot))) =
let rewrap e = E_aux (e,(l,annot)) in
let rewrite = rewriters.rewrite_exp rewriters nmap in
match exp with
- | E_block exps -> rewrap (E_block (List.map rewrite exps))
- | E_nondet exps -> rewrap (E_nondet (List.map rewrite exps))
- | E_lit (L_aux ((L_hex _ | L_bin _) as lit,_)) ->
- let es = List.map (fun p -> E_aux (E_lit p ,(Parse_ast.Generated l,simple_annot {t = Tid "bit"})))
- (vector_string_to_bit_list l lit) in
- rewrap (E_vector es)
- | E_id _ | E_lit _ -> rewrap exp
- | E_cast (typ, exp) -> rewrap (E_cast (typ, rewrite exp))
- | E_app (id,exps) -> rewrap (E_app (id,List.map rewrite exps))
- | E_app_infix(el,id,er) -> rewrap (E_app_infix(rewrite el,id,rewrite er))
- | E_tuple exps -> rewrap (E_tuple (List.map rewrite exps))
- | E_if (c,t,e) -> rewrap (E_if (rewrite c,rewrite t, rewrite e))
- | E_for (id, e1, e2, e3, o, body) ->
- rewrap (E_for (id, rewrite e1, rewrite e2, rewrite e3, o, rewrite body))
- | E_vector exps -> rewrap (E_vector (List.map rewrite exps))
- | E_vector_indexed (exps,(Def_val_aux(default,dannot))) ->
- let def = match default with
- | Def_val_empty -> default
- | Def_val_dec e -> Def_val_dec (rewrite e) in
- rewrap (E_vector_indexed (List.map (fun (i,e) -> (i, rewrite e)) exps, Def_val_aux(def,dannot)))
- | E_vector_access (vec,index) -> rewrap (E_vector_access (rewrite vec,rewrite index))
- | E_vector_subrange (vec,i1,i2) ->
- rewrap (E_vector_subrange (rewrite vec,rewrite i1,rewrite i2))
- | E_vector_update (vec,index,new_v) ->
- rewrap (E_vector_update (rewrite vec,rewrite index,rewrite new_v))
- | E_vector_update_subrange (vec,i1,i2,new_v) ->
- rewrap (E_vector_update_subrange (rewrite vec,rewrite i1,rewrite i2,rewrite new_v))
- | E_vector_append (v1,v2) -> rewrap (E_vector_append (rewrite v1,rewrite v2))
- | E_list exps -> rewrap (E_list (List.map rewrite exps))
- | E_cons(h,t) -> rewrap (E_cons (rewrite h,rewrite t))
- | E_record (FES_aux (FES_Fexps(fexps, bool),fannot)) ->
- rewrap (E_record
- (FES_aux (FES_Fexps
- (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) ->
- FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps, bool), fannot)))
- | E_record_update (re,(FES_aux (FES_Fexps(fexps, bool),fannot))) ->
- rewrap (E_record_update ((rewrite re),
- (FES_aux (FES_Fexps
- (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) ->
- FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps, bool), fannot))))
- | E_field(exp,id) -> rewrap (E_field(rewrite exp,id))
- | E_case (exp ,pexps) ->
- rewrap (E_case (rewrite exp,
- (List.map
- (fun (Pat_aux (Pat_exp(p,e),pannot)) ->
- Pat_aux (Pat_exp(rewriters.rewrite_pat rewriters nmap p,rewrite e),pannot)) pexps)))
- | E_let (letbind,body) -> rewrap (E_let(rewriters.rewrite_let rewriters nmap letbind,rewrite body))
- | E_assign (lexp,exp) -> rewrap (E_assign(rewriters.rewrite_lexp rewriters nmap lexp,rewrite exp))
- | E_exit e -> rewrap (E_exit (rewrite e))
- | E_assert(e1,e2) -> rewrap (E_assert(rewrite e1,rewrite e2))
- | E_internal_cast ((l,casted_annot),exp) ->
- let new_exp = rewrite exp in
- (*let _ = Printf.eprintf "Removing an internal_cast with %s\n" (tannot_to_string casted_annot) in*)
- (match casted_annot,exp with
- | Base((_,t),_,_,_,_,_),E_aux(ec,(ecl,Base((_,exp_t),_,_,_,_,_))) ->
- (*let _ = Printf.eprintf "Considering removing an internal cast where the two types are %s and %s\n" (t_to_string t) (t_to_string exp_t) in*)
- (match t.t,exp_t.t with
- (*TODO should pass d_env into here so that I can look at the abbreviations if there are any here*)
- | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]),
- Tapp("vector",[TA_nexp n2;TA_nexp nw2;TA_ord o2;_])
- | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]),
- Tapp("reg",[TA_typ {t=(Tapp("vector",[TA_nexp n2; TA_nexp nw2; TA_ord o2;_]))}]) ->
- (match n1.nexp with
- | Nconst i1 -> if nexp_eq n1 n2 then new_exp else rewrap (E_cast (t_to_typ t,new_exp))
- | _ -> (match o1.order with
- | Odec ->
- (*let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n"
+ | E_comment _ | E_comment_struc _ -> rewrap exp
+ | E_block exps -> rewrap (E_block (List.map rewrite exps))
+ | E_nondet exps -> rewrap (E_nondet (List.map rewrite exps))
+ | E_lit (L_aux ((L_hex _ | L_bin _) as lit,_)) ->
+ let es = List.map (fun p -> E_aux (E_lit p ,(Parse_ast.Generated l,simple_annot {t = Tid "bit"})))
+ (vector_string_to_bit_list l lit) in
+ rewrap (E_vector es)
+ | E_id _ | E_lit _ -> rewrap exp
+ | E_cast (typ, exp) -> rewrap (E_cast (typ, rewrite exp))
+ | E_app (id,exps) -> rewrap (E_app (id,List.map rewrite exps))
+ | E_app_infix(el,id,er) -> rewrap (E_app_infix(rewrite el,id,rewrite er))
+ | E_tuple exps -> rewrap (E_tuple (List.map rewrite exps))
+ | E_if (c,t,e) -> rewrap (E_if (rewrite c,rewrite t, rewrite e))
+ | E_for (id, e1, e2, e3, o, body) ->
+ rewrap (E_for (id, rewrite e1, rewrite e2, rewrite e3, o, rewrite body))
+ | E_vector exps -> rewrap (E_vector (List.map rewrite exps))
+ | E_vector_indexed (exps,(Def_val_aux(default,dannot))) ->
+ let def = match default with
+ | Def_val_empty -> default
+ | Def_val_dec e -> Def_val_dec (rewrite e) in
+ rewrap (E_vector_indexed (List.map (fun (i,e) -> (i, rewrite e)) exps, Def_val_aux(def,dannot)))
+ | E_vector_access (vec,index) -> rewrap (E_vector_access (rewrite vec,rewrite index))
+ | E_vector_subrange (vec,i1,i2) ->
+ rewrap (E_vector_subrange (rewrite vec,rewrite i1,rewrite i2))
+ | E_vector_update (vec,index,new_v) ->
+ rewrap (E_vector_update (rewrite vec,rewrite index,rewrite new_v))
+ | E_vector_update_subrange (vec,i1,i2,new_v) ->
+ rewrap (E_vector_update_subrange (rewrite vec,rewrite i1,rewrite i2,rewrite new_v))
+ | E_vector_append (v1,v2) -> rewrap (E_vector_append (rewrite v1,rewrite v2))
+ | E_list exps -> rewrap (E_list (List.map rewrite exps))
+ | E_cons(h,t) -> rewrap (E_cons (rewrite h,rewrite t))
+ | E_record (FES_aux (FES_Fexps(fexps, bool),fannot)) ->
+ rewrap (E_record
+ (FES_aux (FES_Fexps
+ (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) ->
+ FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps, bool), fannot)))
+ | E_record_update (re,(FES_aux (FES_Fexps(fexps, bool),fannot))) ->
+ rewrap (E_record_update ((rewrite re),
+ (FES_aux (FES_Fexps
+ (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) ->
+ FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps, bool), fannot))))
+ | E_field(exp,id) -> rewrap (E_field(rewrite exp,id))
+ | E_case (exp ,pexps) ->
+ rewrap (E_case (rewrite exp,
+ (List.map
+ (fun (Pat_aux (Pat_exp(p,e),pannot)) ->
+ Pat_aux (Pat_exp(rewriters.rewrite_pat rewriters nmap p,rewrite e),pannot)) pexps)))
+ | E_let (letbind,body) -> rewrap (E_let(rewriters.rewrite_let rewriters nmap letbind,rewrite body))
+ | E_assign (lexp,exp) -> rewrap (E_assign(rewriters.rewrite_lexp rewriters nmap lexp,rewrite exp))
+ | E_exit e -> rewrap (E_exit (rewrite e))
+ | E_assert(e1,e2) -> rewrap (E_assert(rewrite e1,rewrite e2))
+ | E_internal_cast ((l,casted_annot),exp) ->
+ let new_exp = rewrite exp in
+ (*let _ = Printf.eprintf "Removing an internal_cast with %s\n" (tannot_to_string casted_annot) in*)
+ (match casted_annot,exp with
+ | Base((_,t),_,_,_,_,_),E_aux(ec,(ecl,Base((_,exp_t),_,_,_,_,_))) ->
+ (*let _ = Printf.eprintf "Considering removing an internal cast where the two types are %s and %s\n" (t_to_string t) (t_to_string exp_t) in*)
+ (match t.t,exp_t.t with
+ (*TODO should pass d_env into here so that I can look at the abbreviations if there are any here*)
+ | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]),
+ Tapp("vector",[TA_nexp n2;TA_nexp nw2;TA_ord o2;_])
+ | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]),
+ Tapp("reg",[TA_typ {t=(Tapp("vector",[TA_nexp n2; TA_nexp nw2; TA_ord o2;_]))}]) ->
+ (match n1.nexp with
+ | Nconst i1 -> if nexp_eq n1 n2 then new_exp else rewrap (E_cast (t_to_typ t,new_exp))
+ | _ -> (match o1.order with
+ | Odec ->
+ (*let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n"
(n_to_string nw1) (n_to_string n1) (nexp_one_more_than nw1 n1) in*)
- rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"),Parse_ast.Generated l)),
- Parse_ast.Generated l),new_exp))
- | _ -> new_exp))
- | _ -> new_exp)
- | Base((_,t),_,_,_,_,_),_ ->
- (*let _ = Printf.eprintf "Considering removing an internal cast where the remaining type is %s\n%!"
+ rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"),Parse_ast.Generated l)),
+ Parse_ast.Generated l),new_exp))
+ | _ -> new_exp))
+ | _ -> new_exp)
+ | Base((_,t),_,_,_,_,_),_ ->
+ (*let _ = Printf.eprintf "Considering removing an internal cast where the remaining type is %s\n%!"
(t_to_string t) in*)
- (match t.t with
- | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]) ->
- (match o1.order with
- | Odec ->
- let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n"
+ (match t.t with
+ | Tapp("vector",[TA_nexp n1;TA_nexp nw1;TA_ord o1;_]) ->
+ (match o1.order with
+ | Odec ->
+ let _ = Printf.eprintf "Considering removing a cast or not: %s %s, %b\n"
(n_to_string nw1) (n_to_string n1) (nexp_one_more_than nw1 n1) in
- rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Parse_ast.Generated l)),
- Parse_ast.Generated l), new_exp))
- | _ -> new_exp)
- | _ -> new_exp)
- | _ -> (*let _ = Printf.eprintf "Not a base match?\n" in*) new_exp)
- | E_internal_exp (l,impl) ->
- (match impl with
- | Base((_,t),_,_,_,_,bounds) ->
- let bounds = match nmap with | None -> bounds | Some (nm,_) -> add_map_to_bounds nm bounds in
- (*let _ = Printf.eprintf "Rewriting internal expression, with type %s, and bounds %s\n" (t_to_string t) (bounds_to_string bounds) in*)
- (match t.t with
- (*Old case; should possibly be removed*)
- | Tapp("register",[TA_typ {t= Tapp("vector",[ _; TA_nexp r;_;_])}])
- | Tapp("vector", [_;TA_nexp r;_;_]) ->
- (*let _ = Printf.eprintf "vector case with %s, bounds are %s\n"
+ rewrap (E_cast (Typ_aux (Typ_var (Kid_aux((Var "length"), Parse_ast.Generated l)),
+ Parse_ast.Generated l), new_exp))
+ | _ -> new_exp)
+ | _ -> new_exp)
+ | _ -> (*let _ = Printf.eprintf "Not a base match?\n" in*) new_exp)
+ | E_internal_exp (l,impl) ->
+ (match impl with
+ | Base((_,t),_,_,_,_,bounds) ->
+ let bounds = match nmap with | None -> bounds | Some (nm,_) -> add_map_to_bounds nm bounds in
+ (*let _ = Printf.eprintf "Rewriting internal expression, with type %s, and bounds %s\n" (t_to_string t) (bounds_to_string bounds) in*)
+ (match t.t with
+ (*Old case; should possibly be removed*)
+ | Tapp("register",[TA_typ {t= Tapp("vector",[ _; TA_nexp r;_;_])}])
+ | Tapp("vector", [_;TA_nexp r;_;_]) ->
+ (*let _ = Printf.eprintf "vector case with %s, bounds are %s\n"
(n_to_string r) (bounds_to_string bounds) in*)
- let nexps = expand_nexp r in
- (match (match_to_program_vars nexps bounds) with
- | [] -> rewrite_nexp_to_exp None l r
- | map -> rewrite_nexp_to_exp (Some map) l r)
- | Tapp("implicit", [TA_nexp i]) ->
- (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*)
- let nexps = expand_nexp i in
- (match (match_to_program_vars nexps bounds) with
- | [] -> rewrite_nexp_to_exp None l i
- | map -> rewrite_nexp_to_exp (Some map) l i)
- | _ ->
- raise (Reporting_basic.err_unreachable l
- ("Internal_exp given unexpected types " ^ (t_to_string t))))
- | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp given none Base annot")))
- | E_internal_exp_user ((l,user_spec),(_,impl)) ->
- (match (user_spec,impl) with
- | (Base((_,tu),_,_,_,_,_), Base((_,ti),_,_,_,_,bounds)) ->
- (*let _ = Printf.eprintf "E_interal_user getting rewritten two types are %s and %s\n"
+ let nexps = expand_nexp r in
+ (match (match_to_program_vars nexps bounds) with
+ | [] -> rewrite_nexp_to_exp None l r
+ | map -> rewrite_nexp_to_exp (Some map) l r)
+ | Tapp("implicit", [TA_nexp i]) ->
+ (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*)
+ let nexps = expand_nexp i in
+ (match (match_to_program_vars nexps bounds) with
+ | [] -> rewrite_nexp_to_exp None l i
+ | map -> rewrite_nexp_to_exp (Some map) l i)
+ | _ ->
+ raise (Reporting_basic.err_unreachable l
+ ("Internal_exp given unexpected types " ^ (t_to_string t))))
+ | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp given none Base annot")))
+ | E_internal_exp_user ((l,user_spec),(_,impl)) ->
+ (match (user_spec,impl) with
+ | (Base((_,tu),_,_,_,_,_), Base((_,ti),_,_,_,_,bounds)) ->
+ (*let _ = Printf.eprintf "E_interal_user getting rewritten two types are %s and %s\n"
(t_to_string tu) (t_to_string ti) in*)
- let bounds = match nmap with | None -> bounds | Some (nm,_) -> add_map_to_bounds nm bounds in
- (match (tu.t,ti.t) with
- | (Tapp("implicit", [TA_nexp u]),Tapp("implicit",[TA_nexp i])) ->
- (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*)
- let nexps = expand_nexp i in
- (match (match_to_program_vars nexps bounds) with
- | [] -> rewrite_nexp_to_exp None l i
- (*add u to program_vars env; for now it will work out properly by accident*)
- | map -> rewrite_nexp_to_exp (Some map) l i)
- | _ ->
- raise (Reporting_basic.err_unreachable l
- ("Internal_exp_user given unexpected types " ^ (t_to_string tu) ^ ", " ^ (t_to_string ti))))
- | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp_user given none Base annot")))
- | E_internal_let _ -> raise (Reporting_basic.err_unreachable l "Internal let found before it should have been introduced")
- | E_internal_return _ -> raise (Reporting_basic.err_unreachable l "Internal return found before it should have been introduced")
- | E_internal_plet _ -> raise (Reporting_basic.err_unreachable l " Internal plet found before it should have been introduced")
-
+ let bounds = match nmap with | None -> bounds | Some (nm,_) -> add_map_to_bounds nm bounds in
+ (match (tu.t,ti.t) with
+ | (Tapp("implicit", [TA_nexp u]),Tapp("implicit",[TA_nexp i])) ->
+ (*let _ = Printf.eprintf "Implicit case with %s\n" (n_to_string i) in*)
+ let nexps = expand_nexp i in
+ (match (match_to_program_vars nexps bounds) with
+ | [] -> rewrite_nexp_to_exp None l i
+ (*add u to program_vars env; for now it will work out properly by accident*)
+ | map -> rewrite_nexp_to_exp (Some map) l i)
+ | _ ->
+ raise (Reporting_basic.err_unreachable l
+ ("Internal_exp_user given unexpected types " ^ (t_to_string tu) ^ ", " ^ (t_to_string ti))))
+ | _ -> raise (Reporting_basic.err_unreachable l ("Internal_exp_user given none Base annot")))
+ | E_internal_let _ -> raise (Reporting_basic.err_unreachable l "Internal let found before it should have been introduced")
+ | E_internal_return _ -> raise (Reporting_basic.err_unreachable l "Internal return found before it should have been introduced")
+ | E_internal_plet _ -> raise (Reporting_basic.err_unreachable l " Internal plet found before it should have been introduced")
+
let rewrite_let rewriters map (LB_aux(letbind,(l,annot))) =
let local_map = get_map_tannot annot in
let map =
@@ -457,7 +459,7 @@ let rewrite_fun rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls
in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot))
let rewrite_def rewriters d = match d with
- | DEF_type _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ -> d
+ | DEF_type _ | DEF_kind _ | DEF_spec _ | DEF_default _ | DEF_reg_dec _ | DEF_comm _ -> d
| DEF_fundef fdef -> DEF_fundef (rewriters.rewrite_fun rewriters fdef)
| DEF_val letbind -> DEF_val (rewriters.rewrite_let rewriters None letbind)
| DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "DEF_scattered survived to rewritter")
diff --git a/src/type_check.ml b/src/type_check.ml
index d8c4a400..e3cdb4ac 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -83,8 +83,8 @@ let rec extract_if_first recur name (Typ_aux(typ,l)) =
| None -> None)
| _ -> None
-let rec typ_to_t imp_ok fun_ok (Typ_aux(typ,l)) =
- let trans t = typ_to_t false false t in
+let rec typ_to_t envs imp_ok fun_ok (Typ_aux(typ,l)) =
+ let trans t = typ_to_t envs false false t in
match typ with
| Typ_id i -> {t = Tid (id_to_string i)}
| Typ_var (Kid_aux((Var i),l')) -> {t = Tvar i}
@@ -97,30 +97,36 @@ let rec typ_to_t imp_ok fun_ok (Typ_aux(typ,l)) =
then (match extract_if_first true "implicit" ty1 with
| Some(imp,new_ty1) -> (match imp with
| Typ_app(_,[Typ_arg_aux(Typ_arg_nexp ((Nexp_aux(n,l')) as ne),_)]) ->
- {t = Tfn (trans new_ty1, trans ty2, IP_user (anexp_to_nexp ne), aeffect_to_effect e)}
+ {t = Tfn (trans new_ty1, trans ty2, IP_user (anexp_to_nexp envs ne), aeffect_to_effect e)}
| _ -> typ_error l "Declaring an implicit parameter requires a Nat specification")
| None -> typ_error l "A function type with an implicit parameter must declare the implicit first")
else typ_error l "This function has one (or more) implicit parameter(s) not permitted here"
else {t = Tfn (trans ty1,trans ty2,IP_none,aeffect_to_effect e)}
else typ_error l "Function types are only permitted at the top level."
| Typ_tup(tys) -> {t = Ttup (List.map trans tys) }
- | Typ_app(i,args) -> {t = Tapp (id_to_string i,List.map typ_arg_to_targ args) }
+ | Typ_app(i,args) -> {t = Tapp (id_to_string i,List.map (typ_arg_to_targ envs) args) }
| Typ_wild -> new_t ()
-and typ_arg_to_targ (Typ_arg_aux(ta,l)) =
+and typ_arg_to_targ envs (Typ_arg_aux(ta,l)) =
match ta with
- | Typ_arg_nexp n -> TA_nexp (anexp_to_nexp n)
- | Typ_arg_typ t -> TA_typ (typ_to_t false false t)
+ | Typ_arg_nexp n -> TA_nexp (anexp_to_nexp envs n)
+ | Typ_arg_typ t -> TA_typ (typ_to_t envs false false t)
| Typ_arg_order o -> TA_ord (aorder_to_ord o)
| Typ_arg_effect e -> TA_eft (aeffect_to_effect e)
-and anexp_to_nexp ((Nexp_aux(n,l)) : Ast.nexp) : nexp =
+and anexp_to_nexp envs ((Nexp_aux(n,l)) : Ast.nexp) : nexp =
+ let (Env(d_env,t_env,b_env,tp_env)) = envs in
match n with
- | Nexp_var (Kid_aux((Var i),l')) -> mk_nv i
- | Nexp_constant i -> mk_c_int i
- | Nexp_times(n1,n2) -> mk_mult (anexp_to_nexp n1) (anexp_to_nexp n2)
- | Nexp_sum(n1,n2) -> mk_add (anexp_to_nexp n1) (anexp_to_nexp n2)
- | Nexp_minus(n1,n2) -> mk_sub (anexp_to_nexp n1) (anexp_to_nexp n2)
- | Nexp_exp n -> mk_2n(anexp_to_nexp n)
- | Nexp_neg n -> mk_neg(anexp_to_nexp n)
+ | Nexp_var (Kid_aux((Var i),l')) -> mk_nv i
+ | Nexp_id id ->
+ let s = id_to_string id in
+ (match Envmap.apply d_env.nabbrevs s with
+ |Some n -> n
+ | None -> typ_error l ("Unbound nat id " ^ s))
+ | Nexp_constant i -> mk_c_int i
+ | Nexp_times(n1,n2) -> mk_mult (anexp_to_nexp envs n1) (anexp_to_nexp envs n2)
+ | Nexp_sum(n1,n2) -> mk_add (anexp_to_nexp envs n1) (anexp_to_nexp envs n2)
+ | Nexp_minus(n1,n2) -> mk_sub (anexp_to_nexp envs n1) (anexp_to_nexp envs n2)
+ | Nexp_exp n -> mk_2n(anexp_to_nexp envs n)
+ | Nexp_neg n -> mk_neg(anexp_to_nexp envs n)
and aeffect_to_effect ((Effect_aux(e,l)) : Ast.effect) : effect =
match e with
| Effect_var (Kid_aux((Var i),l')) -> {effect = Evar i}
@@ -163,10 +169,13 @@ let rec quants_to_consts ((Env (d_env,t_env,b_env,tp_env)) as env) qis : (t_para
| QI_const(NC_aux(nconst,l')) ->
(*TODO: somehow the requirement vs best guarantee needs to be derived from user or context*)
(match nconst with
- | NC_fixed(n1,n2) -> (ids,typarms,Eq(Specc l',anexp_to_nexp n1,anexp_to_nexp n2)::cs)
- | NC_bounded_ge(n1,n2) -> (ids,typarms,GtEq(Specc l',Guarantee,anexp_to_nexp n1,anexp_to_nexp n2)::cs)
- | NC_bounded_le(n1,n2) -> (ids,typarms,LtEq(Specc l',Guarantee,anexp_to_nexp n1,anexp_to_nexp n2)::cs)
- | NC_nat_set_bounded(Kid_aux((Var i),l''), bounds) -> (ids,typarms,In(Specc l',i,bounds)::cs)))
+ | NC_fixed(n1,n2) ->
+ (ids,typarms,Eq(Specc l',anexp_to_nexp env n1,anexp_to_nexp env n2)::cs)
+ | NC_bounded_ge(n1,n2) ->
+ (ids,typarms,GtEq(Specc l',Guarantee,anexp_to_nexp env n1,anexp_to_nexp env n2)::cs)
+ | NC_bounded_le(n1,n2) ->
+ (ids,typarms,LtEq(Specc l',Guarantee,anexp_to_nexp env n1,anexp_to_nexp env n2)::cs)
+ | NC_nat_set_bounded(Kid_aux((Var i),l''), bounds) -> (ids,typarms,In(Specc l',i,bounds)::cs)))
let typq_to_params envs (TypQ_aux(tq,l)) =
match tq with
@@ -176,7 +185,7 @@ let typq_to_params envs (TypQ_aux(tq,l)) =
let typschm_to_tannot envs imp_parm_ok fun_ok ((TypSchm_aux(typschm,l)):typschm) (tag : tag) : tannot =
match typschm with
| TypSchm_ts(tq,typ) ->
- let t = typ_to_t imp_parm_ok fun_ok typ in
+ let t = typ_to_t envs imp_parm_ok fun_ok typ in
let (ids,_,constraints) = typq_to_params envs tq in
Base((ids,t),tag,constraints,pure_e,pure_e,nob)
@@ -247,7 +256,7 @@ let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat)
let tannot = Base(([],t),emp_tag,cs,pure_e,pure_e,bounds) in
(P_aux(P_as(pat',id),(l,tannot)),Envmap.insert env (v,tannot),cs@constraints,bounds,t)
| P_typ(typ,pat) ->
- let t = typ_to_t false false typ in
+ let t = typ_to_t envs false false typ in
let t = typ_subst tp_env false t in
let (pat',env,constraints,bounds,u) = check_pattern envs emp_tag t pat in
let t,cs_consistent = type_consistent (Patt l) d_env Guarantee false t expect_t in
@@ -616,7 +625,7 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
let t',cs',_,e' = type_coerce (Expr l) d_env Require false widen b_env (get_e_typ e) e expect_t in
(e',t',t_env,cs@cs',nob,effect)
| E_cast(typ,e) ->
- let cast_t = typ_to_t false false typ in
+ let cast_t = typ_to_t envs false false typ in
let cast_t,cs_a = get_abbrev d_env cast_t in
let cast_t = typ_subst tp_env false cast_t in
let ct = {t = Toptions(cast_t,None)} in
@@ -1338,6 +1347,10 @@ let rec check_exp envs (imp_param:nexp option) (widen:bool) (expect_t:t) (E_aux(
let (msg',mt',_,_,_,_) = check_exp envs imp_param true {t= Tapp("option",[TA_typ string_t])} msg in
let (t',c') = type_consistent (Expr l) d_env Require false unit_t expect_t in
(E_aux (E_assert(cond',msg'), (l, (simple_annot expect_t))), expect_t,t_env,c',nob,pure_e)
+ | E_comment s ->
+ (E_aux (E_comment s, (l, simple_annot unit_t)), expect_t,t_env,[],nob,pure_e)
+ | E_comment_struc e ->
+ (E_aux (E_comment_struc e, (l, simple_annot unit_t)), expect_t,t_env,[],nob,pure_e)
| E_internal_cast _ | E_internal_exp _ | E_internal_exp_user _ | E_internal_let _
| E_internal_plet _ | E_internal_return _ ->
raise (Reporting_basic.err_unreachable l "Internal expression passed back into type checker")
@@ -1523,7 +1536,7 @@ and check_lexp envs imp_param is_top (LEXP_aux(lexp,(l,annot)))
| _ -> typ_error l ("Unbound identifier " ^ i))
| LEXP_cast(typ,id) ->
let i = id_to_string id in
- let ty = typ_to_t false false typ in
+ let ty = typ_to_t envs false false typ in
let ty = typ_subst tp_env false ty in
let new_bounds = extract_bounds d_env i ty in
(match Envmap.apply t_env i with
@@ -1729,6 +1742,132 @@ and check_lbind envs imp_param is_top_level emp_tag (LB_aux(lbind,(l,annot))) :
(*let _ = Printf.eprintf "done checking tannot in let2\n" in*)
(LB_aux (LB_val_implicit(pat',e),(l,tannot)), env,cs,merge_bounds bounds b_env,ef)
+let check_record_typ envs (id: string) (typq : typquant) (fields : (Ast.typ * id) list)
+ : (tannot * (string * typ) list) =
+ let (params,typarms,constraints) = typq_to_params envs typq in
+ let ty = match typarms with | [] -> {t = Tid id} | parms -> {t = Tapp(id,parms)} in
+ let tyannot = Base((params,ty),Emp_global,constraints,pure_e,pure_e,nob) in
+ let fields' = List.map (fun (ty,i)->(id_to_string i),(typ_to_t envs false false ty)) fields in
+ (tyannot, fields')
+
+let check_variant_typ envs (id: string) typq arms =
+ let (Env(d_env,t_env,b_env,tp_env)) = envs in
+ let (params,typarms,constraints) = typq_to_params envs typq in
+ let num_arms = List.length arms in
+ let ty = match params with
+ | [] -> {t=Tid id}
+ | params -> {t = Tapp(id, typarms) }in
+ let tyannot = Base((params,ty),Constructor num_arms,constraints,pure_e,pure_e,nob) in
+ let arm_t input = Base((params,{t=Tfn(input,ty,IP_none,pure_e)}),Constructor num_arms,constraints,pure_e,pure_e,nob) in
+ let arms' = List.map
+ (fun (Tu_aux(tu,l')) ->
+ match tu with
+ | Tu_id i -> ((id_to_string i),(arm_t unit_t))
+ | Tu_ty_id(typ,i)-> ((id_to_string i),(arm_t (typ_to_t envs false false typ))))
+ arms in
+ let t_env = List.fold_right (fun (id,tann) t_env -> Envmap.insert t_env (id,tann)) arms' t_env in
+ tyannot, t_env
+
+let check_enum_type envs (id: string) ids =
+ let (Env(d_env,t_env,b_env,tp_env)) = envs in
+ let ids' = List.map id_to_string ids in
+ let max = (List.length ids') -1 in
+ let ty = Base (([],{t = Tid id }),Enum max,[],pure_e,pure_e,nob) in
+ let t_env = List.fold_right (fun id t_env -> Envmap.insert t_env (id,ty)) ids' t_env in
+ let enum_env = Envmap.insert d_env.enum_env (id,ids') in
+ ty, t_env, enum_env
+
+let check_register_type envs l (id: string) base top ranges =
+ let (Env(d_env,t_env,b_env,tp_env)) = envs in
+ let basei = normalize_nexp(anexp_to_nexp envs base) in
+ let topi = normalize_nexp(anexp_to_nexp envs top) in
+ match basei.nexp,topi.nexp with
+ | Nconst b, Nconst t ->
+ if (le_big_int b t) then (
+ let ty = {t = Tapp("vector",[TA_nexp basei; TA_nexp (mk_c(add_big_int (sub_big_int t b) (big_int_of_int 1)));
+ TA_ord({order = Oinc}); TA_typ({t = Tid "bit"});])} in
+ let rec range_to_type_inc (BF_aux(idx,l)) =
+ (match idx with
+ | BF_single i ->
+ if (le_big_int b (big_int_of_int i)) && (le_big_int (big_int_of_int i) t)
+ then {t = Tid "bit"}, i, 1
+ else typ_error l
+ ("register type declaration " ^ id ^
+ " contains a field specification outside of the declared register size")
+ | BF_range(i1,i2) ->
+ if i1<i2
+ then
+ if (le_big_int b (big_int_of_int i1)) && (le_big_int (big_int_of_int i2) t)
+ then let size = i2 - i1 + 1 in
+ ({t=Tapp("vector",[TA_nexp (mk_c_int i1); TA_nexp (mk_c_int size);
+ TA_ord({order=Oinc}); TA_typ {t=Tid "bit"}])}, i1, size)
+ else typ_error l ("register type declaration " ^ id
+ ^ " contains a field specification outside of the declared register size")
+ else typ_error l ("register type declaration " ^ id ^ " is not consistently increasing")
+ | BF_concat(bf1, bf2) ->
+ (match (range_to_type_inc bf1, range_to_type_inc bf2) with
+ | ({t = Tid "bit"}, start, size1),({t= Tid "bit"}, start2, size2)
+ | (({t = Tid "bit"}, start, size1), ({t= Tapp("vector", _)}, start2, size2))
+ | (({t=Tapp("vector", _)}, start, size1), ({t=Tid "bit"}, start2, size2))
+ | (({t=Tapp("vector",_)}, start, size1), ({t=Tapp("vector",_)}, start2, size2)) ->
+ if start < start2
+ then let size = size1 + size2 in
+ ({t=Tapp("vector", [TA_nexp (mk_c_int start); TA_nexp (mk_c_int size);
+ TA_ord({order = Oinc}); TA_typ {t=Tid"bit"}])}, start, size)
+ else typ_error l ("register type declaration " ^ id ^ " is not consistently increasing")
+ | _ -> raise (Reporting_basic.err_unreachable l "range_to_type returned something odd")))
+ in
+ let franges =
+ List.map
+ (fun (bf,id) ->
+ let (bf_t, _, _) = range_to_type_inc bf in ((id_to_string id),bf_t))
+ ranges
+ in
+ let tannot = into_register d_env (Base(([],ty),External None,[],pure_e,pure_e,nob)) in
+ tannot, franges)
+ else (
+ let ty = {t = Tapp("vector",[TA_nexp basei; TA_nexp (mk_c(add_big_int (sub_big_int b t) one));
+ TA_ord({order = Odec}); TA_typ({t = Tid "bit"});])} in
+ let rec range_to_type_dec (BF_aux(idx,l)) =
+ (match idx with
+ | BF_single i ->
+ if (ge_big_int b (big_int_of_int i)) && (ge_big_int (big_int_of_int i) t)
+ then {t = Tid "bit"}, i, 1
+ else typ_error l
+ ("register type declaration " ^ id ^
+ " contains a field specification outside of the declared register size")
+ | BF_range(i1,i2) ->
+ if i1>i2
+ then
+ if (ge_big_int b (big_int_of_int i1)) && (ge_big_int (big_int_of_int i2) t)
+ then let size = (i1 - i2) + 1 in
+ ({t=Tapp("vector",[TA_nexp (mk_c_int i1); TA_nexp (mk_c_int size);
+ TA_ord({order=Odec}); TA_typ {t=Tid "bit"}])}, i1, size)
+ else typ_error l ("register type declaration " ^ id
+ ^ " contains a field specification outside of the declared register size")
+ else typ_error l ("register type declaration " ^ id ^ " is not consistently decreasing")
+ | BF_concat(bf1, bf2) ->
+ (match (range_to_type_dec bf1, range_to_type_dec bf2) with
+ | ({t = Tid "bit"}, start, size1),({t= Tid "bit"}, start2, size2)
+ | (({t = Tid "bit"}, start, size1), ({t= Tapp("vector", _)}, start2, size2))
+ | (({t=Tapp("vector", _)}, start, size1), ({t=Tid "bit"}, start2, size2))
+ | (({t=Tapp("vector",_)}, start, size1), ({t=Tapp("vector",_)}, start2, size2)) ->
+ if start > start2
+ then let size = size1 + size2 in
+ ({t=Tapp("vector", [TA_nexp (mk_c_int start); TA_nexp (mk_c_int size);
+ TA_ord({order = Oinc}); TA_typ {t=Tid"bit"}])}, start, size)
+ else typ_error l ("register type declaration " ^ id ^ " is not consistently decreasing")
+ | _ -> raise (Reporting_basic.err_unreachable l "range_to_type has returned something odd")))
+ in
+ let franges =
+ List.map
+ (fun (bf,id) -> let (bf_t, _, _) = range_to_type_dec bf in (id_to_string id, bf_t))
+ ranges
+ in
+ let tannot = into_register d_env (Base(([],ty),External None,[],pure_e,pure_e,nob)) in
+ tannot, franges)
+ | _,_ -> raise (Reporting_basic.err_unreachable l "Nexps in register declaration do not evaluate to constants")
+
(*val check_type_def : envs -> (tannot type_def) -> (tannot type_def) envs_out*)
let check_type_def envs (TD_aux(td,(l,annot))) =
let (Env(d_env,t_env,b_env,tp_env)) = envs in
@@ -1739,130 +1878,54 @@ let check_type_def envs (TD_aux(td,(l,annot))) =
Env( { d_env with abbrevs = Envmap.insert d_env.abbrevs ((id_to_string id),tan)},t_env,b_env,tp_env))
| TD_record(id,nmscm,typq,fields,_) ->
let id' = id_to_string id in
- let (params,typarms,constraints) = typq_to_params envs typq in
- let ty = match typarms with | [] -> {t = Tid id'} | parms -> {t = Tapp(id',parms)} in
- let tyannot = Base((params,ty),Emp_global,constraints,pure_e,pure_e,nob) in
- let fields' = List.map (fun (ty,i)->(id_to_string i),(typ_to_t false false ty)) fields in
+ let (tyannot, fields') = check_record_typ envs id' typq fields in
(TD_aux(td,(l,tyannot)),Env({d_env with rec_env = (id',Record,tyannot,fields')::d_env.rec_env},t_env,b_env,tp_env))
| TD_variant(id,nmscm,typq,arms,_) ->
let id' = id_to_string id in
- let (params,typarms,constraints) = typq_to_params envs typq in
- let num_arms = List.length arms in
- let ty = match params with
- | [] -> {t=Tid id'}
- | params -> {t = Tapp(id', typarms) }in
- let tyannot = Base((params,ty),Constructor num_arms,constraints,pure_e,pure_e,nob) in
- let arm_t input = Base((params,{t=Tfn(input,ty,IP_none,pure_e)}),Constructor num_arms,constraints,pure_e,pure_e,nob) in
- let arms' = List.map
- (fun (Tu_aux(tu,l')) ->
- match tu with
- | Tu_id i -> ((id_to_string i),(arm_t unit_t))
- | Tu_ty_id(typ,i)-> ((id_to_string i),(arm_t (typ_to_t false false typ))))
- arms in
- let t_env = List.fold_right (fun (id,tann) t_env -> Envmap.insert t_env (id,tann)) arms' t_env in
+ let tyannot, t_env = check_variant_typ envs id' typq arms in
(TD_aux(td,(l,tyannot)),(Env (d_env,t_env,b_env,tp_env)))
| TD_enum(id,nmscm,ids,_) ->
let id' = id_to_string id in
- let ids' = List.map id_to_string ids in
- let max = (List.length ids') -1 in
- let ty = Base (([],{t = Tid id' }),Enum max,[],pure_e,pure_e,nob) in
- let t_env = List.fold_right (fun id t_env -> Envmap.insert t_env (id,ty)) ids' t_env in
- let enum_env = Envmap.insert d_env.enum_env (id',ids') in
+ let ty,t_env,enum_env = check_enum_type envs id' ids in
(TD_aux(td,(l,ty)),Env({d_env with enum_env = enum_env;},t_env,b_env,tp_env))
| TD_register(id,base,top,ranges) ->
let id' = id_to_string id in
- let basei = normalize_nexp(anexp_to_nexp base) in
- let topi = normalize_nexp(anexp_to_nexp top) in
- match basei.nexp,topi.nexp with
- | Nconst b, Nconst t ->
- if (le_big_int b t) then (
- let ty = {t = Tapp("vector",[TA_nexp basei; TA_nexp (mk_c(add_big_int (sub_big_int t b) (big_int_of_int 1)));
- TA_ord({order = Oinc}); TA_typ({t = Tid "bit"});])} in
- let rec range_to_type_inc (BF_aux(idx,l)) =
- (match idx with
- | BF_single i ->
- if (le_big_int b (big_int_of_int i)) && (le_big_int (big_int_of_int i) t)
- then {t = Tid "bit"}, i, 1
- else typ_error l
- ("register type declaration " ^ id' ^
- " contains a field specification outside of the declared register size")
- | BF_range(i1,i2) ->
- if i1<i2
- then
- if (le_big_int b (big_int_of_int i1)) && (le_big_int (big_int_of_int i2) t)
- then let size = i2 - i1 + 1 in
- ({t=Tapp("vector",[TA_nexp (mk_c_int i1); TA_nexp (mk_c_int size);
- TA_ord({order=Oinc}); TA_typ {t=Tid "bit"}])}, i1, size)
- else typ_error l ("register type declaration " ^ id'
- ^ " contains a field specification outside of the declared register size")
- else typ_error l ("register type declaration " ^ id' ^ " is not consistently increasing")
- | BF_concat(bf1, bf2) ->
- (match (range_to_type_inc bf1, range_to_type_inc bf2) with
- | ({t = Tid "bit"}, start, size1),({t= Tid "bit"}, start2, size2)
- | (({t = Tid "bit"}, start, size1), ({t= Tapp("vector", _)}, start2, size2))
- | (({t=Tapp("vector", _)}, start, size1), ({t=Tid "bit"}, start2, size2))
- | (({t=Tapp("vector",_)}, start, size1), ({t=Tapp("vector",_)}, start2, size2)) ->
- if start < start2
- then let size = size1 + size2 in
- ({t=Tapp("vector", [TA_nexp (mk_c_int start); TA_nexp (mk_c_int size);
- TA_ord({order = Oinc}); TA_typ {t=Tid"bit"}])}, start, size)
- else typ_error l ("register type declaration " ^ id' ^ " is not consistently increasing")
- | _ -> raise (Reporting_basic.err_unreachable l "range_to_type returned something odd")))
- in
- let franges =
- List.map
- (fun (bf,id) ->
- let (bf_t, _, _) = range_to_type_inc bf in ((id_to_string id),bf_t))
- ranges
- in
- let tannot = into_register d_env (Base(([],ty),External None,[],pure_e,pure_e,nob)) in
- (TD_aux(td,(l,tannot)),
- Env({d_env with rec_env = ((id',Register,tannot,franges)::d_env.rec_env);
- abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env,b_env,tp_env)))
- else (
- let ty = {t = Tapp("vector",[TA_nexp basei; TA_nexp (mk_c(add_big_int (sub_big_int b t) one));
- TA_ord({order = Odec}); TA_typ({t = Tid "bit"});])} in
- let rec range_to_type_dec (BF_aux(idx,l)) =
- (match idx with
- | BF_single i ->
- if (ge_big_int b (big_int_of_int i)) && (ge_big_int (big_int_of_int i) t)
- then {t = Tid "bit"}, i, 1
- else typ_error l
- ("register type declaration " ^ id' ^
- " contains a field specification outside of the declared register size")
- | BF_range(i1,i2) ->
- if i1>i2
- then
- if (ge_big_int b (big_int_of_int i1)) && (ge_big_int (big_int_of_int i2) t)
- then let size = (i1 - i2) + 1 in
- ({t=Tapp("vector",[TA_nexp (mk_c_int i1); TA_nexp (mk_c_int size);
- TA_ord({order=Odec}); TA_typ {t=Tid "bit"}])}, i1, size)
- else typ_error l ("register type declaration " ^ id'
- ^ " contains a field specification outside of the declared register size")
- else typ_error l ("register type declaration " ^ id' ^ " is not consistently decreasing")
- | BF_concat(bf1, bf2) ->
- (match (range_to_type_dec bf1, range_to_type_dec bf2) with
- | ({t = Tid "bit"}, start, size1),({t= Tid "bit"}, start2, size2)
- | (({t = Tid "bit"}, start, size1), ({t= Tapp("vector", _)}, start2, size2))
- | (({t=Tapp("vector", _)}, start, size1), ({t=Tid "bit"}, start2, size2))
- | (({t=Tapp("vector",_)}, start, size1), ({t=Tapp("vector",_)}, start2, size2)) ->
- if start > start2
- then let size = size1 + size2 in
- ({t=Tapp("vector", [TA_nexp (mk_c_int start); TA_nexp (mk_c_int size);
- TA_ord({order = Oinc}); TA_typ {t=Tid"bit"}])}, start, size)
- else typ_error l ("register type declaration " ^ id' ^ " is not consistently decreasing")
- | _ -> raise (Reporting_basic.err_unreachable l "range_to_type has returned something odd")))
- in
- let franges =
- List.map
- (fun (bf,id) -> let (bf_t, _, _) = range_to_type_dec bf in (id_to_string id, bf_t))
- ranges
- in
- let tannot = into_register d_env (Base(([],ty),External None,[],pure_e,pure_e,nob)) in
- (TD_aux(td,(l,tannot)),
- Env({d_env with rec_env = (id',Register,tannot,franges)::d_env.rec_env;
- abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env,b_env,tp_env)))
- | _,_ -> raise (Reporting_basic.err_unreachable l "Nexps in register declaration do not evaluate to constants")
+ let (tannot, franges) = check_register_type envs l id' base top ranges in
+ (TD_aux(td,(l,tannot)),
+ Env({d_env with rec_env = ((id',Register,tannot,franges)::d_env.rec_env);
+ abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env,b_env,tp_env))
+
+(*val check_kind_def : envs -> (tannot kind_def) -> (tannot kind_def) envs_out*)
+let check_kind_def envs (KD_aux(kd,(l,annot))) =
+ let (Env(d_env,t_env,b_env,tp_env)) = envs in
+ match kd with
+ | KD_nabbrev(kind,id,nmscm,n) ->
+ let id' = id_to_string id in
+ let n = normalize_nexp (anexp_to_nexp envs n) in
+ (KD_aux(kd,(l,annot)),
+ Env( { d_env with nabbrevs = Envmap.insert d_env.nabbrevs (id', (mk_nid id' n))},t_env,b_env,tp_env))
+ | KD_abbrev(kind,id,nmscm,typschm) ->
+ let tan = typschm_to_tannot envs false false typschm Emp_global in
+ (KD_aux(kd,(l,tan)),
+ Env( { d_env with abbrevs = Envmap.insert d_env.abbrevs ((id_to_string id),tan)},t_env,b_env,tp_env))
+ | KD_record(kind,id,nmscm,typq,fields,_) ->
+ let id' = id_to_string id in
+ let (tyannot, fields') = check_record_typ envs id' typq fields in
+ (KD_aux(kd,(l,tyannot)),Env({d_env with rec_env = (id',Record,tyannot,fields')::d_env.rec_env},t_env,b_env,tp_env))
+ | KD_variant(kind,id,nmscm,typq,arms,_) ->
+ let id' = id_to_string id in
+ let tyannot, t_env = check_variant_typ envs id' typq arms in
+ (KD_aux(kd,(l,tyannot)),(Env (d_env,t_env,b_env,tp_env)))
+ | KD_enum(kind,id,nmscm,ids,_) ->
+ let id' = id_to_string id in
+ let ty,t_env,enum_env = check_enum_type envs id' ids in
+ (KD_aux(kd,(l,ty)),Env({d_env with enum_env = enum_env;},t_env,b_env,tp_env))
+ | KD_register(kind,id,base,top,ranges) ->
+ let id' = id_to_string id in
+ let (tannot, franges) = check_register_type envs l id' base top ranges in
+ (KD_aux(kd,(l,tannot)),
+ Env({d_env with rec_env = ((id',Register,tannot,franges)::d_env.rec_env);
+ abbrevs = Envmap.insert d_env.abbrevs (id',tannot)},t_env,b_env,tp_env))
let check_val_spec envs (VS_aux(vs,(l,annot))) =
let (Env(d_env,t_env,b_env,tp_env)) = envs in
@@ -1914,7 +1977,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
let ret_t,param_t,tannot,t_param_env = match tannotopt with
| Typ_annot_opt_aux(Typ_annot_opt_some(typq,typ),l') ->
let (ids,_,constraints) = typq_to_params envs typq in
- let t = typ_to_t false false typ in
+ let t = typ_to_t envs false false typ in
(*TODO add check that ids == typ_params when has_spec*)
let t,constraints,_,t_param_env = subst (if has_spec then typ_params else ids) true t constraints pure_e in
let p_t = new_t () in
@@ -2076,6 +2139,11 @@ let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
let check_def envs def =
let (Env(d_env,t_env,b_env,tp_env)) = envs in
match def with
+ | DEF_kind kdef ->
+ (*let _ = Printf.eprintf "checking kind def\n" in*)
+ let kd,envs = check_kind_def envs kdef in
+ (*let _ = Printf.eprintf "checked kind def\n" in*)
+ (DEF_kind kd,envs)
| DEF_type tdef ->
(*let _ = Printf.eprintf "checking type def\n" in*)
let td,envs = check_type_def envs tdef in
@@ -2100,7 +2168,7 @@ let check_def envs def =
(DEF_default ds,envs)
| DEF_reg_dec(DEC_aux(DEC_reg(typ,id), (l,annot))) ->
(*let _ = Printf.eprintf "checking reg dec\n" in *)
- let t = (typ_to_t false false typ) in
+ let t = (typ_to_t envs false false typ) in
let i = id_to_string id in
let tannot = into_register d_env (Base(([],t),External (Some i),[],pure_e,pure_e,nob)) in
(*let _ = Printf.eprintf "done checking reg dec\n" in*)
@@ -2114,11 +2182,12 @@ let check_def envs def =
| DEF_reg_dec(DEC_aux(DEC_typ_alias(typ,id,aspec),(l,tannot))) ->
(*let _ = Printf.eprintf "checking reg dec c\n" in*)
let i = id_to_string id in
- let t = typ_to_t false false typ in
+ let t = typ_to_t envs false false typ in
let (aspec,tannot,d_env) = check_alias_spec envs i aspec (Some t) in
(*let _ = Printf.eprintf "done checking reg dec c\n" in*)
(DEF_reg_dec(DEC_aux(DEC_typ_alias(typ,id,aspec),(l,tannot))),(Env(d_env,Envmap.insert t_env (i,tannot),b_env,tp_env)))
| DEF_scattered _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "Scattered given to type checker")
+ | _ -> def,envs (*Else a comment, so skip but keep*)
(*val check : envs -> tannot defs -> tannot defs*)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index a48e7b85..5da8b40b 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -41,6 +41,7 @@ and implicit_parm =
and nexp = { mutable nexp : nexp_aux; mutable imp_param : bool}
and nexp_aux =
| Nvar of string
+ | Nid of string * nexp (*First term is the name of this nid, second is the constant it represents*)
| Nconst of big_int
| Npos_inf
| Nneg_inf
@@ -98,6 +99,12 @@ let rec compare_nexps n1 n2 =
| Nconst n1, Nconst n2 -> compare_big_int n1 n2
| Nconst _ , _ -> -1
| _ , Nconst _ -> 1
+ | Nid(i1,n1), Nid(i2,n2) ->
+ (match compare i1 i2 with
+ | 0 -> 0
+ | _ -> compare_nexps n1 n2)
+ | Nid _ , _ -> -1
+ | _ , Nid _ -> 1
| Nvar i1 , Nvar i2 -> compare i1 i2
| Nvar _ , _ -> -1
| _ , Nvar _ -> 1
@@ -197,7 +204,8 @@ type rec_env = (string * rec_kind * tannot * ((string * t) list))
type alias_kind = OneReg of string * tannot | TwoReg of string * string * tannot | MultiReg of (string list) * tannot
type def_envs = {
k_env: kind emap;
- abbrevs: tannot emap;
+ abbrevs: tannot emap;
+ nabbrevs: nexp emap;
namesch : tannot emap;
enum_env : (string list) emap;
rec_env : rec_env list;
@@ -216,6 +224,7 @@ type exp = tannot Ast.exp
(*Nexpression Makers (as built so often)*)
let mk_nv s = {nexp = Nvar s; imp_param = false}
+let mk_nid s n = {nexp = Nid(s,n); imp_param = false}
let mk_add n1 n2 = {nexp = Nadd(n1,n2); imp_param = false}
let mk_sub n1 n2 = {nexp = Nsub(n1,n2); imp_param = false}
let mk_mult n1 n2 = {nexp = Nmult(n1,n2); imp_param = false}
@@ -285,19 +294,23 @@ and targ_to_string = function
| TA_ord o -> o_to_string o
and n_to_string n =
match n.nexp with
- | Nvar i -> i
- | Nconst i -> string_of_big_int i
- | Npos_inf -> "infinity"
- | Nneg_inf -> "-infinity"
- | Ninexact -> "infinity - infinity"
- | Nadd(n1,n2) -> "("^ (n_to_string n1) ^ " + " ^ (n_to_string n2) ^")"
- | Nsub(n1,n2) -> "("^ (n_to_string n1) ^ " - " ^ (n_to_string n2) ^ ")"
- | Nmult(n1,n2) -> "(" ^ (n_to_string n1) ^ " * " ^ (n_to_string n2) ^ ")"
- | N2n(n,None) -> "2**" ^ (n_to_string n)
- | N2n(n,Some i) -> "2**" ^ (n_to_string n) ^ "(*" ^ (string_of_big_int i) ^ "*)"
- | Npow(n, i) -> "(" ^ (n_to_string n) ^ ")**" ^ (string_of_int i)
- | Nneg n -> "-" ^ (n_to_string n)
- | Nuvar({nindex=i;nsubst=a}) -> if !debug_mode then "Nu_" ^ string_of_int i ^ "(" ^ (match a with | None -> "None" | Some n -> n_to_string n) ^ ")" else "_"
+ | Nid(i,n) -> i ^ "(*" ^ (n_to_string n) ^ "*)"
+ | Nvar i -> i
+ | Nconst i -> string_of_big_int i
+ | Npos_inf -> "infinity"
+ | Nneg_inf -> "-infinity"
+ | Ninexact -> "infinity - infinity"
+ | Nadd(n1,n2) -> "("^ (n_to_string n1) ^ " + " ^ (n_to_string n2) ^")"
+ | Nsub(n1,n2) -> "("^ (n_to_string n1) ^ " - " ^ (n_to_string n2) ^ ")"
+ | Nmult(n1,n2) -> "(" ^ (n_to_string n1) ^ " * " ^ (n_to_string n2) ^ ")"
+ | N2n(n,None) -> "2**" ^ (n_to_string n)
+ | N2n(n,Some i) -> "2**" ^ (n_to_string n) ^ "(*" ^ (string_of_big_int i) ^ "*)"
+ | Npow(n, i) -> "(" ^ (n_to_string n) ^ ")**" ^ (string_of_int i)
+ | Nneg n -> "-" ^ (n_to_string n)
+ | Nuvar({nindex=i;nsubst=a}) ->
+ if !debug_mode
+ then "Nu_" ^ string_of_int i ^ "(" ^ (match a with | None -> "None" | Some n -> n_to_string n) ^ ")"
+ else "_"
and ef_to_string (Ast.BE_aux(b,l)) =
match b with
| Ast.BE_rreg -> "rreg"
@@ -489,7 +502,7 @@ let is_bit_vector t = match t.t with
let rec contains_const n =
match n.nexp with
| Nvar _ | Nuvar _ | Npow _ | N2n _ | Npos_inf | Nneg_inf | Ninexact -> false
- | Nconst _ -> true
+ | Nconst _ | Nid _ -> true
| Nneg n -> contains_const n
| Nmult(n1,n2) | Nadd(n1,n2) | Nsub(n1,n2) -> (contains_const n1) || (contains_const n2)
@@ -582,6 +595,7 @@ let rec nexp_negative n =
let rec normalize_n_rec recur_ok n =
(*let _ = Printf.eprintf "Working on normalizing %s\n" (n_to_string n) in *)
match n.nexp with
+ | Nid(_,n) -> normalize_n_rec true n
| Nconst _ | Nvar _ | Nuvar _ | Npos_inf | Nneg_inf | Ninexact -> n
| Nneg n ->
let n',to_recur,add_neg = (match n.nexp with
@@ -819,9 +833,11 @@ let rec normalize_n_rec recur_ok n =
| _ -> mk_mult (normalize_n_rec true (mk_mult n1' n21)) n22)
| Nmult _ ,Nmult(n21,n22) -> mk_mult (mk_mult n21 n1') (mk_mult n22 n1')
| Nsub _, _ | _, Nsub _ ->
- let _ = Printf.eprintf "nsub case still around %s\n" (n_to_string n) in assert false
+ let _ = Printf.eprintf "nsub case still around %s\n" (n_to_string n) in assert false
| Nneg _,_ | _,Nneg _ ->
let _ = Printf.eprintf "neg case still around %s\n" (n_to_string n) in assert false
+ | Nid _, _ | _, Nid _ ->
+ let _ = Printf.eprintf "nid case still around %s\n" (n_to_string n) in assert false
(* If things are normal, neg should be gone. *)
)
@@ -1029,7 +1045,7 @@ let divisible_by ne n =
(match num with
| Some i -> eq_big_int i (big_int_of_int 2)
| _ -> false)
- | Npow(n,_) | Nneg n -> walk_nexp n
+ | Npow(n,_) | Nneg n | Nid(_,n) -> walk_nexp n
| Nmult(n1,n2) -> walk_nexp n1 || walk_nexp n2
| Nadd(n1,n2) | Nsub(n1,n2) -> walk_nexp n1 && walk_nexp n2
in walk_nexp ne
@@ -1051,6 +1067,7 @@ let divide_by ne n =
| Some answer -> answer
| None ->
let rec walk_nexp n = match n.nexp with
+ | Nid(_,n) -> walk_nexp n
| Npos_inf ->
(match num with
| Some(i) -> if lt_big_int i zero_big_int then mk_n_inf() else n
@@ -1099,6 +1116,7 @@ let isolate_nexp nv ne =
| Nuvar _ -> None, Some (get_index nv)
| _ -> None, None in
let rec remove_from ne = match ne.nexp with
+ | Nid(_,n) -> remove_from n
| Npos_inf | Nneg_inf | Ninexact | Nconst _ | N2n(_,Some _)-> ne,None
| Nvar v ->
(match var with
@@ -1130,7 +1148,7 @@ let isolate_nexp nv ne =
| None -> assert false (*Oh my*)
| Some n_nv ->
(match n_nv.nexp with
- | Nvar _ | Nuvar _ | N2n _ | Npow _ | Nadd _ | Nneg _ | Nsub _ -> (n_nv,new_ne)
+ | Nvar _ | Nuvar _ | N2n _ | Npow _ | Nadd _ | Nneg _ | Nsub _ | Nid _ -> (n_nv,new_ne)
| Nconst _ | Ninexact | Npos_inf | Nneg_inf -> assert false (*double oh my*)
| Nmult(n1,n2) ->
if nexp_eq n1 n_nv
@@ -1239,7 +1257,7 @@ let rec occurs_in_pending_subst n_box n : bool =
else occurs_in_pending_subst n' n
| Nuvar( { nsubst = None } ) ->
(match n.nexp with
- | Nuvar( { nsubst = None }) | Nvar _ | Nconst _ | Npos_inf | Nneg_inf | Ninexact -> false
+ | Nuvar( { nsubst = None }) | Nvar _ | Nid _| Nconst _ | Npos_inf | Nneg_inf | Ninexact -> false
| Nadd(n1,n2) | Nsub(n1,n2) | Nmult(n1,n2) -> occurs_in_nexp n_box n1 || occurs_in_nexp n_box n2
| Nneg n1 | N2n(n1,_) | Npow(n1,_) -> occurs_in_nexp n_box n1
| Nuvar( { nsubst = Some n'}) -> occurs_in_pending_subst n_box n')
@@ -1258,7 +1276,7 @@ and occurs_in_nexp n_box nuvar : bool =
let rec reduce_n_unifications n =
(*let _ = Printf.eprintf "reduce_n_unifications %s\n" (n_to_string n) in*)
(match n.nexp with
- | Nvar _ | Nconst _ | Npos_inf | Nneg_inf | Ninexact-> ()
+ | Nvar _ | Nid _ | Nconst _ | Npos_inf | Nneg_inf | Ninexact-> ()
| N2n(n1,_) | Npow(n1,_) | Nneg n1 -> reduce_n_unifications n1
| Nadd(n1,n2) | Nsub(n1,n2) | Nmult(n1,n2) -> reduce_n_unifications n1; reduce_n_unifications n2
| Nuvar nu ->
@@ -2380,6 +2398,7 @@ and n_subst s_env n =
(match Envmap.apply s_env i with
| Some(TA_nexp n1) -> n1
| _ -> mk_nv i)
+ | Nid(i,n) -> n_subst s_env n
| Nuvar _ -> new_n()
| Nconst _ | Npos_inf | Nneg_inf | Ninexact -> n
| N2n(n1,None) -> mk_2n (n_subst s_env n1)
@@ -2493,7 +2512,7 @@ and ta_remove_unifications s_env ta =
and n_remove_unifications s_env n =
(*let _ = Printf.eprintf "n_remove_unifications %s\n" (n_to_string n) in*)
match n.nexp with
- | Nvar _ | Nconst _ | Npos_inf | Nneg_inf | Ninexact -> s_env
+ | Nvar _ | Nid _ | Nconst _ | Npos_inf | Nneg_inf | Ninexact -> s_env
| Nuvar nu ->
let n' = match nu.nsubst with
| None -> n
@@ -2552,20 +2571,21 @@ and targ_to_typ_arg targ =
| TA_eft e -> Typ_arg_effect (e_to_ef e)), Parse_ast.Unknown)
and n_to_nexp n =
Nexp_aux(
- (match n.nexp with
- | Nvar i -> Nexp_var (Kid_aux((Var i),Parse_ast.Unknown))
- | Nconst i -> Nexp_constant (int_of_big_int i) (*TODO: Push more bigint around*)
- | Npos_inf -> Nexp_constant max_int (*TODO: Not right*)
- | Nneg_inf -> Nexp_constant min_int (* see above *)
- | Ninexact -> Nexp_constant min_int (*and above*)
- | Nmult(n1,n2) -> Nexp_times(n_to_nexp n1,n_to_nexp n2)
- | Nadd(n1,n2) -> Nexp_sum(n_to_nexp n1,n_to_nexp n2)
- | Nsub(n1,n2) -> Nexp_minus(n_to_nexp n1,n_to_nexp n2)
- | N2n(n,_) -> Nexp_exp (n_to_nexp n)
- | Npow(n,1) -> let Nexp_aux(n',_) = n_to_nexp n in n'
- | Npow(n,i) -> Nexp_times(n_to_nexp n,n_to_nexp( mk_pow n (i-1)))
- | Nneg n -> Nexp_neg (n_to_nexp n)
- | Nuvar _ -> Nexp_var (Kid_aux((Var "fresh"),Parse_ast.Unknown))), Parse_ast.Unknown)
+ (match n.nexp with
+ | Nid(i,_) -> Nexp_id (Id_aux ((Id i),Parse_ast.Unknown))
+ | Nvar i -> Nexp_var (Kid_aux((Var i),Parse_ast.Unknown))
+ | Nconst i -> Nexp_constant (int_of_big_int i) (*TODO: Push more bigint around*)
+ | Npos_inf -> Nexp_constant max_int (*TODO: Not right*)
+ | Nneg_inf -> Nexp_constant min_int (* see above *)
+ | Ninexact -> Nexp_constant min_int (*and above*)
+ | Nmult(n1,n2) -> Nexp_times(n_to_nexp n1,n_to_nexp n2)
+ | Nadd(n1,n2) -> Nexp_sum(n_to_nexp n1,n_to_nexp n2)
+ | Nsub(n1,n2) -> Nexp_minus(n_to_nexp n1,n_to_nexp n2)
+ | N2n(n,_) -> Nexp_exp (n_to_nexp n)
+ | Npow(n,1) -> let Nexp_aux(n',_) = n_to_nexp n in n'
+ | Npow(n,i) -> Nexp_times(n_to_nexp n,n_to_nexp( mk_pow n (i-1)))
+ | Nneg n -> Nexp_neg (n_to_nexp n)
+ | Nuvar _ -> Nexp_var (Kid_aux((Var "fresh"),Parse_ast.Unknown))), Parse_ast.Unknown)
and e_to_ef ef =
Effect_aux(
(match ef.effect with
@@ -2758,7 +2778,7 @@ let get_map_tannot = function
let rec expand_nexp n = match n.nexp with
| Nvar _ | Nconst _ | Nuvar _ | Npos_inf | Nneg_inf | Ninexact -> [n]
| Nadd (n1,n2) | Nsub (n1,n2) | Nmult (n1,n2) -> n::((expand_nexp n1)@(expand_nexp n2))
- | N2n (n1,_) | Npow (n1,_) | Nneg n1 -> n::(expand_nexp n1)
+ | N2n (n1,_) | Npow (n1,_) | Nneg n1 | Nid(_,n1) -> n::(expand_nexp n1)
let is_nconst n = match n.nexp with | Nconst _ -> true | _ -> false
@@ -3257,7 +3277,7 @@ let rec contains_var nu n =
| Nvar _ | Nuvar _ -> nexp_eq_check nu n
| Nconst _ | Npos_inf | Nneg_inf | Ninexact -> false
| Nadd(n1,n2) | Nsub(n1,n2) | Nmult(n1,n2) -> contains_var nu n1 || contains_var nu n2
- | Nneg n | N2n(n,_) | Npow(n,_) -> contains_var nu n
+ | Nneg n | N2n(n,_) | Npow(n,_) | Nid(_,n) -> contains_var nu n
let rec contains_in_vars in_env n =
match in_env with
@@ -3269,7 +3289,7 @@ let rec contains_in_vars in_env n =
let rec get_nuvars n =
match n.nexp with
- | Nconst _ | Nvar _ | Npos_inf | Nneg_inf | Ninexact-> []
+ | Nconst _ | Nvar _ | Nid _ | Npos_inf | Nneg_inf | Ninexact-> []
| Nuvar _ -> [n]
| Nmult(n1,n2) | Nadd(n1,n2) | Nsub(n1,n2) -> (get_nuvars n1)@(get_nuvars n2)
| Nneg n | N2n(n,_) | Npow(n,_) -> get_nuvars n
@@ -3296,7 +3316,7 @@ let rec subst_nuvars nus n =
let is_imp_param = n.imp_param in
let new_n =
match n.nexp with
- | Nconst _ | Nvar _ | Npos_inf | Nneg_inf | Ninexact -> n
+ | Nconst _ | Nvar _ | Nid _ | Npos_inf | Nneg_inf | Ninexact -> n
| Nuvar _ ->
(match Nexpmap.apply nus n with
| None -> n
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 17f4f2ff..4d1879fa 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -48,6 +48,7 @@ and implicit_parm =
and nexp = { mutable nexp : nexp_aux ; mutable imp_param : bool}
and nexp_aux =
| Nvar of string
+ | Nid of string * nexp
| Nconst of big_int
| Npos_inf (* Used to define nat and int types, does not arise from source otherwise *)
| Nneg_inf (* Used to define int type, does not arise from source otherwise *)
@@ -131,6 +132,7 @@ val n_zero : nexp
val n_one : nexp
val n_two : nexp
val mk_nv : string -> nexp
+val mk_nid : string -> nexp -> nexp
val mk_add : nexp -> nexp -> nexp
val mk_sub : nexp -> nexp -> nexp
val mk_mult : nexp -> nexp -> nexp
@@ -175,7 +177,8 @@ type rec_env = (string * rec_kind * tannot * ((string * t) list))
type alias_kind = OneReg of string * tannot | TwoReg of string * string * tannot | MultiReg of (string list) * tannot
type def_envs = {
k_env: kind emap;
- abbrevs: tannot emap;
+ abbrevs: tannot emap;
+ nabbrevs: nexp emap;
namesch : tannot emap;
enum_env : (string list) emap;
rec_env : rec_env list;
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 18:40:29 +0000