Fixes bugs in pretty printer to generate legal lem syntax; split ott grammar and rules for lem ast generation; created a new directory for the lem interpreter and moved the Lem ast to it.

4 files changed, 170 insertions, 473 deletions

diff --git a/src/ast.ml b/src/ast.ml
index bc4e7a5d..d280f4b8 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -109,6 +109,12 @@ quant_item =
 
 
 type 
+effects_aux =  (* effect set, of kind $_$ *)
+   Effects_var of id
+ | Effects_set of (efct) list (* effect set *)
+
+
+type 
 order_aux =  (* vector order specifications, of kind $_$ *)
    Ord_id of id (* identifier *)
  | Ord_inc (* increasing (little-endian) *)
@@ -116,25 +122,32 @@ order_aux =  (* vector order specifications, of kind $_$ *)
 
 
 type 
-effects_aux =  (* effect set, of kind $_$ *)
-   Effects_var of id
- | Effects_set of (efct) list (* effect set *)
-
-
-type 
 typquant_aux =  (* type quantifiers and constraints *)
    TypQ_tq of (quant_item) list
  | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
 type 
+effects = 
+   Effects_aux of effects_aux * l
+
+
+type 
 order = 
    Ord_aux of order_aux * l
 
 
 type 
-effects = 
-   Effects_aux of effects_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_string of string (* string constant *)
 
 
 type 
@@ -164,31 +177,13 @@ and typ_arg =
 
 
 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_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
+typschm_aux =  (* type scheme *)
+   TypSchm_ts of typquant * typ
 
 
 type 
@@ -217,6 +212,11 @@ and 'a fpat =
 
 
 type 
