From 018e269b2ebcdd05f8e9b3a685cd8aae561a8cad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Wed, 24 Jun 2020 02:04:59 +0100 Subject: [PATCH 1/5] Have separate ppf and Yojson modules for PP_json --- src/stages/5-ast_typed/PP_json.ml | 14 ++++++++++++-- src/stages/5-ast_typed/formatter.ml | 2 +- 2 files changed, 13 insertions(+), 3 deletions(-) diff --git a/src/stages/5-ast_typed/PP_json.ml b/src/stages/5-ast_typed/PP_json.ml index 745483ebc..d700c65b3 100644 --- a/src/stages/5-ast_typed/PP_json.ml +++ b/src/stages/5-ast_typed/PP_json.ml @@ -76,13 +76,23 @@ module M = struct `Assoc ["typeVariableMap", `List lst'] ); } - let print : ((no_state, json) fold_config -> no_state -> 'a -> json) -> 'a -> json = fun fold v -> + let to_json : ((no_state, json) fold_config -> no_state -> 'a -> json) -> 'a -> json = fun fold v -> fold to_json NoState v + + let print : ((no_state, json) fold_config -> no_state -> 'a -> json) -> formatter -> 'a -> unit = fun fold ppf v -> + fprintf ppf "%a" Yojson.Basic.pp (to_json fold v) end +module Yojson = Fold.Folds(struct + type in_state = M.no_state ;; + type out_state = json ;; + type 'a t = 'a -> json ;; + let f = M.to_json ;; +end) + include Fold.Folds(struct type in_state = M.no_state ;; type out_state = json ;; - type 'a t = 'a -> json ;; + type 'a t = formatter -> 'a -> unit ;; let f = M.print ;; end) diff --git a/src/stages/5-ast_typed/formatter.ml b/src/stages/5-ast_typed/formatter.ml index f6c331722..e42269786 100644 --- a/src/stages/5-ast_typed/formatter.ml +++ b/src/stages/5-ast_typed/formatter.ml @@ -4,7 +4,7 @@ let program_ppformat ~display_format f (typed,_) = match display_format with | Human_readable | Dev -> PP.program f typed -let program_jsonformat (typed,_) : json = PP_json.program typed +let program_jsonformat (typed,_) : json = PP_json.Yojson.program typed let program_format : 'a format = { pp = program_ppformat; From bd8a57df44a76bb7ed9ee3f6e2ab43ace3dbffda Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Wed, 17 Jun 2020 22:59:35 +0100 Subject: [PATCH 2/5] Add a pretty-printer to the heuristics --- .../08-typer-new/heuristic_break_ctor.ml | 9 ++++- .../08-typer-new/heuristic_specialize1.ml | 9 ++++- src/passes/09-typing/08-typer-new/solver.ml | 8 ++--- src/passes/09-typing/08-typer-new/typer.ml | 22 +++++++++--- src/stages/typesystem/solver_types.ml | 34 +++++++++++++++++++ 5 files changed, 71 insertions(+), 11 deletions(-) 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 ab8842443..df54b41c8 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 @@ -51,4 +51,11 @@ let propagator : output_break_ctor propagator = let eqs = eq1 :: eqs3 in (eqs , []) (* no new assignments *) -let heuristic = Propagator_heuristic { selector ; propagator ; comparator = Solver_should_be_generated.compare_output_break_ctor } +let heuristic = + Propagator_heuristic + { + selector ; + propagator ; + printer = Ast_typed.PP_generic.output_break_ctor ; (* TODO: use an accessor that can get the printer for PP_generic or PP_json alike *) + comparator = Solver_should_be_generated.compare_output_break_ctor + } 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 5d7bc863f..8d82cfd3f 100644 --- a/src/passes/09-typing/08-typer-new/heuristic_specialize1.ml +++ b/src/passes/09-typing/08-typer-new/heuristic_specialize1.ml @@ -52,4 +52,11 @@ let propagator : output_specialize1 propagator = let eqs = eq1 :: new_constraints in (eqs, []) (* no new assignments *) -let heuristic = Propagator_heuristic { selector ; propagator ; comparator = Solver_should_be_generated.compare_output_specialize1 } +let heuristic = + Propagator_heuristic + { + selector ; + propagator ; + printer = Ast_typed.PP_generic.output_specialize1 ; + comparator = Solver_should_be_generated.compare_output_specialize1 + } diff --git a/src/passes/09-typing/08-typer-new/solver.ml b/src/passes/09-typing/08-typer-new/solver.ml index aa2df6f24..747e56e4d 100644 --- a/src/passes/09-typing/08-typer-new/solver.ml +++ b/src/passes/09-typing/08-typer-new/solver.ml @@ -13,8 +13,8 @@ let propagator_heuristics = Heuristic_specialize1.heuristic ; ] -let init_propagator_heuristic (Propagator_heuristic { selector ; propagator ; comparator }) = - Propagator_state { selector ; propagator ; already_selected = Set.create ~cmp:comparator } +let init_propagator_heuristic (Propagator_heuristic { selector ; propagator ; printer ; comparator }) = + Propagator_state { selector ; propagator ; printer ; already_selected = Set.create ~cmp:comparator } let initial_state : typer_state = { structured_dbs = @@ -49,12 +49,12 @@ let select_and_propagate : ('old_input, 'selector_output) selector -> 'selector_ | WasNotSelected -> (already_selected, [] , []) -let select_and_propagate_one new_constraint (new_states , new_constraints , dbs) (Propagator_state { selector; propagator; already_selected }) = +let select_and_propagate_one new_constraint (new_states , new_constraints , dbs) (Propagator_state { selector; propagator; printer ; already_selected }) = let sel_propag = (select_and_propagate selector propagator) in let (already_selected , new_constraints', new_assignments) = sel_propag already_selected new_constraint dbs in let assignments = List.fold_left (fun acc ({tv;c_tag=_;tv_list=_} as ele) -> Map.update tv (function None -> Some ele | x -> x) acc) dbs.assignments new_assignments in let dbs = { dbs with assignments } in - Propagator_state { selector; propagator; already_selected } :: new_states, new_constraints' @ new_constraints, dbs + Propagator_state { selector; propagator; printer ; already_selected } :: new_states, new_constraints' @ new_constraints, dbs (* Takes a constraint, applies all selector+propagator pairs to it. Keeps track of which constraints have already been selected. *) diff --git a/src/passes/09-typing/08-typer-new/typer.ml b/src/passes/09-typing/08-typer-new/typer.ml index 8359a281f..3b92319f2 100644 --- a/src/passes/09-typing/08-typer-new/typer.ml +++ b/src/passes/09-typing/08-typer-new/typer.ml @@ -440,9 +440,21 @@ let type_program_returns_state ((env, state, p) : environment * O'.typer_state * let declarations = List.rev declarations in (* Common hack to have O(1) append: prepend and then reverse *) ok (env', state', declarations) +let print_env_state_node (node_printer : Format.formatter -> 'a -> unit) ((env,state,node) : environment * O'.typer_state * 'a) = + ignore node; (* TODO *) + Printf.printf "%s" @@ + Format.asprintf "ENV = %a\nSTATE = %a\nNODE = %a\n\n" + Ast_typed.PP_generic.environment env + Typesystem.Solver_types.pp_typer_state state + node_printer node + let type_and_subst_xyz - (env_state_node : environment * O'.typer_state * 'a) (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 = + (in_printer : Format.formatter -> 'a -> unit) + (out_printer : Format.formatter -> 'b -> unit) + (env_state_node : environment * O'.typer_state * 'a) + (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%bind (env, state, node) = type_xyz_returns_state env_state_node in let subst_all = let aliases = state.structured_dbs.aliases in @@ -471,7 +483,7 @@ let type_and_subst_xyz let type_program (p : I.program) : (O.program * O'.typer_state, typer_error) result = let empty_env = DEnv.default in let empty_state = Solver.initial_state in - type_and_subst_xyz (empty_env , empty_state , p) Typesystem.Misc.Substitution.Pattern.s_program type_program_returns_state + type_and_subst_xyz I.PP.program Ast_typed.PP_generic.program (empty_env , empty_state , p) Typesystem.Misc.Substitution.Pattern.s_program type_program_returns_state let type_expression_returns_state : (environment * O'.typer_state * I.expression) -> (environment * O'.typer_state * O.expression, typer_error) result = fun (env, state, e) -> @@ -480,7 +492,7 @@ let type_expression_returns_state : (environment * O'.typer_state * I.expression let type_expression_subst (env : environment) (state : O'.typer_state) ?(tv_opt : O.type_expression option) (e : I.expression) : (O.expression * O'.typer_state , typer_error) result = let () = ignore tv_opt in (* For compatibility with the old typer's API, this argument can be removed once the new typer is used. *) - type_and_subst_xyz (env , state , e) Typesystem.Misc.Substitution.Pattern.s_expression type_expression_returns_state + type_and_subst_xyz I.PP.expression Ast_typed.PP_generic.expression (env , state , e) Typesystem.Misc.Substitution.Pattern.s_expression type_expression_returns_state let untype_type_expression = Untyper.untype_type_expression let untype_expression = Untyper.untype_expression @@ -493,7 +505,7 @@ and [@warning "-32"] type_expression : environment -> O'.typer_state -> ?tv_opt: and [@warning "-32"] type_lambda e state lam = type_lambda e state lam and [@warning "-32"] type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression, typer_error) result = type_constant name lst tv_opt let [@warning "-32"] type_program_returns_state ((env, state, p) : environment * O'.typer_state * I.program) : (environment * O'.typer_state * O.program, typer_error) result = type_program_returns_state (env, state, p) -let [@warning "-32"] type_and_subst_xyz (env_state_node : environment * O'.typer_state * 'a) (apply_substs : ('b,typer_error) Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * O'.typer_state * 'a) -> (environment * O'.typer_state * 'b, typer_error) result) : ('b * O'.typer_state, typer_error) result = type_and_subst_xyz env_state_node apply_substs type_xyz_returns_state +let [@warning "-32"] type_and_subst_xyz (in_printer : (Format.formatter -> 'a -> unit)) (out_printer : (Format.formatter -> 'b -> unit)) (env_state_node : environment * O'.typer_state * 'a) (apply_substs : ('b,typer_error) Typesystem.Misc.Substitution.Pattern.w) (type_xyz_returns_state : (environment * O'.typer_state * 'a) -> (environment * O'.typer_state * 'b, typer_error) result) : ('b * O'.typer_state, typer_error) result = type_and_subst_xyz in_printer out_printer env_state_node apply_substs type_xyz_returns_state let [@warning "-32"] type_program (p : I.program) : (O.program * O'.typer_state, typer_error) result = type_program p let [@warning "-32"] type_expression_returns_state : (environment * O'.typer_state * I.expression) -> (environment * O'.typer_state * O.expression, typer_error) Trace.result = type_expression_returns_state let [@warning "-32"] type_expression_subst (env : environment) (state : O'.typer_state) ?(tv_opt : O.type_expression option) (e : I.expression) : (O.expression * O'.typer_state, typer_error) result = type_expression_subst env state ?tv_opt e diff --git a/src/stages/typesystem/solver_types.ml b/src/stages/typesystem/solver_types.ml index 8c9b547c3..a1c36b56a 100644 --- a/src/stages/typesystem/solver_types.ml +++ b/src/stages/typesystem/solver_types.ml @@ -15,12 +15,14 @@ type ('old_constraint_type , 'selector_output ) propagator_heuristic = { selector : ('old_constraint_type, 'selector_output) selector ; (* constraint propagation: (buch of constraints) → (new constraints * assignments) *) propagator : 'selector_output propagator ; + printer : Format.formatter -> 'selector_output -> unit ; comparator : 'selector_output -> 'selector_output -> int ; } type ('old_constraint_type , 'selector_output ) propagator_state = { selector : ('old_constraint_type, 'selector_output) selector ; propagator : 'selector_output propagator ; + printer : Format.formatter -> 'selector_output -> unit ; already_selected : 'selector_output Set.t; } @@ -37,6 +39,38 @@ type typer_state = { already_selected_and_propagators : ex_propagator_state list ; } +open Format +open PP_helpers + +let pp_already_selected = fun printer ppf set -> + let lst = (RedBlackTrees.PolySet.elements set) in + Format.fprintf ppf "Set [@,@[ %a @]@,]" (list_sep printer (fun ppf () -> fprintf ppf " ;@ ")) lst + +let pp_ex_propagator_state = fun ppf (Propagator_state { selector ; propagator ; printer ; already_selected }) -> + ignore ( selector, propagator ); + Format.fprintf ppf "{ selector = (* OCaml function *); propagator = (* OCaml function *); already_selected = %a }" + (pp_already_selected printer) already_selected + +let pp_typer_state = fun ppf ({ structured_dbs; already_selected_and_propagators } : typer_state) -> + Format.fprintf ppf "{ structured_dbs = %a ; already_selected_and_propagators = [ %a ] }" + Ast_typed.PP_generic.structured_dbs structured_dbs + (list_sep pp_ex_propagator_state (fun ppf () -> fprintf ppf " ;@ ")) already_selected_and_propagators + + +let json_already_selected = fun printer ppf set -> + let lst = (RedBlackTrees.PolySet.elements set) in + Format.fprintf ppf "[ \"Set\" %a ]" (list_sep printer (fun ppf () -> fprintf ppf " , ")) lst + +let json_ex_propagator_state = fun ppf (Propagator_state { selector; propagator; printer ; already_selected }) -> + ignore (selector,propagator); + Format.fprintf ppf "{ \"selector\": \"OCaml function\"; \"propagator\": \"OCaml function\"; \"already_selected\": %a }" + (json_already_selected printer) already_selected + +let json_typer_state = fun ppf ({ structured_dbs; already_selected_and_propagators } : typer_state) -> + Format.fprintf ppf "{ \"structured_dbs\": %a ; \"already_selected_and_propagators\": [ %a ] }" + Ast_typed.PP_json.structured_dbs structured_dbs + (list_sep json_ex_propagator_state (fun ppf () -> fprintf ppf " , ")) already_selected_and_propagators + (* state+list monad *) type ('state, 'elt) state_list_monad = { state: 'state ; list : 'elt list } let lift_state_list_monad ~state ~list = { state ; list } 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 3/5] 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 From 1cc64d6812aa1dd30cce1b372f710e65756893e0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Wed, 17 Jun 2020 23:18:58 +0100 Subject: [PATCH 4/5] reasons for failing tests --- src/test/integration_tests.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 022942e31..26bc9c6fc 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -2403,16 +2403,16 @@ let loop_bugs_ligo () : (unit, _) result = ok () let main = test_suite "Integration (End to End)" [ - test "bytes unpack" bytes_unpack ; - test "bytes unpack (mligo)" bytes_unpack_mligo ; - test "bytes unpack (religo)" bytes_unpack_religo ; - test "key hash" key_hash ; - test "key hash (mligo)" key_hash_mligo ; - test "key hash (religo)" key_hash_religo ; - test "check signature" check_signature ; - test "check signature (mligo)" check_signature_mligo ; - test "check signature (religo)" check_signature_religo ; - test "chain id" chain_id ; + test "chain id" chain_id ; (* record *) + test "bytes unpack" bytes_unpack ; (* record *) + test "bytes unpack (mligo)" bytes_unpack_mligo ; (* record *) + test "bytes unpack (religo)" bytes_unpack_religo ; (* record *) + test "key hash" key_hash ; (* C_access_label *) + test "key hash (mligo)" key_hash_mligo ; (* C_access_label *) + test "key hash (religo)" key_hash_religo ; (* C_access_label *) + test "check signature" check_signature ; (* C_access_label *) + test "check signature (mligo)" check_signature_mligo ; (* C_access_label *) + test "check signature (religo)" check_signature_religo ; (* C_access_label *) test "type alias" type_alias ; test "function" function_ ; test "blockless function" blockless; From c1d211d98c71ff06b47cae0eed3eadae8b71e3cc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Wed, 17 Jun 2020 22:39:14 +0100 Subject: [PATCH 5/5] Debug prints for the new typer: output JSON --- debug.cmd | 1 + src/main/compile/of_core.ml | 1 - src/passes/09-typing/08-typer-new/typer.ml | 22 ++++++++++++---------- src/stages/common/debug.ml | 1 + 4 files changed, 14 insertions(+), 11 deletions(-) create mode 100644 debug.cmd diff --git a/debug.cmd b/debug.cmd new file mode 100644 index 000000000..b22905ed0 --- /dev/null +++ b/debug.cmd @@ -0,0 +1 @@ +(echo '['; sed -ne '/###############################START_OF_JSON/,/###############################END_OF_JSON/{/^###############################.*_OF_JSON/d;p}' < '/home/suzanne/00ligopam/ligo/_build/default/src/test/_build/_tests/'*'/Integration (End to End).001.output'; echo '"end of json"]') > /tmp/js.json diff --git a/src/main/compile/of_core.ml b/src/main/compile/of_core.ml index 931aee07d..8f580f153 100644 --- a/src/main/compile/of_core.ml +++ b/src/main/compile/of_core.ml @@ -18,7 +18,6 @@ let compile (cform: form) (program : Ast_core.program) : (Ast_typed.program * Ty let compile_expression ?(env = Ast_typed.Environment.empty) ~(state : Typesystem.Solver_types.typer_state) (e : Ast_core.expression) : (Ast_typed.expression * Typesystem.Solver_types.typer_state , _) result = let%bind (ae_typed,state) = trace typer_tracer @@ Typer.type_expression_subst env state e in - let () = Typer.Solver.discard_state state in let%bind ae_typed' = trace self_ast_typed_tracer @@ Self_ast_typed.all_expression ae_typed in ok @@ (ae_typed',state) diff --git a/src/passes/09-typing/08-typer-new/typer.ml b/src/passes/09-typing/08-typer-new/typer.ml index 33462feae..6b690ceb5 100644 --- a/src/passes/09-typing/08-typer-new/typer.ml +++ b/src/passes/09-typing/08-typer-new/typer.ml @@ -443,9 +443,9 @@ let type_program_returns_state ((env, state, p) : environment * O'.typer_state * let print_env_state_node (node_printer : Format.formatter -> 'a -> unit) ((env,state,node) : environment * O'.typer_state * 'a) = ignore node; (* TODO *) Printf.printf "%s" @@ - Format.asprintf "ENV = %a\nSTATE = %a\nNODE = %a\n\n" - Ast_typed.PP_generic.environment env - Typesystem.Solver_types.pp_typer_state state + Format.asprintf "{ \"ENV\": %a,\n\"STATE\": %a,\n\"NODE\": %a\n},\n" + Ast_typed.PP_json.environment env + Typesystem.Solver_types.json_typer_state state node_printer node let type_and_subst_xyz @@ -455,20 +455,21 @@ 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.json_new_typer then Printf.printf "%!\n###############################START_OF_JSON\n[%!") in 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 () = (if Ast_typed.Debug.debug_new_typer || Ast_typed.Debug.json_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 () = (if Ast_typed.Debug.debug_new_typer then Printf.fprintf stderr "%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 () = (if Ast_typed.Debug.debug_new_typer then Printf.fprintf stderr "%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 @@ -476,21 +477,22 @@ 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 + let () = (if Ast_typed.Debug.debug_new_typer then Printf.fprintf stderr "%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 () = (if Ast_typed.Debug.debug_new_typer || Ast_typed.Debug.json_new_typer then print_env_state_node out_printer (env, state, node)) in + let () = (if Ast_typed.Debug.json_new_typer then Printf.printf "%!\"end of JSON\"],\n###############################END_OF_JSON\n%!") in let () = ignore env in (* TODO: shouldn't we use the `env` somewhere? *) ok (node, state) let type_program (p : I.program) : (O.program * O'.typer_state, typer_error) result = let empty_env = DEnv.default in let empty_state = Solver.initial_state in - type_and_subst_xyz I.PP.program Ast_typed.PP_generic.program (empty_env , empty_state , p) Typesystem.Misc.Substitution.Pattern.s_program type_program_returns_state + type_and_subst_xyz (fun ppf _v -> Format.fprintf ppf "\"no JSON yet for I.PP.program\"") Ast_typed.PP_json.program (empty_env , empty_state , p) Typesystem.Misc.Substitution.Pattern.s_program type_program_returns_state let type_expression_returns_state : (environment * O'.typer_state * I.expression) -> (environment * O'.typer_state * O.expression, typer_error) result = fun (env, state, e) -> @@ -499,7 +501,7 @@ let type_expression_returns_state : (environment * O'.typer_state * I.expression let type_expression_subst (env : environment) (state : O'.typer_state) ?(tv_opt : O.type_expression option) (e : I.expression) : (O.expression * O'.typer_state , typer_error) result = let () = ignore tv_opt in (* For compatibility with the old typer's API, this argument can be removed once the new typer is used. *) - type_and_subst_xyz I.PP.expression Ast_typed.PP_generic.expression (env , state , e) Typesystem.Misc.Substitution.Pattern.s_expression type_expression_returns_state + type_and_subst_xyz (fun ppf _v -> Format.fprintf ppf "\"no JSON yet for I.PP.expression\"") Ast_typed.PP_json.expression (env , state , e) Typesystem.Misc.Substitution.Pattern.s_expression type_expression_returns_state let untype_type_expression = Untyper.untype_type_expression let untype_expression = Untyper.untype_expression diff --git a/src/stages/common/debug.ml b/src/stages/common/debug.ml index 6e435e395..a87e6cb46 100644 --- a/src/stages/common/debug.ml +++ b/src/stages/common/debug.ml @@ -1 +1,2 @@ let debug_new_typer = false +let json_new_typer = false