diff options
Diffstat (limited to 'compiler/SynthesizeSymbolic.ml')
-rw-r--r-- | compiler/SynthesizeSymbolic.ml | 26 |
1 files changed, 15 insertions, 11 deletions
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index bdd27d0f..f7437f7e 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -6,22 +6,26 @@ open LlbcAst open SymbolicAst open Errors -let mk_mplace (meta : Meta.meta) (p : place) (ctx : Contexts.eval_ctx) : mplace = +let mk_mplace (meta : Meta.meta) (p : place) (ctx : Contexts.eval_ctx) : mplace + = let bv = Contexts.ctx_lookup_var_binder meta ctx p.var_id in { bv; projection = p.projection } -let mk_opt_mplace (meta : Meta.meta) (p : place option) (ctx : Contexts.eval_ctx) : mplace option = +let mk_opt_mplace (meta : Meta.meta) (p : place option) + (ctx : Contexts.eval_ctx) : mplace option = Option.map (fun p -> mk_mplace meta p ctx) p -let mk_opt_place_from_op (meta : Meta.meta) (op : operand) (ctx : Contexts.eval_ctx) : - mplace option = - match op with Copy p | Move p -> Some (mk_mplace meta p ctx) | Constant _ -> None +let mk_opt_place_from_op (meta : Meta.meta) (op : operand) + (ctx : Contexts.eval_ctx) : mplace option = + match op with + | Copy p | Move p -> Some (mk_mplace meta p ctx) + | Constant _ -> None let mk_emeta (m : emeta) (e : expression) : expression = Meta (m, e) -let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (place : mplace option) - (seel : symbolic_expansion option list) (el : expression list option) : - expression option = +let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) + (place : mplace option) (seel : symbolic_expansion option list) + (el : expression list option) : expression option = match el with | None -> None | Some el -> @@ -87,9 +91,9 @@ let synthesize_symbolic_expansion (meta : Meta.meta) (sv : symbolic_value) (plac in Some (Expansion (place, sv, expansion)) -let synthesize_symbolic_expansion_no_branching (meta : Meta.meta) (sv : symbolic_value) - (place : mplace option) (see : symbolic_expansion) (e : expression option) : - expression option = +let synthesize_symbolic_expansion_no_branching (meta : Meta.meta) + (sv : symbolic_value) (place : mplace option) (see : symbolic_expansion) + (e : expression option) : expression option = let el = Option.map (fun e -> [ e ]) e in synthesize_symbolic_expansion meta sv place [ Some see ] el |