diff options
Diffstat (limited to 'compiler/InterpreterLoops.ml')
| -rw-r--r-- | compiler/InterpreterLoops.ml | 37 |
1 files changed, 12 insertions, 25 deletions
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) |