Update to GHC 9.6, latest Stackage Nightly, and use BNFC in setup

rzk-lang · Oct 1, 2023 · 85be97b · 85be97b
1 parent 554984e
commit 85be97b
Show file tree

Hide file tree

Showing 20 changed files with 201 additions and 112 deletions.
diff --git a/rzk/Setup.hs b/rzk/Setup.hs
@@ -1,2 +1,29 @@
-import Distribution.Simple
-main = defaultMain
+-- Source: https://github.com/haskell/cabal/issues/6726#issuecomment-918663262
+
+-- | Custom Setup that runs bnfc to generate the language sub-libraries
+-- for the parsers included in Ogma.
+module Main (main) where
+
+import           Distribution.Simple         (defaultMainWithHooks,
+                                              hookedPrograms, postConf,
+                                              preBuild, simpleUserHooks)
+import           Distribution.Simple.Program (Program (..), findProgramVersion,
+                                              simpleProgram)
+import           System.Process              (system)
+
+-- | Run BNFC on the grammar before the actual build step.
+--
+-- All options for bnfc are hard-coded here.
+main :: IO ()
+main = defaultMainWithHooks $ simpleUserHooks
+  { hookedPrograms = [ bnfcProgram ]
+  , postConf       = \args flags packageDesc localBuildInfo -> do
+      _ <- system "bnfc -d -p Language.Rzk --generic --functor -o src/ grammar/Syntax.cf"
+      postConf simpleUserHooks args flags packageDesc localBuildInfo
+  }
+
+-- | TODO: This should be in Cabal.Distribution.Simple.Program.Builtin.
+bnfcProgram :: Program
+bnfcProgram = (simpleProgram "bnfc")
+  { programFindVersion = findProgramVersion "--version" id
+  }
diff --git a/rzk/src/Language/Rzk/Syntax.cf → rzk/grammar/Syntax.cf b/rzk/src/Language/Rzk/Syntax.cf → rzk/grammar/Syntax.cf
@@ -73,7 +73,7 @@ separator nonempty Param "" ;
 ParamType.          ParamDecl ::= Term6 ;
 ParamTermType.      ParamDecl ::= "(" Term ":" Term ")" ;
 ParamTermShape.     ParamDecl ::= "(" Term ":" Term "|" Term ")" ;
-ParamTermTypeDeprecated. ParamDecl ::= "{" Pattern ":" Term "}" ; 
+ParamTermTypeDeprecated. ParamDecl ::= "{" Pattern ":" Term "}" ;
 ParamVarShapeDeprecated. ParamDecl ::= "{" "(" Pattern ":" Term ")" "|" Term "}" ;
 paramVarShapeDeprecated. ParamDecl ::= "{" Pattern ":" Term "|" Term "}" ;
 define paramVarShapeDeprecated pat cube tope = ParamVarShapeDeprecated pat cube tope ;
@@ -161,4 +161,4 @@ ASCII_Second.         Term6 ::= "second" Term7 ;
 -- Alternative Unicode syntax rules
 
 unicode_TypeSigmaAlt.   Term1 ::= "∑" "(" Pattern ":" Term ")" "," Term1 ;    -- \sum
-define unicode_TypeSigmaAlt pat fst snd = TypeSigma pat fst snd ;
+define unicode_TypeSigmaAlt pat fst snd = TypeSigma pat fst snd ;
diff --git a/rzk/package.yaml b/rzk/package.yaml
@@ -9,6 +9,7 @@ copyright: '2023 Nikolai Kudasov'
 extra-source-files:
   - README.md
   - ChangeLog.md
+  - grammar/Syntax.cf
 
 synopsis: An experimental proof assistant for synthetic ∞-categories
 category: Dependent Types # same as Agda
@@ -25,9 +26,16 @@ flags:
     manual: true
     default: true
 
+custom-setup:
+  dependencies:
+    base:    ">= 4.11.0.0"
+    Cabal:   ">= 2.4.0.1"
+    process: ">= 1.6.3.0"
+
 build-tools:
   alex:   ">= 3.2.4"
   happy:  ">= 1.19.9"
+  BNFC:   ">= 2.9.4.1"
 
 dependencies:
   array: ">= 0.5.3.0"
@@ -73,8 +81,8 @@ library:
         data-default-class: ">= 0.1.2.0"
         filepath: ">= 1.4.2.1"
         lens: ">= 4.17"
