mirror of
https://github.com/anoma/juvix.git
synced 2024-11-24 08:45:51 +03:00
Add terminating keyword (#71)
* Parsing terminating keyword * cosmetics * Add support for `terminating` keyword to function decl. * Minor replacement * Fix .mjuxix to .mjuvix and the module name
This commit is contained in:
Jonathan Cubides
GitHub
parent
13ce663fe1
commit
038042b733
24
app/Main.hs
24
app/Main.hs
@ -2,8 +2,6 @@
|
||||
|
||||
module Main (main) where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Commands.Extra
|
||||
import Commands.MicroJuvix
|
||||
import Commands.MiniHaskell
|
||||
@ -432,24 +430,30 @@ runCLI cli = do
|
||||
minihaskell <- head . (^. MiniHaskell.resultModules) <$> runIO (upToMiniHaskell (getEntryPoint root o))
|
||||
renderStdOutMini (MiniHaskell.ppOutDefault minihaskell)
|
||||
Termination (Calls opts@CallsOptions {..}) -> do
|
||||
a <- head . (^. Abstract.resultModules) <$> runIO (upToAbstract (getEntryPoint root opts))
|
||||
let callMap0 = T.buildCallMap a
|
||||
results <- runIO (upToAbstract (getEntryPoint root opts))
|
||||
let topModule = head (results ^. Abstract.resultModules)
|
||||
infotable = results ^. Abstract.resultTable
|
||||
callMap0 = T.buildCallMap infotable topModule
|
||||
callMap = case _callsFunctionNameFilter of
|
||||
Nothing -> callMap0
|
||||
Just f -> T.filterCallMap f callMap0
|
||||
opts' = T.callsPrettyOptions opts
|
||||
renderStdOutAbs (Abstract.ppOut opts' callMap)
|
||||
putStrLn ""
|
||||
Termination (CallGraph o@CallGraphOptions {..}) -> do
|
||||
a <- head . (^. Abstract.resultModules) <$> runIO (upToAbstract (getEntryPoint root o))
|
||||
let callMap = T.buildCallMap a
|
||||
Termination (CallGraph opts@CallGraphOptions {..}) -> do
|
||||
results <- runIO (upToAbstract (getEntryPoint root opts))
|
||||
let topModule = head (results ^. Abstract.resultModules)
|
||||
infotable = results ^. Abstract.resultTable
|
||||
callMap = T.buildCallMap infotable topModule
|
||||
opts' =
|
||||
Abstract.defaultOptions
|
||||
{ Abstract._optShowNameId = globalOptions ^. globalShowNameIds
|
||||
}
|
||||
completeGraph = T.completeCallGraph callMap
|
||||
filteredGraph = maybe completeGraph (`T.unsafeFilterGraph` completeGraph) _graphFunctionNameFilter
|
||||
recBehav = map T.recursiveBehaviour (T.reflexiveEdges filteredGraph)
|
||||
rEdges = T.reflexiveEdges filteredGraph
|
||||
|
||||
recBehav = map T.recursiveBehaviour rEdges
|
||||
renderStdOutAbs (Abstract.ppOut opts' filteredGraph)
|
||||
putStrLn ""
|
||||
forM_ recBehav $ \r -> do
|
||||
@ -457,11 +461,11 @@ runCLI cli = do
|
||||
Scoper.defaultOptions
|
||||
{ Scoper._optShowNameId = globalOptions ^. globalShowNameIds
|
||||
}
|
||||
n = toAnsiText' (Scoper.ppOut sopts (A._recBehaviourFunction r))
|
||||
n = toAnsiText' (Scoper.ppOut sopts (A._recursiveBehaviourFun r))
|
||||
renderStdOutAbs (Abstract.ppOut opts' r)
|
||||
putStrLn ""
|
||||
case T.findOrder r of
|
||||
Nothing -> putStrLn (n <> " Fails the termination checking")
|
||||
Nothing -> putStrLn (n <> " Fails the termination checking") >> exitFailure
|
||||
Just (T.LexOrder k) -> putStrLn (n <> " Terminates with order " <> show (toList k))
|
||||
putStrLn ""
|
||||
|
||||
|
||||
@ -4,9 +4,6 @@
|
||||
|
||||
module MiniJuvix.Syntax.Core where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- import Algebra.Graph.Label (Semiring (..))
|
||||
import MiniJuvix.Prelude hiding (Local)
|
||||
import Numeric.Natural (Natural)
|
||||
|
||||
|
||||
@ -77,6 +77,9 @@ any = "Any"
|
||||
type_ :: IsString s => s
|
||||
type_ = "Type"
|
||||
|
||||
questionMark :: IsString s => s
|
||||
questionMark = "?"
|
||||
|
||||
keyword :: IsString s => s
|
||||
keyword = "keyword"
|
||||
|
||||
@ -154,3 +157,9 @@ ghc = "ghc"
|
||||
|
||||
agda :: IsString s => s
|
||||
agda = "agda"
|
||||
|
||||
terminating :: IsString s => s
|
||||
terminating = "terminating"
|
||||
|
||||
waveArrow :: IsString s => s
|
||||
waveArrow = "↝"
|
||||
|
||||
@ -63,8 +63,6 @@ module MiniJuvix.Prelude.Base
|
||||
)
|
||||
where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Monad.Extra
|
||||
import Control.Monad.Fix
|
||||
@ -87,7 +85,18 @@ import Data.Int
|
||||
import Data.List.Extra hiding (groupSortOn, head, last, mconcatMap)
|
||||
import Data.List.Extra qualified as List
|
||||
import Data.List.NonEmpty qualified as NonEmpty
|
||||
import Data.List.NonEmpty.Extra (NonEmpty (..), head, last, maximum1, maximumOn1, minimum1, minimumOn1, nonEmpty, some1, (|:))
|
||||
import Data.List.NonEmpty.Extra
|
||||
( NonEmpty (..),
|
||||
head,
|
||||
last,
|
||||
maximum1,
|
||||
maximumOn1,
|
||||
minimum1,
|
||||
minimumOn1,
|
||||
nonEmpty,
|
||||
some1,
|
||||
(|:),
|
||||
)
|
||||
import Data.Maybe
|
||||
import Data.Monoid
|
||||
import Data.Ord
|
||||
@ -125,27 +134,24 @@ import Safe.Foldable
|
||||
import System.Directory
|
||||
import System.Exit
|
||||
import System.FilePath
|
||||
import System.IO hiding (appendFile, getContents, getLine, hGetContents, hGetLine, hPutStr, hPutStrLn, interact, putStr, putStrLn, readFile, readFile', writeFile)
|
||||
import System.IO hiding
|
||||
( appendFile,
|
||||
getContents,
|
||||
getLine,
|
||||
hGetContents,
|
||||
hGetLine,
|
||||
hPutStr,
|
||||
hPutStrLn,
|
||||
interact,
|
||||
putStr,
|
||||
putStrLn,
|
||||
readFile,
|
||||
readFile',
|
||||
writeFile,
|
||||
)
|
||||
import Text.Show (Show)
|
||||
import Text.Show qualified as Show
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Logical connectives
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
(∨) :: Bool -> Bool -> Bool
|
||||
(∨) = (||)
|
||||
|
||||
infixr 2 ∨
|
||||
|
||||
(∧) :: Bool -> Bool -> Bool
|
||||
(∧) = (&&)
|
||||
|
||||
infixr 3 ∧
|
||||
|
||||
(.||.) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
|
||||
(f .||. g) x = f x || g x
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- High-level syntax sugar.
|
||||
--------------------------------------------------------------------------------
|
||||
@ -249,8 +255,6 @@ undefined = Err.error "undefined"
|
||||
impossible :: HasCallStack => a
|
||||
impossible = Err.error "impossible"
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Errors
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
infixl 7 <+?>
|
||||
@ -263,6 +267,8 @@ infixl 7 <?>
|
||||
(<?>) :: Semigroup m => m -> Maybe m -> m
|
||||
(<?>) a = maybe a (a <>)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data Indexed a = Indexed
|
||||
{ _indexedIx :: Int,
|
||||
_indexedThing :: a
|
||||
|
||||
@ -35,6 +35,9 @@ prettyText = Text.renderStrict . layoutPretty defaultLayoutOptions . pretty
|
||||
vsep :: Foldable f => f (Doc a) -> Doc a
|
||||
vsep = PP.vsep . toList
|
||||
|
||||
vsep2 :: [Doc a] -> Doc a
|
||||
vsep2 = concatWith (\a b -> a <> line <> line <> b)
|
||||
|
||||
hsep :: Foldable f => f (Doc a) -> Doc a
|
||||
hsep = PP.hsep . toList
|
||||
|
||||
|
||||
@ -7,6 +7,7 @@ import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as S
|
||||
newtype FunctionInfo = FunctionInfo
|
||||
{ _functionInfoDef :: FunctionDef
|
||||
}
|
||||
deriving stock (Show)
|
||||
|
||||
data ConstructorInfo = ConstructorInfo
|
||||
{ _constructorInfoInductive :: InductiveInfo,
|
||||
|
||||
@ -57,7 +57,8 @@ data Statement
|
||||
data FunctionDef = FunctionDef
|
||||
{ _funDefName :: FunctionName,
|
||||
_funDefTypeSig :: Expression,
|
||||
_funDefClauses :: NonEmpty FunctionClause
|
||||
_funDefClauses :: NonEmpty FunctionClause,
|
||||
_funDefTerminating :: Bool
|
||||
}
|
||||
deriving stock (Eq, Show)
|
||||
|
||||
|
||||
@ -7,22 +7,22 @@ where
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Abstract.Language
|
||||
|
||||
patternVariables :: Pattern -> [VarName]
|
||||
patternVariables pat = case pat of
|
||||
PatternVariable v -> [v]
|
||||
PatternWildcard {} -> []
|
||||
PatternEmpty {} -> []
|
||||
PatternConstructorApp app -> appVariables app
|
||||
|
||||
appVariables :: ConstructorApp -> [VarName]
|
||||
appVariables (ConstructorApp _ ps) = concatMap patternVariables ps
|
||||
|
||||
smallerPatternVariables :: Pattern -> [VarName]
|
||||
smallerPatternVariables p = case p of
|
||||
smallerPatternVariables = \case
|
||||
PatternVariable {} -> []
|
||||
PatternWildcard {} -> []
|
||||
PatternEmpty {} -> []
|
||||
PatternConstructorApp app -> appVariables app
|
||||
where
|
||||
appVariables :: ConstructorApp -> [VarName]
|
||||
appVariables (ConstructorApp _ ps) = concatMap patternVariables ps
|
||||
|
||||
patternVariables :: Pattern -> [VarName]
|
||||
patternVariables pat = case pat of
|
||||
PatternVariable v -> [v]
|
||||
PatternWildcard {} -> []
|
||||
PatternEmpty {} -> []
|
||||
PatternConstructorApp app -> appVariables app
|
||||
|
||||
viewApp :: Expression -> (Expression, [Expression])
|
||||
viewApp e = case e of
|
||||
|
||||
@ -44,31 +44,17 @@ ppDefault = runPrettyCode defaultOptions
|
||||
runPrettyCode :: PrettyCode c => Options -> c -> Doc Ann
|
||||
runPrettyCode opts = run . runReader opts . ppCode
|
||||
|
||||
instance PrettyCode Iden where
|
||||
ppCode = ppSCode . idenName
|
||||
|
||||
instance PrettyCode Application where
|
||||
ppCode (Application l r) = do
|
||||
l' <- ppLeftExpression appFixity l
|
||||
r' <- ppRightExpression appFixity r
|
||||
return $ l' <+> r'
|
||||
|
||||
keyword :: Text -> Doc Ann
|
||||
keyword = annotate AnnKeyword . pretty
|
||||
|
||||
kwType :: Doc Ann
|
||||
kwType = keyword Str.type_
|
||||
|
||||
instance PrettyCode Universe where
|
||||
ppCode (Universe n) = return $ kwType <+?> (pretty <$> n)
|
||||
kwQuestion :: Doc Ann
|
||||
kwQuestion = keyword Str.questionMark
|
||||
|
||||
instance PrettyCode Expression where
|
||||
ppCode e = case e of
|
||||
ExpressionIden i -> ppCode i
|
||||
ExpressionUniverse u -> ppCode u
|
||||
ExpressionApplication a -> ppCode a
|
||||
ExpressionFunction f -> ppCode f
|
||||
ExpressionLiteral l -> ppSCode l
|
||||
kwWaveArrow :: Doc Ann
|
||||
kwWaveArrow = keyword Str.waveArrow
|
||||
|
||||
kwColon :: Doc Ann
|
||||
kwColon = keyword Str.colon
|
||||
@ -85,40 +71,6 @@ kwColonOne = keyword Str.colonOne
|
||||
kwColonOmega :: Doc Ann
|
||||
kwColonOmega = keyword Str.colonOmegaUnicode
|
||||
|
||||
instance PrettyCode Usage where
|
||||
ppCode u = return $ case u of
|
||||
UsageNone -> kwColonZero
|
||||
UsageOnce -> kwColonOne
|
||||
UsageOmega -> kwColon
|
||||
|
||||
instance PrettyCode FunctionParameter where
|
||||
ppCode FunctionParameter {..} = do
|
||||
case _paramName of
|
||||
Nothing -> ppLeftExpression funFixity _paramType
|
||||
Just n -> do
|
||||
paramName' <- ppSCode n
|
||||
paramType' <- ppCode _paramType
|
||||
paramUsage' <- ppCode _paramUsage
|
||||
return $ parens (paramName' <+> paramUsage' <+> paramType')
|
||||
|
||||
instance PrettyCode Function where
|
||||
ppCode Function {..} = do
|
||||
funParameter' <- ppCode _funParameter
|
||||
funReturn' <- ppRightExpression funFixity _funReturn
|
||||
return $ funParameter' <+> kwTo <+> funReturn'
|
||||
|
||||
instance PrettyCode FunctionRef where
|
||||
ppCode FunctionRef {..} = ppSCode _functionRefName
|
||||
|
||||
instance PrettyCode ConstructorRef where
|
||||
ppCode ConstructorRef {..} = ppSCode _constructorRefName
|
||||
|
||||
instance PrettyCode InductiveRef where
|
||||
ppCode InductiveRef {..} = ppSCode _inductiveRefName
|
||||
|
||||
instance PrettyCode AxiomRef where
|
||||
ppCode AxiomRef {..} = ppSCode _axiomRefName
|
||||
|
||||
parensCond :: Bool -> Doc Ann -> Doc Ann
|
||||
parensCond t d = if t then parens d else d
|
||||
|
||||
@ -153,7 +105,64 @@ ppLRExpression associates fixlr e =
|
||||
parensCond (atomParens associates (atomicity e) fixlr)
|
||||
<$> ppCode e
|
||||
|
||||
ppCodeAtom :: (HasAtomicity c, PrettyCode c, Members '[Reader Options] r) => c -> Sem r (Doc Ann)
|
||||
ppCodeAtom ::
|
||||
(HasAtomicity c, PrettyCode c, Members '[Reader Options] r) =>
|
||||
c ->
|
||||
Sem r (Doc Ann)
|
||||
ppCodeAtom c = do
|
||||
p' <- ppCode c
|
||||
return $ if isAtomic c then p' else parens p'
|
||||
|
||||
instance PrettyCode Iden where
|
||||
ppCode = ppSCode . idenName
|
||||
|
||||
instance PrettyCode Application where
|
||||
ppCode (Application l r) = do
|
||||
l' <- ppLeftExpression appFixity l
|
||||
r' <- ppRightExpression appFixity r
|
||||
return $ l' <+> r'
|
||||
|
||||
instance PrettyCode Universe where
|
||||
ppCode (Universe n) = return $ kwType <+?> (pretty <$> n)
|
||||
|
||||
instance PrettyCode Expression where
|
||||
ppCode e = case e of
|
||||
ExpressionIden i -> ppCode i
|
||||
ExpressionUniverse u -> ppCode u
|
||||
ExpressionApplication a -> ppCode a
|
||||
ExpressionFunction f -> ppCode f
|
||||
ExpressionLiteral l -> ppSCode l
|
||||
|
||||
instance PrettyCode Usage where
|
||||
ppCode u = return $ case u of
|
||||
UsageNone -> kwColonZero
|
||||
UsageOnce -> kwColonOne
|
||||
UsageOmega -> kwColon
|
||||
|
||||
instance PrettyCode FunctionParameter where
|
||||
ppCode FunctionParameter {..} = do
|
||||
case _paramName of
|
||||
Nothing -> ppLeftExpression funFixity _paramType
|
||||
Just n -> do
|
||||
paramName' <- ppSCode n
|
||||
paramType' <- ppCode _paramType
|
||||
paramUsage' <- ppCode _paramUsage
|
||||
return $ parens (paramName' <+> paramUsage' <+> paramType')
|
||||
|
||||
instance PrettyCode Function where
|
||||
ppCode Function {..} = do
|
||||
funParameter' <- ppCode _funParameter
|
||||
funReturn' <- ppRightExpression funFixity _funReturn
|
||||
return $ funParameter' <+> kwTo <+> funReturn'
|
||||
|
||||
instance PrettyCode FunctionRef where
|
||||
ppCode FunctionRef {..} = ppSCode _functionRefName
|
||||
|
||||
instance PrettyCode ConstructorRef where
|
||||
ppCode ConstructorRef {..} = ppSCode _constructorRefName
|
||||
|
||||
instance PrettyCode InductiveRef where
|
||||
ppCode InductiveRef {..} = ppSCode _inductiveRefName
|
||||
|
||||
instance PrettyCode AxiomRef where
|
||||
ppCode AxiomRef {..} = ppSCode _axiomRefName
|
||||
|
||||
@ -17,8 +17,6 @@ module MiniJuvix.Syntax.Concrete.Language
|
||||
)
|
||||
where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Data.Kind qualified as GHC
|
||||
import MiniJuvix.Prelude hiding (show)
|
||||
import MiniJuvix.Syntax.Backends
|
||||
@ -176,7 +174,8 @@ instance HasLoc OperatorSyntaxDef where
|
||||
|
||||
data TypeSignature (s :: Stage) = TypeSignature
|
||||
{ _sigName :: FunctionName s,
|
||||
_sigType :: ExpressionType s
|
||||
_sigType :: ExpressionType s,
|
||||
_sigTerminating :: Bool
|
||||
}
|
||||
|
||||
deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (TypeSignature s)
|
||||
|
||||
@ -1,7 +1,5 @@
|
||||
module MiniJuvix.Syntax.Concrete.Lexer where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Data.Text qualified as Text
|
||||
import GHC.Unicode
|
||||
import MiniJuvix.Internal.Strings qualified as Str
|
||||
@ -259,6 +257,9 @@ kwSemicolon = keyword Str.semicolon
|
||||
kwType :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwType = keyword Str.type_
|
||||
|
||||
kwTerminating :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwTerminating = keyword Str.terminating
|
||||
|
||||
kwUsing :: Member InfoTableBuilder r => ParsecS r ()
|
||||
kwUsing = keyword Str.using
|
||||
|
||||
|
||||
@ -247,8 +247,7 @@ match = do
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
letClause :: Member InfoTableBuilder r => ParsecS r (LetClause 'Parsed)
|
||||
letClause = do
|
||||
either LetTypeSig LetFunClause <$> auxTypeSigFunClause
|
||||
letClause = either LetTypeSig LetFunClause <$> auxTypeSigFunClause
|
||||
|
||||
letBlock :: Member InfoTableBuilder r => ParsecS r (LetBlock 'Parsed)
|
||||
letBlock = do
|
||||
@ -271,8 +270,12 @@ universe = do
|
||||
-- Type signature declaration
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
typeSignature :: Member InfoTableBuilder r => Symbol -> ParsecS r (TypeSignature 'Parsed)
|
||||
typeSignature _sigName = do
|
||||
typeSignature ::
|
||||
Member InfoTableBuilder r =>
|
||||
Bool ->
|
||||
Symbol ->
|
||||
ParsecS r (TypeSignature 'Parsed)
|
||||
typeSignature _sigTerminating _sigName = do
|
||||
kwColon
|
||||
_sigType <- expressionAtoms
|
||||
return TypeSignature {..}
|
||||
@ -286,9 +289,10 @@ auxTypeSigFunClause ::
|
||||
Member InfoTableBuilder r =>
|
||||
ParsecS r (Either (TypeSignature 'Parsed) (FunctionClause 'Parsed))
|
||||
auxTypeSigFunClause = do
|
||||
s <- symbol
|
||||
(Left <$> typeSignature s)
|
||||
<|> (Right <$> functionClause s)
|
||||
terminating <- isJust <$> optional kwTerminating
|
||||
sym <- symbol
|
||||
(Left <$> typeSignature terminating sym)
|
||||
<|> (Right <$> functionClause sym)
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
-- Axioms
|
||||
|
||||
@ -404,7 +404,7 @@ checkTypeSignature ::
|
||||
checkTypeSignature TypeSignature {..} = do
|
||||
sigType' <- checkParseExpressionAtoms _sigType
|
||||
sigName' <- bindFunctionSymbol _sigName
|
||||
registerFunction' TypeSignature {_sigName = sigName', _sigType = sigType'}
|
||||
registerFunction' TypeSignature {_sigName = sigName', _sigType = sigType', ..}
|
||||
|
||||
checkConstructorDef ::
|
||||
Members '[Error ScopeError, Reader LocalVars, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
|
||||
|
||||
@ -7,6 +7,7 @@ where
|
||||
|
||||
import MiniJuvix.Internal.Strings qualified as Str
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Prelude.Pretty qualified as PP
|
||||
import MiniJuvix.Syntax.Concrete.Language (Literal (..), LiteralLoc (..))
|
||||
import MiniJuvix.Syntax.Fixity
|
||||
import MiniJuvix.Syntax.MiniHaskell.Language
|
||||
@ -139,9 +140,7 @@ instance PrettyCode Statement where
|
||||
instance PrettyCode ModuleBody where
|
||||
ppCode m = do
|
||||
statements' <- mapM ppCode (m ^. moduleStatements)
|
||||
return $ vsep2 statements'
|
||||
where
|
||||
vsep2 = concatWith (\a b -> a <> line <> line <> b)
|
||||
return $ PP.vsep2 statements'
|
||||
|
||||
instance PrettyCode Literal where
|
||||
ppCode = \case
|
||||
|
||||
@ -235,8 +235,6 @@ instance PrettyCode ModuleBody where
|
||||
ppCode m = do
|
||||
everything <- mapM ppCode (m ^. moduleStatements)
|
||||
return $ vsep2 everything
|
||||
where
|
||||
vsep2 = concatWith (\a b -> a <> line <> line <> b)
|
||||
|
||||
instance PrettyCode Module where
|
||||
ppCode m = do
|
||||
|
||||
@ -7,13 +7,14 @@ where
|
||||
import Data.HashMap.Strict qualified as HashMap
|
||||
import Data.HashSet qualified as HashSet
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Prelude.Pretty
|
||||
import MiniJuvix.Syntax.Abstract.Language.Extra
|
||||
import MiniJuvix.Syntax.Abstract.Pretty.Base
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Name qualified as S
|
||||
import MiniJuvix.Termination.Types
|
||||
import Prettyprinter as PP
|
||||
|
||||
type Edges = HashMap (FunctionName, FunctionName) Edge
|
||||
type Graph = HashMap (FunctionName, FunctionName) Edge
|
||||
|
||||
data Edge = Edge
|
||||
{ _edgeFrom :: FunctionName,
|
||||
@ -21,37 +22,28 @@ data Edge = Edge
|
||||
_edgeMatrices :: HashSet CallMatrix
|
||||
}
|
||||
|
||||
newtype CompleteCallGraph = CompleteCallGraph Edges
|
||||
newtype CompleteCallGraph = CompleteCallGraph Graph
|
||||
|
||||
data ReflexiveEdge = ReflexiveEdge
|
||||
{ _redgeFun :: FunctionName,
|
||||
_redgeMatrices :: HashSet CallMatrix
|
||||
{ _reflexiveEdgeFun :: FunctionName,
|
||||
_reflexiveEdgeMatrices :: HashSet CallMatrix
|
||||
}
|
||||
|
||||
data RecursiveBehaviour = RecursiveBehaviour
|
||||
{ _recBehaviourFunction :: FunctionName,
|
||||
_recBehaviourMatrix :: [[Rel]]
|
||||
{ _recursiveBehaviourFun :: FunctionName,
|
||||
_recursiveBehaviourMatrix :: [[Rel]]
|
||||
}
|
||||
|
||||
makeLenses ''RecursiveBehaviour
|
||||
makeLenses ''Edge
|
||||
makeLenses ''RecursiveBehaviour
|
||||
makeLenses ''ReflexiveEdge
|
||||
|
||||
multiply :: CallMatrix -> CallMatrix -> CallMatrix
|
||||
multiply a b = map sumProdRow a
|
||||
where
|
||||
rowB :: Int -> CallRow
|
||||
rowB i = CallRow $ case b !? i of
|
||||
Just (CallRow (Just c)) -> Just c
|
||||
_ -> Nothing
|
||||
sumProdRow :: CallRow -> CallRow
|
||||
sumProdRow (CallRow mr) = CallRow $ do
|
||||
(ki, ra) <- mr
|
||||
(j, rb) <- _callRow (rowB ki)
|
||||
return (j, mul' ra rb)
|
||||
-------------------------------------------------------------------------------
|
||||
-- Misc
|
||||
-------------------------------------------------------------------------------
|
||||
|
||||
multiplyMany :: HashSet CallMatrix -> HashSet CallMatrix -> HashSet CallMatrix
|
||||
multiplyMany r s = HashSet.fromList [multiply a b | a <- toList r, b <- toList s]
|
||||
fromEdgeList :: [Edge] -> Graph
|
||||
fromEdgeList l = HashMap.fromList [((e ^. edgeFrom, e ^. edgeTo), e) | e <- l]
|
||||
|
||||
composeEdge :: Edge -> Edge -> Maybe Edge
|
||||
composeEdge a b = do
|
||||
@ -63,6 +55,44 @@ composeEdge a b = do
|
||||
_edgeMatrices = multiplyMany (a ^. edgeMatrices) (b ^. edgeMatrices)
|
||||
}
|
||||
|
||||
edgesCompose :: Graph -> Graph -> Graph
|
||||
edgesCompose g h =
|
||||
fromEdgeList
|
||||
(catMaybes [composeEdge u v | u <- toList g, v <- toList h])
|
||||
|
||||
edgeUnion :: Edge -> Edge -> Edge
|
||||
edgeUnion a b
|
||||
| a ^. edgeFrom == b ^. edgeFrom,
|
||||
a ^. edgeTo == b ^. edgeTo =
|
||||
Edge
|
||||
(a ^. edgeFrom)
|
||||
(a ^. edgeTo)
|
||||
(HashSet.union (a ^. edgeMatrices) (b ^. edgeMatrices))
|
||||
| otherwise = impossible
|
||||
|
||||
edgesUnion :: Graph -> Graph -> Graph
|
||||
edgesUnion = HashMap.unionWith edgeUnion
|
||||
|
||||
edgesCount :: Graph -> Int
|
||||
edgesCount es = sum [HashSet.size (e ^. edgeMatrices) | e <- toList es]
|
||||
|
||||
multiply :: CallMatrix -> CallMatrix -> CallMatrix
|
||||
multiply a b = map sumProdRow a
|
||||
where
|
||||
rowB :: Int -> CallRow
|
||||
rowB i = CallRow $ case b !? i of
|
||||
Just (CallRow (Just c)) -> Just c
|
||||
_ -> Nothing
|
||||
|
||||
sumProdRow :: CallRow -> CallRow
|
||||
sumProdRow (CallRow mr) = CallRow $ do
|
||||
(ki, ra) <- mr
|
||||
(j, rb) <- _callRow (rowB ki)
|
||||
return (j, mul' ra rb)
|
||||
|
||||
multiplyMany :: HashSet CallMatrix -> HashSet CallMatrix -> HashSet CallMatrix
|
||||
multiplyMany r s = HashSet.fromList [multiply a b | a <- toList r, b <- toList s]
|
||||
|
||||
fromFunCall :: FunctionRef -> FunCall -> Call
|
||||
fromFunCall caller fc =
|
||||
Call
|
||||
@ -78,61 +108,37 @@ unsafeFilterGraph funNames (CompleteCallGraph g) =
|
||||
CompleteCallGraph (HashMap.filterWithKey (\(f, _) _ -> S.symbolText f `elem` funNames) g)
|
||||
|
||||
completeCallGraph :: CallMap -> CompleteCallGraph
|
||||
completeCallGraph cm = CompleteCallGraph (go startingEdges)
|
||||
completeCallGraph CallMap {..} = CompleteCallGraph (go startingEdges)
|
||||
where
|
||||
startingEdges :: Edges
|
||||
startingEdges :: Graph
|
||||
startingEdges = foldr insertCall mempty allCalls
|
||||
where
|
||||
insertCall :: Call -> Edges -> Edges
|
||||
insertCall :: Call -> Graph -> Graph
|
||||
insertCall Call {..} = HashMap.alter (Just . aux) (_callFrom, _callTo)
|
||||
where
|
||||
aux :: Maybe Edge -> Edge
|
||||
aux me = case me of
|
||||
Nothing -> Edge _callFrom _callTo (HashSet.singleton _callMatrix)
|
||||
Just e -> over edgeMatrices (HashSet.insert _callMatrix) e
|
||||
|
||||
allCalls :: [Call]
|
||||
allCalls =
|
||||
[ fromFunCall caller funCall
|
||||
| (caller, callerMap) <- HashMap.toList (cm ^. callMap),
|
||||
| (caller, callerMap) <- HashMap.toList _callMap,
|
||||
(_, funCalls) <- HashMap.toList callerMap,
|
||||
funCall <- funCalls
|
||||
]
|
||||
|
||||
go :: Edges -> Edges
|
||||
go m
|
||||
| edgesCount m == edgesCount m' = m
|
||||
| otherwise = go m'
|
||||
go :: Graph -> Graph
|
||||
go g
|
||||
| edgesCount g == edgesCount g' = g
|
||||
| otherwise = go g'
|
||||
where
|
||||
m' = step m
|
||||
g' = step g
|
||||
|
||||
step :: Edges -> Edges
|
||||
step :: Graph -> Graph
|
||||
step s = edgesUnion (edgesCompose s startingEdges) s
|
||||
|
||||
fromEdgeList :: [Edge] -> Edges
|
||||
fromEdgeList l = HashMap.fromList [((e ^. edgeFrom, e ^. edgeTo), e) | e <- l]
|
||||
|
||||
edgesCompose :: Edges -> Edges -> Edges
|
||||
edgesCompose a b =
|
||||
fromEdgeList $
|
||||
catMaybes
|
||||
[composeEdge ea eb | ea <- toList a, eb <- toList b]
|
||||
|
||||
edgeUnion :: Edge -> Edge -> Edge
|
||||
edgeUnion a b
|
||||
| a ^. edgeFrom == b ^. edgeFrom,
|
||||
a ^. edgeTo == b ^. edgeTo =
|
||||
Edge
|
||||
(a ^. edgeFrom)
|
||||
(a ^. edgeTo)
|
||||
(HashSet.union (a ^. edgeMatrices) (b ^. edgeMatrices))
|
||||
| otherwise = impossible
|
||||
|
||||
edgesUnion :: Edges -> Edges -> Edges
|
||||
edgesUnion = HashMap.unionWith edgeUnion
|
||||
|
||||
edgesCount :: Edges -> Int
|
||||
edgesCount es = sum [HashSet.size (e ^. edgeMatrices) | e <- toList es]
|
||||
|
||||
reflexiveEdges :: CompleteCallGraph -> [ReflexiveEdge]
|
||||
reflexiveEdges (CompleteCallGraph es) = mapMaybe reflexive (toList es)
|
||||
where
|
||||
@ -155,14 +161,15 @@ callMatrixDiag m = [col i r | (i, r) <- zip [0 :: Int ..] m]
|
||||
recursiveBehaviour :: ReflexiveEdge -> RecursiveBehaviour
|
||||
recursiveBehaviour re =
|
||||
RecursiveBehaviour
|
||||
(re ^. redgeFun)
|
||||
(map callMatrixDiag (toList $ re ^. redgeMatrices))
|
||||
(re ^. reflexiveEdgeFun)
|
||||
(map callMatrixDiag (toList $ re ^. reflexiveEdgeMatrices))
|
||||
|
||||
findOrder :: RecursiveBehaviour -> Maybe LexOrder
|
||||
findOrder rb = LexOrder <$> listToMaybe (mapMaybe (isLexOrder >=> nonEmpty) allPerms)
|
||||
where
|
||||
b0 :: [[Rel]]
|
||||
b0 = rb ^. recBehaviourMatrix
|
||||
b0 = rb ^. recursiveBehaviourMatrix
|
||||
|
||||
indexed = map (zip [0 :: Int ..] . take minLength) b0
|
||||
where
|
||||
minLength = minimum (map length b0)
|
||||
@ -204,29 +211,32 @@ instance PrettyCode Edge where
|
||||
ppCode Edge {..} = do
|
||||
fromFun <- ppSCode _edgeFrom
|
||||
toFun <- ppSCode _edgeTo
|
||||
matrices <- indent 2 . ppMatrices . zip [0 :: Int ..] <$> mapM ppCode (toList _edgeMatrices)
|
||||
matrices <-
|
||||
indent 2 . ppMatrices . zip [0 :: Int ..]
|
||||
<$> mapM ppCode (toList _edgeMatrices)
|
||||
return $
|
||||
pretty ("Edge" :: Text) <+> fromFun <+> waveFun <+> toFun <> line
|
||||
pretty ("Edge" :: Text) <+> fromFun <+> kwWaveArrow <+> toFun <> line
|
||||
<> matrices
|
||||
where
|
||||
ppMatrices = vsep2 . map ppMatrix
|
||||
ppMatrix (i, t) =
|
||||
pretty ("Matrix" :: Text) <+> pretty i <> colon <> line
|
||||
<> t
|
||||
pretty ("Matrix" :: Text) <+> pretty i <> colon <> line <> t
|
||||
|
||||
instance PrettyCode CompleteCallGraph where
|
||||
ppCode :: forall r. Members '[Reader Options] r => CompleteCallGraph -> Sem r (Doc Ann)
|
||||
ppCode (CompleteCallGraph edges) = do
|
||||
es <- vsep2 <$> mapM ppCode (toList edges)
|
||||
return $ pretty ("Complete Call Graph:" :: Text) <> line <> es
|
||||
ppCode (CompleteCallGraph edges)
|
||||
| null edges = return $ pretty ("Empty graph" :: Text)
|
||||
| otherwise = do
|
||||
es <- vsep2 <$> mapM ppCode (toList edges)
|
||||
return $ pretty ("Complete call graph:" :: Text) <> line <> es <> pretty (length edges)
|
||||
|
||||
instance PrettyCode RecursiveBehaviour where
|
||||
ppCode :: forall r. Members '[Reader Options] r => RecursiveBehaviour -> Sem r (Doc Ann)
|
||||
ppCode :: Members '[Reader Options] r => RecursiveBehaviour -> Sem r (Doc Ann)
|
||||
ppCode (RecursiveBehaviour f m0) = do
|
||||
f' <- ppSCode f
|
||||
let m' = vsep (map (PP.list . map pretty) m)
|
||||
let m' = PP.vsep (map (PP.list . map pretty) m)
|
||||
return $
|
||||
pretty ("Recursive behaviour of " :: Text) <> f' <> colon <> line
|
||||
pretty ("Recursive behaviour of" :: Text) <+> f' <> colon <> line
|
||||
<> indent 2 (align m')
|
||||
where
|
||||
m = toList (HashSet.fromList m0)
|
||||
|
||||
@ -6,6 +6,7 @@ where
|
||||
|
||||
import Data.HashMap.Strict qualified as HashMap
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Abstract.InfoTable
|
||||
import MiniJuvix.Syntax.Abstract.Language.Extra
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Name (unqualifiedSymbol)
|
||||
import MiniJuvix.Termination.Types
|
||||
@ -22,7 +23,7 @@ viewCall ::
|
||||
Members '[Reader SizeInfo] r =>
|
||||
Expression ->
|
||||
Sem r (Maybe FunCall)
|
||||
viewCall e = case e of
|
||||
viewCall = \case
|
||||
ExpressionApplication (Application f x) -> do
|
||||
c <- viewCall f
|
||||
x' <- callArg
|
||||
@ -37,7 +38,7 @@ viewCall e = case e of
|
||||
lessThan :: Sem r CallRow
|
||||
lessThan = case x of
|
||||
ExpressionIden (IdenVar v) -> do
|
||||
s <- asks (HashMap.lookup v . _sizeSmaller)
|
||||
s :: Maybe Int <- asks (HashMap.lookup v . _sizeSmaller)
|
||||
return $ case s of
|
||||
Nothing -> CallRow Nothing
|
||||
Just s' -> CallRow (Just (s', RLe))
|
||||
@ -61,13 +62,21 @@ viewCall e = case e of
|
||||
addCall :: FunctionRef -> FunCall -> CallMap -> CallMap
|
||||
addCall fun c = over callMap (HashMap.alter (Just . insertCall c) fun)
|
||||
where
|
||||
insertCall :: FunCall -> Maybe (HashMap FunctionRef [FunCall]) -> HashMap FunctionRef [FunCall]
|
||||
insertCall f m = case m of
|
||||
insertCall ::
|
||||
FunCall ->
|
||||
Maybe (HashMap FunctionRef [FunCall]) ->
|
||||
HashMap FunctionRef [FunCall]
|
||||
insertCall f = \case
|
||||
Nothing -> singl f
|
||||
Just m' -> addFunCall f m'
|
||||
|
||||
singl :: FunCall -> HashMap FunctionRef [FunCall]
|
||||
singl f = HashMap.singleton (f ^. callRef) [f]
|
||||
addFunCall :: FunCall -> HashMap FunctionRef [FunCall] -> HashMap FunctionRef [FunCall]
|
||||
|
||||
addFunCall ::
|
||||
FunCall ->
|
||||
HashMap FunctionRef [FunCall] ->
|
||||
HashMap FunctionRef [FunCall]
|
||||
addFunCall fc = HashMap.insertWith (flip (<>)) (fc ^. callRef) [fc]
|
||||
|
||||
registerCall ::
|
||||
@ -78,13 +87,16 @@ registerCall c = do
|
||||
fun <- ask
|
||||
modify (addCall fun c)
|
||||
|
||||
buildCallMap :: TopModule -> CallMap
|
||||
buildCallMap = run . execState mempty . checkModule
|
||||
buildCallMap :: InfoTable -> TopModule -> CallMap
|
||||
buildCallMap infotable = run . execState mempty . runReader infotable . checkModule
|
||||
|
||||
checkModule :: Members '[State CallMap] r => TopModule -> Sem r ()
|
||||
checkModule ::
|
||||
Members '[State CallMap, Reader InfoTable] r =>
|
||||
TopModule ->
|
||||
Sem r ()
|
||||
checkModule m = checkModuleBody (m ^. moduleBody)
|
||||
|
||||
checkModuleBody :: Members '[State CallMap] r => ModuleBody -> Sem r ()
|
||||
checkModuleBody :: Members '[State CallMap, Reader InfoTable] r => ModuleBody -> Sem r ()
|
||||
checkModuleBody body = do
|
||||
mapM_ checkFunctionDef moduleFunctions
|
||||
mapM_ checkLocalModule moduleLocalModules
|
||||
@ -92,15 +104,22 @@ checkModuleBody body = do
|
||||
moduleFunctions = [f | StatementFunction f <- body ^. moduleStatements]
|
||||
moduleLocalModules = [f | StatementLocalModule f <- body ^. moduleStatements]
|
||||
|
||||
checkLocalModule :: Members '[State CallMap] r => LocalModule -> Sem r ()
|
||||
checkLocalModule :: Members '[State CallMap, Reader InfoTable] r => LocalModule -> Sem r ()
|
||||
checkLocalModule m = checkModuleBody (m ^. moduleBody)
|
||||
|
||||
checkFunctionDef :: Members '[State CallMap] r => FunctionDef -> Sem r ()
|
||||
checkFunctionDef def = runReader (FunctionRef (unqualifiedSymbol (def ^. funDefName))) $ do
|
||||
checkTypeSignature (def ^. funDefTypeSig)
|
||||
mapM_ checkFunctionClause (def ^. funDefClauses)
|
||||
checkFunctionDef ::
|
||||
Members '[State CallMap, Reader InfoTable] r =>
|
||||
FunctionDef ->
|
||||
Sem r ()
|
||||
checkFunctionDef FunctionDef {..} =
|
||||
runReader (FunctionRef (unqualifiedSymbol _funDefName)) $ do
|
||||
checkTypeSignature _funDefTypeSig
|
||||
mapM_ checkFunctionClause _funDefClauses
|
||||
|
||||
checkTypeSignature :: Members '[State CallMap, Reader FunctionRef] r => Expression -> Sem r ()
|
||||
checkTypeSignature ::
|
||||
Members '[State CallMap, Reader FunctionRef, Reader InfoTable] r =>
|
||||
Expression ->
|
||||
Sem r ()
|
||||
checkTypeSignature = runReader (emptySizeInfo :: SizeInfo) . checkExpression
|
||||
|
||||
emptySizeInfo :: SizeInfo
|
||||
@ -120,29 +139,39 @@ mkSizeInfo ps = SizeInfo {..}
|
||||
]
|
||||
|
||||
checkFunctionClause ::
|
||||
Members '[State CallMap, Reader FunctionRef] r =>
|
||||
Members '[State CallMap, Reader FunctionRef, Reader InfoTable] r =>
|
||||
FunctionClause ->
|
||||
Sem r ()
|
||||
checkFunctionClause cl =
|
||||
runReader (mkSizeInfo (cl ^. clausePatterns)) $
|
||||
checkExpression (cl ^. clauseBody)
|
||||
checkFunctionClause FunctionClause {..} =
|
||||
runReader (mkSizeInfo _clausePatterns) $ checkExpression _clauseBody
|
||||
|
||||
checkExpression :: Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r => Expression -> Sem r ()
|
||||
checkExpression e = do
|
||||
mc <- viewCall e
|
||||
case mc of
|
||||
checkExpression ::
|
||||
Members '[State CallMap, Reader FunctionRef, Reader InfoTable, Reader SizeInfo] r =>
|
||||
Expression ->
|
||||
Sem r ()
|
||||
checkExpression e =
|
||||
viewCall e >>= \case
|
||||
Just c -> do
|
||||
registerCall c
|
||||
mapM_ (checkExpression . snd) (c ^. callArgs)
|
||||
h <- asks _infoFunctions
|
||||
let fname = c ^. callRef
|
||||
info = HashMap.lookupDefault impossible fname h
|
||||
markedTerminating = info ^. (functionInfoDef . funDefTerminating)
|
||||
if
|
||||
| markedTerminating -> do
|
||||
let cargs = map (\x -> (CallRow (Just (0, RLe)), snd x)) (c ^. callArgs)
|
||||
registerCall $ FunCall fname cargs
|
||||
| otherwise -> do
|
||||
registerCall c
|
||||
mapM_ (checkExpression . snd) (c ^. callArgs)
|
||||
Nothing -> case e of
|
||||
ExpressionApplication a -> checkApplication a
|
||||
ExpressionFunction f -> checkFunction f
|
||||
ExpressionIden {} -> return ()
|
||||
ExpressionUniverse {} -> return ()
|
||||
ExpressionFunction f -> checkFunction f
|
||||
ExpressionLiteral {} -> return ()
|
||||
|
||||
checkApplication ::
|
||||
Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r =>
|
||||
Members '[State CallMap, Reader FunctionRef, Reader InfoTable, Reader SizeInfo] r =>
|
||||
Application ->
|
||||
Sem r ()
|
||||
checkApplication (Application l r) = do
|
||||
@ -150,7 +179,7 @@ checkApplication (Application l r) = do
|
||||
checkExpression r
|
||||
|
||||
checkFunction ::
|
||||
Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r =>
|
||||
Members '[State CallMap, Reader FunctionRef, Reader InfoTable, Reader SizeInfo] r =>
|
||||
Function ->
|
||||
Sem r ()
|
||||
checkFunction (Function l r) = do
|
||||
@ -158,7 +187,7 @@ checkFunction (Function l r) = do
|
||||
checkExpression r
|
||||
|
||||
checkFunctionParameter ::
|
||||
Members '[State CallMap, Reader FunctionRef, Reader SizeInfo] r =>
|
||||
Members '[State CallMap, Reader FunctionRef, Reader InfoTable, Reader SizeInfo] r =>
|
||||
FunctionParameter ->
|
||||
Sem r ()
|
||||
checkFunctionParameter p = checkExpression (p ^. paramType)
|
||||
|
||||
@ -44,8 +44,24 @@ newtype LexOrder = LexOrder (NonEmpty Int)
|
||||
makeLenses ''FunCall
|
||||
makeLenses ''CallMap
|
||||
|
||||
filterCallMap :: Foldable f => f Text -> CallMap -> CallMap
|
||||
filterCallMap funNames =
|
||||
over
|
||||
callMap
|
||||
( HashMap.filterWithKey
|
||||
( \k _ ->
|
||||
S.symbolText
|
||||
(nameUnqualify (k ^. functionRefName))
|
||||
`elem` funNames
|
||||
)
|
||||
)
|
||||
|
||||
instance PrettyCode FunCall where
|
||||
ppCode :: forall r. Members '[Reader Options] r => FunCall -> Sem r (Doc Ann)
|
||||
ppCode ::
|
||||
forall r.
|
||||
Members '[Reader Options] r =>
|
||||
FunCall ->
|
||||
Sem r (Doc Ann)
|
||||
ppCode (FunCall f args) = do
|
||||
args' <- mapM ppArg args
|
||||
f' <- ppCode f
|
||||
@ -71,26 +87,21 @@ instance PrettyCode FunCall where
|
||||
dbrackets x = pretty '⟦' <> x <> pretty '⟧'
|
||||
|
||||
instance PrettyCode CallMap where
|
||||
ppCode :: forall r. Members '[Reader Options] r => CallMap -> Sem r (Doc Ann)
|
||||
ppCode ::
|
||||
forall r.
|
||||
Members '[Reader Options] r =>
|
||||
CallMap ->
|
||||
Sem r (Doc Ann)
|
||||
ppCode (CallMap m) = vsep <$> mapM ppEntry (HashMap.toList m)
|
||||
where
|
||||
ppEntry :: (A.FunctionRef, HashMap A.FunctionRef [FunCall]) -> Sem r (Doc Ann)
|
||||
ppEntry (fun, mcalls) = do
|
||||
fun' <- annotate AnnImportant <$> ppCode fun
|
||||
calls' <- vsep <$> mapM ppCode calls
|
||||
return $ fun' <+> waveFun <+> align calls'
|
||||
return $ fun' <+> kwWaveArrow <+> align calls'
|
||||
where
|
||||
calls = concat (HashMap.elems mcalls)
|
||||
|
||||
kwQuestion :: Doc Ann
|
||||
kwQuestion = annotate AnnKeyword "?"
|
||||
|
||||
waveFun :: Doc ann
|
||||
waveFun = pretty ("↝" :: Text)
|
||||
|
||||
vsep2 :: [Doc ann] -> Doc ann
|
||||
vsep2 = concatWith (\a b -> a <> line <> line <> b)
|
||||
|
||||
instance PrettyCode CallRow where
|
||||
ppCode (CallRow r) = return $ case r of
|
||||
Nothing -> kwQuestion
|
||||
@ -99,6 +110,3 @@ instance PrettyCode CallRow where
|
||||
|
||||
instance PrettyCode CallMatrix where
|
||||
ppCode l = vsep <$> mapM ppCode l
|
||||
|
||||
filterCallMap :: Foldable f => f Text -> CallMap -> CallMap
|
||||
filterCallMap funNames = over callMap (HashMap.filterWithKey (\k _ -> S.symbolText (nameUnqualify (k ^. functionRefName)) `elem` funNames))
|
||||
|
||||
@ -1,13 +1,9 @@
|
||||
module MiniJuvix.Termination.Types.SizeRelation where
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Data.Semiring
|
||||
import MiniJuvix.Prelude
|
||||
import Prettyprinter
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
data Rel
|
||||
= RJust Rel'
|
||||
| RNothing
|
||||
|
||||
@ -29,16 +29,22 @@ entryAbstract _resultScoper = do
|
||||
where
|
||||
ms = _resultScoper ^. Scoper.resultModules
|
||||
|
||||
-- translateModule :: Module 'Scoped 'ModuleTop -> Either Err (InfoTable, A.TopModule)
|
||||
-- translateModule = run . runError . runInfoTableBuilder . goTopModule
|
||||
|
||||
goTopModule :: Members '[Error Err, InfoTableBuilder] r => Module 'Scoped 'ModuleTop -> Sem r A.TopModule
|
||||
goTopModule ::
|
||||
Members '[Error Err, InfoTableBuilder] r =>
|
||||
Module 'Scoped 'ModuleTop ->
|
||||
Sem r A.TopModule
|
||||
goTopModule = goModule
|
||||
|
||||
goLocalModule :: Members '[Error Err, InfoTableBuilder] r => Module 'Scoped 'ModuleLocal -> Sem r A.LocalModule
|
||||
goLocalModule ::
|
||||
Members '[Error Err, InfoTableBuilder] r =>
|
||||
Module 'Scoped 'ModuleLocal ->
|
||||
Sem r A.LocalModule
|
||||
goLocalModule = goModule
|
||||
|
||||
goModule :: (Members '[Error Err, InfoTableBuilder] r, ModulePathType 'Scoped t ~ S.Name' c) => Module 'Scoped t -> Sem r (A.Module c)
|
||||
goModule ::
|
||||
(Members '[Error Err, InfoTableBuilder] r, ModulePathType 'Scoped t ~ S.Name' c) =>
|
||||
Module 'Scoped t ->
|
||||
Sem r (A.Module c)
|
||||
goModule (Module n par b) = case par of
|
||||
[] -> A.Module n <$> goModuleBody b
|
||||
_ -> unsupported "Module parameters"
|
||||
@ -62,6 +68,7 @@ goModuleBody ss' = do
|
||||
where
|
||||
ss :: [Indexed (Statement 'Scoped)]
|
||||
ss = zipWith Indexed [0 ..] ss'
|
||||
|
||||
compiledFunctions :: Sem r [Indexed A.FunctionDef]
|
||||
compiledFunctions =
|
||||
sequence $
|
||||
@ -105,10 +112,11 @@ goFunctionDef ::
|
||||
TypeSignature 'Scoped ->
|
||||
NonEmpty (FunctionClause 'Scoped) ->
|
||||
Sem r A.FunctionDef
|
||||
goFunctionDef sig clauses = do
|
||||
let _funDefName = sig ^. sigName
|
||||
goFunctionDef TypeSignature {..} clauses = do
|
||||
let _funDefName = _sigName
|
||||
_funDefTerminating = _sigTerminating
|
||||
_funDefClauses <- mapM goFunctionClause clauses
|
||||
_funDefTypeSig <- goExpression (sig ^. sigType)
|
||||
_funDefTypeSig <- goExpression _sigType
|
||||
registerFunction' A.FunctionDef {..}
|
||||
|
||||
goFunctionClause ::
|
||||
@ -173,14 +181,15 @@ goConstructorDef ::
|
||||
Members '[Error Err] r =>
|
||||
InductiveConstructorDef 'Scoped ->
|
||||
Sem r A.InductiveConstructorDef
|
||||
goConstructorDef (InductiveConstructorDef c ty) = A.InductiveConstructorDef c <$> goExpression ty
|
||||
goConstructorDef (InductiveConstructorDef c ty) =
|
||||
A.InductiveConstructorDef c <$> goExpression ty
|
||||
|
||||
goExpression ::
|
||||
forall r.
|
||||
Members '[Error Err] r =>
|
||||
Expression ->
|
||||
Sem r A.Expression
|
||||
goExpression e = case e of
|
||||
goExpression = \case
|
||||
ExpressionIdentifier nt -> return (goIden nt)
|
||||
ExpressionParensIdentifier nt -> return (goIden nt)
|
||||
ExpressionApplication a -> A.ExpressionApplication <$> goApplication a
|
||||
@ -251,17 +260,26 @@ goPatternApplication ::
|
||||
Sem r A.ConstructorApp
|
||||
goPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternApplication a)
|
||||
|
||||
goPatternConstructor :: forall r. Members '[Error Err] r => ConstructorRef -> Sem r A.ConstructorApp
|
||||
goPatternConstructor ::
|
||||
Members '[Error Err] r =>
|
||||
ConstructorRef ->
|
||||
Sem r A.ConstructorApp
|
||||
goPatternConstructor a = uncurry A.ConstructorApp <$> viewApp (PatternConstructor a)
|
||||
|
||||
goInfixPatternApplication :: forall r. Members '[Error Err] r => PatternInfixApp -> Sem r A.ConstructorApp
|
||||
goInfixPatternApplication ::
|
||||
Members '[Error Err] r =>
|
||||
PatternInfixApp ->
|
||||
Sem r A.ConstructorApp
|
||||
goInfixPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternInfixApplication a)
|
||||
|
||||
goPostfixPatternApplication :: forall r. Members '[Error Err] r => PatternPostfixApp -> Sem r A.ConstructorApp
|
||||
goPostfixPatternApplication ::
|
||||
Members '[Error Err] r =>
|
||||
PatternPostfixApp ->
|
||||
Sem r A.ConstructorApp
|
||||
goPostfixPatternApplication a = uncurry A.ConstructorApp <$> viewApp (PatternPostfixApplication a)
|
||||
|
||||
viewApp :: forall r. Members '[Error Err] r => Pattern -> Sem r (A.ConstructorRef, [A.Pattern])
|
||||
viewApp p = case p of
|
||||
viewApp = \case
|
||||
PatternConstructor c -> return (goConstructorRef c, [])
|
||||
PatternApplication (PatternApp l r) -> do
|
||||
r' <- goPattern r
|
||||
@ -283,7 +301,7 @@ viewApp p = case p of
|
||||
goConstructorRef :: ConstructorRef -> A.ConstructorRef
|
||||
goConstructorRef (ConstructorRef' n) = A.ConstructorRef n
|
||||
|
||||
goPattern :: forall r. Members '[Error Err] r => Pattern -> Sem r A.Pattern
|
||||
goPattern :: Members '[Error Err] r => Pattern -> Sem r A.Pattern
|
||||
goPattern p = case p of
|
||||
PatternVariable a -> return $ A.PatternVariable a
|
||||
PatternConstructor c -> A.PatternConstructorApp <$> goPatternConstructor c
|
||||
|
||||
@ -13,8 +13,6 @@ module MiniJuvix.Utils.Version
|
||||
)
|
||||
where
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
import Data.Version (showVersion)
|
||||
import Development.GitRev (gitBranch, gitCommitDate, gitHash)
|
||||
import MiniJuvix.Prelude hiding (Doc)
|
||||
@ -23,8 +21,6 @@ import Prettyprinter as PP
|
||||
import Prettyprinter.Render.Text (renderIO)
|
||||
import System.Environment (getProgName)
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
versionDoc :: Doc Text
|
||||
versionDoc = PP.pretty (showVersion Paths_minijuvix.version)
|
||||
|
||||
|
||||
11
tests/negative/Termination/Loop.mjuvix
Normal file
11
tests/negative/Termination/Loop.mjuvix
Normal file
@ -0,0 +1,11 @@
|
||||
module NoLexOrde;
|
||||
|
||||
axiom A : Type;
|
||||
|
||||
f : A -> A -> A;
|
||||
g : A -> A -> A;
|
||||
|
||||
g x y := f x x;
|
||||
f x y := g x (f x x);
|
||||
|
||||
end;
|
||||
6
tests/negative/Termination/ToEmpty.mjuvix
Normal file
6
tests/negative/Termination/ToEmpty.mjuvix
Normal file
@ -0,0 +1,6 @@
|
||||
module ToEmpty;
|
||||
axiom A : Type;
|
||||
inductive Empty {};
|
||||
f : A -> Empty;
|
||||
f x := f x;
|
||||
end;
|
||||
13
tests/positive/Termination/TerminatingF.mjuvix
Normal file
13
tests/positive/Termination/TerminatingF.mjuvix
Normal file
@ -0,0 +1,13 @@
|
||||
module TerminatingF;
|
||||
|
||||
axiom A : Type;
|
||||
|
||||
terminating
|
||||
f : A -> A -> A;
|
||||
|
||||
g : A -> A -> A;
|
||||
|
||||
g x y := f x x;
|
||||
f x y := g x (f x x);
|
||||
|
||||
end;
|
||||
13
tests/positive/Termination/TerminatingG.mjuvix
Normal file
13
tests/positive/Termination/TerminatingG.mjuvix
Normal file
@ -0,0 +1,13 @@
|
||||
module TerminatingG;
|
||||
|
||||
axiom A : Type;
|
||||
|
||||
f : A -> A -> A;
|
||||
|
||||
terminating
|
||||
g : A -> A -> A;
|
||||
|
||||
g x y := f x x;
|
||||
f x y := g x (f x x);
|
||||
|
||||
end;
|
||||
7
tests/positive/Termination/ToEmpty.mjuvix
Normal file
7
tests/positive/Termination/ToEmpty.mjuvix
Normal file
@ -0,0 +1,7 @@
|
||||
module ToEmpty;
|
||||
axiom A : Type;
|
||||
inductive Empty {};
|
||||
terminating
|
||||
f : A -> Empty;
|
||||
f x := f x;
|
||||
end;
|
||||
Loading…
Reference in New Issue
Block a user