Upgrade asai to 0.1

lib/elab/Elaborator.ml

@@ -11,7 +11,7 @@ module Internal =
 struct
   let rec chk (tm : CS.t) =
     T.Chk.locate tm.loc @@
-    match tm.node with
+    match tm.value with
     | CS.Lam (names, tm) ->
       chk_lams names tm
     | CS.LamSyn (qs, tm) ->
@@ -55,7 +55,7 @@ struct
 
   and neg_chk (tm : CS.t) =
     T.NegChk.locate tm.loc @@
-    match tm.node with
+    match tm.value with
     | CS.NegPair (a, name, b) ->
       NegSigma.intro (neg_chk a) ~name (fun _ -> neg_chk b)
     | CS.Drop ->
@@ -92,7 +92,7 @@ struct
 
   and syn (tm : CS.t) =
     T.Syn.locate tm.loc @@
-    match tm.node with
+    match tm.value with
     | CS.LamSyn (qs, tm) ->
       List.fold_left
         (fun b (names, a) ms -> Pi.intro_syn ~names (chk a) (fun ns -> b (ms @ ns)))
@@ -160,7 +160,7 @@ struct
 
   and neg_syn (tm : CS.t) =
     T.NegSyn.locate tm.loc @@
-    match tm.node with
+    match tm.value with
     | CS.Var path ->
       begin
         match T.Locals.resolve_neg path with
@@ -184,7 +184,7 @@ struct
 
   and hom (tm : CS.t) =
     T.Hom.locate tm.loc @@
-    match tm.node with
+    match tm.value with
     | Set (pos, neg, steps) ->
       Hom.set (chk pos) (neg_syn neg) (hom steps)
     | HomAp (pos, neg, phi, pos_name, neg_name, steps) ->
@@ -204,7 +204,7 @@ struct
 
   and prog (tm : CS.t) =
     T.Prog.locate tm.loc @@
-    match tm.node with
+    match tm.value with
     | Set (pos, neg, steps) ->
       Prog.set (chk pos) (neg_syn neg) (prog steps)
     | HomAp (pos, neg, phi, pos_name, neg_name, steps) ->

lib/elab/Syntax.ml

@@ -1,13 +1,10 @@
-open Asai
 open Core
 
 type labelset = string list
 type label = string
 type 'a labeled = (string * 'a) list
 
-type 'a node = { node : 'a; loc : Span.t }
-
-type t = t_ node
+type t = t_ Asai.Span.located
 and t_ =
   | Var of Yuujinchou.Trie.path
   | Pi of (Ident.binder list * t) list * t

lib/errors/Code.ml

