summaryrefslogtreecommitdiff
path: root/compiler/SymbolicToPure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/SymbolicToPure.ml')
-rw-r--r--compiler/SymbolicToPure.ml12
1 files changed, 6 insertions, 6 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 8329d80e..6d01614d 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -240,7 +240,7 @@ let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
(** [back_args]: the *additional* list of inputs received by the backward function *)
let bs_ctx_register_backward_call (abs : V.abs) (back_args : texpression list)
- (ctx : bs_ctx) : bs_ctx * fun_id =
+ (ctx : bs_ctx) : bs_ctx * fun_or_op_id =
(* Insert the abstraction in the call informations *)
let back_id = abs.back_id in
let info = V.FunCallId.Map.find abs.call_id ctx.calls in
@@ -259,7 +259,7 @@ let bs_ctx_register_backward_call (abs : V.abs) (back_args : texpression list)
(* Retrieve the fun_id *)
let fun_id =
match info.forward.call_id with
- | S.Fun (fid, _) -> Regular (fid, Some abs.back_id)
+ | S.Fun (fid, _) -> Fun (FromLlbc (fid, Some abs.back_id))
| S.Unop _ | S.Binop _ -> raise (Failure "Unreachable")
in
(* Update the context and return *)
@@ -1167,7 +1167,7 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression)
match call.call_id with
| S.Fun (fid, call_id) ->
(* Regular function call *)
- let func = Regular (fid, None) in
+ let func = Fun (FromLlbc (fid, None)) in
(* Retrieve the effect information about this function (can fail,
* takes a state as input, etc.) *)
let effect_info =
@@ -1235,7 +1235,7 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression)
| None -> dest
| Some out_state -> mk_simpl_tuple_pattern [ out_state; dest ]
in
- let func = { id = Func fun_id; type_args } in
+ let func = { id = FunOrOp fun_id; type_args } in
let input_tys = (List.map (fun (x : texpression) -> x.ty)) args in
let ret_ty =
if effect_info.can_fail then mk_result_ty dest_v.ty else dest_v.ty
@@ -1390,7 +1390,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
if effect_info.can_fail then mk_result_ty output.ty else output.ty
in
let func_ty = mk_arrows input_tys ret_ty in
- let func = { id = Func func; type_args } in
+ let func = { id = FunOrOp func; type_args } in
let func = { e = Qualif func; ty = func_ty } in
let call = mk_apps func args in
(* **Optimization**:
@@ -1487,7 +1487,7 @@ and translate_assertion (config : config) (v : V.typed_value) (e : S.expression)
let monadic = true in
let v = typed_value_to_texpression ctx v in
let args = [ v ] in
- let func = { id = Func Assert; type_args = [] } in
+ let func = { id = FunOrOp (Fun (Pure Assert)); type_args = [] } in
let func_ty = mk_arrow Bool mk_unit_ty in
let func = { e = Qualif func; ty = func_ty } in
let assertion = mk_apps func args in