diff options
Diffstat (limited to 'compiler/InterpreterStatements.ml')
| -rw-r--r-- | compiler/InterpreterStatements.ml | 44 |
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) |