From 81a63e67949dfb07b8626ca1d7d35b0154d338d2 Mon Sep 17 00:00:00 2001 From: matt rice Date: Mon, 6 Apr 2020 20:16:01 -0700 Subject: [PATCH 1/3] testing out with changes to logos 0.11-rc2. --- Cargo.toml | 3 +- src/codespan.rs | 2 +- src/error.rs | 4 +- src/lex.rs | 25 ++++-------- src/main.rs | 15 +++++-- src/prop.lalrpop | 13 +++++-- src/test.rs | 17 ++++++-- src/test_util.rs | 18 +++++---- src/token_wrap.rs | 99 ----------------------------------------------- 9 files changed, 57 insertions(+), 139 deletions(-) delete mode 100644 src/token_wrap.rs diff --git a/Cargo.toml b/Cargo.toml index f8bea9f..db30c1e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,8 +9,9 @@ edition = "2018" [dependencies] lalrpop = "0.18" lalrpop-util = "0.18" -logos = "0.10.0" +logos = "0.11.0-rc2" regex = "1" +logos-derive = "0.11.0-rc2" codespan-reporting = "0.9" structopt = "0.3.12" diff --git a/src/codespan.rs b/src/codespan.rs index fb8aacc..d296aab 100644 --- a/src/codespan.rs +++ b/src/codespan.rs @@ -51,7 +51,7 @@ pub fn codespan<'a>( .with_message("Extra token"), User { error } => Diagnostic::error() .with_message("Invalid token") - .with_labels(vec![Label::primary(file_id, error.0.clone())]) + .with_labels(vec![Label::primary(file_id, *error..*error)]) .with_message("Invalid token"), }; diff --git a/src/error.rs b/src/error.rs index c527819..1520722 100644 --- a/src/error.rs +++ b/src/error.rs @@ -1,6 +1,6 @@ -use crate::token_wrap::*; +use crate::lex::Token; -pub type Error<'a> = lalrpop_util::ParseError, LexicalError>; +pub type Error<'a> = lalrpop_util::ParseError, usize>; #[derive(Debug)] pub enum MainError { diff --git a/src/lex.rs b/src/lex.rs index 8e16ea3..b4ad155 100644 --- a/src/lex.rs +++ b/src/lex.rs @@ -1,12 +1,9 @@ +pub use logos::Lexer; use logos::Logos; -// Notably absent from the above, present in the below are -// Whitespace, EOF, LexError -#[derive(Logos, Debug)] -pub enum Token { - #[end] - EOF, - +#[derive(Logos, Debug, Clone, PartialEq)] +#[logos(trivia = r"(\p{Whitespace}+|#.*\n)")] +pub enum Token<'a> { #[token = "."] Dot, @@ -87,10 +84,10 @@ pub enum Token { // \x{1d62}-\x{1d6a} // // FancyNameAscii ↔ FancyNameUnicode - #[regex = r"[\\][a-zA-Z][_a-zA-Z0-9]*"] - FancyNameAscii, - #[regex = r"[a-zA-Z\p{Greek}\x{1d49c}-\x{1d59f}\x{2100}-\x{214f}][_a-zA-Z0-9\x{207f}-\x{2089}\x{2090}-\x{209c}\x{1d62}-\x{1d6a}]*"] - Name, + #[regex(r"[\\][a-zA-Z][_a-zA-Z0-9]*", |lex| lex.slice())] + FancyNameAscii(&'a str), + #[regex(r"[a-zA-Z\p{Greek}\x{1d49c}-\x{1d59f}\x{2100}-\x{214f}][_a-zA-Z0-9\x{207f}-\x{2089}\x{2090}-\x{209c}\x{1d62}-\x{1d6a}]*", |lex| lex.slice())] + Name(&'a str), #[token = ":"] Colon, @@ -98,12 +95,6 @@ pub enum Token { #[token = ";"] Semi, - #[regex = r"#.*\n"] - Comment, - - #[regex = r"\p{Whitespace}+"] - Whitespace, - #[error] LexError, } diff --git a/src/main.rs b/src/main.rs index 801e093..67c2072 100644 --- a/src/main.rs +++ b/src/main.rs @@ -2,7 +2,6 @@ mod ast; mod codespan; mod error; mod lex; -mod token_wrap; #[cfg(test)] mod test; @@ -12,9 +11,10 @@ mod test_util; use codespan_reporting::term::termcolor::StandardStream; use codespan_reporting::term::{self, ColorArg}; use error::*; +use logos::Logos; use std::io::Read; use structopt::StructOpt; -use token_wrap::*; + #[derive(Debug, StructOpt)] #[structopt(name = "prop")] pub struct Opts { @@ -59,8 +59,15 @@ fn main() -> Result<(), MainError> { // Not really how i'd like this to be. buf.read_to_string(&mut s)?; - let lexer = Tokens::from_string(&s); - let parse_result = parser::propParser::new().parse(lexer); + + let lex = lex::Token::lexer(&s).spanned(); + let parse_result = parser::propParser::new().parse(lex.map(|(t, r)| { + if t == lex::Token::LexError { + Err(r.start) + } else { + Ok((r.start, t, r.end)) + } + })); match parse_result { Err(e) => { diff --git a/src/prop.lalrpop b/src/prop.lalrpop index 8886d89..f9bea18 100644 --- a/src/prop.lalrpop +++ b/src/prop.lalrpop @@ -1,12 +1,11 @@ -use crate::token_wrap; +use crate::lex::Token; use crate::ast::{Prop, Expr, Binding, Typ}; use std::rc::Rc; -use token_wrap::*; grammar<'a>; extern { type Location = usize; - type Error = LexicalError; + type Error = usize; enum Token<'a> { "⊥" => Token::Bot, @@ -23,10 +22,16 @@ extern { ")" => Token::RParen, ":" => Token::Colon, ";" => Token::Semi, - name => Token::Name(<&'a str>), + fancy_name_unicode => Token::Name(<&'a str>), + fancy_name_ascii => Token::FancyNameAscii(<&'a str>), } } +name: &'a str = { + fancy_name_unicode, + fancy_name_ascii, +} + pub prop = Semi; Binding: Rc = { diff --git a/src/test.rs b/src/test.rs index 406aff9..6b74620 100644 --- a/src/test.rs +++ b/src/test.rs @@ -1,6 +1,7 @@ use crate::error::*; -use crate::token_wrap::*; +use crate::lex; use crate::{parser, test_util}; +use logos::Logos; use unindent::unindent; @@ -108,8 +109,16 @@ fn bad_ascii() -> Result<(), &'static str> { let mut num_fail = 0; for s in invalid_source.iter() { - let lexer = Tokens::from_string(&s); - match parser::propParser::new().parse(lexer) { + let lex = lex::Token::lexer(&s).spanned(); + let parse_result = parser::propParser::new().parse(lex.map(|(t, r)| { + if t == lex::Token::LexError { + Err(r.start) + } else { + Ok((r.start, t, r.end)) + } + })); + + match parse_result { Ok(_) => { // bad println!("parsed but shouldn't: {}", s); @@ -117,7 +126,7 @@ fn bad_ascii() -> Result<(), &'static str> { } Err(e) => { // good - println!("expected error: {}", e); + println!("expected error: {:?}", e); () } } diff --git a/src/test_util.rs b/src/test_util.rs index 9594d75..fd7101a 100644 --- a/src/test_util.rs +++ b/src/test_util.rs @@ -1,19 +1,25 @@ use crate::codespan; use crate::error::*; +use crate::lex; use crate::parser; -use crate::token_wrap::*; use codespan_reporting::term; use codespan_reporting::term::termcolor::{ColorChoice, StandardStream}; +use logos::Logos; pub fn do_test<'a>(sources: &[&'a str]) -> Result<(), Vec<(&'a str, Error<'a>)>> { let (_pass, fail): (Vec<_>, Vec<_>) = sources .iter() .enumerate() .map(|(index, s)| { - ( - index, - parser::propParser::new().parse(Tokens::from_string(s)), - ) + (index, { + parser::propParser::new().parse(lex::Token::lexer(&s).spanned().map(|(t, r)| { + if t == lex::Token::LexError { + Err(r.start) + } else { + Ok((r.start, t, r.end)) + } + })) + }) }) .partition(|(_, r)| r.is_ok()); if fail.is_empty() { @@ -39,8 +45,6 @@ pub fn expect_success<'a>(result: Result<(), Vec<(&'a str, Error<'a>)>>) -> Resu let config = codespan_reporting::term::Config::default(); let (files, diagnostic) = codespan::codespan("foo", source, error); - eprintln!("capture stderr?"); - println!("capture stdout?"); term::emit(&mut writer.lock(), &config, &files, &diagnostic)?; } Err(MainError::SomethingWentAwryAndStuffWasPrinted) diff --git a/src/token_wrap.rs b/src/token_wrap.rs deleted file mode 100644 index 87d2f6a..0000000 --- a/src/token_wrap.rs +++ /dev/null @@ -1,99 +0,0 @@ -use crate::lex; -use logos::Logos; -use std::ops::Range; - -#[derive(Debug, Clone)] -pub enum Token<'a> { - Dot, - Semi, - Colon, - LParen, - RParen, - Bot, - Top, - Disj, - Conj, - Abs, - Neg, - Iff, - Arrow, - Def, - Name(&'a str), -} - -impl<'a> std::fmt::Display for Token<'a> { - #[rustfmt::skip] - fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { - match self { - Token::Dot => write!(f, "."), - Token::Abs => write!(f, "ⲗ"), - Token::Bot => write!(f, "⊥"), - Token::Def => write!(f, "≔"), - Token::Iff => write!(f, "↔"), - Token::Neg => write!(f, "¬"), - Token::Top => write!(f, "⊤"), - Token::Conj => write!(f, "∧"), - Token::Disj => write!(f, "∨"), - Token::Semi => write!(f, ";"), - Token::Arrow => write!(f, "→"), - Token::Colon => write!(f, ":"), - Token::LParen => write!(f, "("), - Token::RParen => write!(f, ")"), - Token::Name(s) => write!(f, "{}", s), - } - } -} - -#[derive(Debug)] -pub struct LexicalError(pub Range); - -impl std::fmt::Display for LexicalError { - fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { - write!(f, "lexical error at {:?}", self.0) - } -} - -pub struct Tokens<'a>(logos::Lexer); -pub type Spanned = Result<(Loc, Tok, Loc), Error>; - -impl<'a> Tokens<'a> { - pub fn from_string(source: &'a str) -> Tokens<'a> { - Tokens(lex::Token::lexer(source)) - } -} - -impl<'a> Iterator for Tokens<'a> { - type Item = Spanned, usize, LexicalError>; - - fn next(&mut self) -> Option { - let lex = &mut self.0; - let range = lex.range(); - let ok = |tok: Token<'a>| Ok((range.start, tok, range.end)); - let token = loop { - match &lex.token { - lex::Token::Whitespace | lex::Token::Comment => lex.advance(), - lex::Token::EOF => return None, - lex::Token::LexError => break Err(LexicalError(range)), - lex::Token::Name => break ok(Token::Name(lex.slice())), - lex::Token::FancyNameAscii => break ok(Token::Name(lex.slice())), - // And the rest are all unary members - lex::Token::Dot => break ok(Token::Dot), - lex::Token::Abs => break ok(Token::Abs), - lex::Token::Bot => break ok(Token::Bot), - lex::Token::Top => break ok(Token::Top), - lex::Token::Neg => break ok(Token::Neg), - lex::Token::Iff => break ok(Token::Iff), - lex::Token::Def => break ok(Token::Def), - lex::Token::Disj => break ok(Token::Disj), - lex::Token::Conj => break ok(Token::Conj), - lex::Token::Semi => break ok(Token::Semi), - lex::Token::Arrow => break ok(Token::Arrow), - lex::Token::Colon => break ok(Token::Colon), - lex::Token::LParen => break ok(Token::LParen), - lex::Token::RParen => break ok(Token::RParen), - } - }; - lex.advance(); - Some(token) - } -} From 70cd7606935115051f37e936402413455f81693b Mon Sep 17 00:00:00 2001 From: matt rice Date: Sun, 29 Mar 2020 20:06:43 -0700 Subject: [PATCH 2/3] chowder parser experiment 1. --- docs/Makefile | 7 ++ docs/chowder.ebnf | 22 ++++ docs/inference_rules.tex | 247 +++++++++++++++++++++++++++++++++++++++ src/ast.rs | 74 ------------ src/lex.rs | 58 +++++++++ src/main.rs | 3 +- src/prop.lalrpop | 74 ++++++------ src/test.rs | 56 +++++++++ 8 files changed, 432 insertions(+), 109 deletions(-) create mode 100644 docs/Makefile create mode 100644 docs/chowder.ebnf create mode 100644 docs/inference_rules.tex delete mode 100644 src/ast.rs diff --git a/docs/Makefile b/docs/Makefile new file mode 100644 index 0000000..d3c6c6b --- /dev/null +++ b/docs/Makefile @@ -0,0 +1,7 @@ +.PHONY: clean + +inference_rules.pdf: inference_rules.tex + xelatex inference_rules.tex + +clean: + rm -f *.aux *.pdf *.fdb_latexmk *.log *.fls diff --git a/docs/chowder.ebnf b/docs/chowder.ebnf new file mode 100644 index 0000000..a721bf4 --- /dev/null +++ b/docs/chowder.ebnf @@ -0,0 +1,22 @@ +Name ::= [a-zA-Z][a-zA-Z0-9]* +Bindings ::= (Binding ";") Binding? +Binding ::= Name (":" Prop)? "≔" Stmt +Stmt ::= Stmt "‣" Thus | Thus +Thus ::= Thus "∴" PropOpt | Thus "." PropOpt | PropOpt +PropOpt ::= +() +| Prop + +Prop ::= "¬" BinaryProp | BinaryProp +BinaryProp ::= +BinaryProp "∧" Atom +| BinaryProp "∨" Atom +| BinaryProp "→" Atom +| BinaryProp "↔" Atom +| BinaryProp "∧" "¬" Atom +| BinaryProp "∨" "¬" Atom +| BinaryProp "→" "¬" Atom +| BinaryProp "↔" "¬" Atom +| Atom + +Atom ::= "T" | "(" Prop ")" | Name diff --git a/docs/inference_rules.tex b/docs/inference_rules.tex new file mode 100644 index 0000000..2891271 --- /dev/null +++ b/docs/inference_rules.tex @@ -0,0 +1,247 @@ +\documentclass{article} +\usepackage{bussproofs} +\usepackage{amsfonts,amsmath,amssymb,amsthm} +\usepackage{amsmath} +\usepackage{marvosym} +\usepackage{unicode-math} +\usepackage[margin=0.5in]{geometry} +\usepackage{newunicodechar} +\usepackage{fancyvrb} +\AtBeginDocument{\setmainfont{XITS-Regular.otf}} +\AtBeginDocument{\setmathfont{XITSMath-Regular.otf}} +\AtBeginDocument{\newfontfamily{\mathfont}{FreeMono.otf}} + + +\AtBeginDocument{\newunicodechar{→} {\mathfont{→}}} +\AtBeginDocument{\newunicodechar{∀} {\ensuremath{\forall}}} +\AtBeginDocument{\newunicodechar{∃} {\ensuremath{\exists}}} +\AtBeginDocument{\newunicodechar{‣} {\mathfont{‣}}} +\AtBeginDocument{\newunicodechar{∴} {\mathfont{∴}}} +\AtBeginDocument{\newunicodechar{≔} {\mathfont{≔}}} +\AtBeginDocument{\newunicodechar{⋮} {\mathfont{⋮}}} +\AtBeginDocument{\newunicodechar{∧} {\mathfont{∧}}} +\AtBeginDocument{\newunicodechar{∨} {\mathfont{∨}}} +\AtBeginDocument{\newunicodechar{⚡} {\mbox{\Lightning}}} + +\title{"Chowder" proof checking inference rules augmented with proposed syntax} +\author{matt rice} + +\newenvironment{bprooftree0} + {\leavevmode\hbox\bgroup} + {\DisplayProof\egroup} +\newenvironment{bprooftree} + {\noindent\hbox\bgroup} + {\DisplayProof\egroup} + +\newcommand{\charge}[2]{% + \LeftLabel{$\smalltriangleright$} + \RightLabel{$^+\text{\Lightning}\alpha$} + \AxiomC{}% + \UnaryInfC{#1}% + \noLine% + \UnaryInfC{$\vdots$}% + \noLine% + \UnaryInfC{#2.}}% + +\newcommand{\discharge}[1]{% + \LeftLabel{$^-\text{\Lightning}\alpha$}% + \RightLabel{#1}% +}% + +\newcommand{\thus}[1]{% + $\therefore$ #1 +} +\newcommand{\biimpl}{\leftrightarrow} +\newcommand{\hsep}{\vspace{1em}\par} +\newcommand{\vsep}{\hspace{0.5em}% +%\vrule% +\hspace{0.5em}} + +\begin{document} + + \maketitle + + \section{Inference rules} + Natural deduction rules augmented with chowder syntax + \description + \item{$\smalltriangleright$} acts as n-ary case analysis. + \item{$\therefore$} acts like the natural deduction mid-line in syntax. + \par + \vspace{1em} + Conjunction: + \begin{bprooftree} + \AxiomC{A} + \AxiomC{B} + \RightLabel{\thus{$\wedge$I}} + \BinaryInfC{A $\wedge$ B} + \end{bprooftree} + \begin{bprooftree} + \AxiomC{A $\wedge$ B} + \RightLabel{\thus{$\wedge E_L$}} + \UnaryInfC{A} + \end{bprooftree} + \begin{bprooftree} + \AxiomC{A $\wedge$ B} + \RightLabel{\thus{$\wedge E_R$}} + \UnaryInfC{B} + \end{bprooftree} +\hsep + Disjunction: + \begin{bprooftree} + \AxiomC{A} + \LeftLabel{} + \RightLabel{\thus{$\vee I_L$}} + \UnaryInfC{A $\vee$ B} + \end{bprooftree} + \begin{bprooftree} + \AxiomC{B} + \RightLabel{\thus{$\vee I_R$}} + \UnaryInfC{ A $\vee$ B} + \end{bprooftree} + \begin{bprooftree} + \AxiomC{A $\vee$ B} + \charge{A}{C} + \charge{B}{C} + \discharge{\thus{$\vee E$}} + \TrinaryInfC{C} +\end{bprooftree} + +\hsep +Implication: + \begin{bprooftree} + \charge{A}{B} + \discharge{\thus{$\to$I}} + \UnaryInfC{A $\to$ B} + \end{bprooftree} + \begin{bprooftree} + \AxiomC{$\neg$A} + \AxiomC{A} + \RightLabel{\thus{$\neg$E}} + \BinaryInfC{$\bot$} + \end{bprooftree} +Negation: + \begin{bprooftree} + \charge{A}{$\bot$} + \discharge{\thus{$\neg$I}} + \UnaryInfC{$\neg$A} + \end{bprooftree} + \begin{bprooftree} + \AxiomC{A $\to$ B} + \AxiomC{A} + \RightLabel{\thus{$\to$E}} + \BinaryInfC{B} + \end{bprooftree} + +\hsep + +Top: + \begin{bprooftree} + \AxiomC{} + \RightLabel{$\top$I} + \UnaryInfC{$\top$} + \end{bprooftree} + +\hsep + +Bot: + \begin{bprooftree} + \AxiomC{$\bot$} + \RightLabel{\thus{$\bot$E}} + \UnaryInfC{A} + \end{bprooftree} +\hsep + +Bi-implication: + + \begin{bprooftree} + \charge{A}{B} + \charge{B}{A} + \discharge{\thus{$\leftrightarrow$I}} + \BinaryInfC{A $\biimpl$ B} + \end{bprooftree} + \begin{bprooftree} + \AxiomC{A $\biimpl$ B} + \AxiomC{A} + \RightLabel{\thus{$\biimpl{E_L}$}} + \BinaryInfC{B} + \end{bprooftree} + \begin{bprooftree} + \AxiomC{A $\biimpl$ B} + \AxiomC{B} + \RightLabel{\thus{$\biimpl{E_R}$}} + \BinaryInfC{A} + \end{bprooftree} +\section{EBNF} +\begin{Verbatim} +Name ::= [a-zA-Z][a-zA-Z0-9]* +Bindings ::= (Binding ";") Binding? +Binding ::= Name (":" Prop)? "≔" Stmt +Stmt ::= Stmt "‣" Thus | Thus +Thus ::= Thus "∴" PropOpt | Thus "." PropOpt | PropOpt +PropOpt ::= +() +| Prop + +Prop ::= "¬" BinaryProp | BinaryProp +BinaryProp ::= +BinaryProp "∧" Atom +| BinaryProp "∨" Atom +| BinaryProp "→" Atom +| BinaryProp "↔" Atom +| BinaryProp "∧" "¬" Atom +| BinaryProp "∨" "¬" Atom +| BinaryProp "→" "¬" Atom +| BinaryProp "↔" "¬" Atom +| Atom +Atom ::= "T" | "(" Prop ")" | Name +\end{Verbatim} + +\section{Some unchecked proofs that parse.} + +\begin{Verbatim} +ab_or_cd: (A ∧ B) ∨ (C ∧ D) → B ∨ D +≔ ‣ (A ∧ B) ∨ (C ∧ D) ;; +⚡1 + ‣ A ∧ B ;; +⚡2 + ∴ B ;; ∴ ∧E R + ∴ B ∨ D. ;; ∴ ∨I L + ‣ C ∧ D ;; +⚡2 + ∴ D ;; ∴ ∧E R + ∴ B ∨ D. ;; ∴ ∨I R + ∴ B ∨ D. ;; -⚡2 ∴ ∨E + ∴ (A ∧ B) ∨ (C ∧ D) → B ∨ D. ;; -⚡1 ∴ →I + ; +\end{Verbatim} + + +\begin{Verbatim} +iff_and_or: (A ∧ B) ∨ (C ∧ D) ↔ (B ∧ A) ∨ (D ∧ C) +≔ ‣‣(A ∧ B) ∨ (C ∧ D) ;; +⚡1, +⚡2 + ‣ A ∧ B ;; +⚡3 + ∴ B ;; ∴ ∧E R + ∴ A ;; ∴ ∧E L + ∴ B ∧ A ;; ∴ ∧I + ∴ (B ∧ A) ∨ (D ∧ C). ;; ∴ ∨I L + ‣ C ∧ D ;; +⚡3 + ∴ D ;; ∴ ∧E R + ∴ C ;; ∴ ∧E L + ∴ D ∧ C ;; ∴ ∧I + ∴ (B ∧ A) ∨ (D ∧ C). ;; ∴ ∨I L + ∴ (B ∧ A) ∨ (D ∧ C). ;; -3 ∴ ∨E + ∴ (A ∧ B) ∨ (C ∧ D) → (B ∧ A) ∨ (D ∧ C). ;; -2 ∴ →I + ‣‣ (B ∧ A) ∨ (D ∧ C) ;; +⚡1, +⚡2 + ‣ B ∧ A ;; +⚡3 + ∴ B ∧ A ∴ A ;; ∴ ∧E R + ∴ B ∧ A ∴ B ;; ??, ∴ ∧E L + ∴ A ∧ B ;; ∴ ∧I + ∴ (A ∧ B) ∨ (C ∧ D). ;; ∴ ∨I L + ‣ D ∧ C ;; +⚡3 + ∴ C ;; ∴ ∧E R + ∴ D ;; ??, ∴ ∧E L + ∴ C ∧ D ;; ∴ ∧I + ∴ (A ∧ B) ∨ (C ∧ D). ;; ∴ ∨I R + ∴ (A ∧ B) ∨ (C ∧ D). ;; -⚡3 ∴ ∨E + ∴ (B ∧ A) ∨ (D ∧ C) → (A ∧ B) ∨ (C ∧ D). ;; -⚡2 ∴ →I + ∴ (A ∧ B) ∨ (C ∧ D) ↔ (B ∧ A) ∨ (D ∧ C). ;; -⚡1 ∴ ↔I + ; +\end{Verbatim} +\end{document} diff --git a/src/ast.rs b/src/ast.rs deleted file mode 100644 index 7439e4c..0000000 --- a/src/ast.rs +++ /dev/null @@ -1,74 +0,0 @@ -use std::fmt; -use std::rc::Rc; - -#[derive(Debug)] -pub enum Prop { - True, - And(Rc, Rc), - Or(Rc, Rc), - Neg(Rc), - Imp(Rc, Rc), - Iff(Rc, Rc), - Var(String), -} - -#[derive(Debug)] -pub enum Binding { - Bind(String, Rc, Option), - Var(String, Option), -} - -#[derive(Debug)] -pub enum Typ { - Typ(Prop), -} - -#[derive(Debug)] -pub enum Expr { - Lambda(Rc, Rc, Option), - Prop(Rc), - App(Rc, Rc), -} - -impl fmt::Display for Typ { - fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { - match self { - Typ::Typ(prop) => write!(f, "Typ({})", prop), - } - } -} - -impl fmt::Display for Binding { - fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { - match self { - Binding::Bind(s, expr, typ) => write!(f, "Bind({} : {:?} ≔ {})", s, typ, expr), - Binding::Var(s, typ) => write!(f, "Var({}, {:?})", s, typ), - } - } -} - -impl fmt::Display for Expr { - fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { - match self { - Expr::App(e1, e2) => write!(f, "App({} {})", e1, e2), - Expr::Prop(p) => write!(f, "Prop({})", p), - Expr::Lambda(bind, expr, typ) => { - write!(f, "Lambda((ⲗ {}. {}) : {:?})", bind, expr, typ) - } - } - } -} - -impl fmt::Display for Prop { - fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { - match self { - Prop::Neg(p) => write!(f, "Neg({})", p), - Prop::True => write!(f, "⊤"), - Prop::Iff(p1, p2) => write!(f, "Iff({} ↔ {})", p1, p2), - Prop::And(p1, p2) => write!(f, "And({} ∧ {})", p1, p2), - Prop::Or(p1, p2) => write!(f, "Or({} ∨ {})", p1, p2), - Prop::Imp(p1, p2) => write!(f, "Imp({} → {})", p1, p2), - Prop::Var(s) => write!(f, "Var({})", s), - } - } -} diff --git a/src/lex.rs b/src/lex.rs index b4ad155..6ff2cc1 100644 --- a/src/lex.rs +++ b/src/lex.rs @@ -54,11 +54,38 @@ pub enum Token<'a> { #[token = "⊥"] Bot, + #[token = r"\qed"] + #[token = "□"] + QED, + + #[token = r"\thus"] + #[token = "∴"] + Thus, + + #[token = r"\case"] + Case, + + #[token = r"\match"] + #[token = "‣"] + CaseLeg, + + #[token = r"Prop"] + PropT, + #[token = "("] LParen, #[token = ")"] RParen, + #[token = "["] + LBrack, + #[token = "]"] + RBrack, + + // Name ↔ Name + #[regex = r"[a-zA-Z][_a-zA-Z0-9]*"] + Name, + // Since this uses Coptic letters for keywords all greek letters can be used as variable names. // Variables can start with a slash character, a greek/math alphanumeric symbol, // and ascii letters numbers, and subscripts (TODO superscripts) @@ -98,3 +125,34 @@ pub enum Token<'a> { #[error] LexError, } + +impl<'a> std::fmt::Display for Token<'a> { + #[rustfmt::skip] + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { + match self { + Token::Dot => write!(f, "."), + Token::Abs => write!(f, "ⲗ"), + Token::Bot => write!(f, "⊥"), + Token::Def => write!(f, "≔"), + Token::Iff => write!(f, "↔"), + Token::Neg => write!(f, "¬"), + Token::Top => write!(f, "⊤"), + Token::QED => write!(f, "□"), + Token::Conj => write!(f, "∧"), + Token::Disj => write!(f, "∨"), + Token::Semi => write!(f, ";"), + Token::Thus => write!(f, "∴"), + Token::CaseLeg => write!(f, "‣"), + Token::Case => write!(f, "case"), + Token::Arrow => write!(f, "→"), + Token::Comma => write!(f, ","), + Token::Colon => write!(f, ":"), + Token::PropT => write!(f, "Prop"), + Token::LParen => write!(f, "("), + Token::RParen => write!(f, ")"), + Token::LBrack => write!(f, "["), + Token::RBrack => write!(f, "]"), + Token::Name(s) => write!(f, "{}", s), + } + } +} diff --git a/src/main.rs b/src/main.rs index 67c2072..2bb87c4 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,4 +1,3 @@ -mod ast; mod codespan; mod error; mod lex; @@ -80,7 +79,7 @@ fn main() -> Result<(), MainError> { } Ok(exprs) => { for bind in exprs.iter() { - println!("{}", bind); + println!("{:?}", bind); } } } diff --git a/src/prop.lalrpop b/src/prop.lalrpop index f9bea18..63a76b7 100644 --- a/src/prop.lalrpop +++ b/src/prop.lalrpop @@ -1,6 +1,4 @@ use crate::lex::Token; -use crate::ast::{Prop, Expr, Binding, Typ}; -use std::rc::Rc; grammar<'a>; extern { @@ -8,20 +6,28 @@ extern { type Error = usize; enum Token<'a> { + "ⲗ" => Token::Abs, "⊥" => Token::Bot, "." => Token::Dot, "≔" => Token::Def, "→" => Token::Arrow, "↔" => Token::Iff, "¬" => Token::Neg, - "ⲗ" => Token::Abs, + "⊤" => Token::Top, "∧" => Token::Conj, "∨" => Token::Disj, - "⊤" => Token::Top, "(" => Token::LParen, ")" => Token::RParen, + "[" => Token::LBrack, + "]" => Token::RBrack, ":" => Token::Colon, + "," => Token::Comma, ";" => Token::Semi, + "∴" => Token::Thus, + "‣" => Token::CaseLeg, + "□" => Token::QED, + "Prop" => Token::PropT, + "case" => Token::Case, fancy_name_unicode => Token::Name(<&'a str>), fancy_name_ascii => Token::FancyNameAscii(<&'a str>), } @@ -34,14 +40,19 @@ name: &'a str = { pub prop = Semi; -Binding: Rc = { - ":" "≔" => Rc::new(Binding::Bind(n.to_string(), Rc::new(e), Some(t))), - "≔" => Rc::new(Binding::Bind(n.to_string(), Rc::new(e), None)), +Binding: () = { + "≔" => (), + ":" "≔" => (), +} +Stmt: () = { + "‣" => (), + Thus => (), } -// Currently types can only be added to top-level bindings. -Type: Typ = { - => Typ::Typ(p), +Thus: () = { + => (), + "." => (), + PropOpt } Semi: Vec = { @@ -55,34 +66,31 @@ Semi: Vec = { } } -ExprTerm: Expr = { - "ⲗ" "." => Expr::Lambda(Rc::new(Binding::Var(n.to_string(), None)), Rc::new(e), None), - // wrong... - => Expr::App(Rc::new(e), Rc::new(Expr::Prop(Rc::new(p)))), - => Expr::Prop(Rc::new(p)), -} - -Prop: Prop = { - "¬" => Prop::Neg(Rc::new(t)), +Prop: () = { + "¬" => (), BinaryProp, } -BinaryProp: Prop = { - "∧" => Prop::And(Rc::new(p1), Rc::new(p2)), - "∨" => Prop::Or(Rc::new(p1), Rc::new(p2)), - "→" => Prop::Imp(Rc::new(p1), Rc::new(p2)), - "↔" => Prop::Iff(Rc::new(p1), Rc::new(p2)), +PropOpt: () = { + Prop, + (), +} - "∧" "¬" => Prop::And(Rc::new(p1), Rc::new(Prop::Neg(Rc::new(p2)))), - "∨" "¬" => Prop::Or(Rc::new(p1), Rc::new(Prop::Neg(Rc::new(p2)))), - "→" "¬" => Prop::Imp(Rc::new(p1), Rc::new(Prop::Neg(Rc::new(p2)))), - "↔" "¬" => Prop::Iff(Rc::new(p1), Rc::new(Prop::Neg(Rc::new(p2)))), - Term, +BinaryProp: () = { + "∧" => (), + "∨" => (), + "→" => (), + "↔" => (), + "∧" "¬" => (), + "∨" "¬" => (), + "→" "¬" => (), + "↔" "¬" => (), + Atom, } -Term: Prop = { - "⊤" => Prop::True, - "(" ")" => p, - => Prop::Var(n.to_string()), +Atom: () = { + "⊤" => (), + "(" Prop ")" => (), + => (), }; diff --git a/src/test.rs b/src/test.rs index 6b74620..4851428 100644 --- a/src/test.rs +++ b/src/test.rs @@ -83,6 +83,62 @@ fn bad_unicode() -> Result<(), MainError> { Ok(test_util::expect_fail(test_util::do_test(&invalid_source))?) } +#[test] +fn thus() -> Result<(), MainError> { + let source = [ + r"", + &unindent( + r#"ab_or_cd : (A ∧ B) ∨ (C ∧ D) → B ∨ D + ≔ ‣ (A ∧ B) ∨ (C ∧ D) ;; +⚡1 + ‣ A ∧ B ;; +⚡2 + ∴ B ;; ∴ ∧E R + ∴ B ∨ D. ;; ∴ ∨I L + ‣ C ∧ D ;; +⚡2 + ∴ D ;; ∴ ∧E R + ∴ B ∨ D. ;; ∴ ∨I R + ∴ B ∨ D. ;; -⚡2 ∴ ∨E + ∴ (A ∧ B) ∨ (C ∧ D) → B ∨ D. ;; -⚡1 ∴ →I + ; + "#, + ), + &unindent( + r#"ab_or_cd : (A ∧ B) ∨ (C ∧ D) ↔ (B ∧ A) ∨ (D ∧ C) + ≔ ‣‣(A ∧ B) ∨ (C ∧ D) ;; +⚡1, +⚡2 + ‣ A ∧ B ;; +⚡3 + ∴ B ;; ∴ ∧E R + ∴ A ;; ∴ ∧E L + ∴ B ∧ A ;; ∴ ∧I + ∴ (B ∧ A) ∨ (D ∧ C). ;; ∴ ∨I L + ‣ C ∧ D ;; +⚡3 + ∴ D ;; ∴ ∧E R + ∴ C ;; ∴ ∧E L + ∴ D ∧ C ;; ∴ ∧I + ∴ (B ∧ A) ∨ (D ∧ C). ;; ∴ ∨I R + ∴ (B ∧ A) ∨ (D ∧ C). ;; -3 ∴ ∨E + ∴ (A ∧ B) ∨ (C ∧ D) → (B ∧ A) ∨ (D ∧ C). ;; -2 ∴ →I + + ‣‣ (B ∧ A) ∨ (D ∧ C) ;; +⚡1, +⚡2 + ‣ B ∧ A ;; +⚡3 + ∴ B ∧ A ∴ A ;; ∴ ∧E R + ∴ B ∧ A ∴ B ;; ??, ∴ ∧E L + ∴ A ∧ B ;; ∴ ∧I + ∴ (A ∧ B) ∨ (C ∧ D). ;; ∴ ∨I L + ‣ D ∧ C ;; +⚡3 + ∴ C ;; ∴ ∧E R + ∴ D ;; ??, ∴ ∧E L + ∴ C ∧ D ;; ∴ ∧I + ∴ (A ∧ B) ∨ (C ∧ D). ;; ∴ ∨I R + ∴ (A ∧ B) ∨ (C ∧ D). ;; -⚡3 ∴ ∨E + ∴ (B ∧ A) ∨ (D ∧ C) → (A ∧ B) ∨ (C ∧ D). ;; -⚡2 ∴ →I + + ∴ (A ∧ B) ∨ (C ∧ D) ↔ (B ∧ A) ∨ (D ∧ C). ;; -⚡1 ∴ ↔I + ; + "#, + ), + ]; + Ok(test_util::expect_success(test_util::do_test(&source))?) +} + #[test] fn good_ascii() -> Result<(), MainError> { let source = [ From e53c1877be856446a6031a2ac8e894bc4c9311a1 Mon Sep 17 00:00:00 2001 From: matt rice Date: Mon, 6 Apr 2020 21:12:54 -0700 Subject: [PATCH 3/3] some unused warnings in grammar, get compiling with logos-0.11.0-rc2 --- src/lex.rs | 12 ++++++------ src/prop.lalrpop | 30 +++++++++++++++--------------- 2 files changed, 21 insertions(+), 21 deletions(-) diff --git a/src/lex.rs b/src/lex.rs index 6ff2cc1..572ab8a 100644 --- a/src/lex.rs +++ b/src/lex.rs @@ -2,8 +2,11 @@ pub use logos::Lexer; use logos::Logos; #[derive(Logos, Debug, Clone, PartialEq)] -#[logos(trivia = r"(\p{Whitespace}+|#.*\n)")] +#[logos(trivia = r"(\p{Whitespace}+|;;.*\n)")] pub enum Token<'a> { + #[token = ","] + Comma, + #[token = "."] Dot, @@ -82,10 +85,6 @@ pub enum Token<'a> { #[token = "]"] RBrack, - // Name ↔ Name - #[regex = r"[a-zA-Z][_a-zA-Z0-9]*"] - Name, - // Since this uses Coptic letters for keywords all greek letters can be used as variable names. // Variables can start with a slash character, a greek/math alphanumeric symbol, // and ascii letters numbers, and subscripts (TODO superscripts) @@ -152,7 +151,8 @@ impl<'a> std::fmt::Display for Token<'a> { Token::RParen => write!(f, ")"), Token::LBrack => write!(f, "["), Token::RBrack => write!(f, "]"), - Token::Name(s) => write!(f, "{}", s), + Token::Name(s) | Token::FancyNameAscii(s) => write!(f, "{}", s), + Token::LexError => write!(f, "Lexical Error"), } } } diff --git a/src/prop.lalrpop b/src/prop.lalrpop index 63a76b7..07e9a56 100644 --- a/src/prop.lalrpop +++ b/src/prop.lalrpop @@ -41,17 +41,17 @@ name: &'a str = { pub prop = Semi; Binding: () = { - "≔" => (), - ":" "≔" => (), + <_n:name> "≔" <_s:Stmt> => (), + <_n:name> ":" <_t:Prop> "≔" <_s:Stmt> => (), } Stmt: () = { - "‣" => (), + <_s: Stmt> "‣" <_t:Thus> => (), Thus => (), } Thus: () = { - => (), - "." => (), + <_t:Thus> <_p: ("∴" PropOpt)> => (), + <_t:Thus> "." <_p:PropOpt> => (), PropOpt } @@ -67,7 +67,7 @@ Semi: Vec = { } Prop: () = { - "¬" => (), + "¬" <_t:BinaryProp> => (), BinaryProp, } @@ -77,20 +77,20 @@ PropOpt: () = { } BinaryProp: () = { - "∧" => (), - "∨" => (), - "→" => (), - "↔" => (), - "∧" "¬" => (), - "∨" "¬" => (), - "→" "¬" => (), - "↔" "¬" => (), + <_p1:BinaryProp> "∧" <_p2:Atom> => (), + <_p1:BinaryProp> "∨" <_p2:Atom> => (), + <_p1:BinaryProp> "→" <_p2:Atom> => (), + <_p1:BinaryProp> "↔" <_p2:Atom> => (), + <_p1:BinaryProp> "∧" "¬" <_p2:Atom> => (), + <_p1:BinaryProp> "∨" "¬" <_p2:Atom> => (), + <_p1:BinaryProp> "→" "¬" <_p2:Atom> => (), + <_p1:BinaryProp> "↔" "¬" <_p2:Atom> => (), Atom, } Atom: () = { "⊤" => (), "(" Prop ")" => (), - => (), + <_n:name> => (), };