Pretty printer to Lem ast added; accessed by -lem_ast on the command line

8 files changed, 524 insertions, 302 deletions

diff --git a/src/ast.lem b/src/ast.lem
index 91f61937..c3305c97 100644
--- a/src/ast.lem
+++ b/src/ast.lem
@@ -144,16 +144,6 @@ type k =  (* Internal kinds *)
  | Ki_infer (* Representing an unknown kind, inferred by context *)
 
 
-type t_arg =  (* Argument to type constructors *)
- | Typ of t
- | Nexp of ne
- | Effect of effects
- | Order of order
-
-and t_args =  (* Arguments to type constructors *)
- | T_args of list t_arg
-
-
 type pat =  (* Pattern *)
  | P_lit of lit (* literal constant pattern *)
  | P_wild (* wildcard *)
@@ -221,19 +211,15 @@ and letbind =  (* Let binding *)
  | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
 
 
-type naming_scheme_opt =  (* Optional variable-naming-scheme specification for variables of defined type *)
- | Name_sect_none
- | Name_sect_some of string
-
-
 type index_range =  (* index specification, for bitfields in register types *)
  | BF_single of num (* single index *)
  | BF_range of num * num (* index range *)
  | BF_concat of index_range * index_range (* concatenation of index ranges *)
 
 
-type tannot_opt =  (* Optional type annotation for functions *)
- | Typ_annot_opt_some of typquant * typ
+type naming_scheme_opt =  (* Optional variable-naming-scheme specification for variables of defined type *)
+ | Name_sect_none
+ | Name_sect_some of string
 
 
 type rec_opt =  (* Optional recursive annotation for functions *)
@@ -241,13 +227,21 @@ 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 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 funcl =  (* Function clause *)
- | FCL_Funcl of id * pat * exp
+type val_spec =  (* Value type specification *)
+ | VS_val_spec of typschm * id
 
 
 type type_def =  (* Type definition body *)
@@ -258,19 +252,15 @@ type type_def =  (* Type definition body *)
  | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
 
 
-type fundef =  (* Function definition *)
- | FD_function of rec_opt * tannot_opt * effects_opt * list funcl
-
-
-type val_spec =  (* Value type specification *)
- | VS_val_spec of typschm * id
-
-
 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
+
+
 type def =  (* Top-level definition *)
  | DEF_type of type_def (* type definition *)
  | DEF_fundef of fundef (* function definition *)
@@ -285,6 +275,10 @@ 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$ *)
@@ -302,10 +296,6 @@ 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
 
@@ -316,11 +306,7 @@ indreln
 (** definitions *)
  (* defns check_t *)
 indreln
-[check_t : map id k -> t -> bool]
- and [check_ef : map id k -> effects -> bool]
- and [check_n : map id k -> ne -> bool]
- and [check_ord : map id k -> order -> bool]
- and [check_targs : map id k -> k -> t_arg -> bool](* defn check_t *)
+(* defn check_t *)
 
 check_t_var: forall E_k id .
 ( Pmap.find  id   E_k  =  Ki_typ )
@@ -466,8 +452,7 @@ check_targs E_k Ki_ord (Order order)
 (** definitions *)
  (* defns convert_typ *)
 indreln
-[convert_typ : map id k -> typ -> t -> bool]
- and [convert_targ : map id k -> k -> typ_arg -> t_arg -> bool](* defn convert_typ *)
+(* defn convert_typ *)
 
 convert_typ_var: forall E_k id .
 ( Pmap.find  id   E_k  =  Ki_typ )
@@ -509,7 +494,7 @@ and
 (** definitions *)
  (* defns check_lit *)
 indreln
-[check_lit : lit -> t -> bool](* defn check_lit *)
+(* defn check_lit *)
 
 check_lit_true: forall .
 true
@@ -568,7 +553,7 @@ check_lit L_one (T_var  bit_id )
 (** definitions *)
  (* defns check_pat *)
 indreln
-[check_pat : env -> pat -> t -> map x f_desc -> bool](* defn check_pat *)
+(* defn check_pat *)
 
 check_pat_wild: forall E_k t .
 (check_t E_k t)
diff --git a/src/ast.ml b/src/ast.ml
index 2be8a5b7..bc4e7a5d 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -72,6 +72,16 @@ kinded_id_aux =  (* optionally kind-annotated identifier *)
 
 
 type 
+nexp_constraint = 
+   NC_aux of nexp_constraint_aux * l
+
+
+type 
+kinded_id = 
+   KOpt_aux of kinded_id_aux * l
+
+
+type 
 efct_aux =  (* effect *)
    Effect_rreg (* read register *)
  | Effect_wreg (* write register *)
@@ -83,13 +93,9 @@ efct_aux =  (* effect *)
 
 
 type 
-nexp_constraint = 
-   NC_aux of nexp_constraint_aux * l
-
-
-type 
-kinded_id = 
-   KOpt_aux of kinded_id_aux * l
+quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
+   QI_id of kinded_id (* An optionally kinded identifier *)
+ | QI_const of nexp_constraint (* A constraint for this type *)
 
 
 type 
