summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKathy Gray2013-11-22 15:11:46 +0000
committerKathy Gray2013-11-22 15:12:04 +0000
commit994df0138776a9151b52c1210d4b0e57aafb4ced (patch)
tree9e396429d8522bf4805a3b8725f30d6d5c2de7e7
parent81ccd74f0cc1dbd7bacbeadd86250edf7d6b244a (diff)
Syntax changes per discussions on Thursday.
First pass parser to identify type names is in progress (current test files fail, will correct once pre-parser is in place)
Diffstat
-rw-r--r--language/l2.lem87
-rw-r--r--language/l2.ml118
-rw-r--r--language/l2.ott130
-rw-r--r--language/l2_parse.ml68
-rw-r--r--language/l2_parse.ott32
-rw-r--r--src/initial_check.ml14
-rw-r--r--src/lem_interp/interp.lem6
-rw-r--r--src/lexer.mll247
-rw-r--r--src/parser.mly236
-rw-r--r--src/pre_lexer.mll319
-rw-r--r--src/pre_parser.mly86
-rw-r--r--src/pretty_print.ml18
-rw-r--r--src/type_check.mli9
-rw-r--r--src/type_internal.ml8
-rw-r--r--src/type_internal.mli8
15 files changed, 846 insertions, 540 deletions
diff --git a/language/l2.lem b/language/l2.lem
index 926706a0..79cb82b3 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -1,4 +1,5 @@
(* generated by Ott 0.22 from: l2.ott *)
+open import Pervasives
open import Map
open import Maybe
@@ -21,20 +22,16 @@ val subst : forall 'a. list 'a -> list 'a -> bool
type x = string (* identifier *)
type ix = string (* infix identifier *)
-type base_kind = (* base kind *)
- | BK_type (* kind of types *)
- | BK_nat (* kind of natural number size expressions *)
- | BK_order (* kind of vector order specifications *)
- | BK_effects (* kind of effect sets *)
-
-
type id = (* Identifier *)
| Id of x
| DeIid of x (* remove infix status *)
-type kind = (* kinds *)
- | K_kind of list base_kind
+type base_kind = (* base kind *)
+ | BK_type (* kind of types *)
+ | BK_nat (* kind of natural number size expressions *)
+ | BK_order (* kind of vector order specifications *)
+ | BK_effects (* kind of effect sets *)
type nexp = (* expression of kind $Nat$, for vector sizes and origins *)
@@ -45,6 +42,10 @@ type nexp = (* expression of kind $Nat$, for vector sizes and origins *)
| Nexp_exp of nexp (* exponential *)
+type kind = (* kinds *)
+ | K_kind of list base_kind
+
+
type efct = (* effect *)
| Effect_rreg (* read register *)
| Effect_wreg (* write register *)
@@ -55,11 +56,6 @@ type efct = (* effect *)
| Effect_nondet (* nondeterminism from intra-instruction parallelism *)
-type kinded_id = (* optionally kind-annotated identifier *)
- | KOpt_none of id (* identifier *)
- | KOpt_kind of kind * id (* kind-annotated variable *)
-
-
type nexp_constraint = (* constraint over kind $Nat$ *)
| NC_fixed of nexp * nexp
| NC_bounded_ge of nexp * nexp
@@ -67,6 +63,11 @@ type nexp_constraint = (* constraint over kind $Nat$ *)
| NC_nat_set_bounded of id * list nat
+type kinded_id = (* optionally kind-annotated identifier *)
+ | KOpt_none of id (* identifier *)
+ | KOpt_kind of kind * id (* kind-annotated variable *)
+
+
type effects = (* effect set, of kind $Effects$ *)
| Effects_var of id
| Effects_set of list efct (* effect set *)
@@ -83,6 +84,19 @@ type quant_item = (* Either a kinded identifier or a nexp constraint for a typq
| QI_const of nexp_constraint (* A constraint for this type *)
+type lit = (* Literal constant *)
+ | L_unit (* $() : unit$ *)
+ | L_zero (* $bitzero : bit$ *)
+ | L_one (* $bitone : bit$ *)
+ | L_true (* $true : bool$ *)
+ | L_false (* $false : bool$ *)
+ | L_num of nat (* natural number constant *)
+ | L_hex of string (* bit vector constant, C-style *)
+ | L_bin of string (* bit vector constant, C-style *)
+ | L_undef (* constant representing undefined values *)
+ | L_string of string (* string constant *)
+
+
type typ = (* Type expressions, of kind $Type$ *)
| Typ_wild (* Unspecified type *)
| Typ_var of id (* Type variable *)
@@ -97,19 +111,6 @@ and typ_arg = (* Type constructor arguments of all kinds *)
| Typ_arg_effects of effects
-type lit = (* Literal constant *)
- | L_unit (* $() : unit$ *)
- | L_zero (* $bitzero : bit$ *)
- | L_one (* $bitone : bit$ *)
- | L_true (* $true : bool$ *)
- | L_false (* $false : bool$ *)
- | L_num of nat (* natural number constant *)
- | L_hex of string (* bit vector constant, C-style *)
- | L_bin of string (* bit vector constant, C-style *)
- | L_undef (* constant representing undefined values *)
- | L_string of string (* string constant *)
-
-
type typquant = (* type quantifiers and constraints *)
| TypQ_tq of list quant_item
| TypQ_no_forall (* sugar, omitting quantifier and constraints *)
@@ -142,7 +143,7 @@ type exp = (* Expression *)
| E_id of id (* identifier *)
| E_lit of lit (* literal constant *)
| E_cast of typ * exp (* cast *)
- | E_app of exp * list exp (* function application *)
+ | E_app of id * list exp (* function application *)
| E_app_infix of exp * id * exp (* infix function application *)
| E_tuple of list exp (* tuple *)
| E_if of exp * exp * exp (* conditional *)
@@ -183,10 +184,6 @@ and letbind = (* Let binding *)
| LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
-type tannot_opt = (* Optional type annotation for functions *)
- | Typ_annot_opt_some of typquant * typ
-
-
type funcl = (* Function clause *)
| FCL_Funcl of id * pat * exp
@@ -201,6 +198,15 @@ type rec_opt = (* Optional recursive annotation for functions *)
| Rec_rec (* recursive *)
+type tannot_opt = (* Optional type annotation for functions *)
+ | Typ_annot_opt_some of typquant * typ
+
+
+type type_union = (* Type union constructors *)
+ | Tu_id of id
+ | Tu_ty_id of typ * id
+
+
type naming_scheme_opt = (* Optional variable-naming-scheme specification for variables of defined type *)
| Name_sect_none
| Name_sect_some of string
@@ -212,24 +218,25 @@ type index_range = (* index specification, for bitfields in register types *)
| BF_concat of index_range * index_range (* concatenation of index ranges *)
-type default_typing_spec = (* Default kinding or typing assumption *)
- | DT_kind of base_kind * id
- | DT_typ of typschm * id
+type val_spec = (* 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 fundef = (* Function definition *)
| FD_function of rec_opt * tannot_opt * effects_opt * list funcl
-type val_spec = (* Value type specification *)
- | VS_val_spec 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 default_typing_spec = (* Default kinding or typing assumption *)
+ | DT_kind of base_kind * id
+ | DT_typ of typschm * id
type type_def = (* Type definition body *)
| TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *)
| TD_record of id * naming_scheme_opt * typquant * list (typ * id) * bool (* struct type definition *)
- | TD_variant of id * naming_scheme_opt * typquant * list (typ * id) * bool (* union type definition *)
+ | TD_variant of id * naming_scheme_opt * typquant * list type_union * bool (* union type definition *)
| TD_enum of id * naming_scheme_opt * list id * bool (* enumeration type definition *)
| TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
@@ -257,7 +264,7 @@ type typ_lib = (* library types and syntactic sugar for them *)
| Typ_lib_bool (* booleans $true$ and $false$ *)
| Typ_lib_bit (* pure bit values (not mutable bits) *)
| Typ_lib_nat (* natural numbers 0,1,2,... *)
- | Typ_lib_string of string (* UTF8 strings *)
+ | Typ_lib_string (* UTF8 strings *)
| Typ_lib_enum of nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *)
| Typ_lib_enum1 of nexp (* sugar for \texttt{enum nexp 0 inc} *)
| Typ_lib_enum2 of nexp * nexp (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *)
diff --git a/language/l2.ml b/language/l2.ml
index 664ace51..6ecf3411 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -218,7 +218,11 @@ typschm =
type
-'a letbind =
+'a letbind_aux = (* Let binding *)
+ LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
+ | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
+
+and 'a letbind =
LB_aux of 'a letbind_aux * 'a annot
and 'a exp_aux = (* Expression *)
@@ -226,7 +230,7 @@ and 'a exp_aux = (* Expression *)
| E_id of id (* identifier *)
| E_lit of lit (* literal constant *)
| E_cast of typ * 'a exp (* cast *)
- | E_app of 'a exp * ('a exp) list (* function application *)
+ | E_app of id * ('a exp) list (* function application *)
| E_app_infix of 'a exp * id * 'a exp (* infix function application *)
| E_tuple of ('a exp) list (* tuple *)
| E_if of 'a exp * 'a exp * 'a exp (* conditional *)
@@ -277,25 +281,22 @@ and 'a pexp_aux = (* Pattern match *)
and 'a pexp =
Pat_aux of 'a pexp_aux * 'a annot
-and 'a letbind_aux = (* Let binding *)
- LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
- | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
-
type
-'a tannot_opt_aux = (* Optional type annotation for functions *)
- Typ_annot_opt_some of typquant * typ
+type_union_aux = (* Type union constructors *)
+ Tu_id of id
+ | Tu_ty_id of typ * id
type
-'a funcl_aux = (* Function clause *)
- FCL_Funcl of id * 'a pat * 'a exp
+naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *)
+ Name_sect_none
+ | Name_sect_some of string
type
-'a effects_opt_aux = (* Optional effect annotation for functions *)
- Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of effects
+'a funcl_aux = (* Function clause *)
+ FCL_Funcl of id * 'a pat * 'a exp
type
@@ -305,75 +306,81 @@ rec_opt_aux = (* Optional recursive annotation for functions *)
type
-naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *)
- Name_sect_none
- | Name_sect_some of string
+'a tannot_opt_aux = (* Optional type annotation for functions *)
+ Typ_annot_opt_some of typquant * typ
type
-'a tannot_opt =
- Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
+'a effects_opt_aux = (* Optional effect annotation for functions *)
+ Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of effects
type
-'a funcl =
- FCL_aux of 'a funcl_aux * 'a annot
+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 effects_opt =
- Effects_opt_aux of 'a effects_opt_aux * 'a annot
+type_union =
+ Tu_aux of type_union_aux * l
type
-rec_opt =
- Rec_aux of rec_opt_aux * l
+naming_scheme_opt =
+ Name_sect_aux of naming_scheme_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 *)
+'a funcl =
+ FCL_aux of 'a funcl_aux * 'a annot
-and index_range =
- BF_aux of index_range_aux * l
+
+type
+rec_opt =
+ Rec_aux of rec_opt_aux * l
type
-naming_scheme_opt =
- Name_sect_aux of naming_scheme_opt_aux * l
+'a tannot_opt =
+ Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
type
-'a default_typing_spec_aux = (* Default kinding or typing assumption *)
- DT_kind of base_kind * id
- | DT_typ of typschm * id
+'a effects_opt =
+ Effects_opt_aux of 'a effects_opt_aux * 'a annot
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 *)
type
-'a fundef_aux = (* Function definition *)
- FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
-
-
-type
'a type_def_aux = (* Type definition body *)
TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *)
| TD_record of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
- | TD_variant of id * naming_scheme_opt * typquant * ((typ * id)) list * bool (* union type definition *)
+ | TD_variant of id * naming_scheme_opt * typquant * (type_union) list * bool (* union type definition *)
| TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *)
| TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
type
-'a default_typing_spec =
- DT_aux of 'a default_typing_spec_aux * 'a annot
+'a fundef_aux = (* Function definition *)
+ FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
+
+
+type
+'a default_typing_spec_aux = (* Default kinding or typing assumption *)
+ DT_kind of base_kind * id
+ | DT_typ of typschm * id
type
@@ -382,13 +389,18 @@ type
type
+'a type_def =
+ TD_aux of 'a type_def_aux * 'a annot
+
+
+type
'a fundef =
FD_aux of 'a fundef_aux * 'a annot
type
-'a type_def =
- TD_aux of 'a type_def_aux * 'a annot
+'a default_typing_spec =
+ DT_aux of 'a default_typing_spec_aux * 'a annot
type
@@ -407,17 +419,12 @@ type
type
-'a def =
- DEF_aux of 'a def_aux * 'a annot
-
-
-type
'a typ_lib_aux = (* library types and syntactic sugar for them *)
Typ_lib_unit (* unit type with value $()$ *)
| Typ_lib_bool (* booleans $_$ and $_$ *)
| Typ_lib_bit (* pure bit values (not mutable bits) *)
| Typ_lib_nat (* natural numbers 0,1,2,... *)
- | Typ_lib_string of string (* UTF8 strings *)
+ | Typ_lib_string (* UTF8 strings *)
| Typ_lib_enum of nexp * nexp * order (* natural numbers nexp .. nexp+nexp-1, ordered by order *)
| Typ_lib_enum1 of nexp (* sugar for \texttt{enum nexp 0 inc} *)
| Typ_lib_enum2 of nexp * nexp (* sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} *)
@@ -430,8 +437,8 @@ type
type
-'a defs = (* Definition sequence *)
- Defs of ('a def) list
+'a def =
+ DEF_aux of 'a def_aux * 'a annot
type
@@ -439,4 +446,9 @@ type
Typ_lib_aux of 'a typ_lib_aux * l
+type
+'a defs = (* Definition sequence *)
+ Defs of ('a def) list
+
+
diff --git a/language/l2.ott b/language/l2.ott
index 1e39aaff..e28e0271 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -111,13 +111,7 @@ id :: '' ::=
{{ com Identifier }}
{{ aux _ l }}
| x :: :: id
- | ( x ) :: :: deIid {{ com remove infix status }}
-% Note: we have just a single namespace. We don't want the same
-% identifier to be reused as a type name or variable, expression
-% variable, and field name. We don't enforce any lexical convention
-% on type variables (or variables of other kinds)
-% We don't enforce a lexical convention on infix operators, as some of the
-% targets use alphabetical infix operators.
+ | ( deinfix x ) :: :: deIid {{ com remove infix status }}
| bool :: M :: bool {{ com Built in type identifiers }} {{ ichlo bool_id }}
| bit :: M :: bit {{ ichlo bit_id }}
| unit :: M :: unit {{ ichlo unit_id }}
@@ -128,6 +122,13 @@ id :: '' ::=
| list :: M :: list {{ ichlo list_id }}
| set :: M :: set {{ ichlo set_id }}
| reg :: M :: reg {{ ichlo reg_id }}
+% Note: we have just a single namespace. We don't want the same
+% identifier to be reused as a type name or variable, expression
+% variable, and field name. We don't enforce any lexical convention
+% on type variables (or variables of other kinds)
+% We don't enforce a lexical convention on infix operators, as some of the
+% targets use alphabetical infix operators.
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -137,74 +138,6 @@ id :: '' ::=
grammar
-
-% a :: 'A_' ::=
-% {{ aux _ l }}
-% {{ ocaml terminal * text }}
-% {{ lem terminal * string }}
-% {{ hol string }}
-% {{ com Type variables }}
-% | ' x :: :: A
-% {{ ichlo [[x]] }}
-%
-% N :: 'N_' ::=
-% {{ aux _ l }}
-% {{ ocaml terminal * text }}
-% {{ lem terminal * string }}
-% {{ hol string }}
-% {{ com numeric variables }}
-% | ' ' x :: :: N
-% {{ ichlo [[x]] }}
-%
-% EN :: 'EN_' ::=
-% {{ aux _ l }}
-% {{ ocaml terminal * text }}
-% {{ lem terminal * string }}
-% {{ hol string }}
-% {{ com endianness variables }}
-% | ' ' ' x :: :: EN
-% {{ ichlo [[x]] }}
-%
-% EFF :: 'EFF_' ::=
-% {{ aux _ l }}
-% {{ ocaml terminal * text }}
-% {{ lem terminal * string }}
-% {{ hol string }}
-% {{ com effect set variables }}
-% | ' ' ' ' x :: :: EFF
-% {{ ichlo [[x]] }}
-% % TODO: better concrete syntax!!!!
-%
-%
-% tnvar :: '' ::=
-% {{ com variables of the base kinds }}
-% | a :: :: Av
-% | N :: :: Nv
-% | EN :: :: ENv
-% | EFF :: :: EFFv
-%
-% tnvars :: '' ::= {{ phantom }}
-% {{ hol tnvar list }}
-% {{ ocaml tnvar list }}
-% {{ lem list tnvar }}
-% {{ com Type variable lists }}
-% | tnvar1 .. tnvarn :: :: Tvars
-% {{ hol [[tnvar1..tnvarn]] }}
-% {{ ocaml [[tnvar1..tnvarn]] }}
-% {{ lem [[tnvar1..tnvarn]] }}
-%
-%
-% ids :: '' ::= {{ phantom }}
-% {{ hol id list }}
-% {{ ocaml id list }}
-% {{ lem list id }}
-% {{ com Type variable lists }}
-% | id1 .. idn :: :: Tvars
-% {{ hol [[id1..idn]] }}
-% {{ ocaml [[id1..idn]] }}
-% {{ lem [[id1..idn]] }}
-
-
base_kind :: 'BK_' ::=
{{ com base kind}}
{{ aux _ l }}
@@ -217,7 +150,7 @@ kind :: 'K_' ::=
{{ com kinds}}
{{ aux _ l }}
| base_kind1 -> ... -> base_kindn :: :: kind
-% we'll never use ...-> Nat
+% we'll never use ...-> Nat , .. Order , .. or Effects
nexp :: 'Nexp_' ::=
@@ -228,7 +161,7 @@ nexp :: 'Nexp_' ::=
| nexp1 * nexp2 :: :: times {{ com product }}
%{{ com must be linear after normalisation... except for the type of *, ahem }}
| nexp1 + nexp2 :: :: sum {{ com sum }}
- | 2 ** nexp :: :: exp {{ com exponential }}
+ | 2** nexp :: :: exp {{ com exponential }}
| ( nexp ) :: S :: paren {{ ichlo [[nexp]] }}
order :: 'Ord_' ::=
@@ -275,7 +208,7 @@ typ :: 'Typ_' ::=
| typ1 * .... * typn :: :: tup
{{ com Tuple type }}
% TODO union in the other kind grammars? or make a syntax of argument? or glom together the grammars and leave o the typechecker
- | id typ_arg1 .. typ_argn :: :: app
+ | id < typ_arg1 .. typ_argn > :: :: app
{{ com type constructor application }}
| ( typ ) :: S :: paren {{ ichlo [[typ]] }}
@@ -293,27 +226,27 @@ typ_lib :: 'Typ_lib_' ::=
{{ com library types and syntactic sugar for them }}
{{ aux _ l }} {{ auxparam 'a }}
% boring base types:
- | unit :: :: unit {{ com unit type with value $()$ }}
- | bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }}
- | bit :: :: bit {{ com pure bit values (not mutable bits) }}
+ | Unit :: :: unit {{ com unit type with value $()$ }}
+ | Bool :: :: bool {{ com booleans $[[true]]$ and $[[false]]$ }}
+ | Bit :: :: bit {{ com pure bit values (not mutable bits) }}
% experimentally trying with two distinct types of bool and bit ...
- | nat :: :: nat {{ com natural numbers 0,1,2,... }}
- | string :: :: string {{ com UTF8 strings }}
+ | Nat :: :: nat {{ com natural numbers 0,1,2,... }}
+ | String :: :: string {{ com UTF8 strings }}
% finite subranges of nat
- | enum nexp1 nexp2 order :: :: enum {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1, ordered by [[order]] }}
+ | Enum nexp1 nexp2 order :: :: enum {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1, ordered by [[order]] }}
| [ nexp ] :: :: enum1 {{ com sugar for \texttt{enum nexp 0 inc} }}
| [ nexp : nexp' ] :: :: enum2 {{ com sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} }}
% use .. not - to avoid ambiguity with nexp -
% total maps and vectors indexed by finite subranges of nat
- | vector nexp1 nexp2 order typ :: :: vector {{ com vector of [[typ]], indexed by natural range }}
+ | Vector nexp1 nexp2 order typ :: :: vector {{ com vector of [[typ]], indexed by natural range }}
% probably some sugar for vector types, using [ ] similarly to enums:
% (but with .. not : in the former, to avoid confusion...)
| typ [ nexp ] :: :: vector2 {{ com sugar for vector indexed by [ [[nexp]] ] }}
| typ [ nexp : nexp' ] :: :: vector3 {{ com sugar for vector indexed by [ [[nexp]]..[[nexp']] ] }}
% ...so bit [ nexp ] etc is just an instance of that
- | list typ :: :: list {{ com list of [[typ]] }}
- | set typ :: :: set {{ com finite set of [[typ]] }}
- | reg typ :: :: reg {{ com mutable register components holding [[typ]] }}
+ | List < typ > :: :: list {{ com list of [[typ]] }}
+ | Set < typ > :: :: set {{ com finite set of [[typ]] }}
+ | Reg < typ > :: :: reg {{ com mutable register components holding [[typ]] }}
% "reg t" is basically the ML "t ref"
% not sure how first-class it should be, though
% use "reg word32" etc for the types of vanilla registers
@@ -419,7 +352,7 @@ type_def :: 'TD_' ::=
% let the typi be function types (as constructors are not allowed to
% take parameters of function types)
% concrete syntax: to be even closer to C, could have a postfix id rather than prefix id =
- | typedef id naming_scheme_opt = const union typquant { typ1 id1 ; ... ; typn idn semi_opt } :: :: variant
+ | typedef id naming_scheme_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: :: variant
{{ com union type definition}} {{ texlong }}
| typedef id naming_scheme_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum
@@ -430,6 +363,11 @@ type_def :: 'TD_' ::=
% also sugar [ nexp ]
+type_union :: 'Tu_' ::=
+ {{ com Type union constructors }}
+ {{ aux _ l }}
+ | id :: :: id
+ | typ id :: :: ty_id
index_range :: 'BF_' ::= {{ com index specification, for bitfields in register types}}
{{ aux _ l }}
@@ -498,15 +436,14 @@ pat :: 'P_' ::=
% | ( pat : typ ) :: :: typ
% {{ com Typed patterns }}
% C-style
-% XXX < > are necessary to make the grammar non ambiguous
- | ( < typ > pat ) :: :: typ
+ | ( ( typ ) pat ) :: :: typ
{{ com typed pattern }}
| id :: :: id
{{ com identifier }}
%
- | id pat1 .. patn :: :: app
+ | id ( pat1 , .. , patn ) :: :: app
{{ com union constructor pattern }}
% OR? do we invent something ghastly including a union keyword? Perhaps not...
@@ -532,14 +469,12 @@ pat :: 'P_' ::=
| ( pat1 , .... , patn ) :: :: tup
{{ com tuple pattern }}
- | [| pat1 , .. , patn |] :: :: list
+ | [|| pat1 , .. , patn ||] :: :: list
{{ com list pattern }}
| ( pat ) :: S :: paren
{{ ichlo [[pat]] }}
% | pat1 '::' pat2 :: :: cons
% {{ com Cons patterns }}
-% | id '+' num :: :: num_add
-% {{ com constant addition patterns }}
% XXX Is this still useful?
fpat :: 'FP_' ::=
@@ -575,7 +510,7 @@ exp :: 'E_' ::=
| ( typ ) exp :: :: cast
{{ com cast }}
- | exp exp1 ... expn :: :: app
+ | id ( exp1 , .. , expn ) :: :: app
{{ com function application }}
% Note: fully applied function application only
% We might restrict exp to be an identifier
@@ -627,7 +562,7 @@ exp :: 'E_' ::=
% lists
- | [| exp1 , .. , expn |] :: :: list
+ | [|| exp1 , .. , expn ||] :: :: list
{{ com list }}
| exp1 '::' exp2 :: :: cons
{{ com cons }}
@@ -821,6 +756,7 @@ val_spec :: 'VS_' ::=
{{ com Value type specification }}
{{ aux _ annot }} {{ auxparam 'a }}
| val typschm id :: :: val_spec
+ | val extern typschm id :: :: extern_no_rename
| val extern typschm id = string :: :: extern_spec
{{ com 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 }}
diff --git a/language/l2_parse.ml b/language/l2_parse.ml
index c6153f89..990166c4 100644
--- a/language/l2_parse.ml
+++ b/language/l2_parse.ml
@@ -192,7 +192,7 @@ exp_aux = (* Expression *)
| E_id of id (* identifier *)
| E_lit of lit (* literal constant *)
| E_cast of atyp * exp (* cast *)
- | E_app of exp * (exp) list (* function application *)
+ | E_app of id * (exp) list (* function application *)
| E_app_infix of exp * id * exp (* infix function application *)
| E_tuple of (exp) list (* tuple *)
| E_if of exp * exp * exp (* conditional *)
@@ -248,9 +248,9 @@ naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for va
type
-rec_opt_aux = (* Optional recursive annotation for functions *)
- Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
+type_union_aux = (* Type union constructors *)
+ Tu_id of id
+ | Tu_ty_id of atyp * id
type
@@ -260,14 +260,25 @@ tannot_opt_aux = (* Optional type annotation for functions *)
type
+effects_opt_aux = (* Optional effect annotation for functions *)
+ Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of atyp
+
+
+type
+rec_opt_aux = (* Optional recursive annotation for functions *)
+ Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
+
+
+type
funcl_aux = (* Function clause *)
FCL_Funcl of id * pat * exp
type
-effects_opt_aux = (* Optional effect annotation for functions *)
- Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of atyp
+naming_scheme_opt =
+ Name_sect_aux of naming_scheme_opt_aux * l
type
@@ -281,49 +292,50 @@ and index_range =
type
-naming_scheme_opt =
- Name_sect_aux of naming_scheme_opt_aux * l
+type_union =
+ Tu_aux of type_union_aux * l
type
-rec_opt =
- Rec_aux of rec_opt_aux * l
+tannot_opt =
+ Typ_annot_opt_aux of tannot_opt_aux * l
type
-tannot_opt =
- Typ_annot_opt_aux of tannot_opt_aux * l
+effects_opt =
+ Effects_opt_aux of effects_opt_aux * l
type
-funcl =
- FCL_aux of funcl_aux * l
+rec_opt =
+ Rec_aux of rec_opt_aux * l
type
-effects_opt =
- Effects_opt_aux of effects_opt_aux * l
+funcl =
+ FCL_aux of funcl_aux * l
type
-default_typing_spec_aux = (* Default kinding or typing assumption *)
- DT_kind of base_kind * id
- | DT_typ of typschm * id
+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
type_def_aux = (* Type definition body *)
TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *)
| TD_record of id * naming_scheme_opt * typquant * ((atyp * id)) list * bool (* struct type definition *)
- | TD_variant of id * naming_scheme_opt * typquant * ((atyp * id)) list * bool (* union type definition *)
+ | TD_variant of id * naming_scheme_opt * typquant * (type_union) list * bool (* union type definition *)
| TD_enum of id * naming_scheme_opt * (id) list * bool (* enumeration type definition *)
| TD_register of id * atyp * atyp * ((index_range * id)) list (* register mutable bitfield type definition *)
type
-val_spec_aux = (* Value type specification *)
- VS_val_spec of typschm * id
- | VS_extern_spec of typschm * id * string
+default_typing_spec_aux = (* Default kinding or typing assumption *)
+ DT_kind of base_kind * id
+ | DT_typ of typschm * id
type
@@ -332,8 +344,8 @@ fundef_aux = (* Function definition *)
type
-default_typing_spec =
- DT_aux of default_typing_spec_aux * l
+val_spec =
+ VS_aux of val_spec_aux * l
type
@@ -342,8 +354,8 @@ type_def =
type
-val_spec =
- VS_aux of val_spec_aux * l
+default_typing_spec =
+ DT_aux of default_typing_spec_aux * l
type
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index c2cbe50d..6876fcfa 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -116,7 +116,8 @@ id :: '' ::=
{{ com Identifier }}
{{ aux _ l }}
| x :: :: id
- | ( x ) :: :: deIid {{ com remove infix status }}
+ | ( deinfix x ) :: :: deIid {{ com remove infix status }}
+
% Note: we have just a single namespace. We don't want the same
% identifier to be reused as a type name or variable, expression
% variable, and field name. We don't enforce any lexical convention
@@ -132,8 +133,6 @@ id :: '' ::=
grammar
-
-
base_kind :: 'BK_' ::=
{{ com base kind}}
{{ aux _ l }}
@@ -166,7 +165,7 @@ atyp :: 'ATyp_' ::=
| num :: :: constant {{ com constant }}
| atyp1 * atyp2 :: :: times {{ com product }}
| atyp1 + atyp2 :: :: sum {{ com sum }}
- | 2 ** atyp :: :: exp {{ com exponential }}
+ | 2** atyp :: :: exp {{ com exponential }}
| ( atyp ) :: S :: paren {{ icho [[atyp]] }}
| inc :: :: inc {{ com increasing (little-endian) }}
@@ -181,7 +180,7 @@ atyp :: 'ATyp_' ::=
{{ com Function type (first-order only in user code), last atyp is an effect }}
| atyp1 * .... * atypn :: :: tup
{{ com Tuple type }}
- | id atyp1 .. atypn :: :: app
+ | id < atyp1 .. atypn > :: :: app
{{ com type constructor application }}
@@ -278,6 +277,12 @@ grammar
| :: :: none
| [ name = regexp ] :: :: some
+type_union :: 'Tu_' ::=
+ {{ com Type union constructors }}
+ {{ aux _ l }}
+ | id :: :: id
+ | atyp id :: :: ty_id
+
type_def :: 'TD_' ::=
{{ com Type definition body }}
{{ aux _ l }}
@@ -285,7 +290,7 @@ type_def :: 'TD_' ::=
{{ com type abbreviation }} {{ texlong }}
| typedef id naming_scheme_opt = const struct typquant { atyp1 id1 ; ... ; atypn idn semi_opt } :: :: record
{{ com struct type definition }} {{ texlong }}
- | typedef id naming_scheme_opt = const union typquant { atyp1 id1 ; ... ; atypn idn semi_opt } :: :: variant
+ | typedef id naming_scheme_opt = const union typquant { type_union1 ; ... ; type_unionn semi_opt } :: :: variant
{{ com union type definition}} {{ texlong }}
| typedef id naming_scheme_opt = enumerate { id1 ; ... ; idn semi_opt } :: :: enum
{{ com enumeration type definition}} {{ texlong }}
@@ -358,13 +363,13 @@ pat :: 'P_' ::=
{{ com wildcard }}
| ( pat as id ) :: :: as
{{ com named pattern }}
- | ( < atyp > pat ) :: :: typ
+ | ( ( atyp ) pat ) :: :: typ
{{ com typed pattern }}
| id :: :: id
{{ com identifier }}
- | id pat1 .. patn :: :: app
+ | id ( pat1 , .. , patn ) :: :: app
{{ com union constructor pattern }}
| { fpat1 ; ... ; fpatn semi_opt } :: :: record
@@ -381,7 +386,7 @@ pat :: 'P_' ::=
| ( pat1 , .... , patn ) :: :: tup
{{ com tuple pattern }}
- | [| pat1 , .. , patn |] :: :: list
+ | [|| pat1 , .. , patn ||] :: :: list
{{ com list pattern }}
| ( pat ) :: S :: paren
{{ ichlo [[pat]] }}
@@ -419,7 +424,7 @@ exp :: 'E_' ::=
| ( atyp ) exp :: :: cast
{{ com cast }}
- | exp exp1 ... expn :: :: app
+ | id ( exp1 , .. , expn ) :: :: app
{{ com function application }}
% Note: fully applied function application only
% We might restrict exp to be an identifier
@@ -471,7 +476,7 @@ exp :: 'E_' ::=
% lists
- | [| exp1 , .. , expn |] :: :: list
+ | [|| exp1 , .. , expn ||] :: :: list
{{ com list }}
| exp1 '::' exp2 :: :: cons
{{ com cons }}
@@ -505,8 +510,6 @@ exp :: 'E_' ::=
| switch exp { case pexp1 ... case pexpn } :: :: case
{{ com pattern matching }}
-% | ( typ ) exp :: :: Typed
-% {{ com Type-annotated expressions }}
| letbind in exp :: :: let
{{ com let expression }}
@@ -661,7 +664,7 @@ letbind :: 'LB_' ::=
{{ com Let binding }}
{{ aux _ l }}
% {{ aux _ annot }} {{ auxparam 'a }}
- | typschm pat = exp :: :: val_explicit
+ | let typschm pat = exp :: :: val_explicit
{{ com value binding, explicit type ([[pat]] must be total)}}
| let pat = exp :: :: val_implicit
{{ com value binding, implicit type ([[pat]] must be total)}}
@@ -672,6 +675,7 @@ val_spec :: 'VS_' ::=
{{ aux _ l }}
% {{ aux _ annot }} {{ auxparam 'a }}
| val typschm id :: :: val_spec
+ | val extern typschm id :: :: extern_no_rename
| val extern typschm id = string :: :: extern_spec
default_typing_spec :: 'DT_' ::=
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 4d16fef4..772df3e9 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -323,7 +323,7 @@ and to_ast_exp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
| Parse_ast.E_id(id) -> E_id(to_ast_id id)
| Parse_ast.E_lit(lit) -> E_lit(to_ast_lit lit)
| Parse_ast.E_cast(typ,exp) -> E_cast(to_ast_typ k_env typ, to_ast_exp k_env exp)
- | Parse_ast.E_app(f,args) -> E_app(to_ast_exp k_env f, List.map (to_ast_exp k_env) args)
+ | Parse_ast.E_app(f,args) -> E_app(to_ast_id f, List.map (to_ast_exp k_env) args)
| Parse_ast.E_app_infix(left,op,right) -> E_app_infix(to_ast_exp k_env left, to_ast_id op, to_ast_exp k_env right)
| Parse_ast.E_tuple(exps) -> E_tuple(List.map (to_ast_exp k_env) exps)
| Parse_ast.E_if(e1,e2,e3) -> E_if(to_ast_exp k_env e1, to_ast_exp k_env e2, to_ast_exp k_env e3)
@@ -351,9 +351,9 @@ and to_ast_lexp (k_env : kind Envmap.t) (Parse_ast.E_aux(exp,l) : Parse_ast.exp)
LEXP_aux(
(match exp with
| Parse_ast.E_id(id) -> LEXP_id(to_ast_id id)
- | Parse_ast.E_app(Parse_ast.E_aux(f,l'),[exp]) ->
+ | Parse_ast.E_app((Parse_ast.Id_aux(f,l') as f'),[exp]) ->
(match f with
- | Parse_ast.E_id(id) -> LEXP_memory(to_ast_id id,to_ast_exp k_env exp)
+ | Parse_ast.Id(id) -> LEXP_memory(to_ast_id f',to_ast_exp k_env exp)
| _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None)
| Parse_ast.E_vector_access(vexp,exp) -> LEXP_vector(to_ast_lexp k_env vexp, to_ast_exp k_env exp)
| Parse_ast.E_vector_subrange(vexp,exp1,exp2) -> LEXP_vector_range(to_ast_lexp k_env vexp, to_ast_exp k_env exp1, to_ast_exp k_env exp2)
@@ -466,7 +466,11 @@ let to_ast_typedef (names,k_env,t_env) (td:Parse_ast.type_def) : (tannot type_de
let id = to_ast_id id in
let key = id_to_string id in
let typq,k_env,_ = to_ast_typquant k_env typq in
- let arms = List.map (fun (atyp,id) -> (to_ast_typ k_env atyp),(to_ast_id id)) arms in (* Add check that all arms have unique names *)
+ let arms = List.map (fun (Parse_ast.Tu_aux(tu,l)) ->
+ match tu with
+ | Parse_ast.Tu_ty_id(atyp,id) -> (Tu_aux(Tu_ty_id ((to_ast_typ k_env atyp),(to_ast_id id)),l))
+ | Parse_ast.Tu_id id -> (Tu_aux(Tu_id(to_ast_id id),l)) )
+ arms in (* Add check that all arms have unique names *)
let td_var = TD_aux(TD_variant(id,to_ast_namescm name_scm_opt,typq,arms,false),(l,None)) in
let typ = (match (typquant_to_quantkinds k_env typq) with
| [ ] -> {k = K_Typ}
@@ -595,7 +599,7 @@ let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out *
(match !d with
| (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)),dl), false) ->
let typ = to_ast_typ k typ in
- d:= (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms@[typ,arm_id],false),tl)),dl),false);
+ d:= (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms@[Tu_aux(Tu_ty_id (typ,arm_id), l)],false),tl)),dl),false);
(No_def,envs),partial_defs
| _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None
| _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None))
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 2e8af9d3..640f6b1d 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -130,7 +130,7 @@ let rec to_data_constructors (Defs defs) =
| DEF_type t ->
match t with
| TD_variant id _ tq tid_list _ ->
- (List.map (fun (x,y) -> (y,x)) tid_list)++(to_data_constructors (Defs defs))
+ (List.map (fun (Tu_ty_id x y) -> (y,x)) tid_list)++(to_data_constructors (Defs defs))
| _ -> to_data_constructors (Defs defs) end
| _ -> to_data_constructors (Defs defs) end
end
@@ -268,7 +268,7 @@ let rec to_exp v =
E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(List.length vals),[]) vals))
| V_record(ivals) -> E_record(FES_Fexps (List.map (fun (id,value) -> (FE_Fexp id (to_exp value))) ivals) false)
| V_list(vals) -> E_list (List.map to_exp vals)
- | V_ctor id vals -> E_app (E_id id) [to_exp vals]
+ | V_ctor id vals -> E_app id [to_exp vals]
end
val find_type_def : defs -> id -> maybe type_def
@@ -634,7 +634,7 @@ and interp_main t_level l_env l_mem exp =
| E_block(exps) -> interp_block t_level l_env l_env l_mem exps
| E_app f args ->
match (f,t_level) with
- | (E_id(id),(defs,externs,regs,mems,ctors)) ->
+ | (id,(defs,externs,regs,mems,ctors)) ->
(match find_function defs id with
| Just(funcls) ->
resolve_outcome (interp_main t_level l_env l_mem (List_extra.head args))
diff --git a/src/lexer.mll b/src/lexer.mll
index 3843a50b..b9336e2d 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -45,7 +45,7 @@
(**************************************************************************)
{
-open Parser
+open Pre_parser
module M = Map.Make(String)
exception LexError of string * Lexing.position
@@ -58,64 +58,69 @@ let kw_table =
(fun r (x,y) -> M.add x y r)
M.empty
[
- ("and", (fun _ -> And));
- ("as", (fun _ -> As));
- ("bits", (fun _ -> Bits));
- ("by", (fun _ -> By));
- ("case", (fun _ -> Case));
- ("clause", (fun _ -> Clause));
- ("const", (fun _ -> Const));
- ("default", (fun _ -> Default));
- ("effect", (fun _ -> Effect));
- ("Effects", (fun _ -> Effects));
- ("end", (fun _ -> End));
- ("enumerate", (fun _ -> Enumerate));
- ("else", (fun _ -> Else));
- ("extern", (fun _ -> Extern));
- ("false", (fun _ -> False));
- ("forall", (fun _ -> Forall));
- ("foreach", (fun _ -> Foreach));
- ("function", (fun x -> Function_));
- ("if", (fun x -> If_));
- ("in", (fun x -> In));
- ("IN", (fun x -> IN));
- ("let", (fun x -> Let_));
- ("member", (fun x -> Member));
- ("Nat", (fun x -> Nat));
- ("Order", (fun x -> Order));
- ("pure", (fun x -> Pure));
- ("rec", (fun x -> Rec));
- ("register", (fun x -> Register));
+ ("and", (fun _ -> Other));
+ ("as", (fun _ -> Other));
+ ("bits", (fun _ -> Other));
+ ("by", (fun _ -> Other));
+ ("case", (fun _ -> Other));
+ ("clause", (fun _ -> Other));
+ ("const", (fun _ -> Other));
+ ("dec", (fun _ -> Other));
+ ("default", (fun _ -> Other));
+ ("deinfix", (fun _ -> Other));
+ ("effect", (fun _ -> Other));
+ ("Effects", (fun _ -> Other));
+ ("end", (fun _ -> Other));
+ ("enumerate", (fun _ -> Other));
+ ("else", (fun _ -> Other));
+ ("extern", (fun _ -> Other));
+ ("false", (fun _ -> Other));
+ ("forall", (fun _ -> Other));
+ ("foreach", (fun _ -> Other));
+ ("function", (fun x -> Other));
+ ("if", (fun x -> Other));
+ ("in", (fun x -> Other));
+ ("IN", (fun x -> Other));
+ ("Inc", (fun x -> Other));
+ ("let", (fun x -> Other));
+ ("member", (fun x -> Other));
+ ("Nat", (fun x -> Other));
+ ("Order", (fun x -> Other));
+ ("pure", (fun x -> Other));
+ ("rec", (fun x -> Other));
+ ("register", (fun x -> Other));
("scattered", (fun x -> Scattered));
- ("struct", (fun x -> Struct));
- ("switch", (fun x -> Switch));
- ("then", (fun x -> Then));
- ("true", (fun x -> True));
- ("Type", (fun x -> TYPE));
+ ("struct", (fun x -> Other));
+ ("switch", (fun x -> Other));
+ ("then", (fun x -> Other));
+ ("true", (fun x -> Other));
+ ("Type", (fun x -> Other));
("typedef", (fun x -> Typedef));
- ("undefined", (fun x -> Undefined));
- ("union", (fun x -> Union));
- ("with", (fun x -> With));
- ("val", (fun x -> Val));
-
- ("AND", (fun x -> AND));
- ("div", (fun x -> Div_));
- ("EOR", (fun x -> EOR));
- ("mod", (fun x -> Mod));
- ("OR", (fun x -> OR));
- ("quot", (fun x -> Quot));
- ("rem", (fun x -> Rem));
+ ("undefined", (fun x -> Other));
+ ("union", (fun x -> Other));
+ ("with", (fun x -> Other));
+ ("val", (fun x -> Other));
+
+ ("AND", (fun x -> Other));
+ ("div", (fun x -> Other));
+ ("EOR", (fun x -> Other));
+ ("mod", (fun x -> Other));
+ ("OR", (fun x -> Other));
+ ("quot", (fun x -> Other));
+ ("rem", (fun x -> Other));
]
}
let ws = [' ''\t']+
+let lowerletter = ['a'-'z']
+let upperletter = ['A'-'Z']
let letter = ['a'-'z''A'-'Z']
let digit = ['0'-'9']
let binarydigit = ['0'-'1']
let hexdigit = ['0'-'9''A'-'F''a'-'f']
let alphanum = letter|digit
-let startident = letter|'_'
+let startident = lowerletter|'_'
let ident = alphanum|['_''\'']
let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''?''@''^''|''~']
let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit)
@@ -127,84 +132,6 @@ rule token = parse
{ Lexing.new_line lexbuf;
token lexbuf }
- | "&" { (Amp(r"&")) }
- | "@" { (At(r"@")) }
- | "|" { Bar }
- | "^" { (Carrot(r"^")) }
- | ":" { Colon }
- | "," { Comma }
- | "." { Dot }
- | "/" { (Div(r "/")) }
- | "=" { (Eq(r"=")) }
- | "!" { (Excl(r"!")) }
- | ">" { (Gt(r">")) }
- | "-" { Minus }
- | "<" { (Lt(r"<")) }
- | "+" { (Plus(r"+")) }
- | ";" { Semi }
- | "*" { (Star(r"*")) }
- | "~" { (Tilde(r"~")) }
- | "_" { Under }
- | "{" { Lcurly }
- | "}" { Rcurly }
- | "(" { Lparen }
- | "(:" { LparenColon }
- | ")" { Rparen }
- | "[" { Lsquare }
- | "]" { Rsquare }
- | "&&" as i { (AmpAmp(r i)) }
- | "||" { BarBar }
- | "|>" { BarGt }
- | "|]" { BarSquare }
- | "^^" { (CarrotCarrot(r"^^")) }
- | "::" as i { (ColonColon(r i)) }
- | ":=" { ColonEq }
- | ".." { DotDot }
- | "=/=" { (EqDivEq(r"=/=")) }
- | "==" { (EqEq(r"==")) }
- | "!=" { (ExclEq(r"!=")) }
- | "!!" { (ExclExcl(r"!!")) }
- | ">=" { (GtEq(r">=")) }
- | ">=+" { (GtEqPlus(r">=+")) }
- | ">>" { (GtGt(r">>")) }
- | ">>>" { (GtGtGt(r">>>")) }
- | ">+" { (GtPlus(r">+")) }
- | "#>>" { (HashGtGt(r"#>>")) }
- | "#<<" { (HashLtLt(r"#<<")) }
- | "->" { MinusGt }
- | "<=" { (LtEq(r"<=")) }
- | "<=+" { (LtEqPlus(r"<=+")) }
- | "<>" { (LtGt(r"<>")) }
- | "<<" { (LtLt(r"<<")) }
- | "<<<" { (LtLtLt(r"<<<")) }
- | "<+" { (LtPlus(r"<+")) }
- | "**" { (StarStar(r"**")) }
- | "~^" { (TildeCarrot(r"~^")) }
-
- | ">=_s" { (GtEqUnderS(r">=_s")) }
- | ">=_si" { (GtEqUnderSi(r">=_si")) }
- | ">=_u" { (GtEqUnderU(r">=_u")) }
- | ">=_ui" { (GtEqUnderUi(r">=_ui")) }
- | ">>_u" { (GtGtUnderU(r">>_u")) }
- | ">_s" { (GtUnderS(r">_s")) }
- | ">_si" { (GtUnderSi(r">_si")) }
- | ">_u" { (GtUnderU(r">_u")) }
- | ">_ui" { (GtUnderUi(r">_ui")) }
- | "<=_s" { (LtEqUnderS(r"<=_s")) }
- | "<=_si" { (LtEqUnderSi(r"<=_si")) }
- | "<=_u" { (LtEqUnderU(r"<=_u")) }
- | "<=_ui" { (LtEqUnderUi(r"<=_ui")) }
- | "<_s" { (LtUnderS(r"<_s")) }
- | "<_si" { (LtUnderSi(r"<_si")) }
- | "<_u" { (LtUnderU(r"<_u")) }
- | "<_ui" { (LtUnderUi(r"<_ui")) }
- | "**_s" { (StarStarUnderS(r"**_s")) }
- | "**_si" { (StarStarUnderSi(r"**_si")) }
- | "*_u" { (StarUnderU(r"*_u")) }
- | "*_ui" { (StarUnderUi(r"*_ui")) }
- | "2^" { (TwoCarrot(r"2^")) }
-
-
| "(*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf }
| "*)" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) }
@@ -212,71 +139,13 @@ rule token = parse
(M.find i kw_table) ()
else
Id(r i) }
- | "&" oper_char+ as i { (AmpI(r i)) }
- | "@" oper_char+ as i { (AtI(r i)) }
- | "^" oper_char+ as i { (CarrotI(r i)) }
- | "/" oper_char+ as i { (DivI(r i)) }
- | "=" oper_char+ as i { (EqI(r i)) }
- | "!" oper_char+ as i { (ExclI(r i)) }
- | ">" oper_char+ as i { (GtI(r i)) }
- | "<" oper_char+ as i { (LtI(r i)) }
- | "+" oper_char+ as i { (PlusI(r i)) }
- | "*" oper_char+ as i { (StarI(r i)) }
- | "~" oper_char+ as i { (TildeI(r i)) }
- | "&&" oper_char+ as i { (AmpAmpI(r i)) }
- | "^^" oper_char+ as i { (CarrotCarrotI(r i)) }
- | "::" oper_char+ as i { (ColonColonI(r i)) }
- | "=/=" oper_char+ as i { (EqDivEqI(r i)) }
- | "==" oper_char+ as i { (EqEqI(r i)) }
- | "!=" oper_char+ as i { (ExclEqI(r i)) }
- | "!!" oper_char+ as i { (ExclExclI(r i)) }
- | ">=" oper_char+ as i { (GtEqI(r i)) }
- | ">=+" oper_char+ as i { (GtEqPlusI(r i)) }
- | ">>" oper_char+ as i { (GtGtI(r i)) }
- | ">>>" oper_char+ as i { (GtGtGtI(r i)) }
- | ">+" oper_char+ as i { (GtPlusI(r i)) }
- | "#>>" oper_char+ as i { (HashGtGt(r i)) }
- | "#<<" oper_char+ as i { (HashLtLt(r i)) }
- | "<=" oper_char+ as i { (LtEqI(r i)) }
- | "<=+" oper_char+ as i { (LtEqPlusI(r i)) }
- | "<<" oper_char+ as i { (LtLtI(r i)) }
- | "<<<" oper_char+ as i { (LtLtLtI(r i)) }
- | "<+" oper_char+ as i { (LtPlusI(r i)) }
- | "**" oper_char+ as i { (StarStarI(r i)) }
- | "~^" oper_char+ as i { (TildeCarrot(r i)) }
-
- | ">=_s" oper_char+ as i { (GtEqUnderSI(r i)) }
- | ">=_si" oper_char+ as i { (GtEqUnderSiI(r i)) }
- | ">=_u" oper_char+ as i { (GtEqUnderUI(r i)) }
- | ">=_ui" oper_char+ as i { (GtEqUnderUiI(r i)) }
- | ">>_u" oper_char+ as i { (GtGtUnderUI(r i)) }
- | ">_s" oper_char+ as i { (GtUnderSI(r i)) }
- | ">_si" oper_char+ as i { (GtUnderSiI(r i)) }
- | ">_u" oper_char+ as i { (GtUnderUI(r i)) }
- | ">_ui" oper_char+ as i { (GtUnderUiI(r i)) }
- | "<=_s" oper_char+ as i { (LtEqUnderSI(r i)) }
- | "<=_si" oper_char+ as i { (LtEqUnderSiI(r i)) }
- | "<=_u" oper_char+ as i { (LtEqUnderUI(r i)) }
- | "<=_ui" oper_char+ as i { (LtEqUnderUiI(r i)) }
- | "<_s" oper_char+ as i { (LtUnderSI(r i)) }
- | "<_si" oper_char+ as i { (LtUnderSiI(r i)) }
- | "<_u" oper_char+ as i { (LtUnderUI(r i)) }
- | "<_ui" oper_char+ as i { (LtUnderUiI(r i)) }
- | "**_s" oper_char+ as i { (StarStarUnderSI(r i)) }
- | "**_si" oper_char+ as i { (StarStarUnderSiI(r i)) }
- | "*_u" oper_char+ as i { (StarUnderUI(r i)) }
- | "*_ui" oper_char+ as i { (StarUnderUiI(r i)) }
- | "2^" oper_char+ as i { (TwoCarrotI(r i)) }
-
- | digit+ as i { (Num(int_of_string i)) }
- | "0b" (binarydigit+ as i) { (Bin(i)) }
- | "0x" (hexdigit+ as i) { (Hex(i)) }
- | '"' { (String(
- string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf)) }
+ | oper_char+ { Other }
+ | digit+ as i { Other }
+ | '"' { let s =
+ string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf) in
+ Other }
| eof { Eof }
- | _ as c { raise (LexError(
- Printf.sprintf "Unexpected character: %c" c,
- Lexing.lexeme_start_p lexbuf)) }
+ | _ as c { Other }
and comment pos depth = parse
diff --git a/src/parser.mly b/src/parser.mly
index 2ff88944..c5f82508 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -120,9 +120,9 @@ let star = "*"
/*Terminals with no content*/
-%token And As Bits By Case Clause Const Default Dec Effect Effects End Enumerate Else Extern
+%token And As Bits By Case Clause Const Dec Default Deinfix Effect Effects End Enumerate Else Extern
%token False Forall Foreach Function_ If_ In IN Inc Let_ Member Nat Order Pure Rec Register
-%token Scattered Struct Switch Then True Type TYPE Typedef Undefined Union With Val
+%token Scattered Struct Switch Then True TwoStarStar Type TYPE Typedef Undefined Union With Val
/* Avoid shift/reduce conflict - see right_atomic_exp rule */
%nonassoc Then
@@ -132,11 +132,11 @@ let star = "*"
%token Bar Colon Comma Dot Eof Minus Semi Under
%token Lcurly Rcurly Lparen Rparen Lsquare Rsquare
-%token BarBar BarGt BarSquare DotDot ColonEq ColonGt MinusGt LtBar LparenColon SquareBar
+%token BarBar BarSquare BarBarSquare ColonEq DotDot ColonGt MinusGt LtBar SquareBar SquareBarBar
/*Terminals with content*/
-%token <string> Id TickId
+%token <string> Id TickId TyId
%token <int> Num
%token <string> String Bin Hex
@@ -175,70 +175,74 @@ id:
{ idl (Id($1)) }
| Tilde
{ idl (Id($1)) }
- | LparenColon Amp Rparen
- { idl (DeIid($2)) }
- | LparenColon At Rparen
- { idl (DeIid($2)) }
- | LparenColon Carrot Rparen
- { idl (DeIid($2)) }
- | LparenColon Div Rparen
- { idl (DeIid($2)) }
- | LparenColon Eq Rparen
- { Id_aux(DeIid($2),loc ()) }
- | LparenColon Excl Lparen
- { idl (DeIid($2)) }
- | LparenColon Gt Lparen
- { idl (DeIid($2)) }
- | LparenColon Lt Lparen
- { idl (DeIid($2)) }
- | LparenColon Minus Lparen
+ | Lparen Deinfix Amp Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix At Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix Carrot Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix Div Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix Eq Rparen
+ { Id_aux(DeIid($3),loc ()) }
+ | Lparen Deinfix Excl Lparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix Gt Lparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix Lt Lparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix Minus Lparen
{ idl (DeIid("-")) }
- | LparenColon Plus Rparen
- { idl (DeIid($2)) }
- | LparenColon Star Rparen
- { idl (DeIid($2)) }
- | LparenColon AmpAmp Rparen
- { idl (DeIid($2)) }
- | LparenColon BarBar Rparen
+ | Lparen Deinfix Plus Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix Star Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix AmpAmp Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix BarBar Rparen
{ idl (DeIid("||")) }
- | LparenColon CarrotCarrot Rparen
- { idl (DeIid($2)) }
- | LparenColon ColonColon Rparen
- { idl (DeIid($2)) }
- | LparenColon EqDivEq Rparen
- { idl (DeIid($2)) }
- | LparenColon EqEq Rparen
- { idl (DeIid($2)) }
- | LparenColon ExclEq Rparen
- { idl (DeIid($2)) }
- | LparenColon ExclExcl Rparen
- { idl (DeIid($2)) }
- | LparenColon GtEq Rparen
- { idl (DeIid($2)) }
- | LparenColon GtEqPlus Rparen
- { idl (DeIid($2)) }
- | LparenColon GtGt Rparen
- { idl (DeIid($2)) }
- | LparenColon GtGtGt Rparen
- { idl (DeIid($2)) }
- | LparenColon GtPlus Rparen
- { idl (DeIid($2)) }
- | LparenColon HashGtGt Rparen
- { idl (DeIid($2)) }
- | LparenColon HashLtLt Rparen
- { idl (DeIid($2)) }
- | LparenColon LtEq Rparen
- { idl (DeIid($2)) }
- | LparenColon LtLt Rparen
- { idl (DeIid($2)) }
- | LparenColon LtLtLt Rparen
- { idl (DeIid($2)) }
- | LparenColon LtPlus Rparen
- { idl (DeIid($2)) }
- | LparenColon StarStar Rparen
- { idl (DeIid($2)) }
- | LparenColon TildeCarrot Rparen
- { idl (DeIid($2)) }
+ | Lparen Deinfix CarrotCarrot Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix ColonColon Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix EqDivEq Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix EqEq Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix ExclEq Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix ExclExcl Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix GtEq Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix GtEqPlus Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix GtGt Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix GtGtGt Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix GtPlus Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix HashGtGt Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix HashLtLt Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix LtEq Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix LtLt Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix LtLtLt Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix LtPlus Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix StarStar Rparen
+ { idl (DeIid($3)) }
+ | Lparen Deinfix TildeCarrot Rparen
+ { idl (DeIid($3)) }
+
+tid:
+ | TyId
+ { (idl (Id($1))) }
atomic_kind:
| TYPE
@@ -283,7 +287,7 @@ effect_list:
{ $1::$3 }
effect_typ:
- | Effect id
+ | Effect tid
{ tloc (ATyp_efid($2)) }
| Effect Lcurly effect_list Rcurly
{ tloc (ATyp_set($3)) }
@@ -291,7 +295,7 @@ effect_typ:
{ tloc (ATyp_set([])) }
atomic_typ:
- | id
+ | tid
{ tloc (ATyp_id $1) }
| effect_typ
{ $1 }
@@ -299,32 +303,36 @@ atomic_typ:
{ tloc (ATyp_inc) }
| Dec
{ tloc (ATyp_dec) }
- | Lparen typ Rparen
- { $2 }
| SquareBar nexp_typ BarSquare
{ tloc (make_enum_sugar $2) }
| SquareBar nexp_typ Colon nexp_typ BarSquare
{ tloc (make_enum_sugar_bounded $2 $4) }
+ | Lparen typ Rparen
+ { $2 }
vec_typ:
| atomic_typ
{ $1 }
- | atomic_typ Lsquare nexp_typ Rsquare
- { tloc (make_vector_sugar $1 $3) }
- | atomic_typ Lsquare nexp_typ Colon nexp_typ Rsquare
- { tloc (make_vector_sugar_bounded $1 $3 $5) }
+ | tid Lsquare nexp_typ Rsquare
+ { tloc (make_vector_sugar (ATyp_aux ((ATyp_id $1), locn 1 1)) $3) }
+ | tid Lsquare nexp_typ Colon nexp_typ Rsquare
+ { tloc (make_vector_sugar_bounded (ATyp_aux ((ATyp_id $1), locn 1 1)) $3 $5) }
app_typs:
| vec_typ
{ [$1] }
+ | Num
+ { [tloc (ATyp_constant $1)] }
+ | Num app_typs
+ { (ATyp_aux((ATyp_constant $1),locn 1 1))::$2 }
| vec_typ app_typs
{ $1::$2 }
app_typ:
| vec_typ
{ $1 }
- | id app_typs
- { tloc (ATyp_app($1,$2)) }
+ | tid Lt app_typs Gt
+ { tloc (ATyp_app($1,$3)) }
star_typ_list:
| app_typ
@@ -342,23 +350,23 @@ star_typ:
exp_typ:
| star_typ
{ $1 }
- | Num StarStar typ
- { if (2 = $1)
- then tloc (ATyp_exp($3))
- else raise (Parse_error_locn(loc (), "Only 2 is a valid exponent base in Nats")) }
+ | Num
+ { tloc (ATyp_constant $1) }
+ | TwoStarStar typ
+ { tloc (ATyp_exp($2)) }
nexp_typ:
- | Num
- { tloc (ATyp_constant $1) }
| exp_typ
{ $1 }
- | atomic_typ Plus typ
+ | atomic_typ Plus nexp_typ
{ tloc (ATyp_sum($1,$3)) }
+ | Lparen atomic_typ Plus nexp_typ Rparen
+ { tloc (ATyp_sum($2,$4)) }
typ:
- | nexp_typ
+ | star_typ
{ $1 }
- | star_typ MinusGt atomic_typ effect_typ
+ | star_typ MinusGt typ effect_typ
{ tloc (ATyp_fn($1,$3,$4)) }
lit:
@@ -387,21 +395,25 @@ atomic_pat:
{ ploc P_wild }
| Lparen pat As id Rparen
{ ploc (P_as($2,$4)) }
- | Lt typ Gt atomic_pat
- { ploc (P_typ($2,$4)) }
+ | Lparen Lparen typ Rparen atomic_pat Rparen
+ { ploc (P_typ($3,$5)) }
| id
{ ploc (P_app($1,[])) }
| Lcurly fpats Rcurly
{ ploc (P_record((fst $2, snd $2))) }
- | Lsquare pat Rsquare
- { ploc (P_vector([$2])) }
| Lsquare comma_pats Rsquare
{ ploc (P_vector($2)) }
+ | Lsquare pat Rsquare
+ { ploc (P_vector([$2])) }
| Lsquare npats Rsquare
{ ploc (P_vector_indexed($2)) }
| Lparen comma_pats Rparen
{ ploc (P_tup($2)) }
- | SquareBar comma_pats BarSquare
+ | SquareBarBar BarBarSquare
+ { ploc (P_list([])) }
+ | SquareBarBar pat BarBarSquare
+ { ploc (P_list([$2])) }
+ | SquareBarBar comma_pats BarBarSquare
{ ploc (P_list($2)) }
| Lparen pat Rparen
{ $2 }
@@ -409,10 +421,10 @@ atomic_pat:
app_pat:
| atomic_pat
{ $1 }
- | id Lparen pat Rparen
- { ploc (P_app($1,[$3])) }
| id Lparen comma_pats Rparen
{ ploc (P_app($1,$3)) }
+ | id Lparen pat Rparen
+ { ploc (P_app($1,[$3])) }
pat_colons:
| atomic_pat Colon atomic_pat
@@ -463,7 +475,7 @@ atomic_exp:
{ eloc (E_lit($1)) }
| Lparen exp Rparen
{ $2 }
- | Lt typ Gt atomic_exp
+ | Lparen typ Rparen atomic_exp
{ eloc (E_cast($2,$4)) }
| Lparen comma_exps Rparen
{ eloc (E_tuple($2)) }
@@ -475,7 +487,7 @@ atomic_exp:
{ eloc (E_vector_update($2,$4,$6)) }
| Lsquare exp With atomic_exp Colon atomic_exp Eq exp Rsquare
{ eloc (E_vector_update_subrange($2,$4,$6,$8)) }
- | SquareBar comma_exps BarSquare
+ | SquareBarBar comma_exps BarBarSquare
{ eloc (E_list($2)) }
| Switch exp Lcurly case_exps Rcurly
{ eloc (E_case($2,$4)) }
@@ -498,11 +510,11 @@ app_exp:
| vaccess_exp
{ $1 }
| id Lparen Rparen
- { eloc (E_app((E_aux((E_id $1), locn 1 1)), [eloc (E_lit (lloc L_unit))])) }
+ { eloc (E_app($1, [eloc (E_lit (lloc L_unit))])) }
| id Lparen exp Rparen
- { eloc (E_app((E_aux((E_id $1),locn 1 1)),[ E_aux((E_tuple [$3]),locn 3 3)])) }
+ { eloc (E_app($1,[ E_aux((E_tuple [$3]),locn 3 3)])) }
| id Lparen comma_exps Rparen
- { eloc (E_app((E_aux((E_id $1),locn 1 1)),[E_aux (E_tuple $3,locn 3 3)])) }
+ { eloc (E_app($1,[E_aux (E_tuple $3,locn 3 3)])) }
right_atomic_exp:
| If_ exp Then exp Else exp
@@ -863,15 +875,19 @@ val_spec:
{ vloc (VS_val_spec(mk_typschm $2 $3 2 3,$4)) }
| Val atomic_typ id
{ vloc (VS_val_spec(mk_typschm (mk_typqn ()) $2 2 2,$3)) }
+ | Val Extern typquant atomic_typ id
+ { vloc (VS_extern_no_rename (mk_typschm $3 $4 3 4,$5)) }
+ | Val Extern atomic_typ id
+ { vloc (VS_extern_no_rename (mk_typschm (mk_typqn ()) $3 3 3, $4)) }
| Val Extern typquant atomic_typ id Eq String
{ vloc (VS_extern_spec (mk_typschm $3 $4 3 4,$5,$7)) }
| Val Extern atomic_typ id Eq String
{ vloc (VS_extern_spec (mk_typschm (mk_typqn ()) $3 3 3,$4, $6)) }
kinded_id:
- | id
+ | tid
{ kiloc (KOpt_none $1) }
- | kind id
+ | kind tid
{ kiloc (KOpt_kind($1,$2))}
/*kinded_ids:
@@ -924,6 +940,20 @@ c_def_body:
| atomic_typ id Semi c_def_body
{ ($1,$2)::(fst $4), snd $4 }
+union_body:
+ | id
+ { [Tu_aux( Tu_id $1, loc())],false }
+ | atomic_typ id
+ { [Tu_aux( Tu_ty_id ($1,$2), loc())],false }
+ | id Semi
+ { [Tu_aux( Tu_id $1, loc())],true }
+ | atomic_typ id Semi
+ { [Tu_aux( Tu_ty_id ($1,$2),loc())],true }
+ | id Semi union_body
+ { (Tu_aux( Tu_id $1, loc()))::(fst $3), snd $3 }
+ | atomic_typ id Semi union_body
+ { (Tu_aux(Tu_ty_id($1,$2),loc()))::(fst $4), snd $4 }
+
index_range_atomic:
| Num
{ irloc (BF_single($1)) }
@@ -976,13 +1006,13 @@ type_def:
{ tdloc (TD_record($2,mk_namesectn (), $6, fst $8, snd $8)) }
| Typedef id Eq Const Struct Lcurly c_def_body Rcurly
{ tdloc (TD_record($2, mk_namesectn (), mk_typqn (), fst $7, snd $7)) }
- | Typedef id name_sect Eq Const Union typquant Lcurly c_def_body Rcurly
+ | Typedef id name_sect Eq Const Union typquant Lcurly union_body Rcurly
{ tdloc (TD_variant($2,$3, $7, fst $9, snd $9)) }
- | Typedef id Eq Const Union typquant Lcurly c_def_body Rcurly
+ | Typedef id Eq Const Union typquant Lcurly union_body Rcurly
{ tdloc (TD_variant($2,mk_namesectn (), $6, fst $8, snd $8)) }
- | Typedef id name_sect Eq Const Union Lcurly c_def_body Rcurly
+ | Typedef id name_sect Eq Const Union Lcurly union_body Rcurly
{ tdloc (TD_variant($2, $3, mk_typqn (), fst $8, snd $8)) }
- | Typedef id Eq Const Union Lcurly c_def_body Rcurly
+ | Typedef id Eq Const Union Lcurly union_body Rcurly
{ tdloc (TD_variant($2, mk_namesectn (), mk_typqn (), fst $7, snd $7)) }
| Typedef id Eq Enumerate Lcurly enum_body Rcurly
{ tdloc (TD_enum($2, mk_namesectn (), $6,false)) }
diff --git a/src/pre_lexer.mll b/src/pre_lexer.mll
new file mode 100644
index 00000000..6955c7c3
--- /dev/null
+++ b/src/pre_lexer.mll
@@ -0,0 +1,319 @@
+(**************************************************************************)
+(* Lem *)
+(* *)
+(* Dominic Mulligan, University of Cambridge *)
+(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *)
+(* Gabriel Kerneis, University of Cambridge *)
+(* Kathy Gray, University of Cambridge *)
+(* Peter Boehm, University of Cambridge (while working on Lem) *)
+(* Peter Sewell, University of Cambridge *)
+(* Scott Owens, University of Kent *)
+(* Thomas Tuerk, University of Cambridge *)
+(* *)
+(* The Lem sources are copyright 2010-2013 *)
+(* by the UK authors above and Institut National de Recherche en *)
+(* Informatique et en Automatique (INRIA). *)
+(* *)
+(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *)
+(* are distributed under the license below. The former are distributed *)
+(* under the LGPLv2, as in the LICENSE file. *)
+(* *)
+(* *)
+(* Redistribution and use in source and binary forms, with or without *)
+(* modification, are permitted provided that the following conditions *)
+(* are met: *)
+(* 1. Redistributions of source code must retain the above copyright *)
+(* notice, this list of conditions and the following disclaimer. *)
+(* 2. Redistributions in binary form must reproduce the above copyright *)
+(* notice, this list of conditions and the following disclaimer in the *)
+(* documentation and/or other materials provided with the distribution. *)
+(* 3. The names of the authors may not be used to endorse or promote *)
+(* products derived from this software without specific prior written *)
+(* permission. *)
+(* *)
+(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *)
+(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *)
+(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *)
+(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *)
+(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *)
+(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *)
+(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *)
+(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *)
+(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *)
+(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *)
+(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *)
+(**************************************************************************)
+
+{
+open Parser
+module M = Map.Make(String)
+exception LexError of string * Lexing.position
+
+let r = fun s -> s (* Ulib.Text.of_latin1 *)
+(* Available as Scanf.unescaped since OCaml 4.0 but 3.12 is still common *)
+let unescaped s = Scanf.sscanf ("\"" ^ s ^ "\"") "%S%!" (fun x -> x)
+
+let kw_table =
+ List.fold_left
+ (fun r (x,y) -> M.add x y r)
+ M.empty
+ [
+ ("and", (fun _ -> And));
+ ("as", (fun _ -> As));
+ ("bits", (fun _ -> Bits));
+ ("by", (fun _ -> By));
+ ("case", (fun _ -> Case));
+ ("clause", (fun _ -> Clause));
+ ("const", (fun _ -> Const));
+ ("dec", (fun _ -> Dec));
+ ("default", (fun _ -> Default));
+ ("deinfix", (fun _ -> Deinfix));
+ ("effect", (fun _ -> Effect));
+ ("Effects", (fun _ -> Effects));
+ ("end", (fun _ -> End));
+ ("enumerate", (fun _ -> Enumerate));
+ ("else", (fun _ -> Else));
+ ("extern", (fun _ -> Extern));
+ ("false", (fun _ -> False));
+ ("forall", (fun _ -> Forall));
+ ("foreach", (fun _ -> Foreach));
+ ("function", (fun x -> Function_));
+ ("if", (fun x -> If_));
+ ("in", (fun x -> In));
+ ("IN", (fun x -> IN));
+ ("Inc", (fun x -> Inc));
+ ("let", (fun x -> Let_));
+ ("member", (fun x -> Member));
+ ("Nat", (fun x -> Nat));
+ ("Order", (fun x -> Order));
+ ("pure", (fun x -> Pure));
+ ("rec", (fun x -> Rec));
+ ("register", (fun x -> Register));
+ ("scattered", (fun x -> Scattered));
+ ("struct", (fun x -> Struct));
+ ("switch", (fun x -> Switch));
+ ("then", (fun x -> Then));
+ ("true", (fun x -> True));
+ ("Type", (fun x -> TYPE));
+ ("typedef", (fun x -> Typedef));
+ ("undefined", (fun x -> Undefined));
+ ("union", (fun x -> Union));
+ ("with", (fun x -> With));
+ ("val", (fun x -> Val));
+
+ ("AND", (fun x -> AND));
+ ("div", (fun x -> Div_));
+ ("EOR", (fun x -> EOR));
+ ("mod", (fun x -> Mod));
+ ("OR", (fun x -> OR));
+ ("quot", (fun x -> Quot));
+ ("rem", (fun x -> Rem));
+]
+
+}
+
+let ws = [' ''\t']+
+let lowerletter = ['a'-'z']
+let upperletter = ['A'-'Z']
+let letter = ['a'-'z''A'-'Z']
+let digit = ['0'-'9']
+let binarydigit = ['0'-'1']
+let hexdigit = ['0'-'9''A'-'F''a'-'f']
+let alphanum = letter|digit
+let startident = lowerletter|'_'
+let ident = alphanum|['_''\'']
+let starttident = upperletter
+let oper_char = ['!''$''%''&''*''+''-''.''/'':''<''=''>''?''@''^''|''~']
+let escape_sequence = ('\\' ['\\''\"''\'''n''t''b''r']) | ('\\' digit digit digit) | ('\\' 'x' hexdigit hexdigit)
+
+rule token = parse
+ | ws
+ { token lexbuf }
+ | "\n"
+ { Lexing.new_line lexbuf;
+ token lexbuf }
+
+ | "2**" { TwoStarStar }
+ | "&" { (Amp(r"&")) }
+ | "@" { (At(r"@")) }
+ | "|" { Bar }
+ | "^" { (Carrot(r"^")) }
+ | ":" { Colon }
+ | "," { Comma }
+ | "." { Dot }
+ | "/" { (Div(r "/")) }
+ | "=" { (Eq(r"=")) }
+ | "!" { (Excl(r"!")) }
+ | ">" { (Gt(r">")) }
+ | "-" { Minus }
+ | "<" { (Lt(r"<")) }
+ | "+" { (Plus(r"+")) }
+ | ";" { Semi }
+ | "*" { (Star(r"*")) }
+ | "~" { (Tilde(r"~")) }
+ | "_" { Under }
+ | "{" { Lcurly }
+ | "}" { Rcurly }
+ | "(" { Lparen }
+ | ")" { Rparen }
+ | "[" { Lsquare }
+ | "]" { Rsquare }
+ | "&&" as i { (AmpAmp(r i)) }
+ | "||" { BarBar }
+ | "|]" { BarSquare }
+ | "||]" { BarBarSquare }
+ | "^^" { (CarrotCarrot(r"^^")) }
+ | "::" as i { (ColonColon(r i)) }
+ | ":=" { ColonEq }
+ | ".." { DotDot }
+ | "=/=" { (EqDivEq(r"=/=")) }
+ | "==" { (EqEq(r"==")) }
+ | "!=" { (ExclEq(r"!=")) }
+ | "!!" { (ExclExcl(r"!!")) }
+ | ">=" { (GtEq(r">=")) }
+ | ">=+" { (GtEqPlus(r">=+")) }
+ | ">>" { (GtGt(r">>")) }
+ | ">>>" { (GtGtGt(r">>>")) }
+ | ">+" { (GtPlus(r">+")) }
+ | "#>>" { (HashGtGt(r"#>>")) }
+ | "#<<" { (HashLtLt(r"#<<")) }
+ | "->" { MinusGt }
+ | "<=" { (LtEq(r"<=")) }
+ | "<=+" { (LtEqPlus(r"<=+")) }
+ | "<>" { (LtGt(r"<>")) }
+ | "<<" { (LtLt(r"<<")) }
+ | "<<<" { (LtLtLt(r"<<<")) }
+ | "<+" { (LtPlus(r"<+")) }
+ | "**" { (StarStar(r"**")) }
+ | "~^" { (TildeCarrot(r"~^")) }
+
+ | ">=_s" { (GtEqUnderS(r">=_s")) }
+ | ">=_si" { (GtEqUnderSi(r">=_si")) }
+ | ">=_u" { (GtEqUnderU(r">=_u")) }
+ | ">=_ui" { (GtEqUnderUi(r">=_ui")) }
+ | ">>_u" { (GtGtUnderU(r">>_u")) }
+ | ">_s" { (GtUnderS(r">_s")) }
+ | ">_si" { (GtUnderSi(r">_si")) }
+ | ">_u" { (GtUnderU(r">_u")) }
+ | ">_ui" { (GtUnderUi(r">_ui")) }
+ | "<=_s" { (LtEqUnderS(r"<=_s")) }
+ | "<=_si" { (LtEqUnderSi(r"<=_si")) }
+ | "<=_u" { (LtEqUnderU(r"<=_u")) }
+ | "<=_ui" { (LtEqUnderUi(r"<=_ui")) }
+ | "<_s" { (LtUnderS(r"<_s")) }
+ | "<_si" { (LtUnderSi(r"<_si")) }
+ | "<_u" { (LtUnderU(r"<_u")) }
+ | "<_ui" { (LtUnderUi(r"<_ui")) }
+ | "**_s" { (StarStarUnderS(r"**_s")) }
+ | "**_si" { (StarStarUnderSi(r"**_si")) }
+ | "*_u" { (StarUnderU(r"*_u")) }
+ | "*_ui" { (StarUnderUi(r"*_ui")) }
+ | "2^" { (TwoCarrot(r"2^")) }
+
+
+ | "(*" { comment (Lexing.lexeme_start_p lexbuf) 0 lexbuf; token lexbuf }
+ | "*)" { raise (LexError("Unbalanced comment", Lexing.lexeme_start_p lexbuf)) }
+
+ | startident ident* as i { if M.mem i kw_table then
+ (M.find i kw_table) ()
+ else
+ Id(r i) }
+ | starttident ident* as i { if M.mem i kw_table then
+ (M.find i kw_table) ()
+ else
+ TyId(r i) }
+ | "&" oper_char+ as i { (AmpI(r i)) }
+ | "@" oper_char+ as i { (AtI(r i)) }
+ | "^" oper_char+ as i { (CarrotI(r i)) }
+ | "/" oper_char+ as i { (DivI(r i)) }
+ | "=" oper_char+ as i { (EqI(r i)) }
+ | "!" oper_char+ as i { (ExclI(r i)) }
+ | ">" oper_char+ as i { (GtI(r i)) }
+ | "<" oper_char+ as i { (LtI(r i)) }
+ | "+" oper_char+ as i { (PlusI(r i)) }
+ | "*" oper_char+ as i { (StarI(r i)) }
+ | "~" oper_char+ as i { (TildeI(r i)) }
+ | "&&" oper_char+ as i { (AmpAmpI(r i)) }
+ | "^^" oper_char+ as i { (CarrotCarrotI(r i)) }
+ | "::" oper_char+ as i { (ColonColonI(r i)) }
+ | "=/=" oper_char+ as i { (EqDivEqI(r i)) }
+ | "==" oper_char+ as i { (EqEqI(r i)) }
+ | "!=" oper_char+ as i { (ExclEqI(r i)) }
+ | "!!" oper_char+ as i { (ExclExclI(r i)) }
+ | ">=" oper_char+ as i { (GtEqI(r i)) }
+ | ">=+" oper_char+ as i { (GtEqPlusI(r i)) }
+ | ">>" oper_char+ as i { (GtGtI(r i)) }
+ | ">>>" oper_char+ as i { (GtGtGtI(r i)) }
+ | ">+" oper_char+ as i { (GtPlusI(r i)) }
+ | "#>>" oper_char+ as i { (HashGtGt(r i)) }
+ | "#<<" oper_char+ as i { (HashLtLt(r i)) }
+ | "<=" oper_char+ as i { (LtEqI(r i)) }
+ | "<=+" oper_char+ as i { (LtEqPlusI(r i)) }
+ | "<<" oper_char+ as i { (LtLtI(r i)) }
+ | "<<<" oper_char+ as i { (LtLtLtI(r i)) }
+ | "<+" oper_char+ as i { (LtPlusI(r i)) }
+ | "**" oper_char+ as i { (StarStarI(r i)) }
+ | "~^" oper_char+ as i { (TildeCarrot(r i)) }
+
+ | ">=_s" oper_char+ as i { (GtEqUnderSI(r i)) }
+ | ">=_si" oper_char+ as i { (GtEqUnderSiI(r i)) }
+ | ">=_u" oper_char+ as i { (GtEqUnderUI(r i)) }
+ | ">=_ui" oper_char+ as i { (GtEqUnderUiI(r i)) }
+ | ">>_u" oper_char+ as i { (GtGtUnderUI(r i)) }
+ | ">_s" oper_char+ as i { (GtUnderSI(r i)) }
+ | ">_si" oper_char+ as i { (GtUnderSiI(r i)) }
+ | ">_u" oper_char+ as i { (GtUnderUI(r i)) }
+ | ">_ui" oper_char+ as i { (GtUnderUiI(r i)) }
+ | "<=_s" oper_char+ as i { (LtEqUnderSI(r i)) }
+ | "<=_si" oper_char+ as i { (LtEqUnderSiI(r i)) }
+ | "<=_u" oper_char+ as i { (LtEqUnderUI(r i)) }
+ | "<=_ui" oper_char+ as i { (LtEqUnderUiI(r i)) }
+ | "<_s" oper_char+ as i { (LtUnderSI(r i)) }
+ | "<_si" oper_char+ as i { (LtUnderSiI(r i)) }
+ | "<_u" oper_char+ as i { (LtUnderUI(r i)) }
+ | "<_ui" oper_char+ as i { (LtUnderUiI(r i)) }
+ | "**_s" oper_char+ as i { (StarStarUnderSI(r i)) }
+ | "**_si" oper_char+ as i { (StarStarUnderSiI(r i)) }
+ | "*_u" oper_char+ as i { (StarUnderUI(r i)) }
+ | "*_ui" oper_char+ as i { (StarUnderUiI(r i)) }
+ | "2^" oper_char+ as i { (TwoCarrotI(r i)) }
+
+ | digit+ as i { (Num(int_of_string i)) }
+ | "0b" (binarydigit+ as i) { (Bin(i)) }
+ | "0x" (hexdigit+ as i) { (Hex(i)) }
+ | '"' { (String(
+ string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf)) }
+ | eof { Eof }
+ | _ as c { raise (LexError(
+ Printf.sprintf "Unexpected character: %c" c,
+ Lexing.lexeme_start_p lexbuf)) }
+
+
+and comment pos depth = parse
+ | "(*" { comment pos (depth+1) lexbuf }
+ | "*)" { if depth = 0 then ()
+ else if depth > 0 then comment pos (depth-1) lexbuf
+ else assert false }
+ | "\n" { Lexing.new_line lexbuf;
+ comment pos depth lexbuf }
+ | '"' { ignore(string (Lexing.lexeme_start_p lexbuf) (Buffer.create 10) lexbuf);
+ comment pos depth lexbuf }
+ | _ { comment pos depth lexbuf }
+ | eof { raise (LexError("Unbalanced comment", pos)) }
+
+and string pos b = parse
+ | ([^'"''\n''\\']*'\n' as i) { Lexing.new_line lexbuf;
+ Buffer.add_string b i;
+ string pos b lexbuf }
+ | ([^'"''\n''\\']* as i) { Buffer.add_string b i; string pos b lexbuf }
+ | escape_sequence as i { Buffer.add_string b i; string pos b lexbuf }
+ | '\\' '\n' ws { Lexing.new_line lexbuf; string pos b lexbuf }
+ | '\\' { assert false (*raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
+ "illegal backslash escape in string"*) }
+ | '"' { let s = unescaped(Buffer.contents b) in
+ (*try Ulib.UTF8.validate s; s
+ with Ulib.UTF8.Malformed_code ->
+ raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
+ "String literal is not valid utf8"))) *) s }
+ | eof { assert false (*raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos,
+ "String literal not terminated")))*) }
diff --git a/src/pre_parser.mly b/src/pre_parser.mly
new file mode 100644
index 00000000..5d56738b
--- /dev/null
+++ b/src/pre_parser.mly
@@ -0,0 +1,86 @@
+/**************************************************************************/
+/* Lem */
+/* */
+/* Dominic Mulligan, University of Cambridge */
+/* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt */
+/* Gabriel Kerneis, University of Cambridge */
+/* Kathy Gray, University of Cambridge */
+/* Peter Boehm, University of Cambridge (while working on Lem) */
+/* Peter Sewell, University of Cambridge */
+/* Scott Owens, University of Kent */
+/* Thomas Tuerk, University of Cambridge */
+/* */
+/* The Lem sources are copyright 2010-2013 */
+/* by the UK authors above and Institut National de Recherche en */
+/* Informatique et en Automatique (INRIA). */
+/* */
+/* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} */
+/* are distributed under the license below. The former are distributed */
+/* under the LGPLv2, as in the LICENSE file. */
+/* */
+/* */
+/* Redistribution and use in source and binary forms, with or without */
+/* modification, are permitted provided that the following conditions */
+/* are met: */
+/* 1. Redistributions of source code must retain the above copyright */
+/* notice, this list of conditions and the following disclaimer. */
+/* 2. Redistributions in binary form must reproduce the above copyright */
+/* notice, this list of conditions and the following disclaimer in the */
+/* documentation and/or other materials provided with the distribution. */
+/* 3. The names of the authors may not be used to endorse or promote */
+/* products derived from this software without specific prior written */
+/* permission. */
+/* */
+/* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS */
+/* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED */
+/* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE */
+/* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY */
+/* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL */
+/* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE */
+/* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS */
+/* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER */
+/* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR */
+/* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN */
+/* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. */
+/**************************************************************************/
+
+%{
+
+let r = fun x -> x (* Ulib.Text.of_latin1 *)
+
+%}
+
+/*Terminals with no content*/
+
+%token Scattered Typedef Other Eof
+
+%token <string> Id
+%start file
+%type <list string> file
+
+%%
+
+id:
+ | Id
+ { $1 }
+
+scan:
+ | Typedef id
+ { $2 }
+ | Scattered Typedef id
+ { $3 }
+ | id scan
+ { $2 }
+ | Other scan
+ { $2 }
+
+scan_file:
+ | scan
+ { [$1] }
+ | scan scan_file
+ { $1::$2 }
+
+file:
+ | scan_file Eof
+ { $1 }
+
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 55d09dcb..dd5a792b 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -211,7 +211,7 @@ and pp_exp ppf (E_aux(e,_)) =
| E_id(id) -> pp_id ppf id
| E_lit(lit) -> pp_lit ppf lit
| E_cast(typ,exp) -> fprintf ppf "@[<0>%a%a%a %a@]" kwd "<" pp_typ typ kwd ">" pp_exp exp
- | E_app(f,args) -> fprintf ppf "@[<0>%a %a@]" pp_exp f (list_pp pp_exp pp_exp) args
+ | E_app(f,args) -> fprintf ppf "@[<0>%a %a@]" pp_id f (list_pp pp_exp pp_exp) args
| E_app_infix(l,op,r) -> fprintf ppf "@[<0>%a %a %a@]" pp_exp l pp_id op pp_exp r
| E_tuple(exps) -> fprintf ppf "@[<0>%a %a %a@]" kwd "(" (list_pp pp_comma_exp pp_exp) exps kwd ")"
| E_if(c,t,e) -> fprintf ppf "@[<0> %a %a @[<1> %a %a@] @[<1> %a@ %a@]@]" kwd "if " pp_exp c kwd "then" pp_exp t kwd "else" pp_exp e
@@ -288,8 +288,11 @@ let pp_typdef ppf (TD_aux(td,_)) =
fprintf ppf "@[<0>%a %a %a %a %a %a %a %a@[<1>%a@] %a]@\n"
kwd "typedef" pp_id id pp_namescm nm kwd "=" kwd "const" kwd "struct" pp_typquant typq kwd "{" (list_pp f_pp f_pp) fs kwd "}"
| TD_variant(id,nm,typq,ar,_) ->
- let a_pp ppf (typ,id) =
- fprintf ppf "@[<1>%a %a%a@]" pp_typ typ pp_id id kwd ";" in
+ let a_pp ppf (Tu_aux(typ_u,_)) =
+ match typ_u with
+ | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>%a %a%a@]" pp_typ typ pp_id id kwd ";"
+ | Tu_id(id) -> fprintf ppf "@[<1>%a%a@]" pp_id id kwd ";"
+ in
fprintf ppf "@[<0>%a %a %a %a %a %a %a %a@[<1>%a@] %a]@\n"
kwd "typedef" pp_id id pp_namescm nm kwd "=" kwd "const" kwd "union" pp_typquant typq kwd "{" (list_pp a_pp a_pp) ar kwd "}"
| TD_enum(id,ns,enums,_) ->
@@ -504,7 +507,7 @@ and pp_lem_exp ppf (E_aux(e,_)) =
| E_id(id) -> fprintf ppf "(%a %a)" kwd "E_id" pp_lem_id id
| E_lit(lit) -> fprintf ppf "(%a %a)" kwd "E_lit" pp_lem_lit lit
| E_cast(typ,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp
- | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_exp f (list_pp pp_semi_lem_exp pp_lem_exp) args
+ | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args
| E_app_infix(l,op,r) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_app_infix" pp_lem_exp l pp_lem_id op pp_lem_exp r
| E_tuple(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")"
| E_if(c,t,e) -> fprintf ppf "@[<0>(%a %a @[<1>%a@] @[<1> %a@])@]" kwd "E_if" pp_lem_exp c pp_lem_exp t pp_lem_exp e
@@ -584,8 +587,11 @@ let pp_lem_typdef ppf (TD_aux(td,_)) =
fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs
| TD_variant(id,nm,typq,ar,_) ->
- let a_pp ppf (typ,id) =
- fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in
+ let a_pp ppf (Tu_aux(typ_u,_)) =
+ match typ_u with
+ | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_ty_id %a %a)@]" pp_lem_typ typ pp_lem_id id
+ | Tu_id(id) -> fprintf ppf "@[<1>(Tu_id %a)@]" pp_id id
+ in
fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]"
kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar
| TD_enum(id,ns,enums,_) ->
diff --git a/src/type_check.mli b/src/type_check.mli
new file mode 100644
index 00000000..25992725
--- /dev/null
+++ b/src/type_check.mli
@@ -0,0 +1,9 @@
+open Ast
+open Type_internal
+type kind = Type_internal.kind
+type typ = Type_internal.t
+
+type envs = Nameset.t * kind Envmap.t * typ Envmap.t
+type 'a envs_out = 'a * envs
+
+val check : Nameset.t -> kind Envmap.t -> typ Envmap.t -> tannot defs -> tannot defs
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 8ebb0b69..dabb8100 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -55,6 +55,12 @@ and t_arg =
| TA_eft of effect
| TA_ord of order
+type tag =
+ | Emp
+ | External
+ | Default
+ | Constructor
+
(* Constraints for nexps, plus the location which added the constraint, each nexp is either <= 0 = 0 or >= 0 *)
type nexp_range =
| LtEq of Parse_ast.l * nexp
@@ -62,7 +68,7 @@ type nexp_range =
| GtEq of Parse_ast.l * nexp
| In of Parse_ast.l * nexp * nexp list
-type tannot = (t * nexp_range list) option
+type tannot = (t * tag * nexp_range list) option
let initial_kind_env =
Envmap.from_list [
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 9aa5b9d9..99b82075 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -52,6 +52,12 @@ and t_arg =
| TA_eft of effect
| TA_ord of order
+type tag =
+ | Emp
+ | External
+ | Default
+ | Constructor
+
(* Constraints for nexps, plus the location which added the constraint, each nexp is either <= 0 = 0 or >= 0 *)
type nexp_range =
| LtEq of Parse_ast.l * nexp
@@ -59,6 +65,6 @@ type nexp_range =
| GtEq of Parse_ast.l * nexp
| In of Parse_ast.l * nexp * nexp list
-type tannot = (t * nexp_range list) option
+type tannot = (t * tag * nexp_range list) option
val initial_kind_env : kind Envmap.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:13:07 +0000