+typschm = 
+   TypSchm_aux of typschm_aux * l
+
+
+type 
 'a exp_aux =  (* Expression *)
    E_block of ('a exp) list (* block (parsing conflict with structs?) *)
  | E_id of id (* identifier *)
@@ -281,19 +281,14 @@ and 'a letbind =
 
 
 type 
-ne =  (* internal numeric expressions *)
-   Ne_var of id
- | Ne_const of int
- | Ne_mult of ne * ne
- | Ne_add of ne * ne
- | Ne_exp of ne
- | Ne_unary of ne
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
 
 
 type 
-naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
-   Name_sect_none
- | Name_sect_some of string
+'a funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * 'a pat * 'a exp
 
 
 type 
@@ -302,36 +297,35 @@ type
 
 
 type 
-'a funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * 'a pat * '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
 
 
 type 
-rec_opt_aux =  (* Optional recursive annotation for functions *)
-   Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
+naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+   Name_sect_none
+ | Name_sect_some of string
 
 
 type 
-k =  (* Internal kinds *)
-   Ki_typ
- | Ki_nat
- | Ki_ord
- | Ki_efct
- | Ki_val (* Representing values, for use in identifier checks *)
- | Ki_ctor of (k) list * k
- | Ki_infer (* Representing an unknown kind, inferred by context *)
+rec_opt = 
+   Rec_aux of rec_opt_aux * l
 
 
 type 
-naming_scheme_opt = 
-   Name_sect_aux of naming_scheme_opt_aux * l
+'a funcl = 
+   FCL_aux of 'a funcl_aux * 'a annot
+
+
+type 
+'a tannot_opt = 
+   Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
+
+
+type 
+'a effects_opt = 
+   Effects_opt_aux of 'a effects_opt_aux * 'a annot
 
 
 type 
@@ -345,23 +339,24 @@ and index_range =
 
 
 type 
-'a tannot_opt = 
-   Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
+naming_scheme_opt = 
+   Name_sect_aux of naming_scheme_opt_aux * l
 
 
 type 
-'a funcl = 
-   FCL_aux of 'a funcl_aux * 'a annot
+'a fundef_aux =  (* Function definition *)
+   FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
 
 
 type 
-'a effects_opt = 
-   Effects_opt_aux of 'a effects_opt_aux * 'a annot
+'a val_spec_aux =  (* Value type specification *)
+   VS_val_spec of typschm * id
 
 
 type 
-rec_opt = 
-   Rec_aux of rec_opt_aux * l
+'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
+   DT_kind of base_kind * id
+ | DT_typ of typschm * id
 
 
 type 
@@ -374,24 +369,23 @@ type
 
 
 type 
-'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
-   DT_kind of base_kind * id
- | DT_typ of typschm * id
-
-
-type 
-'a fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
+ne =  (* internal numeric expressions *)
+   Ne_var of id
+ | Ne_const of int
+ | Ne_mult of ne * ne
+ | Ne_add of ne * ne
+ | Ne_exp of ne
+ | Ne_unary of ne
 
 
 type 
-'a val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
+'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 
@@ -400,13 +394,19 @@ type
 
 
 type 
-'a fundef = 
-   FD_aux of 'a fundef_aux * 'a annot
+'a type_def = 
+   TD_aux of 'a type_def_aux * 'a annot
 
 
 type 
-'a val_spec = 
-   VS_aux of 'a val_spec_aux * 'a annot
+k =  (* Internal kinds *)
+   Ki_typ
+ | Ki_nat
+ | Ki_ord
+ | Ki_efct
+ | Ki_val (* Representing values, for use in identifier checks *)
+ | Ki_ctor of (k) list * k
+ | Ki_infer (* Representing an unknown kind, inferred by context *)
 
 
 type 
@@ -466,11 +466,5 @@ type
 'a defs =  (* Definition sequence *)
    Defs of ('a def) list
 
-(** definitions *)
-(** definitions *)
-(** definitions *)
-(** definitions *)
-(** definitions *)
-(** definitions *)
 
 
diff --git a/src/ast.lem b/src/lem_interp/ast.lem
index c3305c97..aebbebc6 100644
--- a/src/ast.lem
+++ b/src/lem_interp/ast.lem
@@ -8,7 +8,7 @@ type l =
   | Trans of string * option l
   | Range of num * num
 
-val disjoint : forall 'a . set 'a -> set 'a -> bool
+ val disjoint : forall 'a . set 'a -> set 'a -> bool
 let disjoint s1 s2 = 
   let diff = s1 inter s2 in
   diff = Pervasives.empty
@@ -32,11 +32,6 @@ val subst : forall 'a. list 'a -> list 'a -> bool
 type x = string (* identifier *)
 type ix = string (* infix identifier *)
 
-type id =  (* Identifier *)
- | Id of x
- | DeIid of x (* remove infix status *)
-
-
 type base_kind =  (* base kind *)
  | BK_type (* kind of types *)
  | BK_nat (* kind of natural number size expressions *)
@@ -44,6 +39,15 @@ type base_kind =  (* base kind *)
  | 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 nexp =  (* expression of kind $Nat$, for vector sizes and origins *)
  | Nexp_id of id (* identifier *)
  | Nexp_constant of num (* constant *)
@@ -52,10 +56,6 @@ 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 *)
@@ -66,6 +66,11 @@ 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
@@ -73,11 +78,6 @@ type nexp_constraint =  (* constraint over kind $Nat$ *)
  | NC_nat_set_bounded of id * list num
 
 
-type kinded_id =  (* optionally kind-annotated identifier *)
- | KOpt_none of id (* identifier *)
- | KOpt_kind of kind * id (* kind-annotated variable *)
-
-
 type order =  (* vector order specifications, of kind $Order$ *)
  | Ord_id of id (* identifier *)
  | Ord_inc (* increasing (little-endian) *)
@@ -94,15 +94,6 @@ 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 ne =  (* internal numeric expressions *)
- | Ne_var of id
- | Ne_const of num
- | Ne_mult of ne * ne
- | Ne_add of ne * ne
- | Ne_exp of ne
- | Ne_unary of ne
-
-
 type typ =  (* Type expressions, of kind $Type$ *)
  | Typ_wild (* Unspecified type *)
  | Typ_var of id (* Type variable *)
@@ -117,6 +108,11 @@ and typ_arg =  (* Type constructor arguments of all kinds *)
  | Typ_arg_effects of effects
 
 
+type typquant =  (* type quantifiers and constraints *)
+ | TypQ_tq of list quant_item
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+
+
 type lit =  (* Literal constant *)
  | L_unit (* $() : unit$ *)
  | L_zero (* $bitzero : bit$ *)
@@ -129,19 +125,8 @@ type lit =  (* Literal constant *)
  | 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 *)
