Debug printing facilities.

This commit is contained in:
Olivier 2023-03-14 13:09:12 +01:00
parent cb4c80d84e
commit 866e0f3b17
3 changed files with 46 additions and 6 deletions

View File

@ -768,9 +768,10 @@ let emit_error loc (error : error) =
emit_type ty1;
Printf.printf "and the type:\n";
emit_type ty2;
| VariableScopeEscape (_, _) ->
| VariableScopeEscape (rank, scope) ->
Printf.printf
"A rigid variable escapes its scope.\n"
"A rigid variable of rank %d escapes its scope %d.\n"
rank scope
| ContextNotAbsurd ->
Printf.printf
"Unexpected typing context.\n"

View File

@ -133,7 +133,7 @@ Variable scope escape
$ midml error-variable-scope-escape.midml
Type inference and translation to System F...
File "error-variable-scope-escape.midml", line 2, characters 2-37:
A rigid variable escapes its scope.
A rigid variable of rank 0 escapes its scope 1.
# Option type
@ -602,7 +602,7 @@ its binding scope.
$ midml rigid-level-escape-wrong.midml
Type inference and translation to System F...
File "rigid-level-escape-wrong.midml", line 2, characters 22-23:
A rigid variable escapes its scope.
A rigid variable of rank 0 escapes its scope 1.
The example below is incorrect, a rigid variable tries to escape
@ -622,4 +622,4 @@ adjusting the level of the type nodes below the arrow.
$ midml rigid-level-escape-later-wrong.midml
Type inference and translation to System F...
File "rigid-level-escape-later-wrong.midml", line 2, characters 2-26:
A rigid variable escapes its scope.
A rigid variable of rank 0 escapes its scope 1.

View File

@ -171,6 +171,36 @@ end = struct
(* ------------------------------------------------------------------------ *)
(* Debug printing *)
let to_string doc =
let b = Buffer.create 128 in
PPrint.ToBuffer.pretty 0.9 80 b doc;
Buffer.contents b
let rec print_vertex (S struc) =
Abs.pprint print_vertex struc
let vertex_to_string s =
print_vertex s |> to_string
let print_edge v1 opt =
match opt with
| None ->
Printf.printf "%s\n" (vertex_to_string v1)
| Some (v2, scope) ->
Printf.printf "%s --%d--> %s\n"
(vertex_to_string v1) scope (vertex_to_string v2)
let _print_graph () =
let table =
match !env with
Equations eqenv | Inconsistent eqenv -> eqenv.table
in
Hashtbl.iter print_edge table
(* ------------------------------------------------------------------------ *)
(* Add vertices and edges. *)
let add v =
@ -533,7 +563,7 @@ let project data =
let pprint elem data =
let open PPrint in
utf8format "@%d[%d]" data.id data.rank ^^
utf8format "@%d[rank=%d / scope=%d]" data.id data.rank data.scope ^^
S.pprint elem data.structure
(* [status] and [mark] are currently not printed. *)
@ -609,6 +639,15 @@ let is_representative (V v) =
let fresh structure : variable =
V (make structure)
let rec print_data data =
let f v = get v |> print_data in
Data.pprint f data
let _print data =
let b = Buffer.create 128 in
PPrint.ToBuffer.pretty 0.9 80 b (print_data data);
Buffer.contents b |> Printf.printf "%s\n"
(* -------------------------------------------------------------------------- *)
(* The unifier uses an explicit waiting queue [q] of pending equations,