From 8b6f8e5fb85bcd1b3257550270c4c857d4ee7f55 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 9 Nov 2022 18:04:03 +0100
Subject: Implement the generation of stateful backward functions (controlled
 by an option)

---
 compiler/SymbolicAst.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'compiler/SymbolicAst.ml')

diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index 528d8255..9d9adf4f 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -77,6 +77,14 @@ type expression =
           We use it to compute meaningful names for the variables we introduce,
           to prettify the generated code.
        *)
+  | ForwardEnd of expression
+      (** We use this delimiter to indicate at which point we switch to the
+          generation of code specific to the backward function(s).
+
+          TODO: use this to factorize the generation of the forward and backward
+          functions (today we replay the *whole* symbolic execution once per
+          generated function).
+       *)
   | Meta of meta * expression  (** Meta information *)
 
 and expansion =
-- 
cgit v1.2.3