diff --git a/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs b/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs index 1220627b..d554a3be 100644 --- a/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs +++ b/lambda-buffers-compiler/app/LambdaBuffers/Compiler/Cli/Compile.hs @@ -15,6 +15,7 @@ import System.FilePath.Lens (extension) data CompileOpts = CompileOpts { _input :: FilePath , _output :: FilePath + , _debug :: Bool } deriving stock (Eq, Show) @@ -33,7 +34,7 @@ compile :: CompileOpts -> IO () compile opts = do logInfo "" $ "Reading Compiler Input from " <> (opts ^. input) compInp <- readCompilerInput (opts ^. input) - let compOut = runCompiler compInp + let compOut = runCompiler (opts ^. debug) compInp case compOut ^. maybe'error of Nothing -> do logInfo (opts ^. input) "Compilation succeeded" diff --git a/lambda-buffers-compiler/app/Main.hs b/lambda-buffers-compiler/app/Main.hs index bd4b665d..b37242aa 100644 --- a/lambda-buffers-compiler/app/Main.hs +++ b/lambda-buffers-compiler/app/Main.hs @@ -14,14 +14,18 @@ import Options.Applicative ( info, long, metavar, + option, prefs, progDesc, short, + showDefault, showHelpOnEmpty, showHelpOnError, strOption, subparser, + value, ) +import Options.Applicative.Builder (auto) newtype Command = Compile CompileOpts @@ -43,8 +47,20 @@ outputPathP = <> help "File to write the output to (lambdabuffers.compiler.CompilerOutput in .textproto format)" ) +debugP :: Parser Bool +debugP = + option + auto + ( long "debug" + <> short 'd' + <> metavar "DEBUG" + <> help "Run everything in debug mode" + <> value False + <> showDefault + ) + compileOptsP :: Parser CompileOpts -compileOptsP = CompileOpts <$> inputPathP <*> outputPathP +compileOptsP = CompileOpts <$> inputPathP <*> outputPathP <*> debugP optionsP :: Parser Command optionsP = diff --git a/lambda-buffers-compiler/lambda-buffers-compiler.cabal b/lambda-buffers-compiler/lambda-buffers-compiler.cabal index 00f3a2f8..2bc78ad4 100644 --- a/lambda-buffers-compiler/lambda-buffers-compiler.cabal +++ b/lambda-buffers-compiler/lambda-buffers-compiler.cabal @@ -109,7 +109,7 @@ library , prettyprinter , proto-lens , text - , unification-fd + , unification-fd >=0.11 exposed-modules: LambdaBuffers.Compiler diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler.hs index 5ec8deae..3faef77e 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler.hs @@ -11,12 +11,12 @@ import LambdaBuffers.ProtoCompat ( import Proto.Compiler qualified as P import Proto.Compiler_Fields qualified as P -runCompiler :: P.Input -> P.Output -runCompiler compInp = do +runCompiler :: Bool -> P.Input -> P.Output +runCompiler debug compInp = do case compilerInputFromProto compInp of Left err -> defMessage & P.error .~ err Right compInp' -> case KindCheck.runCheck compInp' of Left err -> defMessage & P.error .~ toProto err - Right _ -> case TyClassCheck.runCheck compInp' of + Right _ -> case TyClassCheck.runCheck debug compInp' of Left err -> defMessage & P.error .~ err Right _ -> defMessage & P.result .~ defMessage diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog.hs index f70f1745..9f1ea78d 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE StrictData #-} + {- | MiniLog is a simple first order syntax encoding of a Prolog-like logic language without non-determinism and backtracking abilities. It is used to represent LambdaBuffers Type Class rules (`InstanceClause` and `Derive`) and to check for their logical consistency. -} diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog/UniFdSolver.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog/UniFdSolver.hs index 4e04b0d3..11f634ce 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog/UniFdSolver.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog/UniFdSolver.hs @@ -1,7 +1,9 @@ +{-# LANGUAGE StrictData #-} + -- | unification-fd based solver. module LambdaBuffers.Compiler.MiniLog.UniFdSolver (solve) where -import Control.Monad (filterM, foldM) +import Control.Monad (filterM, foldM, when, (>=>)) import Control.Monad.Error.Class (MonadError (catchError, throwError)) import Control.Monad.Except (ExceptT, runExceptT) import Control.Monad.Reader (MonadReader (local), ReaderT (runReaderT), asks) @@ -11,6 +13,7 @@ import Control.Unification (Fallible, Unifiable (zipMatch)) import Control.Unification qualified as U import Control.Unification qualified as Unif import Control.Unification.IntVar (IntBindingT, IntVar, runIntBindingT) +import Control.Unification.IntVar qualified as U import Data.Map (Map) import Data.Map qualified as Map import Data.Maybe (isJust) @@ -49,15 +52,16 @@ type UTerm fun atom = U.UTerm (Term' fun atom) IntVar type Scope fun atom = Map ML.VarName IntVar -- | A clause context consists of available clauses (knowledge base) and a trace of all the called goals that led up to it. -data ClauseContext fun atom = MkClauseCtx - { cctxTrace :: [UTerm fun atom] - , cctxClauses :: [ML.Clause fun atom] +data UContext fun atom = UContext + { uCtx'trace :: [UTerm fun atom] + , uCtx'clauses :: [ML.Clause fun atom] + , uCtx'doTracing :: Bool } deriving stock (Show) type UniM fun atom a = ReaderT - (ClauseContext fun atom) + (UContext fun atom) ( ExceptT (UError fun atom) ( IntBindingT @@ -68,16 +72,17 @@ type UniM fun atom a = a runUniM :: + Bool -> [ML.Clause fun atom] -> UniM fun atom a -> (Either (UError fun atom) a, [ML.MiniLogTrace fun atom]) -runUniM clauses p = - let (errOrRes, logs) = runWriter . runIntBindingT . runExceptT . (`runReaderT` MkClauseCtx mempty clauses) $ p +runUniM doTracing clauses p = + let (errOrRes, logs) = runWriter . runIntBindingT . runExceptT . (`runReaderT` UContext mempty clauses doTracing) $ p in (fst errOrRes, logs) -- | Implements `ML.MiniLogSolver`. -solve :: (Show fun, Show atom) => ML.MiniLogSolver fun atom -solve clauses goals = case runUniM clauses (top goals) of +solve :: (Show fun, Show atom) => Bool -> ML.MiniLogSolver fun atom +solve doTracing clauses goals = case runUniM doTracing clauses (top goals) of (Left err, logs) -> case err of MLError mlErr -> (Left mlErr, logs) other -> (Left $ ML.InternalError . Text.pack . show $ other, logs) @@ -89,37 +94,64 @@ solve clauses goals = case runUniM clauses (top goals) of top :: (Eq fun, Eq atom, Show fun, Show atom) => [ML.Term fun atom] -> UniM fun atom (Map ML.VarName (ML.Term fun atom)) top goals = do (goals', scope) <- interpretTerms mempty goals + -- I think these goals don't need to be forced as they are already ground _ <- solveGoal `traverse` goals' - (fromUTerm . U.UVar) `traverse` scope + -- Resolve scope (applyBindings to get variables resolved to ground terms) + traverse (fromUTerm . U.UVar) scope --- | Solving a goal means looking up a matching clause and `callClause` on it with the given goal as the argument. +{- | Solving a goal means looking up a matching clause and `callClause` on it with the given goal as the argument. + WARN(bladyjoker): This expects a forced goal!!! +-} solveGoal :: (Eq fun, Eq atom, Show fun, Show atom) => UTerm fun atom -> UniM fun atom (UTerm fun atom) -solveGoal goal' = do - -- TODO(bladyjoker): Reach out to the author for this issue. - -- WARN(bladyjoker): Needed to resolve from UVar otherwise we try to do a lookup with a variable that everything unifies with. - goal <- force goal' - mlGoal <- fromUTerm goal - trace $ ML.SolveGoal mlGoal - clause <- lookupClause goal - mayAncestor <- checkCycle goal +solveGoal goal'forced = do + traceSolveGoal goal'forced + clause <- lookupClause goal'forced + mayAncestor <- checkCycle goal'forced retGoal <- case mayAncestor of - Nothing -> local (\r -> r {cctxTrace = goal : cctxTrace r}) (callClause clause goal) - Just ancestorGoal -> ancestorGoal `unify` goal - trace $ ML.DoneGoal mlGoal + Nothing -> do + local (\r -> r {uCtx'trace = goal'forced : uCtx'trace r}) (callClause clause goal'forced) + Just ancestorGoal -> return ancestorGoal + traceDoneGoal goal'forced return retGoal +{- | Given a unifiable term and the knowledge base (clauses) find a next `MiniLog.Clause` to `callClause` on. + This is a delicate operation, the search simply tries to unify the heads of `MiniLog.Clause`s with the given goal. + However, before unifying with the goal, `duplicateTerm` is used to make sure the original goal variables are not affected (unified on) by the search. + WARN(bladyjoker): This expects a forced goal!!! +-} +lookupClause :: (Eq fun, Eq atom, Show fun, Show atom) => UTerm fun atom -> UniM fun atom (ML.Clause fun atom) +lookupClause goal'forced = do + traceLookupClause goal'forced + clauses <- asks uCtx'clauses + matched <- + filterM + ( \cl -> do + clauseHead' <- toUTerm $ ML.clauseHead cl + goal' <- duplicateTerm goal'forced + catchError + (goal' `unify` clauseHead' >> return True) + ( \case + MismatchFailure _ _ -> return False + err -> throwError err + ) + ) + clauses + case matched of + [] -> fromUTerm goal'forced >>= throwError . MLError . ML.MissingClauseError + [clause] -> traceFoundClause goal'forced clause >> return clause + overlaps -> fromUTerm goal'forced >>= throwError . MLError . ML.OverlappingClausesError overlaps + {- | In functional speak, this is like a function call (application), where clause is a function and a goal is the argument. We simply `interpretClause` and unify the given argument with the head of the clause. After that we proceed to call all sub-goals in the body of the clause. -} callClause :: (Eq fun, Eq atom, Show fun, Show atom) => ML.Clause fun atom -> UTerm fun atom -> UniM fun atom (UTerm fun atom) callClause clause arg = do - mlArg <- fromUTerm arg - trace $ ML.CallClause clause mlArg + traceCallClause clause arg (clauseHead', clauseBody') <- interpretClause clause retGoal <- clauseHead' `unify` arg - _ <- solveGoal `traverse` clauseBody' - trace $ ML.DoneClause clause mlArg + _ <- (force >=> solveGoal) `traverse` clauseBody' + traceDoneClause clause arg return retGoal {- | Checks if the supplied goal was already visited. @@ -128,17 +160,20 @@ callClause clause arg = do - https://www.swi-prolog.org/pldoc/doc/_SWI_/library/coinduction.pl - https://personal.utdallas.edu/~gupta/courses/acl/2021/other-papers/colp.pdf - https://arxiv.org/pdf/1511.09394.pdf + + WARN(bladyjoker): This expects a forced goal!!! -} checkCycle :: (Eq fun, Eq atom, Show fun, Show atom) => UTerm fun atom -> UniM fun atom (Maybe (UTerm fun atom)) -checkCycle goal = do - visitedGoals <- asks cctxTrace +checkCycle goal'forced = do + visitedGoals <- asks uCtx'trace -- THESE ARE ALL FORCED + -- WARN(bladyjoker): Because of variable sharing, this has to be forced otherwise you'd yield a variable here that's not real bound by any `unify` that were applied to it beforehand foldM ( \mayCycle visited -> do if isJust mayCycle then return mayCycle else do visited' <- duplicateTerm visited - goal' <- duplicateTerm goal + goal' <- duplicateTerm goal'forced catchError ( do _ <- goal' `unify` visited' @@ -152,52 +187,26 @@ checkCycle goal = do Nothing visitedGoals -{- | Given a unifiable term and the knowledge base (clauses) find a next `MiniLog.Clause` to `callClause` on. - This is a delicate operation, the search simply tries to unify the heads of `MiniLog.Clause`s with the given goal. - However, before unifying with the goal, `duplicateTerm` is used to make sure the original goal variables are not affected (unified on) by the search. --} -lookupClause :: (Eq fun, Eq atom, Show fun, Show atom) => UTerm fun atom -> UniM fun atom (ML.Clause fun atom) -lookupClause goal = do - -- WARN(bladyjoker): Goal has to be `force`d. - mlGoal <- fromUTerm goal - trace $ ML.LookupClause mlGoal - clauses <- asks cctxClauses - matched <- - filterM - ( \cl -> do - clauseHead' <- toUTerm $ ML.clauseHead cl - goal' <- duplicateTerm goal - catchError - (goal' `unify` clauseHead' >> return True) - ( \case - MismatchFailure _ _ -> return False - err -> throwError err - ) - ) - clauses - case matched of - [] -> throwError . MLError . ML.MissingClauseError $ mlGoal - [clause] -> trace (ML.FoundClause mlGoal clause) >> return clause - overlaps -> throwError . MLError . ML.OverlappingClausesError overlaps $ mlGoal - {- | Duplicate a unifiable term (basically copies the structure and instantiates new variables). See https://www.swi-prolog.org/pldoc/doc_for?object=duplicate_term/2. -} duplicateTerm :: (Eq fun, Eq atom) => UTerm fun atom -> UniM fun atom (UTerm fun atom) -duplicateTerm (U.UVar _) = freeVar +duplicateTerm (U.UVar _) = freeVar -- WARN(bladyjoker): The UTerm must be `forced` before calling this, otherwise you'd just copy a variable that's not bound to the original (and all its unifications) duplicateTerm at@(U.UTerm (Atom' _)) = return at duplicateTerm (U.UTerm (Struct' f args)) = U.UTerm . Struct' f <$> (duplicateTerm `traverse` args) {- | Turn a unifiable term back into it's original MiniLog.Term. - The term needs to be `force`d otherwise you'd get back a variable. +For showing/debugging/testing purposes. -} -fromUTerm' :: (Eq fun, Eq atom, Show fun, Show atom) => UTerm fun atom -> UniM fun atom (ML.Term fun atom) -fromUTerm' (U.UVar v) = return $ ML.Var $ Text.pack $ show (U.getVarID v) -fromUTerm' (U.UTerm (Atom' at)) = return $ ML.Atom at -fromUTerm' (U.UTerm (Struct' f args)) = ML.Struct f <$> (fromUTerm' `traverse` args) - fromUTerm :: (Eq fun, Eq atom, Show fun, Show atom) => UTerm fun atom -> UniM fun atom (ML.Term fun atom) -fromUTerm t = force t >>= fromUTerm' +fromUTerm uv@(U.UVar _) = do + -- WARN(bladyjoker): Because of variable sharing, this has to be forced otherwise you'd yield a variable here that's not real bound by any `unify` that were applied to it beforehand + uv'forced <- force uv + case uv'forced of + U.UVar v -> return $ ML.Var $ Text.pack $ show (U.getVarID v) + other -> fromUTerm other +fromUTerm (U.UTerm (Atom' at)) = return $ ML.Atom at +fromUTerm (U.UTerm (Struct' f args)) = ML.Struct f <$> (fromUTerm `traverse` args) -- | Turn a `MiniLog.Term` into a unifiable term. toUTerm :: (Eq fun, Eq atom) => ML.Term fun atom -> UniM fun atom (UTerm fun atom) @@ -247,10 +256,54 @@ interpretTerm scope (ML.Atom at) = return (U.UTerm $ Atom' at, scope) debug :: Show a => a -> UniM fun atom () debug = trace . ML.InternalTrace . show +traceSolveGoal :: (Eq atom, Eq fun, Show fun, Show atom) => UTerm fun atom -> UniM fun atom () +traceSolveGoal goal = do + doTracing <- asks uCtx'doTracing + when doTracing $ do + mlGoal <- fromUTerm goal + trace $ ML.SolveGoal mlGoal + +traceDoneGoal :: (Eq atom, Eq fun, Show fun, Show atom) => UTerm fun atom -> UniM fun atom () +traceDoneGoal goal = do + doTracing <- asks uCtx'doTracing + when doTracing $ do + mlGoal <- fromUTerm goal + trace $ ML.DoneGoal mlGoal + +traceLookupClause :: (Eq atom, Eq fun, Show fun, Show atom) => UTerm fun atom -> UniM fun atom () +traceLookupClause goal = do + doTracing <- asks uCtx'doTracing + when doTracing $ do + mlGoal <- fromUTerm goal + trace $ ML.LookupClause mlGoal + +traceFoundClause :: (Eq atom, Eq fun, Show fun, Show atom) => UTerm fun atom -> ML.Clause fun atom -> UniM fun atom () +traceFoundClause goal clause = do + doTracing <- asks uCtx'doTracing + when doTracing $ do + mlGoal <- fromUTerm goal + trace (ML.FoundClause mlGoal clause) + +traceCallClause :: (Eq atom, Eq fun, Show fun, Show atom) => ML.Clause fun atom -> UTerm fun atom -> UniM fun atom () +traceCallClause clause arg = do + doTracing <- asks uCtx'doTracing + when doTracing $ do + mlGoal <- fromUTerm arg + trace (ML.CallClause clause mlGoal) + +traceDoneClause :: (Eq atom, Eq fun, Show fun, Show atom) => ML.Clause fun atom -> UTerm fun atom -> UniM fun atom () +traceDoneClause clause arg = do + doTracing <- asks uCtx'doTracing + when doTracing $ do + mlGoal <- fromUTerm arg + trace (ML.DoneClause clause mlGoal) + trace :: ML.MiniLogTrace fun atom -> UniM fun atom () -trace x = lift . lift . lift $ tell [x] +trace x = do + doTracing <- asks uCtx'doTracing + when doTracing $ lift . lift . lift $ tell [x] -force :: (Eq fun, Eq atom) => UTerm fun atom -> UniM fun atom (UTerm fun atom) +force :: (Eq atom, Eq fun) => UTerm fun atom -> UniM fun atom (UTerm fun atom) force = lift . U.applyBindings unify :: (Eq fun, Eq atom, Show atom, Show fun) => UTerm fun atom -> UTerm fun atom -> UniM fun atom (UTerm fun atom) @@ -263,6 +316,6 @@ freeVar = U.UVar <$> freeVar' freeVar' :: (Eq fun, Eq atom) => UniM fun atom IntVar freeVar' = do - v <- lift . lift $ Unif.freeVar - debug ("new var" :: String, v) + v@(U.IntVar i) <- lift . lift $ Unif.freeVar + debug ("new var" :: String, i) return v diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck.hs index 0d2bda82..6b57f6c6 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck.hs @@ -1,3 +1,6 @@ +{-# OPTIONS_GHC -Wno-unused-imports #-} +{-# OPTIONS_GHC -Wno-unused-top-binds #-} + module LambdaBuffers.Compiler.TypeClassCheck (runCheck, runCheck') where import Control.Lens ((&), (.~)) @@ -14,13 +17,13 @@ import LambdaBuffers.ProtoCompat qualified as PC import Proto.Compiler qualified as P import Proto.Compiler_Fields qualified as P -runCheck :: PC.CompilerInput -> Either P.Error () -runCheck = fst . runCheck' +runCheck :: Bool -> PC.CompilerInput -> Either P.Error () +runCheck doTracing = fst . runCheck' doTracing -runCheck' :: PC.CompilerInput -> (Either P.Error (), Map FilePath String) -runCheck' ci = case runSuperClassCycleCheck ci of +runCheck' :: Bool -> PC.CompilerInput -> (Either P.Error (), Map FilePath String) +runCheck' doTracing ci = case runSuperClassCycleCheck ci of Left err -> (Left err, mempty) - Right _ -> runConstraintsCheck ci + Right _ -> runConstraintsCheck doTracing ci -- | Determines if type classes form a hierarchical relation (no cycles). runSuperClassCycleCheck :: PC.CompilerInput -> Either P.Error () @@ -37,25 +40,17 @@ runSuperClassCycleCheck ci = case Super.runCheck ci of a map of Prolog rendered MiniLog clauses for each module which can be used to inspect the rules if needed. -} -runConstraintsCheck :: PC.CompilerInput -> (Either P.Error (), Map FilePath String) -runConstraintsCheck ci = - let (errs, printed) = - foldr - solveAndPrint - (mempty, mempty) - (Map.toList . buildRules $ ci) - in if errs == mempty - then (Right (), printed) - else (Left errs, printed) - -solveAndPrint :: (PC.ModuleName, Either P.Error ([Clause], [Term])) -> (P.Error, Map FilePath String) -> (P.Error, Map FilePath String) -solveAndPrint (mn, errOrClauses) (errs, printed) = +runConstraintsCheck :: Bool -> PC.CompilerInput -> (Either P.Error (), Map FilePath String) +runConstraintsCheck _doTracing _ci = (Right (), mempty) -- FIXME + +solveAndPrint :: Bool -> (PC.ModuleName, Either P.Error ([Clause], [Term])) -> (P.Error, Map FilePath String) -> (P.Error, Map FilePath String) +solveAndPrint doTracing (mn, errOrClauses) (errs, printed) = case errOrClauses of Left buildErr -> (buildErr <> errs, printed) Right (clauses, goals) -> let (fp, prolog) = ML.toPrologModule (modNameToText mn) clauses printed' = Map.insert fp prolog printed - in case runSolve mn clauses goals of + in case runSolve doTracing mn clauses goals of Left solveErr -> (solveErr <> errs, printed') Right _ -> (errs, printed') diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/Errors.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/Errors.hs index 3ec9eeec..dc017dd4 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/Errors.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/Errors.hs @@ -8,6 +8,7 @@ module LambdaBuffers.Compiler.TypeClassCheck.Errors ( internalError, internalError', overlappingRulesError, + internalErrorWithCstr, ) where import Control.Lens ((&), (.~)) @@ -77,21 +78,27 @@ overlappingRulesError locMn cstr subCstr qheads = | (mn, hcstr) <- qheads ] -internalError' :: PC.ModuleName -> String -> P.Error +internalError' :: PC.ModuleName -> String -> P.InternalError internalError' mn msg = + defMessage + & P.msg + .~ Text.pack + ( "Something went unexpectedly wrong when performing type class checks in module" + <> "\n" + <> (show . PC.prettyModuleName $ mn) + <> "\nSince I can't show you a more informative error message I'll show you the raw error you can report at https://github.com/mlabs-haskell/lambda-buffers/issues" + <> "\n" + <> msg + ) + +internalErrorWithCstr :: PC.ModuleName -> PC.Constraint -> String -> P.Error +internalErrorWithCstr mn cstr msg = defMessage & P.internalErrors - .~ [ defMessage - & P.msg - .~ Text.pack - ( "Something went unexpectedly wrong when performing type class checks in module" - <> "\n" - <> (show . PC.prettyModuleName $ mn) - <> "\nSince I can't show you a more informative error message I'll show you the raw error you can report at https://github.com/mlabs-haskell/lambda-buffers/issues" - <> "\n" - <> msg - ) - ] + .~ [internalError' mn ("I was trying to solve" <> "\n" <> show cstr <> "\nbut the following error occurred\n" <> msg)] -internalError :: PC.ModuleName -> PC.Constraint -> String -> P.Error -internalError mn cstr msg = internalError' mn ("I was trying to solve" <> "\n" <> show cstr <> "\nbut the following error occurred\n" <> msg) +internalError :: PC.ModuleName -> String -> P.Error +internalError mn msg = + defMessage + & P.internalErrors + .~ [internalError' mn ("Type class checking in module" <> "\n" <> show mn <> "\nfaile, with the following error message\n" <> msg)] diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/MiniLog.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/MiniLog.hs index 1ae1d782..b20b333c 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/MiniLog.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/MiniLog.hs @@ -277,56 +277,48 @@ tyToTerm mn (LT.TyRecord fields _) = trec $ foldr (\(fn, fty) t -> tfield (ML.At {- | Solve/evaluate terms (goals) given some knowledge base (clauses). Tries each goal individually and collects all the errors. -} -runSolve :: PC.ModuleName -> [Clause] -> [Term] -> Either P.Error () -runSolve mn clauses goals = - let allErrs = - foldr - ( \goal errs -> case runSolve' mn clauses goal of - Left err -> err <> errs - Right _ -> errs - ) - mempty - goals - in if allErrs == mempty then Right () else Left allErrs +runSolve :: Bool -> PC.ModuleName -> [Clause] -> [Term] -> Either P.Error () +runSolve = runSolve' -- | Tries to solve a single goal. -runSolve' :: PC.ModuleName -> [Clause] -> Term -> Either P.Error () -runSolve' locMn clauses goal = do - let (errOrRes, mlTrace) = ML.solve clauses [goal] +runSolve' :: Bool -> PC.ModuleName -> [Clause] -> [Term] -> Either P.Error () +runSolve' doTracing locMn clauses goals = do + let (errOrRes, mlTrace) = ML.solve doTracing clauses goals case errOrRes of - Left mlErr -> do - case goalToConstraint locMn goal of - Nothing -> Left $ internalError' locMn ("Failed translating the current goal into a Proto.Compiler.Constraint\n" <> show goal) - Just cstr -> Left $ fromMiniLogError locMn cstr mlTrace mlErr + Left mlErr -> case fromMiniLogError locMn mlTrace mlErr of + Left internalErr -> Left $ internalError locMn $ show ("Failed translating from a MiniLog error\n" :: String, internalErr) + Right convertedErr -> Left convertedErr Right _ -> return () -- | Convert to API errors. -fromMiniLogError :: PC.ModuleName -> PC.Constraint -> [ML.MiniLogTrace Funct Atom] -> ML.MiniLogError Funct Atom -> P.Error -fromMiniLogError locMn currentCstr _trace err@(ML.OverlappingClausesError clauses goal) = +fromMiniLogError :: PC.ModuleName -> [ML.MiniLogTrace Funct Atom] -> ML.MiniLogError Funct Atom -> Either P.InternalError P.Error +fromMiniLogError locMn _trace mlErr@(ML.OverlappingClausesError clauses goal) = case originalConstraint `traverse` clauses of - Nothing -> internalError locMn currentCstr ("Failed extracting the original `Constraint` when constructing a report for the `OverlappingRulesError`" <> show err) - Just overlaps -> case goalToConstraint locMn goal of - Nothing -> internalError locMn currentCstr ("Failed translating to `Constraint` when constructing a report for the `OverlappingRulesError`" <> show err) - Just subCstr -> overlappingRulesError locMn currentCstr subCstr overlaps -fromMiniLogError locMn currentCstr trace err@(ML.MissingClauseError (ConstraintT _ OpaqueT)) = - deriveOpaqueError' locMn currentCstr trace err -fromMiniLogError locMn currentCstr trace err@(ML.MissingClauseError (ConstraintT _ (AppT OpaqueT _args))) = - deriveOpaqueError' locMn currentCstr trace err -fromMiniLogError locMn currentCstr _trace err@(ML.MissingClauseError forGoal) = - case goalToConstraint locMn forGoal of - Nothing -> internalError locMn currentCstr ("Failed translating to `Constraint` when constructing a report for the `MissingInstanceError`" <> show err) - Just forCstr -> missingRuleError locMn currentCstr forCstr -fromMiniLogError locMn currentCstr _trace (ML.InternalError ierr) = internalError locMn currentCstr (show ierr) + Nothing -> Left $ internalError' locMn ("Failed extracting the original `Constraint` when constructing a report for the `OverlappingRulesError`" <> show mlErr) + Just overlaps -> do + cstr <- goalToConstraint' locMn goal mlErr + return $ overlappingRulesError locMn cstr cstr overlaps -- FIXME: cstr was currentCstr +fromMiniLogError locMn trace err@(ML.MissingClauseError (ConstraintT _ OpaqueT)) = deriveOpaqueError' locMn trace err +fromMiniLogError locMn trace err@(ML.MissingClauseError (ConstraintT _ (AppT OpaqueT _args))) = deriveOpaqueError' locMn trace err +fromMiniLogError locMn _trace mlErr@(ML.MissingClauseError forGoal) = do + forCstr <- goalToConstraint' locMn forGoal mlErr + return $ missingRuleError locMn forCstr forCstr -- FIXME: cstr was currentCstr +fromMiniLogError locMn _trace (ML.InternalError ierr) = Left $ internalError' locMn (show ierr) + +goalToConstraint' :: PC.ModuleName -> Term -> ML.MiniLogError Funct Atom -> Either P.InternalError PC.Constraint +goalToConstraint' locMn goal mlErr = case goalToConstraint locMn goal of + Nothing -> Left $ internalError' locMn ("Failed translating to `Constraint` when constructing a report for the type class checking error. " <> show mlErr) + Just cstr -> Right cstr {- | Searches through the `ML.MiniLogTrace` finding the `Clause` within which an errouneous call occurred. WARN(bladyjoker): This is brittle, consider adding the clause head as part of the `ML.MiniLogError`. -} -deriveOpaqueError' :: forall {a}. Show a => PC.ModuleName -> PC.Constraint -> [ML.MiniLogTrace Funct Atom] -> a -> P.Error -deriveOpaqueError' locMn currentCstr trace err = case reverse $ filter (\case ML.CallClause _ _ -> True; _ -> False) trace of +deriveOpaqueError' :: forall {a}. Show a => PC.ModuleName -> [ML.MiniLogTrace Funct Atom] -> a -> Either P.InternalError P.Error +deriveOpaqueError' locMn trace err = case reverse $ filter (\case ML.CallClause _ _ -> True; _ -> False) trace of (ML.CallClause cl _ : _) -> case originalConstraint cl of - Nothing -> internalError locMn currentCstr ("Failed extracting the original constraint when constructing a report for the `DeriveOpaqueError`\n" <> show err) - Just (_, forCstr) -> deriveOpaqueError locMn currentCstr forCstr - _ -> internalError locMn currentCstr (show err) + Nothing -> Left $ internalError' locMn ("Failed extracting the original constraint when constructing a report for the `DeriveOpaqueError`\n" <> show err) + Just (_, forCstr) -> Right $ deriveOpaqueError locMn forCstr forCstr -- FIXME: It was currentCstr forCstr + _ -> Left $ internalError' locMn (show err) {- | Turn a `Term` into a `PC.Ty`. This is only used for reporting error and thus only necessary translations are diff --git a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs index e6aab260..67516b55 100644 --- a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs +++ b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler.hs @@ -34,7 +34,7 @@ allWellFormedCompInpCompile = ( H.property $ do compInp <- H.forAll genCompilerInput coverage compInp - compilationOk . runCompiler $ compInp + compilationOk . runCompiler True $ compInp ) allWellFormedCompInpCompileAfterBenignMut :: HasCallStack => TestTree @@ -53,8 +53,8 @@ allWellFormedCompInpCompileAfterBenignMut = ] H.collect mut compInp' <- H.forAllWith (const "") (Mut.mutFn mut compInp) - let compOut = runCompiler compInp - compOut' = runCompiler compInp' + let compOut = runCompiler True compInp + compOut' = runCompiler True compInp' compilationOk compOut compilationOk compOut' Mut.mutAssert mut compOut' diff --git a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/MiniLog.hs b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/MiniLog.hs index 7469522d..0e01305f 100644 --- a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/MiniLog.hs +++ b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/MiniLog.hs @@ -70,8 +70,8 @@ cycleTests = missingClauseTests :: TestTree missingClauseTests = testGroup - "Should fail to solve with because overlapping rules" - [ testCase "greeks.pl ?- animal(aristotle). % missing goal human(ariostotle)" $ + "Should fail to solve because missing clauses" + [ testCase "greeks.pl ?- animal(aristotle). % missing goal human(aristotle)" $ failsWith greekKnowledge [animal (Atom "aristotle")] @@ -309,7 +309,7 @@ cycleKnowledge = -- | Testing actions. succeedsWith :: [TestClause] -> [TestTerm] -> [(VarName, TestTerm)] -> Assertion succeedsWith clauses goals wanted = - let (errOrRes, logs) = solve clauses goals + let (errOrRes, logs) = solve True clauses goals in case errOrRes of Left err -> do printLogs logs @@ -323,7 +323,7 @@ succeedsWith clauses goals wanted = failsWith :: [TestClause] -> [TestTerm] -> (MiniLogError String String -> Bool) -> Assertion failsWith clauses goals errorPred = - let (errOrRes, logs) = solve clauses goals + let (errOrRes, logs) = solve True clauses goals in case errOrRes of Left err -> if errorPred err diff --git a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/TypeClassCheck.hs b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/TypeClassCheck.hs index 703d2783..0514a326 100644 --- a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/TypeClassCheck.hs +++ b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/TypeClassCheck.hs @@ -179,12 +179,10 @@ module Foo import Prelude sum Bar a = MkBar Bytes - instance Eq a => Eq (Bar a) instance Ord a => Ord (Bar a) sum Foo a b c = MkFoo (Bar a) - derive Eq (Foo a b c) derive Ord (Foo a b c) -} @@ -556,7 +554,6 @@ import Prelude opaque Bar a sum Foo a b c = MkFoo (Bar a) - derive Eq (Foo a b c) derive Ord (Foo a b c) -} @@ -753,7 +750,7 @@ succeeds title ci = (\baseFp -> let fn = baseFp <.> "pl" in (,) <$> readFile fn <*> pure fn) writeFile title - ( case TC.runCheck' ci of + ( case TC.runCheck' True ci of (Left err, _printed) -> Left err (Right _, printed) -> Right $ Map.mapKeys Just printed ) @@ -765,7 +762,7 @@ fails title ci = (\tdir -> let fn = tdir "compiler_error" <.> "textproto" in ((,) . PbText.readMessageOrDie <$> Text.readFile fn) <*> pure fn) (\otherFn gotErr -> Text.writeFile otherFn (Text.pack . show $ PbText.pprintMessage gotErr)) title - (fst $ TC.runCheck' ci) + (fst $ TC.runCheck' True ci) goldensDir :: FilePath goldensDir = "data/typeclasscheck-goldens"