From fe7ec544b4dc832b86c2217cb4c764ed0f448b8a Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Tue, 16 Apr 2019 00:10:45 +0100
Subject: SMT: Add struct value literals

Generates much better SMT that assigning each field one-by-one
starting with an undefined struct.
---
 language/jib.ott | 27 ++++++++++++++-------------
 1 file changed, 14 insertions(+), 13 deletions(-)

(limited to 'language')

diff --git a/language/jib.ott b/language/jib.ott
index 8177ae3a..f0fdde2b 100644
--- a/language/jib.ott
+++ b/language/jib.ott
@@ -65,19 +65,20 @@ name :: '' ::=
 % expressions, used by the aval (ANF) and cval (Jib) types.
 
 cval :: 'V_' ::=
-  | name : ctyp                                  :: :: id
-  | '&' name : ctyp                              :: :: ref
-  | value : ctyp                                 :: :: lit
-  | cval != kind id ( ctyp0 , ... , ctypn ) ctyp :: :: ctor_kind
-  | unwrap id cval ( ctyp0 , ... , ctypn ) ctyp  :: :: ctor_unwrap
-  | cval op cval'                                :: :: op
-  | cval nat0 nat1                               :: :: tuple_member
-  | op cval                                      :: :: unary
-  | string ( cval0 , ... , cvaln )               :: :: call
-  | cval . string                                :: :: field
-  | hd ( cval )                                  :: :: hd
-  | tl ( cval )                                  :: :: tl
-  | poly cval ctyp                               :: :: poly
+  | name : ctyp                                     :: :: id
+  | '&' name : ctyp                                 :: :: ref
+  | value : ctyp                                    :: :: lit
+  | struct { id0 = cval0 , ... , idn = cvaln } ctyp :: :: struct
+  | cval != kind id ( ctyp0 , ... , ctypn ) ctyp    :: :: ctor_kind
+  | unwrap id cval ( ctyp0 , ... , ctypn ) ctyp     :: :: ctor_unwrap
+  | cval op cval'                                   :: :: op
+  | cval nat0 nat1                                  :: :: tuple_member
+  | op cval                                         :: :: unary
+  | string ( cval0 , ... , cvaln )                  :: :: call
+  | cval . string                                   :: :: field
+  | hd ( cval )                                     :: :: hd
+  | tl ( cval )                                     :: :: tl
+  | poly cval ctyp                                  :: :: poly
 
 % Note that init / clear are sometimes refered to as create / kill
 
-- 
cgit v1.2.3