summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
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 12:03:52 +0000