Kathy, Peter tweak Makefile for interactive demo and src/myocamlbuild.ml to temporarily use other version of Lem

1 files changed, 77 insertions, 77 deletions

diff --git a/language/l2.ml b/language/l2.ml
index ac7305a4..bdbec809 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -150,20 +150,6 @@ typquant_aux =  (* type quantifiers and constraints *)
 
 
 type 
-lit_aux =  (* Literal constant *)
-   L_unit (* $() : _$ *)
- | L_zero (* $_ : _$ *)
- | L_one (* $_ : _$ *)
- | L_true (* $_ : _$ *)
- | L_false (* $_ : _$ *)
- | L_num of int (* 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 = 
    TypQ_aux of typquant_aux * l
 
@@ -191,8 +177,17 @@ and typ_arg =
 
 
 type 
-lit = 
-   L_aux of lit_aux * l
+lit_aux =  (* Literal constant *)
+   L_unit (* $() : _$ *)
+ | L_zero (* $_ : _$ *)
+ | L_one (* $_ : _$ *)
+ | L_true (* $_ : _$ *)
+ | L_false (* $_ : _$ *)
+ | L_num of int (* 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 
@@ -201,6 +196,16 @@ typschm_aux =  (* type scheme *)
 
 
 type 
+lit = 
+   L_aux of lit_aux * l
+
+
+type 
+typschm = 
+   TypSchm_aux of typschm_aux * l
+
+
+type 
 'a pat_aux =  (* Pattern *)
    P_lit of lit (* literal constant pattern *)
  | P_wild (* wildcard *)
@@ -226,11 +231,6 @@ and 'a fpat =
 
 
 type 
-typschm = 
-   TypSchm_aux of typschm_aux * l
-
-
-type 
 'a reg_id_aux = 
    RI_id of id
 
@@ -319,6 +319,12 @@ type
 
 
 type 
+name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+   Name_sect_none
+ | Name_sect_some of string
+
+
+type 
 type_union_aux =  (* Type union constructors *)
    Tu_id of id
  | Tu_ty_id of typ * id
@@ -330,8 +336,9 @@ tannot_opt_aux =  (* Optional type annotation for functions *)
 
 
 type 
-'a funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * 'a pat * 'a exp
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
 
 
 type 
@@ -341,15 +348,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
-
-
-type 
-rec_opt_aux =  (* Optional recursive annotation for functions *)
-   Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
+'a funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * 'a pat * 'a exp
 
 
 type 
@@ -361,28 +361,28 @@ type
 
 
 type 
-type_union = 
-   Tu_aux of type_union_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
+type_union = 
+   Tu_aux of type_union_aux * l
 
 
 type 
-'a funcl = 
-   FCL_aux of 'a funcl_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 *)
 
-type 
-effect_opt = 
-   Effect_opt_aux of effect_opt_aux * l
+and index_range = 
+   BF_aux of index_range_aux * l
 
 
 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 
@@ -391,28 +391,18 @@ 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
+effect_opt = 
+   Effect_opt_aux of effect_opt_aux * l
 
 
 type 
-'a alias_spec = 
-   AL_aux of 'a alias_spec_aux * 'a annot
+'a funcl = 
+   FCL_aux of 'a funcl_aux * l
 
 
 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 alias_spec = 
+   AL_aux of 'a alias_spec_aux * 'a annot
 
 
 type 
@@ -425,6 +415,18 @@ type
 
 
 type 
+'a fundef_aux =  (* Function definition *)
+   FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
+
+
+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 default_spec_aux =  (* Default kinding or typing assumption *)
    DT_kind of base_kind * kid
  | DT_order of order
@@ -432,8 +434,13 @@ type
 
 
 type 
-'a fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
+'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 
@@ -444,20 +451,18 @@ 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 type_def = 
+   TD_aux of 'a type_def_aux * 'a annot
 
 
 type 
-'a scattered_def = 
-   SD_aux of 'a scattered_def_aux * 'a annot
+'a fundef = 
+   FD_aux of 'a fundef_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 
@@ -466,8 +471,8 @@ type
 
 
 type 
-'a fundef = 
-   FD_aux of 'a fundef_aux * 'a annot
+'a scattered_def = 
+   SD_aux of 'a scattered_def_aux * 'a annot
 
 
 type 
@@ -476,11 +481,6 @@ type
 
 
 type 
-'a val_spec = 
-   VS_aux of 'a val_spec_aux * 'a annot
-
-
-type 
 'a def =  (* Top-level definition *)
    DEF_type of 'a type_def (* type definition *)
  | DEF_fundef of 'a fundef (* function definition *)