-
-
-type k =  (* Internal kinds *)
- | Ki_typ
- | Ki_nat
- | Ki_ord
- | Ki_efct
- | Ki_val (* Representing values, for use in identifier checks *)
- | Ki_ctor of list k * k
- | Ki_infer (* Representing an unknown kind, inferred by context *)
+type typschm =  (* type scheme *)
+ | TypSchm_ts of typquant * typ
 
 
 type pat =  (* Pattern *)
@@ -162,11 +147,20 @@ and fpat =  (* Field pattern *)
  | FP_Fpat of id * pat
 
 
-type typschm =  (* type scheme *)
- | TypSchm_ts of typquant * typ
+type ne =  (* internal numeric expressions *)
+ | Ne_var of id
+ | Ne_const of num
+ | Ne_mult of ne * ne
+ | Ne_add of ne * ne
+ | Ne_exp of ne
+ | Ne_unary of ne
 
 
-type exp =  (* Expression *)
+type letbind =  (* Let binding *)
+ | LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *)
+ | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
+
+and exp =  (* Expression *)
  | E_block of list exp (* block (parsing conflict with structs?) *)
  | E_id of id (* identifier *)
  | E_lit of lit (* literal constant *)
@@ -206,9 +200,15 @@ and fexps =  (* Field-expression list *)
 and pexp =  (* Pattern match *)
  | Pat_exp of pat * exp
 
-and letbind =  (* Let binding *)
- | LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *)
- | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
+
+type k =  (* Internal kinds *)
+ | Ki_typ
+ | Ki_nat
+ | Ki_ord
+ | Ki_efct
+ | Ki_val (* Representing values, for use in identifier checks *)
+ | Ki_ctor of list k * k
+ | Ki_infer (* Representing an unknown kind, inferred by context *)
 
 
 type index_range =  (* index specification, for bitfields in register types *)
@@ -227,17 +227,22 @@ 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 effects_opt =  (* Optional effect annotation for functions *)
+ | Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of effects
 
 
 type funcl =  (* Function clause *)
  | FCL_Funcl of id * pat * exp
 
 
-type effects_opt =  (* Optional effect annotation for functions *)
- | Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of effects
+type tannot_opt =  (* Optional type annotation for functions *)
+ | Typ_annot_opt_some of typquant * typ
+
+
+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 *)
@@ -252,11 +257,6 @@ type type_def =  (* Type definition body *)
  | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
 
 
-type default_typing_spec =  (* Default kinding or typing assumption *)
- | DT_kind of base_kind * id
- | DT_typ of typschm * id
-
-
 type fundef =  (* Function definition *)
  | FD_function of rec_opt * tannot_opt * effects_opt * list funcl
 
@@ -275,10 +275,6 @@ type def =  (* Top-level definition *)
  | DEF_scattered_end of id (* scattered definition end *)
 
 
-type ctor_def =  (* Datatype constructor definition clause *)
- | CT_ct of id * typschm
-
-
 type typ_lib =  (* library types and syntactic sugar for them *)
  | Typ_lib_unit (* unit type with value $()$ *)
  | Typ_lib_bool (* booleans $true$ and $false$ *)
@@ -296,307 +292,12 @@ type typ_lib =  (* library types and syntactic sugar for them *)
  | Typ_lib_reg of typ (* mutable register components holding typ *)
 
 
+type ctor_def =  (* Datatype constructor definition clause *)
+ | CT_ct of id * typschm
+
+
 type defs =  (* Definition sequence *)
  | Defs of list def
 