@@ -98,9 +104,8 @@ efct =
 
 
 type 
-quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
-   QI_id of kinded_id (* An optionally kinded identifier *)
- | QI_const of nexp_constraint (* A constraint for this type *)
+quant_item = 
+   QI_aux of quant_item_aux * l
 
 
 type 
@@ -117,8 +122,9 @@ effects_aux =  (* effect set, of kind $_$ *)
 
 
 type 
-quant_item = 
-   QI_aux of quant_item_aux * l
+typquant_aux =  (* type quantifiers and constraints *)
+   TypQ_tq of (quant_item) list
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
 type 
@@ -132,9 +138,8 @@ effects =
 
 
 type 
-typquant_aux =  (* type quantifiers and constraints *)
-   TypQ_tq of (quant_item) list
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+typquant = 
+   TypQ_aux of typquant_aux * l
 
 
 type 
@@ -159,11 +164,6 @@ and typ_arg =
 
 
 type 
-typquant = 
-   TypQ_aux of typquant_aux * l
-
-
-type 
 lit_aux =  (* Literal constant *)
    L_unit (* $() : _$ *)
  | L_zero (* $_ : _$ *)
@@ -281,6 +281,16 @@ 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
+
+
+type 
 naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
    Name_sect_none
  | Name_sect_some of string
@@ -292,9 +302,8 @@ type
 
 
 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 
@@ -304,18 +313,20 @@ type
 
 
 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 
-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
+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 
@@ -339,40 +350,18 @@ type
 
 
 type 
-rec_opt = 
-   Rec_aux of rec_opt_aux * l
-
-
-type 
-'a effects_opt = 
-   Effects_opt_aux of 'a effects_opt_aux * 'a annot
-
-
-type 
 'a funcl = 
    FCL_aux of 'a funcl_aux * 'a annot
 
 
 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 *)
+'a effects_opt = 
+   Effects_opt_aux of 'a effects_opt_aux * 'a annot
 
 
 type 
-t_arg =  (* Argument to type constructors *)
-   Typ of t
- | Nexp of ne
- | Effect of effects
- | Order of order
-
-and t_args =  (* Arguments to type constructors *)
-   T_args of (t_arg) list
+rec_opt = 
+   Rec_aux of rec_opt_aux * l
 
 
 type 
@@ -385,6 +374,12 @@ 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
 
@@ -395,14 +390,13 @@ type
 
 
 type 
-'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
-   DT_kind of base_kind * id
- | DT_typ of typschm * id
+'a type_def = 
+   TD_aux of 'a type_def_aux * 'a annot
 
 
 type 
-'a type_def = 
-   TD_aux of 'a type_def_aux * 'a annot
+'a default_typing_spec = 
+   DT_aux of 'a default_typing_spec_aux * 'a annot
 
 
 type 
@@ -416,11 +410,6 @@ type
 
 
 type 
-'a default_typing_spec = 
-   DT_aux of 'a default_typing_spec_aux * 'a annot
-
-
-type 
 'a def_aux =  (* Top-level definition *)
    DEF_type of 'a type_def (* type definition *)
  | DEF_fundef of 'a fundef (* function definition *)
@@ -436,6 +425,11 @@ type
 
 
 type 
+'a ctor_def_aux =  (* Datatype constructor definition clause *)
+   CT_ct of id * typschm
+
+
+type 
 'a typ_lib_aux =  (* library types and syntactic sugar for them *)
    Typ_lib_unit (* unit type with value $()$ *)
  | Typ_lib_bool (* booleans $_$ and $_$ *)
@@ -454,23 +448,18 @@ type
 
 
 type 
-'a ctor_def_aux =  (* Datatype constructor definition clause *)
-   CT_ct of id * typschm
-
-
-type 
 'a def = 
    DEF_aux of 'a def_aux * 'a annot
 
 
 type 
-'a typ_lib = 
-   Typ_lib_aux of 'a typ_lib_aux * l
+'a ctor_def = 
+   CT_aux of 'a ctor_def_aux * 'a annot
 
 
 type 
-'a ctor_def = 
-   CT_aux of 'a ctor_def_aux * 'a annot
+'a typ_lib = 
+   Typ_lib_aux of 'a typ_lib_aux * l
 
 
 type 
diff --git a/src/main.ml b/src/main.ml
index baa887f6..5698b81a 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -348,6 +348,7 @@ let _ =
 let lib = ref []
 let opt_print_version = ref false
 let opt_print_verbose = ref false
+let opt_print_lem = ref false
 let opt_file_arguments = ref ([]:string list)
 let options = Arg.align ([
   ( "-i",
@@ -361,32 +362,16 @@ let options = Arg.align ([
     Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_html)) !backends) then
                 backends := Some(Typed_ast.Target_html)::!backends),
     " generate Html");
