summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-01-05 23:53:38 +0100
committerSon HO2023-02-03 11:21:46 +0100
commit852ee63cb876d419d4830eb5192604d58b07b495 (patch)
treeb610c7483ecc5471c84917e56e96c1d0d870b259
parent23ceb23847f2a5cd568278a47015f4d220f138c5 (diff)
Fix an issue in translate_forward_end
Diffstat (limited to '')
-rw-r--r--compiler/SymbolicToPure.ml3
-rw-r--r--compiler/Translate.ml1
2 files changed, 3 insertions, 1 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 2c82cf93..b024f40e 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -121,6 +121,7 @@ type bs_ctx = {
bid : T.RegionGroupId.id option; (** TODO: rename *)
sg : fun_sig;
(** The function signature - useful in particular to translate [Panic] *)
+ fwd_sg : fun_sig; (** The signature of the forward function *)
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)
@@ -2196,7 +2197,7 @@ and translate_forward_end (ectx : C.eval_ctx)
(* Introduce a fresh output value for the forward function *)
let ctx, output_var =
- let output_ty = mk_simpl_tuple_ty ctx.sg.doutputs in
+ let output_ty = mk_simpl_tuple_ty ctx.fwd_sg.doutputs in
fresh_var None output_ty ctx
in
let args, ctx, out_pats =
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 10a37770..800bac00 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -127,6 +127,7 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
SymbolicToPure.bid = None;
(* Dummy for now *)
sg = forward_sig.sg;
+ fwd_sg = forward_sig.sg;
(* Will need to be updated for the backward functions *)
sv_to_var;
var_counter;