From 5758268fc5f96c82bf7eddc6ff381894107706a5 Mon Sep 17 00:00:00 2001
From: Matt Griffin <30928886+matt-j-griffin@users.noreply.github.com>
Date: Fri, 25 Apr 2025 09:31:41 +0100
Subject: [PATCH 1/3] Fix sequence rules so they reduce.

---
 bil.ott | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/bil.ott b/bil.ott
index 335c29f..15f2727 100644
--- a/bil.ott
+++ b/bil.ott
@@ -819,21 +819,18 @@ defns reduce_stmt :: '' ::=
 
  defn delta , word |- seq ~> delta' , word' , seq' :: :: seq :: '' by
 
- delta,word |- s1 ~> delta',word'
- ------------------------------------------------------------- :: seq_rec
- delta,word |- {s1; s2; ..; sn} ~> delta', word', {s2; ..; sn}
-
- delta,word |- s1 ~> delta',word'
- ------------------------------------------------------------- :: seq_last
- delta,word |- {s1; s2} ~> delta', word', {s2}
+ delta1,word1 |- s1 ~> delta2,word2
+ delta2,word2 |- {s2; ..; sn} ~> delta3, word3
+------------------------------------------------------------- :: seq_rec
+ delta1,word1 |- {s1; s2; ..; sn} ~> delta3, word3
 
  delta,word |- s1 ~> delta',word'
  ------------------------------------------------------------- :: seq_one
- delta,word |- {s1} ~> delta', word', {}
+ delta,word |- {s1} ~> delta', word'
 
 
  ------------------------------------------------------------- :: seq_nil
- delta,word |- {} ~> delta, word, {}
+ delta,word |- {} ~> delta, word
  
 defns multistep_exp :: '' ::=
 

From 161a73c781fbe51f740108d48a5a4857480c3ede Mon Sep 17 00:00:00 2001
From: Matt Griffin <30928886+matt-j-griffin@users.noreply.github.com>
Date: Fri, 25 Apr 2025 09:34:11 +0100
Subject: [PATCH 2/3] Ensure stmts use the correct sequence rules.

---
 bil.ott | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/bil.ott b/bil.ott
index 15f2727..a1c9be8 100644
--- a/bil.ott
+++ b/bil.ott
@@ -790,23 +790,23 @@ defns reduce_stmt :: '' ::=
 
 
  delta |- e ~>* true
- delta,word |- seq ~> delta',word',{}
+ delta,word |- seq ~> delta',word'
  ------------------------------------- :: ifthen_true
  delta,word |- if (e) seq ~> delta', word'
 
  delta |- e ~>* true
- delta,word |- seq ~> delta',word',{}
+ delta,word |- seq ~> delta',word'
  ------------------------------------- :: if_true
  delta,word |- if (e) seq else seq1 ~> delta', word'
 
  delta |- e ~>* false
- delta,word |- seq ~> delta',word',{}
+ delta,word |- seq ~> delta',word'
  ------------------------------------- :: if_false
  delta,word |- if (e) seq1 else seq ~> delta', word'
 
 
  delta1 |- e ~>* true
- delta1,word1 |- seq ~> delta2,word2,{}
+ delta1,word1 |- seq ~> delta2,word2
  delta2,word2 |- while (e) seq ~> delta3,word3
  --------------------------------------------- :: while
  delta1,word1 |- while (e) seq ~> delta3,word3

From 9fb9f529e2fb1b358542522e7312c95d567680e8 Mon Sep 17 00:00:00 2001
From: Matt Griffin <30928886+matt-j-griffin@users.noreply.github.com>
Date: Fri, 25 Apr 2025 09:39:19 +0100
Subject: [PATCH 3/3] Use the new sequence rule in the program step rule

---
 bil.ott | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/bil.ott b/bil.ott
index a1c9be8..85e08f9 100644
--- a/bil.ott
+++ b/bil.ott
@@ -459,7 +459,7 @@ defns program :: '' ::=
  defn delta , w , var ~> delta' , w' , var' :: :: step :: '' by
 
  delta,w,var |-> {addr=w1; size=w2; code=bil}
- delta, w1.+w2 |- bil ~> delta',w3,{}
+ delta, w1.+w2 |- bil ~> delta',w3
  ---------------------------------------------------------- :: step
  delta,w,var  ~> delta',w3,var