summaryrefslogtreecommitdiff
path: root/src/parse_ast.ml
diff options
context:
space:
mode:
authorAlasdair2019-04-06 00:07:11 +0100
committerAlasdair2019-04-06 01:30:27 +0100
commit76bf4a3853e547ae2e0327b20e4f4b89d16820b7 (patch)
treec237dfe772fc299bb1fd37b5035df668b0702ca3 /src/parse_ast.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/parse_ast.ml')
-rw-r--r--src/parse_ast.ml2
1 files changed, 1 insertions, 1 deletions
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 =