Remove the options from the functions synthesizing the symbolic AST

1 files changed, 10 insertions, 34 deletions

diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index c6a65757..4b4bac62 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1035,7 +1035,7 @@ and eval_global (config : config) (span : Meta.span) (dest : place)
       let func = { func = FunId (FRegular global.body); generics } in
       let call = { func = FnOpRegular func; args = []; dest } in
       eval_transparent_function_call_concrete config span global.body call ctx
-  | SymbolicMode -> (
+  | SymbolicMode ->
       (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
        * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *)
       cassert __FILE__ __LINE__ (ty_no_regions global.ty) span
@@ -1058,12 +1058,8 @@ and eval_global (config : config) (span : Meta.span) (dest : place)
           dest ctx
       in
       ( [ (ctx, Unit) ],
-        fun el ->
-          match el with
-          | Some [ e ] ->
-              (cc_comp (S.synthesize_global_eval gid generics sval) cc) (Some e)
-          | Some _ -> internal_error __FILE__ __LINE__ span
-          | _ -> None ))
+        cc_singleton __FILE__ __LINE__ span
+          (cc_comp (S.synthesize_global_eval gid generics sval) cc) )
 
 (** Evaluate a switch *)
 and eval_switch (config : config) (span : Meta.span) (switch : switch) :
@@ -1104,8 +1100,7 @@ and eval_switch (config : config) (span : Meta.span) (switch : switch) :
             in
             let cc el =
               match cf_branches el with
-              | None -> None
-              | Some [ e_true; e_false ] -> cf_bool (Some (e_true, e_false))
+              | [ e_true; e_false ] -> cf_bool (e_true, e_false)
               | _ -> internal_error __FILE__ __LINE__ span
             in
             (ctx_resl, cc)
@@ -1160,11 +1155,8 @@ and eval_switch (config : config) (span : Meta.span) (switch : switch) :
                 (resl_branches @ [ resl_otherwise ])
             in
             let cc el =
-              match el with
-              | None -> None
-              | Some el ->
-                  let el, e_otherwise = Collections.List.pop_last el in
-                  cf_int (Some (el, e_otherwise))
+              let el, e_otherwise = Collections.List.pop_last el in
+              cf_int (el, e_otherwise)
             in
             (resl, cc_comp cc cf)
         | _ -> craise __FILE__ __LINE__ span "Inconsistent state"
@@ -1237,7 +1229,7 @@ and eval_function_call_concrete (config : config) (span : Meta.span)
       match func.func with
       | FunId (FRegular fid) ->
           eval_transparent_function_call_concrete config span fid call ctx
-      | FunId (FAssumed fid) -> (
+      | FunId (FAssumed fid) ->
           (* Continue - note that we do as if the function call has been successful,
            * by giving {!Unit} to the continuation, because we place us in the case
            * where we haven't panicked. Of course, the translation needs to take the
@@ -1245,12 +1237,7 @@ and eval_function_call_concrete (config : config) (span : Meta.span)
           let ctx, cc =
             eval_assumed_function_call_concrete config span fid call ctx
           in
-          ( [ (ctx, Unit) ],
-            fun el ->
-              match el with
-              | Some [ e ] -> cc (Some e)
-              | Some _ -> internal_error __FILE__ __LINE__ span
-              | _ -> None ))
+          ([ (ctx, Unit) ], cc_singleton __FILE__ __LINE__ span cc)
       | TraitMethod _ -> craise __FILE__ __LINE__ span "Unimplemented")
 
 and eval_function_call_symbolic (config : config) (span : Meta.span)
@@ -1353,13 +1340,7 @@ and eval_transparent_function_call_concrete (config : config) (span : Meta.span)
           ctx_resl
       in
       let ctx_resl, cfl = List.split ctx_resl_cfl in
-      let cf_pop el =
-        match el with
-        | None -> None
-        | Some el ->
-            Some
-              (List.map Option.get (List.map2 (fun cf e -> cf (Some e)) cfl el))
-      in
+      let cf_pop el = List.map2 (fun cf e -> cf e) cfl el in
       (* Continue *)
       (ctx_resl, cc_comp cc cf_pop)
 
@@ -1622,11 +1603,6 @@ and eval_function_body (config : config) (body : statement) : stl_cm_fun =
       ctx_resl
   in
   let ctx_resl, cfl = List.split ctx_res_cfl in
-  let cf_end el =
-    match el with
-    | None -> None
-    | Some el ->
-        Some (List.map Option.get (List.map2 (fun cf e -> cf (Some e)) cfl el))
-  in
+  let cf_end el = List.map2 (fun cf e -> cf e) cfl el in
   (* Compose and continue *)
   (ctx_resl, cc_comp cf_body cf_end)