docs: add an example showing how to use a library using asai (#60)

examples/adopt/app/App.ml

@@ -0,0 +1,10 @@
+let lift_syslib f =
+  Logger.adopt (Asai.Diagnostic.map (fun c -> Logger.Code.Syslib c)) Syslib.Logger.run f
+
+module Term = Asai.Tty.Make (Logger.Code)
+
+let () =
+  Logger.run ~emit:Term.interactive_trace ~fatal:Term.display @@ fun () ->
+  (lift_syslib @@ fun () -> Syslib.Operations.operation1 "op1");
+  (lift_syslib @@ fun () -> Syslib.Operations.operation2 "op2");
+  lift_syslib @@ fun () -> Syslib.Operations.operation3 "op3"

examples/adopt/app/Logger.ml

@@ -0,0 +1,19 @@
+module Code =
+struct
+  type t =
+    | Syslib of Syslib.Logger.Code.t
+    | UserError
+
+  let default_severity : t -> Asai.Diagnostic.severity =
+    function
+    | _ -> Warning
+
+  let to_string : t -> string = function
+    | Syslib c -> Syslib.Logger.Code.to_string c
+    | UserError -> "A000"
+end
+
+include Asai.Logger.Make(Code)
+
+let embed_syslib d = Asai.Diagnostic.map (fun c -> Code.Syslib c) d
+let lift_syslib f = adopt embed_syslib Syslib.Logger.run f

examples/adopt/app/dune

@@ -0,0 +1,6 @@
+(executable
+ (name App)
+ (package asai-examples)
+ (public_name asai-examples.app)
+ (libraries algaeff asai asai-examples.syslib)
+ (optional))

examples/adopt/syslib/Logger.ml

@@ -0,0 +1,16 @@
+module Code =
+struct
+  type t = FileError | ChiError | EmojiError
+
+  let default_severity : t -> Asai.Diagnostic.severity =
+    function
+    | _ -> Error
+
+  let to_string =
+    function
+    | FileError -> "C000"
+    | ChiError -> "C001"
+    | EmojiError -> "C002"
+end
+
+include Asai.Logger.Make(Code)

examples/adopt/syslib/Operations.ml

@@ -0,0 +1,9 @@
+let operation1 arg =
+  Logger.emitf ChiError "I got a string %s" arg
+
+let operation2 arg =
+  Logger.trace_string "Meow!\nMeow!" @@ fun () ->
+  operation1 arg
+
+let operation3 arg =
+  Logger.fatalf EmojiError "Not enough emojis in the string %s" (String.escaped arg)

examples/adopt/syslib/Syslib.ml

@@ -0,0 +1,2 @@
+module Logger = Logger
+module Operations = Operations

examples/adopt/syslib/dune

@@ -0,0 +1,5 @@
+(library
+ (name Syslib)
+ (public_name asai-examples.syslib)
+ (libraries algaeff asai)
+ (optional))

examples/stlc/Stlc.ml

@@ -0,0 +1,145 @@
+open Asai
+open Bwd
+
+open Syntax
+
+module Terminal = Asai.Tty.Make(ErrorCode)
+module Logger = Asai.Logger.Make(ErrorCode)
+module Server = Asai.Lsp.Make(ErrorCode)
+
+module Elab =
+struct
+  type env = (string * tp) bwd
+  module Reader = Algaeff.Reader.Make (struct type nonrec env = env end)
+
+  let bind_var nm tp k =
+    Reader.scope (fun env -> Snoc(env, (nm, tp))) k
+
+  let lookup ?loc nm =
+    let ctx = Reader.read () in
+    match Bwd.find_opt (fun (nm', _) -> String.equal nm nm') ctx with
+    | Some (_, tp) -> tp
+    | None ->
+      Logger.fatalf ?loc `UnboundVariable "Variable '%s' is not in scope" nm
+
+  let expected_connective ?loc conn tp =
+    Logger.fatalf ?loc `TypeError "Expected a %s, but got %a." conn pp_tp tp
+
+  let rec equate ?loc expected actual =
+    Logger.tracef ?loc "When equating terms" @@ fun () ->
+    match expected, actual with
+    | Fun (a0, b0), Fun (a1, b1) ->
+      equate a0 a1;
+      equate b0 b1
+    | Tuple (a0, b0), Tuple (a1, b1) ->
+      equate a0 a1;
+      equate b0 b1
+    | Nat, Nat ->
+      ()
+    | _, _ ->
+      Logger.fatalf ?loc `TypeError "Expected type %a, but got %a." pp_tp expected pp_tp actual
+
+  let rec chk (tm : tm) (tp : tp) : unit =
+    Logger.tracef ?loc:tm.loc "When checking against %a" Syntax.pp_tp tp @@ fun () ->
+    match tm.value, tp with
+    | Lam (nm, body), Fun (a, b) ->
+      bind_var nm a @@ fun () ->
+      chk body b
+    | Lam (_, _), _ ->
+      expected_connective ?loc:tm.loc "function type" tp
+    | Pair (l, r), Tuple (a, b) ->
+      chk l a;
+      chk r b;
+    | Pair (_, _), _ ->
+      expected_connective ?loc:tm.loc "pair type" tp
+    | Lit _, Nat ->
+      ()
+    | Lit _, _ ->
+      expected_connective ?loc:tm.loc "ℕ" tp
+    | Suc n, Nat ->
+      chk n Nat
+    | Suc _, _ ->
+      expected_connective ?loc:tm.loc "ℕ" tp
+    | _ ->
+      let actual_tp = syn tm in
+      equate ?loc:tm.loc tp actual_tp
+
+  and syn (tm : tm) : tp =
+    Logger.tracef ?loc:tm.loc "When synthesizing" @@ fun () ->
+    match tm.value with
+    | Var nm ->
+      lookup ?loc:tm.loc nm
+    | Ap (fn, arg) ->
+      begin
+        match syn fn with
+        | Fun (a, b) ->
+          chk arg a;
+          b
+        | tp ->
+          expected_connective ?loc:tm.loc "function type" tp
+      end
+    | Fst tm ->
+      begin
+        match syn tm with
+        | Tuple (l, _) ->
+          l
+        | tp ->
+          expected_connective ?loc:tm.loc "pair type" tp
+      end
+    | Snd tm ->
+      begin
+        match syn tm with
+        | Tuple (_, r) ->
+          r
+        | tp ->
+          expected_connective ?loc:tm.loc "pair type" tp
+      end
+    | NatRec (z, s, scrut) ->
+      begin
+        let mot = syn z in
+        chk s (Fun (mot, mot));
+        chk scrut Nat;
+        mot
+      end
+    | _ ->
+      Logger.fatalf ?loc:tm.loc `TypeError "Unable to infer type"
+end
+
+module Driver =
+struct
+  let load_file filepath =
+    let lexbuf = Lexing.from_channel (open_in filepath) in
+    lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = filepath };
+    let (tm, tp) =
+      try Grammar.defn Lex.token lexbuf with
+      | Lex.SyntaxError tok ->
+        Logger.fatalf ~loc:(Span.of_lex lexbuf) `LexingError {|Unrecognized token "%s"|} (String.escaped tok)
+      | Grammar.Error ->
+        Logger.fatalf ~loc:(Span.of_lex lexbuf) `LexingError "Failed to parse"
+    in
+    Elab.Reader.run ~env:Emp @@ fun () ->
+    Elab.chk tm tp
+
+  let load mode filepath =
+    let display =
+      match mode with
+      | `Debug -> Terminal.display ~show_backtrace:true
+      | `Normal ->  Terminal.display ~show_backtrace:false
+      | `Interactive -> Terminal.interactive_trace
+    in
+    Logger.run ~emit:display ~fatal:display @@ fun () ->
+    load_file filepath
+
+  let server () =
+    Server.start
+      ~source:(Some "STLC")
+      ~init:(fun ~root:_ -> ())
+      ~load_file:(fun ~display:push file -> Logger.run ~emit:push ~fatal:push @@ fun () -> load_file file)
+end
+
+let () =
+  match Sys.argv.(1) with
+  | "--server" -> Driver.server ()
+  | "--debug" -> Driver.load `Debug Sys.argv.(2)
+  | "--interactive" -> Driver.load `Interactive Sys.argv.(2)
+  | filepath -> Driver.load `Normal filepath

examples/stlc/dune

@@ -1,7 +1,7 @@
 (executable
+ (name Checker)
  (package asai-examples)
- (name STLC)
- (public_name asai_stlc)
+ (public_name asai-examples.stlc)
  (libraries algaeff menhirLib asai)
  (optional))