diff --git a/.gitignore b/.gitignore index de5b100b..d3e8735f 100644 --- a/.gitignore +++ b/.gitignore @@ -82,3 +82,5 @@ tmp/ *.pygtex *.pygstyle + +*/_minted/* \ No newline at end of file diff --git a/cabal.project b/cabal.project new file mode 100644 index 00000000..61141f65 --- /dev/null +++ b/cabal.project @@ -0,0 +1,6 @@ +packages: *.cabal + +source-repository-package + type: git + location: https://github.com/disco-lang/polysemy + tag: db923b90c88374c8de4e597136f0ec3154533677 diff --git a/disco.cabal b/disco.cabal index 01330abe..86f2ff10 100644 --- a/disco.cabal +++ b/disco.cabal @@ -397,7 +397,7 @@ common common library import: common - ghc-options: -flate-specialise -fspecialise-aggressively -fplugin=Polysemy.Plugin + ghc-options: -flate-specialise -fspecialise-aggressively default-extensions: DataKinds DeriveGeneric FlexibleContexts @@ -487,7 +487,6 @@ library -- Need the Alpha and Subst instances for -- NonEmpty from unbound-generics 0.4.4 polysemy >= 1.6.0.0 && < 1.10, - polysemy-plugin >= 0.4 && < 0.5, reflection >= 2.1.7 && < 2.2, random >= 1.2.1.1 && < 1.4, constraints >= 0.13.4 && < 0.15, @@ -503,7 +502,6 @@ library splitmix >= 0.1 && < 0.2, fgl >= 5.5 && < 5.9, optparse-applicative >= 0.12 && < 0.20, - oeis2 >= 1.0.9 && < 1.1, algebraic-graphs >= 0.5 && < 0.8, pretty-show >= 1.10 && < 1.11, boxes >= 0.1.5 && < 0.2, @@ -530,7 +528,6 @@ executable disco unbound-generics >= 0.3 && < 0.5, lens >= 4.14 && < 5.4, optparse-applicative >= 0.12 && < 0.20, - oeis2 >= 1.0.9 && < 1.1 default-language: Haskell2010 diff --git a/example/catalan.disco b/example/catalan.disco index dc19c66a..d39aa943 100644 --- a/example/catalan.disco +++ b/example/catalan.disco @@ -1,5 +1,4 @@ import list -import oeis -- The type of binary tree shapes: empty tree, or a pair of subtrees. type BT = Unit + BT*BT @@ -13,7 +12,3 @@ treesOfSize(k+1) = -- Compute first few Catalan numbers by brute force. catalan1 : List(N) catalan1 = each(\k. length(treesOfSize(k)), [0..4]) - --- Extend the sequence via the OEIS. -catalan : List(N) -catalan = extendSequence(catalan1) \ No newline at end of file diff --git a/src/Disco/AST/Core.hs b/src/Disco/AST/Core.hs index 97184c26..aa8e2744 100644 --- a/src/Disco/AST/Core.hs +++ b/src/Disco/AST/Core.hs @@ -218,10 +218,6 @@ data Op OCrash | -- | No-op/identity function OId - | -- | Lookup OEIS sequence - OLookupSeq - | -- | Extend a List via OEIS - OExtendSeq | -- | Not the Boolean `And`, but instead a propositional BOp -- | Should only be seen and used with Props. OAnd @@ -298,7 +294,7 @@ instance Pretty Core where toTuple :: [Core] -> Core toTuple = foldr CPair CUnit -prettyTestVars :: Members '[Reader PA, LFresh] r => [(String, Type, Name Core)] -> Sem r (Doc ann) +prettyTestVars :: Members '[Reader PA, LFresh] r => [(String, Type, Name Core)] -> Sem r Doc prettyTestVars = brackets . intercalate "," . map prettyTestVar where prettyTestVar (s, ty, n) = parens (intercalate "," [text s, pretty ty, pretty n]) @@ -384,8 +380,6 @@ opToStr = \case OMatchErr -> "matchErr" OCrash -> "crash" OId -> "id" - OLookupSeq -> "lookupSeq" - OExtendSeq -> "extendSeq" OForall {} -> "∀" OExists {} -> "∃" OAnd -> "and" diff --git a/src/Disco/AST/Surface.hs b/src/Disco/AST/Surface.hs index abca2551..68cee5bd 100644 --- a/src/Disco/AST/Surface.hs +++ b/src/Disco/AST/Surface.hs @@ -234,7 +234,7 @@ instance Pretty (Name a, Bind [Pattern] Term) where pretty x <> hcat (map prettyPatternP ps) <+> text "=" <+> setPA initPA (pretty t) -- | Pretty-print a type declaration. -prettyTyDecl :: Members '[Reader PA, LFresh] r => Name t -> Type -> Sem r (Doc ann) +prettyTyDecl :: Members '[Reader PA, LFresh] r => Name t -> Type -> Sem r Doc prettyTyDecl x ty = hsep [pretty x, text ":", pretty ty] ------------------------------------------------------------ @@ -525,7 +525,7 @@ pattern PNonlinear p x <- PNonlinear_ (unembed -> p) x -- term (e.g. via the :doc REPL command). -- | Pretty-print a term with guaranteed parentheses. -prettyTermP :: Members '[LFresh, Reader PA] r => Term -> Sem r (Doc ann) +prettyTermP :: Members '[LFresh, Reader PA] r => Term -> Sem r Doc prettyTermP t@TTup {} = setPA initPA $ pretty t -- prettyTermP t@TContainer{} = setPA initPA $ "" <+> prettyTerm t prettyTermP t = withPA initPA $ pretty t @@ -629,12 +629,12 @@ instance Pretty Term where TWild -> text "_" -- | Print appropriate delimiters for a container literal. -containerDelims :: Member (Reader PA) r => Container -> (Sem r (Doc ann) -> Sem r (Doc ann)) +containerDelims :: Member (Reader PA) r => Container -> (Sem r Doc -> Sem r Doc) containerDelims ListContainer = brackets containerDelims BagContainer = bag containerDelims SetContainer = braces -prettyBranches :: Members '[Reader PA, LFresh] r => [Branch] -> Sem r (Doc ann) +prettyBranches :: Members '[Reader PA, LFresh] r => [Branch] -> Sem r Doc prettyBranches = \case [] -> text "" b : bs -> @@ -680,7 +680,7 @@ instance Pretty Qual where QGuard (unembed -> t) -> pretty t -- | Pretty-print a pattern with guaranteed parentheses. -prettyPatternP :: Members '[LFresh, Reader PA] r => Pattern -> Sem r (Doc ann) +prettyPatternP :: Members '[LFresh, Reader PA] r => Pattern -> Sem r Doc prettyPatternP p@PTup {} = setPA initPA $ pretty p prettyPatternP p = withPA initPA $ pretty p diff --git a/src/Disco/Compile.hs b/src/Disco/Compile.hs index 5bc3830f..00a71905 100644 --- a/src/Disco/Compile.hs +++ b/src/Disco/Compile.hs @@ -359,8 +359,6 @@ compilePrim _ PrimFrac = return $ CConst OFrac compilePrim _ PrimCrash = return $ CConst OCrash compilePrim _ PrimUntil = return $ CConst OUntil compilePrim _ PrimHolds = return $ CConst OHolds -compilePrim _ PrimLookupSeq = return $ CConst OLookupSeq -compilePrim _ PrimExtendSeq = return $ CConst OExtendSeq compilePrim ty PrimMin = desugaredPrimErr PrimMin ty compilePrim ty PrimMax = desugaredPrimErr PrimMax ty diff --git a/src/Disco/Effects/Store.hs b/src/Disco/Effects/Store.hs index 8bdb91ed..de33615d 100644 --- a/src/Disco/Effects/Store.hs +++ b/src/Disco/Effects/Store.hs @@ -1,10 +1,6 @@ {-# LANGUAGE BlockArguments #-} {-# LANGUAGE TemplateHaskell #-} ------------------------------------------------------------------------------ - ------------------------------------------------------------------------------ - -- | -- Module : Disco.Effects.Store -- Copyright : disco team and contributors @@ -18,19 +14,20 @@ module Disco.Effects.Store where import qualified Data.IntMap.Lazy as IntMap import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet +import Data.Proxy import Disco.Effects.Counter import Polysemy import Polysemy.State data Store v m a where - ClearStore :: Store v m () + ClearStore :: Proxy v -> Store v m () New :: v -> Store v m Int LookupStore :: Int -> Store v m (Maybe v) InsertStore :: Int -> v -> Store v m () MapStore :: (v -> v) -> Store v m () AssocsStore :: Store v m [(Int, v)] - KeepKeys :: IntSet -> Store v m () + KeepKeys :: Proxy v -> IntSet -> Store v m () makeSem ''Store @@ -40,7 +37,7 @@ runStore = runCounter . evalState @(IntMap.IntMap v) IntMap.empty . reinterpret2 \case - ClearStore -> put IntMap.empty + ClearStore _ -> put @(IntMap.IntMap v) IntMap.empty New v -> do loc <- fromIntegral <$> next modify $ IntMap.insert loc v @@ -49,4 +46,6 @@ runStore = InsertStore k v -> modify (IntMap.insert k v) MapStore f -> modify (IntMap.map f) AssocsStore -> gets IntMap.assocs - KeepKeys ks -> modify (\m -> IntMap.withoutKeys m (IntMap.keysSet m `IntSet.difference` ks)) + KeepKeys _ ks -> + modify @(IntMap.IntMap v) $ \m -> + IntMap.withoutKeys m (IntMap.keysSet m `IntSet.difference` ks) diff --git a/src/Disco/Error.hs b/src/Disco/Error.hs index 289201bc..388e5cd1 100644 --- a/src/Disco/Error.hs +++ b/src/Disco/Error.hs @@ -78,7 +78,7 @@ deriving instance Show EvalError panic :: Member (Error DiscoError) r => String -> Sem r a panic = throw . Panic -outputDiscoErrors :: Member (Output (Message ann)) r => Sem (Error DiscoError ': r) () -> Sem r () +outputDiscoErrors :: Member (Output Message) r => Sem (Error DiscoError ': r) () -> Sem r () outputDiscoErrors m = do e <- runError m either (err . pretty') return e @@ -102,10 +102,10 @@ instance Pretty DiscoError where , "Please report this as a bug at https://github.com/disco-lang/disco/issues/ ." ] -rtd :: String -> Sem r (Doc ann) +rtd :: String -> Sem r Doc rtd page = "https://disco-lang.readthedocs.io/en/latest/reference/" <> text page <> ".html" --- issue :: Int -> Sem r (Doc ann) +-- issue :: Int -> Sem r Doc -- issue n = "See https://github.com/disco-lang/disco/issues/" <> text (show n) squote :: String -> String @@ -114,7 +114,7 @@ squote x = "'" ++ x ++ "'" cyclicImportError :: Members '[Reader PA, LFresh] r => [ModuleName] -> - Sem r (Doc ann) + Sem r Doc cyclicImportError ms = nest 2 $ vcat @@ -122,7 +122,7 @@ cyclicImportError ms = , intercalate " ->" (map pretty ms) ] -prettyEvalError :: Members '[Reader PA, LFresh] r => EvalError -> Sem r (Doc ann) +prettyEvalError :: Members '[Reader PA, LFresh] r => EvalError -> Sem r Doc prettyEvalError = \case UnboundPanic x -> ("Bug! No variable found named" <+> pretty' x <> ".") @@ -139,7 +139,7 @@ prettyEvalError = \case -- [ ] Step 3: improve error messages according to notes below -- [ ] Step 4: get it to return multiple error messages -- [ ] Step 5: save parse locations, display with errors -prettyTCError :: Members '[Reader PA, LFresh] r => TCError -> Sem r (Doc ann) +prettyTCError :: Members '[Reader PA, LFresh] r => TCError -> Sem r Doc prettyTCError = \case -- XXX include some potential misspellings along with Unbound -- see https://github.com/disco-lang/disco/issues/180 @@ -261,13 +261,12 @@ prettyTCError = \case [ "Error: in the definition of " <> text s <> parens (intercalate "," (map text ss)) <> ": recursive occurrences of" <+> text s <+> "may only have type variables as arguments." , indent 2 - ( text s <> parens (intercalate "," (map pretty' tys)) <+> "does not follow this rule." - ) + (text s <> parens (intercalate "," (map pretty' tys)) <+> "does not follow this rule.") , rtd "no-poly-rec" ] NoError -> empty -conWord :: Con -> Sem r (Doc ann) +conWord :: Con -> Sem r Doc conWord = \case CArr -> "function" CProd -> "pair" @@ -280,7 +279,7 @@ conWord = \case CGraph -> "graph" CUser s -> text s -prettySolveError :: Members '[Reader PA, LFresh] r => SolveError -> Sem r (Doc ann) +prettySolveError :: Members '[Reader PA, LFresh] r => SolveError -> Sem r Doc prettySolveError = \case -- XXX say which types! NoWeakUnifier -> @@ -311,12 +310,12 @@ prettySolveError = \case , rtd "qual-skolem" ] -qualPhrase :: Bool -> Qualifier -> Sem r (Doc ann) +qualPhrase :: Bool -> Qualifier -> Sem r Doc qualPhrase b q | q `elem` [QBool, QBasic, QSimple] = "are" <+> (if b then empty else "not") <+> qualAction q | otherwise = "can" <> (if b then empty else "not") <+> "be" <+> qualAction q -qualAction :: Qualifier -> Sem r (Doc ann) +qualAction :: Qualifier -> Sem r Doc qualAction = \case QNum -> "added and multiplied" QSub -> "subtracted" diff --git a/src/Disco/Eval.hs b/src/Disco/Eval.hs index 16600814..d36b8ca9 100644 --- a/src/Disco/Eval.hs +++ b/src/Disco/Eval.hs @@ -162,10 +162,10 @@ type family AppendEffects (r :: EffectRow) (s :: EffectRow) :: EffectRow where -- However, just manually implementing it here seems easier. -- | Effects needed at the top level. -type TopEffects = '[Error DiscoError, State TopInfo, Output (Message ()), Embed IO, Final (H.InputT IO)] +type TopEffects = '[Error DiscoError, State TopInfo, Output Message, Embed IO, Final (H.InputT IO)] -- | Effects needed for evaluation. -type EvalEffects = [Error EvalError, Random, LFresh, Output (Message ()), State Mem] +type EvalEffects = [Error EvalError, Random, LFresh, Output Message, State Mem] -- XXX write about order. -- memory, counter etc. should not be reset by errors. @@ -191,11 +191,11 @@ runDisco cfg = void . H.runInputT inputSettings . runFinal @(H.InputT IO) - . embedToFinal + . embedToFinal @(H.InputT IO) . runEmbedded @_ @(H.InputT IO) liftIO . runOutputSem (handleMsg msgFilter) -- Handle Output Message via printing to console . stateToIO (initTopInfo cfg) -- Run State TopInfo via an IORef - . inputToState -- Dispatch Input TopInfo effect via State effect + . inputToState @TopInfo -- Dispatch Input TopInfo effect via State effect . runState emptyMem -- Start with empty memory . outputDiscoErrors -- Output any top-level errors . runLFresh -- Generate locally fresh names @@ -293,7 +293,7 @@ typecheckTop tcm = do -- The 'Resolver' argument specifies where to look for imported -- modules. loadDiscoModule :: - Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r => + Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r => Bool -> Resolver -> FilePath -> @@ -307,7 +307,7 @@ loadDiscoModule quiet resolver = -- module loaded from disk). Used for e.g. blocks/modules entered -- at the REPL prompt. loadParsedDiscoModule :: - Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r => + Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r => Bool -> Resolver -> ModuleName -> @@ -321,7 +321,7 @@ loadParsedDiscoModule quiet resolver = -- any imported module more than once. Resolve the module, load and -- parse it, then call 'loadParsedDiscoModule''. loadDiscoModule' :: - Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r => + Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r => Bool -> Resolver -> [ModuleName] -> @@ -353,7 +353,7 @@ stdLib = ["list", "container"] -- 'LoadingMode' parameter is 'REPL'. Recursively load all its -- imports, then typecheck it. loadParsedDiscoModule' :: - Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r => + Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r => Bool -> LoadingMode -> Resolver -> @@ -399,7 +399,7 @@ loadParsedDiscoModule' quiet mode resolver inProcess name cm@(Module _ mns _ _ _ -- | Try loading the contents of a file from the filesystem, emitting -- an error if it's not found. -loadFile :: Members '[Output (Message ann), Embed IO] r => FilePath -> Sem r (Maybe String) +loadFile :: Members '[Output Message, Embed IO] r => FilePath -> Sem r (Maybe String) loadFile file = do res <- liftIO $ handle @SomeException (return . Left) (Right <$> readFile file) case res of @@ -409,7 +409,7 @@ loadFile file = do -- | Add things from the given module to the set of currently loaded -- things. addToREPLModule :: - Members '[Error DiscoError, State TopInfo, Random, State Mem, Output (Message ann)] r => + Members '[Error DiscoError, State TopInfo, Random, State Mem, Output Message] r => ModuleInfo -> Sem r () addToREPLModule mi = modify @TopInfo (replModInfo <>~ mi) @@ -419,7 +419,7 @@ addToREPLModule mi = modify @TopInfo (replModInfo <>~ mi) -- term definitions, documentation, types, and type definitions. -- Replaces any previously loaded module. setREPLModule :: - Members '[State TopInfo, Random, Error EvalError, State Mem, Output (Message ann)] r => + Members '[State TopInfo, Random, Error EvalError, State Mem, Output Message] r => ModuleInfo -> Sem r () setREPLModule mi = do @@ -450,7 +450,7 @@ loadDef x body = do v <- inputToState @TopInfo . inputTopEnv $ eval body modify @TopInfo $ topEnv %~ Ctx.insert x v -checkExhaustive :: Members '[Fresh, Output (Message ann), Embed IO] r => TyDefCtx -> Defn -> Sem r () +checkExhaustive :: Members '[Fresh, Output Message, Embed IO] r => TyDefCtx -> Defn -> Sem r () checkExhaustive tyDefCtx (Defn name argsType _ boundClauses) = do clauses <- NonEmpty.map fst <$> mapM unbind boundClauses runReader @TyDefCtx tyDefCtx $ checkClauses name argsType clauses diff --git a/src/Disco/Exhaustiveness.hs b/src/Disco/Exhaustiveness.hs index 41305cd8..f4d8758c 100644 --- a/src/Disco/Exhaustiveness.hs +++ b/src/Disco/Exhaustiveness.hs @@ -72,7 +72,7 @@ import Unbound.Generics.LocallyNameless (Name) -- The most notable change is that here we always generate (at most) 3 -- concrete examples of uncovered patterns, instead of finding the most -- general complete description of every uncovered input. -checkClauses :: (Members '[Fresh, Reader Ty.TyDefCtx, Output (Message ann), Embed IO] r) => Name ATerm -> [Ty.Type] -> NonEmpty [APattern] -> Sem r () +checkClauses :: (Members '[Fresh, Reader Ty.TyDefCtx, Output Message, Embed IO] r) => Name ATerm -> [Ty.Type] -> NonEmpty [APattern] -> Sem r () checkClauses name types pats = do args <- TI.newVars types cl <- zipWithM (desugarClause args) [1 ..] (NonEmpty.toList pats) @@ -99,10 +99,10 @@ checkClauses name types pats = do DSL.<+> DSL.text "is undefined for some inputs. For example:" DSL.$+$ prettyExamples -prettyPrintExample :: ExamplePat -> Sem r (Doc ann) +prettyPrintExample :: ExamplePat -> Sem r Doc prettyPrintExample = runLFresh . runReader initPA . prettyPrintPattern . exampleToDiscoPattern -prettyPrintPattern :: (Members '[Reader PA, LFresh] r) => Pattern -> Sem r (Doc ann) +prettyPrintPattern :: (Members '[Reader PA, LFresh] r) => Pattern -> Sem r Doc prettyPrintPattern = withPA funPA . prettyPatternP exampleToDiscoPattern :: ExamplePat -> Pattern diff --git a/src/Disco/Interactive/CmdLine.hs b/src/Disco/Interactive/CmdLine.hs index 18842482..f3838691 100644 --- a/src/Disco/Interactive/CmdLine.hs +++ b/src/Disco/Interactive/CmdLine.hs @@ -188,7 +188,7 @@ discoMain = do loop :: Members DiscoEffects r => Sem r () loop = do - minput <- embedFinal $ withCtrlC (return $ Just "") (getInputLine "Disco> ") + minput <- embedFinal @(InputT IO) $ withCtrlC (return $ Just "") (getInputLine "Disco> ") case minput of Nothing -> return () Just input @@ -199,7 +199,7 @@ discoMain = do multiLineLoop [] loop | otherwise -> do - mapError @_ @DiscoError (Panic . show) $ + mapError @SomeException @DiscoError (Panic . show) $ absorbMonadCatch $ withCtrlC (return ()) $ handleCMD input @@ -207,12 +207,12 @@ discoMain = do multiLineLoop :: Members DiscoEffects r => [String] -> Sem r () multiLineLoop ls = do - minput <- embedFinal $ withCtrlC (return Nothing) (getInputLine "Disco| ") + minput <- embedFinal $ withCtrlC @(InputT IO) (return Nothing) (getInputLine "Disco| ") case minput of Nothing -> return () Just input | ":}" `isPrefixOf` input -> do - mapError @_ @DiscoError (Panic . show) $ + mapError @SomeException @DiscoError (Panic . show) $ absorbMonadCatch $ withCtrlC (return ()) $ handleCMD (unlines (reverse ls)) diff --git a/src/Disco/Interactive/Commands.hs b/src/Disco/Interactive/Commands.hs index d052d9b0..0c712658 100644 --- a/src/Disco/Interactive/Commands.hs +++ b/src/Disco/Interactive/Commands.hs @@ -309,7 +309,7 @@ annCmd = } handleAnn :: - Members '[Error DiscoError, Input TopInfo, Output (Message ())] r => + Members '[Error DiscoError, Input TopInfo, Output Message] r => REPLExpr 'CAnn -> Sem r () handleAnn (Ann t) = do @@ -332,7 +332,7 @@ compileCmd = } handleCompile :: - Members '[Error DiscoError, Input TopInfo, Output (Message ())] r => + Members '[Error DiscoError, Input TopInfo, Output Message] r => REPLExpr 'CCompile -> Sem r () handleCompile (Compile t) = do @@ -355,7 +355,7 @@ desugarCmd = } handleDesugar :: - Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r => + Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r => REPLExpr 'CDesugar -> Sem r () handleDesugar (Desugar t) = do @@ -389,7 +389,7 @@ parseDoc = <|> (DocOther <$> (sc *> many (anySingleBut ' '))) handleDoc :: - Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r => + Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r => REPLExpr 'CDoc -> Sem r () handleDoc (Doc (DocTerm (TBool _))) = handleDocBool @@ -402,26 +402,26 @@ handleDoc (Doc (DocTerm _)) = handleDoc (Doc (DocPrim p)) = handleDocPrim p handleDoc (Doc (DocOther s)) = handleDocMap (OtherKey s) -handleDocBool :: Members '[Output (Message ())] r => Sem r () +handleDocBool :: Members '[Output Message] r => Sem r () handleDocBool = info $ "T and F (also written true and false, or True and False) are the two possible values of type Boolean." $+$ formatReference (mkRef "bool") -handleDocUnit :: Members '[Output (Message ())] r => Sem r () +handleDocUnit :: Members '[Output Message] r => Sem r () handleDocUnit = info $ "The unit value, i.e. the single value of type Unit." $+$ formatReference (mkRef "unit") -handleDocWild :: Members '[Output (Message ())] r => Sem r () +handleDocWild :: Members '[Output Message] r => Sem r () handleDocWild = info $ "A wildcard pattern." $+$ formatReference (mkRef "wild-pattern") handleDocVar :: - Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r => + Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r => Name Term -> Sem r () handleDocVar x = do @@ -462,7 +462,7 @@ handleDocVar x = do _ -> PP.empty handleDocPrim :: - Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r => + Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r => Prim -> Sem r () handleDocPrim prim = do @@ -504,14 +504,14 @@ handleDocPrim prim = do , if post then "~" else PP.empty ] -formatReference :: Reference -> Sem r (Doc ann) +formatReference :: Reference -> Sem r Doc formatReference (Reference rty p) = case rty of Ref -> "https://disco-lang.readthedocs.io/en/latest/reference/" <> text p <> ".html" Intro -> "https://disco-lang.readthedocs.io/en/latest/introduction/" <> text p <> ".html" URL -> text p handleDocMap :: - Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r => + Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r => DocKey -> Sem r () handleDocMap k = case M.lookup k docMap of @@ -543,7 +543,7 @@ evalCmd = } handleEval :: - Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': Embed IO ': EvalEffects) r => + Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r => REPLExpr 'CEval -> Sem r () handleEval (Eval m) = do @@ -554,7 +554,7 @@ handleEval (Eval m) = do -- garbageCollect? -- First argument = should the value be printed? -evalTerm :: Members (Error EvalError ': State TopInfo ': Output (Message ()) ': EvalEffects) r => Bool -> ATerm -> Sem r Value +evalTerm :: Members (Error EvalError ': State TopInfo ': Output Message ': EvalEffects) r => Bool -> ATerm -> Sem r Value evalTerm pr at = do env <- use @TopInfo topEnv v <- runInputConst env $ eval (compileTerm at) @@ -584,7 +584,7 @@ helpCmd = , parser = return Help } -handleHelp :: Member (Output (Message ())) r => REPLExpr 'CHelp -> Sem r () +handleHelp :: Member (Output Message) r => REPLExpr 'CHelp -> Sem r () handleHelp Help = info $ vcat @@ -623,13 +623,13 @@ loadCmd = -- in the parent module are executed. -- Disco.Interactive.CmdLine uses a version of this function that returns a Bool. handleLoadWrapper :: - Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': Embed IO ': EvalEffects) r => + Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r => REPLExpr 'CLoad -> Sem r () handleLoadWrapper (Load fp) = void (handleLoad fp) handleLoad :: - Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': Embed IO ': EvalEffects) r => + Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r => FilePath -> Sem r Bool handleLoad fp = do @@ -645,7 +645,7 @@ handleLoad fp = do setREPLModule m -- Now run any tests - t <- inputToState $ runAllTests (m ^. miNames) (m ^. miProps) + t <- inputToState @TopInfo $ runAllTests (m ^. miNames) (m ^. miProps) -- Evaluate and print any top-level terms forM_ (m ^. miTerms) (mapError EvalErr . evalTerm True . fst) @@ -657,7 +657,7 @@ handleLoad fp = do -- XXX Return a structured summary of the results, not a Bool; & move -- this somewhere else? -runAllTests :: Members (Output (Message ()) ': Input TopInfo ': EvalEffects) r => [QName Term] -> Ctx ATerm [AProperty] -> Sem r Bool -- (Ctx ATerm [TestResult]) +runAllTests :: Members (Output Message ': Input TopInfo ': EvalEffects) r => [QName Term] -> Ctx ATerm [AProperty] -> Sem r Bool -- (Ctx ATerm [TestResult]) runAllTests declNames aprops | Ctx.null aprops = return True | otherwise = do @@ -667,7 +667,7 @@ runAllTests declNames aprops where numSamples :: Int numSamples = 50 -- XXX make this configurable somehow - runTests :: Members (Output (Message ()) ': Input TopInfo ': EvalEffects) r => QName Term -> [AProperty] -> Sem r Bool + runTests :: Members (Output Message ': Input TopInfo ': EvalEffects) r => QName Term -> [AProperty] -> Sem r Bool runTests (QName _ n) props = do results <- inputTopEnv $ traverse (sequenceA . (id &&& runTest numSamples)) props let failures = P.filter (not . testIsOk . snd) results @@ -697,13 +697,13 @@ namesCmd = , shortHelp = "Show all names in current scope" , category = User , cmdtype = ColonCmd - , action = inputToState . handleNames + , action = inputToState @TopInfo . handleNames , parser = return Names } -- | Show names and types for each item in the top-level context. handleNames :: - Members '[Input TopInfo, LFresh, Output (Message ())] r => + Members '[Input TopInfo, LFresh, Output Message] r => REPLExpr 'CNames -> Sem r () handleNames Names = do @@ -748,7 +748,7 @@ parseCmd = , parser = Parse <$> term } -handleParse :: Member (Output (Message ())) r => REPLExpr 'CParse -> Sem r () +handleParse :: Member (Output Message) r => REPLExpr 'CParse -> Sem r () handleParse (Parse t) = info (text (show t)) ------------------------------------------------------------ @@ -766,7 +766,7 @@ prettyCmd = , parser = Pretty <$> term } -handlePretty :: Members '[LFresh, Output (Message ())] r => REPLExpr 'CPretty -> Sem r () +handlePretty :: Members '[LFresh, Output Message] r => REPLExpr 'CPretty -> Sem r () handlePretty (Pretty t) = info $ pretty' t ------------------------------------------------------------ @@ -784,9 +784,9 @@ printCmd = , parser = Print <$> term } -handlePrint :: Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': EvalEffects) r => REPLExpr 'CPrint -> Sem r () +handlePrint :: Members (Error DiscoError ': State TopInfo ': Output Message ': EvalEffects) r => REPLExpr 'CPrint -> Sem r () handlePrint (Print t) = do - at <- inputToState . typecheckTop $ checkTop t (toPolyType TyString) + at <- inputToState @TopInfo . typecheckTop $ checkTop t (toPolyType TyString) v <- mapError EvalErr . evalTerm False $ at info $ text (vlist vchar v) @@ -805,9 +805,9 @@ tableCmd = , parser = Table <$> parseTermOrOp } -handleTable :: Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': EvalEffects) r => REPLExpr 'CTable -> Sem r () +handleTable :: Members (Error DiscoError ': State TopInfo ': Output Message ': EvalEffects) r => REPLExpr 'CTable -> Sem r () handleTable (Table t) = do - (at, ty) <- inputToState . typecheckTop $ inferTop1 t + (at, ty) <- inputToState @TopInfo . typecheckTop $ inferTop1 t v <- mapError EvalErr . evalTerm False $ at tydefs <- use @TopInfo (replModInfo . to allTydefs) @@ -948,7 +948,7 @@ reloadCmd = } handleReload :: - Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': Embed IO ': EvalEffects) r => + Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r => REPLExpr 'CReload -> Sem r () handleReload Reload = do @@ -973,7 +973,7 @@ showDefnCmd = } handleShowDefn :: - Members '[Input TopInfo, LFresh, Output (Message ())] r => + Members '[Input TopInfo, LFresh, Output Message] r => REPLExpr 'CShowDefn -> Sem r () handleShowDefn (ShowDefn x) = do @@ -1006,13 +1006,13 @@ testPropCmd = } handleTest :: - Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': EvalEffects) r => + Members (Error DiscoError ': State TopInfo ': Output Message ': EvalEffects) r => REPLExpr 'CTestProp -> Sem r () handleTest (TestProp t) = do - at <- inputToState . typecheckTop $ checkProperty t + at <- inputToState @TopInfo . typecheckTop $ checkProperty t tydefs <- use @TopInfo (replModInfo . to allTydefs) - inputToState . inputTopEnv $ do + inputToState @TopInfo . inputTopEnv $ do r <- runTest 100 at -- XXX make configurable info $ runInputConst tydefs . runReader initPA $ indent 2 . nest 2 $ "-" <+> prettyTestResult at r @@ -1035,7 +1035,7 @@ maxInferredTypes :: Int maxInferredTypes = 16 handleTypeCheck :: - Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r => + Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r => REPLExpr 'CTypeCheck -> Sem r () handleTypeCheck (TypeCheck t) = do diff --git a/src/Disco/Interpret/CESK.hs b/src/Disco/Interpret/CESK.hs index 9829ff73..92b071eb 100644 --- a/src/Disco/Interpret/CESK.hs +++ b/src/Disco/Interpret/CESK.hs @@ -32,7 +32,6 @@ import qualified Data.List.Infinite as InfList import qualified Data.Map as M import Data.Maybe (isJust) import Data.Ratio -import qualified Data.Text as T import Disco.AST.Core import Disco.AST.Generic ( Ellipsis (..), @@ -55,12 +54,6 @@ import Math.Combinatorics.Exact.Binomial (choose) import Math.Combinatorics.Exact.Factorial (factorial) import Math.NumberTheory.Primes (factorise, unPrime) import Math.NumberTheory.Primes.Testing (isPrime) -import Math.OEIS ( - SearchStatus (SubSeq), - extendSeq, - lookupSeq, - number, - ) import Polysemy import Polysemy.Error import Polysemy.Random @@ -352,8 +345,6 @@ appConst k = \case -- Sequences OUntil -> arity2 $ \v1 -> out . ellipsis (Until v1) - OLookupSeq -> out . oeisLookup - OExtendSeq -> out . oeisExtend -------------------------------------------------- -- Comparison @@ -647,24 +638,6 @@ constdiff (x : xs) | all (== x) xs = x | otherwise = constdiff (diff (x : xs)) ------------------------------------------------------------- --- OEIS ------------------------------------------------------------- - --- | Looks up a sequence of integers in OEIS. --- Returns 'left()' if the sequence is unknown in OEIS, --- otherwise 'right "https://oeis.org/"' -oeisLookup :: Value -> Value -oeisLookup (vlist vint -> ns) = maybe VNil parseResult (lookupSeq (SubSeq ns)) - where - parseResult r = VInj R (listv charv ("https://oeis.org/" ++ T.unpack (number r))) - --- | Extends a Disco integer list with data from a known OEIS --- sequence. Returns a list of integers upon success, otherwise the --- original list (unmodified). -oeisExtend :: Value -> Value -oeisExtend = listv intv . extendSeq . vlist vint - ------------------------------------------------------------ -- Normalizing bags/sets ------------------------------------------------------------ diff --git a/src/Disco/Messages.hs b/src/Disco/Messages.hs index 0e5eab99..ccd686bf 100644 --- a/src/Disco/Messages.hs +++ b/src/Disco/Messages.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE TemplateHaskell #-} -- | @@ -26,34 +27,34 @@ data MessageType | Debug deriving (Show, Read, Eq, Ord, Enum, Bounded) -data Message ann = Message {_messageType :: MessageType, _message :: Doc ann} +data Message = Message {_messageType :: MessageType, _message :: Doc} deriving (Show) makeLenses ''Message -handleMsg :: Member (Embed IO) r => (Message ann -> Bool) -> Message ann -> Sem r () +handleMsg :: Member (Embed IO) r => (Message -> Bool) -> Message -> Sem r () handleMsg p m = when (p m) $ printMsg m -printMsg :: Member (Embed IO) r => Message ann -> Sem r () +printMsg :: Member (Embed IO) r => Message -> Sem r () printMsg (Message _ m) = embed $ putStrLn (renderDoc' m) -msg :: Member (Output (Message ann)) r => MessageType -> Sem r (Doc ann) -> Sem r () +msg :: Member (Output Message) r => MessageType -> Sem r Doc -> Sem r () msg typ m = m >>= output . Message typ -info :: Member (Output (Message ann)) r => Sem r (Doc ann) -> Sem r () +info :: Member (Output Message) r => Sem r Doc -> Sem r () info = msg Info -infoPretty :: (Member (Output (Message ann)) r, Pretty t) => t -> Sem r () +infoPretty :: (Member (Output Message) r, Pretty t) => t -> Sem r () infoPretty = info . pretty' -warn :: Member (Output (Message ann)) r => Sem r (Doc ann) -> Sem r () +warn :: Member (Output Message) r => Sem r Doc -> Sem r () warn = msg Warning -debug :: Member (Output (Message ann)) r => Sem r (Doc ann) -> Sem r () +debug :: Member (Output Message) r => Sem r Doc -> Sem r () debug = msg Debug -debugPretty :: (Member (Output (Message ann)) r, Pretty t) => t -> Sem r () +debugPretty :: (Member (Output Message) r, Pretty t) => t -> Sem r () debugPretty = debug . pretty' -err :: Member (Output (Message ann)) r => Sem r (Doc ann) -> Sem r () +err :: Member (Output Message) r => Sem r Doc -> Sem r () err = msg ErrMsg diff --git a/src/Disco/Pretty.hs b/src/Disco/Pretty.hs index 64c2951d..1c73dcb0 100644 --- a/src/Disco/Pretty.hs +++ b/src/Disco/Pretty.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DerivingVia #-} +{-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE NoMonomorphismRestriction #-} @@ -25,21 +26,25 @@ import Prelude hiding ((<>)) import Data.Bifunctor import Data.Char (isAlpha) import Data.List.NonEmpty (NonEmpty) -import qualified Data.List.NonEmpty as NE +import Data.List.NonEmpty qualified as NE import Data.Map (Map) -import qualified Data.Map as M +import Data.Map qualified as M import Data.Ratio import Data.Set (Set) -import qualified Data.Set as S +import Data.Set qualified as S import Disco.Effects.LFresh import Disco.Pretty.DSL import Disco.Pretty.Prec import Disco.Syntax.Operators import Polysemy import Polysemy.Reader -import Prettyprinter (Doc) +import Prettyprinter qualified as PP import Unbound.Generics.LocallyNameless (Name) +------------------------------------------------------------ + +type Doc = PP.Doc () + ------------------------------------------------------------ -- Utilities for handling precedence and associativity @@ -48,7 +53,7 @@ import Unbound.Generics.LocallyNameless (Name) -- associativity of a term is, and optionally surround it with -- parentheses depending on the precedence and associativity of its -- parent. -withPA :: Member (Reader PA) r => PA -> Sem r (Doc ann) -> Sem r (Doc ann) +withPA :: Member (Reader PA) r => PA -> Sem r (PP.Doc ann) -> Sem r (PP.Doc ann) withPA pa = mparens pa . setPA pa -- | Locally set the precedence and associativity within a @@ -59,20 +64,20 @@ setPA = local . const -- | Mark a subcomputation as pretty-printing a term on the left of an -- operator (so parentheses can be inserted appropriately, depending -- on the associativity). -lt :: Member (Reader PA) r => Sem r (Doc ann) -> Sem r (Doc ann) +lt :: Member (Reader PA) r => Sem r (PP.Doc ann) -> Sem r (PP.Doc ann) lt = local (\(PA p _) -> PA p InL) -- | Mark a subcomputation as pretty-printing a term on the right of -- an operator (so parentheses can be inserted appropriately, -- depending on the associativity). -rt :: Member (Reader PA) r => Sem r (Doc ann) -> Sem r (Doc ann) +rt :: Member (Reader PA) r => Sem r (PP.Doc ann) -> Sem r (PP.Doc ann) rt = local (\(PA p _) -> PA p InR) -- | Optionally surround a pretty-printed term with parentheses, -- depending on its precedence and associativity (given as the 'PA' -- argument) and that of its context (given by the ambient 'Reader -- PA' effect). -mparens :: Member (Reader PA) r => PA -> Sem r (Doc ann) -> Sem r (Doc ann) +mparens :: Member (Reader PA) r => PA -> Sem r (PP.Doc ann) -> Sem r (PP.Doc ann) mparens pa doc = do parentPA <- ask (if pa `lowerPrec` parentPA then parens else id) doc @@ -81,12 +86,12 @@ mparens pa doc = do -- Pretty type class class Pretty t where - pretty :: Members '[Reader PA, LFresh] r => t -> Sem r (Doc ann) + pretty :: Members '[Reader PA, LFresh] r => t -> Sem r Doc prettyStr :: Pretty t => t -> Sem r String prettyStr = renderDoc . runLFresh . pretty -pretty' :: Pretty t => t -> Sem r (Doc ann) +pretty' :: Pretty t => t -> Sem r Doc pretty' = runReader initPA . runLFresh . pretty ------------------------------------------------------------ diff --git a/src/Disco/Property.hs b/src/Disco/Property.hs index a8724268..43f32d72 100644 --- a/src/Disco/Property.hs +++ b/src/Disco/Property.hs @@ -77,7 +77,7 @@ generateSamples (Randomized n m) e -- Pretty-printing for test results ------------------------------------------------------------ -prettyResultCertainty :: Members '[LFresh, Reader PA] r => TestReason -> AProperty -> String -> Sem r (Doc ann) +prettyResultCertainty :: Members '[LFresh, Reader PA] r => TestReason -> AProperty -> String -> Sem r Doc prettyResultCertainty r prop res = (if resultIsCertain r then "Certainly" else "Possibly") <+> text res <> ":" <+> pretty (eraseProperty prop) @@ -87,7 +87,7 @@ prettyTestReason :: AProperty -> TestReason -> TestEnv -> - Sem r (Doc ann) + Sem r Doc prettyTestReason _ _ TestBool _ = empty prettyTestReason b (ATAbs _ _ body) (TestFound (TestResult b' r' env')) env = do lunbind body $ \(_, p) -> @@ -143,7 +143,7 @@ prettyTestResult :: Members '[Input TyDefCtx, LFresh, Reader PA] r => AProperty -> TestResult -> - Sem r (Doc ann) + Sem r Doc prettyTestResult prop (TestResult bool tr env) = prettyResultCertainty tr prop (map toLower (show bool)) $+$ prettyTestReason bool prop tr env @@ -152,7 +152,7 @@ prettyTestEnv :: Members '[Input TyDefCtx, LFresh, Reader PA] r => String -> TestEnv -> - Sem r (Doc ann) + Sem r Doc prettyTestEnv _ (TestEnv []) = empty prettyTestEnv s (TestEnv vs) = nest 2 $ text s $+$ vcat (map prettyBind vs) where diff --git a/src/Disco/Subst.hs b/src/Disco/Subst.hs index c8905ac8..02950970 100644 --- a/src/Disco/Subst.hs +++ b/src/Disco/Subst.hs @@ -68,7 +68,7 @@ instance Pretty a => Pretty (Substitution a) where ds <- punctuate "," es braces (hsep ds) -prettyMapping :: (Pretty a, Members '[Reader PA, LFresh] r) => Name a -> a -> Sem r (Doc ann) +prettyMapping :: (Pretty a, Members '[Reader PA, LFresh] r) => Name a -> a -> Sem r Doc prettyMapping x a = pretty x <+> "->" <+> pretty a -- | The domain of a substitution is the set of names for which the diff --git a/src/Disco/Syntax/Prims.hs b/src/Disco/Syntax/Prims.hs index 2336987a..1876331a 100644 --- a/src/Disco/Syntax/Prims.hs +++ b/src/Disco/Syntax/Prims.hs @@ -112,10 +112,6 @@ data Prim where PrimUntil :: Prim -- | Test whether a proposition holds PrimHolds :: Prim - -- | Lookup OEIS sequence - PrimLookupSeq :: Prim - -- | Extend OEIS sequence - PrimExtendSeq :: Prim -- | Generates a pseudorandom number generator PrimSeed :: Prim -- | Given a range and a generator, generates random number @@ -190,8 +186,6 @@ primTable = , PrimInfo PrimCrash "crash" False , PrimInfo PrimUntil "until" False , PrimInfo PrimHolds "holds" True - , PrimInfo PrimLookupSeq "lookupSequence" False - , PrimInfo PrimExtendSeq "extendSequence" False , PrimInfo PrimSeed "seed" True , PrimInfo PrimRandom "random" True ] diff --git a/src/Disco/Typecheck.hs b/src/Disco/Typecheck.hs index ba961d50..ab9c54ce 100644 --- a/src/Disco/Typecheck.hs +++ b/src/Disco/Typecheck.hs @@ -41,7 +41,7 @@ import qualified Disco.Subst as Subst import Disco.Syntax.Operators import Disco.Syntax.Prims import Disco.Typecheck.Constraints -import Disco.Typecheck.Solve (SolutionLimit (..), solveConstraint) +import Disco.Typecheck.Solve (SolutionLimit (..), SolveError, solveConstraint) import Disco.Typecheck.Util import Disco.Types import Disco.Types.Rules @@ -120,7 +120,7 @@ suggestionsFrom x = filter ((<= 1) . restrictedDamerauLevenshteinDistance defaul -- imports should already be checked and passed in as the second -- argument. checkModule :: - Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh] r => + Members '[Output Message, Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh] r => ModuleName -> Map ModuleName ModuleInfo -> Module -> @@ -277,7 +277,7 @@ checkCtx = mapM_ checkPolyTyValid . Ctx.elems -- | Type check a top-level definition in the given module. checkDefn :: - Members '[Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh, Output (Message ann)] r => + Members '[Reader TyCtx, Reader TyDefCtx, Error LocTCError, Fresh, Output Message] r => ModuleName -> TermDefn -> Sem r Defn @@ -346,7 +346,7 @@ checkDefn name (TermDefn x clauses) = mapError (LocTCError (Just (name .- x))) $ -- | Given a context mapping names to documentation, extract the -- properties attached to each name and typecheck them. checkProperties :: - Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output (Message ann)] r => + Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output Message] r => Ctx Term Docs -> Sem r (Ctx ATerm [AProperty]) checkProperties docs = @@ -358,7 +358,7 @@ checkProperties docs = -- | Check the types of the terms embedded in a property. checkProperty :: - Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output (Message ann)] r => + Members '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh, Output Message] r => Property -> Sem r AProperty checkProperty prop = do @@ -457,7 +457,7 @@ infer = typecheck Infer -- | Top-level type inference algorithm, returning only the first -- possible result. inferTop1 :: - Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r => + Members '[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r => Term -> Sem r (ATerm, PolyType) inferTop1 t = NE.head <$> inferTop 1 t @@ -467,7 +467,7 @@ inferTop1 t = NE.head <$> inferTop 1 t -- inference, solving the resulting constraints, and quantifying -- over any remaining type variables. inferTop :: - Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r => + Members '[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r => Int -> Term -> Sem r (NonEmpty (ATerm, PolyType)) @@ -539,7 +539,7 @@ inferTop lim t = do -- polymorphic type by running type checking and solving the -- resulting constraints. checkTop :: - Members '[Output (Message ann), Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r => + Members '[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh] r => Term -> PolyType -> Sem r ATerm @@ -1004,8 +1004,6 @@ typecheck Infer (TPrim prim) = do ] return $ TyContainer c a :->: TyContainer c (TyContainer c a) - inferPrim PrimLookupSeq = return $ TyList TyN :->: (TyUnit :+: TyString) - inferPrim PrimExtendSeq = return $ TyList TyN :->: TyList TyN -------------------------------------------------- -- Base types @@ -1788,7 +1786,7 @@ ensureEq ty1 ty2 ------------------------------------------------------------ isSubPolyType :: - Members '[Input TyDefCtx, Output (Message ann), Fresh] r => + Members '[Input TyDefCtx, Output Message, Fresh] r => PolyType -> PolyType -> Sem r Bool @@ -1800,16 +1798,16 @@ isSubPolyType (Forall b1) (Forall b2) = do debug "Checking subtyping..." debugPretty (Forall b1) debugPretty (Forall b2) - ss <- runError (evalState (SolutionLimit 1) (solveConstraint c)) + ss <- runError @SolveError (evalState (SolutionLimit 1) (solveConstraint c)) return (either (const False) (not . P.null) ss) -thin :: Members '[Input TyDefCtx, Output (Message ann), Fresh] r => NonEmpty PolyType -> Sem r (NonEmpty PolyType) +thin :: Members '[Input TyDefCtx, Output Message, Fresh] r => NonEmpty PolyType -> Sem r (NonEmpty PolyType) thin = fmap NE.fromList . thin' . NE.toList -- Intuitively, this will always return a nonempty list given a nonempty list as input; -- we could probably rewrite it in terms of NonEmpty combinators but it's more effort than -- I cared to spend at the moment. -thin' :: Members '[Input TyDefCtx, Output (Message ann), Fresh] r => [PolyType] -> Sem r [PolyType] +thin' :: Members '[Input TyDefCtx, Output Message, Fresh] r => [PolyType] -> Sem r [PolyType] thin' [] = return [] thin' (ty : tys) = do ss <- or <$> mapM (`isSubPolyType` ty) tys diff --git a/src/Disco/Typecheck/Solve.hs b/src/Disco/Typecheck/Solve.hs index daa38d49..a689af26 100644 --- a/src/Disco/Typecheck/Solve.hs +++ b/src/Disco/Typecheck/Solve.hs @@ -36,6 +36,7 @@ import Data.Maybe ( mapMaybe, ) import Data.Monoid (First (..)) +import Data.Proxy import Data.Semigroup (sconcat) import Data.Set (Set) import Data.Set qualified as S @@ -95,9 +96,9 @@ runSolve lim = runError . runFresh . evalState lim -- | Run a list of actions, and return the results from those which do -- not throw an error. If all of them throw an error, rethrow the -- first one. -filterErrors :: Member (Error e) r => NonEmpty (Sem r a) -> Sem r (NonEmpty a) -filterErrors ms = do - es <- mapM try ms +filterErrors :: Member (Error e) r => Proxy e -> NonEmpty (Sem r a) -> Sem r (NonEmpty a) +filterErrors (Proxy :: Proxy err) ms = do + es <- mapM (try @err) ms case partitionEithersNE es of Left (e :| _) -> throw e Right (_, as) -> return as @@ -117,7 +118,7 @@ countSolution = modify (SolutionLimit . subtract 1 . getSolutionLimit) -- being positive. If the solution limit has reached zero, stop -- early. withSolutionLimit :: - (Member (State SolutionLimit) r, Member (Output (Message ann)) r, Monoid a) => + (Member (State SolutionLimit) r, Member (Output Message) r, Monoid a) => Sem r a -> Sem r a withSolutionLimit m = do @@ -265,7 +266,7 @@ lkup messg m k = fromMaybe (error errMsg) (M.lookup k m) -- Top-level solver algorithm solveConstraint :: - Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx, State SolutionLimit] r => + Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx, State SolutionLimit] r => Constraint -> Sem r (NonEmpty S) solveConstraint c = do @@ -284,10 +285,10 @@ solveConstraint c = do qcList <- decomposeConstraint c -- Now try continuing with each set. - sconcat <$> filterErrors (NE.map (uncurry solveConstraintChoice) qcList) + sconcat <$> filterErrors (Proxy :: Proxy SolveError) (NE.map (uncurry solveConstraintChoice) qcList) solveConstraintChoice :: - Members '[Fresh, Error SolveError, Output (Message ann), Input TyDefCtx, State SolutionLimit] r => + Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx, State SolutionLimit] r => TyVarInfoMap -> [SimpleConstraint] -> Sem r (NonEmpty S) @@ -438,7 +439,7 @@ decomposeConstraint (CAll ty) = do where mkSkolems :: [Name Type] -> [(Name Type, Type)] mkSkolems = map (id &&& TySkolem) -decomposeConstraint (COr cs) = sconcat <$> filterErrors (NE.map decomposeConstraint cs) +decomposeConstraint (COr cs) = sconcat <$> filterErrors (Proxy :: Proxy SolveError) (NE.map decomposeConstraint cs) decomposeQual :: Members '[Fresh, Error SolveError, Input TyDefCtx] r => @@ -508,7 +509,7 @@ checkQual q (ABase bty) = -- constraints, that is, only of the form (v1 <: v2), (v <: b), or -- (b <: v), where v is a type variable and b is a base type. simplify :: - Members '[Error SolveError, Output (Message ann), Input TyDefCtx] r => + Members '[Error SolveError, Output Message, Input TyDefCtx] r => TyVarInfoMap -> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S) @@ -538,7 +539,7 @@ simplify origVM cs = -- Iterate picking one simplifiable constraint and simplifying it -- until none are left. simplify' :: - Members '[State SimplifyState, Fresh, Error SolveError, Output (Message ann), Input TyDefCtx] r => + Members '[State SimplifyState, Fresh, Error SolveError, Output Message, Input TyDefCtx] r => Sem r () simplify' = do -- q <- gets fst @@ -772,7 +773,7 @@ mkConstraintGraph as cs = G.mkGraph nodes (S.fromList cs) -- only unsorted variables, just unify them all with the skolem and -- remove those components. checkSkolems :: - Members '[Error SolveError, Output (Message ann), Input TyDefCtx] r => + Members '[Error SolveError, Output Message, Input TyDefCtx] r => TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S) @@ -805,7 +806,7 @@ checkSkolems vm graph = do noSkolems (AVar (S v)) = error $ "Skolem " ++ show v ++ " remaining in noSkolems" unifyWCCs :: - Members '[Error SolveError, Output (Message ann), Input TyDefCtx] r => + Members '[Error SolveError, Output Message, Input TyDefCtx] r => Graph Atom -> S -> [Set Atom] -> @@ -998,7 +999,7 @@ lbsBySort vm rm = allBySort vm rm SubTy -- predecessors in this case, since it seems nice to default to -- "simpler" types lower down in the subtyping chain. solveGraph :: - Members '[Fresh, Error SolveError, Output (Message ann), State SolutionLimit] r => + Members '[Fresh, Error SolveError, Output Message, State SolutionLimit] r => TyVarInfoMap -> Graph UAtom -> Sem r [S] @@ -1067,7 +1068,7 @@ solveGraph vm g = do fromVar _ = error "Impossible! UB but uisVar." go :: - Members '[Fresh, Output (Message ann), State SolutionLimit] r => + Members '[Fresh, Output Message, State SolutionLimit] r => RelMap -> Sem r [Substitution BaseTy] go relMap@(RelMap rm) = withSolutionLimit $ do diff --git a/src/Disco/Typecheck/Util.hs b/src/Disco/Typecheck/Util.hs index 2e4fd57d..b0b4846b 100644 --- a/src/Disco/Typecheck/Util.hs +++ b/src/Disco/Typecheck/Util.hs @@ -146,13 +146,13 @@ withConstraint = fmap swap . runWriter -- (or failing with an error). Note that this locally dispatches -- the constraint writer and solution limit effects. solve :: - Members '[Reader TyDefCtx, Error TCError, Output (Message ann)] r => + Members '[Reader TyDefCtx, Error TCError, Output Message] r => Int -> Sem (Writer Constraint ': r) a -> Sem r (a, NonEmpty S) solve lim m = do (a, c) <- withConstraint m - res <- runSolve (SolutionLimit lim) . inputToReader . solveConstraint $ c + res <- runSolve (SolutionLimit lim) . inputToReader @TyDefCtx . solveConstraint $ c case res of Left e -> throw (Unsolvable e) Right ss -> return (a, ss) diff --git a/src/Disco/Value.hs b/src/Disco/Value.hs index 46d22e71..08865676 100644 --- a/src/Disco/Value.hs +++ b/src/Disco/Value.hs @@ -490,10 +490,10 @@ memoSet n sv v = do -- Pretty-printing values ------------------------------------------------------------ -prettyValue' :: Member (Input TyDefCtx) r => Type -> Value -> Sem r (Doc ann) +prettyValue' :: Member (Input TyDefCtx) r => Type -> Value -> Sem r Doc prettyValue' ty v = runLFresh . runReader initPA $ prettyValue ty v -prettyValue :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r (Doc ann) +prettyValue :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r Doc -- Lazily expand any user-defined types prettyValue (TyUser x args) v = do tydefs <- input @@ -547,23 +547,23 @@ prettyValue ty@TyCon {} v = -- | Pretty-print a value with guaranteed parentheses. Do nothing for -- tuples; add an extra set of parens for other values. -prettyVP :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r (Doc ann) +prettyVP :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r Doc prettyVP ty@(_ :*: _) = prettyValue ty prettyVP ty = parens . prettyValue ty -prettyPlaceholder :: Members '[Reader PA, LFresh] r => Type -> Sem r (Doc ann) +prettyPlaceholder :: Members '[Reader PA, LFresh] r => Type -> Sem r Doc prettyPlaceholder ty = "<" <> pretty ty <> ">" -prettyTuple :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r (Doc ann) +prettyTuple :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r Doc prettyTuple (ty1 :*: ty2) (VPair v1 v2) = prettyValue ty1 v1 <> "," <+> prettyTuple ty2 v2 prettyTuple ty v = prettyValue ty v -- | 'prettySequence' pretty-prints a lists of values separated by a delimiter. -prettySequence :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Doc ann -> [Value] -> Sem r (Doc ann) +prettySequence :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Doc -> [Value] -> Sem r Doc prettySequence ty del vs = hsep =<< punctuate (return del) (map (prettyValue ty) vs) -- | Pretty-print a literal bag value. -prettyBag :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> [(Value, Integer)] -> Sem r (Doc ann) +prettyBag :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> [(Value, Integer)] -> Sem r Doc prettyBag _ [] = bag empty prettyBag ty vs | all ((== 1) . snd) vs = bag $ prettySequence ty "," (map fst vs) diff --git a/test/lib-oeis/expected b/test-old/lib-oeis/expected similarity index 100% rename from test/lib-oeis/expected rename to test-old/lib-oeis/expected diff --git a/test/lib-oeis/input b/test-old/lib-oeis/input similarity index 100% rename from test/lib-oeis/input rename to test-old/lib-oeis/input diff --git a/test-old/lib-oeis/output b/test-old/lib-oeis/output new file mode 100644 index 00000000..dcdbbc1f --- /dev/null +++ b/test-old/lib-oeis/output @@ -0,0 +1,8 @@ +Loading oeis.disco... +right("https://oeis.org/A000045") +left(■) +left(■) +[1, 3, 5, 7, 9, 11, 13, 15, 17, 19, 21, 23, 25, 27, 29, 31, 33, 35, 37, 39, 41, 43, 45, 47, 49, 51, 53, 55, 57, 59, 61, 63, 65, 67, 69, 71, 73, 75, 77, 79, 81, 83, 85, 87, 89, 91, 93, 95, 97, 99, 101, 103, 105, 107, 109, 111, 113, 115, 117, 119, 121, 123, 125, 127, 129, 131] +[] +[1, 10011] +[1, 3, 5, 7, 9, 11, 13, 15, 17, 19, 21, 23, 25, 27, 29, 31, 33, 35, 37, 39, 41, 43, 45, 47, 49, 51, 53, 55, 57, 59, 61, 63, 65, 67, 69, 71, 73, 75, 77, 79, 81, 83, 85, 87, 89, 91, 93, 95, 97, 99, 101, 103, 105, 107, 109, 111, 113, 115, 117, 119, 121, 123, 125, 127, 129, 131] diff --git a/lib/oeis.disco b/test-old/oeis.disco similarity index 100% rename from lib/oeis.disco rename to test-old/oeis.disco diff --git a/test/pretty-issue258/expected b/test/pretty-issue258/expected index bf810e6d..7c1faa82 100644 --- a/test/pretty-issue258/expected +++ b/test/pretty-issue258/expected @@ -1,6 +1,5 @@ Loading catalan.disco... Loading list.disco... -Loading oeis.disco... Loaded. treesOfSize : ℕ → List(BT) treesOfSize(0) = [left(■)] diff --git "a/test\\file.disco" "b/test\\file.disco" deleted file mode 100644 index f4edfc9c..00000000 --- "a/test\\file.disco" +++ /dev/null @@ -1,2 +0,0 @@ -x : N -x = 3 \ No newline at end of file