basic lexer and parser

9 files changed, 199 insertions, 29 deletions

diff --git a/bin/main.ml b/bin/main.ml
index 732b852..1607ec4 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -1 +1,14 @@
-let () = print_ndline "Hello, World!"
+open Toytt
+
+let parse (s : string) : Ast.expr =
+  let lexbuf = Lexing.from_string s in
+  let ast = Parser.parse Lexer.lex lexbuf in
+  ast
+
+let rec repl () =
+  let input = read_line () in
+  let ast = parse input in
+  Format.printf "%a\n%!" Ast.dump_expr ast;
+  repl ()
+
+let () = repl ()
diff --git a/dune-project b/dune-project
index c3564ad..ede6aa8 100644
--- a/dune-project
+++ b/dune-project
@@ -1,7 +1,7 @@
-(lang dune 3.7)
+(lang dune 3.13)
 (generate_opam_files true)
 
-(using menhir 2.1)
+(using menhir 3.0)
 
 (name toytt)
 (source
@@ -15,7 +15,7 @@
  (name toytt)
  (synopsis "A short synopsis")
  (description "A longer description")
- (depends ocaml dune asai)
+ (depends ocaml dune ppx_deriving asai)
  (tags
   (topics "to describe" your project)))
 
diff --git a/flake.lock b/flake.lock
index 1475898..7816aa0 100644
--- a/flake.lock
+++ b/flake.lock
@@ -67,15 +67,15 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1682362401,
-        "narHash": "sha256-/UMUHtF2CyYNl4b60Z2y4wwTTdIWGKhj9H301EDcT9M=",
-        "owner": "nixos",
+        "lastModified": 1707689078,
+        "narHash": "sha256-UUGmRa84ZJHpGZ1WZEBEUOzaPOWG8LZ0yPg1pdDF/yM=",
+        "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "884ac294018409e0d1adc0cae185439a44bd6b0b",
+        "rev": "f9d39fb9aff0efee4a3d5f4a6d7c17701d38a1d8",
         "type": "github"
       },
       "original": {
-        "owner": "nixos",
+        "owner": "NixOS",
         "ref": "nixos-unstable",
         "repo": "nixpkgs",
         "type": "github"
@@ -86,7 +86,9 @@
         "flake-compat": "flake-compat",
         "flake-utils": "flake-utils_2",
         "mirage-opam-overlays": "mirage-opam-overlays",
-        "nixpkgs": "nixpkgs",
+        "nixpkgs": [
+          "nixpkgs"
+        ],
         "opam-overlays": "opam-overlays",
         "opam-repository": [
           "opam-repository"
@@ -163,10 +165,7 @@
     "root": {
       "inputs": {
         "flake-utils": "flake-utils",
-        "nixpkgs": [
-          "opam-nix",
-          "nixpkgs"
-        ],
+        "nixpkgs": "nixpkgs",
         "opam-nix": "opam-nix",
         "opam-repository": "opam-repository"
       }
diff --git a/flake.nix b/flake.nix
index fa15c13..6be9e8b 100644
--- a/flake.nix
+++ b/flake.nix
@@ -1,13 +1,18 @@
 {
   inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
     opam-repository = {
       url = "github:ocaml/opam-repository";
       flake = false;
     };
-    opam-nix.url = "github:tweag/opam-nix";
-    opam-nix.inputs.opam-repository.follows = "opam-repository";
+    opam-nix = {
+      url = "github:tweag/opam-nix";
+      inputs = {
+        nixpkgs.follows = "nixpkgs";
+        opam-repository.follows = "opam-repository";
+      };
+    };
     flake-utils.url = "github:numtide/flake-utils";
-    nixpkgs.follows = "opam-nix/nixpkgs";
   };
 
   outputs = { flake-utils, opam-nix, nixpkgs, ... }:
diff --git a/lib/Ast.ml b/lib/Ast.ml
index 4ca7899..002dfff 100644
--- a/lib/Ast.ml
+++ b/lib/Ast.ml
@@ -1,8 +1,62 @@
-type expr' =
-  | Var of string
-| Bool
-| True
-| False
-| BoolElim of string
-
-type expr = expr' Asai.Range.located
\ No newline at end of file
+type raw_ident = string
+type ident = raw_ident Asai.Range.located
+
+type raw_arg = { name : ident; ty : expr }
+and arg = raw_arg Asai.Range.located
+
+and raw_expr =
+  | Var of raw_ident
+  | Bool
+  | True
+  | False
+  | BoolElim of {
+      motive_var : ident;
+      motive_body : expr;
+      true_case : expr;
+      false_case : expr;
+      scrut : expr;
+    }
+  | Pi of arg * expr
+  | Lam of ident * expr
+  | App of expr * expr
+  | Sg of arg * expr
+  | Pair of expr * expr
+  | Fst of expr
+  | Snd of expr
+
+and expr = raw_expr Asai.Range.located
+
+let dump_raw_ident fmt (id : raw_ident) = Format.fprintf fmt "@[%s@]" id
+let dump_ident fmt ({ value; _ } : ident) = dump_raw_ident fmt value
+
+let rec dump_raw_arg fmt ({ name; ty } : raw_arg) =
+  Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_ident name dump_expr ty
+
+and dump_arg fmt ({ value; _ } : arg) = dump_raw_arg fmt value
+
+and dump_raw_expr fmt = function
+  | Var id -> Format.fprintf fmt "Var @[%a@]" dump_raw_ident id
+  | Bool -> Format.pp_print_string fmt "Bool"
+  | True -> Format.pp_print_string fmt "True"
+  | False -> Format.pp_print_string fmt "False"
+  | BoolElim { motive_var; motive_body; true_case; false_case; scrut } ->
+      Format.fprintf fmt
+        "@[<10>BoolElim (@[%a@] ->@ @[%a@],@ @[%a@],@ @[%a@],@ @[%a@])@]" dump_ident
+        motive_var dump_expr motive_body dump_expr true_case dump_expr
+        false_case dump_expr scrut
+  | Pi (dom, cod) ->
+      Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" dump_arg dom dump_expr cod
+  | Lam (var, body) ->
+      Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" dump_ident var dump_expr
+        body
+  | App (fn, arg) ->
+      Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" dump_expr fn dump_expr arg
+  | Sg (fst, snd) ->
+      Format.fprintf fmt "@[<4>Sg (@[%a@],@ @[%a@])@]" dump_arg fst dump_expr snd
+  | Pair (fst, snd) ->
+      Format.fprintf fmt "@[<6>Pair (@[%a@],@ @[%a@])@]" dump_expr fst dump_expr
+        snd
+  | Fst p -> Format.fprintf fmt "@[<5>Fst (@[%a@])@]" dump_expr p
+  | Snd p -> Format.fprintf fmt "@[<5>Snd (@[%a@])@]" dump_expr p
+
+and dump_expr fmt ({ value; _ } : expr) = dump_raw_expr fmt value
diff --git a/lib/Lexer.mll b/lib/Lexer.mll
new file mode 100644
index 0000000..55a22c2
--- /dev/null
+++ b/lib/Lexer.mll
@@ -0,0 +1,31 @@
+{
+open Parser
+}
+
+let whitespace = [' ' '\t' '\r' '\n']+
+let letter = ['a'-'z' 'A'-'Z']
+let ident = letter+
+
+rule lex =
+  parse
+  | whitespace { lex lexbuf }
+  | "(" { LPR }
+  | ")" { RPR }
+  | "[" { LBR }
+  | "]" { RBR }
+  | "->" { ARROW }
+  | "*" { ASTERISK }
+  | "\\" { BACKSLASH }
+  | ":" { COLON }
+  | "," { COMMA }
+  | "." { DOT }
+  | "=>" { FATARROW }
+  | "bool" { BOOL }
+  | "true" { TRUE }
+  | "false" { FALSE }
+  | "bool-elim" { BOOL_ELIM }
+  | "at" { AT }
+  | "fst" { FST }
+  | "snd" { SND }
+  | ident { IDENT (Lexing.lexeme lexbuf) }
+  | eof { EOF }
diff --git a/lib/Parser.mly b/lib/Parser.mly
new file mode 100644
index 0000000..db2a9e2
--- /dev/null
+++ b/lib/Parser.mly
@@ -0,0 +1,66 @@
+%{
+open Ast
+%}
+
+%token <string> IDENT
+%token LPR RPR
+%token LBR RBR
+%token ARROW ASTERISK BACKSLASH COLON COMMA DOT FATARROW
+%token BOOL TRUE FALSE BOOL_ELIM AT
+%token FST SND
+%token EOF
+
+%right ARROW ASTERISK
+%left IDENT LPR APP BACKSLASH FST SND BOOL TRUE FALSE BOOL_ELIM
+
+%start <Ast.expr> parse
+
+%%
+
+%inline
+locate(X): e = X { Asai.Range.locate_lex $loc e }
+
+%inline
+ident: id = locate(IDENT) { id }
+
+raw_arg: LPR; name = ident; COLON; ty = expr; RPR
+	{ { name; ty } }
+
+%inline
+arg: a = locate(raw_arg) { a }
+
+raw_expr:
+  | name = IDENT
+	{ Var name }
+  | LPR; e = raw_expr; RPR
+	{ e }
+  | BOOL
+	{ Bool }
+  | TRUE
+	{ True }
+  | FALSE
+	{ False }
+  | BOOL_ELIM; scrut = expr; AT; motive_var = ident; ARROW; motive_body = expr;
+	LBR; TRUE; FATARROW; true_case = expr; COMMA; FALSE; FATARROW; false_case = expr; RBR
+	{ BoolElim { motive_var; motive_body; true_case; false_case; scrut } }
+
+  | a = arg; ARROW; b = expr
+	{ Pi (a, b) }
+  | BACKSLASH; a = ident; ARROW; b = expr
+	{ Lam (a, b) }
+  | a = expr; b = expr %prec APP
+	{ App (a, b) }
+
+  | a = arg; ASTERISK; b = expr
+	{ Sg (a, b) }
+  | LPR; a = expr; COMMA; b = expr; RPR
+	{ Pair (a, b) }
+  | FST; p = expr
+	{ Fst p }
+  | SND; p = expr
+	{ Snd p }
+
+%inline
+expr: e = locate(raw_expr) { e }
+
+parse: e = expr; EOF { e }
diff --git a/lib/dune b/lib/dune
index a844074..7a54f53 100644
--- a/lib/dune
+++ b/lib/dune
@@ -1,9 +1,10 @@
 (menhir
- (flags --explain)
+ (explain true)
  (modules Parser))
 
-; (ocamllex Lexer)
+(ocamllex Lexer)
 
 (library
  (name toytt)
- (libraries asai))
+ (libraries asai)
+ (preprocess (pps ppx_deriving.std)))
diff --git a/toytt.opam b/toytt.opam
index c126fcb..1a4a45c 100644
--- a/toytt.opam
+++ b/toytt.opam
@@ -11,7 +11,8 @@ doc: "https://url/to/documentation"
 bug-reports: "https://github.com/username/reponame/issues"
 depends: [
   "ocaml"
-  "dune" {>= "3.7"}
+  "dune" {>= "3.13"}
+  "ppx_deriving"
   "asai"
   "odoc" {with-doc}
 ]