From 5cf94ad18dae917a795249d81017ba90db781bd3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 4 May 2022 15:48:41 +0200
Subject: Fix more issues

---
 src/SymbolicToPure.ml | 26 +++++++++-----------------
 src/Translate.ml      | 18 +++---------------
 2 files changed, 12 insertions(+), 32 deletions(-)

diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 66f4d608..83c045df 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -101,12 +101,8 @@ type bs_ctx = {
   fun_context : fun_context;
   fun_decl : A.fun_decl;
   bid : T.RegionGroupId.id option;  (** TODO: rename *)
-  output_ty : ty;
-      (** The output type - we use it to translate `Panic`.
-   
-       This should be the directly translated output type (i.e., no state,
-       no result).
-    *)
+  sg : fun_sig;
+      (** The function signature - useful in particular to translate `Panic` *)
   sv_to_var : var V.SymbolicValueId.Map.t;
       (** Whenever we encounter a new symbolic value (introduced because of
           a symbolic expansion or upon ending an abstraction, for instance)
@@ -1070,29 +1066,25 @@ let rec translate_expression (config : config) (e : S.expression) (ctx : bs_ctx)
     : texpression =
   match e with
   | S.Return opt_v -> translate_return config opt_v ctx
-  | Panic -> translate_panic config ctx
+  | Panic -> translate_panic ctx
   | FunCall (call, e) -> translate_function_call config call e ctx
   | EndAbstraction (abs, e) -> translate_end_abstraction config abs e ctx
   | Expansion (p, sv, exp) -> translate_expansion config p sv exp ctx
   | Meta (meta, e) -> translate_meta config meta e ctx
 
-and translate_panic (config : config) (ctx : bs_ctx) : texpression =
+and translate_panic (ctx : bs_ctx) : texpression =
   (* Here we use the function return type - note that it is ok because
    * we don't match on panics which happen inside the function body -
    * but it won't be true anymore once we translate individual blocks *)
   (* If we use a state monad, we need to add a lambda for the state variable *)
   (* Note that only forward functions return a state *)
-  if config.use_state_monad && ctx.bid <> None then
+  let output_ty = mk_simpl_tuple_ty ctx.sg.doutputs in
+  if ctx.sg.info.output_state then
     (* Create the `Fail` value *)
-    let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; ctx.output_ty ] in
+    let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in
     let ret_v = mk_result_fail_texpression ret_ty in
-    (* Add the lambda *)
-    let _, state_var =
-      fresh_var (Some ConstStrings.state_basename) mk_state_ty ctx
-    in
-    let state_pattern = mk_typed_pattern_from_var state_var None in
-    mk_abs state_pattern ret_v
-  else mk_result_fail_texpression ctx.output_ty
+    ret_v
+  else mk_result_fail_texpression output_ty
 
 and translate_return (config : config) (opt_v : V.typed_value option)
     (ctx : bs_ctx) : texpression =
diff --git a/src/Translate.ml b/src/Translate.ml
index 92261dba..a264a121 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -122,11 +122,6 @@ let translate_function_to_pure (config : C.partial_config)
 
   (* Initialize the context *)
   let forward_sig = RegularFunIdMap.find (A.Regular def_id, None) fun_sigs in
-  let forward_output_ty =
-    match forward_sig.sg.doutputs with
-    | [ ty ] -> ty
-    | _ -> failwith "Unreachable"
-  in
   let sv_to_var = V.SymbolicValueId.Map.empty in
   let var_counter = Pure.VarId.generator_zero in
   let state_var, var_counter = Pure.VarId.fresh var_counter in
@@ -146,7 +141,7 @@ let translate_function_to_pure (config : C.partial_config)
     {
       SymbolicToPure.bid = None;
       (* Dummy for now *)
-      output_ty = forward_output_ty;
+      sg = forward_sig.sg;
       (* Will need to be updated for the backward functions *)
       sv_to_var;
       var_counter;
@@ -216,10 +211,7 @@ let translate_function_to_pure (config : C.partial_config)
         let backward_sg =
           RegularFunIdMap.find (A.Regular def_id, Some back_id) fun_sigs
         in
-        let backward_output_ty = mk_simpl_tuple_ty backward_sg.sg.doutputs in
-        let ctx =
-          { ctx with bid = Some back_id; output_ty = backward_output_ty }
-        in
+        let ctx = { ctx with bid = Some back_id; sg = backward_sg.sg } in
 
         (* Translate *)
         SymbolicToPure.translate_fun_decl sp_config ctx None
@@ -255,10 +247,6 @@ let translate_function_to_pure (config : C.partial_config)
         let ctx, backward_outputs =
           SymbolicToPure.fresh_vars backward_outputs ctx
         in
-        let backward_output_tys =
-          List.map (fun (v : Pure.var) -> v.ty) backward_outputs
-        in
-        let backward_output_ty = mk_simpl_tuple_ty backward_output_tys in
         let backward_inputs =
           T.RegionGroupId.Map.singleton back_id backward_inputs
         in
@@ -271,7 +259,7 @@ let translate_function_to_pure (config : C.partial_config)
           {
             ctx with
             bid = Some back_id;
-            output_ty = backward_output_ty;
+            sg = backward_sg.sg;
             backward_inputs;
             backward_outputs;
           }
-- 
cgit v1.2.3