diff options
| author | Alasdair Armstrong | 2018-03-20 17:57:20 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-03-22 18:58:59 +0000 |
| commit | e33c8546e005fba30ff882b188c86ca03d0917c8 (patch) | |
| tree | cf72fc3066962718d26a76baedd2d11a7be16946 /src/parser.mly | |
| parent | 0860deb52e55b11e39e3470290e07f861f877483 (diff) | |
Fix C compilation for CHERI and MIPS
First, the specialisation of option types has been fixed by allowing
the specialisation of constructor return types - this essentially
means that a constructor, such as Some : 'a -> option('a) can get
specialised to int -> option(int), rather than int -> option('a). This
means that these constructors are treated like GADTs internally. Since
this only happens just before the C translation, I haven't put much
effort into making this very robust so far.
Second, there was a bug in C compilation for the typing of return
expressions in non-unit contexts, which has been fixed.
Finally support for vector literals that are non-bitvectors has been
added.
Diffstat (limited to 'src/parser.mly')
| -rw-r--r-- | src/parser.mly | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/parser.mly b/src/parser.mly index 40bece90..97b6f28c 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -1164,6 +1164,8 @@ struct_fields: type_union: | id Colon typ { Tu_aux (Tu_ty_id ($3, $1), loc $startpos $endpos) } + | id Colon typ MinusGt typ + { (fun s e -> Tu_aux (Tu_ty_id (mk_typ (ATyp_fn ($3, $5, mk_typ (ATyp_set []) s e)) s e, $1), loc s e)) $startpos $endpos } type_unions: | type_union |