rzk 0.6.1 → 0.6.2
raw patch · 7 files changed
+279/−128 lines, 7 filesdep +data-default-class
Dependencies added: data-default-class
Files
- ChangeLog.md +9/−0
- rzk.cabal +5/−1
- src/Language/Rzk/Syntax/Print.hs +29/−32
- src/Language/Rzk/VSCode/Handlers.hs +54/−5
- src/Language/Rzk/VSCode/Lsp.hs +1/−0
- src/Rzk/Main.hs +2/−2
- src/Rzk/TypeCheck.hs +179/−88
ChangeLog.md view
@@ -6,6 +6,15 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.6.2 — 2023-09-26++This version contains some improvements in efficiency and also to the language server:++- Improve efficiency of the tope solver, applying LEM for directed interval only as a fallback option (see [#102](https://github.com/rzk-lang/rzk/pull/102))+- Support autocompleting definitions from previous modules (see [#102](https://github.com/rzk-lang/rzk/pull/103))+ - Well-typed definitions from the same module also work if the module is only partially well-typed!+- Improve information order in the error messages given in LSP diagnostics (see [#104](https://github.com/rzk-lang/rzk/pull/104))+ ## v0.6.1 — 2023-09-24 This version contains a minor fix:
rzk.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: rzk-version: 0.6.1+version: 0.6.2 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@@ -54,6 +54,7 @@ , base >=4.7 && <5 , bifunctors , bytestring+ , data-default-class , filepath , lens , mtl@@ -91,6 +92,7 @@ , base >=4.7 && <5 , bifunctors , bytestring+ , data-default-class , filepath , lens , mtl@@ -122,6 +124,7 @@ , base , bifunctors , bytestring+ , data-default-class , doctest , filepath , lens@@ -151,6 +154,7 @@ , base >=4.7 && <5 , bifunctors , bytestring+ , data-default-class , filepath , lens , mtl
src/Language/Rzk/Syntax/Print.hs view
@@ -1,8 +1,8 @@ -- File generated by the BNF Converter (bnfc 2.9.4.1). -{-# LANGUAGE CPP #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase #-} #if __GLASGOW_HASKELL__ <= 708 {-# LANGUAGE OverlappingInstances #-} #endif@@ -11,16 +11,13 @@ module Language.Rzk.Syntax.Print where -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 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. @@ -43,9 +40,9 @@ 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@@ -70,8 +67,8 @@ 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@@ -124,10 +121,10 @@ 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@@ -155,8 +152,8 @@ 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@@ -182,7 +179,7 @@ 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@@ -201,8 +198,8 @@ 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@@ -213,8 +210,8 @@ 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@@ -231,8 +228,8 @@ 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@@ -292,6 +289,6 @@ 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]
src/Language/Rzk/VSCode/Handlers.hs view
@@ -1,24 +1,36 @@+{-# LANGUAGE DataKinds #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}+{-# OPTIONS_GHC -Wno-orphans #-} module Language.Rzk.VSCode.Handlers where import Control.Exception (SomeException, evaluate, try)+import Control.Lens import Control.Monad.Cont (MonadIO (liftIO), forM_)+import Data.Default.Class import Data.List (sort, (\\))+import Data.Maybe (fromMaybe) import qualified Data.Text as T import qualified Data.Yaml as Yaml import Language.LSP.Diagnostics (partitionBySource)+import Language.LSP.Protocol.Lens (HasDetail (detail),+ HasDocumentation (documentation),+ HasLabel (label),+ HasParams (params),+ HasTextDocument (textDocument),+ HasUri (uri)) import Language.LSP.Protocol.Message import Language.LSP.Protocol.Types import Language.LSP.Server-import System.FilePath ((</>))+import System.FilePath (makeRelative, (</>)) import System.FilePath.Glob (compile, globDir) -import Data.Maybe (fromMaybe)-import Language.Rzk.Free.Syntax (VarIdent)-import Language.Rzk.Syntax (Module, parseModuleFile)+import Language.Rzk.Free.Syntax (RzkPosition (RzkPosition),+ VarIdent (getVarIdent))+import Language.Rzk.Syntax (Module, VarIdent' (VarIdent),+ parseModuleFile, printTree) import Language.Rzk.VSCode.Env import Language.Rzk.VSCode.State (ProjectConfig (include)) import Rzk.TypeCheck@@ -121,7 +133,7 @@ (Just []) -- related information Nothing -- data that is preserved between different calls where- msg = ppTypeErrorInScopedContext' err+ msg = ppTypeErrorInScopedContext' TopDown err extractLineNumber :: TypeErrorInScopedContext var -> Maybe Int extractLineNumber (PlainTypeError e) = do@@ -142,3 +154,40 @@ Nothing (Just []) Nothing++instance Default T.Text where def = ""+instance Default CompletionItem+instance Default CompletionItemLabelDetails++provideCompletions :: Handler LSP 'Method_TextDocumentCompletion+provideCompletions req res = do+ root <- getRootPath+ let rootDir = fromMaybe "/" root+ cachedModules <- getCachedTypecheckedModules+ let currentFile = fromMaybe "" $ uriToFilePath $ req ^. params . textDocument . uri+ -- Take all the modules up to and including the currently open one+ let modules = takeWhileInc ((/= currentFile) . fst) cachedModules+ where+ takeWhileInc _ [] = []+ takeWhileInc p (x:xs)+ | p x = x : takeWhileInc p xs+ | otherwise = [x]++ let items = concatMap (declsToItems rootDir) modules+ res $ Right $ InL items+ where+ declsToItems :: FilePath -> (FilePath, [Decl']) -> [CompletionItem]+ declsToItems root (path, decls) = map (declToItem root path) decls+ declToItem :: FilePath -> FilePath -> Decl' -> CompletionItem+ declToItem rootDir path (Decl name type' _ _ _) = def+ & label .~ T.pack (printTree $ getVarIdent name)+ & detail ?~ T.pack (show type')+ & documentation ?~ InR (MarkupContent MarkupKind_Markdown $ T.pack $+ "---\nDefined" +++ (if line > 0 then " at line " ++ show line else "")+ ++ " in *" ++ makeRelative rootDir path ++ "*")+ where+ (VarIdent pos _) = getVarIdent name+ (RzkPosition _path pos') = pos+ line = maybe 0 fst pos'+ _col = maybe 0 snd pos'
src/Language/Rzk/VSCode/Lsp.hs view
@@ -58,6 +58,7 @@ -- ms = mkMarkdown "Hello world" -- range' = Range pos pos -- responder (Right $ InL rsp)+ , requestHandler SMethod_TextDocumentCompletion provideCompletions , requestHandler SMethod_TextDocumentSemanticTokensFull $ \req responder -> do let doc = req ^. params . textDocument . uri . to toNormalizedUri mdoc <- getVirtualFile doc
src/Rzk/Main.hs view
@@ -35,7 +35,7 @@ putStrLn "An error occurred when typechecking!" putStrLn $ unlines [ "Type Error:"- , ppTypeErrorInScopedContext' err+ , ppTypeErrorInScopedContext' BottomUp err ] exitFailure Right _declsByPath -> putStrLn "Everything is ok!"@@ -93,7 +93,7 @@ , "Rendering type error... (this may take a few seconds)" , unlines [ "Type Error:"- , ppTypeErrorInScopedContext' err+ , ppTypeErrorInScopedContext' BottomUp err ] ] Right _ -> pure "Everything is ok!"
src/Rzk/TypeCheck.hs view
@@ -12,6 +12,7 @@ import Control.Applicative ((<|>)) import Control.Monad.Except import Control.Monad.Reader+import Data.Bifunctor (first) import Data.List (intercalate, intersect, nub, tails, (\\)) import Data.Maybe (catMaybes, fromMaybe, isNothing,@@ -63,10 +64,10 @@ typecheckModulesWithLocation' = \case [] -> return ([], []) m@(path, _) : ms -> do- declsE <- (Right <$> typecheckModuleWithLocation m) `catchError` (return . Left)- case declsE of- Left err -> return ([], [err])- Right decls -> do+ (decls, errs) <- typecheckModuleWithLocation m+ case errs of+ _:_ -> return ([(path, decls)], errs)+ _ -> do localDeclsPrepared decls $ do (decls', errors) <- typecheckModulesWithLocation' ms return ((path, decls) : decls', errors)@@ -75,19 +76,27 @@ typecheckModulesWithLocation = \case [] -> return [] m@(path, _) : ms -> do- decls <- typecheckModuleWithLocation m- localDeclsPrepared decls $- ((path, decls) :) <$> typecheckModulesWithLocation ms+ (decls, errs) <- typecheckModuleWithLocation m+ if null errs+ then+ localDeclsPrepared decls $+ ((path, decls) :) <$> typecheckModulesWithLocation ms+ else+ return [(path, decls)] typecheckModules :: [Rzk.Module] -> TypeCheck VarIdent [Decl'] typecheckModules = \case [] -> return [] m : ms -> do- decls <- typecheckModule Nothing m- localDeclsPrepared decls $- (decls <>) <$> typecheckModules ms+ (decls, errs) <- typecheckModule Nothing m+ if null errs+ then+ localDeclsPrepared decls $+ (decls <>) <$> typecheckModules ms+ else+ return decls -typecheckModuleWithLocation :: (FilePath, Rzk.Module) -> TypeCheck VarIdent [Decl']+typecheckModuleWithLocation :: (FilePath, Rzk.Module) -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) typecheckModuleWithLocation (path, module_) = do traceTypeCheck Normal ("Checking module from " <> path) $ do withLocation (LocationInfo { locationFilePath = Just path, locationLine = Nothing }) $@@ -96,15 +105,15 @@ countCommands :: Integral a => [Rzk.Command] -> a countCommands = fromIntegral . length -typecheckModule :: Maybe FilePath -> Rzk.Module -> TypeCheck VarIdent [Decl']+typecheckModule :: Maybe FilePath -> Rzk.Module -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) typecheckModule path (Rzk.Module _moduleLoc _lang commands) = withSection Nothing (go 1 commands) $ -- FIXME: use module name? or anonymous section?- return []+ return ([], []) where totalCommands = countCommands commands - go :: Integer -> [Rzk.Command] -> TypeCheck VarIdent [Decl']- go _i [] = return []+ go :: Integer -> [Rzk.Command] -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent])+ go _i [] = return ([], []) go i (command@(Rzk.CommandUnsetOption _loc optionName) : moreCommands) = do traceTypeCheck Normal ("[ " <> show i <> " out of " <> show totalCommands <> " ]"@@ -129,7 +138,7 @@ ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT term' <- typecheck (toTerm' (addParams params term)) ty' >>= whnfT let decl = Decl (varIdentAt path name) ty' (Just term') False (varIdentAt path <$> vars)- fmap (decl :) $+ fmap (first (decl :)) $ localDeclPrepared decl $ do Context{..} <- ask termSVG <-@@ -148,7 +157,7 @@ paramDecls <- concat <$> mapM paramToParamDecl params ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT let decl = Decl (varIdentAt path name) ty' Nothing False (varIdentAt path <$> vars)- fmap (decl :) $+ fmap (first (decl :)) $ localDeclPrepared decl $ go (i + 1) moreCommands @@ -185,7 +194,7 @@ withCommand command $ do ty' <- typecheck (toTerm' ty) universeT let decls = [ Decl (varIdentAt path name) ty' Nothing True [] | name <- names ]- fmap (decls <>) $+ fmap (first (decls <>)) $ localDeclsPrepared decls $ go (i + 1) moreCommands @@ -404,21 +413,22 @@ , " " <> Rzk.printTree (getVarIdent name) ] -ppTypeErrorInContext :: TypeErrorInContext VarIdent -> String-ppTypeErrorInContext TypeErrorInContext{..} = intercalate "\n"- [ ppContext' typeErrorContext- , ppTypeError' typeErrorError+ppTypeErrorInContext :: OutputDirection -> TypeErrorInContext VarIdent -> String+ppTypeErrorInContext dir TypeErrorInContext{..} = block dir+ [ ppTypeError' typeErrorError+ , ppContext' dir typeErrorContext ] ppTypeErrorInScopedContextWith'- :: [VarIdent]+ :: OutputDirection -> [VarIdent]+ -> [VarIdent] -> TypeErrorInScopedContext VarIdent -> String-ppTypeErrorInScopedContextWith' used vars = \case- PlainTypeError err -> ppTypeErrorInContext err+ppTypeErrorInScopedContextWith' dir used vars = \case+ PlainTypeError err -> ppTypeErrorInContext dir err ScopedTypeError orig err -> withFresh orig $ \(x, xs) ->- ppTypeErrorInScopedContextWith' (x:used) xs $ fmap (g x) err+ ppTypeErrorInScopedContextWith' dir (x:used) xs $ fmap (g x) err where g x Z = x g _ (S y) = y@@ -431,8 +441,9 @@ where z' = refreshVar used z -- FIXME: inefficient -ppTypeErrorInScopedContext' :: TypeErrorInScopedContext VarIdent -> String-ppTypeErrorInScopedContext' err = ppTypeErrorInScopedContextWith' vars (defaultVarIdents \\ vars) err+ppTypeErrorInScopedContext' :: OutputDirection -> TypeErrorInScopedContext VarIdent -> String+ppTypeErrorInScopedContext' dir err =+ ppTypeErrorInScopedContextWith' dir vars (defaultVarIdents \\ vars) err where vars = nub (foldMap pure err) @@ -669,36 +680,46 @@ varOrigs :: Context var -> [(var, Maybe VarIdent)] varOrigs = map (fmap varOrig) . varInfos +withPartialDecls+ :: TypeCheck VarIdent ([Decl'], [err])+ -> TypeCheck VarIdent ([Decl'], [err])+ -> TypeCheck VarIdent ([Decl'], [err])+withPartialDecls tc next = do+ (decls, errs) <- tc+ if null errs+ then first (decls <>)+ <$> localDeclsPrepared decls next+ else return (decls, errs)+ withSection :: Maybe Rzk.SectionName- -> TypeCheck VarIdent [Decl VarIdent]- -> TypeCheck VarIdent [Decl VarIdent]- -> TypeCheck VarIdent [Decl VarIdent]-withSection name sectionBody next = do- sectionDecls <- startSection name $ do- decls <- sectionBody+ -> TypeCheck VarIdent ([Decl VarIdent], [TypeErrorInScopedContext VarIdent])+ -> TypeCheck VarIdent ([Decl VarIdent], [TypeErrorInScopedContext VarIdent])+ -> TypeCheck VarIdent ([Decl VarIdent], [TypeErrorInScopedContext VarIdent])+withSection name sectionBody =+ withPartialDecls $ startSection name $ do+ (decls, errs) <- sectionBody localDeclsPrepared decls $ performing (ActionCloseSection name) $ do- endSection- fmap (sectionDecls <>) $- localDeclsPrepared sectionDecls $- next+ (\ decls' -> (decls', errs)) <$> endSection errs startSection :: Maybe Rzk.SectionName -> TypeCheck VarIdent a -> TypeCheck VarIdent a startSection name = local $ \Context{..} -> Context { localScopes = ScopeInfo { scopeName = name, scopeVars = [] } : localScopes , .. } -endSection :: TypeCheck VarIdent [Decl VarIdent]-endSection = askCurrentScope >>= scopeToDecls+endSection :: [TypeErrorInScopedContext VarIdent] -> TypeCheck VarIdent [Decl']+endSection errs = askCurrentScope >>= scopeToDecls errs -scopeToDecls :: Eq var => ScopeInfo var -> TypeCheck var [Decl var]-scopeToDecls ScopeInfo{..} = do- decls <- collectScopeDecls [] scopeVars- forM_ decls $ \Decl{..} -> do- let unusedUsedVars = declUsedVars `intersect` map fst scopeVars- when (not (null unusedUsedVars)) $- issueTypeError $ TypeErrorUnusedUsedVariables unusedUsedVars declName+scopeToDecls :: Eq var => [TypeErrorInScopedContext VarIdent] -> ScopeInfo var -> TypeCheck var [Decl var]+scopeToDecls errs ScopeInfo{..} = do+ decls <- collectScopeDecls errs [] scopeVars+ -- only issue unused variable errors if there were no errors prior in the section+ when (null errs) $ do+ forM_ decls $ \Decl{..} -> do+ let unusedUsedVars = declUsedVars `intersect` map fst scopeVars+ when (not (null unusedUsedVars)) $+ issueTypeError $ TypeErrorUnusedUsedVariables unusedUsedVars declName return decls insertExplicitAssumptionFor@@ -759,16 +780,18 @@ } xs' = map (fmap (insertExplicitAssumptionFor' a (x, xInfo))) xs -collectScopeDecls :: Eq var => [(var, VarInfo var)] -> [(var, VarInfo var)] -> TypeCheck var [Decl var]-collectScopeDecls recentVars (decl@(var, VarInfo{..}) : vars)+collectScopeDecls :: Eq var => [TypeErrorInScopedContext VarIdent] -> [(var, VarInfo var)] -> [(var, VarInfo var)] -> TypeCheck var [Decl var]+collectScopeDecls errs recentVars (decl@(var, VarInfo{..}) : vars) | varIsAssumption = do (used, recentVars') <- makeAssumptionExplicit decl recentVars- when (not used) $ do- issueTypeError $ TypeErrorUnusedVariable var varType- collectScopeDecls recentVars' vars+ -- only issue unused vars error if there were no other errors previously+ when (null errs) $ do+ when (not used) $ do+ issueTypeError $ TypeErrorUnusedVariable var varType+ collectScopeDecls errs recentVars' vars | otherwise = do- collectScopeDecls (decl : recentVars) vars-collectScopeDecls recentVars [] = return (toDecl <$> recentVars)+ collectScopeDecls errs (decl : recentVars) vars+collectScopeDecls _ recentVars [] = return (toDecl <$> recentVars) where toDecl (var, VarInfo{..}) = Decl { declName = var@@ -789,21 +812,27 @@ where newDeclType = typeFunT varOrig varType Nothing (abstract var declType) -ppContext' :: Context VarIdent -> String-ppContext' ctx@Context{..} = unlines- [ "Definitions in context:"- , unlines- [ show (Pure x :: Term') <> " : " <> show (untyped ty)- | (x, ty) <- reverse (varTypes ctx) ]--- , unlines--- [ show (Pure x :: Term') <> " = " <> show (untyped term)--- | (x, Just term) <- reverse varValues ]- , intercalate "\n" (map (("when " <>) . ppAction 0) (reverse actionStack))- , "Local tope context:"- , intercalate "\n" (map ((" " <>) . show . untyped) localTopes)- , case location of- Just (LocationInfo (Just path) _) -> "\n" <> path <> ":"- _ -> ""+data OutputDirection = TopDown | BottomUp++block :: OutputDirection -> [String] -> String+block TopDown = intercalate "\n"+block BottomUp = intercalate "\n" . reverse++namedBlock :: OutputDirection -> String -> [String] -> String+namedBlock dir name lines_ = block dir $+ name : map indent lines_+ where+ indent = intercalate "\n" . (map (" " ++)) . lines+++ppContext' :: OutputDirection -> Context VarIdent -> String+ppContext' dir ctx@Context{..} = block dir+ [ case location of+ Just (LocationInfo (Just path) (Just lineNo)) ->+ path <> " (line " <> show lineNo <> "):"+ Just (LocationInfo (Just path) _) ->+ path <> ":"+ _ -> "" , case currentCommand of Just (Rzk.CommandDefine _loc name _vars _params _ty _term) -> " Error occurred when checking\n #define " <> Rzk.printTree name@@ -827,9 +856,21 @@ " Error occurred when checking\n #section " <> Rzk.printTree name Just (Rzk.CommandSectionEnd _loc name) -> " Error occurred when checking\n #end " <> Rzk.printTree name- Nothing -> " Error occurred"--- , "Local tope context (expanded):"--- , intercalate "\n" (map ((" " <>) . show . untyped) (intercalate [TopeAndT topeT topeBottomT topeBottomT] (saturateTopes [] <$> simplifyLHS localTopes)))+ Nothing -> " Error occurred outside of any command!"+ , ""+ , case filter (/= topeTopT) localTopes of+ [] -> "Local tope context is unrestricted (⊤)."+ localTopes' -> namedBlock TopDown "Local tope context:"+ [ " " <> show (untyped tope)+ | tope <- localTopes' ]+ , ""+ , block dir+ [ "when " <> ppAction 0 action+ | action <- actionStack ]+ , namedBlock TopDown "Definitions in context:"+ [ block dir+ [ show (Pure x :: Term') <> " : " <> show (untyped ty)+ | (x, ty) <- reverse (varTypes ctx) ] ] ] doesShadowName :: VarIdent -> TypeCheck var [VarIdent]@@ -858,12 +899,17 @@ withLocation :: LocationInfo -> TypeCheck var a -> TypeCheck var a withLocation loc = local $ \Context{..} -> Context { location = Just loc, .. } -withCommand :: Rzk.Command -> TypeCheck var a -> TypeCheck var a-withCommand command = local $ \Context{..} -> Context- { currentCommand = Just command- , location = updatePosition (Rzk.hasPosition command) <$> location- , .. }+withCommand :: Rzk.Command -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent])+withCommand command tc = local f $ do+ result <- (Right <$> tc) `catchError` (return . Left)+ case result of+ Left err -> return ([], [err])+ Right (decls, errs) -> return (decls, errs) where+ f Context{..} = Context+ { currentCommand = Just command+ , location = updatePosition (Rzk.hasPosition command) <$> location+ , .. } updatePosition pos loc = loc { locationLine = fst <$> pos } localDecls :: [Decl VarIdent] -> TypeCheck VarIdent a -> TypeCheck VarIdent a@@ -917,15 +963,15 @@ entailM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool entailM topes tope = do- genTopes <- generateTopesForPointsM (allTopePoints tope)- let topes' = nubTermT (topes <> genTopes)+ -- genTopes <- generateTopesForPointsM (allTopePoints tope)+ let topes' = nubTermT topes -- (topes <> genTopes) topes'' = simplifyLHSwithDisjunctions topes' topes''' = saturateTopes (allTopePoints tope) <$> topes''- -- prettyTopes <- mapM ppTermInContext (saturateTopes (allTopePoints tope) (simplifyLHS topes'))- -- prettyTope <- ppTermInContext =<< nfTope tope- return $- -- trace ("entail " <> intercalate ", " prettyTopes <> " |- " <> prettyTope) $- all (`solveRHS` tope) topes'''+ prettyTopes <- mapM ppTermInContext (saturateTopes (allTopePoints tope) (simplifyLHS topes'))+ prettyTope <- ppTermInContext tope+ traceTypeCheck Debug+ ("entail " <> intercalate ", " prettyTopes <> " |- " <> prettyTope) $+ and <$> mapM (`solveRHSM` tope) topes''' entailTraceM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool entailTraceM topes tope = do@@ -1106,6 +1152,54 @@ simplifyLHS (topeEQT x x' : topeEQT y y' : topes') t : topes' -> t : simplifyLHS topes' +solveRHSM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool+solveRHSM topes tope =+ case tope of+ _ | topeBottomT `elem` topes -> return True+ TopeTopT{} -> return True+ TopeEQT _ty (PairT _ty1 x y) (PairT _ty2 x' y') ->+ solveRHSM topes $ topeAndT+ (topeEQT x x')+ (topeEQT y y')+ TopeEQT _ty (PairT TypeInfo{ infoType = CubeProductT _ cubeI cubeJ } x y) r ->+ solveRHSM topes $ topeAndT+ (topeEQT x (firstT cubeI r))+ (topeEQT y (secondT cubeJ r))+ TopeEQT _ty l (PairT TypeInfo{ infoType = CubeProductT _ cubeI cubeJ } x y) ->+ solveRHSM topes $ topeAndT+ (topeEQT (firstT cubeI l) x)+ (topeEQT (secondT cubeJ l) y)+ TopeEQT _ty l r+ | or+ [ l == r+ , tope `elem` topes+ , topeEQT r l `elem` topes+ ] -> return True+ TopeLEQT _ty l r+ | l == r -> return True+ | solveRHS topes (topeEQT l r) -> return True+ | solveRHS topes (topeEQT l cube2_0T) -> return True+ | solveRHS topes (topeEQT r cube2_1T) -> return True+ TopeAndT _ l r -> (&&)+ <$> solveRHSM topes l+ <*> solveRHSM topes r+ _ | tope `elem` topes -> return True+ TopeOrT _ l r -> do+ l' <- solveRHSM topes l+ r' <- solveRHSM topes r+ if (l' || r')+ then return True+ else do+ lems <- generateTopesForPointsM (allTopePoints tope)+ let lems' = [ lem | lem@(TopeOrT _ t1 t2) <- lems, all (`notElem` topes) [t1, t2] ]+ case lems' of+ TopeOrT _ t1 t2 : _ -> do+ l'' <- solveRHSM (saturateTopes [] (t1 : topes)) tope+ r'' <- solveRHSM (saturateTopes [] (t2 : topes)) tope+ return (l'' && r'')+ _ -> return False+ _ -> return False+ solveRHS :: Eq var => [TermT var] -> TermT var -> Bool solveRHS topes tope = case tope of@@ -2634,10 +2728,7 @@ unsafeTypeCheck' :: TypeCheck VarIdent a -> a unsafeTypeCheck' tc = case defaultTypeCheck tc of- Left err -> error $ intercalate "\n"- [ "Type Error:"- , ppTypeErrorInScopedContext' err- ]+ Left err -> error $ ppTypeErrorInScopedContext' BottomUp err Right result -> result type PointId = String