summaryrefslogtreecommitdiff
path: root/src/TranslateCore.ml
diff options
context:
space:
mode:
authorSidney Congard2022-06-08 12:32:14 +0200
committerSidney Congard2022-06-08 12:32:14 +0200
commitba61ed50e7b2fdc78690de92d734a3747029f903 (patch)
treed038735ea4a263f80e1752661c1c707d21810f28 /src/TranslateCore.ml
parent1b3f5a15aaabf5810f07797550d1a19a55b6be3c (diff)
read globals from LLBC JSON into functions
Diffstat (limited to 'src/TranslateCore.ml')
-rw-r--r--src/TranslateCore.ml9
1 files changed, 5 insertions, 4 deletions
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index 17c35cbf..3d3887ce 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -1,6 +1,7 @@
(** Some utilities for the translation *)
open InterpreterStatements
+open FunIdentifier
module L = Logging
module T = Types
module A = LlbcAst
@@ -14,8 +15,8 @@ let log = L.translate_log
type type_context = C.type_context [@@deriving show]
type fun_context = {
- fun_decls : A.fun_decl A.FunDeclId.Map.t;
- fun_infos : FA.fun_info A.FunDeclId.Map.t;
+ fun_decls : A.fun_decl FunDeclId.Map.t;
+ fun_infos : FA.fun_info FunDeclId.Map.t;
}
[@@deriving show]
@@ -49,6 +50,6 @@ let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
let fmt = PrintPure.mk_ast_formatter type_decls fun_decls type_params in
PrintPure.fun_decl_to_string fmt def
-let fun_decl_id_to_string (ctx : trans_ctx) (id : Pure.FunDeclId.id) : string =
+let fun_decl_id_to_string (ctx : trans_ctx) (id : FunDeclId.id) : string =
Print.fun_name_to_string
- (Pure.FunDeclId.Map.find id ctx.fun_context.fun_decls).name
+ (FunDeclId.Map.find id ctx.fun_context.fun_decls).name