-        lsp: ">= 2.1.0.0"
-        lsp-types: ">= 2.0.1.0"
+        lsp: ">= 2.2.0.0"
+        lsp-types: ">= 2.0.2.0"
         stm: ">= 2.5.0.0"
         yaml: ">= 0.11.0.0"
       cpp-options: -DLSP

diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal
@@ -1,6 +1,6 @@
-cabal-version: 1.12
+cabal-version: 1.24
 
--- This file has been generated from package.yaml by hpack version 0.35.2.
+-- This file has been generated from package.yaml by hpack version 0.36.0.
 --
 -- see: https://github.com/sol/hpack
 
@@ -16,15 +16,22 @@ maintainer:     nickolay.kudasov@gmail.com
 copyright:      2023 Nikolai Kudasov
 license:        BSD3
 license-file:   LICENSE
-build-type:     Simple
+build-type:     Custom
 extra-source-files:
     README.md
     ChangeLog.md
+    grammar/Syntax.cf
 
 source-repository head
   type: git
   location: https://github.com/rzk-lang/rzk
 
+custom-setup
+  setup-depends:
+      Cabal >=2.4.0.1
+    , base >=4.11.0.0
+    , process >=1.6.3.0
+
 flag lsp
   description: Build with LSP support (only available with GHC, not GHCJS).
   manual: True
@@ -52,6 +59,8 @@ library
   build-tools:
       alex >=3.2.4
     , happy >=1.19.9
+  build-tool-depends:
+      BNFC:BNFC >=2.9.4.1
   build-depends:
       Glob >=0.9.3
     , array >=0.5.3.0
@@ -78,8 +87,8 @@ library
       , data-default-class >=0.1.2.0
       , filepath >=1.4.2.1
       , lens >=4.17
-      , lsp >=2.1.0.0
-      , lsp-types >=2.0.1.0
+      , lsp >=2.2.0.0
+      , lsp-types >=2.0.2.0
       , stm >=2.5.0.0
       , yaml >=0.11.0.0
 
@@ -93,6 +102,8 @@ executable rzk
   build-tools:
       alex >=3.2.4
     , happy >=1.19.9
+  build-tool-depends:
+      BNFC:BNFC >=2.9.4.1
   build-depends:
       Glob >=0.9.3
     , array >=0.5.3.0
@@ -118,6 +129,8 @@ test-suite doctests
   build-tools:
       alex >=3.2.4
     , happy >=1.19.9
+  build-tool-depends:
+      BNFC:BNFC >=2.9.4.1
   build-depends:
       Glob
     , QuickCheck
@@ -143,6 +156,8 @@ test-suite rzk-test
   build-tools:
       alex >=3.2.4
     , happy >=1.19.9
+  build-tool-depends:
+      BNFC:BNFC >=2.9.4.1
   build-depends:
       Glob >=0.9.3
     , array >=0.5.3.0

diff --git a/rzk/src/Language/Rzk/Free/Syntax.hs b/rzk/src/Language/Rzk/Free/Syntax.hs
@@ -94,7 +94,7 @@ data TermF scope term
     | TypeUnitF
     | TypeAscF term term
     | TypeRestrictedF term [(term, term)]
-    deriving (Eq, Functor)
+    deriving (Eq, Functor, Foldable, Traversable)
 deriveBifunctor ''TermF
 deriveBifoldable ''TermF
 deriveBitraversable ''TermF

diff --git a/rzk/src/Language/Rzk/Syntax/Abs.hs b/rzk/src/Language/Rzk/Syntax/Abs.hs
@@ -1,4 +1,4 @@
--- File generated by the BNF Converter (bnfc 2.9.4.1).
+-- File generated by the BNF Converter (bnfc 2.9.5).
 
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}

diff --git a/rzk/src/Language/Rzk/Syntax/Doc.txt b/rzk/src/Language/Rzk/Syntax/Doc.txt
@@ -183,4 +183,4 @@ All other symbols are terminals.
 
 
 
-%% File generated by the BNF Converter (bnfc 2.9.4.1).
+%% File generated by the BNF Converter (bnfc 2.9.5).

