Debug prints for the new typer
This commit is contained in:
parent
bd8a57df44
commit
283dcf418a
@ -36,6 +36,9 @@ let propagator : output_break_ctor propagator =
|
|||||||
|
|
||||||
(* a.tv = b.tv *)
|
(* 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 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 *)
|
(* a.c_tag = b.c_tag *)
|
||||||
if (Solver_should_be_generated.compare_simple_c_constant a.c_tag b.c_tag) <> 0 then
|
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)"
|
failwith (Format.asprintf "type error: incompatible types, not same ctor %a vs. %a (compare returns %d)"
|
||||||
|
@ -48,6 +48,7 @@ let propagator : output_specialize1 propagator =
|
|||||||
t = P_apply { tf = { tsrc = "solver: propagator: specialize1 tf" ; t = P_forall a.forall };
|
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
|
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
|
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 eq1 = c_equation { tsrc = "solver: propagator: specialize1 eq1" ; t = P_variable b.tv } reduced "propagator: specialize1" in
|
||||||
let eqs = eq1 :: new_constraints in
|
let eqs = eq1 :: new_constraints in
|
||||||
(eqs, []) (* no new assignments *)
|
(eqs, []) (* no new assignments *)
|
||||||
|
@ -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
|
| 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) …) *)
|
(* break down (TC(args)) into (TC('a, …) and ('a = arg) …) *)
|
||||||
| C_typeclass { tc_args; typeclass } -> split_typeclass tc_args typeclass
|
| 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 =
|
let normalizers : type_constraint -> structured_dbs -> (structured_dbs , 'modified_constraint) state_list_monad =
|
||||||
fun new_constraint dbs ->
|
fun new_constraint dbs ->
|
||||||
|
@ -45,6 +45,15 @@ let select_and_propagate : ('old_input, 'selector_output) selector -> 'selector_
|
|||||||
(* Call the propagation rule *)
|
(* Call the propagation rule *)
|
||||||
let (new_constraints , new_assignments) = List.split @@ List.map (propagator dbs) selected_outputs in
|
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 *)
|
(* 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)
|
(already_selected , List.flatten new_constraints , List.flatten new_assignments)
|
||||||
| WasNotSelected ->
|
| WasNotSelected ->
|
||||||
(already_selected, [] , [])
|
(already_selected, [] , [])
|
||||||
|
@ -455,16 +455,20 @@ let type_and_subst_xyz
|
|||||||
(apply_substs : ('b , Typer_common.Errors.typer_error) Typesystem.Misc.Substitution.Pattern.w)
|
(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)
|
(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 =
|
: ('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%bind (env, state, node) = type_xyz_returns_state env_state_node in
|
||||||
let subst_all =
|
let subst_all =
|
||||||
let aliases = state.structured_dbs.aliases in
|
let aliases = state.structured_dbs.aliases in
|
||||||
let assignments = state.structured_dbs.assignments in
|
let assignments = state.structured_dbs.assignments in
|
||||||
let substs : variable: I.type_variable -> _ = fun ~variable ->
|
let substs : variable: I.type_variable -> _ = fun ~variable ->
|
||||||
to_option @@
|
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 =
|
let%bind root =
|
||||||
trace_option (corner_case (Format.asprintf "can't find alias root of variable %a" Var.pp variable)) @@
|
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. *)
|
(* TODO: after upgrading UnionFind, this will be an option, not an exception. *)
|
||||||
try Some (Solver.UF.repr variable aliases) with Not_found -> None in
|
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 =
|
let%bind assignment =
|
||||||
trace_option (corner_case (Format.asprintf "can't find assignment for root %a" Var.pp root)) @@
|
trace_option (corner_case (Format.asprintf "can't find assignment for root %a" Var.pp root)) @@
|
||||||
(Map.find_opt root assignments) in
|
(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 () = 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") @@
|
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
|
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
|
ok @@ expr
|
||||||
in
|
in
|
||||||
let p = apply_substs ~substs node in
|
let p = apply_substs ~substs node in
|
||||||
p in
|
p in
|
||||||
let%bind node = subst_all 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? *)
|
let () = ignore env in (* TODO: shouldn't we use the `env` somewhere? *)
|
||||||
ok (node, state)
|
ok (node, state)
|
||||||
|
|
||||||
|
@ -71,7 +71,7 @@ let rec expression ppf (e : expression) =
|
|||||||
and expression_content ppf (ec : expression_content) =
|
and expression_content ppf (ec : expression_content) =
|
||||||
match ec with
|
match ec with
|
||||||
| E_literal l ->
|
| E_literal l ->
|
||||||
literal ppf l
|
fprintf ppf "%a" literal l
|
||||||
| E_variable n ->
|
| E_variable n ->
|
||||||
fprintf ppf "%a" expression_variable n
|
fprintf ppf "%a" expression_variable n
|
||||||
| E_application {lamb;args} ->
|
| E_application {lamb;args} ->
|
||||||
|
@ -17,5 +17,6 @@ module Helpers = Helpers
|
|||||||
include Types
|
include Types
|
||||||
include Misc
|
include Misc
|
||||||
include Combinators
|
include Combinators
|
||||||
|
module Debug = Stage_common.Debug
|
||||||
|
|
||||||
let program_environment env program = fst (Compute_environment.program env program)
|
let program_environment env program = fst (Compute_environment.program env program)
|
||||||
|
@ -3,3 +3,4 @@ include Types
|
|||||||
module Types = Types
|
module Types = Types
|
||||||
module PP = PP
|
module PP = PP
|
||||||
module Helpers = Helpers
|
module Helpers = Helpers
|
||||||
|
module Debug = Debug
|
||||||
|
1
src/stages/common/debug.ml
Normal file
1
src/stages/common/debug.ml
Normal file
@ -0,0 +1 @@
|
|||||||
|
let debug_new_typer = false
|
@ -27,8 +27,10 @@ type type_variable = Ast_typed.type_variable
|
|||||||
type type_expression = Ast_typed.type_expression
|
type type_expression = Ast_typed.type_expression
|
||||||
|
|
||||||
(* generate a new type variable and gave it an id *)
|
(* generate a new type variable and gave it an id *)
|
||||||
let fresh_type_variable : ?name:string -> unit -> type_variable =
|
let fresh_type_variable : ?name:string -> unit -> type_variable = fun ?name () ->
|
||||||
Var.fresh
|
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) ->
|
let type_expression'_of_simple_c_constant : constant_tag * type_expression list -> Ast_typed.type_content option = fun (c, l) ->
|
||||||
match c, l with
|
match c, l with
|
||||||
|
@ -98,7 +98,9 @@ let typed_program_with_imperative_input_to_michelson
|
|||||||
let env = Ast_typed.program_environment Environment.default program in
|
let env = Ast_typed.program_environment Environment.default program in
|
||||||
let%bind sugar = Compile.Of_imperative.compile_expression input in
|
let%bind sugar = Compile.Of_imperative.compile_expression input in
|
||||||
let%bind core = Compile.Of_sugar.compile_expression sugar 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%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%bind (typed_app,new_state) = Compile.Of_core.compile_expression ~env ~state app in
|
||||||
let () = Typer.Solver.discard_state new_state in
|
let () = Typer.Solver.discard_state new_state in
|
||||||
let%bind compiled_applied = Compile.Of_typed.compile_expression typed_app in
|
let%bind compiled_applied = Compile.Of_typed.compile_expression typed_app in
|
||||||
|
2
vendors/ligo-utils/simple-utils/var.ml
vendored
2
vendors/ligo-utils/simple-utils/var.ml
vendored
@ -47,3 +47,5 @@ let fresh ?name () =
|
|||||||
|
|
||||||
let fresh_like v =
|
let fresh_like v =
|
||||||
fresh ~name:v.name ()
|
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
|
||||||
|
2
vendors/ligo-utils/simple-utils/var.mli
vendored
2
vendors/ligo-utils/simple-utils/var.mli
vendored
@ -43,3 +43,5 @@ val fresh_like : 'a t -> 'b t
|
|||||||
(* Reset the global counter. Danger, do not use... Provided for tests
|
(* Reset the global counter. Danger, do not use... Provided for tests
|
||||||
only. *)
|
only. *)
|
||||||
val reset_counter : unit -> unit
|
val reset_counter : unit -> unit
|
||||||
|
|
||||||
|
val debug : 'a t -> string
|
||||||
|
Loading…
Reference in New Issue
Block a user