diff options
| author | Alasdair Armstrong | 2018-07-25 16:16:35 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-07-25 18:08:50 +0100 |
| commit | 7173035868aa45773c86cc555ff88de6dc9b0999 (patch) | |
| tree | 55080d2a5977a74d3fe1feaefc69a5c0b4901de9 /src/rewriter.mli | |
| parent | 4a2d0a9f0bcd6b3d0cfc6f35ddc0b6757fb5d5e2 (diff) | |
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.
Diffstat (limited to 'src/rewriter.mli')
| -rw-r--r-- | src/rewriter.mli | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/src/rewriter.mli b/src/rewriter.mli index edc93e5d..eed22376 100644 --- a/src/rewriter.mli +++ b/src/rewriter.mli @@ -139,12 +139,7 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux, ; e_throw : 'exp -> 'exp_aux ; e_return : 'exp -> 'exp_aux ; e_assert : 'exp * 'exp -> 'exp_aux - ; e_internal_cast : 'a annot * 'exp -> 'exp_aux - ; e_internal_exp : 'a annot -> 'exp_aux - ; e_internal_exp_user : 'a annot * 'a annot -> 'exp_aux - ; e_comment : string -> 'exp_aux - ; e_comment_struc : 'exp -> 'exp_aux - ; e_internal_let : 'lexp * 'exp * 'exp -> 'exp_aux + ; e_var : 'lexp * 'exp * 'exp -> 'exp_aux ; e_internal_plet : 'pat * 'exp * 'exp -> 'exp_aux ; e_internal_return : 'exp -> 'exp_aux ; e_internal_value : Value.value -> 'exp_aux |