rzk 0.6.4 → 0.6.5
raw patch · 19 files changed
+1228/−129 lines, 19 filesdep +co-log-coredep +directorydep ~lspdep ~lsp-typesbuild-type:Customsetup-changed
Dependencies added: co-log-core, directory
Dependency ranges changed: lsp, lsp-types
Files
- ChangeLog.md +18/−0
- Setup.hs +29/−2
- grammar/Syntax.cf +164/−0
- rzk.cabal +36/−29
- src/Language/Rzk/Free/Syntax.hs +1/−1
- src/Language/Rzk/Syntax.hs +68/−2
- src/Language/Rzk/Syntax/Abs.hs +1/−1
- src/Language/Rzk/Syntax/Layout.hs +1/−1
- src/Language/Rzk/Syntax/Lex.x +292/−0
- src/Language/Rzk/Syntax/Par.y +457/−0
- src/Language/Rzk/Syntax/Print.hs +38/−36
- src/Language/Rzk/VSCode/Handlers.hs +19/−4
- src/Language/Rzk/VSCode/Logging.hs +20/−0
- src/Language/Rzk/VSCode/Lsp.hs +14/−14
- src/Language/Rzk/VSCode/State.hs +0/−20
- src/Language/Rzk/VSCode/Tokenize.hs +0/−1
- src/Rzk/Main.hs +30/−6
- src/Rzk/Project/Config.hs +18/−0
- src/Rzk/TypeCheck.hs +22/−12
ChangeLog.md view
@@ -6,6 +6,24 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.6.5 — 2023-10-01++This version contains mostly intrastructure improvements:++- Typecheck using `rzk.yaml` if it exists (see [#119](https://github.com/rzk-lang/rzk/pull/119))+- Update Rzk Playground and Nix Flake (see [#84](https://github.com/rzk-lang/rzk/pull/84))+ - Rzk Playground now uses CodeMirror 6 and NextJS+ - `miso` dependency is dropped+ - GHCJS 9.6 is now used+ - Support `snippet={code}` or `code={code}` param (see [#118](https://github.com/rzk-lang/rzk/pull/118))+ - Support for `snippet_url={URL}` is temporarily dropped+- Update to GHC 9.6, latest Stackage Nightly, improve Rzk setup, and GitHub Actions (see [#116](https://github.com/rzk-lang/rzk/pull/116))+- Add logging for Rzk Language Server (see [#114](https://github.com/rzk-lang/rzk/pull/114))++Fixes:++- Fix error messages in Rzk Playground (see [#115](https://github.com/rzk-lang/rzk/pull/115))+ ## v0.6.4 — 2023-09-27 This version improves the stucture of the project, in particular w.r.t dependencies:
Setup.hs view
@@ -1,2 +1,29 @@-import Distribution.Simple-main = defaultMain+-- Source: https://github.com/haskell/cabal/issues/6726#issuecomment-918663262++-- | Custom Setup that runs bnfc to generate the language sub-libraries+-- for the parsers included in Ogma.+module Main (main) where++import Distribution.Simple (defaultMainWithHooks,+ hookedPrograms, postConf,+ preBuild, simpleUserHooks)+import Distribution.Simple.Program (Program (..), findProgramVersion,+ simpleProgram)+import System.Process (system)++-- | Run BNFC on the grammar before the actual build step.+--+-- All options for bnfc are hard-coded here.+main :: IO ()+main = defaultMainWithHooks $ simpleUserHooks+ { hookedPrograms = [ bnfcProgram ]+ , postConf = \args flags packageDesc localBuildInfo -> do+ _ <- system "bnfc -d -p Language.Rzk --generic --functor -o src/ grammar/Syntax.cf"+ postConf simpleUserHooks args flags packageDesc localBuildInfo+ }++-- | TODO: This should be in Cabal.Distribution.Simple.Program.Builtin.+bnfcProgram :: Program+bnfcProgram = (simpleProgram "bnfc")+ { programFindVersion = findProgramVersion "--version" id+ }
+ grammar/Syntax.cf view
@@ -0,0 +1,164 @@+comment "--" ;+comment "{-" "-}" ;++layout toplevel ;++token VarIdentToken ((char - ["-?!.\\;,#\"][)(}{><| \t\n\r"]) (char - ["\\;,#\"][)(}{><| \t\n\r"])*) ;++token HoleIdentToken '?' ;++Module. Module ::= LanguageDecl [Command] ;++HoleIdent. HoleIdent ::= HoleIdentToken ;++VarIdent. VarIdent ::= VarIdentToken ;+separator nonempty VarIdent "" ;++LanguageDecl. LanguageDecl ::= "#lang" Language ";" ;++Rzk1. Language ::= "rzk-1" ;++CommandSetOption. Command ::= "#set-option" String "=" String ;+CommandUnsetOption. Command ::= "#unset-option" String ;++CommandCheck. Command ::= "#check" Term ":" Term ;++CommandCompute. Command ::= "#compute" Term ;+CommandComputeWHNF. Command ::= "#compute-whnf" Term ;+CommandComputeNF. Command ::= "#compute-nf" Term ;++CommandPostulate. Command ::= "#postulate" VarIdent DeclUsedVars [Param] ":" Term ;+commandPostulateNoParams. Command ::= "#postulate" VarIdent DeclUsedVars ":" Term ;+define commandPostulateNoParams x vars ty = CommandPostulate x vars [] ty ;++CommandAssume. Command ::= "#assume" [VarIdent] ":" Term ;+commandVariable. Command ::= "#variable" VarIdent ":" Term ;+define commandVariable name term = CommandAssume [name] term ;+commandVariables. Command ::= "#variables" [VarIdent] ":" Term ;+define commandVariables names term = CommandAssume names term ;++CommandSection. Command ::= "#section" SectionName ;+CommandSectionEnd. Command ::= "#end" SectionName ;++CommandDefine. Command ::= "#define" VarIdent DeclUsedVars [Param] ":" Term ":=" Term ;+commandDefineNoParams. Command ::= "#define" VarIdent DeclUsedVars ":" Term ":=" Term ;+define commandDefineNoParams x vars ty term = CommandDefine x vars [] ty term ;+commandDef. Command ::= "#def" VarIdent DeclUsedVars [Param] ":" Term ":=" Term ;+define commandDef x vars params ty term = CommandDefine x vars params ty term ;+commandDefNoParams. Command ::= "#def" VarIdent DeclUsedVars ":" Term ":=" Term ;+define commandDefNoParams x vars ty term = CommandDefine x vars [] ty term ;+terminator Command ";" ;++DeclUsedVars. DeclUsedVars ::= "uses" "(" [VarIdent] ")" ;+noDeclUsedVars. DeclUsedVars ::= ;+define noDeclUsedVars = DeclUsedVars [] ;++NoSectionName. SectionName ::= ;+SomeSectionName. SectionName ::= VarIdent ;++-- Patterns+PatternUnit. Pattern ::= "unit" ;+PatternVar. Pattern ::= VarIdent ;+PatternPair. Pattern ::= "(" Pattern "," Pattern ")" ;+separator nonempty Pattern "" ;++-- Parameter introduction (for lambda abstractions)+ParamPattern. Param ::= Pattern ;+ParamPatternType. Param ::= "(" [Pattern] ":" Term ")" ;+ParamPatternShape. Param ::= "(" [Pattern] ":" Term "|" Term ")" ;+ParamPatternShapeDeprecated. Param ::= "{" Pattern ":" Term "|" Term "}" ;+separator nonempty Param "" ;++-- Parameter declaration for functions and extension types+ParamType. ParamDecl ::= Term6 ;+ParamTermType. ParamDecl ::= "(" Term ":" Term ")" ;+ParamTermShape. ParamDecl ::= "(" Term ":" Term "|" Term ")" ;+ParamTermTypeDeprecated. ParamDecl ::= "{" Pattern ":" Term "}" ;+ParamVarShapeDeprecated. ParamDecl ::= "{" "(" Pattern ":" Term ")" "|" Term "}" ;+paramVarShapeDeprecated. ParamDecl ::= "{" Pattern ":" Term "|" Term "}" ;+define paramVarShapeDeprecated pat cube tope = ParamVarShapeDeprecated pat cube tope ;++Restriction. Restriction ::= Term "↦" Term ;+separator nonempty Restriction "," ;++-- Universes+Universe. Term7 ::= "U" ;+UniverseCube. Term7 ::= "CUBE" ;+UniverseTope. Term7 ::= "TOPE" ;+-- Cubes+CubeUnit. Term7 ::= "1" ;+CubeUnitStar. Term7 ::= "*₁" ;+Cube2. Term7 ::= "2" ;+Cube2_0. Term7 ::= "0₂" ;+Cube2_1. Term7 ::= "1₂" ;+CubeProduct. Term5 ::= Term5 "×" Term6 ;+-- Topes+TopeTop. Term7 ::= "⊤" ;+TopeBottom. Term7 ::= "⊥" ;+TopeEQ. Term4 ::= Term5 "≡" Term5 ;+TopeLEQ. Term4 ::= Term5 "≤" Term5 ;+TopeAnd. Term3 ::= Term4 "∧" Term3 ;+TopeOr. Term2 ::= Term3 "∨" Term2 ;+-- Tope disjunction elimination+RecBottom. Term7 ::= "recBOT" ;+RecOr. Term7 ::= "recOR" "(" [Restriction] ")" ;+RecOrDeprecated. Term7 ::= "recOR" "(" Term "," Term "," Term "," Term ")" ;+-- Types+TypeFun. Term1 ::= ParamDecl "→" Term1 ;+TypeSigma. Term1 ::= "Σ" "(" Pattern ":" Term ")" "," Term1 ;+TypeUnit. Term7 ::= "Unit" ;+TypeId. Term1 ::= Term2 "=_{" Term "}" Term2 ;+TypeIdSimple. Term1 ::= Term2 "=" Term2 ;+TypeRestricted. Term6 ::= Term6 "[" [Restriction] "]" ;+TypeExtensionDeprecated. Term7 ::= "<" ParamDecl "→" Term ">" ;+-- Terms+App. Term6 ::= Term6 Term7 ;+Lambda. Term1 ::= "\\" [Param] "→" Term1 ;+Pair. Term7 ::= "(" Term "," Term ")" ;+First. Term6 ::= "π₁" Term7 ;+Second. Term6 ::= "π₂" Term7 ;+Unit. Term7 ::= "unit" ;+Refl. Term7 ::= "refl";+ReflTerm. Term7 ::= "refl_{" Term "}" ;+ReflTermType. Term7 ::= "refl_{" Term ":" Term "}" ;+IdJ. Term7 ::= "idJ" "(" Term "," Term "," Term "," Term "," Term "," Term ")" ;+-- Variables and holes+Hole. Term7 ::= HoleIdent;+Var. Term7 ::= VarIdent ;+-- Miscellaneous+TypeAsc. Term ::= Term2 "as" Term1 ;++separator nonempty Term "," ;+coercions Term 7 ;++-- ASCII version of some rules above++ascii_CubeProduct. Term5 ::= Term5 "*" Term6 ;+define ascii_CubeProduct l r = CubeProduct l r ;++ASCII_CubeUnitStar. Term7 ::= "*_1" ;+ASCII_Cube2_0. Term7 ::= "0_2" ;+ASCII_Cube2_1. Term7 ::= "1_2" ;++ASCII_TopeTop. Term7 ::= "TOP" ;+ASCII_TopeBottom. Term7 ::= "BOT" ;+ASCII_TopeEQ. Term4 ::= Term5 "===" Term5 ;+ASCII_TopeLEQ. Term4 ::= Term5 "<=" Term5 ;+ASCII_TopeAnd. Term3 ::= Term4 "/\\" Term3 ;+ASCII_TopeOr. Term2 ::= Term3 "\\/" Term2 ;++ASCII_TypeFun. Term1 ::= ParamDecl "->" Term1 ;+ASCII_TypeSigma. Term1 ::= "Sigma" "(" Pattern ":" Term ")" "," Term1 ;++ASCII_Lambda. Term1 ::= "\\" [Param] "->" Term1 ;+ASCII_Restriction. Restriction ::= Term "|->" Term ;++ASCII_TypeExtensionDeprecated. Term7 ::= "<" ParamDecl "->" Term ">" ;++ASCII_First. Term6 ::= "first" Term7 ;+ASCII_Second. Term6 ::= "second" Term7 ;++-- Alternative Unicode syntax rules++unicode_TypeSigmaAlt. Term1 ::= "∑" "(" Pattern ":" Term ")" "," Term1 ; -- \sum+define unicode_TypeSigmaAlt pat fst snd = TypeSigma pat fst snd ;
rzk.cabal view
@@ -1,11 +1,11 @@-cabal-version: 1.12+cabal-version: 1.24 --- This file has been generated from package.yaml by hpack version 0.35.2.+-- This file has been generated from package.yaml by hpack version 0.36.0. -- -- see: https://github.com/sol/hpack name: rzk-version: 0.6.4+version: 0.6.5 synopsis: An experimental proof assistant for synthetic ∞-categories description: Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme> category: Dependent Types@@ -16,17 +16,24 @@ copyright: 2023 Nikolai Kudasov license: BSD3 license-file: LICENSE-build-type: Simple+build-type: Custom extra-source-files: README.md ChangeLog.md+ grammar/Syntax.cf source-repository head type: git location: https://github.com/rzk-lang/rzk +custom-setup+ setup-depends:+ Cabal >=2.4.0.1 && <4.0+ , base >=4.11.0.0 && <5.0+ , process >=1.6.3.0+ flag lsp- description: Build with LSP support.+ description: Build with LSP support (only available with GHC, not GHCJS). manual: True default: True @@ -43,6 +50,7 @@ Language.Rzk.Syntax.Print Rzk Rzk.Main+ Rzk.Project.Config Rzk.TypeCheck other-modules: Paths_rzk@@ -52,19 +60,17 @@ build-tools: alex >=3.2.4 , happy >=1.19.9+ build-tool-depends:+ BNFC:BNFC >=2.9.4.1 build-depends: Glob >=0.9.3- , aeson >=1.4.2.0 , array >=0.5.3.0 , base >=4.7 && <5 , bifunctors >=5.5.3 , bytestring >=0.10.8.2- , data-default-class >=0.1.2.0- , filepath >=1.4.2.1- , lens >=4.17+ , directory >=1.2.7.0 , mtl >=2.2.2 , optparse-generic >=1.3.0- , stm >=2.5.0.0 , template-haskell >=2.14.0.0 , text >=1.2.3.1 , yaml >=0.11.0.0@@ -74,11 +80,18 @@ Language.Rzk.VSCode.Env Language.Rzk.VSCode.Handlers Language.Rzk.VSCode.Lsp- Language.Rzk.VSCode.State Language.Rzk.VSCode.Tokenize+ Language.Rzk.VSCode.Logging+ cpp-options: -DLSP build-depends:- lsp >=2.1.0.0- , lsp-types >=2.0.1.0+ aeson >=1.4.2.0+ , co-log-core >=0.3.2.0+ , data-default-class >=0.1.2.0+ , filepath >=1.4.2.1+ , lens >=4.17+ , lsp >=2.2.0.0+ , lsp-types >=2.0.2.0+ , stm >=2.5.0.0 executable rzk main-is: Main.hs@@ -90,25 +103,23 @@ build-tools: alex >=3.2.4 , happy >=1.19.9+ build-tool-depends:+ BNFC:BNFC >=2.9.4.1 build-depends: Glob >=0.9.3- , aeson >=1.4.2.0 , array >=0.5.3.0 , base >=4.7 && <5 , bifunctors >=5.5.3 , bytestring >=0.10.8.2- , data-default-class >=0.1.2.0- , filepath >=1.4.2.1- , lens >=4.17+ , directory >=1.2.7.0 , mtl >=2.2.2 , optparse-generic >=1.3.0 , rzk- , stm >=2.5.0.0 , template-haskell >=2.14.0.0 , text >=1.2.3.1 , yaml >=0.11.0.0 default-language: Haskell2010- if flag(lsp) && !impl(ghcjs)+ if !impl(ghcjs) build-depends: with-utf8 >=1.0.2.4 @@ -121,21 +132,19 @@ build-tools: alex >=3.2.4 , happy >=1.19.9+ build-tool-depends:+ BNFC:BNFC >=2.9.4.1 build-depends: Glob , QuickCheck- , aeson >=1.4.2.0 , array >=0.5.3.0 , base , bifunctors >=5.5.3 , bytestring >=0.10.8.2- , data-default-class >=0.1.2.0+ , directory >=1.2.7.0 , doctest- , filepath >=1.4.2.1- , lens >=4.17 , mtl >=2.2.2 , optparse-generic >=1.3.0- , stm >=2.5.0.0 , template-haskell , text >=1.2.3.1 , yaml >=0.11.0.0@@ -152,20 +161,18 @@ build-tools: alex >=3.2.4 , happy >=1.19.9+ build-tool-depends:+ BNFC:BNFC >=2.9.4.1 build-depends: Glob >=0.9.3- , aeson >=1.4.2.0 , array >=0.5.3.0 , base >=4.7 && <5 , bifunctors >=5.5.3 , bytestring >=0.10.8.2- , data-default-class >=0.1.2.0- , filepath >=1.4.2.1- , lens >=4.17+ , directory >=1.2.7.0 , mtl >=2.2.2 , optparse-generic >=1.3.0 , rzk- , stm >=2.5.0.0 , template-haskell >=2.14.0.0 , text >=1.2.3.1 , yaml >=0.11.0.0
src/Language/Rzk/Free/Syntax.hs view
@@ -94,7 +94,7 @@ | TypeUnitF | TypeAscF term term | TypeRestrictedF term [(term, term)]- deriving (Eq)+ deriving (Eq, Functor, Foldable, Traversable) deriveBifunctor ''TermF deriveBifoldable ''TermF deriveBitraversable ''TermF
src/Language/Rzk/Syntax.hs view
@@ -9,7 +9,7 @@ parseModuleRzk, parseModuleFile, parseTerm,- printTree,+ Print.Print(..), printTree, tryExtractMarkdownCodeBlocks, extractMarkdownCodeBlocks, tryOrDisplayException,@@ -23,7 +23,7 @@ import qualified Data.List as List import Language.Rzk.Syntax.Abs-import Language.Rzk.Syntax.Print (printTree)+import qualified Language.Rzk.Syntax.Print as Print import Language.Rzk.Syntax.Layout (resolveLayout) import Language.Rzk.Syntax.Lex (tokens)@@ -121,3 +121,69 @@ | otherwise = NonCode where (prefix, suffix) = List.splitAt 3 line++-- * Overriding BNFC pretty-printer++-- | Like 'Print.printTree', but does not insert newlines for curly braces.+printTree :: Print.Print a => a -> String+printTree = render . Print.prt 0++-- | Like 'Print.render', but does not insert newlines for curly braces.+render :: Print.Doc -> String+render d = rend 0 False (map ($ "") $ d []) ""+ where+ rend+ :: Int -- ^ Indentation level.+ -> Bool -- ^ Pending indentation to be output before next character?+ -> [String]+ -> ShowS+ rend i p = \case+ "[" :ts -> char '[' . rend i False ts+ "(" :ts -> char '(' . rend i False ts+ -- "{" :ts -> onNewLine i p . showChar '{' . new (i+1) ts+ -- "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts+ -- "}" :ts -> onNewLine (i-1) p . showChar '}' . new (i-1) ts+ [";"] -> char ';'+ ";" :ts -> char ';' . new i ts+ t : ts@(s:_) | closingOrPunctuation s+ -> pending . showString t . rend i False ts+ t :ts -> pending . space t . rend i False ts+ [] -> id+ where+ -- Output character after pending indentation.+ char :: Char -> ShowS+ char c = pending . showChar c++ -- Output pending indentation.+ pending :: ShowS+ pending = if p then indent i else id++ -- Indentation (spaces) for given indentation level.+ indent :: Int -> ShowS+ indent i = Print.replicateS (2*i) (showChar ' ')++ -- Continue rendering in new line with new indentation.+ new :: Int -> [String] -> ShowS+ new j ts = showChar '\n' . rend j True ts++ -- -- Make sure we are on a fresh line.+ -- onNewLine :: Int -> Bool -> ShowS+ -- onNewLine i p = (if p then id else showChar '\n') . indent i++ -- Separate given string from following text by a space (if needed).+ space :: String -> ShowS+ space t s =+ case (all isSpace t, null spc, null rest) of+ (True , _ , True ) -> [] -- remove trailing space+ (False, _ , True ) -> t -- remove trailing space+ (False, True, False) -> t ++ ' ' : s -- add space if none+ _ -> t ++ s+ where+ (spc, rest) = span isSpace s++ closingOrPunctuation :: String -> Bool+ closingOrPunctuation [c] = c `elem` closerOrPunct+ closingOrPunctuation _ = False++ closerOrPunct :: String+ closerOrPunct = ")],;"
src/Language/Rzk/Syntax/Abs.hs view
@@ -1,4 +1,4 @@--- File generated by the BNF Converter (bnfc 2.9.4.1).+-- File generated by the BNF Converter (bnfc 2.9.5). {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-}
src/Language/Rzk/Syntax/Layout.hs view
@@ -1,4 +1,4 @@--- File generated by the BNF Converter (bnfc 2.9.4.1).+-- File generated by the BNF Converter (bnfc 2.9.5). {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
+ src/Language/Rzk/Syntax/Lex.x view
@@ -0,0 +1,292 @@+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).++-- Lexer definition for use with Alex 3+{+{-# OPTIONS -fno-warn-incomplete-patterns #-}+{-# OPTIONS_GHC -w #-}++{-# LANGUAGE PatternSynonyms #-}++module Language.Rzk.Syntax.Lex where++import Prelude++import qualified Data.Bits+import Data.Char (ord)+import Data.Function (on)+import Data.Word (Word8)+}++-- Predefined character classes++$c = [A-Z\192-\221] # [\215] -- capital isolatin1 letter (215 = \times) FIXME+$s = [a-z\222-\255] # [\247] -- small isolatin1 letter (247 = \div ) FIXME+$l = [$c $s] -- letter+$d = [0-9] -- digit+$i = [$l $d _ '] -- identifier character+$u = [. \n] -- universal: any character++-- Symbols and non-identifier-like reserved words++@rsyms = \Σ | \π \₁ | \π \₂ | \# "lang" | \; | "rzk" \- "1" | \# "set" \- "option" | \= | \# "unset" \- "option" | \# "check" | \: | \# "compute" | \# "compute" \- "whnf" | \# "compute" \- "nf" | \# "postulate" | \# "assume" | \# "variable" | \# "variables" | \# "section" | \# "end" | \# "define" | \: \= | \# "def" | \( | \) | \, | \| | \{ | \} | \↦ | "1" | \* \₁ | "2" | "0" \₂ | "1" \₂ | \× | \⊤ | \⊥ | \≡ | \≤ | \∧ | \∨ | \→ | \= \_ \{ | \[ | \] | \< | \> | \\ | "refl" \_ \{ | \* | \* \_ "1" | "0" \_ "2" | "1" \_ "2" | \= \= \= | \< \= | \/ \\ | \\ \/ | \- \> | \| \- \> | \∑++:-++-- Line comment "--"+"--" [.]* ;++-- Block comment "{-" "-}"+\{ \- [$u # \-]* \- ([$u # [\- \}]] [$u # \-]* \- | \-)* \} ;++-- Whitespace (skipped)+$white+ ;++-- Symbols+@rsyms+ { tok (eitherResIdent TV) }++-- token VarIdentToken+[$u # [\t \n \r \ \! \" \# \( \) \, \- \. \; \< \> \? \[ \\ \] \{ \| \}]] [$u # [\t \n \r \ \" \# \( \) \, \; \< \> \[ \\ \] \{ \| \}]] *+ { tok (eitherResIdent T_VarIdentToken) }++-- token HoleIdentToken+\?+ { tok (eitherResIdent T_HoleIdentToken) }++-- Keywords and Ident+$l $i*+ { tok (eitherResIdent TV) }++-- String+\" ([$u # [\" \\ \n]] | (\\ (\" | \\ | \' | n | t | r | f)))* \"+ { tok (TL . unescapeInitTail) }++{+-- | Create a token with position.+tok :: (String -> Tok) -> (Posn -> String -> Token)+tok f p = PT p . f++-- | Token without position.+data Tok+ = TK {-# UNPACK #-} !TokSymbol -- ^ Reserved word or symbol.+ | TL !String -- ^ String literal.+ | TI !String -- ^ Integer literal.+ | TV !String -- ^ Identifier.+ | TD !String -- ^ Float literal.+ | TC !String -- ^ Character literal.+ | T_VarIdentToken !String+ | T_HoleIdentToken !String+ deriving (Eq, Show, Ord)++-- | Smart constructor for 'Tok' for the sake of backwards compatibility.+pattern TS :: String -> Int -> Tok+pattern TS t i = TK (TokSymbol t i)++-- | Keyword or symbol tokens have a unique ID.+data TokSymbol = TokSymbol+ { tsText :: String+ -- ^ Keyword or symbol text.+ , tsID :: !Int+ -- ^ Unique ID.+ } deriving (Show)++-- | Keyword/symbol equality is determined by the unique ID.+instance Eq TokSymbol where (==) = (==) `on` tsID++-- | Keyword/symbol ordering is determined by the unique ID.+instance Ord TokSymbol where compare = compare `on` tsID++-- | Token with position.+data Token+ = PT Posn Tok+ | Err Posn+ deriving (Eq, Show, Ord)++-- | Pretty print a position.+printPosn :: Posn -> String+printPosn (Pn _ l c) = "line " ++ show l ++ ", column " ++ show c++-- | Pretty print the position of the first token in the list.+tokenPos :: [Token] -> String+tokenPos (t:_) = printPosn (tokenPosn t)+tokenPos [] = "end of file"++-- | Get the position of a token.+tokenPosn :: Token -> Posn+tokenPosn (PT p _) = p+tokenPosn (Err p) = p++-- | Get line and column of a token.+tokenLineCol :: Token -> (Int, Int)+tokenLineCol = posLineCol . tokenPosn++-- | Get line and column of a position.+posLineCol :: Posn -> (Int, Int)+posLineCol (Pn _ l c) = (l,c)++-- | Convert a token into "position token" form.+mkPosToken :: Token -> ((Int, Int), String)+mkPosToken t = (tokenLineCol t, tokenText t)++-- | Convert a token to its text.+tokenText :: Token -> String+tokenText t = case t of+ PT _ (TS s _) -> s+ PT _ (TL s) -> show s+ PT _ (TI s) -> s+ PT _ (TV s) -> s+ PT _ (TD s) -> s+ PT _ (TC s) -> s+ Err _ -> "#error"+ PT _ (T_VarIdentToken s) -> s+ PT _ (T_HoleIdentToken s) -> s++-- | Convert a token to a string.+prToken :: Token -> String+prToken t = tokenText t++-- | Finite map from text to token organized as binary search tree.+data BTree+ = N -- ^ Nil (leaf).+ | B String Tok BTree BTree+ -- ^ Binary node.+ deriving (Show)++-- | Convert potential keyword into token or use fallback conversion.+eitherResIdent :: (String -> Tok) -> String -> Tok+eitherResIdent tv s = treeFind resWords+ where+ treeFind N = tv s+ treeFind (B a t left right) =+ case compare s a of+ LT -> treeFind left+ GT -> treeFind right+ EQ -> t++-- | The keywords and symbols of the language organized as binary search tree.+resWords :: BTree+resWords =+ b "BOT" 39+ (b "*\8321" 20+ (b "#postulate" 10+ (b "#compute-whnf" 5+ (b "#compute" 3+ (b "#check" 2 (b "#assume" 1 N N) N) (b "#compute-nf" 4 N N))+ (b "#end" 8 (b "#define" 7 (b "#def" 6 N N) N) (b "#lang" 9 N N)))+ (b "#variables" 15+ (b "#unset-option" 13+ (b "#set-option" 12 (b "#section" 11 N N) N)+ (b "#variable" 14 N N))+ (b "*" 18 (b ")" 17 (b "(" 16 N N) N) (b "*_1" 19 N N))))+ (b ":" 30+ (b "0\8322" 25+ (b "/\\" 23 (b "->" 22 (b "," 21 N N) N) (b "0_2" 24 N N))+ (b "1\8322" 28 (b "1_2" 27 (b "1" 26 N N) N) (b "2" 29 N N)))+ (b "=" 35+ (b "<" 33 (b ";" 32 (b ":=" 31 N N) N) (b "<=" 34 N N))+ (b "=_{" 37 (b "===" 36 N N) (b ">" 38 N N)))))+ (b "unit" 59+ (b "]" 49+ (b "U" 44+ (b "TOP" 42 (b "Sigma" 41 (b "CUBE" 40 N N) N) (b "TOPE" 43 N N))+ (b "\\" 47 (b "[" 46 (b "Unit" 45 N N) N) (b "\\/" 48 N N)))+ (b "recOR" 54+ (b "idJ" 52 (b "first" 51 (b "as" 50 N N) N) (b "recBOT" 53 N N))+ (b "rzk-1" 57+ (b "refl_{" 56 (b "refl" 55 N N) N) (b "second" 58 N N))))+ (b "\8594" 69+ (b "}" 64+ (b "|" 62 (b "{" 61 (b "uses" 60 N N) N) (b "|->" 63 N N))+ (b "\960\8321" 67+ (b "\931" 66 (b "\215" 65 N N) N) (b "\960\8322" 68 N N)))+ (b "\8801" 74+ (b "\8743" 72+ (b "\8721" 71 (b "\8614" 70 N N) N) (b "\8744" 73 N N))+ (b "\8868" 76 (b "\8804" 75 N N) (b "\8869" 77 N N)))))+ where+ b s n = B bs (TS bs n)+ where+ bs = s++-- | Unquote string literal.+unescapeInitTail :: String -> String+unescapeInitTail = id . unesc . tail . id+ where+ unesc s = case s of+ '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs+ '\\':'n':cs -> '\n' : unesc cs+ '\\':'t':cs -> '\t' : unesc cs+ '\\':'r':cs -> '\r' : unesc cs+ '\\':'f':cs -> '\f' : unesc cs+ '"':[] -> []+ c:cs -> c : unesc cs+ _ -> []++-------------------------------------------------------------------+-- Alex wrapper code.+-- A modified "posn" wrapper.+-------------------------------------------------------------------++data Posn = Pn !Int !Int !Int+ deriving (Eq, Show, Ord)++alexStartPos :: Posn+alexStartPos = Pn 0 1 1++alexMove :: Posn -> Char -> Posn+alexMove (Pn a l c) '\t' = Pn (a+1) l (((c+7) `div` 8)*8+1)+alexMove (Pn a l c) '\n' = Pn (a+1) (l+1) 1+alexMove (Pn a l c) _ = Pn (a+1) l (c+1)++type Byte = Word8++type AlexInput = (Posn, -- current position,+ Char, -- previous char+ [Byte], -- pending bytes on the current char+ String) -- current input string++tokens :: String -> [Token]+tokens str = go (alexStartPos, '\n', [], str)+ where+ go :: AlexInput -> [Token]+ go inp@(pos, _, _, str) =+ case alexScan inp 0 of+ AlexEOF -> []+ AlexError (pos, _, _, _) -> [Err pos]+ AlexSkip inp' len -> go inp'+ AlexToken inp' len act -> act pos (take len str) : (go inp')++alexGetByte :: AlexInput -> Maybe (Byte,AlexInput)+alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s))+alexGetByte (p, _, [], s) =+ case s of+ [] -> Nothing+ (c:s) ->+ let p' = alexMove p c+ (b:bs) = utf8Encode c+ in p' `seq` Just (b, (p', c, bs, s))++alexInputPrevChar :: AlexInput -> Char+alexInputPrevChar (p, c, bs, s) = c++-- | Encode a Haskell String to a list of Word8 values, in UTF8 format.+utf8Encode :: Char -> [Word8]+utf8Encode = map fromIntegral . go . ord+ where+ go oc+ | oc <= 0x7f = [oc]++ | oc <= 0x7ff = [ 0xc0 + (oc `Data.Bits.shiftR` 6)+ , 0x80 + oc Data.Bits..&. 0x3f+ ]++ | oc <= 0xffff = [ 0xe0 + (oc `Data.Bits.shiftR` 12)+ , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)+ , 0x80 + oc Data.Bits..&. 0x3f+ ]+ | otherwise = [ 0xf0 + (oc `Data.Bits.shiftR` 18)+ , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f)+ , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)+ , 0x80 + oc Data.Bits..&. 0x3f+ ]+}
+ src/Language/Rzk/Syntax/Par.y view
@@ -0,0 +1,457 @@+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).++-- Parser definition for use with Happy+{+{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}+{-# LANGUAGE PatternSynonyms #-}++module Language.Rzk.Syntax.Par+ ( happyError+ , myLexer+ , pModule+ , pHoleIdent+ , pVarIdent+ , pListVarIdent+ , pLanguageDecl+ , pLanguage+ , pCommand+ , pListCommand+ , pDeclUsedVars+ , pSectionName+ , pPattern+ , pListPattern+ , pParam+ , pListParam+ , pParamDecl+ , pRestriction+ , pListRestriction+ , pTerm7+ , pTerm5+ , pTerm4+ , pTerm3+ , pTerm2+ , pTerm1+ , pTerm6+ , pTerm+ , pListTerm+ ) where++import Prelude++import qualified Language.Rzk.Syntax.Abs+import Language.Rzk.Syntax.Lex++}++%name pModule_internal Module+%name pHoleIdent_internal HoleIdent+%name pVarIdent_internal VarIdent+%name pListVarIdent_internal ListVarIdent+%name pLanguageDecl_internal LanguageDecl+%name pLanguage_internal Language+%name pCommand_internal Command+%name pListCommand_internal ListCommand+%name pDeclUsedVars_internal DeclUsedVars+%name pSectionName_internal SectionName+%name pPattern_internal Pattern+%name pListPattern_internal ListPattern+%name pParam_internal Param+%name pListParam_internal ListParam+%name pParamDecl_internal ParamDecl+%name pRestriction_internal Restriction+%name pListRestriction_internal ListRestriction+%name pTerm7_internal Term7+%name pTerm5_internal Term5+%name pTerm4_internal Term4+%name pTerm3_internal Term3+%name pTerm2_internal Term2+%name pTerm1_internal Term1+%name pTerm6_internal Term6+%name pTerm_internal Term+%name pListTerm_internal ListTerm+-- no lexer declaration+%monad { Err } { (>>=) } { return }+%tokentype {Token}+%token+ '#assume' { PT _ (TS _ 1) }+ '#check' { PT _ (TS _ 2) }+ '#compute' { PT _ (TS _ 3) }+ '#compute-nf' { PT _ (TS _ 4) }+ '#compute-whnf' { PT _ (TS _ 5) }+ '#def' { PT _ (TS _ 6) }+ '#define' { PT _ (TS _ 7) }+ '#end' { PT _ (TS _ 8) }+ '#lang' { PT _ (TS _ 9) }+ '#postulate' { PT _ (TS _ 10) }+ '#section' { PT _ (TS _ 11) }+ '#set-option' { PT _ (TS _ 12) }+ '#unset-option' { PT _ (TS _ 13) }+ '#variable' { PT _ (TS _ 14) }+ '#variables' { PT _ (TS _ 15) }+ '(' { PT _ (TS _ 16) }+ ')' { PT _ (TS _ 17) }+ '*' { PT _ (TS _ 18) }+ '*_1' { PT _ (TS _ 19) }+ '*₁' { PT _ (TS _ 20) }+ ',' { PT _ (TS _ 21) }+ '->' { PT _ (TS _ 22) }+ '/\\' { PT _ (TS _ 23) }+ '0_2' { PT _ (TS _ 24) }+ '0₂' { PT _ (TS _ 25) }+ '1' { PT _ (TS _ 26) }+ '1_2' { PT _ (TS _ 27) }+ '1₂' { PT _ (TS _ 28) }+ '2' { PT _ (TS _ 29) }+ ':' { PT _ (TS _ 30) }+ ':=' { PT _ (TS _ 31) }+ ';' { PT _ (TS _ 32) }+ '<' { PT _ (TS _ 33) }+ '<=' { PT _ (TS _ 34) }+ '=' { PT _ (TS _ 35) }+ '===' { PT _ (TS _ 36) }+ '=_{' { PT _ (TS _ 37) }+ '>' { PT _ (TS _ 38) }+ 'BOT' { PT _ (TS _ 39) }+ 'CUBE' { PT _ (TS _ 40) }+ 'Sigma' { PT _ (TS _ 41) }+ 'TOP' { PT _ (TS _ 42) }+ 'TOPE' { PT _ (TS _ 43) }+ 'U' { PT _ (TS _ 44) }+ 'Unit' { PT _ (TS _ 45) }+ '[' { PT _ (TS _ 46) }+ '\\' { PT _ (TS _ 47) }+ '\\/' { PT _ (TS _ 48) }+ ']' { PT _ (TS _ 49) }+ 'as' { PT _ (TS _ 50) }+ 'first' { PT _ (TS _ 51) }+ 'idJ' { PT _ (TS _ 52) }+ 'recBOT' { PT _ (TS _ 53) }+ 'recOR' { PT _ (TS _ 54) }+ 'refl' { PT _ (TS _ 55) }+ 'refl_{' { PT _ (TS _ 56) }+ 'rzk-1' { PT _ (TS _ 57) }+ 'second' { PT _ (TS _ 58) }+ 'unit' { PT _ (TS _ 59) }+ 'uses' { PT _ (TS _ 60) }+ '{' { PT _ (TS _ 61) }+ '|' { PT _ (TS _ 62) }+ '|->' { PT _ (TS _ 63) }+ '}' { PT _ (TS _ 64) }+ '×' { PT _ (TS _ 65) }+ 'Σ' { PT _ (TS _ 66) }+ 'π₁' { PT _ (TS _ 67) }+ 'π₂' { PT _ (TS _ 68) }+ '→' { PT _ (TS _ 69) }+ '↦' { PT _ (TS _ 70) }+ '∑' { PT _ (TS _ 71) }+ '∧' { PT _ (TS _ 72) }+ '∨' { PT _ (TS _ 73) }+ '≡' { PT _ (TS _ 74) }+ '≤' { PT _ (TS _ 75) }+ '⊤' { PT _ (TS _ 76) }+ '⊥' { PT _ (TS _ 77) }+ L_quoted { PT _ (TL _) }+ L_VarIdentToken { PT _ (T_VarIdentToken _) }+ L_HoleIdentToken { PT _ (T_HoleIdentToken _) }++%%++String :: { (Language.Rzk.Syntax.Abs.BNFC'Position, String) }+String : L_quoted { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), ((\(PT _ (TL s)) -> s) $1)) }++VarIdentToken :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.VarIdentToken) }+VarIdentToken : L_VarIdentToken { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.VarIdentToken (tokenText $1)) }++HoleIdentToken :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.HoleIdentToken) }+HoleIdentToken : L_HoleIdentToken { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.HoleIdentToken (tokenText $1)) }++Module :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Module) }+Module+ : LanguageDecl ListCommand { (fst $1, Language.Rzk.Syntax.Abs.Module (fst $1) (snd $1) (snd $2)) }++HoleIdent :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.HoleIdent) }+HoleIdent+ : HoleIdentToken { (fst $1, Language.Rzk.Syntax.Abs.HoleIdent (fst $1) (snd $1)) }++VarIdent :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.VarIdent) }+VarIdent+ : VarIdentToken { (fst $1, Language.Rzk.Syntax.Abs.VarIdent (fst $1) (snd $1)) }++ListVarIdent :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.VarIdent]) }+ListVarIdent+ : VarIdent { (fst $1, (:[]) (snd $1)) }+ | VarIdent ListVarIdent { (fst $1, (:) (snd $1) (snd $2)) }++LanguageDecl :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.LanguageDecl) }+LanguageDecl+ : '#lang' Language ';' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.LanguageDecl (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }++Language :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Language) }+Language+ : 'rzk-1' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Rzk1 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }++Command :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Command) }+Command+ : '#set-option' String '=' String { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandSetOption (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '#unset-option' String { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandUnsetOption (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | '#check' Term ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandCheck (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '#compute' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandCompute (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | '#compute-whnf' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandComputeWHNF (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | '#compute-nf' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandComputeNF (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | '#postulate' VarIdent DeclUsedVars ListParam ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandPostulate (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $4) (snd $6)) }+ | '#postulate' VarIdent DeclUsedVars ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandPostulateNoParams (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $5)) }+ | '#assume' ListVarIdent ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandAssume (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '#variable' VarIdent ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandVariable (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '#variables' ListVarIdent ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandVariables (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '#section' SectionName { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandSection (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | '#end' SectionName { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandSectionEnd (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | '#define' VarIdent DeclUsedVars ListParam ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandDefine (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $4) (snd $6) (snd $8)) }+ | '#define' VarIdent DeclUsedVars ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandDefineNoParams (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $5) (snd $7)) }+ | '#def' VarIdent DeclUsedVars ListParam ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandDef (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $4) (snd $6) (snd $8)) }+ | '#def' VarIdent DeclUsedVars ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandDefNoParams (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $5) (snd $7)) }++ListCommand :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Command]) }+ListCommand+ : {- empty -} { (Language.Rzk.Syntax.Abs.BNFC'NoPosition, []) }+ | Command ';' ListCommand { (fst $1, (:) (snd $1) (snd $3)) }++DeclUsedVars :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.DeclUsedVars) }+DeclUsedVars+ : 'uses' '(' ListVarIdent ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.DeclUsedVars (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3)) }+ | {- empty -} { (Language.Rzk.Syntax.Abs.BNFC'NoPosition, Language.Rzk.Syntax.Abs.noDeclUsedVars Language.Rzk.Syntax.Abs.BNFC'NoPosition) }++SectionName :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.SectionName) }+SectionName+ : {- empty -} { (Language.Rzk.Syntax.Abs.BNFC'NoPosition, Language.Rzk.Syntax.Abs.NoSectionName Language.Rzk.Syntax.Abs.BNFC'NoPosition) }+ | VarIdent { (fst $1, Language.Rzk.Syntax.Abs.SomeSectionName (fst $1) (snd $1)) }++Pattern :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Pattern) }+Pattern+ : 'unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | VarIdent { (fst $1, Language.Rzk.Syntax.Abs.PatternVar (fst $1) (snd $1)) }+ | '(' Pattern ',' Pattern ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternPair (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }++ListPattern :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Pattern]) }+ListPattern+ : Pattern { (fst $1, (:[]) (snd $1)) }+ | Pattern ListPattern { (fst $1, (:) (snd $1) (snd $2)) }++Param :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Param) }+Param+ : Pattern { (fst $1, Language.Rzk.Syntax.Abs.ParamPattern (fst $1) (snd $1)) }+ | '(' ListPattern ':' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamPatternType (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '(' ListPattern ':' Term '|' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamPatternShape (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }+ | '{' Pattern ':' Term '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamPatternShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }++ListParam :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Param]) }+ListParam+ : Param { (fst $1, (:[]) (snd $1)) }+ | Param ListParam { (fst $1, (:) (snd $1) (snd $2)) }++ParamDecl :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.ParamDecl) }+ParamDecl+ : Term6 { (fst $1, Language.Rzk.Syntax.Abs.ParamType (fst $1) (snd $1)) }+ | '(' Term ':' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamTermType (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '(' Term ':' Term '|' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamTermShape (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }+ | '{' Pattern ':' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamTermTypeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '{' '(' Pattern ':' Term ')' '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamVarShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }+ | '{' Pattern ':' Term '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.paramVarShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }++Restriction :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Restriction) }+Restriction+ : Term '↦' Term { (fst $1, Language.Rzk.Syntax.Abs.Restriction (fst $1) (snd $1) (snd $3)) }+ | Term '|->' Term { (fst $1, Language.Rzk.Syntax.Abs.ASCII_Restriction (fst $1) (snd $1) (snd $3)) }++ListRestriction :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Restriction]) }+ListRestriction+ : Restriction { (fst $1, (:[]) (snd $1)) }+ | Restriction ',' ListRestriction { (fst $1, (:) (snd $1) (snd $3)) }++Term7 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }+Term7+ : 'U' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Universe (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'CUBE' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.UniverseCube (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'TOPE' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.UniverseTope (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '1' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CubeUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '*₁' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CubeUnitStar (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '2' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Cube2 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '0₂' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Cube2_0 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '1₂' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Cube2_1 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '⊤' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TopeTop (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '⊥' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TopeBottom (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'recBOT' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.RecBottom (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'recOR' '(' ListRestriction ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.RecOr (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3)) }+ | 'recOR' '(' Term ',' Term ',' Term ',' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.RecOrDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $7) (snd $9)) }+ | 'Unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '<' ParamDecl '→' Term '>' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeExtensionDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '(' Term ',' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Pair (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | 'unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Unit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'refl' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Refl (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'refl_{' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ReflTerm (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | 'refl_{' Term ':' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ReflTermType (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | 'idJ' '(' Term ',' Term ',' Term ',' Term ',' Term ',' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.IdJ (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $7) (snd $9) (snd $11) (snd $13)) }+ | HoleIdent { (fst $1, Language.Rzk.Syntax.Abs.Hole (fst $1) (snd $1)) }+ | VarIdent { (fst $1, Language.Rzk.Syntax.Abs.Var (fst $1) (snd $1)) }+ | '(' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), (snd $2)) }+ | '*_1' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_CubeUnitStar (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '0_2' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Cube2_0 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '1_2' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Cube2_1 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'TOP' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TopeTop (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'BOT' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TopeBottom (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '<' ParamDecl '->' Term '>' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TypeExtensionDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }++Term5 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }+Term5+ : Term5 '×' Term6 { (fst $1, Language.Rzk.Syntax.Abs.CubeProduct (fst $1) (snd $1) (snd $3)) }+ | Term6 { (fst $1, (snd $1)) }+ | Term5 '*' Term6 { (fst $1, Language.Rzk.Syntax.Abs.ascii_CubeProduct (fst $1) (snd $1) (snd $3)) }++Term4 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }+Term4+ : Term5 '≡' Term5 { (fst $1, Language.Rzk.Syntax.Abs.TopeEQ (fst $1) (snd $1) (snd $3)) }+ | Term5 '≤' Term5 { (fst $1, Language.Rzk.Syntax.Abs.TopeLEQ (fst $1) (snd $1) (snd $3)) }+ | Term5 { (fst $1, (snd $1)) }+ | Term5 '===' Term5 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeEQ (fst $1) (snd $1) (snd $3)) }+ | Term5 '<=' Term5 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeLEQ (fst $1) (snd $1) (snd $3)) }++Term3 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }+Term3+ : Term4 '∧' Term3 { (fst $1, Language.Rzk.Syntax.Abs.TopeAnd (fst $1) (snd $1) (snd $3)) }+ | Term4 { (fst $1, (snd $1)) }+ | Term4 '/\\' Term3 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeAnd (fst $1) (snd $1) (snd $3)) }++Term2 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }+Term2+ : Term3 '∨' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TopeOr (fst $1) (snd $1) (snd $3)) }+ | Term3 { (fst $1, (snd $1)) }+ | Term3 '\\/' Term2 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeOr (fst $1) (snd $1) (snd $3)) }++Term1 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }+Term1+ : ParamDecl '→' Term1 { (fst $1, Language.Rzk.Syntax.Abs.TypeFun (fst $1) (snd $1) (snd $3)) }+ | 'Σ' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeSigma (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }+ | Term2 '=_{' Term '}' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TypeId (fst $1) (snd $1) (snd $3) (snd $5)) }+ | Term2 '=' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TypeIdSimple (fst $1) (snd $1) (snd $3)) }+ | '\\' ListParam '→' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Lambda (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | Term2 { (fst $1, (snd $1)) }+ | ParamDecl '->' Term1 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TypeFun (fst $1) (snd $1) (snd $3)) }+ | 'Sigma' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TypeSigma (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }+ | '\\' ListParam '->' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Lambda (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '∑' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.unicode_TypeSigmaAlt (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }++Term6 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }+Term6+ : Term6 '[' ListRestriction ']' { (fst $1, Language.Rzk.Syntax.Abs.TypeRestricted (fst $1) (snd $1) (snd $3)) }+ | Term6 Term7 { (fst $1, Language.Rzk.Syntax.Abs.App (fst $1) (snd $1) (snd $2)) }+ | 'π₁' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.First (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | 'π₂' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Second (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | Term7 { (fst $1, (snd $1)) }+ | 'first' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_First (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | 'second' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Second (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }++Term :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }+Term+ : Term2 'as' Term1 { (fst $1, Language.Rzk.Syntax.Abs.TypeAsc (fst $1) (snd $1) (snd $3)) }+ | Term1 { (fst $1, (snd $1)) }++ListTerm :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Term]) }+ListTerm+ : Term { (fst $1, (:[]) (snd $1)) }+ | Term ',' ListTerm { (fst $1, (:) (snd $1) (snd $3)) }++{++type Err = Either String++happyError :: [Token] -> Err a+happyError ts = Left $+ "syntax error at " ++ tokenPos ts +++ case ts of+ [] -> []+ [Err _] -> " due to lexer error"+ t:_ -> " before `" ++ (prToken t) ++ "'"++myLexer :: String -> [Token]+myLexer = tokens++-- Entrypoints++pModule :: [Token] -> Err Language.Rzk.Syntax.Abs.Module+pModule = fmap snd . pModule_internal++pHoleIdent :: [Token] -> Err Language.Rzk.Syntax.Abs.HoleIdent+pHoleIdent = fmap snd . pHoleIdent_internal++pVarIdent :: [Token] -> Err Language.Rzk.Syntax.Abs.VarIdent+pVarIdent = fmap snd . pVarIdent_internal++pListVarIdent :: [Token] -> Err [Language.Rzk.Syntax.Abs.VarIdent]+pListVarIdent = fmap snd . pListVarIdent_internal++pLanguageDecl :: [Token] -> Err Language.Rzk.Syntax.Abs.LanguageDecl+pLanguageDecl = fmap snd . pLanguageDecl_internal++pLanguage :: [Token] -> Err Language.Rzk.Syntax.Abs.Language+pLanguage = fmap snd . pLanguage_internal++pCommand :: [Token] -> Err Language.Rzk.Syntax.Abs.Command+pCommand = fmap snd . pCommand_internal++pListCommand :: [Token] -> Err [Language.Rzk.Syntax.Abs.Command]+pListCommand = fmap snd . pListCommand_internal++pDeclUsedVars :: [Token] -> Err Language.Rzk.Syntax.Abs.DeclUsedVars+pDeclUsedVars = fmap snd . pDeclUsedVars_internal++pSectionName :: [Token] -> Err Language.Rzk.Syntax.Abs.SectionName+pSectionName = fmap snd . pSectionName_internal++pPattern :: [Token] -> Err Language.Rzk.Syntax.Abs.Pattern+pPattern = fmap snd . pPattern_internal++pListPattern :: [Token] -> Err [Language.Rzk.Syntax.Abs.Pattern]+pListPattern = fmap snd . pListPattern_internal++pParam :: [Token] -> Err Language.Rzk.Syntax.Abs.Param+pParam = fmap snd . pParam_internal++pListParam :: [Token] -> Err [Language.Rzk.Syntax.Abs.Param]+pListParam = fmap snd . pListParam_internal++pParamDecl :: [Token] -> Err Language.Rzk.Syntax.Abs.ParamDecl+pParamDecl = fmap snd . pParamDecl_internal++pRestriction :: [Token] -> Err Language.Rzk.Syntax.Abs.Restriction+pRestriction = fmap snd . pRestriction_internal++pListRestriction :: [Token] -> Err [Language.Rzk.Syntax.Abs.Restriction]+pListRestriction = fmap snd . pListRestriction_internal++pTerm7 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm7 = fmap snd . pTerm7_internal++pTerm5 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm5 = fmap snd . pTerm5_internal++pTerm4 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm4 = fmap snd . pTerm4_internal++pTerm3 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm3 = fmap snd . pTerm3_internal++pTerm2 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm2 = fmap snd . pTerm2_internal++pTerm1 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm1 = fmap snd . pTerm1_internal++pTerm6 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm6 = fmap snd . pTerm6_internal++pTerm :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm = fmap snd . pTerm_internal++pListTerm :: [Token] -> Err [Language.Rzk.Syntax.Abs.Term]+pListTerm = fmap snd . pListTerm_internal+}+
src/Language/Rzk/Syntax/Print.hs view
@@ -1,8 +1,8 @@--- File generated by the BNF Converter (bnfc 2.9.4.1).+-- File generated by the BNF Converter (bnfc 2.9.5). -{-# LANGUAGE CPP #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-} #if __GLASGOW_HASKELL__ <= 708 {-# LANGUAGE OverlappingInstances #-} #endif@@ -11,13 +11,16 @@ module Language.Rzk.Syntax.Print where -import Data.Char (Char, isSpace)+import Prelude+ ( ($), (.)+ , Bool(..), (==), (<)+ , Int, Integer, Double, (+), (-), (*)+ , String, (++)+ , ShowS, showChar, showString+ , all, elem, foldr, id, map, null, replicate, shows, span+ )+import Data.Char ( Char, isSpace ) import qualified Language.Rzk.Syntax.Abs-import Prelude (Bool (..), Double, Int, Integer,- ShowS, String, all, elem, foldr, id,- map, null, replicate, showChar,- showString, shows, span, ($), (*),- (++), (.), (<), (==)) -- | The top-level printing method. @@ -40,9 +43,9 @@ rend i p = \case "[" :ts -> char '[' . rend i False ts "(" :ts -> char '(' . rend i False ts- -- "{" :ts -> onNewLine i p . showChar '{' . new (i+1) ts- -- "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts- -- "}" :ts -> onNewLine (i-1) p . showChar '}' . new (i-1) ts+ "{" :ts -> onNewLine i p . showChar '{' . new (i+1) ts+ "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts+ "}" :ts -> onNewLine (i-1) p . showChar '}' . new (i-1) ts [";"] -> char ';' ";" :ts -> char ';' . new i ts t : ts@(s:_) | closingOrPunctuation s@@ -67,19 +70,18 @@ new j ts = showChar '\n' . rend j True ts -- Make sure we are on a fresh line.- -- onNewLine :: Int -> Bool -> ShowS- -- onNewLine i p = (if p then id else showChar '\n') . indent i+ onNewLine :: Int -> Bool -> ShowS+ onNewLine i p = (if p then id else showChar '\n') . indent i -- Separate given string from following text by a space (if needed). space :: String -> ShowS space t s =- case (all isSpace t', null spc, null rest) of- (True , _ , True ) -> [] -- remove trailing space- (False, _ , True ) -> t' -- remove trailing space- (False, True, False) -> t' ++ ' ' : s -- add space if none- _ -> t' ++ s+ case (all isSpace t, null spc, null rest) of+ (True , _ , True ) -> [] -- remove trailing space+ (False, _ , True ) -> t -- remove trailing space+ (False, True, False) -> t ++ ' ' : s -- add space if none+ _ -> t ++ s where- t' = showString t [] (spc, rest) = span isSpace s closingOrPunctuation :: String -> Bool@@ -121,10 +123,10 @@ mkEsc :: Char -> Char -> ShowS mkEsc q = \case s | s == q -> showChar '\\' . showChar s- '\\' -> showString "\\\\"- '\n' -> showString "\\n"- '\t' -> showString "\\t"- s -> showChar s+ '\\' -> showString "\\\\"+ '\n' -> showString "\\n"+ '\t' -> showString "\\t"+ s -> showChar s prPrec :: Int -> Int -> Doc -> Doc prPrec i j = if j < i then parenth else id@@ -152,8 +154,8 @@ Language.Rzk.Syntax.Abs.VarIdent _ varidenttoken -> prPrec i 0 (concatD [prt 0 varidenttoken]) instance Print [Language.Rzk.Syntax.Abs.VarIdent' a] where- prt _ [] = concatD []- prt _ [x] = concatD [prt 0 x]+ prt _ [] = concatD []+ prt _ [x] = concatD [prt 0 x] prt _ (x:xs) = concatD [prt 0 x, prt 0 xs] instance Print (Language.Rzk.Syntax.Abs.LanguageDecl' a) where@@ -179,7 +181,7 @@ Language.Rzk.Syntax.Abs.CommandDefine _ varident declusedvars params term1 term2 -> prPrec i 0 (concatD [doc (showString "#define"), prt 0 varident, prt 0 declusedvars, prt 0 params, doc (showString ":"), prt 0 term1, doc (showString ":="), prt 0 term2]) instance Print [Language.Rzk.Syntax.Abs.Command' a] where- prt _ [] = concatD []+ prt _ [] = concatD [] prt _ (x:xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs] instance Print (Language.Rzk.Syntax.Abs.DeclUsedVars' a) where@@ -198,8 +200,8 @@ Language.Rzk.Syntax.Abs.PatternPair _ pattern_1 pattern_2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ")")]) instance Print [Language.Rzk.Syntax.Abs.Pattern' a] where- prt _ [] = concatD []- prt _ [x] = concatD [prt 0 x]+ prt _ [] = concatD []+ prt _ [x] = concatD [prt 0 x] prt _ (x:xs) = concatD [prt 0 x, prt 0 xs] instance Print (Language.Rzk.Syntax.Abs.Param' a) where@@ -210,8 +212,8 @@ Language.Rzk.Syntax.Abs.ParamPatternShapeDeprecated _ pattern_ term1 term2 -> prPrec i 0 (concatD [doc (showString "{"), prt 0 pattern_, doc (showString ":"), prt 0 term1, doc (showString "|"), prt 0 term2, doc (showString "}")]) instance Print [Language.Rzk.Syntax.Abs.Param' a] where- prt _ [] = concatD []- prt _ [x] = concatD [prt 0 x]+ prt _ [] = concatD []+ prt _ [x] = concatD [prt 0 x] prt _ (x:xs) = concatD [prt 0 x, prt 0 xs] instance Print (Language.Rzk.Syntax.Abs.ParamDecl' a) where@@ -228,8 +230,8 @@ Language.Rzk.Syntax.Abs.ASCII_Restriction _ term1 term2 -> prPrec i 0 (concatD [prt 0 term1, doc (showString "|->"), prt 0 term2]) instance Print [Language.Rzk.Syntax.Abs.Restriction' a] where- prt _ [] = concatD []- prt _ [x] = concatD [prt 0 x]+ prt _ [] = concatD []+ prt _ [x] = concatD [prt 0 x] prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs] instance Print (Language.Rzk.Syntax.Abs.Term' a) where@@ -289,6 +291,6 @@ Language.Rzk.Syntax.Abs.ASCII_Second _ term -> prPrec i 6 (concatD [doc (showString "second"), prt 7 term]) instance Print [Language.Rzk.Syntax.Abs.Term' a] where- prt _ [] = concatD []- prt _ [x] = concatD [prt 0 x]+ prt _ [] = concatD []+ prt _ [x] = concatD [prt 0 x] prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]
src/Language/Rzk/VSCode/Handlers.hs view
@@ -8,10 +8,11 @@ import Control.Exception (SomeException, evaluate, try) import Control.Lens-import Control.Monad.Cont (MonadIO (liftIO), forM_)+import Control.Monad (forM_, when)+import Control.Monad.IO.Class (MonadIO (..)) import Data.Default.Class import Data.List (sort, (\\))-import Data.Maybe (fromMaybe)+import Data.Maybe (fromMaybe, isNothing) import qualified Data.Text as T import qualified Data.Yaml as Yaml import Language.LSP.Diagnostics (partitionBySource)@@ -32,7 +33,8 @@ import Language.Rzk.Syntax (Module, VarIdent' (VarIdent), parseModuleFile, printTree) import Language.Rzk.VSCode.Env-import Language.Rzk.VSCode.State (ProjectConfig (include))+import Language.Rzk.VSCode.Logging+import Rzk.Project.Config (ProjectConfig (include)) import Rzk.TypeCheck -- | Given a list of file paths, reads them and parses them as Rzk modules,@@ -66,18 +68,21 @@ typecheckFromConfigFile :: LSP () typecheckFromConfigFile = do+ logInfo "Looking for rzk.yaml" root <- getRootPath case root of Nothing -> do+ logWarning "Workspace has no root path, cannot find rzk.yaml" sendNotification SMethod_WindowShowMessage (ShowMessageParams MessageType_Warning "Cannot find the workspace root") Just rootPath -> do let rzkYamlPath = rootPath </> "rzk.yaml" eitherConfig <- liftIO $ Yaml.decodeFileEither @ProjectConfig rzkYamlPath case eitherConfig of Left err -> do- sendNotification SMethod_WindowShowMessage (ShowMessageParams MessageType_Warning (T.pack $ "Invalid or missing rzk.yaml: " ++ Yaml.prettyPrintParseException err))+ logError ("Invalid or missing rzk.yaml: " ++ Yaml.prettyPrintParseException err) Right config -> do+ logDebug "Starting typechecking" rawPaths <- liftIO $ globDir (map compile (include config)) rootPath let paths = concatMap sort rawPaths @@ -85,6 +90,9 @@ let cachedPaths = map fst cachedModules modifiedFiles = paths \\ cachedPaths + logDebug ("Found " ++ show (length cachedPaths) ++ " files in the cache")+ logDebug (show (length modifiedFiles) ++ " files have been modified")+ (parseErrors, parsedModules) <- liftIO $ collectErrors <$> parseFiles modifiedFiles tcResults <- liftIO $ try $ evaluate $ defaultTypeCheck (typecheckModulesWithLocationIncremental cachedModules parsedModules)@@ -94,11 +102,14 @@ Right (Left err) -> return ([err], []) -- sort of impossible Right (Right (checkedModules, errors)) -> do -- cache well-typed modules+ logInfo (show (length checkedModules) ++ " modules successfully typechecked")+ logInfo (show (length errors) ++ " errors found") cacheTypecheckedModules checkedModules return (errors, checkedModules) -- Reset all published diags -- TODO: remove this after properly grouping by path below, after which there can be an empty list of errors+ -- TODO: handle clearing diagnostics for files that got removed from the project (rzk.yaml) forM_ paths $ \path -> do publishDiagnostics 0 (filePathToNormalizedUri path) Nothing (partitionBySource []) @@ -161,9 +172,12 @@ provideCompletions :: Handler LSP 'Method_TextDocumentCompletion provideCompletions req res = do+ logInfo "Providing text completions" root <- getRootPath+ when (isNothing root) $ logDebug "Not in a workspace. Cannot find root path for relative paths" let rootDir = fromMaybe "/" root cachedModules <- getCachedTypecheckedModules+ logDebug ("Found " ++ show (length cachedModules) ++ " modules in the cache") let currentFile = fromMaybe "" $ uriToFilePath $ req ^. params . textDocument . uri -- Take all the modules up to and including the currently open one let modules = takeWhileInc ((/= currentFile) . fst) cachedModules@@ -174,6 +188,7 @@ | otherwise = [x] let items = concatMap (declsToItems rootDir) modules+ logDebug ("Sending " ++ show (length items) ++ " completion items") res $ Right $ InL items where declsToItems :: FilePath -> (FilePath, [Decl']) -> [CompletionItem]
+ src/Language/Rzk/VSCode/Logging.hs view
@@ -0,0 +1,20 @@+module Language.Rzk.VSCode.Logging where++import Colog.Core (Severity (..), WithSeverity (..), (<&))+import qualified Data.Text as T+import Language.LSP.Logging (defaultClientLogger)+import Language.LSP.Server (MonadLsp)+++logDebug :: MonadLsp c m => String -> m ()+logDebug msg = defaultClientLogger <& T.pack msg `WithSeverity` Debug++logInfo :: MonadLsp c m => String -> m ()+logInfo msg = defaultClientLogger <& T.pack msg `WithSeverity` Info++logWarning :: MonadLsp c m => String -> m ()+logWarning msg = defaultClientLogger <& T.pack msg `WithSeverity` Warning++-- | Error logs will also be shown to the user via `window/showMessage`+logError :: MonadLsp c m => String -> m ()+logError msg = defaultClientLogger <& T.pack msg `WithSeverity` Error
src/Language/Rzk/VSCode/Lsp.hs view
@@ -1,6 +1,5 @@ {-# LANGUAGE DuplicateRecordFields #-} {-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE TypeApplications #-} module Language.Rzk.VSCode.Lsp where @@ -20,6 +19,7 @@ import Language.Rzk.Syntax (parseModuleSafe) import Language.Rzk.VSCode.Env import Language.Rzk.VSCode.Handlers+import Language.Rzk.VSCode.Logging import Language.Rzk.VSCode.Tokenize (tokenizeModule) -- | The maximum number of diagnostic messages to send to the client@@ -39,12 +39,10 @@ , notificationHandler SMethod_WorkspaceDidChangeWatchedFiles $ \msg -> do let modifiedPaths = msg ^.. params . changes . traverse . uri . to uriToFilePath . _Just if any ("rzk.yaml" `isSuffixOf`) modifiedPaths- then resetCacheForAllFiles+ then do+ logDebug "rzk.yaml modified. Clearing module cache"+ resetCacheForAllFiles else resetCacheForFiles modifiedPaths- -- TODO: see what files changed and typecheck them again- -- Need to handle 3 events: added, changed, and deleted-- -- Currently, this is only sent for changes in `rzk.yaml`, so it makes sense to typecheck again (unconditionally) typecheckFromConfigFile , notificationHandler SMethod_TextDocumentDidSave $ \_msg -> do -- TODO: check if the file is included in the config's `include` list.@@ -67,9 +65,9 @@ Just sourceCode -> fmap (fmap tokenizeModule) $ liftIO $ parseModuleSafe (T.unpack sourceCode) case possibleTokens of- Left _err -> do+ Left err -> do -- Exception occurred when parsing the module- return ()+ logWarning ("Failed to tokenize file: " ++ err) Right tokens -> do let encoded = encodeTokens defaultSemanticTokensLegend $ relativizeTokens tokens case encoded of@@ -95,10 +93,12 @@ rzkEnv <- defaultRzkEnv runServer $ ServerDefinition- { onConfigurationChange = const $ pure $ Right (),- doInitialize = const . pure . Right,- staticHandlers = const handlers,- interpretHandler = \env -> Iso (flip runReaderT rzkEnv . runLspT env) liftIO,- options = defaultOptions { optTextDocumentSync = Just syncOptions },- defaultConfig = ()+ { configSection = "rzk"+ , parseConfig = const . pure+ , onConfigChange = const $ pure ()+ , doInitialize = const . pure . Right+ , staticHandlers = const handlers+ , interpretHandler = \env -> Iso (flip runReaderT rzkEnv . runLspT env) liftIO+ , options = defaultOptions { optTextDocumentSync = Just syncOptions }+ , defaultConfig = () }
− src/Language/Rzk/VSCode/State.hs
@@ -1,20 +0,0 @@-{-# LANGUAGE OverloadedStrings #-}--module Language.Rzk.VSCode.State where--import Data.Yaml (FromJSON (..), (.!=), (.:), (.:?))-import qualified Data.Yaml as Y--data ProjectConfig = ProjectConfig- { include :: [FilePath]- , exclude :: [FilePath]- } deriving (Eq, Show)--instance FromJSON ProjectConfig where- parseJSON (Y.Object v) =- ProjectConfig <$>- v .: "include" <*>- v .:? "exclude" .!= []- parseJSON _ = fail "Expected config value to be an object"---- TODO: Add a "ServerState" data structure for holding the typechecking cache
src/Language/Rzk/VSCode/Tokenize.hs view
@@ -6,7 +6,6 @@ SemanticTokenModifiers (..), SemanticTokenTypes (..)) import Language.Rzk.Syntax-import Language.Rzk.Syntax.Print tokenizeModule :: Module -> [SemanticTokenAbsolute] tokenizeModule (Module _loc langDecl commands) = concat
src/Rzk/Main.hs view
@@ -3,21 +3,28 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TypeApplications #-} module Rzk.Main where import Control.Monad (forM, void) import Data.List (sort) import Data.Version (showVersion)-#ifndef __GHCJS__++#ifdef LSP import Language.Rzk.VSCode.Lsp (runLsp) #endif++import qualified Data.Yaml as Yaml import Options.Generic+import System.Directory (doesPathExist) import System.Exit (exitFailure) import System.FilePath.Glob (glob) import qualified Language.Rzk.Syntax as Rzk import Paths_rzk (version)+import Rzk.Project.Config import Rzk.TypeCheck data Command@@ -41,10 +48,10 @@ Right _decls -> putStrLn "Everything is ok!" Lsp ->-#ifndef __GHCJS__+#ifdef LSP void runLsp #else- error "rzk lsp is not supported with a GHCJS build"+ error "rzk lsp is not supported with this build" #endif Version -> putStrLn (showVersion version)@@ -66,12 +73,29 @@ [] -> error ("File(s) not found at " <> path) paths -> return (sort paths) +extractFilesFromRzkYaml :: FilePath -> IO [FilePath]+extractFilesFromRzkYaml rzkYamlPath = do+ eitherConfig <- Yaml.decodeFileEither @ProjectConfig rzkYamlPath+ case eitherConfig of+ Left err -> do+ error ("Invalid or missing rzk.yaml: " ++ Yaml.prettyPrintParseException err)+ Right ProjectConfig{..} -> do+ return include+ parseRzkFilesOrStdin :: [FilePath] -> IO [(FilePath, Rzk.Module)] parseRzkFilesOrStdin = \case -- if no paths are given — read from stdin [] -> do- rzkModule <- parseStdin- return [("<stdin>", rzkModule)]+ let rzkYamlPath = "rzk.yaml"+ rzkYamlExists <- doesPathExist rzkYamlPath+ if rzkYamlExists+ then do+ putStrLn ("Using Rzk project stucture specified in " <> rzkYamlPath)+ paths <- extractFilesFromRzkYaml rzkYamlPath+ parseRzkFilesOrStdin paths+ else do+ rzkModule <- parseStdin+ return [("<stdin>", rzkModule)] -- otherwise — parse all given files in given order paths -> do expandedPaths <- foldMap globNonEmpty paths@@ -87,7 +111,7 @@ typecheckString :: String -> Either String String typecheckString moduleString = do rzkModule <- Rzk.parseModule moduleString- case defaultTypeCheck (typecheckModule Nothing rzkModule) of+ case defaultTypeCheck (typecheckModules [rzkModule]) of Left err -> Left $ unlines [ "An error occurred when typechecking!" , "Rendering type error... (this may take a few seconds)"
+ src/Rzk/Project/Config.hs view
@@ -0,0 +1,18 @@+{-# LANGUAGE OverloadedStrings #-}++module Rzk.Project.Config where++import Data.Yaml (FromJSON (..), (.!=), (.:), (.:?))+import qualified Data.Yaml as Y++data ProjectConfig = ProjectConfig+ { include :: [FilePath]+ , exclude :: [FilePath]+ } deriving (Eq, Show)++instance FromJSON ProjectConfig where+ parseJSON (Y.Object v) =+ ProjectConfig <$>+ v .: "include" <*>+ v .:? "exclude" .!= []+ parseJSON _ = fail "Expected config value to be an object"
src/Rzk/TypeCheck.hs view
@@ -10,6 +10,7 @@ module Rzk.TypeCheck where import Control.Applicative ((<|>))+import Control.Monad (forM, forM_, join, unless, when) import Control.Monad.Except import Control.Monad.Reader import Data.Bifunctor (first)@@ -88,12 +89,12 @@ [] -> return [] m : ms -> do (decls, errs) <- typecheckModule Nothing m- if null errs- then+ case errs of+ err : _ -> do+ throwError err+ _ -> do localDeclsPrepared decls $ (decls <>) <$> typecheckModules ms- else- return decls typecheckModuleWithLocation :: (FilePath, Rzk.Module) -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) typecheckModuleWithLocation (path, module_) = do@@ -1938,14 +1939,23 @@ switchVariance $ -- unifying in the negative position! unifyTerms cube cube' -- FIXME: unifyCubes enterScope orig' cube $ do- case (mtope, mtope') of- (Just tope, Just tope') -> do- topeNF <- nfT tope- topeNF' <- nfT tope'- unifyTopes topeNF topeNF'- (Nothing, Nothing) -> return ()- (Just tope, Nothing) -> nfT tope >>= (`unifyTopes` topeTopT)- (Nothing, Just tope) -> nfT tope >>= unifyTopes topeTopT+ case ret' of+ -- UniverseTopeT{} ->+ -- (Just tope, Just tope') -> do+ -- topeNF <- nfT tope+ -- topeNF' <- nfT tope'+ -- unifyTopes topeNF topeNF'+ -- (Nothing, Nothing) -> return ()+ -- (Just tope, Nothing) -> nfT tope >>= (`unifyTopes` topeTopT)+ -- (Nothing, Just tope) -> nfT tope >>= unifyTopes topeTopT+ _ -> case (mtope, mtope') of+ (Just tope, Just tope') -> do+ topeNF <- nfT tope+ topeNF' <- nfT tope'+ unifyTopes topeNF topeNF'+ (Nothing, Nothing) -> return ()+ (Just tope, Nothing) -> nfT tope >>= (`unifyTopes` topeTopT)+ (Nothing, Just tope) -> nfT tope >>= unifyTopes topeTopT case mterm of Nothing -> unifyTerms ret ret' Just term -> unifyTypes (appT ret' (S <$> term) (Pure Z)) ret ret'