From 06d52c8ba30b1bd6e1174ebffbd6cc5ba668ecc2 Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Fri, 16 Feb 2024 00:43:04 +0100 Subject: basic lexer and parser --- bin/main.ml | 15 ++++++++++++- dune-project | 6 ++--- flake.lock | 19 ++++++++-------- flake.nix | 11 ++++++--- lib/Ast.ml | 70 +++++++++++++++++++++++++++++++++++++++++++++++++++------- lib/Lexer.mll | 31 ++++++++++++++++++++++++++ lib/Parser.mly | 66 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/dune | 7 +++--- toytt.opam | 3 ++- 9 files changed, 199 insertions(+), 29 deletions(-) create mode 100644 lib/Lexer.mll create mode 100644 lib/Parser.mly 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 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 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} ] -- cgit 1.4.1