summaryrefslogtreecommitdiff
path: root/src/ast.ml
diff options
context:
space:
mode:
authorPeter Sewell2013-07-17 16:50:36 +0100
committerPeter Sewell2013-07-17 16:50:36 +0100
commit9538d030494bdfb07bdbd5c99ebb64a8fffe55e7 (patch)
treefd7d7eb0909f9d82bbe35633e8e7261e1ec6d64e /src/ast.ml
parent80fd65368f2769a29ce657aaffef50f3c8f0455f (diff)
wib
Diffstat (limited to 'src/ast.ml')
-rw-r--r--src/ast.ml168
1 files changed, 84 insertions, 84 deletions
diff --git a/src/ast.ml b/src/ast.ml
index e777ba4f..64659f2c 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -59,19 +59,14 @@ base_kind_aux = (* base kind *)
type
-base_kind =
- BK_aux of base_kind_aux * l
-
-
-type
id_aux = (* Identifier *)
Id of x
| DeIid of terminal * x * terminal (* remove infix status *)
type
-kind_aux = (* kinds *)
- K_kind of (base_kind * terminal) list
+base_kind =
+ BK_aux of base_kind_aux * l
type
@@ -80,6 +75,11 @@ id =
type
+kind_aux = (* kinds *)
+ K_kind of (base_kind * terminal) list
+
+
+type
effect_aux = (* effect *)
Effect_rreg of terminal (* read register *)
| Effect_wreg of terminal (* write register *)
@@ -91,11 +91,6 @@ effect_aux = (* effect *)
type
-kind =
- K_aux of kind_aux * l
-
-
-type
nexp_aux = (* expression of kind $_$, for vector sizes and origins *)
Nexp_id of id (* identifier *)
| Nexp_constant of terminal * int (* constant *)
@@ -108,14 +103,13 @@ and nexp =
type
-effect =
- Effect_aux of effect_aux * l
+kind =
+ K_aux of kind_aux * l
type
-kinded_id_aux = (* optionally kind-annotated identifier *)
- KOpt_none of id (* identifier *)
- | KOpt_kind of kind * id (* kind-annotated variable *)
+effect =
+ Effect_aux of effect_aux * l
type
@@ -127,6 +121,12 @@ type
type
+kinded_id_aux = (* optionally kind-annotated identifier *)
+ KOpt_none of id (* identifier *)
+ | KOpt_kind of kind * id (* kind-annotated variable *)
+
+
+type
effects_aux = (* effect set, of kind $_$ *)
Effects_var of id
| Effects_set of terminal * (effect * terminal) list * terminal (* effect set *)
@@ -140,13 +140,13 @@ order_aux = (* vector order specifications, of kind $_$ *)
type
-kinded_id =
- KOpt_aux of kinded_id_aux * l
+'a nexp_constraint =
+ NC_aux of 'a nexp_constraint_aux * 'a annot
type
-'a nexp_constraint =
- NC_aux of 'a nexp_constraint_aux * 'a annot
+kinded_id =
+ KOpt_aux of kinded_id_aux * l
type
@@ -167,19 +167,6 @@ type
type
-lit_aux = (* Literal constant *)
- L_unit of terminal * terminal (* $() : _$ *)
- | L_zero of terminal (* $_ : _$ *)
- | L_one of terminal (* $_ : _$ *)
- | L_true of terminal (* $_ : _$ *)
- | L_false of terminal (* $_ : _$ *)
- | L_num of terminal * int (* natural number constant *)
- | L_hex of terminal * string (* bit vector constant, C-style *)
- | L_bin of terminal * string (* bit vector constant, C-style *)
- | L_string of terminal * string (* string constant *)
-
-
-type
typ_aux = (* Type expressions, of kind $_$ *)
Typ_wild of terminal (* Unspecified type *)
| Typ_var of id (* Type variable *)
@@ -206,8 +193,16 @@ type
type
-lit =
- L_aux of lit_aux * l
+lit_aux = (* Literal constant *)
+ L_unit of terminal * terminal (* $() : _$ *)
+ | L_zero of terminal (* $_ : _$ *)
+ | L_one of terminal (* $_ : _$ *)
+ | L_true of terminal (* $_ : _$ *)
+ | L_false of terminal (* $_ : _$ *)
+ | L_num of terminal * int (* natural number constant *)
+ | L_hex of terminal * string (* bit vector constant, C-style *)
+ | L_bin of terminal * string (* bit vector constant, C-style *)
+ | L_string of terminal * string (* string constant *)
type
@@ -216,6 +211,16 @@ type
type
+lit =
+ L_aux of lit_aux * l
+
+
+type
+'a typschm =
+ TypSchm_aux of 'a typschm_aux * 'a annot
+
+
+type
'a pat_aux = (* Pattern *)
P_lit of lit (* literal constant pattern *)
| P_wild of terminal (* wildcard *)
@@ -241,15 +246,7 @@ and 'a fpat =
type
-'a typschm =
- TypSchm_aux of 'a typschm_aux * 'a annot
-
-
-type
-'a letbind =
- LB_aux of 'a letbind_aux * 'a annot
-
-and 'a exp_aux = (* Expression *)
+'a exp_aux = (* Expression *)
E_block of terminal * ('a exp * terminal) list * terminal (* block (parsing conflict with structs?) *)
| E_id of id (* identifier *)
| E_lit of lit (* literal constant *)
@@ -307,6 +304,9 @@ and 'a letbind_aux = (* Let binding *)
LB_val_explicit of 'a typschm * 'a pat * terminal * 'a exp (* value binding, explicit type ('a pat must be total) *)
| LB_val_implicit of terminal * 'a pat * terminal * 'a exp (* value binding, implicit type ('a pat must be total) *)
+and 'a letbind =
+ LB_aux of 'a letbind_aux * 'a annot
+
type
naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for variables of defined type *)
@@ -315,26 +315,31 @@ naming_scheme_opt_aux = (* Optional variable-naming-scheme specification for va
type
+'a tannot_opt_aux = (* Optional type annotation for functions *)
+ Typ_annot_opt_none
+ | Typ_annot_opt_some of terminal * typ
+
+
+type
rec_opt_aux = (* Optional recursive annotation for functions *)
Rec_nonrec (* non-recursive *)
| Rec_rec of terminal (* recursive *)
type
-'a funcl_aux = (* Function clause *)
- FCL_Funcl of id * 'a pat * terminal * 'a exp
+'a effects_opt_aux = (* Optional effect annotation for functions *)
+ Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of effects
type
-'a tannot_opt_aux = (* Optional type annotation for functions *)
- Typ_annot_opt_none
- | Typ_annot_opt_some of terminal * typ
+'a funcl_aux = (* Function clause *)
+ FCL_Funcl of id * 'a pat * terminal * 'a exp
type
-'a effects_opt_aux = (* Optional effect annotation for functions *)
- Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of effects
+naming_scheme_opt =
+ Name_sect_aux of naming_scheme_opt_aux * l
type
@@ -348,8 +353,8 @@ and index_range =
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
@@ -358,18 +363,19 @@ rec_opt =
type
-'a funcl =
- FCL_aux of 'a funcl_aux * 'a annot
+'a effects_opt =
+ Effects_opt_aux of 'a effects_opt_aux * 'a annot
type
-'a tannot_opt =
- Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
+'a funcl =
+ FCL_aux of 'a funcl_aux * 'a annot
type
-'a effects_opt =
- Effects_opt_aux of 'a effects_opt_aux * 'a annot
+'a default_typing_spec_aux = (* Default kinding or typing assumption *)
+ DT_kind of terminal * base_kind * id
+ | DT_typ of terminal * 'a typschm * id
type
@@ -382,19 +388,18 @@ type
type
-'a val_spec_aux = (* Value type specification *)
- VS_val_spec of terminal * 'a typschm * id
+'a fundef_aux = (* Function definition *)
+ FD_function of terminal * rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl * terminal) list
type
-'a default_typing_spec_aux = (* Default kinding or typing assumption *)
- DT_kind of terminal * base_kind * id
- | DT_typ of terminal * 'a typschm * id
+'a val_spec_aux = (* Value type specification *)
+ VS_val_spec of terminal * 'a typschm * id
type
-'a fundef_aux = (* Function definition *)
- FD_function of terminal * rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl * terminal) list
+'a default_typing_spec =
+ DT_aux of 'a default_typing_spec_aux * 'a annot
type
@@ -403,18 +408,13 @@ type
type
-'a val_spec =
- VS_aux of 'a val_spec_aux * 'a annot
-
-
-type
-'a default_typing_spec =
- DT_aux of 'a default_typing_spec_aux * 'a annot
+'a fundef =
+ FD_aux of 'a fundef_aux * 'a annot
type
-'a fundef =
- FD_aux of 'a fundef_aux * 'a annot
+'a val_spec =
+ VS_aux of 'a val_spec_aux * 'a annot
type
@@ -433,6 +433,11 @@ 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 of terminal (* unit type with value $()$ *)
| Typ_lib_bool of terminal (* booleans $_$ and $_$ *)
@@ -456,8 +461,8 @@ type
type
-'a def =
- DEF_aux of 'a def_aux * 'a annot
+'a defs = (* Definition sequence *)
+ Defs of ('a def) list
type
@@ -470,9 +475,4 @@ type
CT_aux of 'a ctor_def_aux * 'a annot
-type
-'a defs = (* Definition sequence *)
- Defs of ('a def) list
-
-