From 6137b6b5b788138dd02503cb1e88242a618a3677 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Thu, 14 Mar 2019 23:39:11 +0000
Subject: C: Wrap Jib identifiers

Avoids duplication between l-expressions and expressions. Also means that
special variables like current_exception and have_exception are treated
normally by functions such as instr_reads and instr_writes etc. Furthermore
we can now easily annotate Jib identifiers in ways that were not previously
possible with plain sail ids.
---
 language/jib.ott | 29 +++++++++++++++--------------
 1 file changed, 15 insertions(+), 14 deletions(-)

(limited to 'language')

diff --git a/language/jib.ott b/language/jib.ott
index e54e2ea5..5a0e3eba 100644
--- a/language/jib.ott
+++ b/language/jib.ott
@@ -47,15 +47,19 @@ open import Value2
 
 grammar
 
+name :: '' ::=
+  | id nat                :: :: name
+  | have_exception nat    :: :: have_exception
+  | current_exception nat :: :: current_exception
+  | return nat            :: :: return
+
 % Fragments are small pure snippets of (abstract) C code, mostly
-% expressions, used by the aval and cval types.
+% expressions, used by the aval (ANF) and cval (Jib) types.
 
 fragment :: 'F_' ::=
-  | id                                     :: :: id
-  | '&' id                                 :: :: ref
+  | name                                   :: :: id
+  | '&' name                               :: :: ref
   | value                                  :: :: lit
-  | have_exception                         :: :: have_exception
-  | current_exception                      :: :: current_exception
   | fragment op fragment'                  :: :: op
   | op fragment                            :: :: unary
   | string ( fragment0 , ... , fragmentn ) :: :: call
@@ -129,13 +133,10 @@ cval :: 'CV_' ::=
   {{ lem fragment * ctyp }}
 
 clexp :: 'CL_' ::=
-  | id : ctyp                :: :: id
+  | name : ctyp              :: :: id
   | clexp . string           :: :: field
   | * clexp                  :: :: addr
   | clexp . nat              :: :: tuple
-  | current_exception : ctyp :: :: current_exception
-  | have_exception           :: :: have_exception
-  | return : ctyp            :: :: return
   | void                     :: :: void
 
 ctype_def :: 'CTD_' ::=
@@ -152,14 +153,14 @@ instr :: 'I_' ::=
   {{ aux _ iannot }}
 % The following are the minimal set of instructions output by
 % Jib_compile.ml.
-  | ctyp id                                        :: :: decl
-  | ctyp id = cval                                 :: :: init
+  | ctyp name                                      :: :: decl
+  | ctyp name = cval                               :: :: init
   | jump ( cval ) string                           :: :: jump
   | goto string                                    :: :: goto
   | string :                                       :: :: label
   | clexp = bool id ( cval0 , ... , cvaln )        :: :: funcall
   | clexp = cval                                   :: :: copy
-  | clear ctyp id                                  :: :: clear
+  | clear ctyp name                                :: :: clear
   | undefined ctyp                                 :: :: undefined
   | match_failure                                  :: :: match_failure
   | end                                            :: :: end
@@ -187,8 +188,8 @@ instr :: 'I_' ::=
   | return cval                                    :: :: return
 
 % For optimising away allocations and copying.
-  | reset ctyp id                                  :: :: reset
-  | ctyp id = cval                                 :: :: reinit
+  | reset ctyp name                                :: :: reset
+  | ctyp name = cval                               :: :: reinit
   | alias clexp = cval                             :: :: alias
 
 cdef :: 'CDEF_' ::=
-- 
cgit v1.2.3