@@ -12,7 +12,7 @@ type t =
   | `LoadFailure
   ]
 
-let default_severity _ = Asai.Severity.Error
+let default_severity _ = Asai.Diagnostic.Error
 
 let to_string : t -> string =
   function

lib/loader/Loader.ml

@@ -2,7 +2,7 @@ open Errors
 open Parser
 open Vernacular
 
-module Terminal = Asai_unix.Make(Code)
+module Terminal = Asai.Tty.Make(Code)
 
 type env = { manager : Bantorra.Manager.t; lib : Bantorra.Manager.library }
 
@@ -13,9 +13,9 @@ let parse_file path =
   lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = path };
   try Grammar.commands Lex.token lexbuf with
   | Lex.SyntaxError tok ->
-    Logger.fatalf ~loc:(Span.of_lex lexbuf) `LexError {|Unrecognized token "%s"|} (String.escaped tok)
+    Logger.fatalf ~loc:(Span.of_lexbuf lexbuf) `LexError {|Unrecognized token "%s"|} (String.escaped tok)
   | Grammar.Error ->
-    Logger.fatalf ~loc:(Span.of_lex lexbuf) `ParseError "Failed to parse"
+    Logger.fatalf ~loc:(Span.of_lexbuf lexbuf) `ParseError "Failed to parse"
 
 let load_file (unitpath : Bantorra.Manager.path) =
   let env = Eff.read () in
@@ -25,7 +25,7 @@ let load_file (unitpath : Bantorra.Manager.path) =
 
 let initialize_bantorra dir =
   let open Bantorra in
-  let router = 
+  let router =
     Router.dispatch @@
     function
     | "file" -> Option.some @@
@@ -38,11 +38,11 @@ let initialize_bantorra dir =
   { manager; lib }
 
 let load path debug =
-  let open Bantorra in
+  let module B = Bantorra in
   Logger.run ~emit:Terminal.display ~fatal:Terminal.display @@ fun () ->
-  Logger.wrap (Asai.Diagnostic.map (fun _ -> `LoadFailure)) Bantorra.Error.run @@ fun () ->
-  let dir = FilePath.parent @@ FilePath.of_string ~relative_to:(File.get_cwd ()) path in
-  Format.eprintf "Entering directory '%s'@." (FilePath.to_string dir);
+  Logger.adopt (Asai.Diagnostic.map (fun _ -> `LoadFailure)) B.Logger.run @@ fun () ->
+  let dir = B.FilePath.parent @@ B.FilePath.of_string ~relative_to:(B.File.get_cwd ()) path in
+  Format.eprintf "Entering directory '%s'@." (Bantorra.FilePath.to_string dir);
   let env = initialize_bantorra dir in
   Eff.run ~env @@ fun () ->
   let cmds = parse_file path in

lib/loader/dune

@@ -1,4 +1,4 @@
 (library
   (name Loader)
   (public_name polytt.loader)
-  (libraries polytt.errors polytt.parser polytt.vernacular asai.unix bantorra))
+  (libraries polytt.errors polytt.parser polytt.vernacular asai bantorra))

lib/parser/Grammar.mly

@@ -4,20 +4,15 @@ open Asai
 module CS = Vernacular.Syntax
 module Ident = Core.Ident
 
-let locate (start, stop) node =
-  {CS.node; loc = Span.make (Span.of_lex_position start) (Span.of_lex_position stop)}
-
-let unlocate {CS.node; loc = _} = node
-let get_loc {CS.loc; node = _} = loc
-let clonecate other node =
-  { CS.node;
-    loc = get_loc other
-  }
-let duolocate (starter, stopper) node =
-  { CS.node;
-    loc = Span.make
-      (fst @@ Span.to_positions @@ get_loc starter)
-      (snd @@ Span.to_positions @@ get_loc stopper)
+let unlocate ({value; _} : _ Asai.Span.located) = value
+let get_loc ({loc; _} : _ Asai.Span.located) = Option.get loc
+let clonecate other value : _ Asai.Span.located =
+  { other with value }
+let duolocate (starter, stopper) value : _ Asai.Span.located =
+  { value;
+    loc = Option.some @@ Span.make
+      (fst @@ Span.split @@ get_loc starter,
+       snd @@ Span.split @@ get_loc stopper)
   }
 
 
@@ -86,7 +81,7 @@ let rec fold_pat = fun t ->
 %inline
 located(X):
   | e = X
-    { locate $loc e }
+    { Asai.Span.locate_lex $loc e }
 
 path:
   | path = PATH
@@ -193,7 +188,7 @@ let_binding:
   | LET; nm = pattern; COLON_EQUALS; tm1 = term; IN; tm2 = term
     { CS.Let (nm, tm1, tm2) }
   | LET; nm = pattern; COLON; ty1 = term; COLON_EQUALS; tm1 = term; IN; tm2 = term
-    { CS.Let (nm, { node = Anno(tm1, ty1) ; loc = get_loc tm1 }, tm2) }
+    { CS.Let (nm, clonecate tm1 (CS.Anno(tm1, ty1)), tm2) }
 
 labeled_field(sep):
   | label = LABEL; sep; term = term;

lib/refiner/Eff.ml

@@ -385,26 +385,22 @@ end
 
 module Error =
 struct
-  module Eff = Algaeff.Reader.Make(struct type nonrec env = Span.t end)
-
   let error code fmt =
-    let loc = Eff.read () in
-    Logger.fatalf ~loc:loc code fmt
+    Logger.fatalf code fmt
 
   let type_error tp conn =
-    let loc = Eff.read () in
     let env = Locals.qenv () in
     let ppenv = Locals.ppenv () in
     let qtp = Quote.quote ~env ~tp:D.Univ tp in
-    Logger.fatalf ~loc:loc `TypeError "Expected %a, but got %s@."
+    Logger.fatalf `TypeError "Expected %a, but got %s@."
       (S.pp ppenv Precedence.isolated) qtp
       conn
 
   let locate loc k =
-    Eff.scope (fun _ -> loc) k
+    Logger.merge_loc loc k
 
   let run ~loc k =
-    Eff.run ~env:loc k
+    Logger.with_loc loc k
 end
 
 module Hole =

lib/refiner/Eff.mli

@@ -47,8 +47,8 @@ end
 module Error : sig
   val error : Code.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a
   val type_error : D.t -> string -> 'a
-  val locate : Span.t -> (unit -> 'a) -> 'a
-  val run : loc:Span.t -> (unit -> 'a) -> 'a
+  val locate : Span.t option -> (unit -> 'a) -> 'a
+  val run : loc:Span.t option -> (unit -> 'a) -> 'a
 end
 
 module Hole : sig
@@ -70,4 +70,3 @@ val do_nat_elim : mot:D.t -> zero:D.t -> succ:D.t -> scrut:D.t -> D.t
 val do_base : D.t -> D.t
 val do_fib : D.t -> D.t -> D.t
 val do_hom_elim : D.t -> D.t -> D.t
-

lib/refiner/Tactic.ml

@@ -13,7 +13,7 @@ module rec Chk : sig
   val run : tac -> D.tp -> S.t
   val run2 : tac -> D.tp -> D.tp -> (S.t * bool)
   val syn : Syn.tac -> Chk.tac
-  val locate : Asai.Span.t -> tac -> tac
+  val locate : Asai.Span.t option -> tac -> tac
 end =
 struct
   type tac = D.tp -> S.t
@@ -34,7 +34,7 @@ and Syn : sig
   val rule : (unit -> D.tp * S.t) -> tac
   val run : tac -> D.tp * S.t
   val ann : Chk.tac -> Chk.tac -> tac
-  val locate : Asai.Span.t -> tac -> tac
+  val locate : Asai.Span.t option -> tac -> tac
 end =
 struct
   type tac = unit -> D.tp * S.t
@@ -54,7 +54,7 @@ and Hom : sig
   type tac
   val rule : (D.t * (unit -> S.t) -> S.t) -> tac
   val run : tac -> D.t * (unit -> S.t) -> S.t
-  val locate : Asai.Span.t -> tac -> tac
+  val locate : Asai.Span.t option -> tac -> tac
 end =
 struct
   type tac = D.t * (unit -> S.t) -> S.t
@@ -70,7 +70,7 @@ and Prog : sig
   type tac
   val rule : (unit -> unit) -> tac
   val run : tac -> unit -> unit
-  val locate : Asai.Span.t -> tac -> tac
+  val locate : Asai.Span.t option -> tac -> tac
 end =
 struct
   type tac = unit -> unit
@@ -86,7 +86,7 @@ and NegChk : sig
   val rule : (D.t -> (D.t -> unit)) -> tac
   val run : tac -> D.t -> (D.t -> unit)
   val syn : NegSyn.tac -> tac
-  val locate : Asai.Span.t -> tac -> tac
+  val locate : Asai.Span.t option -> tac -> tac
 end =
 struct
   type tac = D.t -> (D.t -> unit)
@@ -106,7 +106,7 @@ and NegSyn : sig
   type tac
   val rule : (unit -> D.t * (D.t -> unit)) -> tac
   val run : tac -> D.t * (D.t -> unit)
-  val locate : Asai.Span.t -> tac -> tac
+  val locate : Asai.Span.t option -> tac -> tac
 end =
 struct
   type tac = unit -> D.t * (D.t -> unit)

lib/vernacular/Driver.ml

@@ -28,7 +28,7 @@ let normalize tm =
     S.pp_toplevel ntm
 
 let rec execute_cmd  (cmd : CS.cmd) =
-  match cmd.node with
+  match cmd.value with
   | CS.Def {name; tp = Some tp; tm} ->
     Debug.print "-------------------------------------------------@.";
     Debug.print "> Elaborating %a@." Ident.pp name;

lib/vernacular/Syntax.ml

@@ -1,7 +1,7 @@
 include Elab.Syntax
 open Core
 
-type cmd = cmd_ node
+type cmd = cmd_ Asai.Span.located
 and cmd_ =
   | Def of { name : Ident.t; tp : t option; tm : t }
   | Fail of { name: Ident.t; tp : t option; tm : t }

polytt.opam

@@ -15,7 +15,7 @@ depends: [
   "algaeff" {>= "0.2"}
   "eio" {< "0.9"}
   "alcotest"
-  "asai"
+  "asai" {>= "0.1"}
   "bantorra"
   "bwd" {>= "1.1"}
   "cmdliner" {>= "1.1"}
@@ -37,7 +37,6 @@ build: [
   ]
 ]
 pin-depends: [
-  [ "asai.0.1.0~dev" "git+https://github.com/RedPRL/asai#4b0679bb051e9a820596d830d29dd74915521802" ]
-  [ "bantorra.0.2.0~dev" "git+https://github.com/RedPRL/bantorra#ce619fbf8f87f24c5c93847af6721cfcdb7c85be" ]
+  [ "bantorra.0.2.0~dev" "git+https://github.com/RedPRL/bantorra#e83d74b0e1318317bc1adc486191862fb6e8bfc8" ]
 ]
 dev-repo: "git+https://github.com/ToposInstitute/polytt.git"

test/test.expected

@@ -31,15 +31,14 @@ Here is the context!
 - y⁻ : fib Q (fst (snd _ (borrow p⁻)))
 ──────────────
 
-
     🭁 ./hole/eval.poly
     │
  10 │     return q⁺ ⇜ λ⁻ q →
  11 │       x⁻ ← f q;
  12 │       -- y⁻ involves (borrow p⁻)
  13 │       ?
-    │
-    █ [E010] Didn't use all your linear variables in hom.
+    ┷
+ [E010] Didn't use all your linear variables in hom.
 --------------------[./hole/let.poly]--------------------
 
 Encountered hole with known type!
@@ -72,12 +71,11 @@ Encountered negative hole with known type!
 ──────────────
 - ⊢ ?1 : fib P ?0
 
-
-   🭁 ./hole/morph1.poly
-   │
- 3 │     return ? ⇜ ?
-   │
-   █ [E010] Didn't use all your linear variables in hom.
+    🭁 ./hole/morph1.poly
+    │
+  3 │     return ? ⇜ ?
+    ┷
+ [E010] Didn't use all your linear variables in hom.
 --------------------[./hole/morph2.poly]--------------------
 
 Encountered hole with known type!
@@ -87,13 +85,12 @@ Encountered hole with known type!
 ──────────────
 + ⊢ ?0 : base P
 
-
-   🭁 ./hole/morph2.poly
-   │
- 3 │     return ? ⇜ p⁻
-   │
-   █ [E006] Could not solve:
-              fib P ?0 = fib P p⁺
+    🭁 ./hole/morph2.poly
+    │
+  3 │     return ? ⇜ p⁻
+    ┷
+ [E006] Could not solve:
+          fib P ?0 = fib P p⁺
 --------------------[./hole/morph3.poly]--------------------
 
 Encountered hole with known type!
@@ -152,12 +149,11 @@ baz : ℕ
 
 --------------------[./std-lib/Data/Records.poly]--------------------
 
-
-   🭁 ./std-lib/Data/Records.poly
-   │
- 3 │ def MyRecordTy := { .foo : ℕ, .bar : Unit, .baz : ℕ → Unit }
-   │
-   █ [E004] Variable is not bound (or is negative, idk).
+    🭁 ./std-lib/Data/Records.poly
+    │
+  3 │ def MyRecordTy := { .foo : ℕ, .bar : Unit, .baz : ℕ → Unit }
+    ┷
+ [E004] Variable is not bound (or is negative, idk).
 --------------------[./std-lib/Data/Unit.poly]--------------------
 
 --------------------[./std-lib/Data/Void.poly]--------------------