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.
---
 language/sail.ott | 36 ++++++++++++------------------------
 1 file changed, 12 insertions(+), 24 deletions(-)

(limited to 'language')

diff --git a/language/sail.ott b/language/sail.ott
index 12a71b9f..6bef08d8 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -803,12 +803,6 @@ exp :: 'E_' ::=
     {{ com halt with error $[[exp']]$ when not $[[exp]]$ }}
 % exp' is optional?
   | ( exp )                                             :: S :: paren {{ ichlo [[exp]] }}
-  | ( annot ) exp                                   :: I :: internal_cast {{ com This is an internal cast, generated during type checking that will resolve into a syntactic cast after }}
-  | annot                       :: I :: internal_exp {{ com This is an internal use for passing nexp information  to library functions, postponed for constraint solving }}
-  | sizeof annot             :: I :: sizeof_internal {{ com For sizeof during type checking, to replace nexp with internal n}}
-  | annot , annot'           :: I :: internal_exp_user {{ com This is like the above but the user has specified an implicit parameter for the current function }}
-  | comment string            :: I :: comment {{ com For generated unstructured comments }}
-  | comment exp               :: I :: comment_struc {{ com For generated structured comments }}
   | var lexp = exp in exp'    :: I :: var {{ com This is an internal node for compilation that demonstrates the scope of a local mutable variable }}
   | let pat = exp in exp' :: I :: internal_plet {{ com This is an internal node, used to distinguised some introduced lets during processing from original ones }}
   | return_int ( exp )                                          ::  :: internal_return {{ com For internal use to embed into monad definition }}
@@ -1101,10 +1095,6 @@ dec_spec :: 'DEC_' ::=
   | register alias id = alias_spec				:: :: alias
   | register alias typ id = alias_spec				:: :: typ_alias
 
-dec_comm :: 'DC_' ::= {{ com top-level generated comments }} {{auxparam 'a}}
-  | comment string :: :: comm {{ com generated unstructured comment }}
-  | comment def    :: :: comm_struct {{ com generated structured comment }}
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Top-level definitions                                        %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1117,31 +1107,29 @@ prec :: '' ::=
 def :: 'DEF_' ::=
   {{ com top-level definition }}
   {{ auxparam 'a }}
-  | kind_def                                                    :: :: kind
+  | kind_def                                         :: :: kind
     {{ com definition of named kind identifiers }}
-  | type_def                                                    :: :: type
+  | type_def                                         :: :: type
     {{ com type definition }}
-  | fundef                                                   :: :: fundef
+  | fundef                                           :: :: fundef
     {{ com function definition }}
-  | mapdef                                                   :: :: mapdef
+  | mapdef                                           :: :: mapdef
     {{ com mapping definition }}
-  | letbind                                                   :: :: val
+  | letbind                                          :: :: val
     {{ com value definition }}
-  | val_spec                                                    :: :: spec
+  | val_spec                                         :: :: spec
     {{ com top-level type constraint }}
-  | fix prec num id  :: :: fixity
+  | fix prec num id                                  :: :: fixity
     {{ com fixity declaration }}
-  |  overload id [ id1 ; ... ; idn ] :: :: overload
+  |  overload id [ id1 ; ... ; idn ]                 :: :: overload
     {{ com operator overload specification }}
-  | default_spec                                         :: :: default
+  | default_spec                                     :: :: default
     {{ com default kind and type assumptions }}
-  | scattered_def                                        :: :: scattered
+  | scattered_def                                    :: :: scattered
     {{ com scattered function and type definition }}
-  | dec_spec                                            :: :: reg_dec
+  | dec_spec                                         :: :: reg_dec
     {{ com register declaration }}
-  | dec_comm                                            :: I :: comm
-    {{ com generated comments }}
-  | fundef1 .. fundefn                                  :: I :: internal_mutrec
+  | fundef1 .. fundefn                               :: I :: internal_mutrec
     {{ com internal representation of mutually recursive functions }}
 
 defs :: '' ::=
-- 
cgit v1.2.3