From 2d4be10eeadcbb6aa4cc3d48e596dfc500a0d773 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 31 May 2022 02:04:52 +0100
Subject: Update the Gible semantics with correct termination

---
 src/hls/Gible.v | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

(limited to 'src/hls/Gible.v')

diff --git a/src/hls/Gible.v b/src/hls/Gible.v
index e7378ea..0ab8c1f 100644
--- a/src/hls/Gible.v
+++ b/src/hls/Gible.v
@@ -234,7 +234,7 @@ Step Instruction
 Variant step_instr: val -> istate -> instr -> istate -> Prop :=
   | exec_RBnop:
     forall sp ist,
-      step_instr sp ist RBnop ist
+      step_instr sp (Iexec ist) RBnop (Iexec ist)
   | exec_RBop:
     forall op v res args rs m sp p ist pr,
       eval_operation ge sp op rs##args m = Some v ->
@@ -283,14 +283,15 @@ nested to describe the execution of nested lists.
 
 Inductive step_list {A} (step_i: val -> istate -> A -> istate -> Prop):
   val -> istate -> list A -> istate -> Prop :=
-| exec_RBcons:
-  forall state i state' state'' instrs sp,
-    step_i sp state i state' ->
-    step_list step_i sp state' instrs state'' ->
-    step_list step_i sp state (i :: instrs) state''
-| exec_RBnil:
-  forall state sp,
-    step_list step_i sp state nil state.
+| exec_RBcons :
+  forall state i state' state'' instrs sp cf,
+    step_i sp (Iexec state) i (Iexec state') ->
+    step_list step_i sp (Iexec state') instrs (Iterm state'' cf) ->
+    step_list step_i sp (Iexec state) (i :: instrs) (Iterm state'' cf)
+| exec_RBterm :
+  forall state sp i state' cf instrs,
+    step_i sp (Iexec state) i (Iterm state' cf) ->
+    step_list step_i sp (Iexec state) (i :: instrs) (Iterm state' cf).
 
 (*|
 Top-Level Type Definitions
-- 
cgit