-  ( "-hol",
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_hol)) !backends) then
-                backends := Some(Typed_ast.Target_hol)::!backends),
-    " generate HOL");
-  ( "-ocaml",
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_ocaml)) !backends) then
-                backends := Some(Typed_ast.Target_ocaml)::!backends),
-    " generate OCaml");
-  ( "-isa",
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_isa)) !backends) then
-                backends := Some(Typed_ast.Target_isa)::!backends),
-    " generate Isabelle");
-  ( "-coq",
-    Arg.Unit (fun b -> if not (List.mem (Some(Typed_ast.Target_coq)) !backends) then
-                backends := Some(Typed_ast.Target_coq)::!backends),
-    " generate Coq");
   ( "-ident",
     Arg.Unit (fun b -> if not (List.mem None !backends) then
                 backends := None::!backends),
     " generate input on stdout");*)
-(*  ( "-print_types",
-    Arg.Unit (fun b -> opt_print_types := true),
-    " print types on stdout");*)
   ( "-verbose",
     Arg.Unit (fun b -> opt_print_verbose := true),
     " pretty-print out the file");
+  ( "-lem_ast",
+    Arg.Unit (fun b -> opt_print_lem := true),
+    " pretty-print a Lem AST representation of the file");
   ( "-v",
     Arg.Unit (fun b -> opt_print_version := true),
     " print version");
@@ -406,12 +391,16 @@ let _ =
 let main() =
   if !(opt_print_version)
   then Printf.printf "L2 pre alpha \n"
-  else let parsed = (List.map (fun f -> (parse_file f))  !opt_file_arguments) in
-       let merged = List.flatten [parsed] in
-       let ast = convert_ast (List.hd merged) in
-       if !(opt_print_verbose)
-       then ((Pretty_print.pp_defs Format.std_formatter) ast)
-       else ()
+  else let parsed = (List.map (fun f -> (f,(parse_file f)))  !opt_file_arguments) in
+       let asts = (List.map (fun (f,past) -> (f,convert_ast past)) parsed) in
+       begin 
+	 (if !(opt_print_verbose)
+	  then ((Pretty_print.pp_defs Format.std_formatter) (snd (List.hd asts)))
+	  else ());
+	 (if !(opt_print_lem)
+	  then output "" Lem_ast_out asts
+	  else ());
+       end
 
 let _ =  try
     begin
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index e0c75495..23957118 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -25,12 +25,6 @@ base_kind_aux =  (* base kind *)
 
 
 type 
-id_aux =  (* Identifier *)
-   Id of x
- | DeIid of x (* remove infix status *)
-
-
-type 
 efct_aux =  (* effect *)
    Effect_rreg (* read register *)
  | Effect_wreg (* write register *)
@@ -42,13 +36,14 @@ efct_aux =  (* effect *)
 
 
 type 
-base_kind = 
-   BK_aux of base_kind_aux * l
+id_aux =  (* Identifier *)
+   Id of x
+ | DeIid of x (* remove infix status *)
 
 
 type 
-id = 
-   Id_aux of id_aux * l
+base_kind = 
+   BK_aux of base_kind_aux * l
 
 
 type 
@@ -57,6 +52,11 @@ efct =
 
 
 type 
+id = 
+   Id_aux of id_aux * l
+
+
+type 
 kind_aux =  (* kinds *)
    K_kind of (base_kind) list
 
@@ -128,11 +128,6 @@ typquant_aux =  (* type quantifiers and constraints *)
 
 
 type 
-typquant = 
-   TypQ_aux of typquant_aux * l
-
-
-type 
 lit_aux =  (* Literal constant *)
    L_unit (* $() : _$ *)
  | L_zero (* $_ : _$ *)
@@ -146,8 +141,8 @@ lit_aux =  (* Literal constant *)
 
 
 type 
-typschm_aux =  (* type scheme *)
-   TypSchm_ts of typquant * atyp
+typquant = 
+   TypQ_aux of typquant_aux * l
 
 
 type 
@@ -156,8 +151,8 @@ lit =
 
 
 type 
-typschm = 
-   TypSchm_aux of typschm_aux * l
+typschm_aux =  (* type scheme *)
+   TypSchm_ts of typquant * atyp
 
 
 type 
@@ -186,6 +181,11 @@ and fpat =
 
 
 type 
+typschm = 
+   TypSchm_aux of typschm_aux * l
+
+
+type 
 exp_aux =  (* Expression *)
    E_block of (exp) list (* block (parsing conflict with structs?) *)
  | E_id of id (* identifier *)
@@ -253,25 +253,20 @@ tannot_opt_aux =  (* Optional type annotation for functions *)
 
 
 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 *)
  | Effects_opt_effects of atyp
 
 
 type 
-funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * pat * exp
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
 
 
 type 
-naming_scheme_opt = 
-   Name_sect_aux of naming_scheme_opt_aux * l
+funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * pat * exp
 
 
 type 
@@ -285,13 +280,13 @@ and index_range =
 
 
 type 
-tannot_opt = 
-   Typ_annot_opt_aux of tannot_opt_aux * l
+naming_scheme_opt = 
+   Name_sect_aux of naming_scheme_opt_aux * l
 
 
 type 
-rec_opt = 
-   Rec_aux of rec_opt_aux * l
+tannot_opt = 
+   Typ_annot_opt_aux of tannot_opt_aux * l
 
 
 type 
@@ -300,11 +295,21 @@ effects_opt =
 
 
 type 