-(** definitions *)
- (* defns translate_ast *)
-indreln
-
-(** definitions *)
- (* defns check_t *)
-indreln
-(* defn check_t *)
-
-check_t_var: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_typ )
- ==> 
-check_t E_k (T_var id)
-
-and
-check_t_varInfer: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_infer ) &&
-((Formula_update_k E_k id Ki_typ))
- ==> 
-check_t E_k (T_var id)
-
-and
-check_t_fn: forall E_k t1 t2 effects .
-(check_t E_k t1) &&
-(check_t E_k t2) &&
-(check_ef E_k effects)
- ==> 
-check_t E_k (T_fn t1 t2 effects)
-
-and
-check_t_tup: forall t_list E_k .
-((List.for_all (fun b -> b) ((List.map (fun t_ -> check_t E_k t_) t_list))))
- ==> 
-check_t E_k (T_tup (t_list))
-
-and
-check_t_app: forall t_arg_k_list E_k id .
-( Pmap.find  id   E_k  =  (Ki_ctor ((List.map (fun (t_arg_,k_) -> k_) t_arg_k_list)) Ki_typ) ) &&
-((List.for_all (fun b -> b) ((List.map (fun (t_arg_,k_) -> check_targs E_k k_ t_arg_) t_arg_k_list))))
- ==> 
-check_t E_k (T_app id (T_args ((List.map (fun (t_arg_,k_) -> t_arg_) t_arg_k_list))))
-
-
-and
-(* defn check_ef *)
-
-check_ef_var: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_efct )
- ==> 
-check_ef E_k (Effects_var id)
-
-and
-check_ef_varInfer: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_infer ) &&
-((Formula_update_k E_k id Ki_efct))
- ==> 
-check_ef E_k (Effects_var id)
-
-and
-check_ef_set: forall efct_list E_k .
-true
- ==> 
-check_ef E_k (Effects_set (efct_list))
-
-
-and
-(* defn check_n *)
-
-check_n_var: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_nat )
- ==> 
-check_n E_k (Ne_var id)
-
-and
-check_n_varInfer: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_infer ) &&
-((Formula_update_k E_k id Ki_nat))
- ==> 
-check_n E_k (Ne_var id)
-
-and
-check_n_num: forall E_k num .
-true
- ==> 
-check_n E_k (Ne_const num)
-
-and
-check_n_sum: forall E_k ne1 ne2 .
-(check_n E_k ne1) &&
-(check_n E_k ne2)
- ==> 
-check_n E_k (Ne_add ne1 ne2)
-
-and
-check_n_mult: forall E_k ne1 ne2 .
-(check_n E_k ne1) &&
-(check_n E_k ne2)
- ==> 
-check_n E_k (Ne_mult ne1 ne2)
-
-and
-check_n_exp: forall E_k ne .
-(check_n E_k ne)
- ==> 
-check_n E_k (Ne_exp ne)
-
-
-and
-(* defn check_ord *)
-
-check_ord_var: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_ord )
- ==> 
-check_ord E_k (Ord_id id)
-
-and
-check_ord_varInfer: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_infer ) &&
-((Formula_update_k E_k id Ki_ord))
- ==> 
-check_ord E_k (Ord_id id)
-
-
-and
-(* defn check_targs *)
-
-check_targs_typ: forall E_k t .
-(check_t E_k t)
- ==> 
-check_targs E_k Ki_typ (Typ t)
-
-and
-check_targs_eff: forall E_k effects .
-(check_ef E_k effects)
- ==> 
-check_targs E_k Ki_efct (Effect effects)
-
-and
-check_targs_nat: forall E_k ne .
-(check_n E_k ne)
- ==> 
-check_targs E_k Ki_nat (Nexp ne)
-
-and
-check_targs_ord: forall E_k order .
-(check_ord E_k order)
- ==> 
-check_targs E_k Ki_ord (Order order)
-
-
-(** definitions *)
- (* defns convert_typ *)
-indreln
-(* defn convert_typ *)
-
-convert_typ_var: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_typ )
- ==> 
-convert_typ E_k (Typ_var id) (T_var id)
-
-and
-convert_typ_fn: forall E_k typ1 typ2 effects t1 t2 .
-(convert_typ E_k typ1 t1) &&
-(convert_typ E_k typ2 t2) &&
-(check_ef E_k effects)
- ==> 
-convert_typ E_k (Typ_fn typ1 typ2 effects) (T_fn t1 t2 effects)
-
-and
-convert_typ_tup: forall typ_t_list E_k .
-((List.for_all (fun b -> b) ((List.map (fun (typ_,t_) -> convert_typ E_k typ_ t_) typ_t_list))))
- ==> 
-convert_typ E_k (Typ_tup ((List.map (fun (typ_,t_) -> typ_) typ_t_list))) (T_tup ((List.map (fun (typ_,t_) -> t_) typ_t_list)))
-
-and
-convert_typ_app: forall typ_arg_t_arg_k_list E_k id .
-( Pmap.find  id   E_k  =  (Ki_ctor ((List.map (fun (typ_arg_,t_arg_,k_) -> k_) typ_arg_t_arg_k_list)) Ki_typ) ) &&
-((List.for_all (fun b -> b) ((List.map (fun (typ_arg_,t_arg_,k_) -> convert_targ E_k k_ typ_arg_ t_arg_) typ_arg_t_arg_k_list))))
- ==> 
-convert_typ E_k (Typ_app id ((List.map (fun (typ_arg_,t_arg_,k_) -> typ_arg_) typ_arg_t_arg_k_list))) (T_app id (T_args ((List.map (fun (typ_arg_,t_arg_,k_) -> t_arg_) typ_arg_t_arg_k_list))))
-
-and
-convert_typ_eq: forall E_k typ t2 t1 .
-(convert_typ E_k typ t1)
- ==> 
-convert_typ E_k typ t2
-
-
-and
-(* defn convert_targ *)
-
-
-(** definitions *)
- (* defns check_lit *)
-indreln
-(* defn check_lit *)
-
-check_lit_true: forall .
-true
- ==> 
-check_lit L_true (T_var  bool_id )
-
-and
-check_lit_false: forall .
-true
- ==> 
-check_lit L_false (T_var  bool_id )
-
-and
-check_lit_num: forall num .
-true
- ==> 
-check_lit (L_num num) (T_var  nat_id )
-
-and
-check_lit_string: forall string .
-true
- ==> 
-check_lit (L_string string) (T_var  string_id )
-
-and
-check_lit_hex: forall hex zero num .
-( ( (Ne_const num)  =   (hlength  hex )  ) )
- ==> 
-check_lit (L_hex hex) (T_app  vector_id  (T_args ([((Nexp (Ne_const zero)))] @ [((Nexp (Ne_const num)))] @ [((Order Ord_inc))] @ [((Typ (T_var  bit_id )))])))
-
-and
-check_lit_bin: forall bin zero num .
-( ( (Ne_const num)  =   (blength  bin )  ) )
- ==> 
-check_lit (L_bin bin) (T_app  vector_id  (T_args ([((Nexp (Ne_const zero)))] @ [((Nexp (Ne_const num)))] @ [((Order Ord_inc))] @ [((Typ (T_var  bit_id )))])))
-
-and
-check_lit_unit: forall .
-true
- ==> 
-check_lit L_unit (T_var  unit_id )
-
-and
-check_lit_bitzero: forall .
-true
- ==> 
-check_lit L_zero (T_var  bit_id )
-
-and
-check_lit_bitone: forall .
-true
- ==> 
-check_lit L_one (T_var  bit_id )
-
-
-(** definitions *)
- (* defns check_pat *)
-indreln
-(* defn check_pat *)
-
-check_pat_wild: forall E_k t .
-(check_t E_k t)
- ==> 
-(PARSE_ERROR "line 1762 - 1763" "no parses (char 16): <E_t,E_k> |- _ a***nnot : t gives {}  ")
-
-and
-check_pat_as: forall E_t E_k pat id t E_t1 .
-(check_pat  (Env  E_k   E_t )  pat t E_t1) &&
-( Pervasives.not (Pmap.mem  id   E_t1 ) )
- ==> 
-check_pat  (Env  E_k   E_t )  (P_as pat id) t  (List.fold_right union_map  ([(E_t1)] @ [( (List.fold_right (fun (x,f) m -> Pmap.add x f m)  ([(id,t)])  Pmap.empty) )])  Pmap.empty) 
-
-and
-check_pat_typ: forall E_t E_k typ pat t E_t1 .
-(convert_typ E_k typ t) &&
-(check_pat  (Env  E_k   E_t )  pat t E_t1)
- ==> 
-check_pat  (Env  E_k   E_t )  (P_typ typ pat) t E_t1
-
-and
-check_pat_ident_constr: forall pat_E_t_t_list E_t E_k id t_args .
-((List.for_all (fun b -> b) ((List.map (fun (pat_,E_t_,t_) -> check_pat  (Env  E_k   E_t )  pat_ t_ E_t_) pat_E_t_t_list))))
- ==> 
-check_pat  (Env  E_k   E_t )  (P_app id ((List.map (fun (pat_,E_t_,t_) -> pat_) pat_E_t_t_list))) (T_app id t_args)  (List.fold_right union_map  ((List.map (fun (pat_,E_t_,t_) -> E_t_) pat_E_t_t_list))  Pmap.empty) 
-
-and
-check_pat_var: forall E_t E_k id t .
-(check_t E_k t)
- ==> 
-check_pat  (Env  E_k   E_t )  (P_id id) t  (List.fold_right union_map  ([(E_t)] @ [( (List.fold_right (fun (x,f) m -> Pmap.add x f m)  ([(id,t)])  Pmap.empty) )])  Pmap.empty) 
-
-and
-check_pat_tup: forall pat_t_E_t_list E_t E_k .
-((List.for_all (fun b -> b) ((List.map (fun (pat_,t_,E_t_) -> check_pat  (Env  E_k   E_t )  pat_ t_ E_t_) pat_t_E_t_list)))) &&
-( disjoint_all (List.map Pmap.domain  ((List.map (fun (pat_,t_,E_t_) -> E_t_) pat_t_E_t_list)) ) )
- ==> 
-check_pat  (Env  E_k   E_t )  (P_tup ((List.map (fun (pat_,t_,E_t_) -> pat_) pat_t_E_t_list))) (T_tup ((List.map (fun (pat_,t_,E_t_) -> t_) pat_t_E_t_list)))  (List.fold_right union_map  ((List.map (fun (pat_,t_,E_t_) -> E_t_) pat_t_E_t_list))  Pmap.empty) 
-
-
-(** definitions *)
- (* defns check_exp *)
-indreln
-
 
 
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index d51e0c12..bcc5961d 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -340,8 +340,8 @@ let pp_defs ppf (Defs(defs)) =
 
 let pp_format_id_lem (Id_aux(i,_)) =
   match i with
