Type rules unto coercion now represented in ott

1 files changed, 36 insertions, 36 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 934b1ec0..a4bc2545 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -76,30 +76,30 @@ type base_effect =
  | BE_aux of base_effect_aux * l
 
 
-type effect_aux =  (* effect set, of kind Effects *)
- | Effect_var of kid
- | Effect_set of list base_effect (* effect set *)
-
-
 type id_aux =  (* Identifier *)
  | Id of x
  | DeIid of x (* remove infix status *)
 
 
+type effect_aux =  (* effect set, of kind Effects *)
+ | Effect_var of kid
+ | Effect_set of list base_effect (* effect set *)
+
+
 type order_aux =  (* vector order specifications, of kind Order *)
  | Ord_var of kid (* variable *)
  | Ord_inc (* increasing (little-endian) *)
  | Ord_dec (* decreasing (big-endian) *)
 
 
-type effect = 
- | Effect_aux of effect_aux * l
-
-
 type id = 
  | Id_aux of id_aux * l
 
 
+type effect = 
+ | Effect_aux of effect_aux * l
+
+
 type order = 
  | Ord_aux of order_aux * l
 
@@ -143,19 +143,6 @@ type typquant_aux =  (* type quantifiers and constraints *)
  | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
-type lit_aux =  (* Literal constant *)
- | L_unit (* $() : unit$ *)
- | L_zero (* $bitzero : bit$ *)
- | L_one (* $bitone : bit$ *)
- | L_true (* $true : bool$ *)
- | L_false (* $false : bool$ *)
- | L_num of integer (* 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
 
@@ -181,14 +168,31 @@ and typ_arg =
  | Typ_arg_aux of typ_arg_aux * l
 
 
-type lit = 
- | L_aux of lit_aux * l
+type lit_aux =  (* Literal constant *)
+ | L_unit (* $() : unit$ *)
+ | L_zero (* $bitzero : bit$ *)
+ | L_one (* $bitone : bit$ *)
+ | L_true (* $true : bool$ *)
+ | L_false (* $false : bool$ *)
+ | L_num of integer (* 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 typschm_aux =  (* type scheme *)
  | TypSchm_ts of typquant * typ
 
 
+type lit = 
+ | L_aux of lit_aux * l
+
+
+type typschm = 
+ | TypSchm_aux of typschm_aux * l
+
+
 type pat_aux 'a =  (* Pattern *)
  | P_lit of lit (* literal constant pattern *)
  | P_wild (* wildcard *)
@@ -213,10 +217,6 @@ and fpat 'a =
  | FP_aux of (fpat_aux 'a) * annot 'a
 
 
-type typschm = 
- | TypSchm_aux of typschm_aux * l
-
-
 type reg_id_aux 'a = 
  | RI_id of id
 
@@ -318,15 +318,15 @@ type funcl_aux 'a =  (* Function clause *)
  | FCL_Funcl of id * (pat 'a) * (exp 'a)
 
 
-type tannot_opt_aux =  (* Optional type annotation for functions *)
- | Typ_annot_opt_some of typquant * typ
-
-
 type effect_opt_aux =  (* Optional effect annotation for functions *)
  | Effect_opt_pure (* sugar for empty effect set *)
  | Effect_opt_effect of effect
 
 
+type tannot_opt_aux =  (* Optional type annotation for functions *)
+ | Typ_annot_opt_some of typquant * typ
+
+
 type name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
  | Name_sect_none
  | Name_sect_some of string
@@ -349,14 +349,14 @@ type funcl 'a =
  | FCL_aux of (funcl_aux 'a) * annot 'a
 
 
-type tannot_opt = 
- | Typ_annot_opt_aux of tannot_opt_aux * l
-
-
 type effect_opt = 
  | Effect_opt_aux of effect_opt_aux * l
 
 
+type tannot_opt = 
+ | Typ_annot_opt_aux of tannot_opt_aux * l
+
+
 type name_scm_opt = 
  | Name_sect_aux of name_scm_opt_aux * l