+rec_opt = 
+   Rec_aux of rec_opt_aux * l
+
+
+type 
 funcl = 
    FCL_aux of funcl_aux * l
 
 
 type 
+val_spec_aux =  (* Value type specification *)
+   VS_val_spec of typschm * id
+
+
+type 
 type_def_aux =  (* Type definition body *)
    TD_abbrev of id * naming_scheme_opt * typschm (* type abbreviation *)
  | TD_record of id * naming_scheme_opt * typquant * ((atyp * id)) list * bool (* struct type definition *)
@@ -314,34 +319,24 @@ type_def_aux =  (* Type definition body *)
 
 
 type 
-fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * tannot_opt * effects_opt * (funcl) list
-
-
-type 
-val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
-
-
-type 
 default_typing_spec_aux =  (* Default kinding or typing assumption *)
    DT_kind of base_kind * id
  | DT_typ of typschm * id
 
 
 type 
-type_def = 
-   TD_aux of type_def_aux * l
+fundef_aux =  (* Function definition *)
+   FD_function of rec_opt * tannot_opt * effects_opt * (funcl) list
 
 
 type 
-fundef = 
-   FD_aux of fundef_aux * l
+val_spec = 
+   VS_aux of val_spec_aux * l
 
 
 type 
-val_spec = 
-   VS_aux of val_spec_aux * l
+type_def = 
+   TD_aux of type_def_aux * l
 
 
 type 
@@ -350,6 +345,11 @@ default_typing_spec =
 
 
 type 
+fundef = 
+   FD_aux of fundef_aux * l
+
+
+type 
 def_aux =  (* Top-level definition *)
    DEF_type of type_def (* type definition *)
  | DEF_fundef of fundef (* function definition *)
@@ -365,6 +365,16 @@ def_aux =  (* Top-level definition *)
 
 
 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 $()$ *)
  | Typ_lib_bool (* booleans $_$ and $_$ *)
@@ -383,26 +393,6 @@ typ_lib_aux =  (* library types and syntactic sugar for them *)
 
 
 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 *)
  | LEXP_vector of lexp * exp (* vector element *)
@@ -418,4 +408,14 @@ 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
+
+
 
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index f941bd94..d51e0c12 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1,7 +1,22 @@
 open Ast
-
 open Format
 
+let is_atomic_typ (Typ_aux(t,_)) =
+  match t with
+  | Typ_var _ | Typ_tup _ -> true
+  | _ -> false
+let is_atomic_nexp (Nexp_aux(n,_)) =
+  match n with
+  | Nexp_id _ | Nexp_constant _ | Nexp_exp _ -> true
+  | _ -> false
+ 
+let is_atomic_pat (P_aux(p,l)) =
+  match p with
+  | P_lit(_) | P_wild | P_id(_) | P_as _ | P_typ _ -> true
+  | P_app(_,pats) -> if (pats = []) then true else false
+  | P_record(_,_) | P_vector(_) | P_vector_indexed(_) | P_tup(_) | P_list(_) -> true
+  | _ -> false
+
 let rec list_format (sep : string) (fmt : 'a -> string) (ls : 'a list) : string =
   match ls with
   | [] -> ""
@@ -28,6 +43,10 @@ let pp_parens is_atomic format =
     then format ppf v
     else fprintf ppf "%a %a %a" kwd "(" format v kwd ")"
 
+(****************************************************************************
+ * source to source pretty printer
+****************************************************************************)
+
 let pp_format_id (Id_aux(i,_)) =
   match i with
   | Id(i) -> i
@@ -49,22 +68,6 @@ let pp_format_kind (K_aux(K_kind(klst),_)) =
 
 let pp_kind ppf k = base ppf (pp_format_kind k)
 
-let is_atomic_typ (Typ_aux(t,_)) =
-  match t with
-  | Typ_var _ | Typ_tup _ -> true
-  | _ -> false
-let is_atomic_nexp (Nexp_aux(n,_)) =
-  match n with
-  | Nexp_id _ | Nexp_constant _ | Nexp_exp _ -> true
-  | _ -> false
- 
-let is_atomic_pat (P_aux(p,l)) =
-  match p with
-  | P_lit(_) | P_wild | P_id(_) | P_as _ | P_typ _ -> true
-  | P_app(_,pats) -> if (pats = []) then true else false
-  | P_record(_,_) | P_vector(_) | P_vector_indexed(_) | P_tup(_) | P_list(_) -> true
-  | _ -> false
-
 let rec pp_format_typ (Typ_aux(t,_)) =
   match t with
   | Typ_var(id) -> pp_format_id id
@@ -329,3 +332,294 @@ let pp_def ppf (DEF_aux(d,(l,_))) =
 
 let pp_defs ppf (Defs(defs)) =
   fprintf ppf "@[%a@]@\n" (list_pp pp_def pp_def) defs
