diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -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 `Variable` command in Coq. 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.
diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -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
diff --git a/rzk.cabal b/rzk.cabal
--- a/rzk.cabal
+++ b/rzk.cabal
@@ -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
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
diff --git a/src/Language/Rzk/Syntax/Lex.x b/src/Language/Rzk/Syntax/Lex.x
deleted file mode 100644
--- a/src/Language/Rzk/Syntax/Lex.x
+++ /dev/null
@@ -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
- ]
-}
diff --git a/src/Language/Rzk/Syntax/Par.y b/src/Language/Rzk/Syntax/Par.y
deleted file mode 100644
--- a/src/Language/Rzk/Syntax/Par.y
+++ /dev/null
@@ -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
-}
-
diff --git a/src/Rzk/Main.hs b/src/Rzk/Main.hs
--- a/src/Rzk/Main.hs
+++ b/src/Rzk/Main.hs
@@ -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 [("", 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!"
-
diff --git a/src/Rzk/TypeCheck.hs b/src/Rzk/TypeCheck.hs
--- a/src/Rzk/TypeCheck.hs
+++ b/src/Rzk/TypeCheck.hs
@@ -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