From 04d31c93b39b222e730816af89bcfac3efa23f96 Mon Sep 17 00:00:00 2001 From: Abdelrahman Abounegm Date: Fri, 15 Dec 2023 15:49:56 +0300 Subject: [PATCH 1/9] Add a couple of logs for errors while typechecking --- rzk/src/Language/Rzk/VSCode/Handlers.hs | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/rzk/src/Language/Rzk/VSCode/Handlers.hs b/rzk/src/Language/Rzk/VSCode/Handlers.hs index ab9a06f92..f84702506 100644 --- a/rzk/src/Language/Rzk/VSCode/Handlers.hs +++ b/rzk/src/Language/Rzk/VSCode/Handlers.hs @@ -106,8 +106,14 @@ typecheckFromConfigFile = do defaultTypeCheck (typecheckModulesWithLocationIncremental cachedModules parsedModules) (typeErrors, _checkedModules) <- case tcResults of - Left (_ex :: SomeException) -> return ([], []) -- FIXME: publish diagnostics about an exception during typechecking! - Right (Left err) -> return ([err], []) -- sort of impossible + Left (ex :: SomeException) -> do + -- Just a warning to be logged in the "Output" panel and not shown to the user as an error message + -- because exceptions are expected when the file has invalid syntax + logWarning ("Encountered an exception while typechecking:\n" ++ show ex) + return ([], []) + Right (Left err) -> do + logError ("An impossible error happened! Please report a bug:\n" ++ ppTypeErrorInScopedContext' BottomUp err) + return ([err], []) -- sort of impossible Right (Right (checkedModules, errors)) -> do -- cache well-typed modules logInfo (show (length checkedModules) ++ " modules successfully typechecked") From f0aadcb1b6e87a13808ea08c0a188a3968667ec9 Mon Sep 17 00:00:00 2001 From: Abdelrahman Abounegm Date: Fri, 15 Dec 2023 15:48:19 +0300 Subject: [PATCH 2/9] Add DeepSeq package to dependencies --- rzk/package.yaml | 1 + rzk/rzk.cabal | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/rzk/package.yaml b/rzk/package.yaml index c4eb1e8fe..f34f51103 100644 --- a/rzk/package.yaml +++ b/rzk/package.yaml @@ -52,6 +52,7 @@ dependencies: template-haskell: ">= 2.14.0.0" text: ">= 1.2.3.1" yaml: ">= 0.11.0.0" + deepseq: ">=1.4.8.1" ghc-options: - -Wall diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index edac20166..d1ed4c6c9 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -69,6 +69,7 @@ library , base >=4.7 && <5 , bifunctors >=5.5.3 , bytestring >=0.10.8.2 + , deepseq >=1.4.8.1 , directory >=1.2.7.0 , mtl >=2.2.2 , template-haskell >=2.14.0.0 @@ -113,6 +114,7 @@ executable rzk , base >=4.7 && <5 , bifunctors >=5.5.3 , bytestring >=0.10.8.2 + , deepseq >=1.4.8.1 , directory >=1.2.7.0 , mtl >=2.2.2 , rzk @@ -145,6 +147,7 @@ test-suite doctests , base , bifunctors >=5.5.3 , bytestring >=0.10.8.2 + , deepseq >=1.4.8.1 , directory >=1.2.7.0 , doctest , mtl >=2.2.2 @@ -175,6 +178,7 @@ test-suite rzk-test , base >=4.7 && <5 , bifunctors >=5.5.3 , bytestring >=0.10.8.2 + , deepseq >=1.4.8.1 , directory >=1.2.7.0 , hspec , hspec-discover From 75ae60ac9df15c22f185b8bb33b1444d5ae31c49 Mon Sep 17 00:00:00 2001 From: Abdelrahman Abounegm Date: Fri, 15 Dec 2023 15:52:28 +0300 Subject: [PATCH 3/9] Convert `formatTextEdits` to IO to catch errors --- rzk/src/Language/Rzk/VSCode/Handlers.hs | 4 +- rzk/src/Rzk/Format.hs | 66 +++++++++++++++++-------- rzk/test/Rzk/FormatSpec.hs | 4 +- 3 files changed, 51 insertions(+), 23 deletions(-) diff --git a/rzk/src/Language/Rzk/VSCode/Handlers.hs b/rzk/src/Language/Rzk/VSCode/Handlers.hs index f84702506..1e5d0dbb0 100644 --- a/rzk/src/Language/Rzk/VSCode/Handlers.hs +++ b/rzk/src/Language/Rzk/VSCode/Handlers.hs @@ -239,7 +239,9 @@ formatDocument req res = do mdoc <- getVirtualFile doc possibleEdits <- case virtualFileText <$> mdoc of Nothing -> return (Left "Failed to get file contents") - Just sourceCode -> return (Right $ map formattingEditToTextEdit $ formatTextEdits (filter (/= '\r') $ T.unpack sourceCode)) + Just sourceCode -> do + edits <- liftIO $ formatTextEdits (filter (/= '\r') $ T.unpack sourceCode) + return (Right $ map formattingEditToTextEdit edits) case possibleEdits of Left err -> res $ Left $ ResponseError (InR ErrorCodes_InternalError) err Nothing Right edits -> do diff --git a/rzk/src/Rzk/Format.hs b/rzk/src/Rzk/Format.hs index 75f1f5ffb..dd546c2cf 100644 --- a/rzk/src/Rzk/Format.hs +++ b/rzk/src/Rzk/Format.hs @@ -5,8 +5,10 @@ Description : This module defines the formatter for rzk files. The formatter is designed in a way that can be consumed both by the CLI and the LSP server. -} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# OPTIONS_GHC -Wno-orphans #-} module Rzk.Format ( FormattingEdit (FormattingEdit), @@ -15,15 +17,18 @@ module Rzk.Format ( isWellFormatted, isWellFormattedFile, ) where -import Control.Monad ((<$!>)) import Data.List (elemIndex, foldl', sort) +import Control.DeepSeq (NFData, force, rnf) +import Control.Exception (SomeException, evaluate, try) +import qualified Data.Text as T +import qualified Data.Text.IO as T + import Language.Rzk.Syntax (tryExtractMarkdownCodeBlocks) import Language.Rzk.Syntax.Layout (resolveLayout) -import Language.Rzk.Syntax.Lex (Posn (Pn), - Tok (TK, T_VarIdentToken), - TokSymbol (TokSymbol), Token (PT), - tokens) +import Language.Rzk.Syntax.Lex (Posn (Pn), Tok (..), + TokSymbol (TokSymbol), + Token (Err, PT), tokens) -- | All indices are 1-based (as received from the lexer) -- Note: LSP uses 0-based indices @@ -47,19 +52,38 @@ data FormatState = FormatState { parensDepth :: Int -- ^ The level of parentheses nesting , definingName :: Bool -- ^ After #define, in name or assumptions (to detect the : for the type) , lambdaArrow :: Bool -- ^ After a lambda '\', in the parameters (to leave its -> on the same line) + , allTokens :: [Token] -- ^ The full array of tokens after resolving the layout } +instance NFData Posn where + rnf (Pn a l c) = rnf a `seq` rnf l `seq` rnf c + +instance NFData Token where + rnf (Err pos) = rnf pos + rnf (PT pos (TK (TokSymbol s i))) = rnf pos `seq` rnf s `seq` rnf i + rnf (PT pos (T_VarIdentToken s)) = rnf pos `seq` rnf s + rnf (PT pos (T_HoleIdentToken s)) = rnf pos `seq` rnf s + rnf (PT pos (TL s)) = rnf pos `seq` rnf s + rnf (PT pos (TI s)) = rnf pos `seq` rnf s + rnf (PT pos (TV s)) = rnf pos `seq` rnf s + rnf (PT pos (TD s)) = rnf pos `seq` rnf s + rnf (PT pos (TC s)) = rnf pos `seq` rnf s + -- TODO: replace all tabs with 1 space before processing -formatTextEdits :: String -> [FormattingEdit] -formatTextEdits contents = go initialState toks +formatTextEdits :: String -> IO [FormattingEdit] +formatTextEdits contents = do + toksOrError <- try $ evaluate $ force $ resolveLayout True (tokens rzkBlocks) + case toksOrError of + Left (_ :: SomeException) -> return [] -- TODO: log error (in a CLI and LSP friendly way) + Right toks -> do + return $ go (initialState {allTokens = toks}) toks where - initialState = FormatState { parensDepth = 0, definingName = False, lambdaArrow = False } + initialState = FormatState { parensDepth = 0, definingName = False, lambdaArrow = False, allTokens = [] } incParensDepth s = s { parensDepth = parensDepth s + 1 } - decParensDepth s = s { parensDepth = parensDepth s - 1 } + decParensDepth s = s { parensDepth = 0 `max` (parensDepth s - 1) } rzkBlocks = tryExtractMarkdownCodeBlocks "rzk" contents -- TODO: replace tabs with spaces contentLines line = lines rzkBlocks !! (line - 1) -- Sorry - toks = resolveLayout True (tokens rzkBlocks) - lineTokensBefore line col = filter isBefore toks + lineTokensBefore toks line col = filter isBefore toks where isBefore (PT (Pn _ l c) _) = l == line && c < col isBefore _ = False @@ -124,7 +148,7 @@ formatTextEdits contents = go initialState toks where spaceCol = col + 1 lineContent = contentLines line - precededBySingleCharOnly = all isPunctuation (lineTokensBefore line col) + precededBySingleCharOnly = all isPunctuation (lineTokensBefore (allTokens s) line col) singleCharUnicodeTokens = filter (\(_, unicode) -> length unicode == 1) unicodeTokens punctuations = concat [ map fst singleCharUnicodeTokens -- ASCII sequences will be converted soon @@ -283,12 +307,14 @@ applyTextEdits :: [FormattingEdit] -> String -> String applyTextEdits edits contents = foldl' (flip applyTextEdit) contents (reverse $ sort edits) -- | Format Rzk code, returning the formatted version. -format :: String -> String -format = applyTextEdits =<< formatTextEdits +format :: String -> IO String +format s = do + edits <- formatTextEdits s + return $ applyTextEdits edits s -- | Format Rzk code from a file formatFile :: FilePath -> IO String -formatFile path = format <$!> readFile path -- strict because possibility of writing to same file +formatFile path = readFile path >>= format -- | Format the file and write the result back to the file. formatFileWrite :: FilePath -> IO () @@ -296,9 +322,9 @@ formatFileWrite path = formatFile path >>= writeFile path -- | Check if the given Rzk source code is well formatted. -- This is useful for automation tasks. -isWellFormatted :: String -> Bool -isWellFormatted src = null (formatTextEdits src) +isWellFormatted :: String -> IO Bool +isWellFormatted src = null <$> formatTextEdits src -- | Same as 'isWellFormatted', but reads the source code from a file. isWellFormattedFile :: FilePath -> IO Bool -isWellFormattedFile path = isWellFormatted <$> readFile path +isWellFormattedFile path = T.readFile path >>= isWellFormatted . T.unpack diff --git a/rzk/test/Rzk/FormatSpec.hs b/rzk/test/Rzk/FormatSpec.hs index 0ac91d09d..267129b20 100644 --- a/rzk/test/Rzk/FormatSpec.hs +++ b/rzk/test/Rzk/FormatSpec.hs @@ -12,8 +12,8 @@ formatsTo :: FilePath -> FilePath -> Expectation formatsTo beforePath afterPath = do beforeSrc <- readFile ("test/files/" ++ beforePath) afterSrc <- readFile ("test/files/" ++ afterPath) - format beforeSrc `shouldBe` afterSrc - isWellFormatted afterSrc `shouldBe` True -- idempotency + format beforeSrc `shouldReturn` afterSrc + isWellFormatted afterSrc `shouldReturn` True -- idempotency formats :: FilePath -> Expectation formats path = (path ++ "-bad.rzk") `formatsTo` (path ++ "-good.rzk") From 0e97ab29783614d5259703052e26f7d30f4f274d Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sat, 16 Dec 2023 00:14:55 +0300 Subject: [PATCH 4/9] Make safer resolveLayout, use that in the formatter, drop deepseq dependency --- rzk/package.yaml | 1 - rzk/rzk.cabal | 4 ---- rzk/src/Language/Rzk/Syntax.hs | 26 +++++++++++++++++++---- rzk/src/Rzk/Format.hs | 38 ++++++++++++---------------------- 4 files changed, 35 insertions(+), 34 deletions(-) diff --git a/rzk/package.yaml b/rzk/package.yaml index f34f51103..c4eb1e8fe 100644 --- a/rzk/package.yaml +++ b/rzk/package.yaml @@ -52,7 +52,6 @@ dependencies: template-haskell: ">= 2.14.0.0" text: ">= 1.2.3.1" yaml: ">= 0.11.0.0" - deepseq: ">=1.4.8.1" ghc-options: - -Wall diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index d1ed4c6c9..edac20166 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -69,7 +69,6 @@ library , base >=4.7 && <5 , bifunctors >=5.5.3 , bytestring >=0.10.8.2 - , deepseq >=1.4.8.1 , directory >=1.2.7.0 , mtl >=2.2.2 , template-haskell >=2.14.0.0 @@ -114,7 +113,6 @@ executable rzk , base >=4.7 && <5 , bifunctors >=5.5.3 , bytestring >=0.10.8.2 - , deepseq >=1.4.8.1 , directory >=1.2.7.0 , mtl >=2.2.2 , rzk @@ -147,7 +145,6 @@ test-suite doctests , base , bifunctors >=5.5.3 , bytestring >=0.10.8.2 - , deepseq >=1.4.8.1 , directory >=1.2.7.0 , doctest , mtl >=2.2.2 @@ -178,7 +175,6 @@ test-suite rzk-test , base >=4.7 && <5 , bifunctors >=5.5.3 , bytestring >=0.10.8.2 - , deepseq >=1.4.8.1 , directory >=1.2.7.0 , hspec , hspec-discover diff --git a/rzk/src/Language/Rzk/Syntax.hs b/rzk/src/Language/Rzk/Syntax.hs index 291a883e3..8a93e47f7 100644 --- a/rzk/src/Language/Rzk/Syntax.hs +++ b/rzk/src/Language/Rzk/Syntax.hs @@ -9,6 +9,7 @@ module Language.Rzk.Syntax ( parseModuleRzk, parseModuleFile, parseTerm, + resolveLayout, Print.Print(..), printTree, tryExtractMarkdownCodeBlocks, extractMarkdownCodeBlocks, @@ -23,11 +24,12 @@ import Data.Char (isSpace) import qualified Data.List as List import Language.Rzk.Syntax.Abs +import qualified Language.Rzk.Syntax.Layout as Layout import qualified Language.Rzk.Syntax.Print as Print -import Language.Rzk.Syntax.Layout (resolveLayout) -import Language.Rzk.Syntax.Lex (tokens) +import Language.Rzk.Syntax.Lex (tokens, Token) import Language.Rzk.Syntax.Par (pModule, pTerm) +import GHC.IO (unsafePerformIO) tryOrDisplayException :: Either String a -> IO (Either String a) tryOrDisplayException = tryOrDisplayExceptionIO . evaluate @@ -42,10 +44,10 @@ parseModuleSafe :: String -> IO (Either String Module) parseModuleSafe = tryOrDisplayException . parseModule parseModule :: String -> Either String Module -parseModule = pModule . resolveLayout True . tokens . tryExtractMarkdownCodeBlocks "rzk" +parseModule = pModule . Layout.resolveLayout True . tokens . tryExtractMarkdownCodeBlocks "rzk" parseModuleRzk :: String -> Either String Module -parseModuleRzk = pModule . resolveLayout True . tokens +parseModuleRzk = pModule . Layout.resolveLayout True . tokens parseModuleFile :: FilePath -> IO (Either String Module) parseModuleFile path = do @@ -122,6 +124,22 @@ identifyCodeBlockStart line where (prefix, suffix) = List.splitAt 3 line +-- * Making BNFC resolveLayout safer + +-- | Replace layout syntax with explicit layout tokens. +resolveLayout + :: Bool -- ^ Whether to use top-level layout. + -> [Token] -- ^ Token stream before layout resolution. + -> Either String [Token] -- ^ Token stream after layout resolution. +resolveLayout isTopLevel toks = unsafePerformIO $ do + -- NOTE: we use (length . show) as poor man's Control.DeepSeq.force + -- NOTE: this is required to force all resolveLayout error's to come out + try (evaluate (length (show resolvedToks))) >>= \case + Left (err :: SomeException) -> return (Left (displayException err)) + Right _ -> return (Right resolvedToks) + where + resolvedToks = Layout.resolveLayout isTopLevel toks + -- * Overriding BNFC pretty-printer -- | Like 'Print.printTree', but does not insert newlines for curly braces. diff --git a/rzk/src/Rzk/Format.hs b/rzk/src/Rzk/Format.hs index dd546c2cf..7677d451d 100644 --- a/rzk/src/Rzk/Format.hs +++ b/rzk/src/Rzk/Format.hs @@ -9,6 +9,7 @@ LSP server. {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -Wno-orphans #-} +{-# LANGUAGE LambdaCase #-} module Rzk.Format ( FormattingEdit (FormattingEdit), @@ -19,16 +20,14 @@ module Rzk.Format ( import Data.List (elemIndex, foldl', sort) -import Control.DeepSeq (NFData, force, rnf) -import Control.Exception (SomeException, evaluate, try) import qualified Data.Text as T import qualified Data.Text.IO as T -import Language.Rzk.Syntax (tryExtractMarkdownCodeBlocks) -import Language.Rzk.Syntax.Layout (resolveLayout) +import Language.Rzk.Syntax (tryExtractMarkdownCodeBlocks, + resolveLayout) import Language.Rzk.Syntax.Lex (Posn (Pn), Tok (..), TokSymbol (TokSymbol), - Token (Err, PT), tokens) + Token (PT), tokens) -- | All indices are 1-based (as received from the lexer) -- Note: LSP uses 0-based indices @@ -55,28 +54,17 @@ data FormatState = FormatState , allTokens :: [Token] -- ^ The full array of tokens after resolving the layout } -instance NFData Posn where - rnf (Pn a l c) = rnf a `seq` rnf l `seq` rnf c - -instance NFData Token where - rnf (Err pos) = rnf pos - rnf (PT pos (TK (TokSymbol s i))) = rnf pos `seq` rnf s `seq` rnf i - rnf (PT pos (T_VarIdentToken s)) = rnf pos `seq` rnf s - rnf (PT pos (T_HoleIdentToken s)) = rnf pos `seq` rnf s - rnf (PT pos (TL s)) = rnf pos `seq` rnf s - rnf (PT pos (TI s)) = rnf pos `seq` rnf s - rnf (PT pos (TV s)) = rnf pos `seq` rnf s - rnf (PT pos (TD s)) = rnf pos `seq` rnf s - rnf (PT pos (TC s)) = rnf pos `seq` rnf s - --- TODO: replace all tabs with 1 space before processing formatTextEdits :: String -> IO [FormattingEdit] formatTextEdits contents = do - toksOrError <- try $ evaluate $ force $ resolveLayout True (tokens rzkBlocks) - case toksOrError of - Left (_ :: SomeException) -> return [] -- TODO: log error (in a CLI and LSP friendly way) - Right toks -> do - return $ go (initialState {allTokens = toks}) toks + let edits = unsafeFormatTextEdits contents + return edits + +-- TODO: replace all tabs with 1 space before processing +unsafeFormatTextEdits :: String -> [FormattingEdit] +unsafeFormatTextEdits contents = + case resolveLayout True (tokens rzkBlocks) of + Left _err -> [] -- TODO: log error (in a CLI and LSP friendly way) + Right allToks -> go (initialState {allTokens = allToks}) allToks where initialState = FormatState { parensDepth = 0, definingName = False, lambdaArrow = False, allTokens = [] } incParensDepth s = s { parensDepth = parensDepth s + 1 } From 6fd360b1ea9f5370f3c9cce61962cd42d5272791 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sat, 16 Dec 2023 00:17:56 +0300 Subject: [PATCH 5/9] Apply autoformatting to docs --- docs/docs/en/examples/recId.rzk.md | 26 +++++++++---------- .../en/getting-started/dependent-types.rzk.md | 18 ++++++------- docs/docs/ru/examples/recId.rzk.md | 26 +++++++++---------- .../ru/getting-started/dependent-types.rzk.md | 18 ++++++------- 4 files changed, 44 insertions(+), 44 deletions(-) diff --git a/docs/docs/en/examples/recId.rzk.md b/docs/docs/en/examples/recId.rzk.md index 96d780dce..b16d35934 100644 --- a/docs/docs/en/examples/recId.rzk.md +++ b/docs/docs/en/examples/recId.rzk.md @@ -19,17 +19,17 @@ We begin by introducing common HoTT definitions: -- A is contractible there exists x : A such that for any y : A we have x = y. #define iscontr (A : U) : U - := Σ ( a : A) , (x : A) → a =_{A} x + := Σ (a : A) , (x : A) → a =_{A} x -- A is a proposition if for any x, y : A we have x = y #define isaprop (A : U) : U - := ( x : A) → (y : A) → x =_{A} y + := (x : A) → (y : A) → x =_{A} y -- A is a set if for any x, y : A the type x =_{A} y is a proposition #define isaset (A : U) : U - := ( x : A) → (y : A) → isaprop (x =_{A} y) + := (x : A) → (y : A) → isaprop (x =_{A} y) -- A function f : A → B is an equivalence -- if there exists g : B → A @@ -37,7 +37,7 @@ We begin by introducing common HoTT definitions: -- and for all y : B we have f (g y) = y #define isweq (A : U) (B : U) (f : A → B) : U - := Σ ( g : B → A) + := Σ (g : B → A) , prod ( ( x : A) → g (f x) =_{A} x) ( ( y : B) → f (g y) =_{B} y) @@ -45,7 +45,7 @@ We begin by introducing common HoTT definitions: -- Equivalence of types A and B #define weq (A : U) (B : U) : U - := Σ ( f : A → B) + := Σ (f : A → B) , isweq A B f -- Transport along a path @@ -66,12 +66,12 @@ We can now define relative function extensionality. There are several formulatio -- [RS17, Axiom 4.6] Relative function extensionality. #define relfunext : U - := ( I : CUBE) + := (I : CUBE) → ( ψ : I → TOPE) → ( φ : ψ → TOPE) → ( A : ψ → U) → ( ( t : ψ) → iscontr (A t)) - → ( a : ( t : φ) → A t) + → ( a : (t : φ) → A t) → ( t : ψ) → A t [ φ t ↦ a t] -- [RS17, Proposition 4.8] A (weaker) formulation of function extensionality. @@ -82,9 +82,9 @@ We can now define relative function extensionality. There are several formulatio → ( ψ : I → TOPE) → ( φ : ψ → TOPE) → ( A : ψ → U) - → ( a : ( t : φ) → A t) + → ( a : (t : φ) → A t) → ( f : (t : ψ) → A t [ φ t ↦ a t ]) - → ( g : ( t : ψ) → A t [ φ t ↦ a t ]) + → ( g : (t : ψ) → A t [ φ t ↦ a t ]) → weq ( f = g) ( ( t : ψ) → (f t =_{A t} g t) [ φ t ↦ refl ]) @@ -106,13 +106,13 @@ First, we define how to restrict an extension type to a subshape: -- Restrict extension type to a subshape. #define restrict_phi - ( a : ( t : φ) → A t) + ( a : (t : φ) → A t) : ( t : I | ψ t ∧ φ t) → A t := \ t → a t -- Restrict extension type to a subshape. #define restrict_psi - ( a : ( t : ψ) → A t) + ( a : (t : ψ) → A t) : ( t : I | ψ t ∧ φ t) → A t := \ t → a t ``` @@ -122,14 +122,14 @@ Then, how to reformulate an `a` (or `b`) as an extension of its restriction: ```rzk -- Reformulate extension type as an extension of a restriction. #define ext-of-restrict_psi - ( a : ( t : ψ) → A t) + ( a : (t : ψ) → A t) : ( t : ψ) → A t [ ψ t ∧ φ t ↦ restrict_psi a t ] := a -- type is coerced automatically here -- Reformulate extension type as an extension of a restriction. #define ext-of-restrict_phi - ( a : ( t : φ) → A t) + ( a : (t : φ) → A t) : ( t : φ) → A t [ ψ t ∧ φ t ↦ restrict_phi a t ] := a -- type is coerced automatically here diff --git a/docs/docs/en/getting-started/dependent-types.rzk.md b/docs/docs/en/getting-started/dependent-types.rzk.md index cfbed328a..72b00613b 100644 --- a/docs/docs/en/getting-started/dependent-types.rzk.md +++ b/docs/docs/en/getting-started/dependent-types.rzk.md @@ -79,7 +79,7 @@ which we will discuss soon. For now, we give definition of product types: #define prod ( A B : U) : U - := Σ ( _ : A) , B + := Σ (_ : A) , B ``` The type `#!rzk prod A B` corresponds to the product type $A \times B$. @@ -188,7 +188,7 @@ For example, for the product type `#!rzk prod A B`, recursion principle looks li ( C : U) ( f : A → B → C) : prod A B → C - := \ ( a , b) → f a b + := \ (a , b) → f a b ``` For the `#!rzk Unit` type, recursion principle is trivial: @@ -223,7 +223,7 @@ For example, for the product type `#!rzk prod A B`, induction principle looks li ( C : prod A B → U) ( f : (a : A) → (b : B) → C (a , b)) : ( z : prod A B) → C z - := \ ( a , b) → f a b + := \ (a , b) → f a b ``` We can use `#!rzk ind-prod` to prove the uniqueness principle for products. @@ -313,7 +313,7 @@ The first projection can be easily defined in terms of pattern matching: ( A : U) ( B : A → U) : ( Σ ( a : A) , B a) → A - := \ ( a , _) → a + := \ (a , _) → a ``` However, second projection requires some care. For instance, we might try this: @@ -339,7 +339,7 @@ To access it, we need a dependent function: ( A : U) ( B : A → U) : ( z : Σ (a : A) , B a) → B (pr₁ A B z) - := \ ( _ , b) → b + := \ (_ , b) → b ``` In Rzk, it is sometimes more convenient to talk about Σ-types as "total" types (as in "total spaces"): @@ -349,7 +349,7 @@ In Rzk, it is sometimes more convenient to talk about Σ-types as "total" types ( A : U) ( B : A → U) : U - := Σ ( a : A) , B a + := Σ (a : A) , B a ``` We can use pattern matching in the function type and this new definition to write @@ -376,7 +376,7 @@ the recursion principle for product types: ( C : U) ( f : (a : A) → B a → C) : total-type A B → C - := \ ( a , b) → f a b + := \ (a , b) → f a b ``` The induction principle is, again, a generalization of the recursion @@ -389,7 +389,7 @@ principle to dependent types: ( C : total-type A B → U) ( f : (a : A) → (b : B a) → C (a , b)) : ( z : total-type A B) → C z - := \ ( a , b) → f a b + := \ (a , b) → f a b ``` As before, using `#!rzk ind-Σ` we may prove the uniqueness principle, now for Σ-types: @@ -424,7 +424,7 @@ Using `#!rzk ind-Σ` we can also prove a type-theoretic axiom of choice: ```rzk #define AxiomOfChoice : U - := ( A : U) + := (A : U) → ( B : U) → ( R : A → B → U) → ( ( x : A) → Σ (y : B) , R x y) diff --git a/docs/docs/ru/examples/recId.rzk.md b/docs/docs/ru/examples/recId.rzk.md index 96d780dce..b16d35934 100644 --- a/docs/docs/ru/examples/recId.rzk.md +++ b/docs/docs/ru/examples/recId.rzk.md @@ -19,17 +19,17 @@ We begin by introducing common HoTT definitions: -- A is contractible there exists x : A such that for any y : A we have x = y. #define iscontr (A : U) : U - := Σ ( a : A) , (x : A) → a =_{A} x + := Σ (a : A) , (x : A) → a =_{A} x -- A is a proposition if for any x, y : A we have x = y #define isaprop (A : U) : U - := ( x : A) → (y : A) → x =_{A} y + := (x : A) → (y : A) → x =_{A} y -- A is a set if for any x, y : A the type x =_{A} y is a proposition #define isaset (A : U) : U - := ( x : A) → (y : A) → isaprop (x =_{A} y) + := (x : A) → (y : A) → isaprop (x =_{A} y) -- A function f : A → B is an equivalence -- if there exists g : B → A @@ -37,7 +37,7 @@ We begin by introducing common HoTT definitions: -- and for all y : B we have f (g y) = y #define isweq (A : U) (B : U) (f : A → B) : U - := Σ ( g : B → A) + := Σ (g : B → A) , prod ( ( x : A) → g (f x) =_{A} x) ( ( y : B) → f (g y) =_{B} y) @@ -45,7 +45,7 @@ We begin by introducing common HoTT definitions: -- Equivalence of types A and B #define weq (A : U) (B : U) : U - := Σ ( f : A → B) + := Σ (f : A → B) , isweq A B f -- Transport along a path @@ -66,12 +66,12 @@ We can now define relative function extensionality. There are several formulatio -- [RS17, Axiom 4.6] Relative function extensionality. #define relfunext : U - := ( I : CUBE) + := (I : CUBE) → ( ψ : I → TOPE) → ( φ : ψ → TOPE) → ( A : ψ → U) → ( ( t : ψ) → iscontr (A t)) - → ( a : ( t : φ) → A t) + → ( a : (t : φ) → A t) → ( t : ψ) → A t [ φ t ↦ a t] -- [RS17, Proposition 4.8] A (weaker) formulation of function extensionality. @@ -82,9 +82,9 @@ We can now define relative function extensionality. There are several formulatio → ( ψ : I → TOPE) → ( φ : ψ → TOPE) → ( A : ψ → U) - → ( a : ( t : φ) → A t) + → ( a : (t : φ) → A t) → ( f : (t : ψ) → A t [ φ t ↦ a t ]) - → ( g : ( t : ψ) → A t [ φ t ↦ a t ]) + → ( g : (t : ψ) → A t [ φ t ↦ a t ]) → weq ( f = g) ( ( t : ψ) → (f t =_{A t} g t) [ φ t ↦ refl ]) @@ -106,13 +106,13 @@ First, we define how to restrict an extension type to a subshape: -- Restrict extension type to a subshape. #define restrict_phi - ( a : ( t : φ) → A t) + ( a : (t : φ) → A t) : ( t : I | ψ t ∧ φ t) → A t := \ t → a t -- Restrict extension type to a subshape. #define restrict_psi - ( a : ( t : ψ) → A t) + ( a : (t : ψ) → A t) : ( t : I | ψ t ∧ φ t) → A t := \ t → a t ``` @@ -122,14 +122,14 @@ Then, how to reformulate an `a` (or `b`) as an extension of its restriction: ```rzk -- Reformulate extension type as an extension of a restriction. #define ext-of-restrict_psi - ( a : ( t : ψ) → A t) + ( a : (t : ψ) → A t) : ( t : ψ) → A t [ ψ t ∧ φ t ↦ restrict_psi a t ] := a -- type is coerced automatically here -- Reformulate extension type as an extension of a restriction. #define ext-of-restrict_phi - ( a : ( t : φ) → A t) + ( a : (t : φ) → A t) : ( t : φ) → A t [ ψ t ∧ φ t ↦ restrict_phi a t ] := a -- type is coerced automatically here diff --git a/docs/docs/ru/getting-started/dependent-types.rzk.md b/docs/docs/ru/getting-started/dependent-types.rzk.md index 0d0a0be1b..6f833e9b6 100644 --- a/docs/docs/ru/getting-started/dependent-types.rzk.md +++ b/docs/docs/ru/getting-started/dependent-types.rzk.md @@ -83,7 +83,7 @@ Rzk не предоставляет встроенных типов-произв #define prod ( A B : U) : U - := Σ ( _ : A) , B + := Σ (_ : A) , B ``` Запись `#!rzk prod A B` соответствует типу-произведению $A \times B$. @@ -193,7 +193,7 @@ Rzk не предоставляет встроенных типов-произв ( C : U) ( f : A → B → C) : prod A B → C - := \ ( a , b) → f a b + := \ (a , b) → f a b ``` Для типа `#!rzk Unit`, принцип рекурсии тривиален: @@ -228,7 +228,7 @@ Rzk не предоставляет встроенных типов-произв ( C : prod A B → U) ( f : (a : A) → (b : B) → C (a , b)) : ( z : prod A B) → C z - := \ ( a , b) → f a b + := \ (a , b) → f a b ``` Мы можем использовать `#!rzk ind-prod` для доказательства принципа уникальности. @@ -318,7 +318,7 @@ Rzk не предоставляет встроенных типов-произв ( A : U) ( B : A → U) : ( Σ ( a : A) , B a) → A - := \ ( a , _) → a + := \ (a , _) → a ``` Однако, для определения второй проекции нужна осторожность. В частности, следующее определение не сработает: @@ -344,7 +344,7 @@ undefined variable: a ( A : U) ( B : A → U) : ( z : Σ (a : A) , B a) → B (pr₁ A B z) - := \ ( _ , b) → b + := \ (_ , b) → b ``` Иногда о Σ-типах удобнее говорить как о тотальных (общих?) типах (аналогично "total spaces"): @@ -354,7 +354,7 @@ undefined variable: a ( A : U) ( B : A → U) : U - := Σ ( a : A) , B a + := Σ (a : A) , B a ``` Мы можем переписать более компактно определение второй проекции, @@ -381,7 +381,7 @@ undefined variable: a ( C : U) ( f : (a : A) → B a → C) : total-type A B → C - := \ ( a , b) → f a b + := \ (a , b) → f a b ``` Аналогично с принципом индукции: @@ -393,7 +393,7 @@ undefined variable: a ( C : total-type A B → U) ( f : (a : A) → (b : B a) → C (a , b)) : ( z : total-type A B) → C z - := \ ( a , b) → f a b + := \ (a , b) → f a b ``` Как и раньше, мы можем использовать `#!rzk ind-Σ` для доказательства принципа уникальности, @@ -431,7 +431,7 @@ undefined variable: a ```rzk #define AxiomOfChoice : U - := ( A : U) + := (A : U) → ( B : U) → ( R : A → B → U) → ( ( x : A) → Σ (y : B) , R x y) From 40505ea20ee625dc1a35146e9fbe22ac544e46c0 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sat, 16 Dec 2023 00:23:32 +0300 Subject: [PATCH 6/9] Check Rzk formatting for all languages before rendering MkDocs --- .github/workflows/mkdocs.yml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.github/workflows/mkdocs.yml b/.github/workflows/mkdocs.yml index 93476dca8..21e6a7176 100644 --- a/.github/workflows/mkdocs.yml +++ b/.github/workflows/mkdocs.yml @@ -43,6 +43,12 @@ jobs: pushd ${lang_dir} && rzk typecheck; popd ; done + - name: Check Rzk formatting for each language + run: + for lang_dir in $(ls -d docs/docs/*/); do + pushd ${lang_dir} && rzk format --check; popd ; + done + - name: 🔨 Install MkDocs Material and mike run: pip install -r docs/requirements.txt From 20dfcc2072bfd80080bd631346b4c9ebdc151dd5 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sat, 16 Dec 2023 00:51:48 +0300 Subject: [PATCH 7/9] Clean up formatting code --- rzk/src/Language/Rzk/VSCode/Handlers.hs | 2 +- rzk/src/Rzk/Format.hs | 28 ++++++++++--------------- rzk/test/Rzk/FormatSpec.hs | 4 ++-- 3 files changed, 14 insertions(+), 20 deletions(-) diff --git a/rzk/src/Language/Rzk/VSCode/Handlers.hs b/rzk/src/Language/Rzk/VSCode/Handlers.hs index 1e5d0dbb0..2744dcb85 100644 --- a/rzk/src/Language/Rzk/VSCode/Handlers.hs +++ b/rzk/src/Language/Rzk/VSCode/Handlers.hs @@ -240,7 +240,7 @@ formatDocument req res = do possibleEdits <- case virtualFileText <$> mdoc of Nothing -> return (Left "Failed to get file contents") Just sourceCode -> do - edits <- liftIO $ formatTextEdits (filter (/= '\r') $ T.unpack sourceCode) + let edits = formatTextEdits (filter (/= '\r') $ T.unpack sourceCode) return (Right $ map formattingEditToTextEdit edits) case possibleEdits of Left err -> res $ Left $ ResponseError (InR ErrorCodes_InternalError) err Nothing diff --git a/rzk/src/Rzk/Format.hs b/rzk/src/Rzk/Format.hs index 7677d451d..2ba6a9f7d 100644 --- a/rzk/src/Rzk/Format.hs +++ b/rzk/src/Rzk/Format.hs @@ -9,7 +9,6 @@ LSP server. {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -Wno-orphans #-} -{-# LANGUAGE LambdaCase #-} module Rzk.Format ( FormattingEdit (FormattingEdit), @@ -54,14 +53,9 @@ data FormatState = FormatState , allTokens :: [Token] -- ^ The full array of tokens after resolving the layout } -formatTextEdits :: String -> IO [FormattingEdit] -formatTextEdits contents = do - let edits = unsafeFormatTextEdits contents - return edits - -- TODO: replace all tabs with 1 space before processing -unsafeFormatTextEdits :: String -> [FormattingEdit] -unsafeFormatTextEdits contents = +formatTextEdits :: String -> [FormattingEdit] +formatTextEdits contents = case resolveLayout True (tokens rzkBlocks) of Left _err -> [] -- TODO: log error (in a CLI and LSP friendly way) Right allToks -> go (initialState {allTokens = allToks}) allToks @@ -292,17 +286,15 @@ applyTextEdit (FormattingEdit sl sc el ec newText) oldText = Nothing -> length t' applyTextEdits :: [FormattingEdit] -> String -> String -applyTextEdits edits contents = foldl' (flip applyTextEdit) contents (reverse $ sort edits) +applyTextEdits edits contents = foldr applyTextEdit contents (sort edits) -- | Format Rzk code, returning the formatted version. -format :: String -> IO String -format s = do - edits <- formatTextEdits s - return $ applyTextEdits edits s +format :: String -> String +format = applyTextEdits =<< formatTextEdits -- | Format Rzk code from a file formatFile :: FilePath -> IO String -formatFile path = readFile path >>= format +formatFile path = format <$> readFile path -- | Format the file and write the result back to the file. formatFileWrite :: FilePath -> IO () @@ -310,9 +302,11 @@ formatFileWrite path = formatFile path >>= writeFile path -- | Check if the given Rzk source code is well formatted. -- This is useful for automation tasks. -isWellFormatted :: String -> IO Bool -isWellFormatted src = null <$> formatTextEdits src +isWellFormatted :: String -> Bool +isWellFormatted src = null (formatTextEdits src) -- | Same as 'isWellFormatted', but reads the source code from a file. isWellFormattedFile :: FilePath -> IO Bool -isWellFormattedFile path = T.readFile path >>= isWellFormatted . T.unpack +isWellFormattedFile path = do + contents <- T.readFile path + return (isWellFormatted (T.unpack contents)) diff --git a/rzk/test/Rzk/FormatSpec.hs b/rzk/test/Rzk/FormatSpec.hs index 267129b20..0ac91d09d 100644 --- a/rzk/test/Rzk/FormatSpec.hs +++ b/rzk/test/Rzk/FormatSpec.hs @@ -12,8 +12,8 @@ formatsTo :: FilePath -> FilePath -> Expectation formatsTo beforePath afterPath = do beforeSrc <- readFile ("test/files/" ++ beforePath) afterSrc <- readFile ("test/files/" ++ afterPath) - format beforeSrc `shouldReturn` afterSrc - isWellFormatted afterSrc `shouldReturn` True -- idempotency + format beforeSrc `shouldBe` afterSrc + isWellFormatted afterSrc `shouldBe` True -- idempotency formats :: FilePath -> Expectation formats path = (path ++ "-bad.rzk") `formatsTo` (path ++ "-good.rzk") From 3a2ddec9157d1498ef6a1d7f380d6d57d28f1f28 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sat, 16 Dec 2023 00:53:46 +0300 Subject: [PATCH 8/9] Make formatFile strict --- rzk/src/Rzk/Format.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/rzk/src/Rzk/Format.hs b/rzk/src/Rzk/Format.hs index 2ba6a9f7d..2afd32aa6 100644 --- a/rzk/src/Rzk/Format.hs +++ b/rzk/src/Rzk/Format.hs @@ -294,7 +294,9 @@ format = applyTextEdits =<< formatTextEdits -- | Format Rzk code from a file formatFile :: FilePath -> IO String -formatFile path = format <$> readFile path +formatFile path = do + contents <- T.readFile path + return (format (T.unpack contents)) -- | Format the file and write the result back to the file. formatFileWrite :: FilePath -> IO () From a5a1642edad07d140671b723f522d3b415ab381d Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Sat, 16 Dec 2023 00:56:25 +0300 Subject: [PATCH 9/9] Fix warning --- rzk/src/Rzk/Format.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rzk/src/Rzk/Format.hs b/rzk/src/Rzk/Format.hs index 2afd32aa6..233f04448 100644 --- a/rzk/src/Rzk/Format.hs +++ b/rzk/src/Rzk/Format.hs @@ -17,7 +17,7 @@ module Rzk.Format ( isWellFormatted, isWellFormattedFile, ) where -import Data.List (elemIndex, foldl', sort) +import Data.List (elemIndex, sort) import qualified Data.Text as T import qualified Data.Text.IO as T