+
+
+(****************************************************************************
+ * source to Lem ast pretty printer
+****************************************************************************)
+
+let pp_format_id_lem (Id_aux(i,_)) =
+  match i with
+  | Id(i) -> "(Id " ^ i ^ ")"
+  | DeIid(x) -> "(DeIid " ^ x ^ ")"
+
+let pp_lem_id ppf id = base ppf (pp_format_id_lem id)
+
+let pp_format_bkind_lem (BK_aux(k,_)) =
+  match k with
+  | BK_type -> "BK_type"
+  | BK_nat -> "BK_nat"
+  | BK_order -> "BK_order"
+  | BK_effects -> "BK_effects"
+
+let pp_lem_bkind ppf bk = base ppf (pp_format_bkind bk)
+
+let pp_format_kind_lem (K_aux(K_kind(klst),_)) = 
+  "(K_kind [" ^ list_format "; " pp_format_bkind klst ^ "])"
+
+let pp_lem_kind ppf k = base ppf (pp_format_kind k)
+
+let rec pp_format_typ_lem (Typ_aux(t,_)) =
+  match t with
+  | Typ_var(id) -> "(Typ_var " ^ pp_format_id_lem id ^ ")"
+  | 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_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
+  | Nexp_id(id) -> "(Nexp_id " ^ pp_format_id_lem id ^ ")"
+  | Nexp_constant(i) -> "(Nexp_constant " ^ string_of_int i ^ ")"
+  | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
+  | Nexp_times(n1,n2) -> "(Nexp_times " ^  (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
+  | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")"
+and pp_format_ord_lem (Ord_aux(o,_)) = 
+  match o with
+  | Ord_id(id) -> "(Ord_id " ^ pp_format_id_lem id ^ ")"
+  | Ord_inc -> "Ord_inc"
+  | Ord_dec -> "Ord_dec"  
+and pp_format_effects_lem (Effects_aux(e,_)) =
+  match e with
+  | Effects_var(id) -> "(Effects_var " ^ pp_format_id id ^ ")"
+  | Effects_set(efcts) ->
+    "(Effects_set [" ^
+      (list_format "; " 
+         (fun (Effect_aux(e,l)) ->
+	   match e with
+	   | Effect_rreg -> "Effect_rreg"
+	   | Effect_wreg -> "Effect_wreg"
+	   | Effect_rmem -> "Effect_rmem"
+	   | Effect_wmem -> "Effect_wmem"
+	   | Effect_undef -> "Effect_undef"
+	   | Effect_unspec -> "Effect_unspec"
+	   | Effect_nondet -> "Effect_nondet")
+	 efcts) ^ " ])"
+and pp_format_typ_arg_lem (Typ_arg_aux(t,_)) = 
+  match t with
+  | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")"
+  | Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")"
+  | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")"
+  | Typ_arg_effects(e) -> "(Typ_arg_effects " ^ pp_format_effects_lem e ^ ")"
+
+let pp_lem_typ ppf t = base ppf (pp_format_typ_lem t)
+let pp_lem_nexp ppf n = base ppf (pp_format_nexp_lem n)
+let pp_lem_ord ppf o = base ppf (pp_format_ord_lem o)
+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_nat_set_bounded(id,bounds) -> "(NC_nat_set_bounded " ^ 
+    pp_format_id id ^
+      " [" ^
+      list_format "; " string_of_int bounds ^
+      "])"
+
+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_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 ^ ")") ^ ")"
+
+let pp_lem_qi ppf qi = base ppf (pp_format_qi_lem qi)
+
+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) ^
+    ")"
+
+let pp_lem_typquant ppf tq = base ppf (pp_format_typquant_lem tq)
+
+let pp_format_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),_)) =
+  "(TypSchm_ts " ^ (pp_format_typquant_lem tq) ^ " " ^ pp_format_typ_lem t ^ ")"
+ 
+let pp_lem_typscm ppf ts = base ppf (pp_format_typscm_lem ts)
+
+let pp_format_lit_lem (L_aux(l,_)) =
+  match l with
+  | L_unit -> "L_unit"
+  | L_zero -> "L_zero"
+  | L_one -> "L_one"
+  | L_true -> "L_true"
+  | L_false -> "L_false"
+  | L_num(i) -> "(L_num " ^ string_of_int i ^ ")"
+  | L_hex(n) -> "(L_hex " ^ n ^ ")"
+  | L_bin(n) -> "(L_bin " ^ n ^ ")"
+  | L_string(s) -> "(L_string \"" ^ s ^ "\")" 
+
+let pp_lem_lit ppf l = base ppf (pp_format_lit_lem l)
+
+let rec pp_format_pat_lem (P_aux(p,l)) =
+  match p with
+  | P_lit(lit) -> "(P_lit " ^ pp_format_lit_lem lit ^ ")"
+  | P_wild -> "P_wild"
+  | P_id(id) -> "(P_id " ^ pp_format_id_lem id ^ ")"
+  | P_as(pat,id) -> "(P_as " ^ pp_format_pat_lem pat ^ " " ^ pp_format_id_lem id ^ ")"
+  | P_typ(typ,pat) -> "(P_typ " ^ pp_format_typ_lem typ ^ " " ^ pp_format_pat_lem pat ^ ")"
+  | P_app(id,pats) -> "(P_app " ^ pp_format_id_lem id ^ " [" ^
+                      list_format "; " pp_format_pat_lem pats ^ "])"
+  | P_record(fpats,_) -> "(P_record [" ^
+                       list_format "; " (fun (FP_aux(FP_Fpat(id,fpat),_)) -> 
+			                  "(FP_Fpat " ^ pp_format_id_lem id ^ " " ^ pp_format_pat_lem fpat ^ ")") fpats
+                       ^ "])"
+  | P_vector(pats) -> "(P_vector [" ^ list_format "; " pp_format_pat_lem pats ^ "])"
+  | P_vector_indexed(ipats) ->
+    "(P_vector [" ^ list_format "; " (fun (i,p) -> string_of_int i ^ ", " ^ pp_format_pat_lem p) ipats ^ "])"
+  | P_vector_concat(pats) -> "(P_vector_concat [" ^ list_format "; " pp_format_pat_lem pats ^ "])"
+  | P_tup(pats) -> "(P_tup [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])"
+  | P_list(pats) -> "(P_list [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])"
+
+let pp_lem_pat ppf p = base ppf (pp_format_pat_lem p)
+
+let rec pp_lem_let ppf (LB_aux(lb,_)) =
+  match lb with
+  | LB_val_explicit(ts,pat,exp) -> 
+    fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "LB_val_explicit" pp_lem_typscm ts pp_lem_pat pat pp_lem_exp exp
+  | LB_val_implicit(pat,exp) -> 
+    fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val_implicit" pp_lem_pat pat  pp_lem_exp exp
+
+and pp_lem_exp ppf (E_aux(e,_)) = 
+  match e with
+  | E_block(exps) -> fprintf ppf "@[<0>%a [%a@] %a@]" 
+                                 kwd "(E_block" 
+                                 (list_pp pp_semi_lem_exp pp_lem_exp) exps
+                                 kwd ")"
+  | E_id(id) -> fprintf ppf "(%a %a)" kwd "E_id" pp_lem_id id
+  | E_lit(lit) -> fprintf ppf "(%a %a)" kwd "E_lit" pp_lem_lit lit
+  | E_cast(typ,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp 
+  | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_exp f (list_pp pp_semi_lem_exp pp_lem_exp) args
+  | E_app_infix(l,op,r) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_app_infix" pp_lem_exp l pp_lem_id op pp_lem_exp r
+  | E_tuple(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")"
+  | E_if(c,t,e) -> fprintf ppf "@[<0>(%a %a @[<1>%a@] @[<1> %a@])@]" kwd "E_if" pp_lem_exp c pp_lem_exp t pp_lem_exp e
+  | E_for(id,exp1,exp2,exp3,exp4) ->
+    fprintf ppf "@[<0>(%a %a %a %a %a@ @[<1> %a @])@]" 
+      kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_exp exp4
+  | E_vector(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps
+  | E_vector_indexed(iexps) -> 
+    let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in
+    let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in
+    fprintf ppf "@[<0>(%a [%a]) @]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps
+  | E_vector_access(v,e) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_vector_access" pp_lem_exp v pp_lem_exp e
+  | E_vector_subrange(v,e1,e2) -> 
+    fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e1 
+  | E_vector_update(v,e1,e2) -> 
+    fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_update" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2
+  | E_vector_update_subrange(v,e1,e2,e3) -> 
+    fprintf ppf "@[<0>(%a %a %a %a %a)@]" kwd "E_vector_update_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3 
+  | E_list(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_list" (list_pp pp_semi_lem_exp pp_lem_exp) exps
+  | E_cons(e1,e2) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cons" pp_lem_exp e1 pp_lem_exp e2
+  | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> 
+    fprintf ppf "@[<0>(%a [%a]))@]" kwd "E_record(FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps
+  | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),_))) ->
+    fprintf ppf "@[<0>(%a %a (%a [%a]))@]" 
+      kwd "E_record_update" pp_lem_exp exp kwd "FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps 
+  | E_field(fexp,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_field" pp_lem_exp fexp pp_lem_id id
+  | E_case(exp,pexps) -> 
+    fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_case" pp_lem_exp exp (list_pp pp_lem_case pp_lem_case) pexps
+  | E_let(leb,exp) -> fprintf ppf "@[<0>(%a %a %a) @]" kwd "E_let" pp_lem_let leb pp_lem_exp exp
+  | E_assign(lexp,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp
+
+and pp_semi_lem_exp ppf e = fprintf ppf "@[<1>%a%a@]" pp_lem_exp e kwd ";"
+
+and pp_lem_fexp ppf (FE_aux(FE_Fexp(id,exp),_)) = fprintf ppf "@[<1>(%a %a %a)@]" kwd "FE_Fexp" pp_lem_id id pp_lem_exp exp
+and pp_semi_lem_fexp ppf fexp = fprintf ppf "@[<1>(%a %a)@]" pp_lem_fexp fexp kwd ";"
+
+and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),_)) = 
+  fprintf ppf "@[<1>(%a %a@ %a)@]" kwd "Pat_exp" pp_lem_pat pat pp_lem_exp exp 
+
+and pp_lem_lexp ppf (LEXP_aux(lexp,_)) =
+  match lexp with
+  | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id
+  | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp
+  | LEXP_vector_range(v,e1,e2) -> 
+    fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v  pp_lem_exp e1 pp_lem_exp e2
+  | LEXP_field(v,id) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_field" pp_lem_lexp v pp_lem_id id
+
+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
+
+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
+
+let pp_lem_namescm ppf (Name_sect_aux(ns,_)) =
+  match ns with
+  | Name_sect_none -> fprintf ppf "Name_sect_none"
+  | Name_sect_some(s) -> fprintf ppf "(%a \"%s\")" kwd "Name_sect_some" s
+
+let rec pp_lem_range ppf (BF_aux(r,_)) =
+  match r with 
+  | BF_single(i) -> fprintf ppf "(BF_single %i)" i
+  | BF_range(i1,i2) -> fprintf ppf "(BF_range %i %i)" i1 i2
+  | BF_concat(ir1,ir2) -> fprintf ppf "(%a %a %a)" kwd "BF_concat" pp_lem_range ir1 pp_lem_range ir2
+
+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
+  | 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" 
+      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" 
+      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"
+      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"
+     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,_)) =
+  match r with
+  | Rec_nonrec -> fprintf ppf "Rec_nonrec"
+  | Rec_rec -> fprintf ppf "Rec_rec"
+
+let pp_lem_tannot_opt ppf (Typ_annot_opt_aux(t,_)) =
+  match t with
+  | Typ_annot_opt_some(tq,typ) -> fprintf ppf "(Typ_annot_opt_some %a %a)" pp_lem_typquant tq pp_lem_typ typ
+
+let pp_lem_effects_opt ppf (Effects_opt_aux(e,_)) =
+  match e with
+  | Effects_opt_pure -> fprintf ppf "Effects_opt_pure"
+  | Effects_opt_effects e -> fprintf ppf "(Effects_opt_effects %a)" pp_effects e
+
+let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
+  fprintf ppf "@[<0>(%a %a %a %a)@]@\n" kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp 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" 
+    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
+  | _ -> raise (Reporting_basic.err_unreachable l "initial_check didn't remove all scattered Defs")
+
+let pp_lem_defs ppf (Defs(defs)) =
+  fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs
diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index ebe9301a..d1ea2479 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -2,4 +2,8 @@ open Ast
 open Type_internal
 open Format
 
