summaryrefslogtreecommitdiff
path: root/src/jib/c_backend.ml
diff options
context:
space:
mode:
authorAlasdair2019-04-06 00:07:11 +0100
committerAlasdair2019-04-06 01:30:27 +0100
commit76bf4a3853e547ae2e0327b20e4f4b89d16820b7 (patch)
treec237dfe772fc299bb1fd37b5035df668b0702ca3 /src/jib/c_backend.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/jib/c_backend.ml')
-rw-r--r--src/jib/c_backend.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 0e73fed8..ee16e2e6 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -95,7 +95,7 @@ let c_error ?loc:(l=Parse_ast.Unknown) message =
let zencode_id = function
| Id_aux (Id str, l) -> Id_aux (Id (Util.zencode_string str), l)
- | Id_aux (DeIid str, l) -> Id_aux (Id (Util.zencode_string ("op " ^ str)), l)
+ | Id_aux (Operator str, l) -> Id_aux (Id (Util.zencode_string ("op " ^ str)), l)
(**************************************************************************)
(* 2. Converting sail types to C types *)