rzk 0.7.5 → 0.7.6
raw patch · 9 files changed
+79/−43 lines, 9 filesdep ~Globdep ~QuickCheckdep ~base
Dependency ranges changed: Glob, QuickCheck, base, doctest, template-haskell
Files
- ChangeLog.md +8/−0
- grammar/Syntax.cf +3/−1
- rzk.cabal +18/−9
- src/Language/Rzk/Free/Syntax.hs +1/−0
- src/Language/Rzk/Syntax/Abs.hs +18/−19
- src/Language/Rzk/Syntax/Layout.hs +2/−2
- src/Language/Rzk/Syntax/Lex.x +4/−4
- src/Language/Rzk/Syntax/Par.y +21/−3
- src/Language/Rzk/Syntax/Print.hs +4/−5
ChangeLog.md view
@@ -6,6 +6,14 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.7.6 — 2025-08-14++Minor fixes:++- Support BNFC 2.9.6 (see [#201](https://github.com/rzk-lang/rzk/pull/201))+- Fix typo in the sHoTT link (see [#194](https://github.com/rzk-lang/rzk/pull/194))+- Fix tuple pattern syntax (see [#193](https://github.com/rzk-lang/rzk/pull/193) and [#191](https://github.com/rzk-lang/rzk/pull/191))+ ## v0.7.5 — 2024-08-18 Minor changes:
grammar/Syntax.cf view
@@ -60,8 +60,10 @@ PatternUnit. Pattern ::= "unit" ; PatternVar. Pattern ::= VarIdent ; PatternPair. Pattern ::= "(" Pattern "," Pattern ")" ;-PatternTuple. Pattern ::= "(" Pattern "," Pattern "," [Pattern] ")" ;+PatternTuple. Pattern ::= "(" Pattern "," Pattern "," [Pattern1] ")" ; separator nonempty Pattern "" ;+_. Pattern1 ::= Pattern ;+separator nonempty Pattern1 "," ; -- Parameter introduction (for lambda abstractions) ParamPattern. Param ::= Pattern ;
rzk.cabal view
@@ -1,11 +1,11 @@ cabal-version: 1.24 --- This file has been generated from package.yaml by hpack version 0.36.0.+-- This file has been generated from package.yaml by hpack version 0.38.0. -- -- see: https://github.com/sol/hpack name: rzk-version: 0.7.5+version: 0.7.6 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@@ -13,14 +13,15 @@ bug-reports: https://github.com/rzk-lang/rzk/issues author: Nikolai Kudasov maintainer: nickolay.kudasov@gmail.com-copyright: 2023-2024 Nikolai Kudasov+copyright: 2023-2025 Nikolai Kudasov license: BSD3 license-file: LICENSE build-type: Custom extra-source-files:+ grammar/Syntax.cf+extra-doc-files: README.md ChangeLog.md- grammar/Syntax.cf source-repository head type: git@@ -57,6 +58,8 @@ Paths_rzk hs-source-dirs: src+ default-extensions:+ DeriveDataTypeable ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path build-tools: alex >=3.2.4@@ -101,6 +104,8 @@ Paths_rzk hs-source-dirs: app+ default-extensions:+ DeriveDataTypeable ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N build-tools: alex >=3.2.4@@ -132,6 +137,8 @@ main-is: doctests.hs hs-source-dirs: test+ default-extensions:+ DeriveDataTypeable ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path build-tools: alex >=3.2.4@@ -139,16 +146,16 @@ build-tool-depends: BNFC:bnfc >=2.9.4.1 build-depends:- Glob- , QuickCheck+ Glob >=0.9.3+ , QuickCheck >=2.14 , array >=0.5.3.0- , base+ , base >=4.11.0.0 && <5.0 , bifunctors >=5.5.3 , bytestring >=0.10.8.2 , directory >=1.2.7.0- , doctest+ , doctest >=0.21.0 , mtl >=2.2.2- , template-haskell+ , template-haskell >=2.14.0.0 , text >=1.2.3.1 , yaml >=0.11.0.0 default-language: Haskell2010@@ -163,6 +170,8 @@ Paths_rzk hs-source-dirs: test+ default-extensions:+ DeriveDataTypeable ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N build-tools: alex >=3.2.4
src/Language/Rzk/Free/Syntax.hs view
@@ -341,6 +341,7 @@ Rzk.Unit loc -> Rzk.PatternUnit loc Rzk.Var loc x -> Rzk.PatternVar loc x Rzk.Pair loc l r -> Rzk.PatternPair loc (ttp l) (ttp r)+ Rzk.Tuple loc t1 t2 ts -> Rzk.PatternTuple loc (ttp t1) (ttp t2) (map ttp ts) term -> error ("ERROR: expected a pattern but got\n " ++ Rzk.printTree term) fromTerm' :: Term' -> Rzk.Term
src/Language/Rzk/Syntax/Abs.hs view
@@ -1,6 +1,5 @@--- File generated by the BNF Converter (bnfc 2.9.5).+-- File generated by the BNF Converter (bnfc 2.9.6). -{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleInstances #-}@@ -20,28 +19,28 @@ ) import qualified Data.String -import qualified Data.Data as C (Data, Typeable)+import qualified Data.Data as C (Data) import qualified GHC.Generics as C (Generic) type Module = Module' BNFC'Position data Module' a = Module a (LanguageDecl' a) [Command' a]- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic) type HoleIdent = HoleIdent' BNFC'Position data HoleIdent' a = HoleIdent a HoleIdentToken- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic) type VarIdent = VarIdent' BNFC'Position data VarIdent' a = VarIdent a VarIdentToken- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic) type LanguageDecl = LanguageDecl' BNFC'Position data LanguageDecl' a = LanguageDecl a (Language' a)- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic) type Language = Language' BNFC'Position data Language' a = Rzk1 a- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic) type Command = Command' BNFC'Position data Command' a@@ -56,16 +55,16 @@ | CommandSection a (SectionName' a) | CommandSectionEnd a (SectionName' a) | CommandDefine a (VarIdent' a) (DeclUsedVars' a) [Param' a] (Term' a) (Term' a)- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic) type DeclUsedVars = DeclUsedVars' BNFC'Position data DeclUsedVars' a = DeclUsedVars a [VarIdent' a]- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic) type SectionName = SectionName' BNFC'Position data SectionName' a = NoSectionName a | SomeSectionName a (VarIdent' a)- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic) type Pattern = Pattern' BNFC'Position data Pattern' a@@ -73,7 +72,7 @@ | PatternVar a (VarIdent' a) | PatternPair a (Pattern' a) (Pattern' a) | PatternTuple a (Pattern' a) (Pattern' a) [Pattern' a]- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic) type Param = Param' BNFC'Position data Param' a@@ -81,7 +80,7 @@ | ParamPatternType a [Pattern' a] (Term' a) | ParamPatternShape a [Pattern' a] (Term' a) (Term' a) | ParamPatternShapeDeprecated a (Pattern' a) (Term' a) (Term' a)- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic) type ParamDecl = ParamDecl' BNFC'Position data ParamDecl' a@@ -90,17 +89,17 @@ | ParamTermShape a (Term' a) (Term' a) (Term' a) | ParamTermTypeDeprecated a (Pattern' a) (Term' a) | ParamVarShapeDeprecated a (Pattern' a) (Term' a) (Term' a)- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic) type SigmaParam = SigmaParam' BNFC'Position data SigmaParam' a = SigmaParam a (Pattern' a) (Term' a)- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic) type Restriction = Restriction' BNFC'Position data Restriction' a = Restriction a (Term' a) (Term' a) | ASCII_Restriction a (Term' a) (Term' a)- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic) type Term = Term' BNFC'Position data Term' a@@ -160,7 +159,7 @@ | ASCII_TypeExtensionDeprecated a (ParamDecl' a) (Term' a) | ASCII_First a (Term' a) | ASCII_Second a (Term' a)- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Generic) commandPostulateNoParams :: a -> VarIdent' a -> DeclUsedVars' a -> Term' a -> Command' a commandPostulateNoParams = \ _a x vars ty -> CommandPostulate _a x vars [] ty@@ -196,10 +195,10 @@ unicode_TypeSigmaTupleAlt = \ _a par pars t -> TypeSigmaTuple _a par pars t newtype VarIdentToken = VarIdentToken String- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Generic, Data.String.IsString) newtype HoleIdentToken = HoleIdentToken String- deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString)+ deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Generic, Data.String.IsString) -- | Start position (line, column) of something.
src/Language/Rzk/Syntax/Layout.hs view
@@ -1,6 +1,6 @@--- File generated by the BNF Converter (bnfc 2.9.5).+-- File generated by the BNF Converter (bnfc 2.9.6). -{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}+{-# OPTIONS_GHC -Wno-incomplete-patterns #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PatternGuards #-}
src/Language/Rzk/Syntax/Lex.x view
@@ -1,8 +1,8 @@--- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.6). -- Lexer definition for use with Alex 3 {-{-# OPTIONS -fno-warn-incomplete-patterns #-}+{-# OPTIONS -Wno-incomplete-patterns #-} {-# OPTIONS_GHC -w #-} {-# LANGUAGE PatternSynonyms #-}@@ -19,8 +19,8 @@ -- 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+$c = [A-Z\192-\222] # [\215] -- capital isolatin1 letter (215 = \times)+$s = [a-z\223-\255] # [\247] -- small isolatin1 letter (247 = \div ) $l = [$c $s] -- letter $d = [0-9] -- digit $i = [$l $d _ '] -- identifier character
src/Language/Rzk/Syntax/Par.y view
@@ -1,8 +1,8 @@--- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.6). -- Parser definition for use with Happy {-{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}+{-# OPTIONS_GHC -Wno-incomplete-patterns -Wno-overlapping-patterns #-} {-# LANGUAGE PatternSynonyms #-} module Language.Rzk.Syntax.Par@@ -20,6 +20,8 @@ , pSectionName , pPattern , pListPattern+ , pPattern1+ , pListPattern1 , pParam , pListParam , pParamDecl@@ -57,6 +59,8 @@ %name pSectionName_internal SectionName %name pPattern_internal Pattern %name pListPattern_internal ListPattern+%name pPattern1_internal Pattern1+%name pListPattern1_internal ListPattern1 %name pParam_internal Param %name pListParam_internal ListParam %name pParamDecl_internal ParamDecl@@ -234,13 +238,21 @@ : '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)) }- | '(' Pattern ',' Pattern ',' ListPattern ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternTuple (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }+ | '(' Pattern ',' Pattern ',' ListPattern1 ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternTuple (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) } 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)) } +Pattern1 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Pattern) }+Pattern1 : Pattern { (fst $1, (snd $1)) }++ListPattern1 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Pattern]) }+ListPattern1+ : Pattern1 { (fst $1, (:[]) (snd $1)) }+ | Pattern1 ',' ListPattern1 { (fst $1, (:) (snd $1) (snd $3)) }+ 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)) }@@ -429,6 +441,12 @@ pListPattern :: [Token] -> Err [Language.Rzk.Syntax.Abs.Pattern] pListPattern = fmap snd . pListPattern_internal++pPattern1 :: [Token] -> Err Language.Rzk.Syntax.Abs.Pattern+pPattern1 = fmap snd . pPattern1_internal++pListPattern1 :: [Token] -> Err [Language.Rzk.Syntax.Abs.Pattern]+pListPattern1 = fmap snd . pListPattern1_internal pParam :: [Token] -> Err Language.Rzk.Syntax.Abs.Param pParam = fmap snd . pParam_internal
src/Language/Rzk/Syntax/Print.hs view
@@ -1,11 +1,8 @@--- File generated by the BNF Converter (bnfc 2.9.5).+-- File generated by the BNF Converter (bnfc 2.9.6). {-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE LambdaCase #-}-#if __GLASGOW_HASKELL__ <= 708-{-# LANGUAGE OverlappingInstances #-}-#endif -- | Pretty-printer for Language. @@ -198,10 +195,12 @@ Language.Rzk.Syntax.Abs.PatternUnit _ -> prPrec i 0 (concatD [doc (showString "unit")]) Language.Rzk.Syntax.Abs.PatternVar _ varident -> prPrec i 0 (concatD [prt 0 varident]) Language.Rzk.Syntax.Abs.PatternPair _ pattern_1 pattern_2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ")")])- Language.Rzk.Syntax.Abs.PatternTuple _ pattern_1 pattern_2 patterns -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ","), prt 0 patterns, doc (showString ")")])+ Language.Rzk.Syntax.Abs.PatternTuple _ pattern_1 pattern_2 patterns -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ","), prt 1 patterns, doc (showString ")")]) instance Print [Language.Rzk.Syntax.Abs.Pattern' a] where prt _ [] = concatD []+ prt 1 [x] = concatD [prt 1 x]+ prt 1 (x:xs) = concatD [prt 1 x, doc (showString ","), prt 1 xs] prt _ [x] = concatD [prt 0 x] prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]