diff options
| author | Son Ho | 2022-10-28 11:59:49 +0200 |
|---|---|---|
| committer | Son HO | 2022-10-28 17:41:04 +0200 |
| commit | b4e4e6f6776b2af9607438f6e4249b295c784608 (patch) | |
| tree | ecfd9c4464c5a38f74d9f35f24b67eaa3f086957 /compiler | |
| parent | 9c7fe7eb0cd3fdda6b64ff4dc9f6b68f631bdb44 (diff) | |
Make minor modifications
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Driver.ml | 2 | ||||
| -rw-r--r-- | compiler/Print.ml | 10 | ||||
| -rw-r--r-- | compiler/PrintPure.ml | 2 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 4 |
4 files changed, 11 insertions, 7 deletions
diff --git a/compiler/Driver.ml b/compiler/Driver.ml index c8a1fef4..bd9396c0 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -155,7 +155,7 @@ let () = | Ok m -> (* Logging *) main_log#linfo (lazy ("Imported: " ^ filename)); - main_log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n")); + main_log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n")); (* Apply the pre-passes *) let m = PrePasses.apply_passes m in diff --git a/compiler/Print.ml b/compiler/Print.ml index 3f15bd32..c22f9171 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -1,7 +1,11 @@ -include Charon.Print +include Charon.PrintUtils +include Charon.PrintLlbcAst module V = Values module VU = ValuesUtils module C = Contexts +module PrimitiveValues = Charon.PrintPrimitiveValues +module Types = Charon.PrintTypes +module Expressions = Charon.PrintExpressions (** Pretty-printing for values *) module Values = struct @@ -555,11 +559,11 @@ module EvalCtxLlbcAst = struct let place_to_string (ctx : C.eval_ctx) (op : E.place) : string = let fmt = PC.eval_ctx_to_ast_formatter ctx in - PA.place_to_string fmt op + PE.place_to_string fmt op let operand_to_string (ctx : C.eval_ctx) (op : E.operand) : string = let fmt = PC.eval_ctx_to_ast_formatter ctx in - PA.operand_to_string fmt op + PE.operand_to_string fmt op let statement_to_string (ctx : C.eval_ctx) (indent : string) (indent_incr : string) (e : A.statement) : string = diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 0b2e3a62..64b527a2 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -418,7 +418,7 @@ let unop_to_string (unop : unop) : string = "cast<" ^ integer_type_to_string src ^ "," ^ integer_type_to_string tgt ^ ">" -let binop_to_string = Print.LlbcAst.binop_to_string +let binop_to_string = Print.Expressions.binop_to_string let fun_id_to_string (fmt : ast_formatter) (fun_id : fun_id) : string = match fun_id with diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 1341bccc..6e60acc2 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -147,8 +147,8 @@ let type_check_texpression (ctx : bs_ctx) (e : texpression) : unit = PureTypeCheck.check_texpression ctx e (* TODO: move *) -let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.LlbcAst.ast_formatter = - Print.LlbcAst.fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls +let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.Ast.ast_formatter = + Print.Ast.decls_and_fun_decl_to_ast_formatter ctx.type_context.llbc_type_decls ctx.fun_context.llbc_fun_decls ctx.global_context.llbc_global_decls ctx.fun_decl |