diff options
| author | Alasdair | 2019-04-16 00:10:45 +0100 |
|---|---|---|
| committer | Alasdair | 2019-04-16 00:10:45 +0100 |
| commit | fe7ec544b4dc832b86c2217cb4c764ed0f448b8a (patch) | |
| tree | 152e1195ca8f6d1b2de469f09dcc1bc3cf706d95 /language | |
| parent | dd4603715e0197007db780a5e4879b0ef7cd3c13 (diff) | |
SMT: Add struct value literals
Generates much better SMT that assigning each field one-by-one
starting with an undefined struct.
Diffstat (limited to 'language')
| -rw-r--r-- | language/jib.ott | 27 |
1 files changed, 14 insertions, 13 deletions
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 |