From 4b87c34cb91485bae744cd5aa42d63493686fdd3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 30 May 2024 22:34:05 +0200
Subject: Remove the options from the functions synthesizing the symbolic AST

---
 compiler/InterpreterLoops.ml | 37 ++++++++++++-------------------------
 1 file changed, 12 insertions(+), 25 deletions(-)

(limited to 'compiler/InterpreterLoops.ml')

diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 776cb6fa..4755f0e9 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -64,10 +64,7 @@ let eval_loop_concrete (span : Meta.span) (eval_loop_body : stl_cm_fun) :
      the loop body at least once *)
   let ctx_resl = rec_eval_loop_body ctx (Continue 0) in
   (* If we evaluate in concrete mode, we shouldn't have to generate any symbolic expression *)
-  let cf el =
-    sanity_check __FILE__ __LINE__ (el = None) span;
-    None
-  in
+  let cf _ = internal_error __FILE__ __LINE__ span in
   (ctx_resl, cf)
 
 (** Evaluate a loop in symbolic mode *)
@@ -161,7 +158,7 @@ let eval_loop_symbolic (config : config) (span : span)
   (* Synthesize the loop body *)
   let (resl_loop_body, cf_loop_body) :
       (eval_ctx * statement_eval_res) list
-      * (SymbolicAst.expression list option -> eval_result) =
+      * (SymbolicAst.expression list -> eval_result) =
     (* First, evaluate the loop body starting from the **fixed-point** context *)
     let ctx_resl, cf_loop = eval_loop_body fp_ctx in
 
@@ -201,16 +198,9 @@ let eval_loop_symbolic (config : config) (span : span)
 
     (* Apply and compose *)
     let ctx_resl, cfl = List.split (List.map eval_after_loop_iter ctx_resl) in
-    let cc (el : SymbolicAst.expression list option) : eval_result =
-      match el with
-      | None -> None
-      | Some el ->
-          let el =
-            List.map
-              (fun (cf, e) -> Option.get (cf (Some e)))
-              (List.combine cfl el)
-          in
-          cf_loop (Some el)
+    let cc (el : SymbolicAst.expression list) : eval_result =
+      let el = List.map (fun (cf, e) -> cf e) (List.combine cfl el) in
+      cf_loop el
     in
 
     (ctx_resl, cc)
@@ -296,17 +286,14 @@ let eval_loop_symbolic (config : config) (span : span)
   in
 
   (* Put everything together *)
-  let cc (el : SymbolicAst.expression list option) =
+  let cc (el : SymbolicAst.expression list) =
     match el with
-    | None -> None
-    | Some el -> (
-        match el with
-        | [] -> internal_error __FILE__ __LINE__ span
-        | e :: el ->
-            let fun_end_expr = cf_fun_end (Some e) in
-            let loop_expr = cf_loop_body (Some el) in
-            S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back
-              fun_end_expr loop_expr span)
+    | [] -> internal_error __FILE__ __LINE__ span
+    | e :: el ->
+        let fun_end_expr = cf_fun_end e in
+        let loop_expr = cf_loop_body el in
+        S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back
+          fun_end_expr loop_expr span
   in
   (res_fun_end :: resl_loop_body, cc)
 
-- 
cgit v1.2.3


From 7e50cacd736fc85930bd22689fb7e2b61ddda794 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 30 May 2024 22:37:08 +0200
Subject: Remove the cps.eval_result type

---
 compiler/InterpreterLoops.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'compiler/InterpreterLoops.ml')

diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 4755f0e9..90a3afe8 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -105,7 +105,9 @@ let eval_loop_symbolic (config : config) (span : span)
      will end with a call to the loop translation
   *)
   let ((res_fun_end, cf_fun_end), fp_bl_corresp) :
-      ((eval_ctx * statement_eval_res) * (eval_result -> eval_result)) * _ =
+      ((eval_ctx * statement_eval_res)
+      * (SymbolicAst.expression -> SymbolicAst.expression))
+      * _ =
     (* First, preemptively end borrows/move values by matching the current
        context with the target context *)
     let ctx, cf_prepare =
@@ -158,7 +160,7 @@ let eval_loop_symbolic (config : config) (span : span)
   (* Synthesize the loop body *)
   let (resl_loop_body, cf_loop_body) :
       (eval_ctx * statement_eval_res) list
-      * (SymbolicAst.expression list -> eval_result) =
+      * (SymbolicAst.expression list -> SymbolicAst.expression) =
     (* First, evaluate the loop body starting from the **fixed-point** context *)
     let ctx_resl, cf_loop = eval_loop_body fp_ctx in
 
@@ -198,7 +200,7 @@ let eval_loop_symbolic (config : config) (span : span)
 
     (* Apply and compose *)
     let ctx_resl, cfl = List.split (List.map eval_after_loop_iter ctx_resl) in
-    let cc (el : SymbolicAst.expression list) : eval_result =
+    let cc (el : SymbolicAst.expression list) : SymbolicAst.expression =
       let el = List.map (fun (cf, e) -> cf e) (List.combine cfl el) in
       cf_loop el
     in
-- 
cgit v1.2.3