From 1310ac9a03e69a01444000026bcd1afec2528e3a Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Tue, 30 Aug 2022 21:12:01 -0400 Subject: [PATCH 1/5] add phase tags to traces --- src/core/Asai.ml | 1 + src/core/Asai.mli | 1 + src/core/Diagnostic.ml | 4 ++-- src/core/Logger.ml | 6 +++--- src/core/Logger.mli | 2 +- src/core/LoggerSigs.ml | 25 ++++++++++++------------ src/core/Phase.ml | 8 ++++++++ src/core/logger/DiagnosticBuilder.ml | 8 ++++---- src/core/logger/DiagnosticBuilder.mli | 2 +- src/core/logger/DiagnosticBuilderSigs.ml | 13 ++++++------ src/core/logger/DiagnosticEmitter.ml | 6 +++--- src/core/logger/DiagnosticEmitter.mli | 2 +- src/core/logger/DiagnosticEmitterSigs.ml | 9 +++++---- src/file/Assembler.ml | 6 +++--- src/file/Assembler.mli | 2 +- src/file/Marked.ml | 4 ++-- src/unix/Asai_unix.ml | 20 +++++++++++-------- src/unix/Asai_unix.mli | 14 ++++++------- 18 files changed, 75 insertions(+), 58 deletions(-) create mode 100644 src/core/Phase.ml diff --git a/src/core/Asai.ml b/src/core/Asai.ml index d315a5f..77df42c 100644 --- a/src/core/Asai.ml +++ b/src/core/Asai.ml @@ -2,6 +2,7 @@ module Span = Span module Severity = Severity module Code = Code +module Phase = Phase module Diagnostic = Diagnostic module Logger = Logger diff --git a/src/core/Asai.mli b/src/core/Asai.mli index 8ef670a..55bfd09 100644 --- a/src/core/Asai.mli +++ b/src/core/Asai.mli @@ -22,6 +22,7 @@ module Span = Span module Severity = Severity module Code = Code +module Phase = Phase module Diagnostic = Diagnostic (** {1 Effects} diff --git a/src/core/Diagnostic.ml b/src/core/Diagnostic.ml index 380b3f3..73a3a6c 100644 --- a/src/core/Diagnostic.ml +++ b/src/core/Diagnostic.ml @@ -6,7 +6,7 @@ open Bwd type message = Format.formatter -> unit (** The type of diagnostics. *) -type 'code t = { +type ('code,'phase) t = { code : 'code; (** The message code. *) severity : Severity.t; @@ -15,7 +15,7 @@ type 'code t = { (** The main message. *) additional_marks : Span.t list; (** Additional marking associated with the main message. *) - backtrace : message Span.located bwd; + backtrace : ('phase * message Span.located) bwd; (** The backtrace leading to this diagnostic. *) } diff --git a/src/core/Logger.ml b/src/core/Logger.ml index d86c1f0..2c1290f 100644 --- a/src/core/Logger.ml +++ b/src/core/Logger.ml @@ -1,9 +1,9 @@ module type S = LoggerSigs.S -module Make (Code : Code.S) : S with module Code := Code = +module Make (Code : Code.S) (Phase : Phase.S) : S with module Code := Code and module Phase := Phase = struct - module DE = DiagnosticEmitter.Make(Code) - module DB = DiagnosticBuilder.Make(Code) + module DE = DiagnosticEmitter.Make(Code)(Phase) + module DB = DiagnosticBuilder.Make(Code)(Phase) let backtrace = DB.backtrace let messagef = DB.messagef diff --git a/src/core/Logger.mli b/src/core/Logger.mli index 3ef5650..37fbf5a 100644 --- a/src/core/Logger.mli +++ b/src/core/Logger.mli @@ -1,3 +1,3 @@ module type S = LoggerSigs.S -module Make (Code : Code.S) : S with module Code := Code +module Make (Code : Code.S) (Phase : Phase.S) : S with module Code := Code and module Phase := Phase diff --git a/src/core/LoggerSigs.ml b/src/core/LoggerSigs.ml index fef5367..af91df8 100644 --- a/src/core/LoggerSigs.ml +++ b/src/core/LoggerSigs.ml @@ -1,35 +1,36 @@ module type S = sig module Code : Code.S + module Phase : Phase.S (** [messagef ~loc ~additional_marks ~code format ...] constructs a diagnostic along with the backtrace frames recorded via [tracef]. *) - val messagef : ?loc:Span.t -> ?additional_marks:Span.t list -> ?severity:Severity.t -> code:Code.t -> ('a, Format.formatter, unit, Code.t Diagnostic.t) format4 -> 'a + val messagef : ?loc:Span.t -> ?additional_marks:Span.t list -> ?severity:Severity.t -> code:Code.t -> ('a, Format.formatter, unit, (Code.t, Phase.t) Diagnostic.t) format4 -> 'a (** [kmessagef kont ~loc ~additional_marks ~code format ...] constructs a diagnostic and then apply [kont] to the resulting diagnostic. *) - val kmessagef : (Code.t Diagnostic.t -> 'b) -> ?loc:Span.t -> ?additional_marks:Span.t list -> ?severity:Severity.t -> code:Code.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a + val kmessagef : ((Code.t, Phase.t) Diagnostic.t -> 'b) -> ?loc:Span.t -> ?additional_marks:Span.t list -> ?severity:Severity.t -> code:Code.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a (** [tracef ~loc format ...] record a frame. *) - val tracef : ?loc:Span.t -> ('a, Format.formatter, unit, (unit -> 'b) -> 'b) format4 -> 'a + val tracef : ?loc:Span.t -> Phase.t -> ('a, Format.formatter, unit, (unit -> 'b) -> 'b) format4 -> 'a (** [append_marks msg marks] appends [marks] to the additional marks of [msg]. *) - val append_marks : Code.t Diagnostic.t -> Span.t list -> Code.t Diagnostic.t + val append_marks : (Code.t, Phase.t) Diagnostic.t -> Span.t list -> (Code.t, Phase.t) Diagnostic.t (** Emit a diagnostic and continue the computation. *) - val emit : Code.t Diagnostic.t -> unit + val emit : (Code.t, Phase.t) Diagnostic.t -> unit (** [emitf ~loc ~additional_marks ~code format ...] constructs and emits a diagnostic. *) val emitf : ?loc:Span.t -> ?additional_marks:Span.t list -> ?severity:Severity.t -> code:Code.t -> ('a, Format.formatter, unit, unit) format4 -> 'a (** Emit a diagnostic and abort the computation. *) - val fatal: Code.t Diagnostic.t -> 'a + val fatal: (Code.t, Phase.t) Diagnostic.t -> 'a (** [fatalf ~loc ~additional_marks ~code format ...] constructs a diagnostic and abort the current computation. *) val fatalf : ?loc:Span.t -> ?additional_marks:Span.t list -> ?severity:Severity.t -> code:Code.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a (** [run ~emit ~fatal f] runs the thunk [f], using [emit] to handle emitted diagnostics before continuing the computation, and [fatal] to handle diagnostics after aborting the computation. *) - val run : ?init_backtrace:Diagnostic.message Span.located Bwd.bwd - -> emit:(Code.t Diagnostic.t -> unit) -> fatal:(Code.t Diagnostic.t -> 'a) -> (unit -> 'a) -> 'a + val run : ?init_backtrace:(Phase.t * Diagnostic.message Span.located) Bwd.bwd + -> emit:((Code.t, Phase.t) Diagnostic.t -> unit) -> fatal:((Code.t, Phase.t) Diagnostic.t -> 'a) -> (unit -> 'a) -> 'a (** [bridge m run f] runs the thunk [f] that uses different error codes, using the runner [run] that is intended to a different instance of {!val:run} with a different {!module:Code}. The diagnostics [d] generated by [f] @@ -44,13 +45,13 @@ sig ]} *) val bridge : - ('code Diagnostic.t -> Code.t Diagnostic.t) -> - (?init_backtrace:Diagnostic.message Span.located Bwd__BwdDef.bwd -> - emit:('code Diagnostic.t -> unit) -> fatal:('code Diagnostic.t -> 'a) -> (unit -> 'a) -> 'a) -> + (('code,'phase) Diagnostic.t -> (Code.t, Phase.t) Diagnostic.t) -> + (?init_backtrace:(Phase.t * Diagnostic.message Span.located) Bwd.bwd -> + emit:(('code,'phase) Diagnostic.t -> unit) -> fatal:(('code,'phase) Diagnostic.t -> 'a) -> (unit -> 'a) -> 'a) -> (unit -> 'a) -> 'a (** [try_with ~emit ~fatal f] runs the thunk [f], using [emit] to intercept emitted diagnostics before continuing the computation, and [fatal] to intercept diagnostics after aborting the computation. The default interceptors reperform or reraise the intercepted diagnostics. *) - val try_with : ?emit:(Code.t Diagnostic.t -> unit) -> ?fatal:(Code.t Diagnostic.t -> 'a) -> (unit -> 'a) -> 'a + val try_with : ?emit:((Code.t, Phase.t) Diagnostic.t -> unit) -> ?fatal:((Code.t, Phase.t) Diagnostic.t -> 'a) -> (unit -> 'a) -> 'a end diff --git a/src/core/Phase.ml b/src/core/Phase.ml new file mode 100644 index 0000000..26b854b --- /dev/null +++ b/src/core/Phase.ml @@ -0,0 +1,8 @@ +module type S = +sig + (** The type of tace tags. *) + type t + + (** Get the string representation. *) + val to_string : t -> string +end diff --git a/src/core/logger/DiagnosticBuilder.ml b/src/core/logger/DiagnosticBuilder.ml index 12551e0..fb5d866 100644 --- a/src/core/logger/DiagnosticBuilder.ml +++ b/src/core/logger/DiagnosticBuilder.ml @@ -3,9 +3,9 @@ open Bwd.Infix module type S = DiagnosticBuilderSigs.S -module Make (Code : Code.S) : S with module Code := Code = +module Make (Code : Code.S) (Phase : Phase.S) : S with module Code := Code and module Phase := Phase = struct - type env = Diagnostic.message Span.located bwd + type env = (Phase.t * Diagnostic.message Span.located) bwd module Traces = Algaeff.Reader.Make (struct type nonrec env = env end) let backtrace = Traces.read @@ -26,9 +26,9 @@ struct let append_marks d marks = Diagnostic.{ d with additional_marks = d.additional_marks @ marks } - let tracef ?loc fmt = + let tracef ?loc tag fmt = fmt |> Format.kdprintf @@ fun message f -> - Traces.scope (fun bt -> bt #< { loc; value = message }) f + Traces.scope (fun bt -> bt #< (tag,{ loc; value = message })) f let run ?(init=Emp) f = Traces.run ~env:init f diff --git a/src/core/logger/DiagnosticBuilder.mli b/src/core/logger/DiagnosticBuilder.mli index ce43dc2..e6bc215 100644 --- a/src/core/logger/DiagnosticBuilder.mli +++ b/src/core/logger/DiagnosticBuilder.mli @@ -1,3 +1,3 @@ module type S = DiagnosticBuilderSigs.S -module Make (Code : Code.S) : S with module Code := Code +module Make (Code : Code.S) (Phase : Phase.S) : S with module Code := Code and module Phase := Phase diff --git a/src/core/logger/DiagnosticBuilderSigs.ml b/src/core/logger/DiagnosticBuilderSigs.ml index b10b5f9..14487d3 100644 --- a/src/core/logger/DiagnosticBuilderSigs.ml +++ b/src/core/logger/DiagnosticBuilderSigs.ml @@ -1,12 +1,13 @@ module type S = sig module Code : Code.S + module Phase : Phase.S - val backtrace : unit -> Diagnostic.message Span.located Bwd.bwd - val messagef : ?loc:Span.t -> ?additional_marks:Span.t list -> ?severity:Severity.t -> code:Code.t -> ('a, Format.formatter, unit, Code.t Diagnostic.t) format4 -> 'a - val kmessagef : (Code.t Diagnostic.t -> 'b) -> ?loc:Span.t -> ?additional_marks:Span.t list -> ?severity:Severity.t -> code:Code.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a - val tracef : ?loc:Span.t -> ('a, Format.formatter, unit, (unit -> 'b) -> 'b) format4 -> 'a - val append_marks : Code.t Diagnostic.t -> Span.t list -> Code.t Diagnostic.t + val backtrace : unit -> (Phase.t * Diagnostic.message Span.located) Bwd.bwd + val messagef : ?loc:Span.t -> ?additional_marks:Span.t list -> ?severity:Severity.t -> code:Code.t -> ('a, Format.formatter, unit, (Code.t,Phase.t) Diagnostic.t) format4 -> 'a + val kmessagef : ((Code.t,Phase.t) Diagnostic.t -> 'b) -> ?loc:Span.t -> ?additional_marks:Span.t list -> ?severity:Severity.t -> code:Code.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a + val tracef : ?loc:Span.t -> Phase.t -> ('a, Format.formatter, unit, (unit -> 'b) -> 'b) format4 -> 'a + val append_marks : (Code.t,Phase.t) Diagnostic.t -> Span.t list -> (Code.t,Phase.t) Diagnostic.t - val run : ?init:Diagnostic.message Span.located Bwd.bwd -> (unit -> 'a) -> 'a + val run : ?init:((Phase.t * Diagnostic.message Span.located) Bwd.bwd) -> (unit -> 'a) -> 'a end diff --git a/src/core/logger/DiagnosticEmitter.ml b/src/core/logger/DiagnosticEmitter.ml index d286d21..0bea96d 100644 --- a/src/core/logger/DiagnosticEmitter.ml +++ b/src/core/logger/DiagnosticEmitter.ml @@ -1,9 +1,9 @@ module type S = DiagnosticEmitterSigs.S -module Make (Code : Code.S) : S with module Code := Code = +module Make (Code : Code.S) (Phase : Phase.S) : S with module Code := Code and module Phase := Phase = struct - type _ Effect.t += Emit : Code.t Diagnostic.t -> unit Effect.t - exception Fatal of Code.t Diagnostic.t + type _ Effect.t += Emit : (Code.t, Phase.t) Diagnostic.t -> unit Effect.t + exception Fatal of (Code.t, Phase.t) Diagnostic.t let emit d = Effect.perform @@ Emit d let fatal d = raise @@ Fatal d diff --git a/src/core/logger/DiagnosticEmitter.mli b/src/core/logger/DiagnosticEmitter.mli index 9360124..a8b91ff 100644 --- a/src/core/logger/DiagnosticEmitter.mli +++ b/src/core/logger/DiagnosticEmitter.mli @@ -1,3 +1,3 @@ module type S = DiagnosticEmitterSigs.S -module Make (Code : Code.S) : S with module Code := Code +module Make (Code : Code.S) (Phase : Phase.S) : S with module Code := Code and module Phase := Phase diff --git a/src/core/logger/DiagnosticEmitterSigs.ml b/src/core/logger/DiagnosticEmitterSigs.ml index 3f77ece..4eaed55 100644 --- a/src/core/logger/DiagnosticEmitterSigs.ml +++ b/src/core/logger/DiagnosticEmitterSigs.ml @@ -1,18 +1,19 @@ module type S = sig module Code : Code.S + module Phase : Phase.S (** Emit a diagnostic and continue the computation. *) - val emit : Code.t Diagnostic.t -> unit + val emit : (Code.t, Phase.t) Diagnostic.t -> unit (** Emit a diagnostic and abort the computation. *) - val fatal: Code.t Diagnostic.t -> 'a + val fatal: (Code.t, Phase.t) Diagnostic.t -> 'a (** [run ~emit ~fatal f] runs the thunk [f], using [emit] to handle emitted diagnostics before continuing the computation, and [fatal] to handle diagnostics after aborting the computation. *) - val run : emit:(Code.t Diagnostic.t -> unit) -> fatal:(Code.t Diagnostic.t -> 'a) -> (unit -> 'a) -> 'a + val run : emit:((Code.t, Phase.t) Diagnostic.t -> unit) -> fatal:((Code.t, Phase.t) Diagnostic.t -> 'a) -> (unit -> 'a) -> 'a (** [try_with ~emit ~fatal f] runs the thunk [f], using [emit] to intercept emitted diagnostics before continuing the computation, and [fatal] to intercept diagnostics after aborting the computation. *) - val try_with : ?emit:(Code.t Diagnostic.t -> unit) -> ?fatal:(Code.t Diagnostic.t -> 'a) -> (unit -> 'a) -> 'a + val try_with : ?emit:((Code.t, Phase.t) Diagnostic.t -> unit) -> ?fatal:((Code.t, Phase.t) Diagnostic.t -> 'a) -> (unit -> 'a) -> 'a end diff --git a/src/file/Assembler.ml b/src/file/Assembler.ml index abca78e..8d6db11 100644 --- a/src/file/Assembler.ml +++ b/src/file/Assembler.ml @@ -2,7 +2,7 @@ open Bwd module type S = sig - val assemble : splitting_threshold:int -> 'code Asai.Diagnostic.t -> 'code Marked.t + val assemble : splitting_threshold:int -> ('code,'phase) Asai.Diagnostic.t -> ('code,'phase) Marked.t end module Make (R : Reader.S) = @@ -24,12 +24,12 @@ struct let message ~splitting_threshold ~additional_marks (msg : _ Asai.Span.located) = sections ~splitting_threshold ~additional_marks msg.loc, msg.value - let assemble ~splitting_threshold (d : 'code Asai.Diagnostic.t) = + let assemble ~splitting_threshold (d : ('code,'phase) Asai.Diagnostic.t) = R.run @@ fun () -> Marked.{ code = d.code; severity = d.severity; message = message ~splitting_threshold ~additional_marks:d.additional_marks d.message; - backtrace = Bwd.map (message ~splitting_threshold ~additional_marks:[]) d.backtrace; + backtrace = Bwd.map (fun (tag,msg) -> (tag,message ~splitting_threshold ~additional_marks:[] msg)) d.backtrace; } end diff --git a/src/file/Assembler.mli b/src/file/Assembler.mli index ae87a63..82295c2 100644 --- a/src/file/Assembler.mli +++ b/src/file/Assembler.mli @@ -1,7 +1,7 @@ module type S = sig (** [assemble ~splitting_threshold d] reads the file content and flatten the spans into marked text. *) - val assemble : splitting_threshold:int -> 'code Asai.Diagnostic.t -> 'code Marked.t + val assemble : splitting_threshold:int -> ('code,'phase) Asai.Diagnostic.t -> ('code,'phase) Marked.t end module Make (R : Reader.S) : S diff --git a/src/file/Marked.ml b/src/file/Marked.ml index 6aa9ef1..12c176d 100644 --- a/src/file/Marked.ml +++ b/src/file/Marked.ml @@ -19,9 +19,9 @@ type section = { file_path : string; blocks : block list } type message = section list * Asai.Diagnostic.message (** a message *) -type 'code t = +type ('code,'phase) t = { code : 'code ; severity : Asai.Severity.t ; message : message - ; backtrace : message bwd + ; backtrace : ('phase * message) bwd } diff --git a/src/unix/Asai_unix.ml b/src/unix/Asai_unix.ml index 90660d5..fdac007 100644 --- a/src/unix/Asai_unix.ml +++ b/src/unix/Asai_unix.ml @@ -5,7 +5,7 @@ open Asai open Notty open Notty.Infix -module Make (Code : Code.S) = +module Make (Code : Code.S) (Phase : Phase.S) = struct let vline ~attr height str = I.vcat @@ List.init height (fun _ -> I.string ~attr str) @@ -75,27 +75,31 @@ struct header <-> (sections |> List.map (fun s -> s |> section |> I.vpad 0 2) |> I.vcat) |> I.vcrop 0 2 - let display_marked debug (m : 'code Asai_file.Marked.t) = + let display_marked trace_phases (m : ('code,'phase) Asai_file.Marked.t) = + let traces = + (m.backtrace |> Bwd.filter_map (fun (p,t) -> if trace_phases p then t |> display_message m.code m.severity |> I.vpad 0 1 |> Option.some else None) + |> Bwd.to_list |> List.rev) + in I.vpad 1 1 (display_message m.code m.severity m.message) <-> - if debug then + if List.length traces > 0 then I.string "Trace" <-> I.string "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━" <-> I.string "" <-> - (m.backtrace |> Bwd.map (fun t -> t |> display_message m.code m.severity |> I.vpad 0 1) |> Bwd.to_list |> List.rev |> I.vcat) + I.vcat traces else I.void 0 0 module Assemble = Asai_file.Assembler.Make(Asai_file.FileReader) - let display ?(display_traces = false) diag = + let display trace_phases diag = let m = Assemble.assemble ~splitting_threshold:5 diag in - Notty_unix.output_image (display_marked display_traces m) + Notty_unix.output_image (display_marked trace_phases m) - let interactive_trace diag = + let interactive_trace trace_phases diag = let m = Assemble.assemble ~splitting_threshold:5 diag in let traces = Bwd.append - (m.backtrace |> Bwd.map (display_message m.code m.severity)) + (m.backtrace |> Bwd.filter_map (fun (p,t) -> if trace_phases p then t |> display_message m.code m.severity |> Option.some else None)) [display_message m.code m.severity m.message] |> Bwd.to_list |> List.rev |> Array.of_list in let len = Array.length traces in diff --git a/src/unix/Asai_unix.mli b/src/unix/Asai_unix.mli index 5887d53..c1111a5 100644 --- a/src/unix/Asai_unix.mli +++ b/src/unix/Asai_unix.mli @@ -4,14 +4,14 @@ open Asai (** {1 Display} This module provides functions to display and interact with Asai diagnostics in UNIX terminals. *) -module Make (Code : Code.S) : sig - (** [display ?display_traces diag] displays the message provided in [diag], - along with relevant text from its span, optionally displaying the traces in [diag] +module Make (Code : Code.S) (Phase : Phase.S) : sig + (** [display trace_phases diag] displays the message provided in [diag], + along with relevant text from its span, optionally displaying the traces in [diag] filtered by [trace_phases] *) - val display : ?display_traces:bool -> Code.t Diagnostic.t -> unit + val display : (Phase.t -> bool) -> (Code.t, Phase.t) Diagnostic.t -> unit - (** [interactive_trace diag] drops the user in a small interactive terminal app where they can cycle through - the message provided in [diag] and its traces + (** [interactive_trace trace_phases diag] drops the user in a small interactive terminal app where they can cycle through + the message provided in [diag] and its traces, filtered by [trace_phases] *) - val interactive_trace : Code.t Diagnostic.t -> unit + val interactive_trace : (Phase.t -> bool) -> (Code.t, Phase.t) Diagnostic.t -> unit end From b49dfa3a4480a55f91928b50992271aa1ef7f3a5 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Tue, 30 Aug 2022 21:12:08 -0400 Subject: [PATCH 2/5] update example --- examples/stlc/{Doctor.ml => ErrorLogger.ml} | 17 +++++++++-- examples/stlc/Grammar.mly | 2 ++ examples/stlc/STLC.ml | 34 +++++++++++---------- examples/stlc/example2.lambda | 1 + 4 files changed, 36 insertions(+), 18 deletions(-) rename examples/stlc/{Doctor.ml => ErrorLogger.ml} (74%) create mode 100644 examples/stlc/example2.lambda diff --git a/examples/stlc/Doctor.ml b/examples/stlc/ErrorLogger.ml similarity index 74% rename from examples/stlc/Doctor.ml rename to examples/stlc/ErrorLogger.ml index c5a19be..80fd3d5 100644 --- a/examples/stlc/Doctor.ml +++ b/examples/stlc/ErrorLogger.ml @@ -7,6 +7,11 @@ type code = | RequiresAnnotation | LexerError | ParseError + +type phase = + | Elaboration + | Conversion + module Code : Asai.Code.S with type t = code = struct type t = code @@ -32,5 +37,13 @@ struct "The parser encountered an error." end -module Logger = Asai.Logger.Make(Code) -include Logger +module Phase : Asai.Phase.S with type t = phase = +struct + type t = phase + + let to_string = function + | Elaboration -> "Elaboration" + | Conversion -> "Conversion" +end + +include Asai.Logger.Make(Code)(Phase) diff --git a/examples/stlc/Grammar.mly b/examples/stlc/Grammar.mly index 5123cf3..869a117 100644 --- a/examples/stlc/Grammar.mly +++ b/examples/stlc/Grammar.mly @@ -57,3 +57,5 @@ term_: { Suc a } | LPR; NAT_REC; z = term; s = term; scrut = term; RPR { NatRec(z, s, scrut) } + | LPR; f = term; x = term; RPR + { Ap (f,x) } diff --git a/examples/stlc/STLC.ml b/examples/stlc/STLC.ml index 54b209e..b200248 100644 --- a/examples/stlc/STLC.ml +++ b/examples/stlc/STLC.ml @@ -3,7 +3,7 @@ open Bwd open Syntax -module Terminal = Asai_unix.Make(Doctor.Code) +module Terminal = Asai_unix.Make(ErrorLogger.Code)(ErrorLogger.Phase) module Elab = struct @@ -25,13 +25,13 @@ struct match Bwd.find_opt (fun (nm', _) -> String.equal nm nm') ctx with | Some (_, tp) -> tp | None -> - Doctor.fatalf ?loc ~code:UnboundVariable "Variable '%s' is not in scope" nm + ErrorLogger.fatalf ?loc ~code:UnboundVariable "Variable '%s' is not in scope" nm let expected_connective conn tp = - Doctor.fatalf ?loc:(get_loc ()) ~code:TypeError "Expected a %s, but got %a." conn pp_tp tp + ErrorLogger.fatalf ?loc:(get_loc ()) ~code:TypeError "Expected a %s, but got %a." conn pp_tp tp let rec equate expected actual = - Doctor.tracef "When Equating" @@ fun () -> + ErrorLogger.tracef ?loc:(get_loc ()) Conversion "When Equating %a with %a" pp_tp expected pp_tp actual @@ fun () -> match expected, actual with | Fun (a0, b0), Fun (a1, b1) -> equate a0 a1; @@ -42,10 +42,10 @@ struct | Nat, Nat -> () | _, _ -> - Doctor.fatalf ?loc:(get_loc ()) ~code:TypeError "Expected type %a, but got %a." pp_tp expected pp_tp actual + ErrorLogger.fatalf ?loc:(get_loc ()) ~code:TypeError "Expected type %a, but got %a." pp_tp expected pp_tp actual let rec chk (tm : tm) (tp : tp) : unit = - Doctor.tracef ?loc:tm.loc "When checking against %a" Syntax.pp_tp tp @@ fun () -> + ErrorLogger.tracef ?loc:tm.loc Elaboration "When checking against %a" Syntax.pp_tp tp @@ fun () -> locate tm.loc @@ fun () -> match tm.value, tp with | Lam (nm, body), Fun (a, b) -> @@ -71,7 +71,7 @@ struct equate tp actual_tp and syn (tm : tm) : tp = - Doctor.tracef ?loc:tm.loc "When synthesizing" @@ fun () -> + ErrorLogger.tracef ?loc:tm.loc Elaboration "When synthesizing" @@ fun () -> locate tm.loc @@ fun () -> match tm.value with | Var nm -> @@ -109,7 +109,7 @@ struct mot end | _ -> - Doctor.fatalf ?loc:(get_loc ()) ~code:TypeError "Unable to infer type" + ErrorLogger.fatalf ?loc:(get_loc ()) ~code:TypeError "Unable to infer type" end module Driver = @@ -121,10 +121,10 @@ struct try Grammar.defn Lex.token lexbuf with | Lex.SyntaxError tok -> let pos = Span.of_lex_position lexbuf.lex_curr_p in - Doctor.fatalf ~loc:(Span.make pos pos) ~code:LexerError "Unrecognized token '%s'" tok + ErrorLogger.fatalf ~loc:(Span.make pos {pos with offset = pos.offset + 1}) ~code:LexerError "Unrecognized token '%s'" tok | Grammar.Error -> let pos = Span.of_lex_position lexbuf.lex_curr_p in - Doctor.fatalf ~loc:(Span.make pos pos) ~code:LexerError "Failed to parse" + ErrorLogger.fatalf ~loc:(Span.make pos {pos with offset = pos.offset + 1}) ~code:LexerError "Failed to parse" in Elab.Reader.run ~env:{ctx = Emp ; loc = None} @@ fun () -> Elab.chk tm tp @@ -132,23 +132,25 @@ struct let load mode filepath = let display = match mode with - | `Debug -> Terminal.display ~display_traces:true - | `Normal -> Terminal.display ~display_traces:false - | `Interactive -> Terminal.interactive_trace + | `Debug -> Terminal.display (fun _ -> true) + | `Normal -> Terminal.display (fun _ -> false) + | `Interactive phases -> Terminal.interactive_trace phases in - Doctor.run ~emit:display ~fatal:display @@ fun () -> + ErrorLogger.run ~emit:display ~fatal:display @@ fun () -> load_file filepath end let () = let mode = - if Array.length Sys.argv < 2 then + if Array.length Sys.argv < 3 then `Normal else match Sys.argv.(2) with | "--debug" | "-d" -> `Debug - | "--interactive" | "-i" -> `Interactive + | "--interactive" | "-i" -> `Interactive (fun _ -> true) + | "--interactive=elab" | "-i=elab" -> `Interactive (function ErrorLogger.Elaboration -> true | _ -> false) + | "--interactive=conv" | "-i=conv" -> `Interactive (function ErrorLogger.Conversion -> true | _ -> false) | _ -> failwith "Unrecognized argument" in Driver.load mode Sys.argv.(1) \ No newline at end of file diff --git a/examples/stlc/example2.lambda b/examples/stlc/example2.lambda new file mode 100644 index 0000000..d4b70f7 --- /dev/null +++ b/examples/stlc/example2.lambda @@ -0,0 +1 @@ +(check (λ f (λ x (f x))) (→ (→ nat nat) (→ (× nat nat) nat))) From 45127a3e91a246bd4ed27d5e6e821028cd01cae7 Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Wed, 31 Aug 2022 09:11:42 -0400 Subject: [PATCH 3/5] PR comments --- src/core/Diagnostic.ml | 2 +- src/core/Phase.ml | 2 +- src/file/Assembler.ml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/core/Diagnostic.ml b/src/core/Diagnostic.ml index 73a3a6c..c12cf99 100644 --- a/src/core/Diagnostic.ml +++ b/src/core/Diagnostic.ml @@ -20,4 +20,4 @@ type ('code,'phase) t = { } (** Mapping the code *) -let map f d = {d with code = f d.code} +let map f g d = {d with code = f d.code ; backtrace = Bwd.map (fun (p,t) -> (g p,t)) d.backtrace} diff --git a/src/core/Phase.ml b/src/core/Phase.ml index 26b854b..9623de4 100644 --- a/src/core/Phase.ml +++ b/src/core/Phase.ml @@ -1,6 +1,6 @@ module type S = sig - (** The type of tace tags. *) + (** The type of trace phases. *) type t (** Get the string representation. *) diff --git a/src/file/Assembler.ml b/src/file/Assembler.ml index 8d6db11..9edadcc 100644 --- a/src/file/Assembler.ml +++ b/src/file/Assembler.ml @@ -30,6 +30,6 @@ struct code = d.code; severity = d.severity; message = message ~splitting_threshold ~additional_marks:d.additional_marks d.message; - backtrace = Bwd.map (fun (tag,msg) -> (tag,message ~splitting_threshold ~additional_marks:[] msg)) d.backtrace; + backtrace = Bwd.map (fun (p,t) -> (p,message ~splitting_threshold ~additional_marks:[] t)) d.backtrace; } end From b70d124b4163cec7fa3cbbace1d04866be35f82f Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Wed, 31 Aug 2022 09:12:43 -0400 Subject: [PATCH 4/5] update bride comment --- src/core/LoggerSigs.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/core/LoggerSigs.ml b/src/core/LoggerSigs.ml index af91df8..82bcc18 100644 --- a/src/core/LoggerSigs.ml +++ b/src/core/LoggerSigs.ml @@ -41,7 +41,7 @@ sig module M1 = Logger.Make(Code1) module M2 = Logger.Make(Code2) - M1.bridge (Diagnostic.map code_mapper) M2.run @@ fun () -> ... + M1.bridge (Diagnostic.map code_mapper phase_mapper) M2.run @@ fun () -> ... ]} *) val bridge : From 14e3ea020de9c8edc5d13b55285b90d3d100989b Mon Sep 17 00:00:00 2001 From: Matthew McQuaid Date: Wed, 31 Aug 2022 13:36:06 -0400 Subject: [PATCH 5/5] fix a name --- src/core/logger/DiagnosticBuilder.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/core/logger/DiagnosticBuilder.ml b/src/core/logger/DiagnosticBuilder.ml index fb5d866..a7601b1 100644 --- a/src/core/logger/DiagnosticBuilder.ml +++ b/src/core/logger/DiagnosticBuilder.ml @@ -26,9 +26,9 @@ struct let append_marks d marks = Diagnostic.{ d with additional_marks = d.additional_marks @ marks } - let tracef ?loc tag fmt = + let tracef ?loc phase fmt = fmt |> Format.kdprintf @@ fun message f -> - Traces.scope (fun bt -> bt #< (tag,{ loc; value = message })) f + Traces.scope (fun bt -> bt #< (phase,{ loc; value = message })) f let run ?(init=Emp) f = Traces.run ~env:init f