From 76bf4a3853e547ae2e0327b20e4f4b89d16820b7 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Sat, 6 Apr 2019 00:07:11 +0100 Subject: Various bugfixes and improvements - Rename DeIid to Operator. It corresponds to operator in the syntax. The previous name is from when it was called deinfix in sail1. - Removed things that weren't actually common from pretty_print_common.ml, e.g. printing identifiers is backend specific. The doc_id function here was only used for a very specific use case in pretty_print_lem, so I simplified it and renamed it to doc_sia_id, as it is always used for a SIA.Id whatever that is. - There is some support for anonymous records in constructors, e.g. union Foo ('a : Type) = { MkFoo : { field1 : 'a, field2 : int } } somewhat similar to the enum syntax in Rust. I'm not sure when this was added, but there were a few odd things about it. It was desugared in the preprocessor, rather than initial_check, and the desugaring generated incorrect code for polymorphic anonymous records as above. I moved the code to initial_check, so the pre-processor now just deals with pre-processor things and not generating types, and I fixed the code to work with polymorphic types. This revealed some issues in the C backend w.r.t. polymorphic structs, which is the bulk of this commit. I also added some tests for this feature. - OCaml backend can now generate a valid string_of function for polymorphic structs, previously this would cause the ocaml to fail to compile. - Some cleanup in the Sail ott definition - Add support for E_var in interpreter previously this would just cause the interpreter to fail --- src/interpreter.ml | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/interpreter.ml') diff --git a/src/interpreter.ml b/src/interpreter.ml index 1e1bb816..f01a3846 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -448,6 +448,11 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = let record = coerce_record (value_of_exp exp) in return (exp_of_value (StringMap.find (string_of_id id) record)) + | E_var (lexp, exp, E_aux (E_block body, _)) -> + wrap (E_block (E_aux (E_assign (lexp, exp), annot) :: body)) + | E_var (lexp, exp, body) -> + wrap (E_block [E_aux (E_assign (lexp, exp), annot); body]) + | E_assign (lexp, exp) when not (is_value exp) -> step exp >>= fun exp' -> wrap (E_assign (lexp, exp')) | E_assign (LEXP_aux (LEXP_memory (id, args), _), exp) -> wrap (E_app (id, args @ [exp])) | E_assign (LEXP_aux (LEXP_field (lexp, id), ul), exp) -> -- cgit v1.2.3