From 9d6875ba4147e3f52b3251bab77e52df03257aa3 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Wed, 2 Mar 2016 17:04:09 +0000 Subject: Add new language feature to permit definitions of items of kind Nat, etc as well as items of kind Type. Syntax for the feature is: def Nat id = nexp Note: some useful nexps may not parse properly. All typedef forms can also be used as def Type ... if desired, but this is not required. --- language/l2.lem | 139 +++++++++-------- language/l2.ml | 151 ++++++++++-------- language/l2.ott | 24 ++- language/l2_parse.ml | 165 +++++++++++--------- language/l2_parse.ott | 18 +++ language/manual.pdf | Bin 342551 -> 342588 bytes language/manual.tex | 2 +- src/initial_check.ml | 106 +++++++++++-- src/initial_check_full_ast.ml | 89 ++++++++++- src/parser.mly | 42 ++++- src/pre_lexer.mll | 1 + src/pre_parser.mly | 6 +- src/pretty_print.ml | 174 ++++++++++++++++++--- src/process_file.ml | 3 +- src/rewriter.ml | 260 +++++++++++++++---------------- src/type_check.ml | 351 +++++++++++++++++++++++++----------------- src/type_internal.ml | 98 +++++++----- src/type_internal.mli | 5 +- 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 @@ -24,6 +24,12 @@ base_kind = BK_aux of base_kind_aux * l +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 @@ -34,6 +40,11 @@ kind_aux = (* kinds *) K_kind of (base_kind) list +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 *) @@ -87,12 +99,6 @@ order_aux = (* vector order specifications, of kind Order *) | Ord_dec (* decreasing (big-endian) *) -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 @@ -104,11 +110,6 @@ order = Ord_aux of order_aux * l -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 @@ -365,6 +361,11 @@ rec_opt_aux = (* Optional recursive annotation for functions *) | Rec_rec (* recursive *) +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 @@ -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 @@ -488,18 +509,14 @@ type DEC_aux of 'a dec_spec_aux * 'a annot -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 @@ -30,17 +30,6 @@ base_kind = BK_aux of base_kind_aux * l -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 *) @@ -57,14 +46,25 @@ base_effect_aux = (* effect *) | BE_escape +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 @@ -145,6 +145,11 @@ typquant_aux = (* type quantifiers and constraints *) | TypQ_no_forall (* sugar, omitting quantifier and constraints *) +type +typquant = + TypQ_aux of typquant_aux * l + + type lit_aux = (* Literal constant *) L_unit (* $() : _$ *) @@ -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 @@ -199,11 +204,6 @@ and fpat = FP_aux of fpat_aux * l -type -typschm = - TypSchm_aux of typschm_aux * l - - type exp_aux = (* Expression *) E_block of (exp) list (* block (parsing conflict with structs?) *) @@ -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 @@ -410,19 +434,10 @@ scattered_def = SD_aux of scattered_def_aux * l -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 Binary files a/language/manual.pdf and b/language/manual.pdf 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 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 + (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 - (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; -- cgit v1.2.3