-  | Id(i) -> "(Id " ^ i ^ ")"
-  | DeIid(x) -> "(DeIid " ^ x ^ ")"
+  | Id(i) -> "(Id \"" ^ i ^ "\")"
+  | DeIid(x) -> "(DeIid \"" ^ x ^ "\")"
 
 let pp_lem_id ppf id = base ppf (pp_format_id_lem id)
 
@@ -352,12 +352,12 @@ let pp_format_bkind_lem (BK_aux(k,_)) =
   | BK_order -> "BK_order"
   | BK_effects -> "BK_effects"
 
-let pp_lem_bkind ppf bk = base ppf (pp_format_bkind bk)
+let pp_lem_bkind ppf bk = base ppf (pp_format_bkind_lem bk)
 
 let pp_format_kind_lem (K_aux(K_kind(klst),_)) = 
-  "(K_kind [" ^ list_format "; " pp_format_bkind klst ^ "])"
+  "(K_kind [" ^ list_format "; " pp_format_bkind_lem klst ^ "])"
 
-let pp_lem_kind ppf k = base ppf (pp_format_kind k)
+let pp_lem_kind ppf k = base ppf (pp_format_kind_lem k)
 
 let rec pp_format_typ_lem (Typ_aux(t,_)) =
   match t with
@@ -365,7 +365,7 @@ let rec pp_format_typ_lem (Typ_aux(t,_)) =
   | Typ_fn(arg,ret,efct) -> "(Typ_fn " ^ pp_format_typ_lem arg ^ " " ^ 
                              pp_format_typ_lem ret ^ " " ^
                             (pp_format_effects_lem efct) ^ ")"
