diff options
author | Son Ho | 2022-01-27 15:26:20 +0100 |
---|---|---|
committer | Son Ho | 2022-01-27 15:26:20 +0100 |
commit | c821fff1b512e66f0aa588c38f952045084777ac (patch) | |
tree | 60f148fd44df9fe3819bb487d854ff6c3bf8ff3c /src/Translate.ml | |
parent | f26e6a3f00efd3f4e178c8731ddec403887caa37 (diff) |
Add more printing facilities and fix minor bugs
Diffstat (limited to '')
-rw-r--r-- | src/Translate.ml | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/Translate.ml b/src/Translate.ml index ce9f085c..58847d42 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -9,6 +9,28 @@ module SA = SymbolicAst (** The local logger *) let log = L.translate_log +type trans_ctx = { type_context : C.type_context; fun_context : C.fun_context } + +let type_def_to_string (ctx : trans_ctx) (def : Pure.type_def) : string = + let type_params = def.type_params in + let type_defs = ctx.type_context.type_defs in + let fmt = PrintPure.mk_type_formatter type_defs type_params in + PrintPure.type_def_to_string fmt def + +let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string = + let type_params = sg.type_params in + let type_defs = ctx.type_context.type_defs in + let fun_defs = ctx.fun_context.fun_defs in + let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in + PrintPure.fun_sig_to_string fmt sg + +let fun_def_to_string (ctx : trans_ctx) (def : Pure.fun_def) : string = + let type_params = def.signature.type_params in + let type_defs = ctx.type_context.type_defs in + let fun_defs = ctx.fun_context.fun_defs in + let fmt = PrintPure.mk_ast_formatter type_defs fun_defs type_params in + PrintPure.fun_def_to_string fmt def + type symbolic_fun_translation = V.symbolic_value list * SA.expression (** The result of running the symbolic interpreter on a function: - the list of symbolic values used for the input values |