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/parse_ast.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/parse_ast.ml') diff --git a/src/parse_ast.ml b/src/parse_ast.ml index 2ff7b5e2..818c9340 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -109,7 +109,7 @@ kid_aux = (* identifiers with kind, ticked to differntiate from program variabl type id_aux = (* Identifier *) Id of x - | DeIid of x (* remove infix status *) + | Operator of x (* remove infix status *) type base_effect = -- cgit v1.2.3