-  | Typ_tup(typs) -> "(Typ_tup " ^ (list_format " " pp_format_typ_lem typs) ^ ")"
+  | Typ_tup(typs) -> "(Typ_tup [" ^ (list_format "; " pp_format_typ_lem typs) ^ "])"
   | Typ_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])"
 and pp_format_nexp_lem (Nexp_aux(n,_)) = 
   match n with
@@ -409,9 +409,9 @@ let pp_lem_effects ppf e = base ppf (pp_format_effects_lem e)
 
 let pp_format_nexp_constraint_lem (NC_aux(nc,_)) =
   match nc with
-  | NC_fixed(n1,n2) -> "(NC_fixed " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp n2 ^ ")"
-  | NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp n1 ^ " " ^ pp_format_nexp n2 ^ ")"
-  | NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp n1 ^ " " ^ pp_format_nexp n2 ^ ")"
+  | NC_fixed(n1,n2) -> "(NC_fixed " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
+  | NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
+  | NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
   | NC_nat_set_bounded(id,bounds) -> "(NC_nat_set_bounded " ^ 
     pp_format_id id ^
       " [" ^
@@ -422,12 +422,12 @@ let pp_lem_nexp_constraint ppf nc = base ppf (pp_format_nexp_constraint_lem nc)
 
 let pp_format_qi_lem (QI_aux(qi,_)) =
   match qi with
