diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/SymbolicToPure.ml | 47 | ||||
| -rw-r--r-- | compiler/Translate.ml | 1 |
2 files changed, 15 insertions, 33 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 93e6cb4e..e2787271 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -213,17 +213,6 @@ type bs_ctx = { The option is [None] before we detect the ended input abstraction, and [Some] afterwards. *) - loop_backward_outputs : var list option; - (** Same as {!backward_outputs}, but for loops (if we entered a loop). - - TODO: merge with [backward_outputs]? - - [None] if we are not inside a loop, [Some] otherwise (and whatever - the kind of function we are translating: it will be [Some] even - though we are synthesizing a forward function). - - TODO: move to {!loop_info} - *) calls : call_info V.FunCallId.Map.t; (** The function calls we encountered so far *) abstractions : (V.abs * texpression list) V.AbstractionId.Map.t; @@ -1744,13 +1733,7 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool) (* Backward *) (* Group the variables in which we stored the values we need to give back. * See the explanations for the [SynthInput] case in [translate_end_abstraction] *) - let backward_outputs = - if ctx.inside_loop then - (* We are synthesizing a loop body *) - Option.get ctx.loop_backward_outputs - else (* Regular function *) - Option.get ctx.backward_outputs - in + let backward_outputs = Option.get ctx.backward_outputs in let field_values = List.map mk_texpression_from_var backward_outputs in mk_simpl_tuple_texpression field_values in @@ -1950,20 +1933,20 @@ and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) the standard body of a function. *) let ctx, given_back_variables = - if ctx.inside_loop then - (* We are synthesizing a loop body *) - let loop_id = Option.get ctx.loop_id in - let loop = LoopId.Map.find loop_id ctx.loops in - let tys = RegionGroupId.Map.find bid loop.back_outputs in - let vars = List.map (fun ty -> (None, ty)) tys in - let ctx, vars = fresh_vars vars ctx in - ({ ctx with loop_backward_outputs = Some vars }, vars) - else - (* Regular function body *) - let back_sg = RegionGroupId.Map.find bid ctx.sg.back_sg in - let vars = List.combine back_sg.output_names back_sg.outputs in - let ctx, vars = fresh_vars vars ctx in - ({ ctx with backward_outputs = Some vars }, vars) + let vars = + if ctx.inside_loop then + (* We are synthesizing a loop body *) + let loop_id = Option.get ctx.loop_id in + let loop = LoopId.Map.find loop_id ctx.loops in + let tys = RegionGroupId.Map.find bid loop.back_outputs in + List.map (fun ty -> (None, ty)) tys + else + (* Regular function body *) + let back_sg = RegionGroupId.Map.find bid ctx.sg.back_sg in + List.combine back_sg.output_names back_sg.outputs + in + let ctx, vars = fresh_vars vars ctx in + ({ ctx with backward_outputs = Some vars }, vars) in (* Get the list of values consumed by the abstraction upon ending *) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 0fa0202b..631a5af9 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -172,7 +172,6 @@ let translate_function_to_pure (trans_ctx : trans_ctx) (* Initialized just below *) backward_inputs_with_state = RegionGroupId.Map.empty; backward_outputs = None; - loop_backward_outputs = None; (* Empty for now *) calls; abstractions; |