summaryrefslogtreecommitdiff
path: root/compiler/Translate.ml
diff options
context:
space:
mode:
authorSon Ho2023-03-07 23:31:57 +0100
committerSon HO2023-06-04 21:44:33 +0200
commitfa76f1b94e1f68d520b02c0dc1072cb73fa9d8be (patch)
tree6d301b14dc1909beff34691796c4abae88490408 /compiler/Translate.ml
parenta946df8b716695f4d387d852b7e74cf288ddb03e (diff)
Add a special expression for structure creation/update
Diffstat (limited to '')
-rw-r--r--compiler/Translate.ml10
1 files changed, 9 insertions, 1 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 6bff936b..347052a8 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -77,11 +77,19 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
let fuel, var_counter = Pure.VarId.fresh var_counter in
let calls = V.FunCallId.Map.empty in
let abstractions = V.AbstractionId.Map.empty in
+ let recursive_type_decls =
+ T.TypeDeclId.Set.of_list
+ (List.filter_map
+ (fun (tid, g) ->
+ match g with Charon.GAst.NonRec _ -> None | Rec _ -> Some tid)
+ (T.TypeDeclId.Map.bindings trans_ctx.type_context.type_decls_groups))
+ in
let type_context =
{
- SymbolicToPure.types_infos = type_context.type_infos;
+ SymbolicToPure.type_infos = type_context.type_infos;
llbc_type_decls = type_context.type_decls;
type_decls = pure_type_decls;
+ recursive_decls = recursive_type_decls;
}
in
let fun_context =