From 3fa11fb6edf7bcc3c4b77e7859da60750bcb11a6 Mon Sep 17 00:00:00 2001 From: favonia Date: Sat, 23 Sep 2023 15:12:58 -0500 Subject: [PATCH] docs: add an example showing how to use a library using asai --- examples/adopt/app/App.ml | 10 ++ examples/adopt/app/Logger.ml | 19 ++++ examples/adopt/app/dune | 6 ++ examples/adopt/syslib/Logger.ml | 16 +++ examples/adopt/syslib/Operations.ml | 9 ++ examples/adopt/syslib/Syslib.ml | 2 + examples/adopt/syslib/dune | 5 + examples/stlc/{STLC.ml => Checker.ml} | 0 examples/stlc/Stlc.ml | 145 ++++++++++++++++++++++++++ examples/stlc/dune | 4 +- 10 files changed, 214 insertions(+), 2 deletions(-) create mode 100644 examples/adopt/app/App.ml create mode 100644 examples/adopt/app/Logger.ml create mode 100644 examples/adopt/app/dune create mode 100644 examples/adopt/syslib/Logger.ml create mode 100644 examples/adopt/syslib/Operations.ml create mode 100644 examples/adopt/syslib/Syslib.ml create mode 100644 examples/adopt/syslib/dune rename examples/stlc/{STLC.ml => Checker.ml} (100%) create mode 100644 examples/stlc/Stlc.ml diff --git a/examples/adopt/app/App.ml b/examples/adopt/app/App.ml new file mode 100644 index 0000000..782fdc4 --- /dev/null +++ b/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" diff --git a/examples/adopt/app/Logger.ml b/examples/adopt/app/Logger.ml new file mode 100644 index 0000000..7ead073 --- /dev/null +++ b/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 diff --git a/examples/adopt/app/dune b/examples/adopt/app/dune new file mode 100644 index 0000000..edc49e7 --- /dev/null +++ b/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)) diff --git a/examples/adopt/syslib/Logger.ml b/examples/adopt/syslib/Logger.ml new file mode 100644 index 0000000..18322d5 --- /dev/null +++ b/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) diff --git a/examples/adopt/syslib/Operations.ml b/examples/adopt/syslib/Operations.ml new file mode 100644 index 0000000..ca814f3 --- /dev/null +++ b/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) diff --git a/examples/adopt/syslib/Syslib.ml b/examples/adopt/syslib/Syslib.ml new file mode 100644 index 0000000..9463bc2 --- /dev/null +++ b/examples/adopt/syslib/Syslib.ml @@ -0,0 +1,2 @@ +module Logger = Logger +module Operations = Operations diff --git a/examples/adopt/syslib/dune b/examples/adopt/syslib/dune new file mode 100644 index 0000000..d17c3ae --- /dev/null +++ b/examples/adopt/syslib/dune @@ -0,0 +1,5 @@ +(library + (name Syslib) + (public_name asai-examples.syslib) + (libraries algaeff asai) + (optional)) diff --git a/examples/stlc/STLC.ml b/examples/stlc/Checker.ml similarity index 100% rename from examples/stlc/STLC.ml rename to examples/stlc/Checker.ml diff --git a/examples/stlc/Stlc.ml b/examples/stlc/Stlc.ml new file mode 100644 index 0000000..da49167 --- /dev/null +++ b/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 diff --git a/examples/stlc/dune b/examples/stlc/dune index f5e9391..b033cfd 100644 --- a/examples/stlc/dune +++ b/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))