From e33c8546e005fba30ff882b188c86ca03d0917c8 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 20 Mar 2018 17:57:20 +0000
Subject: 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.
---
 src/parser.mly | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/parser.mly')

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
-- 
cgit v1.2.3