feat: ⛎ Trace Phases

examples/stlc/Doctor.ml → 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)

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) }

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,34 +121,36 @@ 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
 
   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)

examples/stlc/example2.lambda

@@ -0,0 +1 @@
+(check (λ f (λ x (f x))) (→ (→ nat nat) (→ (× nat nat) nat)))

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

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}

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. *)
 }
 

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

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

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

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

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
 

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

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

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

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

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

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

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

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
   }