rzk 0.5.4 → 0.5.5
raw patch · 7 files changed
+83/−777 lines, 7 filesdep +with-utf8
Dependencies added: with-utf8
Files
- ChangeLog.md +19/−9
- app/Main.hs +9/−1
- rzk.cabal +23/−5
- src/Language/Rzk/Syntax/Lex.x +0/−292
- src/Language/Rzk/Syntax/Par.y +0/−456
- src/Rzk/Main.hs +19/−9
- src/Rzk/TypeCheck.hs +13/−5
ChangeLog.md view
@@ -6,14 +6,24 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). -## v0.5.4 — 2022-08-19+## v0.5.5 — 2023-09-19 +This version contains Unicode and tope logic-related fixes:++1. Fix (add missing checks) for subshapes (see [#85](https://github.com/rzk-lang/rzk/pull/85));+2. Allow to handle wildcards in `rzk` itself (see [#83](https://github.com/rzk-lang/rzk/pull/83));+3. Fix Unicode on machines with non-standard locales (see [#82](https://github.com/rzk-lang/rzk/pull/82));+4. Specify `happy` and `alex` as build tools to fix cabal build from Hackage (see [#80](https://github.com/rzk-lang/rzk/pull/80)).+5. Add configuration for MkDocs plugin for Rzk (see [#79](https://github.com/rzk-lang/rzk/pull/79)).++## v0.5.4 — 2023-08-19+ This version contains minor improvements: 1. Improve typechecking by trying an easier unification strategy first (see [#76](https://github.com/rzk-lang/rzk/pull/76)); 2. Update GitHub Action for Nix (see [#74](https://github.com/rzk-lang/rzk/pull/74)). -## v0.5.3 — 2022-07-12+## v0.5.3 — 2023-07-12 This version contains a few minor improvements: @@ -24,7 +34,7 @@ 5. Migrate from `fizruk` to `rzk-lang` organisation on GitHub (see [`ee0d063`](https://github.com/rzk-lang/rzk/commit/ee0d0638283232c99003a83fdf41eb109ae78983)); 6. Speed up GHCJS build with Nix (see [#66](https://github.com/rzk-lang/rzk/pull/66)); -## v0.5.2 — 2022-07-05+## v0.5.2 — 2023-07-05 This version introduces support for Unicode syntax, better recognition of Markdown code blocks and improves documentation a bit: @@ -34,7 +44,7 @@ - Factor out Pygments highlighting to https://github.com/rzk-lang/pygments-rzk; - Use new cache action for Nix (see [#60](https://github.com/rzk-lang/rzk/pull/60)). -## v0.5.1 — 2022-06-29+## v0.5.1 — 2023-06-29 This version fixes `Unit` type and makes some changes to documentation: @@ -45,7 +55,7 @@ - Switch to Material theme for MkDocs (see [#57](https://github.com/rzk-lang/rzk/pull/57)); - Fix links to `*.rzk.md` in `mkdocs.yml` (see [8ba1c55b](https://github.com/rzk-lang/rzk/commit/8ba1c55b)); -## v0.5 — 2022-06-20+## v0.5 — 2023-06-20 This version contains the following changes: @@ -53,7 +63,7 @@ - Add basic tokenizer support via `rzk tokenize` (see [#53](https://github.com/rzk-lang/rzk/pull/53)); - Add location information for shadowing warnings and duplicate definition errors (see [bf9d6cd9](https://github.com/rzk-lang/rzk/commit/bf9d6cd9)). -## v0.4.1 — 2022-06-16+## v0.4.1 — 2023-06-16 This is version contains minor changes, primarily in tools around rzk: @@ -64,7 +74,7 @@ - Add Pygments highlighting (see [01c2a017](https://github.com/rzk-lang/rzk/commit/01c2a017), [cbd656cc](https://github.com/rzk-lang/rzk/commit/cbd656cc), [5220ddf9](https://github.com/rzk-lang/rzk/commit/5220ddf9), [142ec003](https://github.com/rzk-lang/rzk/commit/142ec003), [5c7425f2](https://github.com/rzk-lang/rzk/commit/5c7425f2)); - Update HighlightJS config for rzk v0.4.0 (see [171ee63f](https://github.com/rzk-lang/rzk/commit/171ee63f)); -## v0.4.0 — 2022-05-18+## v0.4.0 — 2023-05-18 This version introduces sections and variables. The feature is similar to <a href="https://coq.inria.fr/refman/language/core/assumptions.html#coq:cmd.Variable" target="_blank">`Variable` command in Coq</a>. An important difference, however, is that `rzk` does not allow definitions to use variables implicitly and adds `uses (...)` annotations to ensure such dependencies are not accidental. @@ -75,7 +85,7 @@ - Add flake, set up nix and cabal builds, cache nix store on CI (see [#39](https://github.com/rzk-lang/rzk/pull/39)); - Apply stylish-haskell (see [7d42ef62](https://github.com/rzk-lang/rzk/commit/7d42ef62)); -## v0.3.0 — 2022-04-28+## v0.3.0 — 2023-04-28 This version introduces an experimental feature for generating visualisations for simplicial terms in SVG. To enable rendering, enable option `"render" = "svg"` (to disable, `"render" = "none"`):@@ -94,7 +104,7 @@ - Fixed an issue with tope solver when context was empty (see 6196af9e); - Fixed #33 (missing coherence check for restricted types). -## v0.2.0 - 2022-04-20+## v0.2.0 - 2023-04-20 This version was a complete rewrite of the proof assistant, using a new parser, a new internal representation, and a rewrite of the typechecking logic. This is still a prototype, but, arguably, significantly more stable and manageable than version 0.1.0.
app/Main.hs view
@@ -1,6 +1,14 @@+{-# LANGUAGE CPP #-} module Main (main) where +#ifndef __GHCJS__+import Main.Utf8 (withUtf8)+#endif import qualified Rzk.Main main :: IO ()-main = Rzk.Main.main+main =+#ifndef __GHCJS__+ withUtf8+#endif+ Rzk.Main.main
rzk.cabal view
@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.35.1.+-- This file has been generated from package.yaml by hpack version 0.35.2. -- -- see: https://github.com/sol/hpack name: rzk-version: 0.5.4+version: 0.5.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@@ -46,8 +46,12 @@ hs-source-dirs: src ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints+ build-tools:+ alex+ , happy build-depends:- aeson+ Glob+ , aeson , array , base >=4.7 && <5 , bifunctors@@ -65,8 +69,12 @@ hs-source-dirs: app ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+ build-tools:+ alex+ , happy build-depends:- aeson+ Glob+ , aeson , array , base >=4.7 && <5 , bifunctors@@ -77,6 +85,9 @@ , template-haskell , text default-language: Haskell2010+ if !impl(ghcjs)+ build-depends:+ with-utf8 test-suite doctests type: exitcode-stdio-1.0@@ -84,6 +95,9 @@ hs-source-dirs: test ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints+ build-tools:+ alex+ , happy build-depends: Glob , QuickCheck@@ -107,8 +121,12 @@ hs-source-dirs: test ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+ build-tools:+ alex+ , happy build-depends:- aeson+ Glob+ , aeson , array , base >=4.7 && <5 , bifunctors
− src/Language/Rzk/Syntax/Lex.x
@@ -1,292 +0,0 @@--- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.4.1).---- 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
@@ -1,456 +0,0 @@--- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.4.1).---- 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 ';' ListCommand '#end' 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) (snd $4) (snd $6)) }- | '#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/Rzk/Main.hs view
@@ -10,6 +10,7 @@ import Data.Version (showVersion) import Options.Generic import System.Exit (exitFailure)+import System.FilePath.Glob (glob) import qualified Language.Rzk.Syntax as Rzk import Language.Rzk.VSCode.Tokenize (tokenizeModule)@@ -51,6 +52,14 @@ error err Right rzkModule -> return rzkModule +-- | Finds matches to the given pattern in the current working directory.+-- **NOTE:** throws exception when 'glob' returns an empty list.+globNonEmpty :: FilePath -> IO [FilePath]+globNonEmpty path = do+ glob path >>= \case+ [] -> error ("File(s) not found at " <> path)+ paths -> return paths+ parseRzkFilesOrStdin :: [FilePath] -> IO [(FilePath, Rzk.Module)] parseRzkFilesOrStdin = \case -- if no paths are given — read from stdin@@ -58,14 +67,16 @@ rzkModule <- parseStdin return [("<stdin>", rzkModule)] -- otherwise — parse all given files in given order- paths -> forM paths $ \path -> do- putStrLn ("Loading file " <> path)- result <- Rzk.parseModule <$> readFile path- case result of- Left err -> do- putStrLn ("An error occurred when parsing file " <> path)- error err- Right rzkModule -> return (path, rzkModule)+ paths -> do+ expandedPaths <- foldMap globNonEmpty paths+ forM (reverse expandedPaths) $ \path -> do+ putStrLn ("Loading file " <> path)+ result <- Rzk.parseModule <$> readFile path+ case result of+ Left err -> do+ putStrLn ("An error occurred when parsing file " <> path)+ error err+ Right rzkModule -> return (path, rzkModule) typecheckString :: String -> Either String String typecheckString moduleString = do@@ -80,4 +91,3 @@ ] ] Right _ -> pure "Everything is ok!"-
src/Rzk/TypeCheck.hs view
@@ -2361,13 +2361,15 @@ b' <- enterScope orig a' $ inferAs universeT b return (typeFunT orig a' Nothing b') -- an argument can be a shape- TypeFunT _ty _orig cube _mtope UniverseTopeT{} -> do+ TypeFunT _ty _orig cube mtope UniverseTopeT{} -> do mapM_ checkNameShadowing orig enterScope orig cube $ do let tope' = appT topeT (S <$> a') (Pure Z) -- eta expand a' localTope tope' $ do b' <- inferAs universeT b- return (typeFunT orig cube (Just tope') b')+ case mtope of+ Nothing -> return (typeFunT orig cube (Just tope') b')+ Just tope'' -> return (typeFunT orig cube (Just (topeAndT tope'' tope')) b') ty -> issueTypeError $ TypeErrorInvalidArgumentType a ty TypeFun orig cube (Just tope) ret -> do@@ -2403,10 +2405,16 @@ RecBottomT{} -> pure recBottomT -- FIXME: is this ok? TypeFunT _ty _orig a mtope b -> do x' <- typecheck x a+ let result = appT (substituteT x' b) f' x' case b of- UniverseTopeT{} -> return ()- _ -> mapM_ (contextEntails . substituteT x') mtope -- FIXME: need to check?- return (appT (substituteT x' b) f' x')+ UniverseTopeT{} -> do+ case mtope of+ Nothing -> return result+ Just tope -> do+ return (topeAndT (substituteT x' tope) result)+ _ -> do+ mapM_ (contextEntails . substituteT x') mtope -- FIXME: need to check?+ return result ty -> issueTypeError $ TypeErrorNotFunction f' ty Lambda _orig Nothing _body -> do