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/pretty_print_coq.ml | |
| 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/pretty_print_coq.ml')
| -rw-r--r-- | src/pretty_print_coq.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 74e97a29..d2b140cd 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1296,9 +1296,7 @@ let doc_exp_lem, doc_let_lem = parens (doc_typ ctxt (typ_of r))] in align (parens (string "early_return" ^//^ expV true r ^//^ ta)) | E_constraint nc -> wrap_parens (doc_nc_exp ctxt nc) - | E_comment _ | E_comment_struc _ -> empty - | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _ - | E_internal_exp_user _ | E_internal_value _ -> + | E_internal_value _ -> raise (Reporting_basic.err_unreachable l "unsupported internal expression encountered while pretty-printing") and if_exp ctxt (elseif : bool) c t e = @@ -1918,10 +1916,6 @@ let rec doc_def unimplemented def = | DEF_kind _ -> empty - | DEF_comm (DC_comm s) -> comment (string s) - | DEF_comm (DC_comm_struct d) -> comment (doc_def unimplemented d) - - let find_exc_typ defs = let is_exc_typ_def = function | DEF_type td -> string_of_id (id_of_type_def td) = "exception" |