From 4b87c34cb91485bae744cd5aa42d63493686fdd3 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 30 May 2024 22:34:05 +0200 Subject: Remove the options from the functions synthesizing the symbolic AST --- compiler/InterpreterStatements.ml | 44 +++++++++------------------------------ 1 file changed, 10 insertions(+), 34 deletions(-) (limited to 'compiler/InterpreterStatements.ml') 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) -- cgit v1.2.3 From 7e50cacd736fc85930bd22689fb7e2b61ddda794 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 30 May 2024 22:37:08 +0200 Subject: Remove the cps.eval_result type --- compiler/InterpreterStatements.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'compiler/InterpreterStatements.ml') diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 4b4bac62..c74a1218 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -306,7 +306,9 @@ let get_assumed_function_return_type (span : Meta.span) (ctx : eval_ctx) let move_return_value (config : config) (span : Meta.span) (pop_return_value : bool) (ctx : eval_ctx) : - typed_value option * eval_ctx * (eval_result -> eval_result) = + typed_value option + * eval_ctx + * (SymbolicAst.expression -> SymbolicAst.expression) = if pop_return_value then let ret_vid = VarId.zero in let v, ctx, cc = @@ -317,7 +319,9 @@ let move_return_value (config : config) (span : Meta.span) let pop_frame (config : config) (span : Meta.span) (pop_return_value : bool) (ctx : eval_ctx) : - typed_value option * eval_ctx * (eval_result -> eval_result) = + typed_value option + * eval_ctx + * (SymbolicAst.expression -> SymbolicAst.expression) = (* Debug *) log#ldebug (lazy ("pop_frame:\n" ^ eval_ctx_to_string ~span:(Some span) ctx)); -- cgit v1.2.3