From 6f0cef006557bf87d126ce0d8f46e086bf455816 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Wed, 24 Feb 2021 03:18:43 -0300 Subject: [PATCH] initial commit w/ lexer & parser --- .gitignore | 1 + LICENSE | 30 ++++++++++++++++ README.md | 1 + Setup.hs | 2 ++ cubical.cabal | 33 +++++++++++++++++ hie.yaml | 2 ++ src/Main.hs | 5 +++ src/Presyntax/Lexer.x | 40 +++++++++++++++++++++ src/Presyntax/Parser.y | 74 ++++++++++++++++++++++++++++++++++++++ src/Presyntax/Presyntax.hs | 19 ++++++++++ src/Presyntax/Tokens.hs | 26 ++++++++++++++ stack.yaml | 67 ++++++++++++++++++++++++++++++++++ stack.yaml.lock | 13 +++++++ 13 files changed, 313 insertions(+) create mode 100644 .gitignore create mode 100644 LICENSE create mode 100644 README.md create mode 100644 Setup.hs create mode 100644 cubical.cabal create mode 100644 hie.yaml create mode 100644 src/Main.hs create mode 100644 src/Presyntax/Lexer.x create mode 100644 src/Presyntax/Parser.y create mode 100644 src/Presyntax/Presyntax.hs create mode 100644 src/Presyntax/Tokens.hs create mode 100644 stack.yaml create mode 100644 stack.yaml.lock diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..3a5b475 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +.stack-work/ diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..ca46626 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright Abigail Magalhães (c) 2021 + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Abigail Magalhães nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. \ No newline at end of file diff --git a/README.md b/README.md new file mode 100644 index 0000000..a3a84ef --- /dev/null +++ b/README.md @@ -0,0 +1 @@ +# cubical diff --git a/Setup.hs b/Setup.hs new file mode 100644 index 0000000..9a994af --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/cubical.cabal b/cubical.cabal new file mode 100644 index 0000000..b424f7d --- /dev/null +++ b/cubical.cabal @@ -0,0 +1,33 @@ +name: cubical +version: 0.1.0.0 +-- synopsis: +-- description: +homepage: https://github.com/plt-hokusai/cubical#readme +license: BSD3 +license-file: LICENSE +author: Abigail Magalhães +maintainer: magalhaes.alcantara@pucpr.edu.br +copyright: 2021 Abigail Magalhães +category: Web +build-type: Simple +cabal-version: >=2.0 +extra-source-files: README.md + +executable cubical + hs-source-dirs: src + main-is: Main.hs + default-language: Haskell2010 + + build-depends: base ^>= 4.14 + , text ^>= 1.2 + , array ^>= 0.5.4 + , bytestring ^>= 0.10 + + other-modules: Presyntax.Lexer + , Presyntax.Parser + , Presyntax.Tokens + , Presyntax.Presyntax + + build-tool-depends: alex:alex >= 3.2.4 && < 4.0 + , happy:happy >= 1.19.12 && < 2.0 + diff --git a/hie.yaml b/hie.yaml new file mode 100644 index 0000000..4ef275e --- /dev/null +++ b/hie.yaml @@ -0,0 +1,2 @@ +cradle: + stack: diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 index 0000000..9cd992d --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,5 @@ +module Main where + +main :: IO () +main = do + putStrLn "hello world" diff --git a/src/Presyntax/Lexer.x b/src/Presyntax/Lexer.x new file mode 100644 index 0000000..8f3e734 --- /dev/null +++ b/src/Presyntax/Lexer.x @@ -0,0 +1,40 @@ +{ +module Presyntax.Lexer where + +import qualified Data.ByteString.Lazy as Lbs +import qualified Data.Text.Encoding as T +import qualified Data.ByteString as Sbs + +import Presyntax.Tokens +} + +%wrapper "monad-bytestring" + +$alpha = [a-zA-Z] +$digit = [0-9] + +tokens :- + $white+ ; + $alpha [$alpha $digit \_ \']* { yield TokVar } + + \= { always TokEqual } + \: { always TokColon } + + \\ { always TokLambda } + "->" { always TokArrow } + + \( { always TokOParen } + \{ { always TokOBrace } + + \) { always TokCParen } + \} { always TokCBrace } + +{ +alexEOF :: Alex Token +alexEOF = do + (AlexPn _ l c, _, _, _) <- alexGetInput + pure $ Token TokEof l c + +yield k t@(AlexPn _ l c, _, s, _) i = pure (Token (k $! (T.decodeUtf8 (Lbs.toStrict (Lbs.take i s)))) l c) +always k x i = yield (const k) x i +} \ No newline at end of file diff --git a/src/Presyntax/Parser.y b/src/Presyntax/Parser.y new file mode 100644 index 0000000..0dc4125 --- /dev/null +++ b/src/Presyntax/Parser.y @@ -0,0 +1,74 @@ +{ +module Presyntax.Parser where + +import qualified Data.Text as T +import Data.Text (Text) + +import Presyntax.Presyntax +import Presyntax.Tokens +import Presyntax.Lexer + +} + +%name parseExp Exp + +%tokentype { Token } + +%monad { Alex } +%lexer { lexer } { Token TokEof _ _ } + +%errorhandlertype explist +%error { parseError } + +%token + var { Token (TokVar $$) _ _ } + '(' { Token TokOParen _ _ } + ')' { Token TokCParen _ _ } + + '{' { Token TokOBrace _ _ } + '}' { Token TokCBrace _ _ } + + '\\' { Token TokLambda _ _ } + + '->' { Token TokArrow _ _ } + ':' { Token TokColon _ _ } + '=' { Token TokEqual _ _ } + +%% + +Exp :: { Expr } +Exp + : ExpFun Exp { App Ex $1 $2 } + | ExpFun '{' Exp '}' { App Im $1 $3 } + | '\\' LambdaList '->' Exp { makeLams $2 $4 } + | '(' VarList ':' Exp ')' '->' Exp { makePis Ex $2 $4 $7 } + | '{' VarList ':' Exp '}' '->' Exp { makePis Im $2 $4 $7 } + | ExpFun '->' Exp { Pi Ex (T.singleton '_') $1 $3 } + | ExpFun { $1 } + +LambdaList :: { [(Plicity, Text)] } + : var { [(Ex, $1)] } + | var LambdaList { (Ex, $1):$2 } + + | '{'var'}' { [(Im, $2)] } + | '{'var'}' LambdaList { (Im, $2):$4 } + +VarList :: { [Text] } + : var { [$1] } + | var VarList { $1:$2 } + +ExpFun :: { Expr } + : Atom { $1 } + | '(' Exp ')' { $2 } + +Atom :: { Expr } + : var { Var $1 } + +{ +lexer cont = alexMonadScan >>= cont + +parseError x = alexError (show x) + +makeLams xs b = foldr (uncurry Lam) b xs +makePis p xs t b = foldr (flip (Pi p) t) b xs +} \ No newline at end of file diff --git a/src/Presyntax/Presyntax.hs b/src/Presyntax/Presyntax.hs new file mode 100644 index 0000000..b957358 --- /dev/null +++ b/src/Presyntax/Presyntax.hs @@ -0,0 +1,19 @@ +module Presyntax.Presyntax where + +import Data.Text (Text) + +data Plicity + = Im | Ex + deriving (Eq, Show, Ord) + +data Expr + = Var Text + | App Plicity Expr Expr + | Lam Plicity Text Expr + | Pi Plicity Text Expr Expr + deriving (Eq, Show, Ord) + +data Statement + = Decl Text Expr + | Defn Text Expr + deriving (Eq, Show, Ord) \ No newline at end of file diff --git a/src/Presyntax/Tokens.hs b/src/Presyntax/Tokens.hs new file mode 100644 index 0000000..709ec7a --- /dev/null +++ b/src/Presyntax/Tokens.hs @@ -0,0 +1,26 @@ +module Presyntax.Tokens where + +import Data.Text (Text) + +data TokenClass + = TokVar Text + | TokEof + + | TokLambda + | TokArrow + + | TokOParen + | TokOBrace + | TokCParen + | TokCBrace + + | TokColon + | TokEqual + deriving (Eq, Show, Ord) + +data Token + = Token { tokenClass :: TokenClass + , tokStartLine :: !Int + , tokStartCol :: !Int + } + deriving (Eq, Show, Ord) \ No newline at end of file diff --git a/stack.yaml b/stack.yaml new file mode 100644 index 0000000..60846eb --- /dev/null +++ b/stack.yaml @@ -0,0 +1,67 @@ +# This file was automatically generated by 'stack init' +# +# Some commonly used options have been documented as comments in this file. +# For advanced use and comprehensive documentation of the format, please see: +# https://docs.haskellstack.org/en/stable/yaml_configuration/ + +# Resolver to choose a 'specific' stackage snapshot or a compiler version. +# A snapshot resolver dictates the compiler version and the set of packages +# to be used for project dependencies. For example: +# +# resolver: lts-3.5 +# resolver: nightly-2015-09-21 +# resolver: ghc-7.10.2 +# +# The location of a snapshot can be provided as a file or url. Stack assumes +# a snapshot provided as a file might change, whereas a url resource does not. +# +# resolver: ./custom-snapshot.yaml +# resolver: https://example.com/snapshots/2018-01-01.yaml +resolver: + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/1.yaml + +# User packages to be built. +# Various formats can be used as shown in the example below. +# +# packages: +# - some-directory +# - https://example.com/foo/bar/baz-0.0.2.tar.gz +# subdirs: +# - auto-update +# - wai +packages: +- . +# Dependency packages to be pulled from upstream that are not in the resolver. +# These entries can reference officially published versions as well as +# forks / in-progress versions pinned to a git hash. For example: +# +# extra-deps: +# - acme-missiles-0.3 +# - git: https://github.com/commercialhaskell/stack.git +# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a +# +# extra-deps: [] + +# Override default flag values for local packages and extra-deps +# flags: {} + +# Extra package databases containing global packages +# extra-package-dbs: [] + +# Control whether we use the GHC we find on the path +# system-ghc: true +# +# Require a specific version of stack, using version ranges +# require-stack-version: -any # Default +# require-stack-version: ">=2.5" +# +# Override the architecture used by stack, especially useful on Windows +# arch: i386 +# arch: x86_64 +# +# Extra directories used by stack for building +# extra-include-dirs: [/path/to/dir] +# extra-lib-dirs: [/path/to/dir] +# +# Allow a newer minor version of GHC than the snapshot specifies +# compiler-check: newer-minor diff --git a/stack.yaml.lock b/stack.yaml.lock new file mode 100644 index 0000000..0b2383c --- /dev/null +++ b/stack.yaml.lock @@ -0,0 +1,13 @@ +# This file was autogenerated by Stack. +# You should not edit this file by hand. +# For more information, please see the documentation at: +# https://docs.haskellstack.org/en/stable/lock_files + +packages: [] +snapshots: +- completed: + size: 563098 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/1.yaml + sha256: 395775c03e66a4286f134d50346b0b6f1432131cf542886252984b4cfa5fef69 + original: + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/1.yaml