-  | QI_const(n_const) -> "(QI_const " ^ pp_format_nexp_constraint n_const ^ ")"
+  | QI_const(n_const) -> "(QI_const " ^ pp_format_nexp_constraint_lem n_const ^ ")"
   | QI_id(KOpt_aux(ki,_)) ->
     "(QI_id " ^
     (match ki with
-    | KOpt_none(id) -> "(KOpt_none " ^ pp_format_id id ^ ")"
-    | KOpt_kind(k,id) -> "(KOpt_kind " ^ pp_format_kind k ^ " " ^ pp_format_id id ^ ")") ^ ")"
+    | KOpt_none(id) -> "(KOpt_none " ^ pp_format_id_lem id ^ ")"
+    | KOpt_kind(k,id) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_id_lem id ^ ")") ^ ")"
 
 let pp_lem_qi ppf qi = base ppf (pp_format_qi_lem qi)
 
@@ -435,9 +435,9 @@ let pp_format_typquant_lem (TypQ_aux(tq,_)) =
   match tq with
   | TypQ_no_forall -> "TypQ_no_forall"
   | TypQ_tq(qlist) ->
-    "(TypQ_tq " ^ 
-    (list_format " " pp_format_qi qlist) ^
-    ")"
+    "(TypQ_tq [" ^ 
+    (list_format "; " pp_format_qi_lem qlist) ^
+    "])"
 
 let pp_lem_typquant ppf tq = base ppf (pp_format_typquant_lem tq)
 
@@ -548,8 +548,8 @@ and pp_lem_lexp ppf (LEXP_aux(lexp,_)) =
 
 let pp_lem_default ppf (DT_aux(df,_)) =
   match df with
