diff --git a/Makefile b/Makefile index ab23ad5..6968ae0 100644 --- a/Makefile +++ b/Makefile @@ -9,15 +9,19 @@ lib: .PHONY: exe exe: - make -C exe exe + $(MAKE) -C exe exe .PHONY: test test: - make -C tests test + $(MAKE) -C tests test + +.PHONY: prove +prove: + $(MAKE) -C tests prove .PHONY: clean clean: - rm -rf build depends - rm -f quox - make -C exe clean - make -C tests clean + $(RM) -r build depends + $(RM) quox + $(MAKE) -C exe clean + $(MAKE) -C tests clean diff --git a/exe/Makefile b/exe/Makefile index 19b9fb3..287a38a 100644 --- a/exe/Makefile +++ b/exe/Makefile @@ -2,7 +2,7 @@ all: test .PHONY: lib lib: - make -C .. lib + $(MAKE) -C .. lib depends/quox: lib mkdir -p depends @@ -14,4 +14,4 @@ exe: depends/quox .PHONY: clean clean: - rm -rf build depends + $(RM) -r build depends diff --git a/quox.ipkg b/quox.ipkg index f3ca34e..6f53343 100644 --- a/quox.ipkg +++ b/quox.ipkg @@ -28,6 +28,7 @@ modules = Quox.Syntax.Term.Subst, Quox.Syntax.Universe, Quox.Syntax.Var, + Quox.Lexer, Quox.Context, Quox.Equal, diff --git a/src/Quox/Lexer.idr b/src/Quox/Lexer.idr new file mode 100644 index 0000000..d2baaa0 --- /dev/null +++ b/src/Quox/Lexer.idr @@ -0,0 +1,129 @@ +module Quox.Lexer + +import Quox.Error + +import Data.String +import public Text.Lexer + + +public export +record Error where + constructor Err + line, col : Int + char : Char + +public export +data Punc += LParen | RParen +| LSquare | RSquare +| LBrace | RBrace +| Comma +| Colon | DblColon +| Arrow | DblArrow +| Times | Triangle +| Wild + +puncRepr : Punc -> Nat +puncRepr = \case + LParen => 0; RParen => 1; LSquare => 2; RSquare => 3 + LBrace => 4; RBrace => 5; Comma => 5 + Colon => 6; DblColon => 7; Arrow => 8; DblArrow => 9 + Times => 10; Triangle => 11 + Wild => 12 + +export Eq Punc where (==) = (==) `on` puncRepr +export Ord Punc where compare = compare `on` puncRepr + +export +Show Punc where + show = \case + LParen => "'('"; RParen => "')'"; LSquare => "'['"; RSquare => "']'" + LBrace => "'{'"; RBrace => "'}'"; Comma => "','" + Colon => "':'"; DblColon => "'∷'"; Arrow => "'→'"; DblArrow => "'⇒'" + Times => "'×'"; Triangle => "'⊲'" + Wild => "'_'" + + + +public export +data Kind += P Punc +| Name | Symbol + +kindRepr : Kind -> (Nat, Nat) +kindRepr (P p) = (0, puncRepr p) +kindRepr Name = (1, 0) +kindRepr Symbol = (2, 0) + +export Eq Kind where (==) = (==) `on` kindRepr +export Ord Kind where compare = compare `on` kindRepr + +export +Show Kind where + show (P p) = show p + show Name = "Name" + show Symbol = "Symbol" + + +export +TokenKind Kind where + TokType (P _) = () + TokType Name = String + TokType Symbol = String + + tokValue (P _) _ = () + tokValue Name x = x + tokValue Symbol x = assert_total strTail x + + +Token' = Token (Maybe Kind) +Token = Token Kind + +TokenMap' = TokenMap Token' +TokenMap = TokenMap Token + +nameStart = pred $ \c => isAlpha c || c == '_' +nameCont = pred $ \c => isAlphaNum c || c == '_' || c == '\'' + +name = nameStart <+> many nameCont <+> reject nameCont + +wild = exact "_" <+> reject nameCont + +%hide Text.Lexer.symbol +symbol = exact "'" <+> name + + +tokens = toTokenMap [ + (lineComment (exact "--"), Nothing), + (blockComment (exact "{-") (exact "-}"), Nothing), + (spaces, Nothing), + + (exact "(", Just $ P LParen), (exact ")", Just $ P RParen), + (exact "[", Just $ P LSquare), (exact "]", Just $ P RSquare), + (exact "{", Just $ P LBrace), (exact "}", Just $ P RBrace), + (exact ",", Just $ P Comma), + (exact "::" <|> exact "∷", Just $ P DblColon), + (exact ":", Just $ P Colon), + + (exact "->" <|> exact "→", Just $ P Arrow), + (exact "=>" <|> exact "⇒", Just $ P DblArrow), + (exact "**" <|> exact "×", Just $ P Times), + (exact "<<" <|> exact "⊲", Just $ P Triangle), + (wild, Just $ P Wild), + + (name, Just Name), (symbol, Just Symbol) +] + +sequenceT : Token (Maybe Kind) -> Maybe (Token Kind) +sequenceT tok = + case tok.kind of + Just k => Just $ {kind := k} tok + Nothing => Nothing + +export +lex : MonadThrow Error m => String -> m (List (WithBounds Token)) +lex str = + let (res, (line, col, str)) = lex tokens str in + case asList str of + [] => pure $ mapMaybe (traverse sequenceT) res + c :: _ => throw $ Err {line, col, char = c} diff --git a/tests/Makefile b/tests/Makefile index c757352..835ba35 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -2,7 +2,7 @@ all: test .PHONY: lib lib: - make -C .. lib + $(MAKE) -C .. lib depends/quox: lib mkdir -p depends @@ -23,4 +23,4 @@ prove: build-tests .PHONY: clean clean: - rm -rf build depends + $(RM) -r build depends diff --git a/tests/TAP.idr b/tests/TAP.idr index 5316ce2..f3a5b7e 100644 --- a/tests/TAP.idr +++ b/tests/TAP.idr @@ -84,13 +84,18 @@ export %inline todo : String -> Test todo label = todoWith label "" -export %inline -skipWith : String -> String -> Test -skipWith label reason = One $ MakeTest label $ pure $ Skip reason +private %inline +makeSkip : String -> String -> Test +makeSkip label reason = One $ MakeTest label $ pure $ Skip reason export %inline -skip : String -> Test -skip label = skipWith label "" +skipWith : Test -> String -> Test +skipWith (One t) reason = makeSkip t.label reason +skipWith (Group l _) reason = makeSkip l reason + +export %inline +skip : Test -> Test +skip test = skipWith test "" export testThrows : Show a => String -> Lazy (Error es a) -> Test diff --git a/tests/Tests.idr b/tests/Tests.idr index 783968a..b24b7fe 100644 --- a/tests/Tests.idr +++ b/tests/Tests.idr @@ -7,7 +7,10 @@ import Tests.Equal import System -allTests = [Equal.tests] +allTests = [ + Lexer.tests, + skip Equal.tests +] main = do opts <- getTestOpts diff --git a/tests/Tests/Lexer.idr b/tests/Tests/Lexer.idr new file mode 100644 index 0000000..a9cf3f5 --- /dev/null +++ b/tests/Tests/Lexer.idr @@ -0,0 +1,105 @@ +module Tests.Lexer + +import Quox.Lexer +import TAP + + +export +ToInfo Error where + toInfo (Err line col char) = + [("line", show line), ("col", show col), ("char", show char)] + +data ExtraError += WrongAnswer (List Kind) (List Kind) +| TestFailed (List Kind) + +ToInfo ExtraError where + toInfo (WrongAnswer exp got) = + [("expected", show exp), ("received", show got)] + toInfo (TestFailed got) = [("failed", show got)] + + +parameters (label : String) (input : String) + acceptsSuchThat' : (List Kind -> Maybe ExtraError) -> Test + acceptsSuchThat' p = test {es = [Lexer.Error, ExtraError]} label $ do + res <- map (kind . val) <$> lex input + case p res of + Just err => throw err + Nothing => pure () + + acceptsSuchThat : (List Kind -> Bool) -> Test + acceptsSuchThat p = acceptsSuchThat' $ \res => + if p res then Nothing else Just $ TestFailed res + + acceptsWith : List Kind -> Test + acceptsWith expect = acceptsSuchThat' $ \res => + if res == expect then Nothing else Just $ WrongAnswer expect res + + accepts : Test + accepts = acceptsSuchThat $ const True + + rejects : Test + rejects = testThrows {es = [Lexer.Error]} label $ delay $ + map (kind . val) <$> lex input + +parameters (input : String) {default False esc : Bool} + show' : String -> String + show' s = if esc then show s else "\"\{s}\"" + + acceptsWith' : List Kind -> Test + acceptsWith' = acceptsWith (show' input) input + + accepts' : Test + accepts' = accepts (show' input) input + + rejects' : Test + rejects' = rejects "\{show' input} (reject)" input + + +tests = "lexer" :- [ + "comments" :- [ + acceptsWith' "" [], + acceptsWith' " \n \t\t " [] {esc = True}, + acceptsWith' "-- a" [], + acceptsWith' "{- -}" [], + acceptsWith' "{--}" [], + acceptsWith' "{------}" [], + acceptsWith' "{- {- -} -}" [], + acceptsWith' "{- } -}" [], + rejects' "{-}", + rejects' "{- {- -}", + acceptsWith' "( -- comment \n )" [P LParen, P RParen] {esc = True} + ], + + "punctuation" :- [ + acceptsWith' "({[:,::]})" + [P LParen, P LBrace, P LSquare, + P Colon, P Comma, P DblColon, + P RSquare, P RBrace, P RParen], + acceptsWith' " ( { [ : , :: ] } ) " + [P LParen, P LBrace, P LSquare, + P Colon, P Comma, P DblColon, + P RSquare, P RBrace, P RParen], + acceptsWith' "-> → => ⇒ ** × << ⊲ ∷" + [P Arrow, P Arrow, P DblArrow, P DblArrow, + P Times, P Times, P Triangle, P Triangle, P DblColon], + acceptsWith' "_" [P Wild] + ], + + "names & symbols" :- [ + acceptsWith' "a" [Name], + acceptsWith' "abc" [Name], + acceptsWith' "_a" [Name], + acceptsWith' "a_" [Name], + acceptsWith' "a_b" [Name], + acceptsWith' "abc'" [Name], + acceptsWith' "a'b'c''" [Name], + acceptsWith' "abc123" [Name], + acceptsWith' "ab cd" [Name, Name], + acceptsWith' "ab{--}cd" [Name, Name], + acceptsWith' "'a" [Symbol], + acceptsWith' "'ab" [Symbol], + acceptsWith' "'_b" [Symbol], + rejects' "'" + ] +]