From cf4c7c0fd5fb8a9851fa6ca325d1b106ff080fd5 Mon Sep 17 00:00:00 2001
From: Peter Sewell
Date: Thu, 5 Sep 2013 15:21:42 +0100
Subject: workaround likely aux rule bug

---
 src/parse_ast.ml | 138 +++++++++++++++++++++++++++----------------------------
 1 file changed, 69 insertions(+), 69 deletions(-)

(limited to 'src/parse_ast.ml')

diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index 23957118..e0c75495 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -24,6 +24,12 @@ base_kind_aux =  (* base kind *)
  | BK_effects (* kind of effect sets *)
 
 
+type 
+id_aux =  (* Identifier *)
+   Id of x
+ | DeIid of x (* remove infix status *)
+
+
 type 
 efct_aux =  (* effect *)
    Effect_rreg (* read register *)
@@ -35,25 +41,19 @@ efct_aux =  (* effect *)
  | Effect_nondet (* nondeterminism from intra-instruction parallelism *)
 
 
-type 
-id_aux =  (* Identifier *)
-   Id of x
- | DeIid of x (* remove infix status *)
-
-
 type 
 base_kind = 
    BK_aux of base_kind_aux * l
 
 
 type 
-efct = 
-   Effect_aux of efct_aux * l
+id = 
+   Id_aux of id_aux * l
 
 
 type 
-id = 
-   Id_aux of id_aux * l
+efct = 
+   Effect_aux of efct_aux * l
 
 
 type 
@@ -127,6 +127,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 (* $() : _$ *)
@@ -141,8 +146,8 @@ lit_aux =  (* Literal constant *)
 
 
 type 
-typquant = 
-   TypQ_aux of typquant_aux * l
+typschm_aux =  (* type scheme *)
+   TypSchm_ts of typquant * atyp
 
 
 type 
@@ -151,8 +156,8 @@ lit =
 
 
 type 
-typschm_aux =  (* type scheme *)
-   TypSchm_ts of typquant * atyp
+typschm = 
+   TypSchm_aux of typschm_aux * l
 
 
 type 
@@ -180,11 +185,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?) *)
@@ -252,6 +252,12 @@ tannot_opt_aux =  (* Optional type annotation for functions *)
  | Typ_annot_opt_some of typquant * atyp
 
 
+type 
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
+
+
 type 
 effects_opt_aux =  (* Optional effect annotation for functions *)
    Effects_opt_pure (* sugar for empty effect set *)
@@ -259,14 +265,13 @@ effects_opt_aux =  (* Optional effect annotation for functions *)
 
 
 type 
-rec_opt_aux =  (* Optional recursive annotation for functions *)
-   Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
+funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * pat * exp
 
 
 type 
-funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * pat * exp
+naming_scheme_opt = 
+   Name_sect_aux of naming_scheme_opt_aux * l
 
 
 type 
@@ -279,34 +284,24 @@ and index_range =
    BF_aux of index_range_aux * l
 
 
-type 
-naming_scheme_opt = 
-   Name_sect_aux of naming_scheme_opt_aux * l
-
-
 type 
 tannot_opt = 
    Typ_annot_opt_aux of tannot_opt_aux * l
 
 
-type 
-effects_opt = 
-   Effects_opt_aux of effects_opt_aux * l
-
-
 type 
 rec_opt = 
    Rec_aux of rec_opt_aux * l
 
 
 type 
-funcl = 
-   FCL_aux of funcl_aux * l
+effects_opt = 
+   Effects_opt_aux of effects_opt_aux * l
 
 
 type 
-val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
+funcl = 
+   FCL_aux of funcl_aux * l
 
 
 type 
@@ -319,19 +314,19 @@ type_def_aux =  (* Type definition body *)
 
 
 type 
-default_typing_spec_aux =  (* Default kinding or typing assumption *)
-   DT_kind of base_kind * id
- | DT_typ of typschm * id
+fundef_aux =  (* Function definition *)
+   FD_function of rec_opt * tannot_opt * effects_opt * (funcl) list
 
 
 type 
-fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * tannot_opt * effects_opt * (funcl) list
+val_spec_aux =  (* Value type specification *)
+   VS_val_spec of typschm * id
 
 
 type 
-val_spec = 
-   VS_aux of val_spec_aux * l
+default_typing_spec_aux =  (* Default kinding or typing assumption *)
+   DT_kind of base_kind * id
+ | DT_typ of typschm * id
 
 
 type 
@@ -340,13 +335,18 @@ type_def =
 
 
 type 
-default_typing_spec = 
-   DT_aux of default_typing_spec_aux * l
+fundef = 
+   FD_aux of fundef_aux * l
 
 
 type 
-fundef = 
-   FD_aux of fundef_aux * l
+val_spec = 
+   VS_aux of val_spec_aux * l
+
+
+type 
+default_typing_spec = 
+   DT_aux of default_typing_spec_aux * l
 
 
 type 
@@ -364,16 +364,6 @@ def_aux =  (* Top-level definition *)
  | DEF_scattered_end of id (* scattered definition end *)
 
 
-type 
-def = 
-   DEF_aux of def_aux * l
-
-
-type 
-ctor_def_aux =  (* Datatype constructor definition clause *)
-   CT_ct of id * typschm
-
-
 type 
 typ_lib_aux =  (* library types and syntactic sugar for them *)
    Typ_lib_unit (* unit type with value $()$ *)
@@ -392,6 +382,26 @@ typ_lib_aux =  (* library types and syntactic sugar for them *)
  | Typ_lib_reg of atyp (* mutable register components holding atyp *)
 
 
+type 
+ctor_def_aux =  (* Datatype constructor definition clause *)
+   CT_ct of id * typschm
+
+
+type 
+def = 
+   DEF_aux of def_aux * l
+
+
+type 
+typ_lib = 
+   Typ_lib_aux of typ_lib_aux * l
+
+
+type 
+ctor_def = 
+   CT_aux of ctor_def_aux * l
+
+
 type 
 lexp_aux =  (* lvalue expression *)
    LEXP_id of id (* identifier *)
@@ -408,14 +418,4 @@ defs =  (* Definition sequence *)
    Defs of (def) list
 
 
-type 
-ctor_def = 
-   CT_aux of ctor_def_aux * l
-
-
-type 
-typ_lib = 
-   Typ_lib_aux of typ_lib_aux * l
-
-
 
-- 
cgit v1.2.3