diff --git a/rzk/src/Language/Rzk/Syntax/ErrM.hs b/rzk/src/Language/Rzk/Syntax/ErrM.hs
@@ -1,4 +1,4 @@
--- File generated by the BNF Converter (bnfc 2.9.4.1).
+-- File generated by the BNF Converter (bnfc 2.9.5).
 
 {-# LANGUAGE CPP #-}
 

diff --git a/rzk/src/Language/Rzk/Syntax/Layout.hs b/rzk/src/Language/Rzk/Syntax/Layout.hs
@@ -1,4 +1,4 @@
--- File generated by the BNF Converter (bnfc 2.9.4.1).
+-- File generated by the BNF Converter (bnfc 2.9.5).
 
 {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
 

diff --git a/rzk/src/Language/Rzk/Syntax/Lex.x b/rzk/src/Language/Rzk/Syntax/Lex.x
@@ -1,4 +1,4 @@
--- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.4.1).
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).
 
 -- Lexer definition for use with Alex 3
 {

diff --git a/rzk/src/Language/Rzk/Syntax/Par.y b/rzk/src/Language/Rzk/Syntax/Par.y
@@ -1,4 +1,4 @@
--- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.4.1).
+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.5).
 
 -- Parser definition for use with Happy
 {

diff --git a/rzk/src/Language/Rzk/Syntax/Print.hs b/rzk/src/Language/Rzk/Syntax/Print.hs
@@ -1,8 +1,8 @@
--- File generated by the BNF Converter (bnfc 2.9.4.1).
+-- File generated by the BNF Converter (bnfc 2.9.5).
 
-{-# LANGUAGE CPP                  #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE LambdaCase           #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
 #if __GLASGOW_HASKELL__ <= 708
 {-# LANGUAGE OverlappingInstances #-}
 #endif
@@ -11,13 +11,16 @@
 
 module Language.Rzk.Syntax.Print where
 
-import           Data.Char               (Char, isSpace)
+import Prelude
+  ( ($), (.)
+  , Bool(..), (==), (<)
+  , Int, Integer, Double, (+), (-), (*)
+  , String, (++)
+  , ShowS, showChar, showString
+  , all, elem, foldr, id, map, null, replicate, shows, span
+  )
+import Data.Char ( Char, isSpace )
 import qualified Language.Rzk.Syntax.Abs
-import           Prelude                 (Bool (..), Double, Int, Integer,
-                                          ShowS, String, all, elem, foldr, id,
-                                          map, null, replicate, showChar,
-                                          showString, shows, span, ($), (*),
-                                          (++), (.), (<), (==))
 
 -- | The top-level printing method.
 
@@ -40,9 +43,9 @@ render d = rend 0 False (map ($ "") $ d []) ""
   rend i p = \case
       "["      :ts -> char '[' . rend i False ts
       "("      :ts -> char '(' . rend i False ts
-      -- "{"      :ts -> onNewLine i     p . showChar   '{'  . new (i+1) ts
-      -- "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
-      -- "}"      :ts -> onNewLine (i-1) p . showChar   '}'  . new (i-1) ts
+      "{"      :ts -> onNewLine i     p . showChar   '{'  . new (i+1) ts
+      "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts
+      "}"      :ts -> onNewLine (i-1) p . showChar   '}'  . new (i-1) ts
       [";"]        -> char ';'
       ";"      :ts -> char ';' . new i ts
       t  : ts@(s:_) | closingOrPunctuation s
@@ -67,19 +70,18 @@ render d = rend 0 False (map ($ "") $ d []) ""
   new j ts = showChar '\n' . rend j True ts
 
   -- Make sure we are on a fresh line.
-  -- onNewLine :: Int -> Bool -> ShowS
-  -- onNewLine i p = (if p then id else showChar '\n') . indent i
+  onNewLine :: Int -> Bool -> ShowS
+  onNewLine i p = (if p then id else showChar '\n') . indent i
 
   -- Separate given string from following text by a space (if needed).
   space :: String -> ShowS
   space t s =
-    case (all isSpace t', null spc, null rest) of
-      (True , _   , True ) -> []              -- remove trailing space
-      (False, _   , True ) -> t'              -- remove trailing space
-      (False, True, False) -> t' ++ ' ' : s   -- add space if none
-      _                    -> t' ++ s
+    case (all isSpace t, null spc, null rest) of
+      (True , _   , True ) -> []             -- remove trailing space
+      (False, _   , True ) -> t              -- remove trailing space
+      (False, True, False) -> t ++ ' ' : s   -- add space if none
+      _                    -> t ++ s
     where
-      t'          = showString t []
       (spc, rest) = span isSpace s
 
   closingOrPunctuation :: String -> Bool
@@ -121,10 +123,10 @@ printString s = doc (showChar '"' . concatS (map (mkEsc '"') s) . showChar '"')
 mkEsc :: Char -> Char -> ShowS
 mkEsc q = \case
   s | s == q -> showChar '\\' . showChar s
-  '\\'       -> showString "\\\\"
-  '\n'       -> showString "\\n"
-  '\t'       -> showString "\\t"
-  s          -> showChar s
+  '\\' -> showString "\\\\"
+  '\n' -> showString "\\n"
+  '\t' -> showString "\\t"
+  s -> showChar s
 
 prPrec :: Int -> Int -> Doc -> Doc
 prPrec i j = if j < i then parenth else id
@@ -152,8 +154,8 @@ instance Print (Language.Rzk.Syntax.Abs.VarIdent' a) where
     Language.Rzk.Syntax.Abs.VarIdent _ varidenttoken -> prPrec i 0 (concatD [prt 0 varidenttoken])
 
 instance Print [Language.Rzk.Syntax.Abs.VarIdent' a] where
-  prt _ []     = concatD []
-  prt _ [x]    = concatD [prt 0 x]
+  prt _ [] = concatD []
+  prt _ [x] = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]
 
 instance Print (Language.Rzk.Syntax.Abs.LanguageDecl' a) where
@@ -179,7 +181,7 @@ instance Print (Language.Rzk.Syntax.Abs.Command' a) where
     Language.Rzk.Syntax.Abs.CommandDefine _ varident declusedvars params term1 term2 -> prPrec i 0 (concatD [doc (showString "#define"), prt 0 varident, prt 0 declusedvars, prt 0 params, doc (showString ":"), prt 0 term1, doc (showString ":="), prt 0 term2])
 
 instance Print [Language.Rzk.Syntax.Abs.Command' a] where
-  prt _ []     = concatD []
+  prt _ [] = concatD []
   prt _ (x:xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs]
 
 instance Print (Language.Rzk.Syntax.Abs.DeclUsedVars' a) where
@@ -198,8 +200,8 @@ instance Print (Language.Rzk.Syntax.Abs.Pattern' a) where
     Language.Rzk.Syntax.Abs.PatternPair _ pattern_1 pattern_2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ")")])
 
 instance Print [Language.Rzk.Syntax.Abs.Pattern' a] where
-  prt _ []     = concatD []
-  prt _ [x]    = concatD [prt 0 x]
+  prt _ [] = concatD []
+  prt _ [x] = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]
 
 instance Print (Language.Rzk.Syntax.Abs.Param' a) where
@@ -210,8 +212,8 @@ instance Print (Language.Rzk.Syntax.Abs.Param' a) where
     Language.Rzk.Syntax.Abs.ParamPatternShapeDeprecated _ pattern_ term1 term2 -> prPrec i 0 (concatD [doc (showString "{"), prt 0 pattern_, doc (showString ":"), prt 0 term1, doc (showString "|"), prt 0 term2, doc (showString "}")])
 
 instance Print [Language.Rzk.Syntax.Abs.Param' a] where
-  prt _ []     = concatD []
-  prt _ [x]    = concatD [prt 0 x]
+  prt _ [] = concatD []
+  prt _ [x] = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, prt 0 xs]
 
 instance Print (Language.Rzk.Syntax.Abs.ParamDecl' a) where
@@ -228,8 +230,8 @@ instance Print (Language.Rzk.Syntax.Abs.Restriction' a) where
     Language.Rzk.Syntax.Abs.ASCII_Restriction _ term1 term2 -> prPrec i 0 (concatD [prt 0 term1, doc (showString "|->"), prt 0 term2])
 
 instance Print [Language.Rzk.Syntax.Abs.Restriction' a] where
-  prt _ []     = concatD []
-  prt _ [x]    = concatD [prt 0 x]
+  prt _ [] = concatD []
+  prt _ [x] = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]
 
 instance Print (Language.Rzk.Syntax.Abs.Term' a) where
@@ -289,6 +291,6 @@ instance Print (Language.Rzk.Syntax.Abs.Term' a) where
     Language.Rzk.Syntax.Abs.ASCII_Second _ term -> prPrec i 6 (concatD [doc (showString "second"), prt 7 term])
 
 instance Print [Language.Rzk.Syntax.Abs.Term' a] where
-  prt _ []     = concatD []
-  prt _ [x]    = concatD [prt 0 x]
+  prt _ [] = concatD []
+  prt _ [x] = concatD [prt 0 x]
   prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]
diff --git a/rzk/src/Language/Rzk/Syntax/Skel.hs b/rzk/src/Language/Rzk/Syntax/Skel.hs
@@ -1,4 +1,4 @@
--- File generated by the BNF Converter (bnfc 2.9.4.1).
+-- File generated by the BNF Converter (bnfc 2.9.5).
 
 -- Templates for pattern matching on abstract syntax