summaryrefslogtreecommitdiff
path: root/src/constant_propagation.ml
diff options
context:
space:
mode:
authorAlasdair2019-04-06 00:07:11 +0100
committerAlasdair2019-04-06 01:30:27 +0100
commit76bf4a3853e547ae2e0327b20e4f4b89d16820b7 (patch)
treec237dfe772fc299bb1fd37b5035df668b0702ca3 /src/constant_propagation.ml
parent889f129b824790694f820d7d083607796abd3efb (diff)
Various bugfixes and improvements
- Rename DeIid to Operator. It corresponds to operator <string> 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
Diffstat (limited to 'src/constant_propagation.ml')
-rw-r--r--src/constant_propagation.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml
index 6caa5ecd..5c99a534 100644
--- a/src/constant_propagation.ml
+++ b/src/constant_propagation.ml
@@ -408,7 +408,7 @@ let const_props defs ref_vars =
let env1 = env_of e1_no_casts in
let is_equal id =
List.exists (fun id' -> Id.compare id id' == 0)
- (Env.get_overloads (Id_aux (DeIid "==", Parse_ast.Unknown))
+ (Env.get_overloads (Id_aux (Operator "==", Parse_ast.Unknown))
env1)
in
let substs_true =