From 7173035868aa45773c86cc555ff88de6dc9b0999 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 25 Jul 2018 16:16:35 +0100
Subject: Remove unused internal AST nodes

E_internal_cast, E_sizeof_internal, E_internal_exp,
E_internal_exp_user, E_comment, and E_comment_struc were all
unused. For a lem based interpreter, we want to be able to compile it
to iUsabelle, and due to slowness inherent in Isabelle's datatype
package we want to remove unused constructors in our AST type.

Also remove the lem_ast backend - it's heavily bitrotted, and for
loading the ARM ast into the interpreter it's just not viable to use
this approach as it just doesn't scale. We really need a way to be
able to serialise and deserialise the AST efficiently in Lem.
---
 src/process_file.ml | 25 ++++++-------------------
 1 file changed, 6 insertions(+), 19 deletions(-)

(limited to 'src/process_file.ml')

diff --git a/src/process_file.ml b/src/process_file.ml
index 6afbae3d..958720ea 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -52,7 +52,6 @@ open PPrint
 open Pretty_print_common
 
 type out_type =
-  | Lem_ast_out
   | Lem_out of string list
   | Coq_out of string list
 
@@ -330,28 +329,16 @@ let rec iterate (f : int -> unit) (n : int) : unit =
 
 let output1 libpath out_arg filename defs  =
   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 *)@\n" (generated_line filename);
-          Format.fprintf o "open import Interp_ast@\n";
-	  Format.fprintf o "open import Pervasives@\n";
-          Format.fprintf o "(*Supply common numeric constants at the right type to alleviate repeated calls to typeclass macro*)\n";
-          iterate (fun n -> Format.fprintf o "let int%i : integer = integerFromNat %i\n" (n - 1) (n - 1)) 129;
-          Format.fprintf o "let defs = ";
-	  Pretty_print.pp_lem_defs o defs;
-	  close_output_with_check ext_o
-	end
-      | Lem_out libs ->
-        output_lem f' libs defs
-      | Coq_out libs ->
-         output_coq f' libs defs
+  match out_arg with
+  | Lem_out libs ->
+     output_lem f' libs defs
+  | Coq_out libs ->
+     output_coq f' libs defs
 
 let output libpath out_arg files =
   List.iter
     (fun (f, defs) ->
-       output1 libpath out_arg f defs)
+      output1 libpath out_arg f defs)
     files
 
 let rewrite_step defs (name,rewriter) =
-- 
cgit v1.2.3