diff options
author | Son Ho | 2022-02-03 21:06:11 +0100 |
---|---|---|
committer | Son Ho | 2022-02-03 21:06:11 +0100 |
commit | 6a6134dbcb8039a74f38c7cdc8af63cd3b320c61 (patch) | |
tree | e4d430293eeca1a92c6048011072789fc14695ce /src/ExtractToFStar.ml | |
parent | bef57f9d4921e5e8021c086923628b16f5ea18ea (diff) |
Implement a micro pass to filter the box functions
Diffstat (limited to '')
-rw-r--r-- | src/ExtractToFStar.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 2994d95f..a3972578 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -692,6 +692,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) let _ = extract_typed_rvalue ctx fmt inside rv in () | Call call -> ( + log#ldebug (lazy ("ctx_get_function: " ^ show_fun_id call.func)); match (call.func, call.args) with | Unop unop, [ arg ] -> ctx.fmt.extract_unop (extract_texpression ctx fmt) fmt inside unop arg |