diff options
author | Son Ho | 2022-11-25 08:13:37 +0100 |
---|---|---|
committer | Son HO | 2023-02-03 11:21:46 +0100 |
commit | 59596561873162d632f3d3091485b32a76427ee9 (patch) | |
tree | 2bdeb89950981306bacff00a1e8e68b92ec0f9db /compiler/SynthesizeSymbolic.ml | |
parent | bbdd0da25b974b03d58489d3bbc2654f4f774644 (diff) |
Start implementing support for loops
Diffstat (limited to '')
-rw-r--r-- | compiler/SynthesizeSymbolic.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 5bcbd482..02b6e47c 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -155,3 +155,10 @@ let synthesize_assertion (v : V.typed_value) (e : expression option) = let synthesize_forward_end (e : expression) (el : expression T.RegionGroupId.Map.t) = Some (ForwardEnd (e, el)) + +let synthesize_loop (end_expr : expression option) + (loop_expr : expression option) : expression option = + match (end_expr, loop_expr) with + | None, None -> None + | Some end_expr, Some loop_expr -> Some (Loop { end_expr; loop_expr }) + | _ -> raise (Failure "Unreachable") |