-  | DT_kind(bk,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "DT_kind" pp_lem_bkind bk pp_lem_id id
-  | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id
+  | DT_kind(bk,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_id id
+  | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id
 
 let pp_lem_spec ppf (VS_aux(VS_val_spec(ts,id),_)) =
   fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id
@@ -568,25 +568,25 @@ let rec pp_lem_range ppf (BF_aux(r,_)) =
 let pp_lem_typdef ppf (TD_aux(td,_)) =
   match td with
   | TD_abbrev(id,namescm,typschm) -> 
-    fprintf ppf "@[<0>(%a %a %a %a)@]@\n" kwd "TD_abbrev" pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm
+    fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "TD_abbrev" pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm
   | TD_record(id,nm,typq,fs,_) -> 
     let f_pp ppf (typ,id) =
       fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in
-    fprintf ppf "@[<0>(%a %a %a %a [%a])]@\n" 
+    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
-    fprintf ppf "@[<0>(%a %a %a %a [%a])]@\n" 
+    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,_) ->
     let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in
-    fprintf ppf "@[<0>(%a %a %a [%a])@]@\n"
+    fprintf ppf "@[<0>(%a %a %a [%a] false)@]"
       kwd "TD_enum" pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums
   | TD_register(id,n1,n2,rs) -> 
     let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in
     let pp_rids = (list_pp pp_rid pp_rid) in
-    fprintf ppf "@[<0>(%a %a %a %a [%a])@]@\n"
+    fprintf ppf "@[<0>(%a %a %a %a [%a])@]"
      kwd "TD_register" pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs
 
 let pp_lem_rec ppf (Rec_aux(r,_)) =
@@ -608,17 +608,17 @@ let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
 
 let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),_)) =
   let pp_funcls ppf funcl = fprintf ppf "%a %a" kwd ";" pp_lem_funcl funcl in
-  fprintf ppf "@[<0>(%a %a %a %a [%a]@]@\n" 
+  fprintf ppf "@[<0>(%a %a %a %a [%a]@]" 
     kwd "FD_function" pp_lem_rec r pp_lem_tannot_opt typa pp_lem_effects_opt efa (list_pp pp_funcls pp_funcls) fcls
 
 let pp_lem_def ppf (DEF_aux(d,(l,_))) =
   match d with
-  | DEF_default(df) -> fprintf ppf "(DEF_default %a)" pp_lem_default df
-  | DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a)" pp_lem_spec v_spec
-  | DEF_type(t_def) -> fprintf ppf "(DEF_type %a)" pp_lem_typdef t_def
-  | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a)" pp_lem_fundef f_def
-  | DEF_val(lbind) -> fprintf ppf "(DEF_val %a)" pp_lem_let lbind
-  | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "DEF_reg_dec" pp_lem_typ typ pp_lem_id id
+  | DEF_default(df) -> fprintf ppf "(DEF_default %a);@\n" pp_lem_default df
+  | DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a);@\n" pp_lem_spec v_spec
+  | DEF_type(t_def) -> fprintf ppf "(DEF_type %a);@\n" pp_lem_typdef t_def
+  | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a);@\n" pp_lem_fundef f_def
+  | DEF_val(lbind) -> fprintf ppf "(DEF_val %a);@\n" pp_lem_let lbind
+  | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>(%a %a %a)@];@\n" kwd "DEF_reg_dec" pp_lem_typ typ pp_lem_id id
   | _ -> raise (Reporting_basic.err_unreachable l "initial_check didn't remove all scattered Defs")
 
 let pp_lem_defs ppf (Defs(defs)) =
diff --git a/src/process_file.ml b/src/process_file.ml
index a73eeac3..ce99f037 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -77,7 +77,7 @@ let convert_ast (defs : Parse_ast.defs) : Type_internal.tannot Ast.defs =
   Initial_check.to_ast Nameset.empty Type_internal.initial_kind_env Envmap.empty defs
 
 let open_output_with_check file_name =
-  let (temp_file_name, o) = Filename.open_temp_file "lem_temp" "" in
+  let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
   let o' = Format.formatter_of_out_channel o in
   (o', (o, temp_file_name, file_name))
 
@@ -136,7 +136,9 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo
       | Lem_ast_out ->
 	begin
 	  let (o, ext_o) = open_output_with_check (f' ^ ".lem") in
-	  Format.fprintf o "(* %s *)" (generated_line filename);
+	  Format.fprintf o "(* %s *)@\n" (generated_line filename);
+          Format.fprintf o "open Ast@\n";
+          Format.fprintf o "let defs = ";
 	  Pretty_print.pp_lem_defs o defs;
 	  close_output_with_check ext_o
 	end