+(* Prints on formatter the defs following source syntax *)
 val pp_defs : Format.formatter -> tannot defs -> unit
+
+(* Prints on formatter the defs as Lem Ast nodes *)
+val pp_lem_defs : Format.formatter -> tannot defs -> unit
diff --git a/src/process_file.ml b/src/process_file.ml
index e642baf5..a73eeac3 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -46,6 +46,10 @@
 
 open Type_internal
 
+type out_type =
+  | Lem_ast_out
+  | Lem_out
+
 (* let r = Ulib.Text.of_latin1 *)
 
 let get_lexbuf fn =
@@ -72,34 +76,10 @@ let parse_file (f : string) : Parse_ast.defs =
 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
 
-(* type instances = Types.instance list Types.Pfmap.t
-
-let check_ast (ts : Typed_ast.Targetset.t) (mod_path : Name.t list)
-      ((tdefs,env) : ((Types.type_defs * instances) * Typed_ast.env))
-      (ast, end_lex_skips)
-      : (Types.type_defs * instances * instances) * Typed_ast.env * (Typed_ast.def list * Ast.lex_skips) =
-  try
-    let (defs,env,tast) =
-      Typecheck.check_defs ts mod_path tdefs env ast
-    in
-      (defs,env,(tast,end_lex_skips))
-  with
-    | Ident.No_type(l,m) ->
-        raise (Reporting_basic.Fatal_error (Reporting_basic.Err_type (l, m)))
-
-let check_ast_as_module (ts : Typed_ast.Targetset.t) (mod_path : Name.t list)
-      (e : ((Types.type_defs * instances) * Typed_ast.env))
-      (mod_name : Ulib.Text.t) (ast, end_lex_skips)
-      : (Types.type_defs * instances * instances) * Typed_ast.env * (Typed_ast.def list * Ast.lex_skips) =
-  check_ast ts mod_path e
-    (Ast.Defs([(Ast.Def_l(Ast.Module(None, Ast.X_l((None,mod_name),Ast.Unknown), None, None, ast, None), Ast.Unknown),
-                None,
-                false)]), end_lex_skips)
-
-
 let open_output_with_check file_name =
   let (temp_file_name, o) = Filename.open_temp_file "lem_temp" "" in
-  (o, (o, temp_file_name, file_name))
+  let o' = Format.formatter_of_out_channel o in
+  (o', (o, temp_file_name, file_name))
 
 let always_replace_files = ref true
 
@@ -111,9 +91,9 @@ let close_output_with_check (o, temp_file_name, file_name) =
   ()
 
 let generated_line f =
-  Printf.sprintf "Generated by Lem from %s." f
+  Printf.sprintf "Generated by XX from %s." f
 
-let tex_preamble =
+(*let tex_preamble =
   "\\documentclass{article}\n" ^
   "\\usepackage{amsmath,amssymb}\n" ^
   "\\usepackage{color}\n" ^
@@ -148,20 +128,20 @@ let html_postamble =
 "</pre>\n" ^
 "  </body>\n" ^
 "</html>\n"
+*)
 
-let output1 libpath isa_thy targ avoid type_info m alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum =
-  let module C = struct
-    let avoid = avoid
-  end
-  in
-  let module B = Backend.Make(C) in
-  let open Typed_ast in
-  let f' = Filename.basename (Filename.chop_extension m.filename) in
-    match targ with
-      | None ->
-          let r = B.ident_defs m.typed_ast in
-            Printf.printf "%s" (Ulib.Text.to_string r)
-      | Some(Typed_ast.Target_html) ->
+let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum*) =
+  let f' = Filename.basename (Filename.chop_extension filename) in
+    match out_arg with
+      | Lem_ast_out ->
+	begin
+	  let (o, ext_o) = open_output_with_check (f' ^ ".lem") in
+	  Format.fprintf o "(* %s *)" (generated_line filename);
+	  Pretty_print.pp_lem_defs o defs;
+	  close_output_with_check ext_o
+	end
+      | Lem_out -> assert false
+(*      | Some(Typed_ast.Target_html) ->
           begin
             let r = B.html_defs m.typed_ast in
             let (o, ext_o) = open_output_with_check (f' ^ ".html") in
@@ -328,16 +308,16 @@ let output1 libpath isa_thy targ avoid type_info m alldoc_accum alldoc_inc_accum
               Printf.fprintf o "Open Scope string_scope.\n\n";
               Printf.fprintf o "%s" (Ulib.Text.to_string r);
               close_output_with_check ext_o
-          end
+          end*)
 
-let output libpath isa_thy targ consts type_info mods alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum =
+let output libpath out_arg files (*alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum*) =
   List.iter
-    (fun m ->
-       output1 libpath isa_thy targ consts type_info m alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum)
-    mods
+    (fun (f, defs) ->
+       output1 libpath out_arg f defs (*alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum*))
+    files
 
 
-let output_alldoc f' fs alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum =
+(*let output_alldoc f' fs alldoc_accum alldoc_inc_accum alldoc_inc_usage_accum =
   let rs = !alldoc_accum in
   let (o, ext_o) = open_output_with_check (f' ^ ".tex") in
   Printf.fprintf o "%%%s\n" (generated_line fs);
diff --git a/src/process_file.mli b/src/process_file.mli
index f01aa251..8dde8e02 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -44,43 +44,25 @@
 (*  IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.                         *)
 (**************************************************************************)
 
-(* open Typed_ast *)
-
 val parse_file : string -> Parse_ast.defs
 val convert_ast : Parse_ast.defs -> Type_internal.tannot Ast.defs
 
-(* type instances = Types.instance list Types.Pfmap.t
-
-val check_ast_as_module :
-  Targetset.t ->
-  Name.t list ->
-  (Types.type_defs * instances) * env ->
-  Ulib.Text.t ->
-  Ast.defs * Ast.lex_skips ->
-  (Types.type_defs * instances * instances) * env *
-  (def list * Ast.lex_skips)
-
-val check_ast :
-  Targetset.t ->
-  Name.t list ->
-  (Types.type_defs * instances) * env ->
-  Ast.defs * Ast.lex_skips ->
-  (Types.type_defs * instances * instances) * env *
-  (def list * Ast.lex_skips)
+type out_type =
+  | Lem_ast_out
+  | Lem_out
 
 val output :
   string ->                           (* The path to the library *)
-  string ->                           (* Isabelle Theory to be included *)
-  target option ->                    (* Backend name (None for the identity backend) *)
-  Typed_ast.var_avoid_f ->
-  (Types.type_defs * instances) -> (* The full environment built after all typechecking, and transforming *)
+  out_type ->                         (* Backend kind *)
+  (string * Type_internal.tannot Ast.defs) list -> (*File names paired with definitions *)
+(*  (Types.type_defs * instances) -> (* The full environment built after all typechecking, and transforming *)
   checked_module list ->              (* The typechecked modules *)
   Ulib.Text.t list ref ->               (* alldoc accumulator *)
   Ulib.Text.t list ref ->               (* alldoc-inc accumulator *)
-  Ulib.Text.t list ref ->               (* alldoc-use_inc accumulator *)
+  Ulib.Text.t list ref ->               (* alldoc-use_inc accumulator *) *)
   unit
 
-val output_alldoc : string -> string -> Ulib.Text.t list ref -> Ulib.Text.t list ref -> Ulib.Text.t list ref -> unit
+(*val output_alldoc : string -> string -> Ulib.Text.t list ref -> Ulib.Text.t list ref -> Ulib.Text.t list ref -> unit*)
 
 (** [always_replace_files] determines whether Lem only updates modified files.
     If it is set to [true], all output files are written, regardless of whether the
@@ -89,4 +71,3 @@ val output_alldoc : string -> string -> Ulib.Text.t list ref -> Ulib.Text.t list
     backends like OCaml, HOL, Isabelle, this is benefitial, since it prevents them
     from reprocessing these unchanged files. *)
 val always_replace_files : bool ref
-*)