Merge branch 'release-v0.7.6'

* release-v0.7.6:
  Bump version and update changelog
  Update from macos-12 to macos-13 and macos-latest runners
  Enable DeriveDataTypeable to work around a minor bug in BNFC 2.9.6 (fix #200)
  fix typo
  Fix tuple pattern syntax
  Fix tuple patterns in parameter declarations

Author: fizruk

.github/workflows/ghc.yml

@@ -36,7 +36,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [ubuntu-latest, windows-latest, macos-12]
+        os: [ubuntu-latest, windows-latest, macos-13, macos-latest]
 
     steps:
       - name: 📥 Checkout repository

.github/workflows/release.yml

@@ -33,7 +33,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [ubuntu-latest, windows-latest, macos-latest]
+        os: [ubuntu-latest, windows-latest, macos-13, macos-latest]
 
     steps:
       - name: 📥 Checkout repository

README.md

@@ -20,7 +20,7 @@ An experimental proof assistant for synthetic ∞-categories.
 
 ## About this project
 
-This project has started with the idea of bringing Riehl and Shulman's 2017 paper [1] to "life" by implementing a proof assistant based on their type theory with shapes. Currently an early prototype with an [online playground](https://rzk-lang.github.io/rzk/develop/playground/) is available. The current implementation is capable of checking various formalisations. Perhaps, the largest formalisations are available in two related projects: <https://rzk-lang.github.com/sHoTT> and <https://github.com/emilyriehl/yoneda>. `sHoTT` project (originally a fork of the yoneda project) aims to cover more formalisations in simplicial HoTT and ∞-categories, while `yoneda` project aims to compare different formalisations of the Yoneda lemma.
+This project has started with the idea of bringing Riehl and Shulman's 2017 paper [1] to "life" by implementing a proof assistant based on their type theory with shapes. Currently an early prototype with an [online playground](https://rzk-lang.github.io/rzk/develop/playground/) is available. The current implementation is capable of checking various formalisations. Perhaps, the largest formalisations are available in two related projects: <https://rzk-lang.github.io/sHoTT> and <https://github.com/emilyriehl/yoneda>. `sHoTT` project (originally a fork of the yoneda project) aims to cover more formalisations in simplicial HoTT and ∞-categories, while `yoneda` project aims to compare different formalisations of the Yoneda lemma.
 
 Internally, `rzk` uses a version of second-order abstract syntax allowing relatively straightforward handling of binders (such as lambda abstraction). In the future, `rzk` aims to support dependent type inference relying on E-unification for second-order abstract syntax [2].
 Using such representation is motivated by automatic handling of binders and easily automated boilerplate code. The idea is that this should keep the implementation of `rzk` relatively small and less error-prone than some of the existing approaches to implementation of dependent type checkers.

rzk/ChangeLog.md

@@ -6,6 +6,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 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:

rzk/grammar/Syntax.cf

@@ -60,8 +60,10 @@ SomeSectionName.  SectionName ::= VarIdent ;
 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/package.yaml

@@ -1,5 +1,5 @@
 name: rzk
-version: 0.7.5
+version: 0.7.6
 github: "rzk-lang/rzk"
 license: BSD3
 author: "Nikolai Kudasov"
@@ -64,6 +64,7 @@ ghc-options:
   - -Wpartial-fields
   - -Wredundant-constraints
   - -optP-Wno-nonportable-include-path
+  - -XDeriveDataTypeable
 
 library:
   source-dirs: src

rzk/rzk.cabal

@@ -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.37.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
@@ -57,7 +57,7 @@ library
       Paths_rzk
   hs-source-dirs:
       src
-  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -XDeriveDataTypeable
   build-tools:
       alex >=3.2.4
     , happy >=1.19.9
@@ -101,7 +101,7 @@ executable rzk
       Paths_rzk
   hs-source-dirs:
       app
-  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
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -XDeriveDataTypeable -threaded -rtsopts -with-rtsopts=-N
   build-tools:
       alex >=3.2.4
     , happy >=1.19.9
@@ -132,7 +132,7 @@ test-suite doctests
   main-is: doctests.hs
   hs-source-dirs:
       test
-  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -XDeriveDataTypeable
   build-tools:
       alex >=3.2.4
     , happy >=1.19.9
@@ -163,7 +163,7 @@ test-suite rzk-test
       Paths_rzk
   hs-source-dirs:
       test
-  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
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -XDeriveDataTypeable -threaded -rtsopts -with-rtsopts=-N
   build-tools:
       alex >=3.2.4
     , happy >=1.19.9

rzk/src/Language/Rzk/Free/Syntax.hs

@@ -341,6 +341,7 @@ unsafeTermToPattern = ttp
       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