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/InterpreterLoops.ml | 37 ++++++++++++------------------------- 1 file changed, 12 insertions(+), 25 deletions(-) (limited to 'compiler/InterpreterLoops.ml') diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 776cb6fa..4755f0e9 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -64,10 +64,7 @@ let eval_loop_concrete (span : Meta.span) (eval_loop_body : stl_cm_fun) : the loop body at least once *) let ctx_resl = rec_eval_loop_body ctx (Continue 0) in (* If we evaluate in concrete mode, we shouldn't have to generate any symbolic expression *) - let cf el = - sanity_check __FILE__ __LINE__ (el = None) span; - None - in + let cf _ = internal_error __FILE__ __LINE__ span in (ctx_resl, cf) (** Evaluate a loop in symbolic mode *) @@ -161,7 +158,7 @@ let eval_loop_symbolic (config : config) (span : span) (* Synthesize the loop body *) let (resl_loop_body, cf_loop_body) : (eval_ctx * statement_eval_res) list - * (SymbolicAst.expression list option -> eval_result) = + * (SymbolicAst.expression list -> eval_result) = (* First, evaluate the loop body starting from the **fixed-point** context *) let ctx_resl, cf_loop = eval_loop_body fp_ctx in @@ -201,16 +198,9 @@ let eval_loop_symbolic (config : config) (span : span) (* Apply and compose *) let ctx_resl, cfl = List.split (List.map eval_after_loop_iter ctx_resl) in - let cc (el : SymbolicAst.expression list option) : eval_result = - match el with - | None -> None - | Some el -> - let el = - List.map - (fun (cf, e) -> Option.get (cf (Some e))) - (List.combine cfl el) - in - cf_loop (Some el) + let cc (el : SymbolicAst.expression list) : eval_result = + let el = List.map (fun (cf, e) -> cf e) (List.combine cfl el) in + cf_loop el in (ctx_resl, cc) @@ -296,17 +286,14 @@ let eval_loop_symbolic (config : config) (span : span) in (* Put everything together *) - let cc (el : SymbolicAst.expression list option) = + let cc (el : SymbolicAst.expression list) = match el with - | None -> None - | Some el -> ( - match el with - | [] -> internal_error __FILE__ __LINE__ span - | e :: el -> - let fun_end_expr = cf_fun_end (Some e) in - let loop_expr = cf_loop_body (Some el) in - S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back - fun_end_expr loop_expr span) + | [] -> internal_error __FILE__ __LINE__ span + | e :: el -> + let fun_end_expr = cf_fun_end e in + let loop_expr = cf_loop_body el in + S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back + fun_end_expr loop_expr span in (res_fun_end :: resl_loop_body, cc) -- 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/InterpreterLoops.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'compiler/InterpreterLoops.ml') diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 4755f0e9..90a3afe8 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -105,7 +105,9 @@ let eval_loop_symbolic (config : config) (span : span) will end with a call to the loop translation *) let ((res_fun_end, cf_fun_end), fp_bl_corresp) : - ((eval_ctx * statement_eval_res) * (eval_result -> eval_result)) * _ = + ((eval_ctx * statement_eval_res) + * (SymbolicAst.expression -> SymbolicAst.expression)) + * _ = (* First, preemptively end borrows/move values by matching the current context with the target context *) let ctx, cf_prepare = @@ -158,7 +160,7 @@ let eval_loop_symbolic (config : config) (span : span) (* Synthesize the loop body *) let (resl_loop_body, cf_loop_body) : (eval_ctx * statement_eval_res) list - * (SymbolicAst.expression list -> eval_result) = + * (SymbolicAst.expression list -> SymbolicAst.expression) = (* First, evaluate the loop body starting from the **fixed-point** context *) let ctx_resl, cf_loop = eval_loop_body fp_ctx in @@ -198,7 +200,7 @@ let eval_loop_symbolic (config : config) (span : span) (* Apply and compose *) let ctx_resl, cfl = List.split (List.map eval_after_loop_iter ctx_resl) in - let cc (el : SymbolicAst.expression list) : eval_result = + let cc (el : SymbolicAst.expression list) : SymbolicAst.expression = let el = List.map (fun (cf, e) -> cf e) (List.combine cfl el) in cf_loop el in -- cgit v1.2.3