From 283dcf418a1f212f777542b089ffebae202a3bbd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Wed, 17 Jun 2020 23:15:17 +0100 Subject: [PATCH] Debug prints for the new typer --- .../09-typing/08-typer-new/heuristic_break_ctor.ml | 3 +++ .../09-typing/08-typer-new/heuristic_specialize1.ml | 1 + src/passes/09-typing/08-typer-new/normalizer.ml | 2 +- src/passes/09-typing/08-typer-new/solver.ml | 9 +++++++++ src/passes/09-typing/08-typer-new/typer.ml | 7 +++++++ src/stages/2-ast_imperative/PP.ml | 2 +- src/stages/5-ast_typed/ast_typed.ml | 1 + src/stages/common/ast_common.ml | 1 + src/stages/common/debug.ml | 1 + src/stages/typesystem/core.ml | 6 ++++-- src/test/test_helpers.ml | 2 ++ vendors/ligo-utils/simple-utils/var.ml | 2 ++ vendors/ligo-utils/simple-utils/var.mli | 2 ++ 13 files changed, 35 insertions(+), 4 deletions(-) create mode 100644 src/stages/common/debug.ml diff --git a/src/passes/09-typing/08-typer-new/heuristic_break_ctor.ml b/src/passes/09-typing/08-typer-new/heuristic_break_ctor.ml index df54b41c8..d140ecdc3 100644 --- a/src/passes/09-typing/08-typer-new/heuristic_break_ctor.ml +++ b/src/passes/09-typing/08-typer-new/heuristic_break_ctor.ml @@ -36,6 +36,9 @@ let propagator : output_break_ctor propagator = (* a.tv = b.tv *) let eq1 = c_equation { tsrc = "solver: propagator: break_ctor a" ; t = P_variable a.tv} { tsrc = "solver: propagator: break_ctor b" ; t = P_variable b.tv} "propagator: break_ctor" in + let () = if Ast_typed.Debug.debug_new_typer then + let p = Ast_typed.PP_generic.c_constructor_simpl in + Format.printf "\npropagator_break_ctor\na = %a\nb = %a\n%!" p a p b in (* a.c_tag = b.c_tag *) if (Solver_should_be_generated.compare_simple_c_constant a.c_tag b.c_tag) <> 0 then failwith (Format.asprintf "type error: incompatible types, not same ctor %a vs. %a (compare returns %d)" diff --git a/src/passes/09-typing/08-typer-new/heuristic_specialize1.ml b/src/passes/09-typing/08-typer-new/heuristic_specialize1.ml index 8d82cfd3f..d9c3563c1 100644 --- a/src/passes/09-typing/08-typer-new/heuristic_specialize1.ml +++ b/src/passes/09-typing/08-typer-new/heuristic_specialize1.ml @@ -48,6 +48,7 @@ let propagator : output_specialize1 propagator = t = P_apply { tf = { tsrc = "solver: propagator: specialize1 tf" ; t = P_forall a.forall }; targ = { tsrc = "solver: propagator: specialize1 targ" ; t = P_variable fresh_existential }} } in let (reduced, new_constraints) = Typelang.check_applied @@ Typelang.type_level_eval apply in + (if Ast_typed.Debug.debug_new_typer then Format.printf "apply = %a\nb = %a\nreduced = %a\nnew_constraints = [\n%a\n]\n" Ast_typed.PP_generic.type_value apply Ast_typed.PP_generic.c_constructor_simpl b Ast_typed.PP_generic.type_value reduced (PP_helpers.list_sep Ast_typed.PP_generic.type_constraint (fun ppf () -> Format.fprintf ppf " ;\n")) new_constraints); let eq1 = c_equation { tsrc = "solver: propagator: specialize1 eq1" ; t = P_variable b.tv } reduced "propagator: specialize1" in let eqs = eq1 :: new_constraints in (eqs, []) (* no new assignments *) diff --git a/src/passes/09-typing/08-typer-new/normalizer.ml b/src/passes/09-typing/08-typer-new/normalizer.ml index 5c6549c03..ecd0c8a5a 100644 --- a/src/passes/09-typing/08-typer-new/normalizer.ml +++ b/src/passes/09-typing/08-typer-new/normalizer.ml @@ -114,7 +114,7 @@ let rec normalizer_simpl : (type_constraint , type_constraint_simpl) normalizer | C_equation {aval=({ tsrc = _ ; t = P_apply _ } as a); bval=(_ as b)} -> reduce_type_app b a (* break down (TC(args)) into (TC('a, …) and ('a = arg) …) *) | C_typeclass { tc_args; typeclass } -> split_typeclass tc_args typeclass - | C_access_label { c_access_label_tval; accessor; c_access_label_tvar } -> let _todo = ignore (c_access_label_tval, accessor, c_access_label_tvar) in failwith "TODO" (* tv, label, result *) + | C_access_label { c_access_label_tval; accessor; c_access_label_tvar } -> let _todo = ignore (c_access_label_tval, accessor, c_access_label_tvar) in failwith "TODO C_access_label" (* tv, label, result *) let normalizers : type_constraint -> structured_dbs -> (structured_dbs , 'modified_constraint) state_list_monad = fun new_constraint dbs -> diff --git a/src/passes/09-typing/08-typer-new/solver.ml b/src/passes/09-typing/08-typer-new/solver.ml index 747e56e4d..06ada30f0 100644 --- a/src/passes/09-typing/08-typer-new/solver.ml +++ b/src/passes/09-typing/08-typer-new/solver.ml @@ -45,6 +45,15 @@ let select_and_propagate : ('old_input, 'selector_output) selector -> 'selector_ (* Call the propagation rule *) let (new_constraints , new_assignments) = List.split @@ List.map (propagator dbs) selected_outputs in (* return so that the new constraints are pushed to some kind of work queue and the new assignments stored *) +let () = + (if Ast_typed.Debug.debug_new_typer && false then + let s str = (fun ppf () -> Format.fprintf ppf str) in + Format.printf "propagator produced\nnew_constraints = %a\nnew_assignments = %a\n" + (PP_helpers.list_sep (PP_helpers.list_sep Ast_typed.PP_generic.type_constraint (s "\n")) (s "\n")) + new_constraints + (PP_helpers.list_sep (PP_helpers.list_sep Ast_typed.PP_generic.c_constructor_simpl (s "\n")) (s "\n")) + new_assignments) +in (already_selected , List.flatten new_constraints , List.flatten new_assignments) | WasNotSelected -> (already_selected, [] , []) diff --git a/src/passes/09-typing/08-typer-new/typer.ml b/src/passes/09-typing/08-typer-new/typer.ml index 3b92319f2..33462feae 100644 --- a/src/passes/09-typing/08-typer-new/typer.ml +++ b/src/passes/09-typing/08-typer-new/typer.ml @@ -455,16 +455,20 @@ let type_and_subst_xyz (apply_substs : ('b , Typer_common.Errors.typer_error) Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * O'.typer_state * 'a) -> (environment * O'.typer_state * 'b , typer_error) Trace.result) : ('b * O'.typer_state , typer_error) result = + let () = (if Ast_typed.Debug.debug_new_typer then Printf.printf "\nTODO AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA Print env_state_node here.\n\n") in + let () = (if Ast_typed.Debug.debug_new_typer then print_env_state_node in_printer env_state_node) in let%bind (env, state, node) = type_xyz_returns_state env_state_node in let subst_all = let aliases = state.structured_dbs.aliases in let assignments = state.structured_dbs.assignments in let substs : variable: I.type_variable -> _ = fun ~variable -> to_option @@ + let () = (if Ast_typed.Debug.debug_new_typer then Printf.printf "%s" @@ Format.asprintf "TRY %a\n" Var.pp variable) in let%bind root = trace_option (corner_case (Format.asprintf "can't find alias root of variable %a" Var.pp variable)) @@ (* TODO: after upgrading UnionFind, this will be an option, not an exception. *) try Some (Solver.UF.repr variable aliases) with Not_found -> None in + let () = (if Ast_typed.Debug.debug_new_typer then Printf.printf "%s" @@ Format.asprintf "TRYR %a (%a)\n" Var.pp variable Var.pp root) in let%bind assignment = trace_option (corner_case (Format.asprintf "can't find assignment for root %a" Var.pp root)) @@ (Map.find_opt root assignments) in @@ -472,11 +476,14 @@ let type_and_subst_xyz let () = ignore tv (* I think there is an issue where the tv is stored twice (as a key and in the element itself) *) in let%bind (expr : O.type_content) = trace_option (corner_case "wrong constant tag") @@ Typesystem.Core.type_expression'_of_simple_c_constant (c_tag , (List.map (fun s -> O.t_variable s ()) tv_list)) in + let () = (if Ast_typed.Debug.debug_new_typer then Printf.printf "%s" @@ Format.asprintf "SUBST %a (%a is %a)\n" Var.pp variable Var.pp root Ast_typed.PP_generic.type_content expr) in ok @@ expr in let p = apply_substs ~substs node in p in let%bind node = subst_all in + let () = (if Ast_typed.Debug.debug_new_typer then Printf.printf "\nTODO AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA Print env,state,node here again.\n\n") in + let () = (if Ast_typed.Debug.debug_new_typer then print_env_state_node out_printer (env, state, node)) in let () = ignore env in (* TODO: shouldn't we use the `env` somewhere? *) ok (node, state) diff --git a/src/stages/2-ast_imperative/PP.ml b/src/stages/2-ast_imperative/PP.ml index 2853dd37e..0bb99ad44 100644 --- a/src/stages/2-ast_imperative/PP.ml +++ b/src/stages/2-ast_imperative/PP.ml @@ -71,7 +71,7 @@ let rec expression ppf (e : expression) = and expression_content ppf (ec : expression_content) = match ec with | E_literal l -> - literal ppf l + fprintf ppf "%a" literal l | E_variable n -> fprintf ppf "%a" expression_variable n | E_application {lamb;args} -> diff --git a/src/stages/5-ast_typed/ast_typed.ml b/src/stages/5-ast_typed/ast_typed.ml index 99f048844..561e3f694 100644 --- a/src/stages/5-ast_typed/ast_typed.ml +++ b/src/stages/5-ast_typed/ast_typed.ml @@ -17,5 +17,6 @@ module Helpers = Helpers include Types include Misc include Combinators +module Debug = Stage_common.Debug let program_environment env program = fst (Compute_environment.program env program) diff --git a/src/stages/common/ast_common.ml b/src/stages/common/ast_common.ml index 605fd90c8..43676422b 100644 --- a/src/stages/common/ast_common.ml +++ b/src/stages/common/ast_common.ml @@ -3,3 +3,4 @@ include Types module Types = Types module PP = PP module Helpers = Helpers +module Debug = Debug diff --git a/src/stages/common/debug.ml b/src/stages/common/debug.ml new file mode 100644 index 000000000..6e435e395 --- /dev/null +++ b/src/stages/common/debug.ml @@ -0,0 +1 @@ +let debug_new_typer = false diff --git a/src/stages/typesystem/core.ml b/src/stages/typesystem/core.ml index eb707b5f5..413613104 100644 --- a/src/stages/typesystem/core.ml +++ b/src/stages/typesystem/core.ml @@ -27,8 +27,10 @@ type type_variable = Ast_typed.type_variable type type_expression = Ast_typed.type_expression (* generate a new type variable and gave it an id *) -let fresh_type_variable : ?name:string -> unit -> type_variable = - Var.fresh +let fresh_type_variable : ?name:string -> unit -> type_variable = fun ?name () -> + let fresh_name = Var.fresh ?name () in + let () = (if Ast_typed.Debug.debug_new_typer && false then Printf.printf "Generated variable %s\n%!%s\n%!" (Var.debug fresh_name) (Printexc.get_backtrace ())) in + fresh_name let type_expression'_of_simple_c_constant : constant_tag * type_expression list -> Ast_typed.type_content option = fun (c, l) -> match c, l with diff --git a/src/test/test_helpers.ml b/src/test/test_helpers.ml index 9ed64a53c..ca68a94b9 100644 --- a/src/test/test_helpers.ml +++ b/src/test/test_helpers.ml @@ -98,7 +98,9 @@ let typed_program_with_imperative_input_to_michelson let env = Ast_typed.program_environment Environment.default program in let%bind sugar = Compile.Of_imperative.compile_expression input in let%bind core = Compile.Of_sugar.compile_expression sugar in +let () = (if Ast_typed.Debug.debug_new_typer then Printf.printf "\nINPUT = %s\n\n%!" (Format.asprintf "%a" Ast_core.PP.expression core)) in let%bind app = Compile.Of_core.apply entry_point core in +let () = (if Ast_typed.Debug.debug_new_typer then Format.printf "\n\nSTATE IZ=%a\n\n" Typesystem.Solver_types.pp_typer_state state) in let%bind (typed_app,new_state) = Compile.Of_core.compile_expression ~env ~state app in let () = Typer.Solver.discard_state new_state in let%bind compiled_applied = Compile.Of_typed.compile_expression typed_app in diff --git a/vendors/ligo-utils/simple-utils/var.ml b/vendors/ligo-utils/simple-utils/var.ml index 490d3430f..8aa5b3b92 100644 --- a/vendors/ligo-utils/simple-utils/var.ml +++ b/vendors/ligo-utils/simple-utils/var.ml @@ -47,3 +47,5 @@ let fresh ?name () = let fresh_like v = fresh ~name:v.name () + +let debug v = match v.counter with Some c -> Printf.sprintf "%s(%d)" v.name c | None -> Printf.sprintf "%s(None)" v.name diff --git a/vendors/ligo-utils/simple-utils/var.mli b/vendors/ligo-utils/simple-utils/var.mli index 6d4936761..d81d69548 100644 --- a/vendors/ligo-utils/simple-utils/var.mli +++ b/vendors/ligo-utils/simple-utils/var.mli @@ -43,3 +43,5 @@ val fresh_like : 'a t -> 'b t (* Reset the global counter. Danger, do not use... Provided for tests only. *) val reset_counter : unit -> unit + +val debug : 'a t -> string