From 2d0cc9f3708fb88f4dc5bf0d3ef41ef8c52b4602 Mon Sep 17 00:00:00 2001 From: Emmet Murray Date: Wed, 11 Dec 2019 11:56:05 +1100 Subject: [PATCH 1/7] Added stub for termination checking --- minigent/src/Minigent/CLI.hs | 14 ++- minigent/src/Minigent/Syntax/Utils.hs | 3 +- minigent/src/Minigent/Termination.hs | 145 ++++++++++++++++++++++++++ 3 files changed, 159 insertions(+), 3 deletions(-) create mode 100644 minigent/src/Minigent/Termination.hs diff --git a/minigent/src/Minigent/CLI.hs b/minigent/src/Minigent/CLI.hs index 1ac1619f6..91d0d6b4b 100644 --- a/minigent/src/Minigent/CLI.hs +++ b/minigent/src/Minigent/CLI.hs @@ -27,6 +27,7 @@ import Minigent.Syntax.PrettyPrint import Minigent.Environment import Minigent.Reorganiser import Minigent.TC +import Minigent.Termination import Minigent.CG import Control.Monad import Control.Applicative @@ -47,7 +48,7 @@ import Data.Text.Prettyprint.Doc (unAnnotateS, unAnnotate, defaultLayoutOptions, -- | The phases of the compiler, ordered in the order listed. -data Phase = Lex | Parse | Reorg | TC | CG deriving (Ord, Enum, Eq) +data Phase = Lex | Parse | Reorg | TC | Term | CG deriving (Ord, Enum, Eq) -- | The way a dump should be formatted when printed. data Format = PrettyColour -- ^ Print with a pretty printer and ANSI colours if printing to stdout @@ -199,6 +200,15 @@ tcPhase colour envs pure [] go (Right b) = pure [b] +terminationPhase :: GlobalEnvironments -> IO () +terminationPhase envs + = case termCheck envs of + [] -> do return () + xs -> do -- Error + mapM_ (hPutStrLn stderr) xs + return () + + cgPhase :: GlobalEnvironments -> IO String cgPhase gs = pure (cg gs) @@ -298,6 +308,8 @@ compiler phase dirs files = do upTo TC binds <- tcPhase (NoColour `elem` dirs) envs mapM_ (tcDump binds) dirs + upTo Term + _ <- terminationPhase envs upTo CG barf <- cgPhase binds mapM_ (cgDump barf) dirs diff --git a/minigent/src/Minigent/Syntax/Utils.hs b/minigent/src/Minigent/Syntax/Utils.hs index e8b7c0402..8738d5412 100644 --- a/minigent/src/Minigent/Syntax/Utils.hs +++ b/minigent/src/Minigent/Syntax/Utils.hs @@ -297,5 +297,4 @@ unifVars :: S.Stream VarName unifVars = S.fromList names where names = [ g:n | n <- nums, g <- "𝛂𝛃𝛄𝛅𝛆𝛇𝛈𝛉𝛊𝛋𝛍𝛎𝛏𝛑𝛖𝛗𝛘𝛙" ] - nums = "":map show [1 :: Integer ..] - + nums = "":map show [1 :: Integer ..] \ No newline at end of file diff --git a/minigent/src/Minigent/Termination.hs b/minigent/src/Minigent/Termination.hs new file mode 100644 index 000000000..f0905bb2c --- /dev/null +++ b/minigent/src/Minigent/Termination.hs @@ -0,0 +1,145 @@ + +-- | +-- Module : Minigent.Termination +-- Copyright : (c) Data61 2018-2019 +-- Commonwealth Science and Research Organisation (CSIRO) +-- ABN 41 687 119 230 +-- License : BSD3 +-- +-- The termination checking module +-- +-- May be used qualified or unqualified. +module Minigent.Termination + ( termCheck ) where + +import Minigent.Fresh +import Minigent.Syntax +import Minigent.Syntax.Utils +import Minigent.Environment + +import Control.Monad.State.Strict +import Data.Maybe (maybeToList) + +import qualified Data.Map as M +import qualified Data.Set as S + +-- A directed graph +type Node = String +type Graph = M.Map Node [Node] + +-- Our environment +type Env a = FreshT VarName (State (M.Map VarName VarName)) a + +infixr 0 :<: +data Assertion = + VarName :<: VarName -- ^ Structurally less than + | VarName :~: VarName -- ^ Structurally equal to + deriving (Eq, Ord, Show) + + +termCheck :: GlobalEnvironments -> [String] +termCheck = undefined + +termAssertionGen :: Expr -> Env ([Assertion], [VarName]) +termAssertionGen expr + = case expr of + PrimOp _ es -> + join $ map termAssertionGen es + Sig e _ -> + termAssertionGen e + Apply f e -> do + a <- termAssertionGen f + b <- termAssertionGen e + c <- getv e + return $ flatten [([],maybeToList c), a, b] + Struct fs -> + let es = map snd fs + in join $ map termAssertionGen es + If b e1 e2 -> + join $ map termAssertionGen [b, e1, e2] + Let x e1 e2 -> do + -- First evaluate the variable binding expression + a <- termAssertionGen e1 + + -- Preserve the old state + env <- lift $ get + let old = M.lookup x env + + -- Map our bound program variable to a new name + fvar <- insert x + + -- Evaluate the rest + res <- termAssertionGen e2 + + -- Roll back the state for the program variable + undo x old + + -- calculate the assertion for the old variable + env <- lift $ get + mv <- getv e1 + let l = (case mv of + Just x' -> [fvar :~: (env M.! x')] + Nothing -> []) + + return $ flatten [(l,[]), res] + + _ -> return ([],[]) + + where + + -- Returns the variable name from an environment if it exists, otherwise nothing + getv :: Expr -> Env (Maybe VarName) + getv e = do + env <- lift $ get + return $ + case e of + Var v -> Just $ env M.! v + _ -> Nothing + + -- Updates an environment binding + insert :: VarName -> Env VarName + insert v = do + e <- lift $ get + n <- fresh + lift $ put (M.insert v n e) + return n + + undo :: VarName -> Maybe VarName -> Env () + undo x m = do + env <- lift $ get + lift $ put (M.delete x env) + case m of + Just v -> lift $ put (M.insert x v env) + _ -> return () + + join :: [Env ([Assertion], [VarName])] -> Env ([Assertion], [VarName]) + join (e:es) = do + (a,b) <- e + (as,bs) <- join es + return (a ++ as, b ++ bs) + join [] = return ([],[]) + + flatten :: [([Assertion], [VarName])] -> ([Assertion], [VarName]) + flatten (x:xs) = + let rest = flatten xs + in (fst x ++ fst rest, snd x ++ snd rest) + flatten [] = ([],[]) + + add :: [Maybe Assertion] -> [VarName] -> ([Maybe Assertion], [VarName]) -> ([Maybe Assertion], [VarName]) + add a g t = (a ++ fst t, g ++ snd t) + +hasPathTo :: Node -> Node -> Graph -> Bool +hasPathTo src dst g + = hasPathTo' src dst g S.empty + where + hasPathTo' :: Node -> Node -> Graph -> S.Set Node -> Bool + hasPathTo' s d g seen = + case M.lookup s g of + Nothing -> False + Just nbs -> + any (\n -> + n == dst || + (notElem n seen && + hasPathTo' n d g (S.insert n seen)) + ) nbs + From 5a13357deab9bf1162a1e665746ca7b80ce54413 Mon Sep 17 00:00:00 2001 From: Emmet Murray Date: Wed, 11 Dec 2019 16:39:13 +1100 Subject: [PATCH 2/7] minigent: further work on termination gen --- minigent/src/Minigent/Termination.hs | 109 +++++++++++++-------------- 1 file changed, 52 insertions(+), 57 deletions(-) diff --git a/minigent/src/Minigent/Termination.hs b/minigent/src/Minigent/Termination.hs index f0905bb2c..79cf6e973 100644 --- a/minigent/src/Minigent/Termination.hs +++ b/minigent/src/Minigent/Termination.hs @@ -27,8 +27,10 @@ import qualified Data.Set as S type Node = String type Graph = M.Map Node [Node] --- Our environment -type Env a = FreshT VarName (State (M.Map VarName VarName)) a + + +-- Our environment, a mapping between program variables and fresh variables +type Env = M.Map VarName VarName infixr 0 :<: data Assertion = @@ -40,79 +42,75 @@ data Assertion = termCheck :: GlobalEnvironments -> [String] termCheck = undefined -termAssertionGen :: Expr -> Env ([Assertion], [VarName]) -termAssertionGen expr +termAssertionGen :: Env -> Expr -> Fresh VarName ([Assertion], [VarName]) +termAssertionGen env expr = case expr of PrimOp _ es -> - join $ map termAssertionGen es + join $ map (termAssertionGen env) es Sig e _ -> - termAssertionGen e + termAssertionGen env e Apply f e -> do - a <- termAssertionGen f - b <- termAssertionGen e - c <- getv e - return $ flatten [([],maybeToList c), a, b] + a <- termAssertionGen env f + b <- termAssertionGen env e + let c = getv env e + return $ flatten [([], maybeToList c), a, b] Struct fs -> let es = map snd fs - in join $ map termAssertionGen es + in join $ map (termAssertionGen env) es If b e1 e2 -> - join $ map termAssertionGen [b, e1, e2] + join $ map (termAssertionGen env) [b, e1, e2] Let x e1 e2 -> do -- First evaluate the variable binding expression - a <- termAssertionGen e1 + a <- termAssertionGen env e1 - -- Preserve the old state - env <- lift $ get let old = M.lookup x env - -- Map our bound program variable to a new name - fvar <- insert x - - -- Evaluate the rest - res <- termAssertionGen e2 + -- Map our bound program variable to a new name and evaluate the rest + alpha <- fresh + let env' = M.insert x alpha env + res <- termAssertionGen env' e2 - -- Roll back the state for the program variable - undo x old - - -- calculate the assertion for the old variable - env <- lift $ get - mv <- getv e1 - let l = (case mv of - Just x' -> [fvar :~: (env M.! x')] + -- Generate assertion + let l = (case getv env e1 of + Just x' -> [alpha :~: (env M.! x')] Nothing -> []) - return $ flatten [(l,[]), res] + + LetBang vs v e1 e2 -> + termAssertionGen env (Let v e1 e2) -- TODO - Correct? + Take r' f x e1 e2 -> do + alpha <- fresh + beta <- fresh + + res <- termAssertionGen env e1 + + -- Update variable to fresh name bindings + let env' = M.insert r' beta (M.insert x alpha env) + res' <- termAssertionGen env' e2 + + -- generate assertions + let res'' = (case getv env e1 of + Just x' -> [alpha :<: (env M.! x')] + Nothing -> []) + ++ + (case getv env e2 of + Just x' -> [beta :~: (env M.! x')] + Nothing -> []) + + return $ flatten [(res'', []), res', res] _ -> return ([],[]) where -- Returns the variable name from an environment if it exists, otherwise nothing - getv :: Expr -> Env (Maybe VarName) - getv e = do - env <- lift $ get - return $ - case e of - Var v -> Just $ env M.! v - _ -> Nothing - - -- Updates an environment binding - insert :: VarName -> Env VarName - insert v = do - e <- lift $ get - n <- fresh - lift $ put (M.insert v n e) - return n - - undo :: VarName -> Maybe VarName -> Env () - undo x m = do - env <- lift $ get - lift $ put (M.delete x env) - case m of - Just v -> lift $ put (M.insert x v env) - _ -> return () - - join :: [Env ([Assertion], [VarName])] -> Env ([Assertion], [VarName]) + getv :: Env -> Expr -> Maybe VarName + getv env e = + case e of + Var v -> Just $ env M.! v + _ -> Nothing + + join :: [Fresh VarName ([Assertion], [VarName])] -> Fresh VarName ([Assertion], [VarName]) join (e:es) = do (a,b) <- e (as,bs) <- join es @@ -124,9 +122,6 @@ termAssertionGen expr let rest = flatten xs in (fst x ++ fst rest, snd x ++ snd rest) flatten [] = ([],[]) - - add :: [Maybe Assertion] -> [VarName] -> ([Maybe Assertion], [VarName]) -> ([Maybe Assertion], [VarName]) - add a g t = (a ++ fst t, g ++ snd t) hasPathTo :: Node -> Node -> Graph -> Bool hasPathTo src dst g From 8b6b002ff1627b67bb9b2b49537878d186a22a76 Mon Sep 17 00:00:00 2001 From: Emmet Murray Date: Thu, 12 Dec 2019 14:16:17 +1100 Subject: [PATCH 3/7] Added termination checking to minigent, working on integrating with recursive types --- minigent/src/Minigent/CLI.hs | 15 ++-- minigent/src/Minigent/Termination.hs | 126 ++++++++++++++++++++++----- 2 files changed, 112 insertions(+), 29 deletions(-) diff --git a/minigent/src/Minigent/CLI.hs b/minigent/src/Minigent/CLI.hs index 91d0d6b4b..eaf52d9eb 100644 --- a/minigent/src/Minigent/CLI.hs +++ b/minigent/src/Minigent/CLI.hs @@ -61,7 +61,7 @@ data Output = File FilePath | Stdout deriving (Eq) -- | The various command line arguments of the compiler. -data Directive +data Directive = Dump Phase Output Format | NoColour deriving (Eq) @@ -108,7 +108,7 @@ parseDirectives ("--dump-stdout":rest) = do pure (Dump phase Stdout format: dirs, files) parseDirectives ("--no-colour":rest) = do (dirs, files) <- parseDirectives rest - pure (NoColour:dirs, files) + pure (NoColour:dirs, files) parseDirectives ("--dump":rest) = do (rest', phase) <- singleToken parsePhase rest (rest'', format) <- singleToken parseFormat rest' <|> pure (rest', PrettyPlain) @@ -187,7 +187,7 @@ reorgPhase x = die ("Reorg failed.\n" ++ unlines errs ++ "\n\n") tcPhase :: Bool -> GlobalEnvironments -> IO GlobalEnvironments -tcPhase colour envs +tcPhase colour envs = let rs = withUnifVars (tc envs (M.toList (defns envs))) in GlobalEnvs <$> (M.fromList . concat <$> mapM go rs) <*> pure (types envs) @@ -201,12 +201,11 @@ tcPhase colour envs go (Right b) = pure [b] terminationPhase :: GlobalEnvironments -> IO () -terminationPhase envs +terminationPhase envs = case termCheck envs of - [] -> do return () - xs -> do -- Error + [] -> return () + xs -> -- Error mapM_ (hPutStrLn stderr) xs - return () cgPhase :: GlobalEnvironments -> IO String @@ -288,7 +287,7 @@ cgDump s (Dump CG out fmt) = write out s write (File f) = writeFile f write (Stdout) = putStrLn cgDump _ _ = mempty - + -- | Compile the given files up to the given phase, dumping -- output according to the given directives. diff --git a/minigent/src/Minigent/Termination.hs b/minigent/src/Minigent/Termination.hs index 79cf6e973..09cf4c43f 100644 --- a/minigent/src/Minigent/Termination.hs +++ b/minigent/src/Minigent/Termination.hs @@ -27,10 +27,9 @@ import qualified Data.Set as S type Node = String type Graph = M.Map Node [Node] - - -- Our environment, a mapping between program variables and fresh variables -type Env = M.Map VarName VarName +type FreshVar = String +type Env = M.Map VarName FreshVar infixr 0 :<: data Assertion = @@ -40,25 +39,51 @@ data Assertion = termCheck :: GlobalEnvironments -> [String] -termCheck = undefined +termCheck genvs = M.foldrWithKey go [] (defns genvs) + where + go :: FunName -> (VarName, Expr) -> [String] -> [String] + go f (x,e) errs = + if fst $ runFresh unifVars (init x e) then + errs + else + ("Error: Function " ++ f ++ " cannot be shown to terminate.") : errs + + -- Maps the function argument to a name, then runs the termination + -- assertion generator. + -- Return true if the function terminates + init :: VarName -> Expr -> Fresh VarName Bool + init x e = do + alpha <- fresh + let env = M.insert x alpha M.empty + (a,c) <- termAssertionGen env e + let graph = toGraph a + return $ + all (\goal -> hasPathTo alpha goal graph && (not $ hasPathTo goal alpha graph)) c + + termAssertionGen :: Env -> Expr -> Fresh VarName ([Assertion], [VarName]) termAssertionGen env expr = case expr of PrimOp _ es -> join $ map (termAssertionGen env) es + Sig e _ -> termAssertionGen env e + Apply f e -> do a <- termAssertionGen env f b <- termAssertionGen env e let c = getv env e return $ flatten [([], maybeToList c), a, b] + Struct fs -> let es = map snd fs in join $ map (termAssertionGen env) es + If b e1 e2 -> join $ map (termAssertionGen env) [b, e1, e2] + Let x e1 e2 -> do -- First evaluate the variable binding expression a <- termAssertionGen env e1 @@ -71,58 +96,118 @@ termAssertionGen env expr res <- termAssertionGen env' e2 -- Generate assertion - let l = (case getv env e1 of - Just x' -> [alpha :~: (env M.! x')] - Nothing -> []) + let l = toAssertion env e1 (alpha :~:) return $ flatten [(l,[]), res] LetBang vs v e1 e2 -> termAssertionGen env (Let v e1 e2) -- TODO - Correct? + Take r' f x e1 e2 -> do alpha <- fresh beta <- fresh res <- termAssertionGen env e1 - -- Update variable to fresh name bindings + -- Update variable to fresh name bindings and generate assertions recursively let env' = M.insert r' beta (M.insert x alpha env) res' <- termAssertionGen env' e2 -- generate assertions - let res'' = (case getv env e1 of - Just x' -> [alpha :<: (env M.! x')] - Nothing -> []) - ++ - (case getv env e2 of - Just x' -> [beta :~: (env M.! x')] - Nothing -> []) + let assertions = toAssertion env e1 (alpha :<:) + ++ toAssertion env e2 (beta :~:) + + return $ flatten [(assertions, []), res', res] + + Put e1 f e2 -> do + alpha <- fresh + beta <- fresh + + res <- termAssertionGen env e1 + res' <- termAssertionGen env e2 + + let assertions = [alpha :<: beta] + ++ toAssertion env e1 (beta :~:) + ++ toAssertion env e2 (alpha :~:) + + return $ flatten [(assertions, []), res', res] + + Member e f -> + termAssertionGen env e + + Case e1 _ x e2 y e3 -> do + alpha <- fresh + beta <- fresh + gamma <- fresh + + res <- termAssertionGen env e1 + + let env' = M.insert x alpha env + res' <- termAssertionGen env' e2 + + let env'' = M.insert y gamma env + res'' <- termAssertionGen env'' e3 + + let assertions = toAssertion env e1 (beta :~:) + ++ [alpha :<: beta, gamma :~: beta] + + return $ flatten [(assertions, []), res, res', res''] + + Esac e1 _ x e2 -> do + alpha <- fresh + beta <- fresh + + res <- termAssertionGen env e1 + + let env' = M.insert x alpha env + res' <- termAssertionGen env' e2 + + let assertions = toAssertion env e1 (beta :~:) + ++ [alpha :<: beta] - return $ flatten [(res'', []), res', res] + return $ flatten [(assertions, []), res, res'] + -- All other cases, like literals and nonrecursive expressions _ -> return ([],[]) where + + toAssertion :: Env -> Expr -> (FreshVar -> Assertion) -> [Assertion] + toAssertion env e f = + case getv env e of + Just x -> [f x] + Nothing -> [] -- Returns the variable name from an environment if it exists, otherwise nothing - getv :: Env -> Expr -> Maybe VarName + getv :: Env -> Expr -> Maybe FreshVar getv env e = case e of Var v -> Just $ env M.! v _ -> Nothing - join :: [Fresh VarName ([Assertion], [VarName])] -> Fresh VarName ([Assertion], [VarName]) + join :: [Fresh VarName ([Assertion], [FreshVar])] -> Fresh VarName ([Assertion], [FreshVar]) join (e:es) = do (a,b) <- e (as,bs) <- join es return (a ++ as, b ++ bs) join [] = return ([],[]) - flatten :: [([Assertion], [VarName])] -> ([Assertion], [VarName]) + flatten :: [([Assertion], [FreshVar])] -> ([Assertion], [FreshVar]) flatten (x:xs) = let rest = flatten xs in (fst x ++ fst rest, snd x ++ snd rest) flatten [] = ([],[]) +toGraph :: [Assertion] -> Graph +toGraph [] = mempty +toGraph (x:xs) = + case x of + (a :<: b) -> addEdge b a $ toGraph xs + (a :~: b) -> addEdge a b $ addEdge b a $ toGraph xs + where + addEdge a b = + M.insertWith (++) a [b] + + hasPathTo :: Node -> Node -> Graph -> Bool hasPathTo src dst g = hasPathTo' src dst g S.empty @@ -136,5 +221,4 @@ hasPathTo src dst g n == dst || (notElem n seen && hasPathTo' n d g (S.insert n seen)) - ) nbs - + ) nbs \ No newline at end of file From 7b67edc119756bf1dd7df98a9309af17d1cbebd2 Mon Sep 17 00:00:00 2001 From: Emmet Murray Date: Thu, 12 Dec 2019 14:19:58 +1100 Subject: [PATCH 4/7] Recursive Types (minigent) (#327) Merging in recursive types from @emmet-m 's thesis fork --- minigent/.gitignore | 3 +- .../3_records/04-double-take/expected.err | 4 +- .../6_recursive/01-basic/expected.err | 0 .../6_recursive/01-basic/expected.out | 13 + .../examples/6_recursive/01-basic/in.minigent | 7 + .../examples/6_recursive/02-poly/expected.err | 0 .../examples/6_recursive/02-poly/expected.out | 18 ++ .../examples/6_recursive/02-poly/in.minigent | 9 + .../03-non-strictly-positive/expected.err | 2 + .../03-non-strictly-positive/expected.out | 0 .../03-non-strictly-positive/in.minigent | 2 + .../expected.err | 2 + .../expected.out | 0 .../in.minigent | 12 + .../05-strictly-positive-allowed/expected.err | 0 .../05-strictly-positive-allowed/expected.out | 3 + .../05-strictly-positive-allowed/in.minigent | 2 + .../6_recursive/06-list-push/expected.err | 0 .../6_recursive/06-list-push/expected.out | 32 ++ .../6_recursive/06-list-push/in.minigent | 12 + .../6_recursive/07-self-calling/expected.err | 0 .../6_recursive/07-self-calling/expected.out | 12 + .../6_recursive/07-self-calling/in.minigent | 9 + .../6_recursive/08-list-sum/expected.err | 0 .../6_recursive/08-list-sum/expected.out | 20 ++ .../6_recursive/08-list-sum/in.minigent | 10 + .../examples/6_recursive/09-map/expected.err | 0 .../examples/6_recursive/09-map/expected.out | 86 ++++++ .../examples/6_recursive/09-map/in.minigent | 29 ++ .../10-bang-incompatible/expected.err | 2 + .../10-bang-incompatible/expected.out | 1 + .../10-bang-incompatible/in.minigent | 3 + .../11-incompatible-recpars/expected.err | 7 + .../11-incompatible-recpars/expected.out | 6 + .../11-incompatible-recpars/in.minigent | 25 ++ minigent/src/Minigent/CG.hs | 2 +- minigent/src/Minigent/CLI.hs | 2 +- minigent/src/Minigent/Reorganiser.hs | 49 ++- minigent/src/Minigent/Syntax.hs | 25 +- minigent/src/Minigent/Syntax/Lexer.hs | 3 +- minigent/src/Minigent/Syntax/Parser.hs | 11 +- minigent/src/Minigent/Syntax/PrettyPrint.hs | 114 ++++--- minigent/src/Minigent/Syntax/Utils.hs | 291 +++++++++++------- minigent/src/Minigent/TC.hs | 2 + minigent/src/Minigent/TC/Assign.hs | 4 + minigent/src/Minigent/TC/ConstraintGen.hs | 45 ++- minigent/src/Minigent/TC/Equate.hs | 13 +- minigent/src/Minigent/TC/JoinMeet.hs | 33 +- minigent/src/Minigent/TC/Normalise.hs | 24 +- minigent/src/Minigent/TC/Simplify.hs | 73 ++++- minigent/src/Minigent/TC/SinkFloat.hs | 12 +- minigent/src/Minigent/TC/Unify.hs | 44 ++- minigent/test/Example.hs | 4 +- 53 files changed, 848 insertions(+), 234 deletions(-) create mode 100644 minigent/examples/6_recursive/01-basic/expected.err create mode 100644 minigent/examples/6_recursive/01-basic/expected.out create mode 100644 minigent/examples/6_recursive/01-basic/in.minigent create mode 100644 minigent/examples/6_recursive/02-poly/expected.err create mode 100644 minigent/examples/6_recursive/02-poly/expected.out create mode 100644 minigent/examples/6_recursive/02-poly/in.minigent create mode 100644 minigent/examples/6_recursive/03-non-strictly-positive/expected.err create mode 100644 minigent/examples/6_recursive/03-non-strictly-positive/expected.out create mode 100644 minigent/examples/6_recursive/03-non-strictly-positive/in.minigent create mode 100644 minigent/examples/6_recursive/04-harder-non-strictly-positive/expected.err create mode 100644 minigent/examples/6_recursive/04-harder-non-strictly-positive/expected.out create mode 100644 minigent/examples/6_recursive/04-harder-non-strictly-positive/in.minigent create mode 100644 minigent/examples/6_recursive/05-strictly-positive-allowed/expected.err create mode 100644 minigent/examples/6_recursive/05-strictly-positive-allowed/expected.out create mode 100644 minigent/examples/6_recursive/05-strictly-positive-allowed/in.minigent create mode 100644 minigent/examples/6_recursive/06-list-push/expected.err create mode 100644 minigent/examples/6_recursive/06-list-push/expected.out create mode 100644 minigent/examples/6_recursive/06-list-push/in.minigent create mode 100644 minigent/examples/6_recursive/07-self-calling/expected.err create mode 100644 minigent/examples/6_recursive/07-self-calling/expected.out create mode 100644 minigent/examples/6_recursive/07-self-calling/in.minigent create mode 100644 minigent/examples/6_recursive/08-list-sum/expected.err create mode 100644 minigent/examples/6_recursive/08-list-sum/expected.out create mode 100644 minigent/examples/6_recursive/08-list-sum/in.minigent create mode 100644 minigent/examples/6_recursive/09-map/expected.err create mode 100644 minigent/examples/6_recursive/09-map/expected.out create mode 100644 minigent/examples/6_recursive/09-map/in.minigent create mode 100644 minigent/examples/6_recursive/10-bang-incompatible/expected.err create mode 100644 minigent/examples/6_recursive/10-bang-incompatible/expected.out create mode 100644 minigent/examples/6_recursive/10-bang-incompatible/in.minigent create mode 100644 minigent/examples/6_recursive/11-incompatible-recpars/expected.err create mode 100644 minigent/examples/6_recursive/11-incompatible-recpars/expected.out create mode 100644 minigent/examples/6_recursive/11-incompatible-recpars/in.minigent diff --git a/minigent/.gitignore b/minigent/.gitignore index 7fb45696b..284f07445 100644 --- a/minigent/.gitignore +++ b/minigent/.gitignore @@ -1,3 +1,4 @@ .stack-work/ minigent.cabal -*~ \ No newline at end of file +stack.yaml.lock +*~ diff --git a/minigent/examples/3_records/04-double-take/expected.err b/minigent/examples/3_records/04-double-take/expected.err index 1dae50ece..bee42f763 100644 --- a/minigent/examples/3_records/04-double-take/expected.err +++ b/minigent/examples/3_records/04-double-take/expected.err @@ -1,3 +1,3 @@ Typecheck failed in function foo - • {x : Foo take}# :< {x : Foo,𝛈...}# - • Drop {x : Foo take,𝛈...}# \ No newline at end of file + • {x : Foo take}# :< {x : Foo,𝛉...}# + • Drop {x : Foo take,𝛉...}# \ No newline at end of file diff --git a/minigent/examples/6_recursive/01-basic/expected.err b/minigent/examples/6_recursive/01-basic/expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/minigent/examples/6_recursive/01-basic/expected.out b/minigent/examples/6_recursive/01-basic/expected.out new file mode 100644 index 000000000..cd95aa803 --- /dev/null +++ b/minigent/examples/6_recursive/01-basic/expected.out @@ -0,0 +1,13 @@ +alloc : Unit -> mu t {l : take}; +makeEmptyList : Unit -> mu t {l : }; +makeEmptyList a = let r = (alloc[] : Unit + -> mu t {l : take}) (Unit : Unit) : mu t {l : take} + in put r : mu t {l : take}.l := End (Unit : Unit) : + end : mu t {l : } + end : mu t {l : }; \ No newline at end of file diff --git a/minigent/examples/6_recursive/01-basic/in.minigent b/minigent/examples/6_recursive/01-basic/in.minigent new file mode 100644 index 000000000..317289b54 --- /dev/null +++ b/minigent/examples/6_recursive/01-basic/in.minigent @@ -0,0 +1,7 @@ +alloc : Unit -> mu t { l : < End Unit | Cons { d : U8, r : t }# > take }; + +makeEmptyList : Unit -> mu t { l : < End Unit | Cons { d : U8, r : t }# > }; +makeEmptyList a = + let r = alloc Unit in + put r.l := End Unit end + end; diff --git a/minigent/examples/6_recursive/02-poly/expected.err b/minigent/examples/6_recursive/02-poly/expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/minigent/examples/6_recursive/02-poly/expected.out b/minigent/examples/6_recursive/02-poly/expected.out new file mode 100644 index 000000000..172c8bb54 --- /dev/null +++ b/minigent/examples/6_recursive/02-poly/expected.out @@ -0,0 +1,18 @@ +allocNode : [a] + . + Unit -> mu t {l : take}; +createEmptyList : [a] + . + U8 -> mu t {l : }; +createEmptyList a = let node = (allocNode[a] : Unit + -> mu t {l : take}) (Unit : Unit) : mu t {l : take} + in put node : mu t {l : take}.l := Nil (Unit : Unit) : + end : mu t {l : } + end : mu t {l : }; \ No newline at end of file diff --git a/minigent/examples/6_recursive/02-poly/in.minigent b/minigent/examples/6_recursive/02-poly/in.minigent new file mode 100644 index 000000000..b6ec01de6 --- /dev/null +++ b/minigent/examples/6_recursive/02-poly/in.minigent @@ -0,0 +1,9 @@ +allocNode : [a]. Unit -> mu t { l: < Nil Unit | Cons { data: a, rest: t }# > take }; + +createEmptyList : [a]. U8 -> mu t { l : < Nil Unit | Cons { data : a, rest : t }# >}; +createEmptyList a = + let node = allocNode Unit in + put node.l := Nil Unit end + end; + + diff --git a/minigent/examples/6_recursive/03-non-strictly-positive/expected.err b/minigent/examples/6_recursive/03-non-strictly-positive/expected.err new file mode 100644 index 000000000..a04abdbfc --- /dev/null +++ b/minigent/examples/6_recursive/03-non-strictly-positive/expected.err @@ -0,0 +1,2 @@ +Reorg failed. +Variables occuring non-strictly positive: t \ No newline at end of file diff --git a/minigent/examples/6_recursive/03-non-strictly-positive/expected.out b/minigent/examples/6_recursive/03-non-strictly-positive/expected.out new file mode 100644 index 000000000..e69de29bb diff --git a/minigent/examples/6_recursive/03-non-strictly-positive/in.minigent b/minigent/examples/6_recursive/03-non-strictly-positive/in.minigent new file mode 100644 index 000000000..545a18e9a --- /dev/null +++ b/minigent/examples/6_recursive/03-non-strictly-positive/in.minigent @@ -0,0 +1,2 @@ +listop : Unit -> mu t { f : (t -> U8) }; +listop a = { f = End Unit }; diff --git a/minigent/examples/6_recursive/04-harder-non-strictly-positive/expected.err b/minigent/examples/6_recursive/04-harder-non-strictly-positive/expected.err new file mode 100644 index 000000000..a04abdbfc --- /dev/null +++ b/minigent/examples/6_recursive/04-harder-non-strictly-positive/expected.err @@ -0,0 +1,2 @@ +Reorg failed. +Variables occuring non-strictly positive: t \ No newline at end of file diff --git a/minigent/examples/6_recursive/04-harder-non-strictly-positive/expected.out b/minigent/examples/6_recursive/04-harder-non-strictly-positive/expected.out new file mode 100644 index 000000000..e69de29bb diff --git a/minigent/examples/6_recursive/04-harder-non-strictly-positive/in.minigent b/minigent/examples/6_recursive/04-harder-non-strictly-positive/in.minigent new file mode 100644 index 000000000..46cd888c8 --- /dev/null +++ b/minigent/examples/6_recursive/04-harder-non-strictly-positive/in.minigent @@ -0,0 +1,12 @@ +listop : Unit -> + mu t { + f : < Left U8 + | Midde Unit + | Right { + a : U64, + b: (((U8 -> t) -> U8) -> Unit) + } + > + }; + +listop a = { f = Middle Unit }; \ No newline at end of file diff --git a/minigent/examples/6_recursive/05-strictly-positive-allowed/expected.err b/minigent/examples/6_recursive/05-strictly-positive-allowed/expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/minigent/examples/6_recursive/05-strictly-positive-allowed/expected.out b/minigent/examples/6_recursive/05-strictly-positive-allowed/expected.out new file mode 100644 index 000000000..71975d07e --- /dev/null +++ b/minigent/examples/6_recursive/05-strictly-positive-allowed/expected.out @@ -0,0 +1,3 @@ +id : mu t {l : } + -> mu t {l : }; +id a = a : mu t {l : }; \ No newline at end of file diff --git a/minigent/examples/6_recursive/05-strictly-positive-allowed/in.minigent b/minigent/examples/6_recursive/05-strictly-positive-allowed/in.minigent new file mode 100644 index 000000000..5c3072133 --- /dev/null +++ b/minigent/examples/6_recursive/05-strictly-positive-allowed/in.minigent @@ -0,0 +1,2 @@ +id : mu t { l : < End Unit | Rest { a : U8, b : t } > } -> mu t { l : < End Unit | Rest { a : U8, b : t } > }; +id a = a; diff --git a/minigent/examples/6_recursive/06-list-push/expected.err b/minigent/examples/6_recursive/06-list-push/expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/minigent/examples/6_recursive/06-list-push/expected.out b/minigent/examples/6_recursive/06-list-push/expected.out new file mode 100644 index 000000000..28ea02aee --- /dev/null +++ b/minigent/examples/6_recursive/06-list-push/expected.out @@ -0,0 +1,32 @@ +allocNode : [a] + . + Unit -> mu t {l : take}; +push : [a] + . + {data : a,list : mu t {l : }}# + -> mu t {l : }; +push r = let node = (allocNode[a] : Unit + -> mu t {l : take}) (Unit : Unit) : mu t {l : take} + in take r2 { data = x } = r : {data : a + ,list : mu t {l : }}# + in take r3 { list = y } = r2 : {data : a take + ,list : mu t {l : }}# + in put node : mu t {l : take}.l := Cons ({data = x : a + ,rest = y : mu t {l : }} : {data : a + ,rest : rec t}#) : + end : mu t {l : } + end : mu t {l : } + end : mu t {l : } + end : mu t {l : }; \ No newline at end of file diff --git a/minigent/examples/6_recursive/06-list-push/in.minigent b/minigent/examples/6_recursive/06-list-push/in.minigent new file mode 100644 index 000000000..ba2782fed --- /dev/null +++ b/minigent/examples/6_recursive/06-list-push/in.minigent @@ -0,0 +1,12 @@ +allocNode : [a]. Unit -> mu t { l: < Nil Unit | Cons { data: a, rest: t }# > take }; + +push : [a]. { data: a, list: mu t { l: < Nil Unit | Cons { data: a, rest: t }# > } }# + -> mu t { l: < Nil Unit | Cons { data: a, rest: t }# >}; +push r = + let node = allocNode Unit in + take r2 { data = x } = r in + take r3 { list = y } = r2 in + put node.l := Cons { data = x, rest = y } end + end + end + end; \ No newline at end of file diff --git a/minigent/examples/6_recursive/07-self-calling/expected.err b/minigent/examples/6_recursive/07-self-calling/expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/minigent/examples/6_recursive/07-self-calling/expected.out b/minigent/examples/6_recursive/07-self-calling/expected.out new file mode 100644 index 000000000..71b43239a --- /dev/null +++ b/minigent/examples/6_recursive/07-self-calling/expected.out @@ -0,0 +1,12 @@ +add : {x : U8,y : U8}# -> U8; +add r = take r2 { x = a } = r : {x : U8,y : U8}# + in take r3 { y = b } = r2 : {x : U8 take,y : U8}# + in if (a : U8) == (0 : U8) : Bool + then b : U8 + else (add[] : {x : U8,y : U8}# + -> U8) ({x = (a : U8) - (1 : U8) : U8 + ,y = (b : U8) + (1 : U8) : U8} : {x : U8 + ,y : U8}#) : U8 + end : U8 + end : U8 + end : U8; \ No newline at end of file diff --git a/minigent/examples/6_recursive/07-self-calling/in.minigent b/minigent/examples/6_recursive/07-self-calling/in.minigent new file mode 100644 index 000000000..ce6e8f7d6 --- /dev/null +++ b/minigent/examples/6_recursive/07-self-calling/in.minigent @@ -0,0 +1,9 @@ +add : { x: U8, y: U8 }# -> U8; +add r = + take r2 { x = a } = r in + take r3 { y = b } = r2 in + if a == 0 then b + else add { x = a-1, y = b+1 } + end + end + end; \ No newline at end of file diff --git a/minigent/examples/6_recursive/08-list-sum/expected.err b/minigent/examples/6_recursive/08-list-sum/expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/minigent/examples/6_recursive/08-list-sum/expected.out b/minigent/examples/6_recursive/08-list-sum/expected.out new file mode 100644 index 000000000..990385ace --- /dev/null +++ b/minigent/examples/6_recursive/08-list-sum/expected.out @@ -0,0 +1,20 @@ +sumList : mu t {l : }! -> U32; +sumList r = case (r : mu t {l : }!).l : of + Nil u -> 0 : U32 + | v2 -> case v2 : of + Cons s -> ((s : {data : U32 + ,rest : rec t!}#).data : U32) + ((sumList[ ] : mu t {l : }! + -> U32) ((s : {data : U32 + ,rest : mu t {l : }!}#).rest : mu t {l : }!) : U32) : U32 + end : U32 + end : U32; \ No newline at end of file diff --git a/minigent/examples/6_recursive/08-list-sum/in.minigent b/minigent/examples/6_recursive/08-list-sum/in.minigent new file mode 100644 index 000000000..f55d213b5 --- /dev/null +++ b/minigent/examples/6_recursive/08-list-sum/in.minigent @@ -0,0 +1,10 @@ +sumList : mu t { l: < Nil Unit | Cons { data: U32, rest: t! }# >}! -> U32; +sumList r = + case r.l of + Nil u -> 0 + | v2 -> + case v2 of + Cons s -> + s.data + sumList s.rest + end + end; \ No newline at end of file diff --git a/minigent/examples/6_recursive/09-map/expected.err b/minigent/examples/6_recursive/09-map/expected.err new file mode 100644 index 000000000..e69de29bb diff --git a/minigent/examples/6_recursive/09-map/expected.out b/minigent/examples/6_recursive/09-map/expected.out new file mode 100644 index 000000000..2e7ce888e --- /dev/null +++ b/minigent/examples/6_recursive/09-map/expected.out @@ -0,0 +1,86 @@ +alloc : [x] . Unit -> mu t {l : take}; +map : [a, b] + . + {f : a -> b,list : mu t {l : }!}# + -> mu t {l : }; +map l = take l2 { list = node } = l : {f : a -> b + ,list : mu t {l : }!}# + in take l3 { f = fun } = l2 : {f : a -> b + ,list : mu t {l : }! take}# + in take node2 { l = head } = node : mu t {l : }! + in case head : of + Nil u -> let newNode = (alloc[b] : Unit + -> mu t {l : take}) (Unit : Unit) : mu t {l : take} + in put newNode : mu t {l : take}.l := Nil (Unit : Unit) : + end : mu t {l : } + end : mu t {l : } + | v2 -> case v2 : of + Cons remaining -> take remaining2 { data = x } = remaining : {data : a + ,rest : rec t}# + in let newNode = (alloc[b] : Unit + -> mu t {l : take}) (Unit : Unit) : mu t {l : take} + in put newNode : mu t {l : take}.l := Cons ({data = (fun : a + -> b) (x : a) : b + ,rest = (map[ a + , b ] : {f : a + -> b + ,list : mu t {l : }!}# + -> mu t {l : }) ({list = (remaining2 : {data : a take + ,rest : mu t {l : }!}#).rest : mu t {l : }! + ,f = fun : a + -> b} : {f : a + -> b + ,list : mu t {l : }!}#) : mu t {l : }} : {data : b + ,rest : rec t}#) : + end : mu t {l : } + end : mu t {l : } + end : mu t {l : } + end : mu t {l : } + end : mu t {l : } + end : mu t {l : } + end : mu t {l : } + end : mu t {l : }; \ No newline at end of file diff --git a/minigent/examples/6_recursive/09-map/in.minigent b/minigent/examples/6_recursive/09-map/in.minigent new file mode 100644 index 000000000..f03e71c1e --- /dev/null +++ b/minigent/examples/6_recursive/09-map/in.minigent @@ -0,0 +1,29 @@ +alloc : [x]. Unit -> mu t { l: < Nil Unit | Cons { data: x, rest: t }# > take }; + +map : [a,b]. { list: mu t { l: < Nil Unit | Cons { data: a, rest: t }# > }!, f: (a -> b) }# + -> mu t { l: < Nil Unit | Cons { data: b, rest: t }# >}; +map l = + take l2 { list = node } = l in + take l3 { f = fun } = l2 in + take node2 { l = head } = node in + case head of + Nil u -> + let newNode = alloc Unit in + put newNode.l := Nil Unit end + end + | v2 -> case v2 of + Cons remaining -> + take remaining2 { data = x } = remaining in + let newNode = alloc Unit in + put newNode.l := + Cons { + data = fun x, + rest = map { list = remaining2.rest, f = fun } + } end + end + end + end + end + end + end + end; \ No newline at end of file diff --git a/minigent/examples/6_recursive/10-bang-incompatible/expected.err b/minigent/examples/6_recursive/10-bang-incompatible/expected.err new file mode 100644 index 000000000..6d114eaa0 --- /dev/null +++ b/minigent/examples/6_recursive/10-bang-incompatible/expected.err @@ -0,0 +1,2 @@ +Typecheck failed in function bad + • rec k! :< rec k \ No newline at end of file diff --git a/minigent/examples/6_recursive/10-bang-incompatible/expected.out b/minigent/examples/6_recursive/10-bang-incompatible/expected.out new file mode 100644 index 000000000..a5fee5cb2 --- /dev/null +++ b/minigent/examples/6_recursive/10-bang-incompatible/expected.out @@ -0,0 +1 @@ +bad : mu k {f : } -> mu k {f : }; \ No newline at end of file diff --git a/minigent/examples/6_recursive/10-bang-incompatible/in.minigent b/minigent/examples/6_recursive/10-bang-incompatible/in.minigent new file mode 100644 index 000000000..b1bf13255 --- /dev/null +++ b/minigent/examples/6_recursive/10-bang-incompatible/in.minigent @@ -0,0 +1,3 @@ +bad: mu k { f: < Some U8 | Chain k! > } + -> mu k { f: < Some U8 | Chain k > }; +bad x = x; \ No newline at end of file diff --git a/minigent/examples/6_recursive/11-incompatible-recpars/expected.err b/minigent/examples/6_recursive/11-incompatible-recpars/expected.err new file mode 100644 index 000000000..77c794cef --- /dev/null +++ b/minigent/examples/6_recursive/11-incompatible-recpars/expected.err @@ -0,0 +1,7 @@ +Typecheck failed in function incompatible + • mu t {f : } :< mu t {l : } \ No newline at end of file diff --git a/minigent/examples/6_recursive/11-incompatible-recpars/expected.out b/minigent/examples/6_recursive/11-incompatible-recpars/expected.out new file mode 100644 index 000000000..b89d55c65 --- /dev/null +++ b/minigent/examples/6_recursive/11-incompatible-recpars/expected.out @@ -0,0 +1,6 @@ +deallocList : mu t {l : } -> Unit; +genTree : Unit + -> mu t {f : }; +incompatible : mu t {l : } + -> mu t {l : }; \ No newline at end of file diff --git a/minigent/examples/6_recursive/11-incompatible-recpars/in.minigent b/minigent/examples/6_recursive/11-incompatible-recpars/in.minigent new file mode 100644 index 000000000..da0e6c20d --- /dev/null +++ b/minigent/examples/6_recursive/11-incompatible-recpars/in.minigent @@ -0,0 +1,25 @@ +genTree : Unit -> mu t { f: < Leaf Unit | Node { left: t, right: t, data: U64 }# > }; + +deallocList: mu t { l: < Nil Unit | Cons { data: U64, rest: t }# > } -> Unit; + +incompatible : mu t { l: < Nil Unit | Cons { data: U64, rest: t }# > } + -> mu t { l: < Nil Unit | Cons { data: U64, rest: t }# > }; +incompatible list = + take emptyList { l = node } = list in + case node of + Nil u -> put emptyList.l := Nil u end + | node2 -> + case node2 of + Cons r -> + take r2 { rest = restOfList } = r in + let drop = deallocList restOfList in + put emptyList.l := + Cons { + data = 0, + rest = genTree Unit + } end + end + end + end + end + end; \ No newline at end of file diff --git a/minigent/src/Minigent/CG.hs b/minigent/src/Minigent/CG.hs index 32a94512b..fe429fa8f 100644 --- a/minigent/src/Minigent/CG.hs +++ b/minigent/src/Minigent/CG.hs @@ -55,7 +55,7 @@ cg envs = let ds = M.toList (defns envs) genExpr (Take v f vf e1 e2) = format "C.Let($3, $0=> C.Let(($3).$1, $2=> $4))" [v,f,vf,genExpr e1, genExpr e2] genExpr (Put e1 f e2) = case e1 of - Sig e1' (Record _ Unboxed) + Sig e1' (Record _ _ Unboxed) -> format "C.UPut($0,{$1:$2})" [genExpr e1', f, genExpr e2] _ -> format "Object.assign($0,{$1:$2})" [genExpr e1 , f, genExpr e2] diff --git a/minigent/src/Minigent/CLI.hs b/minigent/src/Minigent/CLI.hs index eaf52d9eb..acad857c0 100644 --- a/minigent/src/Minigent/CLI.hs +++ b/minigent/src/Minigent/CLI.hs @@ -305,7 +305,7 @@ compiler phase dirs files = do envs <- reorgPhase ast mapM_ (reorgDump envs) dirs upTo TC - binds <- tcPhase (NoColour `elem` dirs) envs + binds <- tcPhase (NoColour `notElem` dirs) envs mapM_ (tcDump binds) dirs upTo Term _ <- terminationPhase envs diff --git a/minigent/src/Minigent/Reorganiser.hs b/minigent/src/Minigent/Reorganiser.hs index 1d4518bb8..0db081647 100644 --- a/minigent/src/Minigent/Reorganiser.hs +++ b/minigent/src/Minigent/Reorganiser.hs @@ -25,19 +25,27 @@ module Minigent.Reorganiser import Minigent.Syntax import Minigent.Syntax.Utils import Minigent.Environment +import qualified Minigent.Syntax.Utils.Row as Row +import Minigent.Syntax.Utils (mapRecPars) import Control.Monad.Trans.Writer.Strict import qualified Data.Map as M +import qualified Data.Set as S import Data.List (nub, (\\), intersperse ) type Error = String sanityCheckType :: [VarName] -> Type -> Writer [Error] () sanityCheckType tvs t = do - let leftovers = nub (typeVariables t) \\ tvs - if null leftovers - then return () - else tell ["Type variables used unquantified:" ++ concat (intersperse ", " leftovers)] + -- TODO: Potentially do a single pass over the type and change all recursive parameters from TV's to + -- Recursive Parameter variables + let leftovers = nub (typeVariables t) \\ tvs + let nsp = nonStrictlyPositiveVars t + if leftovers /= [] then + tell ["Type variables used unquantified:" ++ concat (intersperse ", " leftovers)] + else if nsp /= [] then + tell ["Variables occuring non-strictly positive: " ++ concat (intersperse ", " nsp)] + else return () sanityCheckExpr :: GlobalEnvironments -> [VarName] -> [VarName] -> Expr -> Writer [Error] Expr sanityCheckExpr envs tvs vs exp = check vs exp @@ -108,7 +116,7 @@ reorganiseTopLevel (TypeSig f pt@(Forall tvs c t)) envs = do then tell ["Duplicate quantified type variable in type signature for " ++ f] else return () sanityCheckType (nub tvs) t - return (envs { types = M.insert f pt (types envs) }) + return (envs { types = M.insert f (mapRecParsPT pt) (types envs) }) reorganiseTopLevel (Equation f x e) envs = do case M.lookup f (defns envs) of @@ -121,6 +129,37 @@ reorganiseTopLevel (Equation f x e) envs = do return (envs { defns = M.insert f (x,e') (defns envs) }) +nonStrictlyPositiveVars :: Type -> [VarName] +nonStrictlyPositiveVars t = sp t M.empty + where + -- Map if variables in scope are in argument position + sp :: Type -> M.Map VarName Bool -> [VarName] + sp (PrimType _) vs = [] + sp (AbsType _ _ ts) vs = concatMap (\t -> sp t vs) ts + sp (Variant r) vs = + concatMap (\(Entry _ t _) -> sp t vs) (Row.entries r) + sp (Bang t) vs = sp t vs + + -- If we encounter a type variable, check if it occurs non-strictly positive + sp (TypeVar v) vs = concat $ M.elems $ M.mapWithKey (\t p -> if p && v == t then [v] else []) vs + sp (TypeVarBang v) vs = concat $ M.elems $ M.mapWithKey (\t p -> if p && v == t then [v] else []) vs + + -- Records are special - only here can we pick up recursive parameters + sp (Record m r _) vs = + let vs' = case m of + (Rec mt) -> M.insert mt False vs + _ -> vs + -- Shadow old recursive variables if they exist too + in concatMap (\(Entry _ t _) -> sp t vs') (Row.entries r) + + -- Only in functions can the sp check be violated + sp (Function a b) vs = + -- No recursive parameters in a non sp position + -- As we enter a function argument, we mark all existing mu vars in a non-sp position + sp a (fmap (const True) vs) ++ sp b vs + + sp _ _ = error "strictlyPositive" + reorganise :: [RawTopLevel] -> GlobalEnvironments -> Writer [Error] GlobalEnvironments reorganise [] envs = return envs reorganise (x:xs) envs = reorganise xs =<< reorganiseTopLevel x envs diff --git a/minigent/src/Minigent/Syntax.hs b/minigent/src/Minigent/Syntax.hs index b5d2fd97c..f649b6d31 100644 --- a/minigent/src/Minigent/Syntax.hs +++ b/minigent/src/Minigent/Syntax.hs @@ -21,6 +21,7 @@ module Minigent.Syntax , -- * Types Type (..) , Sigil (..) + , RecPar (..) , PrimType (..) , -- ** Entries and Rows Row (..) @@ -88,14 +89,25 @@ data Row , rowVar :: Maybe VarName -- ^ Used only in type inference. } deriving (Show, Eq) +-- | A recursive parameter type, for embedding in front of records. +-- Uses of the parameter inside the embedded record can be treated as recursively +-- referencing the record +data RecPar + = None | Rec VarName + | UnknownParameter VarName -- ^ Used only in type inference + deriving (Show, Eq) + -- | A type, which may contain unification variables or type operators. data Type = PrimType PrimType - | Record Row Sigil + | Record RecPar Row Sigil -- ^ A recursive parameter, field entry row and sigil | AbsType AbsTypeName Sigil [Type] | Variant Row | TypeVar VarName -- ^ Refers to a rigid type variable bound with a forall. | TypeVarBang VarName -- ^ A 'TypeVar' with 'Bang' applied. + -- ^ Refers to a recursive parameter, with the context of it's recursive references for Unrolling + | RecPar VarName (M.Map VarName Type) + | RecParBang VarName (M.Map VarName Type) -- ^ A 'RecPar' with 'Bang' applied. | Function Type Type -- used in type inference: | UnifVar VarName -- ^ Stands for an unknown type @@ -152,11 +164,12 @@ data Constraint | Type :=: Type -- ^ Type equality. | Integer :<=: Type -- ^ The 'fits in' relation, that says a given literal fits in the given -- type. Only satisfiable if the type is a numeric type. - | Share Type -- ^ The given type can be duplicated or shared freely - | Drop Type -- ^ The given type can go out of scope without being used - | Escape Type -- ^ The given type can be safely bound in a 'LetBang' expression - | Exhausted Type -- ^ The given type is a variant type where all entries are 'Taken'. - | Solved Type -- ^ Constraint is satisfied when the type has no unification variables. + | Share Type -- ^ The given type can be duplicated or shared freely + | Drop Type -- ^ The given type can go out of scope without being used + | Escape Type -- ^ The given type can be safely bound in a 'LetBang' expression + | Exhausted Type -- ^ The given type is a variant type where all entries are 'Taken'. + | Solved Type -- ^ Constraint is satisfied when the type has no unification variables. + | UnboxedNoRecurse Type -- ^ Satisfied when either Sigil is Unboxed, or is boxed and RecPar is None | Sat -- ^ Trivially true. | Unsat -- ^ Trivially false. deriving (Show, Eq) diff --git a/minigent/src/Minigent/Syntax/Lexer.hs b/minigent/src/Minigent/Syntax/Lexer.hs index 051cf769c..cf80806a0 100644 --- a/minigent/src/Minigent/Syntax/Lexer.hs +++ b/minigent/src/Minigent/Syntax/Lexer.hs @@ -25,7 +25,7 @@ data Bracket = Paren | Brace | Square deriving (Show, Eq) -data Keyword = Case | Of | If | Then | Else | Take | Put | Let | In | End +data Keyword = Case | Of | If | Then | Else | Take | Put | Let | In | End | Mu deriving (Show, Eq) data Token @@ -61,6 +61,7 @@ toToken "take" = Keyword Take toToken "put" = Keyword Put toToken "let" = Keyword Let toToken "in" = Keyword In +toToken "mu" = Keyword Mu toToken (x:xs) | isLower x = LowerIdent (x:xs) | otherwise = UpperIdent (x:xs) diff --git a/minigent/src/Minigent/Syntax/Parser.hs b/minigent/src/Minigent/Syntax/Parser.hs index 9da560e02..723422852 100644 --- a/minigent/src/Minigent/Syntax/Parser.hs +++ b/minigent/src/Minigent/Syntax/Parser.hs @@ -95,7 +95,8 @@ toplevel = mdo atomicTy <- rule $ PrimType <$> primTy <|> TypeVar <$> typeVar <|> TypeVarBang <$> typeVar <* token (L.Bang) - <|> Record <$ token (L.Open L.Brace) + <|> Record <$> recTy + <* token (L.Open L.Brace) <*> (Row.fromList <$> fieldEntries) <* token (L.Close L.Brace) <*> sigil @@ -248,6 +249,12 @@ toplevel = mdo typeVars <- rule $ (:) <$> typeVar <* token (L.Comma) <*> typeVars <|> (:[]) <$> typeVar <|> pure [] + + -- mu t + recTy <- rule $ Rec <$> (token (L.Keyword L.Mu) *> typeVar) + -- recursive parameter ommitted + <|> pure None + "recursive type" constraint <- rule $ Share . TypeVar <$ token (L.UpperIdent "Share") <*> typeVar <|> Drop . TypeVar <$ token (L.UpperIdent "Drop") <*> typeVar @@ -266,7 +273,7 @@ toplevel = mdo <|> Forall [] [] <$> ty topLevel <- rule $ TypeSig <$> var <* token (L.Colon) - <*> polyType + <*> polyType <* token (L.Semi) <|> Equation <$> var <*> var diff --git a/minigent/src/Minigent/Syntax/PrettyPrint.hs b/minigent/src/Minigent/Syntax/PrettyPrint.hs index b26d3e8f4..80b292cef 100644 --- a/minigent/src/Minigent/Syntax/PrettyPrint.hs +++ b/minigent/src/Minigent/Syntax/PrettyPrint.hs @@ -26,17 +26,19 @@ import Data.Text.Prettyprint.Doc.Render.Terminal import qualified Data.Text as T import qualified Data.Map as M +import Minigent.TC.Assign + prettyPrimType t = annotate S.primType (viaShow (t :: PrimType)) -prettyREntry (Entry v x tk) - = annotate S.field (pretty v) - <+> annotate S.sym ":" +prettyREntry (Entry v x tk) + = annotate S.field (pretty v) + <+> annotate S.sym ":" <+> prettyType x <> if tk then space <> annotate S.keyword "take" else mempty -prettyVEntry (Entry v x tk) - = annotate S.con (pretty v) +prettyVEntry (Entry v x tk) + = annotate S.con (pretty v) <+> prettyType x <> if tk then space <> annotate S.keyword "take" else mempty @@ -46,6 +48,9 @@ prettySigil Unboxed = annotate S.sigil "#" prettySigil (UnknownSigil s) = annotate S.sigil (pretty s) prettySigil _ = mempty +prettyRecPar None = mempty +prettyRecPar (Rec x) = annotate S.typeVar (annotate S.keyword "mu" <+> pretty x) <+> mempty +prettyRecPar (UnknownParameter x) = annotate S.unifVar (pretty x) <+> mempty prettyVRow r@(Row _ Nothing) = encloseSep langle rangle pipe (map prettyVEntry (Row.entries r)) prettyVRow r@(Row _ (Just v)) = encloseSep langle rangle pipe (map prettyVEntry (Row.entries r) @@ -55,16 +60,18 @@ prettyRRow r@(Row _ Nothing) = encloseSep lbrace rbrace comma (map prettyREntry prettyRRow r@(Row _ (Just v)) = encloseSep lbrace rbrace comma (map prettyREntry (Row.entries r) ++ [annotate S.var (pretty (v ++ "...")) ]) -prettyType ty = case ty of +prettyType ty = case ty of Function t1 t2 -> align (sep [pretty' t1, annotate S.sym "->" <+> prettyType t2]) Bang t -> annotate S.typeOp "bang" <+> prettyA t _ -> pretty' ty where prettyA (TypeVar n) = annotate S.typeVar (pretty n) + prettyA (RecPar n _) = annotate S.keyword "rec" <+> annotate S.typeVar (pretty n) prettyA (UnifVar n) = annotate S.unifVar (pretty n) prettyA (TypeVarBang n) = annotate S.typeVar (pretty n) <> annotate S.sigil "!" + prettyA (RecParBang n _) = annotate S.keyword "rec" <+> annotate S.typeVar (pretty n) <> annotate S.sigil "!" prettyA (PrimType t) = prettyPrimType t - prettyA (Record r s) = align (prettyRRow r) <> prettySigil s + prettyA (Record n r s) = prettyRecPar n <> align (prettyRRow r) <> prettySigil s prettyA (Variant r) = align (prettyVRow r) prettyA (AbsType n s []) = annotate S.absType (pretty n) <> prettySigil s prettyA ty = parens (prettyType ty) @@ -81,19 +88,19 @@ prettyOp o | Just v <- lookup o (map (\(a,b) -> (b,a)) operators) prettyExp (Sig e t) = prettyExp e <+> annotate S.sym ":" <+> prettyType t prettyExp e = prettyBool e -prettyBool (PrimOp o [e1,e2]) +prettyBool (PrimOp o [e1,e2]) | o `elem` boolOps = prettyBool e1 <+> prettyOp o <+> prettyComp e2 prettyBool e = prettyComp e -prettyComp (PrimOp o [e1,e2]) +prettyComp (PrimOp o [e1,e2]) | o `elem` compOps = prettySum e1 <+> prettyOp o <+> prettySum e2 prettyComp e = prettySum e -prettySum (PrimOp o [e1,e2]) +prettySum (PrimOp o [e1,e2]) | o `elem` sumOps = prettySum e1 <+> prettyOp o <+> prettyProd e2 prettySum e = prettyProd e -prettyProd (PrimOp o [e1,e2]) +prettyProd (PrimOp o [e1,e2]) | o `elem` prodOps = prettyProd e1 <+> prettyOp o <+> prettyApp e2 prettyProd e = prettyApp e @@ -110,59 +117,59 @@ prettyAtom (If e1 e2 e3) , annotate S.keyword "then" <+> prettyExp e2 , annotate S.keyword "else" <+> prettyExp e3 , annotate S.keyword "end" ]) -prettyAtom (Let v e1 e2) +prettyAtom (Let v e1 e2) = align (sep [ annotate S.keyword "let" <+> annotate S.var (pretty v) - <+> annotate S.sym "=" + <+> annotate S.sym "=" <+> prettyExp e1 , annotate S.keyword "in" <+> prettyExp e2 - , annotate S.keyword "end" ]) -prettyAtom (LetBang vs v e1 e2) + , annotate S.keyword "end" ]) +prettyAtom (LetBang vs v e1 e2) = align (sep [ annotate S.keyword "let" <> annotate S.sigil "!" <+> align (tupled (map (annotate S.var . pretty) vs)) <+> annotate S.var (pretty v) - <+> annotate S.sym "=" + <+> annotate S.sym "=" <+> prettyExp e1 , annotate S.keyword "in" <+> prettyExp e2 - , annotate S.keyword "end" ]) + , annotate S.keyword "end" ]) prettyAtom (Struct fs) = align . encloseSep lbrace rbrace comma $ map (\(f, e) -> annotate S.field (pretty f) <+> annotate S.sym "=" <+> prettyExp e) fs -prettyAtom (Case e c v1 e1 v2 e2) +prettyAtom (Case e c v1 e1 v2 e2) = align (sep [ annotate S.keyword "case" <+> prettyExp e <+> annotate S.keyword "of", - indent 2 (annotate S.con (pretty c) <+> annotate S.var (pretty v1) - <+> annotate S.sym "->" + indent 2 (annotate S.con (pretty c) <+> annotate S.var (pretty v1) + <+> annotate S.sym "->" <+> prettyExp e1) , annotate S.sym "|" <+> hang 2 (annotate S.var (pretty v2 ) - <+> annotate S.sym "->" + <+> annotate S.sym "->" <+> prettyExp e2) , annotate S.keyword "end" ]) -prettyAtom (Esac e c v1 e1) +prettyAtom (Esac e c v1 e1) = align (sep [ annotate S.keyword "case" <+> prettyExp e <+> annotate S.keyword "of", - indent 2 (annotate S.con (pretty c) <+> annotate S.var (pretty v1) - <+> annotate S.sym "->" + indent 2 (annotate S.con (pretty c) <+> annotate S.var (pretty v1) + <+> annotate S.sym "->" <+> prettyExp e1) , annotate S.keyword "end" ]) -prettyAtom (Take r f v e1 e2) +prettyAtom (Take r f v e1 e2) = align (sep [ annotate S.keyword "take" <+> annotate S.var (pretty r) <+> lbrace <+> annotate S.field (pretty f) - <+> annotate S.sym "=" + <+> annotate S.sym "=" <+> annotate S.var (pretty v) - <+> rbrace - <+> annotate S.sym "=" + <+> rbrace + <+> annotate S.sym "=" <+> prettyExp e1 , annotate S.keyword "in" <+> prettyExp e2 - , annotate S.keyword "end" ]) -prettyAtom (Put e1 f e2 ) + , annotate S.keyword "end" ]) +prettyAtom (Put e1 f e2 ) = align (sep [ annotate S.keyword "put" <+> prettyExp e1 <> annotate S.sym "." <> annotate S.field (pretty f) - <+> annotate S.sym ":=" + <+> annotate S.sym ":=" <+> prettyExp e2 - , annotate S.keyword "end" ]) + , annotate S.keyword "end" ]) prettyAtom (Member e f) = prettyAtom e <> annotate S.sym "." <> annotate S.field (pretty f) prettyAtom e = parens (prettyExp e) @@ -170,17 +177,17 @@ prettyLiteral (BoolV b) = annotate S.literal (viaShow b) prettyLiteral (IntV i) = annotate S.literal (viaShow i) prettyLiteral (UnitV) = annotate S.literal "Unit" -prettyToplevel (TypeSig f t) = annotate S.func (pretty f) - <+> annotate S.sym ":" +prettyToplevel (TypeSig f t) = annotate S.func (pretty f) + <+> annotate S.sym ":" <+> prettyPolyType t <> annotate S.sym ";" -prettyToplevel (Equation f x t) = annotate S.func (pretty f) +prettyToplevel (Equation f x t) = annotate S.func (pretty f) <+> annotate S.var (pretty x) <+> annotate S.sym "=" <+> prettyExp t <> annotate S.sym ";" -prettyGlobalEnvs (GlobalEnvs defns types) +prettyGlobalEnvs (GlobalEnvs defns types) = align . vsep . map prettyToplevel . flip concatMap (M.toList types) $ \(f,t) -> TypeSig f t : case M.lookup f defns of @@ -194,25 +201,46 @@ prettySimpleConstraint c = case c of (Exhausted p) -> annotate S.constraintKeyword "Exhausted" <+> prettyType p (Solved p) -> annotate S.constraintKeyword "Solved" <+> prettyType p (t1 :< t2) -> prettyType t1 <+> annotate S.constraintKeyword ":<" <+> prettyType t2 - (i :<=: t) -> annotate S.literal (viaShow i) - <+> annotate S.constraintKeyword ":<=:" + (i :<=: t) -> annotate S.literal (viaShow i) + <+> annotate S.constraintKeyword ":<=:" <+> prettyType t - (t1 :=: t2) -> prettyType t1 <+> annotate S.constraintKeyword ":=:" <+> prettyType t2 + (t1 :=: t2) -> prettyType t1 <+> annotate S.constraintKeyword ":=:" <+> prettyType t2 (Sat) -> annotate S.constraintKeyword "Sat" (Unsat) -> annotate S.constraintKeyword "Unsat" + (UnboxedNoRecurse t) -> annotate S.constraintKeyword "UnboxedNoRecurse" <+> prettyType t _ -> error "prettySimpleConstraint called on non-simple constraint" prettyConstraint cs = vsep (punctuate (space <> annotate S.constraintKeyword ":&:") (map prettySimpleConstraint (flattenConstraint cs))) -prettyPolyType (Forall [] [] t) = prettyType t -prettyPolyType (Forall ts c t) = align (sep [ list (map (prettyType . TypeVar) ts) +prettyPolyType (Forall [] [] t) = prettyType t +prettyPolyType (Forall ts c t) = align (sep [ list (map (prettyType . TypeVar) ts) , sep (punctuate comma (map prettyConstraint c)) <> annotate S.sym "." - , prettyType t ] ) - + , prettyType t ] ) +debugAssigns + = T.unpack . renderStrict + . layoutPretty defaultLayoutOptions + . vcat . map (newl . prettyAssign) + where + prettyAssign (TyAssign v t) + = parens $ annotate S.con "TyAssign" <+> annotate S.unifVar (pretty v) <+> prettyType t + prettyAssign (RowAssign v r) + = parens $ annotate S.con "RowAssign" <+> annotate S.unifVar (pretty v) <+> prettyRRow r + prettyAssign (SigilAssign v s) + = parens $ annotate S.con "SigilAssign" <+> annotate S.unifVar (pretty v) <+> prettySigil s + prettyAssign (RecParAssign v rp) + = parens $ annotate S.con "RecParAssign" <+> annotate S.unifVar (pretty v) <+> prettyRecPar rp + + newl s = s <> pretty (",\n" :: String) + + +debugPrettyType + = T.unpack . renderStrict + . layoutPretty defaultLayoutOptions + . prettyType debugPrettyConstraints = T.unpack . renderStrict diff --git a/minigent/src/Minigent/Syntax/Utils.hs b/minigent/src/Minigent/Syntax/Utils.hs index 8738d5412..fedc2fe62 100644 --- a/minigent/src/Minigent/Syntax/Utils.hs +++ b/minigent/src/Minigent/Syntax/Utils.hs @@ -14,7 +14,10 @@ module Minigent.Syntax.Utils operators , -- ** Operator categories -- | The various syntactic precendence categories of binary operators - prodOps, sumOps, compOps, boolOps + prodOps + , sumOps + , compOps + , boolOps , -- * Constraints flattenConstraint , conjunction @@ -23,6 +26,9 @@ module Minigent.Syntax.Utils -- ** Applying rewrites traverseType , normaliseType + , unroll + , mapRecPars + , mapRecParsPT , -- ** Rewrites substUV , substRowV @@ -30,11 +36,13 @@ module Minigent.Syntax.Utils , substTV , substUVs , substTVs + , substRecPar , -- ** Queries for type inference fits , unorderedType , typeUVs , typeVariables + , muTypeVariables , rigid , rootUnifVar , -- * Entries @@ -49,102 +57,125 @@ module Minigent.Syntax.Utils ) where -import Minigent.Syntax -import Minigent.Fresh +import Minigent.Syntax +import Minigent.Fresh import qualified Minigent.Syntax.Utils.Rewrite as RW -import qualified Minigent.Syntax.Utils.Row as Row +import qualified Minigent.Syntax.Utils.Row as Row -import Control.Applicative -import Control.Monad(guard) -import Data.Maybe (fromMaybe) +import Control.Applicative +import Control.Monad ( guard ) +import Data.Maybe ( fromMaybe + , maybeToList + , isNothing + ) -import qualified Data.Stream as S -import qualified Data.Map as M +import qualified Data.Stream as S +import qualified Data.Map as M +import Debug.Trace -- | Returns true iff the given argument type is not subject to subtyping. That is, if @a :\< b@ -- (subtyping) is equivalent to @a :=: b@ (equality), then this function returns true. -- -- At least for now, this returns true for all types but variants, records and functions. unorderedType :: Type -> Bool -unorderedType (Record {}) = False -unorderedType (Variant {}) = False -unorderedType (Function {}) = False -unorderedType t = rigid t +unorderedType (Record{} ) = False +unorderedType (Variant{} ) = False +unorderedType (Function{}) = False +unorderedType t = rigid t -- | Return all of the unification type variables inside a type. typeUVs :: Type -> [VarName] typeUVs (UnifVar v) = [v] -typeUVs (Record r s) = concatMap (\(Entry _ t _) -> typeUVs t) (Row.entries r) +typeUVs (Record n r s) = concatMap (\(Entry _ t _) -> typeUVs t) (Row.entries r) ++ maybe [] pure (rowVar r) - ++ (case s of UnknownSigil s' -> [s']; _ -> []) + ++ (case s of UnknownSigil s' -> [s']; _ -> []) + ++ (case n of UnknownParameter n' -> [n']; _ -> []) typeUVs (Variant r) = concatMap (\(Entry _ t _) -> typeUVs t) (Row.entries r) ++ maybe [] pure (rowVar r) typeUVs (AbsType _ _ ts) = concatMap typeUVs ts typeUVs (Function t1 t2) = typeUVs t1 ++ typeUVs t2 -typeUVs (Bang t) = typeUVs t -typeUVs _ = [] +typeUVs (Bang t ) = typeUVs t +typeUVs _ = [] --- | Return all of the (rigid, non-unification) type variables in a type. +-- | Return all of the (rigid, non-unification) type variables in a type. Does not include mu variables typeVariables :: Type -> [VarName] -typeVariables (TypeVar v) = [v] -typeVariables (TypeVarBang v) = [v] -typeVariables (Record r _) = concatMap (\(Entry _ t _) -> typeVariables t) (Row.entries r) -typeVariables (Variant r) = concatMap (\(Entry _ t _) -> typeVariables t) (Row.entries r) -typeVariables (AbsType _ _ ts) = concatMap typeVariables ts -typeVariables (Function t1 t2) = typeVariables t1 ++ typeVariables t2 -typeVariables (Bang t) = typeVariables t -typeVariables _ = [] +typeVariables t = typeVariables' t [] + where + -- Ensures recursive parameters are not included in type variables + typeVariables' :: Type -> [VarName] -> [VarName] + typeVariables' (TypeVar v) mvs = if elem v mvs then [] else [v] + typeVariables' (TypeVarBang v) mvs = if elem v mvs then [] else [v] + typeVariables' (Record mt r _) mvs = concatMap + (\(Entry _ t _) -> typeVariables' t ((case mt of Rec x -> [x]; _ -> []) ++ mvs)) + (Row.entries r) + typeVariables' (Variant r) mvs = concatMap (\(Entry _ t _) -> typeVariables' t mvs) (Row.entries r) + typeVariables' (AbsType _ _ ts) mvs = concatMap (\x -> typeVariables' x mvs) ts + typeVariables' (Function t1 t2) mvs = typeVariables' t1 mvs ++ typeVariables' t2 mvs + typeVariables' (Bang t ) mvs = typeVariables' t mvs + typeVariables' _ _ = [] + +muTypeVariables :: Type -> [VarName] +muTypeVariables (Record mt r _) = case mt of Rec x -> [x]; _ -> [] + ++ concatMap (\(Entry _ t _) -> muTypeVariables t) (Row.entries r) +muTypeVariables (Variant r) = + concatMap (\(Entry _ t _) -> muTypeVariables t) (Row.entries r) +muTypeVariables (AbsType _ _ ts) = concatMap muTypeVariables ts +muTypeVariables (Function t1 t2) = muTypeVariables t1 ++ muTypeVariables t2 +muTypeVariables (Bang t ) = muTypeVariables t +muTypeVariables _ = [] + -- | Returns @True@ unless the given type is a unification variable or a type operator -- applied to a unification variable. rigid :: Type -> Bool rigid (UnifVar _) = False rigid (Bang _) = False -rigid (Record r _) = not $ Row.justVar r +rigid (Record _ r _) = not $ Row.justVar r rigid (Variant r) = not $ Row.justVar r rigid _ = True -- | Return the unification variable in a non-rigid type. -- If the type is rigid, then returns @Nothing@. rootUnifVar :: Type -> Maybe VarName -rootUnifVar (UnifVar n) = Just n -rootUnifVar (Bang n) = rootUnifVar n -rootUnifVar (Variant r) = rowVar r -rootUnifVar (Record r s) = rowVar r -rootUnifVar _ = Nothing +rootUnifVar (UnifVar n ) = Just n +rootUnifVar (Bang n ) = rootUnifVar n +rootUnifVar (Variant r ) = rowVar r +rootUnifVar (Record _ r s) = rowVar r +rootUnifVar _ = Nothing -- | A table of all operators, mapping string representations -- to their 'Op' values. operators :: [(String, Op)] -operators = [ ("+", Plus) - , ("*", Times) - , ("-", Minus) - , ("/", Divide) - , ("%", Mod) - , ("<", Less) - , (">", Greater) - , ("==", Equal) - , ("/=", NotEqual) - , ("<=", LessEqual) - , (">=", GreaterEqual) - , ("&&", And) - , ("||", Or) - , ("~", Not) - ] +operators = + [ ("+" , Plus) + , ("*" , Times) + , ("-" , Minus) + , ("/" , Divide) + , ("%" , Mod) + , ("<" , Less) + , (">" , Greater) + , ("==", Equal) + , ("/=", NotEqual) + , ("<=", LessEqual) + , (">=", GreaterEqual) + , ("&&", And) + , ("||", Or) + , ("~" , Not) + ] prodOps, sumOps, compOps, boolOps :: [Op] prodOps = [Times, Divide, Mod] -sumOps = [Plus, Minus] -compOps = [Equal, NotEqual,Greater,Less, GreaterEqual, LessEqual] +sumOps = [Plus, Minus] +compOps = [Equal, NotEqual, Greater, Less, GreaterEqual, LessEqual] boolOps = [And, Or, Not] -- | Given a constraint, flatten it out to remove all conjunctions, -- returning a list of conjunction-free constraints. flattenConstraint :: Constraint -> [Constraint] flattenConstraint (a :&: b) = flattenConstraint a ++ flattenConstraint b -flattenConstraint x = [x] +flattenConstraint x = [x] -- | Given a list of constraints, combine them into one constraint -- using constraint conjunction. @@ -161,38 +192,40 @@ entryTypes func (Entry f t k) = Entry f (func t) k constraintTypes :: (Type -> Type) -> Constraint -> Constraint constraintTypes func constraint = go constraint where - go (c1 :&: c2) = go c1 :&: go c2 - go (i :<=: t) = i :<=: func t - go (Share t) = Share (func t) - go (Drop t) = Drop (func t) - go (Escape t) = Escape (func t) - go (Exhausted t) = Exhausted (func t) - go (t1 :< t2 ) = func t1 :< func t2 - go (t1 :=: t2 ) = func t1 :=: func t2 - go (Solved t) = Solved $ func t - go Sat = Sat - go Unsat = Unsat + go (c1 :&: c2) = go c1 :&: go c2 + go (i :<=: t) = i :<=: func t + go (Share t) = Share (func t) + go (Drop t) = Drop (func t) + go (Escape t) = Escape (func t) + go (Exhausted t) = Exhausted (func t) + go (t1 :< t2 ) = func t1 :< func t2 + go (t1 :=: t2 ) = func t1 :=: func t2 + go (Solved t) = Solved $ func t + go Sat = Sat + go (UnboxedNoRecurse t) = UnboxedNoRecurse $ func t + go Unsat = Unsat + -- | Given a function that acts on 'Type' values, produce a function -- that acts on the types inside an 'Expr'. exprTypes :: (Type -> Type) -> Expr -> Expr exprTypes func expr = go expr - where - go (TypeApp f ts) = TypeApp f (map func ts) - go (Sig e t) = Sig (go e) (func t) - go (PrimOp o es) = PrimOp o (map go es) - go (Con n e) = Con n (go e) - go (Apply e1 e2) = Apply (go e1) (go e2) - go (Struct fs) = Struct (map (fmap go) fs) - go (If e e1 e2) = If (go e) (go e1) (go e2) - go (Let v e1 e2) = Let v (go e1) (go e2) - go (LetBang vs v e1 e2) = LetBang vs v (go e1) (go e2) - go (Take r f v e1 e2) = Take r f v (go e1) (go e2) - go (Put e1 f e2) = Put (go e1) f (go e2) - go (Member e f) = Member (go e) f - go (Case e k x e1 y e2) = Case (go e) k x (go e1) y (go e2) - go (Esac e k x e1) = Esac (go e) k x (go e1) - go e = e + where + go (TypeApp f ts ) = TypeApp f (map func ts) + go (Sig e t ) = Sig (go e) (func t) + go (PrimOp o es ) = PrimOp o (map go es) + go (Con n e ) = Con n (go e) + go (Apply e1 e2 ) = Apply (go e1) (go e2) + go (Struct fs ) = Struct (map (fmap go) fs) + go (If e e1 e2 ) = If (go e) (go e1) (go e2) + go (Let v e1 e2 ) = Let v (go e1) (go e2) + go (LetBang vs v e1 e2) = LetBang vs v (go e1) (go e2) + go (Take r f v e1 e2 ) = Take r f v (go e1) (go e2) + go (Put e1 f e2 ) = Put (go e1) f (go e2) + go (Member e f ) = Member (go e) f + go (Case e k x e1 y e2) = Case (go e) k x (go e1) y (go e2) + go (Esac e k x e1 ) = Esac (go e) k x (go e1) + go e = e -- | Given a 'RW.Rewrite' on types, apply it over every subterm in a type, i.e. recursively applying -- the rewrite to every subterm. @@ -204,14 +237,15 @@ exprTypes func expr = go expr -- think. traverseType :: (RW.Rewrite Type) -> Type -> Type traverseType func ty = case RW.run func ty of - Just t' -> t' - Nothing -> case ty of - Record es s -> Record (Row.mapEntries (entryTypes (traverseType func)) es) s + Just t' -> t' + Nothing -> case ty of + Record n es s -> + Record n (Row.mapEntries (entryTypes (traverseType func)) es) s AbsType n s ts -> AbsType n s (map (traverseType func) ts) - Variant es -> Variant (Row.mapEntries (entryTypes (traverseType func)) es) + Variant es -> Variant (Row.mapEntries (entryTypes (traverseType func)) es) Function t1 t2 -> Function (traverseType func t1) (traverseType func t2) Bang t -> Bang (traverseType func t) - _ -> ty + _ -> ty -- | Given a 'RW.Rewrite' on types, apply it over every subterm in a type, i.e. recursively applying -- the rewrite to every subterm. @@ -224,45 +258,88 @@ traverseType func ty = case RW.run func ty of normaliseType :: (RW.Rewrite Type) -> Type -> Type normaliseType func ty = let t' = fromMaybe ty (RW.run func ty) - in case t' of - Record es s -> Record (Row.mapEntries (entryTypes (normaliseType func)) es) s - AbsType n s ts -> AbsType n s (map (normaliseType func) ts) - Variant es -> Variant (Row.mapEntries (entryTypes (normaliseType func)) es) - Function t1 t2 -> Function (normaliseType func t1) (normaliseType func t2) - Bang t -> Bang (normaliseType func t) - _ -> t' + in + case t' of + Record n es s -> + Record n (Row.mapEntries (entryTypes (normaliseType func)) es) s + AbsType n s ts -> AbsType n s (map (normaliseType func) ts) + Variant es -> + Variant (Row.mapEntries (entryTypes (normaliseType func)) es) + Function t1 t2 -> + Function (normaliseType func t1) (normaliseType func t2) + Bang t -> Bang (normaliseType func t) + _ -> t' + + +-- | Unrolls a recursive parameter to the record it references +unroll :: Type -> Type +unroll (RecPar n ctxt) = mapRecPars ctxt (ctxt M.! n) +-- TODO: Should this be an error? +unroll t = trace "Warning: Unroll called on type that is not a recursive parameter" t + +-- | Given a PolyType definition, changes all recursive parameter references from TypeVar to RecPar +mapRecParsPT :: PolyType -> PolyType +mapRecParsPT (Forall vs cs t) = Forall vs cs $ mapRecPars M.empty t + +-- | Given a context, changes all recursive parameter references from TypeVar to RecPar according to the context +mapRecPars :: M.Map VarName Type -> Type -> Type +mapRecPars rp (AbsType n s ts) = AbsType n s $ map (mapRecPars rp) ts +mapRecPars rp (Variant row) = Variant $ Row.mapEntries (\(Entry n t tk) -> Entry n (mapRecPars rp t) tk) row +mapRecPars rp (Bang t) = Bang $ mapRecPars rp t +mapRecPars rp tv@(TypeVar v) = if M.member v rp then (RecPar v rp) else tv +mapRecPars rp tv@(TypeVarBang v) = if M.member v rp then (RecParBang v rp) else tv +mapRecPars rp r@(Record par row s) = + Record par (Row.mapEntries (\(Entry n t tk) -> Entry n (mapRecPars (addRecPar par) t) tk) row) s + where addRecPar p = case p of + Rec v -> (M.insert v r rp) + _ -> rp +mapRecPars rp (Function a b) = Function (mapRecPars rp a) (mapRecPars rp b) +mapRecPars _ t = t + -- | A rewrite that substitutes a given unification type variable for a type term in a type. substUV :: (VarName, Type) -> RW.Rewrite Type -substUV (x, t) = RW.rewrite $ \ t' -> case t' of - (UnifVar v) | x == v -> Just t - _ -> Nothing +substUV (x, t) = RW.rewrite $ + \t' -> case t' of + (UnifVar v) | x == v -> Just t + _ -> Nothing -- | A rewrite that substitutes a given unification row variable for a row in a type. substRowV :: (VarName, Row) -> RW.Rewrite Type -substRowV (x, (Row m' q)) = RW.rewrite $ \ t' -> case t' of - Variant (Row m (Just v)) | x == v -> Just (Variant (Row (M.union m m') q)) - Record (Row m (Just v)) s | x == v -> Just (Record (Row (M.union m m') q) s) - _ -> Nothing +substRowV (x, (Row m' q)) = RW.rewrite $ + \t' -> case t' of + Variant (Row m (Just v)) | x == v -> Just (Variant (Row (M.union m m') q)) + Record n (Row m (Just v)) s | x == v -> + Just (Record n (Row (M.union m m') q) s) + _ -> Nothing -- | A rewrite that substitutes a given unification sigil variable for a sigil in a type. substSigilV :: (VarName, Sigil) -> RW.Rewrite Type -substSigilV (x, s) = RW.rewrite $ \ t' -> case t' of - Record r (UnknownSigil v) | x == v -> Just (Record r s) - _ -> Nothing +substSigilV (x, s) = RW.rewrite $ + \t' -> case t' of + Record n r (UnknownSigil v) | x == v -> Just (Record n r s) + _ -> Nothing -- | A rewrite that substitutes a rigid type variable for a type term in a type. substTV :: (VarName, Type) -> RW.Rewrite Type -substTV (x, t) = RW.rewrite $ \ t' -> case t' of - (TypeVar v) | x == v -> Just t - (TypeVarBang v) | x == v -> Just (Bang t) - _ -> Nothing +substTV (x, t) = RW.rewrite $ + \t' -> case t' of + (TypeVar v) | x == v -> Just t + (TypeVarBang v) | x == v -> Just (Bang t) + _ -> Nothing + +-- | A rewrite that substitutes the unkown recursive parameter on a boxed record for a parameter +substRecPar :: (VarName, RecPar) -> RW.Rewrite Type +substRecPar (v1, v2) = RW.rewrite $ + \t' -> case t' of + Record (UnknownParameter n) r s | n == v1 -> + Just (Record v2 r s) + _ -> Nothing -- | A convenience that allows multiple substitutions to type variables to be made simulatenously. substTVs :: [(VarName, Type)] -> RW.Rewrite Type substTVs = foldMap substTV - -- | A convenience that allows multiple substitutions to unification type variables to be made -- simulatenously. substUVs :: [(VarName, Type)] -> RW.Rewrite Type @@ -284,9 +361,9 @@ fits _ _ = False -- | Returns @True@ if the two inputs are equal, or if either of them are an unknown sigil -- variable (morally, in this case the two inputs could be made equal by unification). sigilsCompatible :: Sigil -> Sigil -> Bool -sigilsCompatible (UnknownSigil {}) y = True -sigilsCompatible x (UnknownSigil {}) = True -sigilsCompatible x y = x == y +sigilsCompatible (UnknownSigil{}) y = True +sigilsCompatible x (UnknownSigil{}) = True +sigilsCompatible x y = x == y -- | Run a 'Fresh' computation with 'unifVars' as the source of fresh names. withUnifVars :: Fresh VarName a -> a diff --git a/minigent/src/Minigent/TC.hs b/minigent/src/Minigent/TC.hs index cf8d2ef1b..fd6a3bc02 100644 --- a/minigent/src/Minigent/TC.hs +++ b/minigent/src/Minigent/TC.hs @@ -24,6 +24,8 @@ import Control.Monad.Reader import qualified Data.Map as M import Debug.Trace +import Minigent.Syntax.PrettyPrint + -- | Run type checking/inference on the given definitions under the given 'GlobalEnvironments'. -- -- Returns either a list of unsolved constraints (if inference fails) or a new definition diff --git a/minigent/src/Minigent/TC/Assign.hs b/minigent/src/Minigent/TC/Assign.hs index 8e7826b88..9575e2a2e 100644 --- a/minigent/src/Minigent/TC/Assign.hs +++ b/minigent/src/Minigent/TC/Assign.hs @@ -21,9 +21,13 @@ import qualified Minigent.Syntax.Utils.Rewrite as Rewrite data Assign = TyAssign VarName Type | RowAssign VarName Row | SigilAssign VarName Sigil + | RecParAssign VarName RecPar + deriving (Show) -- | Apply an assignment to a unification variable to a type. substAssign :: Assign -> Rewrite.Rewrite Type substAssign (TyAssign v t) = substUV (v, t) substAssign (RowAssign v t) = substRowV (v, t) substAssign (SigilAssign v t) = substSigilV (v, t) +substAssign (RecParAssign v1 v2) = substRecPar (v1, v2) + diff --git a/minigent/src/Minigent/TC/ConstraintGen.hs b/minigent/src/Minigent/TC/ConstraintGen.hs index 423f0accf..0499cac9d 100644 --- a/minigent/src/Minigent/TC/ConstraintGen.hs +++ b/minigent/src/Minigent/TC/ConstraintGen.hs @@ -24,6 +24,7 @@ import Control.Monad.State.Strict import qualified Data.Map as M import Data.Stream (Stream) +import Minigent.Syntax.PrettyPrint import Debug.Trace -- | A monad that is a combination of a state monad for the current type context, @@ -183,42 +184,54 @@ cg e tau = case e of (Member e f) -> do row <- Row.incomplete [Entry f tau False] sigil <- fresh - let alpha = Record row (UnknownSigil sigil) + recPar <- UnknownParameter <$> fresh + -- TODO: Member is supposed to be on nonlinear records, will these ever have a recursive parameter + -- (i.e. are they *always* unboxed records?) + let alpha = Record recPar row (UnknownSigil sigil) (e', c1) <- cg e alpha - let c2 = Drop (Record (Row.take f row) (UnknownSigil sigil)) + let c2 = Drop (Record recPar (Row.take f row) (UnknownSigil sigil)) withSig (Member e' f, c1 :&: c2) + -- Remaining record, field name, extracted contents var, record extrating from, following expression (Take x f y e1 e2) -> do beta <- UnifVar <$> fresh row <- Row.incomplete [Entry f beta False] - sigil <- fresh - let alpha = Record row (UnknownSigil sigil) + sigil <- fresh + recPar <- UnknownParameter <$> fresh + let alpha = Record recPar row (UnknownSigil sigil) + let c0 = UnboxedNoRecurse alpha (e1', c1) <- cg e1 alpha modify (push (y, beta)) - modify (push (x, Record (Row.take f row) (UnknownSigil sigil))) + modify (push (x, Record recPar (Row.take f row) (UnknownSigil sigil))) (e2', c2) <- cg e2 tau xUsed <- topUsed <$> get - let c3 = if xUsed then Sat else Drop (Record (Row.take f row) (UnknownSigil sigil)) + let c3 = if xUsed then Sat else Drop (Record recPar (Row.take f row) (UnknownSigil sigil)) modify pop yUsed <- topUsed <$> get let c4 = if yUsed then Sat else Drop beta modify pop - withSig (Take x f y e1' e2', c1 :&: c2 :&: c3 :&: c4) + withSig (Take x f y e1' e2', c0 :&: c1 :&: c2 :&: c3 :&: c4)-- :&: c5) (Put e1 f e2) -> do beta <- UnifVar <$> fresh - row <- Row.incomplete [Entry f beta True] sigil <- fresh - let alpha = Record row (UnknownSigil sigil) + recPar <- UnknownParameter <$> fresh + row <- Row.incomplete [Entry f beta True] + + let alpha = Record recPar row (UnknownSigil sigil) (e1', c1) <- cg e1 alpha (e2', c2) <- cg e2 beta - let c3 = Record (Row.put f row) (UnknownSigil sigil) :< tau - withSig (Put e1' f e2', c1 :&: c2 :&: c3) + + let c0 = UnboxedNoRecurse alpha + + let c3 = Record recPar (Row.put f row) (UnknownSigil sigil) :< tau + + withSig (Put e1' f e2', c0 :&: c1 :&: c2 :&: c3) (Struct fs) -> do (fs', ts, cs) <- cgStruct fs - withSig (Struct fs', conjunction cs :&: Record (Row.fromList ts) Unboxed :< tau ) + withSig (Struct fs', conjunction cs :&: Record None (Row.fromList ts) Unboxed :< tau ) where @@ -234,16 +247,19 @@ cg e tau = case e of withSig :: (Expr, Constraint) -> CG (Expr, Constraint) withSig (e, c) = pure (Sig e tau, c) + -- | Looks up a variable and increases it's usage count, adding the + -- constraint that it is shareable if it's been used more than once lookupVar :: VarName -> CG (Type, Constraint) lookupVar v = do (rho, used, ctx') <- use v <$> get put ctx' return (rho, if used then Share rho else Sat) + -- | Used for constraint generation for top-level functions. -- Given a function name, argument name and a function body expression, -- return an annotated function body along with the constraint that would make --- it well typed. Also included in the first componenet of the return value +-- it well typed. Also included in the first component of the return value -- are the axioms (constraints placed by the user in the type signature) -- about polymorphic type variables. cgFunction :: FunName -> VarName -> Expr -> CG ([Constraint], Expr, Constraint) @@ -260,4 +276,7 @@ cgFunction f x e = do let (c'',axs) = case M.lookup f (types envs) of Nothing -> (Sat, []) Just (Forall vs cs tau) -> (proposedType :< tau, cs) + -- Inferred constraints for return type + -- && proposed function type is subtype of inferred function type + -- && Argument to function is used or droppable pure (axs, e', c :&: c'' :&: c') diff --git a/minigent/src/Minigent/TC/Equate.hs b/minigent/src/Minigent/TC/Equate.hs index 9e5a8fc01..f6f2ef0f4 100644 --- a/minigent/src/Minigent/TC/Equate.hs +++ b/minigent/src/Minigent/TC/Equate.hs @@ -26,9 +26,15 @@ import qualified Data.Map as M import Debug.Trace +import Minigent.Syntax.PrettyPrint + -- | The equate phase, which finds subtyping constraints that can be safely converted to equalities. equate :: Rewrite.Rewrite [Constraint] equate = Rewrite.withTransform findEquatable (pure . map toEquality) + -- (\x -> + -- let c = toEquality x + -- in trace ("About to simpliy:\n" ++ debugPrettyConstraints [c]) c) + -- ) where findEquatable cs = let mentions = getMentions cs @@ -83,15 +89,16 @@ findEquateCandidates mentions (c:cs) = let , Row.justVar r1 , canEquate fst a t -> (c:sups, subs, others) - Record r1 s :< t | Just a <- rowVar r1 - , Row.justVar r1 + -- TODO: Rethink record equation with recpars + Record n r1 s :< t | Just a <- rowVar r1 + , Row.justVar r1 , canEquate fst a t -> (c:sups, subs, others) t :< Variant r1 | Just a <- rowVar r1 , Row.justVar r1 , canEquate snd a t -> (sups, c : subs, others) - t :< Record r1 s | Just a <- rowVar r1 + t :< Record n r1 s | Just a <- rowVar r1 , Row.justVar r1 , canEquate snd a t -> (sups, c : subs, others) diff --git a/minigent/src/Minigent/TC/JoinMeet.hs b/minigent/src/Minigent/TC/JoinMeet.hs index ca488a875..b8327ca2b 100644 --- a/minigent/src/Minigent/TC/JoinMeet.hs +++ b/minigent/src/Minigent/TC/JoinMeet.hs @@ -35,6 +35,8 @@ data Candidate = Meet Type Type Type joinMeet :: (Monad m, MonadFresh VarName m) => Rewrite.Rewrite' m [Constraint] joinMeet = Rewrite.withTransform find $ \c -> case c of +-- TODO: Fix this + Meet v (Function t1 t2) (Function r1 r2) -> do b1 <- UnifVar <$> fresh b2 <- UnifVar <$> fresh @@ -59,25 +61,28 @@ joinMeet = Rewrite.withTransform find $ \c -> case c of Join v (Variant r1) (Variant r2) | r1 == r2 -> do pure [Variant r1 :< v ] - Meet v (Record r1 s1) (Record r2 s2) | r1 /= r2 -> do + Meet v (Record n1 r1 s1) (Record n2 r2 s2) | r1 /= r2 -> do guard (Row.compatible r1 r2) guard (sigilsCompatible s1 s2) r <- Row.union Row.leastTaken r1 r2 s <- UnknownSigil <$> fresh - pure [v :< Record r s, Record r s :< Record r1 s1, Record r s :< Record r2 s2 ] + n <- UnknownParameter <$> fresh + pure [v :< Record n r s, Record n r s :< Record n1 r1 s1, Record n r s :< Record n2 r2 s2 ] - Meet v (Record r1 s1) (Record r2 s2) | r1 == r2 && s1 == s2 -> do - pure [v :< Record r1 s1] + Meet v (Record n1 r1 s1) (Record n2 r2 s2) | r1 == r2 && s1 == s2 && n1 == n2 -> do + pure [v :< Record n1 r1 s1] - Join v (Record r1 s1) (Record r2 s2) | r1 /= r2 -> do + Join v (Record n1 r1 s1) (Record n2 r2 s2) | r1 /= r2 -> do guard (Row.compatible r1 r2) guard (sigilsCompatible s1 s2) r <- Row.union Row.mostTaken r1 r2 s <- UnknownSigil <$> fresh - pure [Record r s :< v, Record r1 s1 :< Record r s, Record r2 s2 :< Record r s] + n <- UnknownParameter <$> fresh + pure [Record n r s :< v, Record n1 r1 s1 :< Record n r s, Record n2 r2 s2 :< Record n r s] - Join v (Record r1 s1) (Record r2 s2) | r1 == r2 && s1 == s2 -> do - pure [Record r1 s1 :< v ] + -- TODO: Check if the recursive parameters need to be compared? + Join v (Record n1 r1 s1) (Record n2 r2 s2) | r1 == r2 && s1 == s2 && n1 == n2 -> do + pure [Record n1 r1 s1 :< v] Join v (Function t1 t2) (Function r1 r2) -> do b1 <- UnifVar <$> fresh @@ -109,14 +114,14 @@ find (c:cs) = case c of ([] , rs ) -> fmap (c:) <$> find cs (rho :< _:rs, rs') -> pure (Join (Variant (Row m (Just v))) tau rho , rs ++ rs') - (Record (Row m (Just v)) s) :< tau@(Record (Row m' Nothing) s') + (Record n (Row m (Just v)) s) :< tau@(Record n' (Row m' Nothing) s') | M.null m -> case partition (flexRowSub v) cs of ([] , rs ) -> fmap (c:) <$> find cs - (_ :< rho :rs, rs') -> pure (Meet (Record (Row m (Just v)) s) tau rho , rs ++ rs') - tau@(Record (Row m' Nothing) s') :< (Record (Row m (Just v)) s) + (_ :< rho :rs, rs') -> pure (Meet (Record n (Row m (Just v)) s) tau rho , rs ++ rs') + tau@(Record n' (Row m' Nothing) s') :< (Record n (Row m (Just v)) s) | M.null m -> case partition (flexRowSup v) cs of ([] , rs ) -> fmap (c:) <$> find cs - (rho :< _:rs, rs') -> pure (Join (Record (Row m (Just v)) s) tau rho , rs ++ rs') + (rho :< _:rs, rs') -> pure (Join (Record n (Row m (Just v)) s) tau rho , rs ++ rs') _ -> fmap (c:) <$> find cs @@ -125,12 +130,12 @@ find (c:cs) = case c of flexRigidSub v _ = False flexRowSub v (Variant (Row m (Just v')) :< Variant (Row m' Nothing)) = M.null m && v == v' - flexRowSub v (Record (Row m (Just v')) s :< Record (Row m' Nothing) s') = M.null m && v == v' + flexRowSub v (Record _ (Row m (Just v')) s :< Record _ (Row m' Nothing) s') = M.null m && v == v' flexRowSub v _ = False flexRigidSup v (rho :< UnifVar v') = rigid rho && v == v' flexRigidSup v _ = False flexRowSup v (Variant (Row m Nothing) :< Variant (Row m' (Just v'))) = M.null m' && v == v' - flexRowSup v (Record (Row m Nothing) s :< Record (Row m' (Just v')) s') = M.null m' && v == v' + flexRowSup v (Record _ (Row m Nothing) s :< Record _ (Row m' (Just v')) s') = M.null m' && v == v' flexRowSup v _ = False diff --git a/minigent/src/Minigent/TC/Normalise.hs b/minigent/src/Minigent/TC/Normalise.hs index 8031e4087..5ea8a8d94 100644 --- a/minigent/src/Minigent/TC/Normalise.hs +++ b/minigent/src/Minigent/TC/Normalise.hs @@ -15,23 +15,33 @@ import Minigent.Syntax.Utils import Minigent.Syntax.Utils.Rewrite import qualified Minigent.Syntax.Utils.Row as Row -bangRW :: Rewrite Type -bangRW = rewrite $ \t -> case t of +import qualified Data.Map as M + + +-- TODO: Remove +import Debug.Trace +import Minigent.Syntax.PrettyPrint + +normaliseRW :: Rewrite Type +normaliseRW = rewrite $ \t -> --trace ("Norm about to look at type:\n" ++ debugPrettyType t) $ + case t of Bang (Function t1 t2) -> Just (Function t1 t2) Bang (AbsType n s ts) -> Just (AbsType n (bangSigil s) (map Bang ts)) Bang (TypeVar a) -> Just (TypeVarBang a) Bang (TypeVarBang a) -> Just (TypeVarBang a) + Bang (RecPar a ctxt) -> Just (RecParBang a ctxt) + Bang (RecParBang a ctxt) -> Just (RecParBang a ctxt) Bang (PrimType t) -> Just (PrimType t) Bang (Variant r) | rowVar r == Nothing -> Just (Variant (Row.mapEntries (entryTypes Bang) r)) - Bang (Record r s) | rowVar r == Nothing, s == ReadOnly || s == Writable || s == Unboxed - -> Just (Record (Row.mapEntries (entryTypes Bang) r) (bangSigil s)) - _ -> Nothing + Bang (Record n r s) | rowVar r == Nothing, s == ReadOnly || s == Writable || s == Unboxed + -> Just (Record n (Row.mapEntries (entryTypes Bang) r) (bangSigil s)) + + _ -> Nothing where bangSigil Writable = ReadOnly bangSigil x = x - -- | Normalise all types within a set of constraints normaliseConstraints :: [Constraint] -> [Constraint] -normaliseConstraints = nub . map (constraintTypes (normaliseType bangRW)) +normaliseConstraints = nub . map (constraintTypes (normaliseType normaliseRW)) diff --git a/minigent/src/Minigent/TC/Simplify.hs b/minigent/src/Minigent/TC/Simplify.hs index 3bd7866d8..e24c80d44 100644 --- a/minigent/src/Minigent/TC/Simplify.hs +++ b/minigent/src/Minigent/TC/Simplify.hs @@ -21,10 +21,14 @@ import qualified Data.Set as S import qualified Data.Map as M import Data.Foldable (toList) +import Minigent.Syntax.PrettyPrint +import Debug.Trace + -- | Rewrite a set of constraints, removing all trivially satisfiable constraints -- and breaking down large constraints into smaller ones. simplify :: [Constraint] -> Rewrite.Rewrite [Constraint] -simplify axs = Rewrite.pickOne $ \c -> case c of +simplify axs = Rewrite.pickOne $ \c -> -- trace ("About to simpliy:\n" ++ debugPrettyConstraints [c]) $ + case c of c | c `elem` axs -> Just [] Sat -> Just [] c1 :&: c2 -> Just [c1,c2] @@ -36,6 +40,9 @@ simplify axs = Rewrite.pickOne $ \c -> case c of Escape (Function _ _) -> Just [] Drop (TypeVarBang _) -> Just [] Share (TypeVarBang _) -> Just [] + Drop (RecParBang _ _) -> Just [] + Share (RecParBang _ _) -> Just [] + -- TODO: Drop/Share RecParBang? Share (Variant es) -> guard (rowVar es == Nothing) >> Just (map Share (Row.untakenTypes es)) Drop (Variant es) -> guard (rowVar es == Nothing) @@ -48,13 +55,13 @@ simplify axs = Rewrite.pickOne $ \c -> case c of >> Just (map Drop ts) Escape (AbsType n s ts) -> guard (s == Writable || s == Unboxed) >> Just (map Escape ts) - Share (Record es s) -> guard (s == ReadOnly || s == Unboxed) + Share (Record n es s) -> guard (s == ReadOnly || s == Unboxed) >> guard (rowVar es == Nothing) >> Just (map Share (Row.untakenTypes es)) - Drop (Record es s) -> guard (s == ReadOnly || s == Unboxed) + Drop (Record n es s) -> guard (s == ReadOnly || s == Unboxed) >> guard (rowVar es == Nothing) >> Just (map Drop (Row.untakenTypes es)) - Escape (Record es s) -> guard (s == Writable || s == Unboxed) + Escape (Record n es s) -> guard (s == Writable || s == Unboxed) >> guard (rowVar es == Nothing) >> Just (map Escape (Row.untakenTypes es)) Exhausted (Variant es) -> guard (null (Row.untakenTypes es) && rowVar es == Nothing) @@ -79,11 +86,11 @@ simplify axs = Rewrite.pickOne $ \c -> case c of c = Variant r1' :< Variant r2' Just (c:cs) - Record r1 s1 :< Record r2 s2 -> - if Row.null r1 && Row.null r2 && s1 == s2 then Just [] + Record n1 r1 s1 :< Record n2 r2 s2 -> + if Row.null r1 && Row.null r2 && s1 == s2 && n1 == n2 then Just [] else if Row.null r1 && null (Row.entries r2) || Row.null r2 && null (Row.entries r1) - then Just [Record r1 s1 :=: Record r2 s2] + then Just [Record n1 r1 s1 :=: Record n2 r2 s2] else do let commons = Row.common r1 r2 (ls, rs) = unzip commons @@ -92,9 +99,40 @@ simplify axs = Rewrite.pickOne $ \c -> case c of let (r1',r2') = Row.withoutCommon r1 r2 cs = map (\(Entry _ t _, Entry _ t' _) -> t :< t') commons ds = map Drop (Row.typesFor (untakenLabels ls S.\\ untakenLabels rs) r1) - c = Record r1' s1 :< Record r2' s2 + c = Record n1 r1' s1 :< Record n2 r2' s2 Just (c:cs ++ ds) + {- + - Recursive Parameters: + - If we are reasoning about two recursive parameters, check if their context references + - are equal + -} + RecPar n ctxt :< RecPar n' ctxt' -> guard (ctxt M.! n == ctxt M.! n') >> Just [] + RecPar n ctxt :=: RecPar n' ctxt' -> guard (ctxt M.! n == ctxt M.! n') >> Just [] + RecParBang n ctxt :< RecParBang n' ctxt' -> guard (ctxt M.! n == ctxt M.! n') >> Just [] + RecParBang n ctxt :=: RecParBang n' ctxt' -> guard (ctxt M.! n == ctxt M.! n') >> Just [] + + -- We need this here as otherwise it triggers the cases below + RecParBang n ctxt :< RecPar n' ctxt' -> Nothing + RecPar n ctxt :< RecParBang n' ctxt' -> Nothing + RecParBang n ctxt :=: RecPar n' ctxt' -> Nothing + RecPar n ctxt :=: RecParBang n' ctxt' -> Nothing + + {- + - otherwise: + - If we are reasoning about a recursive parameter and a type, unroll the parameter + - and reason about the type and the unrolled parameter + -} + RecPar n ctxt :< t -> Just [ unroll (RecPar n ctxt) :< t] + t :< RecPar n ctxt -> Just [t :< unroll (RecPar n ctxt)] + RecPar n ctxt :=: t -> Just [unroll (RecPar n ctxt) :=: t] + t :=: RecPar n ctxt -> Just [t :=: unroll (RecPar n ctxt)] + + RecParBang n ctxt :< t -> Just [Bang (unroll (RecPar n ctxt)) :< t] + t :< RecParBang n ctxt -> Just [t :< Bang (unroll (RecPar n ctxt))] + RecParBang n ctxt :=: t -> Just [Bang (unroll (RecPar n ctxt)) :=: t] + t :=: RecParBang n ctxt -> Just [t :=: Bang (unroll (RecPar n ctxt))] + t :< t' -> guard (unorderedType t || unorderedType t') >> Just [t :=: t'] AbsType n s ts :=: AbsType n' s' ts' -> guard (n == n' && s == s') >> Just (zipWith (:=:) ts ts') @@ -113,10 +151,10 @@ simplify axs = Rewrite.pickOne $ \c -> case c of c = Variant r1' :=: Variant r2' Just (c:cs) - Record r1 s1 :=: Record r2 s2 -> - if Row.null r1 && Row.null r2 && s1 == s2 then Just [] - else if Row.justVar r1 && Row.justVar r2 && s1 == s2 && r1 == r2 - then Just [Solved (Record r1 s1)] + Record n1 r1 s1 :=: Record n2 r2 s2 -> + if Row.null r1 && Row.null r2 && s1 == s2 && n1 == n2 then Just [] + else if Row.justVar r1 && Row.justVar r2 && s1 == s2 && r1 == r2 && n1 == n2 + then Just [Solved (Record n1 r1 s1)] else do let commons = Row.common r1 r2 (ls, rs) = unzip commons @@ -124,15 +162,22 @@ simplify axs = Rewrite.pickOne $ \c -> case c of guard (untakenLabels rs == untakenLabels ls) let (r1',r2') = Row.withoutCommon r1 r2 cs = map (\(Entry _ t _, Entry _ t' _) -> t :=: t') commons - c = Record r1' s1 :=: Record r2' s2 + c = Record n1 r1' s1 :=: Record n2 r2' s2 Just (c:cs) - + t :=: t' -> guard (t == t') >> if typeUVs t == [] then Just [] else Just [Solved t] Solved t -> guard (typeUVs t == []) >> Just [] + -- If an unboxed record has no recursive parameter, sat + UnboxedNoRecurse (Record None _ Unboxed) -> Just [] + -- If a boxed record, sat + UnboxedNoRecurse (Record _ _ c) | (c == ReadOnly || c == Writable) -> Just [] + _ -> Nothing + + where untakenLabels :: [Entry] -> S.Set FieldName diff --git a/minigent/src/Minigent/TC/SinkFloat.hs b/minigent/src/Minigent/TC/SinkFloat.hs index 4d6fcf69a..20ce1596b 100644 --- a/minigent/src/Minigent/TC/SinkFloat.hs +++ b/minigent/src/Minigent/TC/SinkFloat.hs @@ -29,6 +29,8 @@ import qualified Data.Map as M import Data.Semigroup (First(..)) +-- | The sinkFloat phase propagates the structure of types containing +-- rows (i.e. Records and Variants) through subtyping/equality constraints sinkFloat :: forall m. (MonadFresh VarName m, MonadWriter [Assign] m) => Rewrite.Rewrite' m [Constraint] sinkFloat = Rewrite.rewrite' $ \cs -> do (cs',as) <- tryEach cs @@ -51,19 +53,19 @@ sinkFloat = Rewrite.rewrite' $ \cs -> do genStructSubst (v :=: Bang t) = genStructSubst (v :=: t) -- records - genStructSubst (Record r s :< UnifVar i) = do + genStructSubst (Record n r s :< UnifVar i) = do s' <- case s of Unboxed -> return Unboxed -- unboxed is preserved by bang, so we may propagate it _ -> UnknownSigil <$> fresh - rowUnifRowSubs (flip Record s') i r + rowUnifRowSubs (flip (Record n) s') i r - genStructSubst (UnifVar i :< Record r s) = do + genStructSubst (UnifVar i :< Record n r s) = do s' <- case s of Unboxed -> return Unboxed -- unboxed is preserved by bang, so we may propagate it _ -> UnknownSigil <$> fresh - rowUnifRowSubs (flip Record s') i r + rowUnifRowSubs (flip (Record n) s') i r - genStructSubst (Record r1 s1 :< Record r2 s2) + genStructSubst (Record _ r1 s1 :< Record _ r2 s2) {- The most tricky case. Taken is the bottom of the order, Untaken is the top. diff --git a/minigent/src/Minigent/TC/Unify.hs b/minigent/src/Minigent/TC/Unify.hs index de658ffca..c58274e9f 100644 --- a/minigent/src/Minigent/TC/Unify.hs +++ b/minigent/src/Minigent/TC/Unify.hs @@ -25,30 +25,37 @@ import Control.Monad.Trans.Maybe import Control.Applicative import Data.Foldable (asum) +import Debug.Trace + +import Minigent.Syntax.PrettyPrint + -- | The unify phase, which seeks out equality constraints to solve via substitution. unify :: (MonadFresh VarName m, MonadWriter [Assign] m) => Rewrite.Rewrite' m [Constraint] unify = Rewrite.rewrite' $ \cs -> do a <- asum (map assignOf cs) tell a - pure (map (constraintTypes (traverseType (foldMap substAssign a))) cs) + --traceM ("About to perform the substitutions:\n" ++ "[\n" ++ debugAssigns a ++ "]") + pure (map (constraintTypes (normaliseType (foldMap substAssign a))) cs) assignOf :: (MonadFresh VarName m, MonadWriter [Assign] m) => Constraint -> MaybeT m [Assign] assignOf (UnifVar a :=: tau) | rigid tau && (a `notOccurs` tau) = pure [TyAssign a tau] assignOf (tau :=: UnifVar a) | rigid tau && (a `notOccurs` tau) = pure [TyAssign a tau] -assignOf (Record _ (UnknownSigil v) :=: Record _ s) +assignOf (Record _ _ (UnknownSigil v) :=: Record _ _ s) | s `elem` [ReadOnly, Unboxed, Writable] = pure [ SigilAssign v s ] -assignOf (Record _ s :=: Record _ (UnknownSigil v)) +assignOf (Record _ _ s :=: Record _ _ (UnknownSigil v)) | s `elem` [ReadOnly, Unboxed, Writable] = pure [ SigilAssign v s ] -assignOf (Record _ (UnknownSigil v) :< Record _ s) +assignOf (Record _ _ (UnknownSigil v) :< Record _ _ s) | s `elem` [ReadOnly, Unboxed, Writable] = pure [ SigilAssign v s ] -assignOf (Record _ s :< Record _ (UnknownSigil v)) +assignOf (Record _ _ s :< Record _ _ (UnknownSigil v)) | s `elem` [ReadOnly, Unboxed, Writable] = pure [ SigilAssign v s ] +assignOf (Record (UnknownParameter x) _ s :< Record _ _ Unboxed) + = pure [RecParAssign x None] -- N.B. we know from the previous phase that common alternatives have been factored out. assignOf (Variant r1 :=: Variant r2) | rowVar r1 /= rowVar r2 @@ -62,7 +69,7 @@ assignOf (Variant r1 :=: Variant r2) ] -- N.B. we know from the previous phase that common fields have been factored out. -assignOf (Record r1 s1 :=: Record r2 s2) +assignOf (Record _ r1 s1 :=: Record _ r2 s2) | rowVar r1 /= rowVar r2, s1 == s2 , [] <- Row.common r1 r2 = case (rowVar r1, rowVar r2) of @@ -72,8 +79,31 @@ assignOf (Record r1 s1 :=: Record r2 s2) pure [ RowAssign x (r2 { rowVar = Just v }) , RowAssign y (r1 { rowVar = Just v }) ] + +-- TODO: Generalise +assignOf (Record n1 _ _ :=: Record n2 _ _) + = case (n1,n2) of + (Rec _, UnknownParameter x) -> pure [RecParAssign x n1] + (UnknownParameter x, Rec _) -> pure [RecParAssign x n2] + (UnknownParameter x, None) -> pure [RecParAssign x None] + (None, UnknownParameter x) -> pure [RecParAssign x None] + _ -> empty + +assignOf (Record n1 _ _ :< Record n2 _ _) + = case (n1,n2) of + (Rec _, UnknownParameter x) -> pure [RecParAssign x n1] + (UnknownParameter x, Rec _) -> pure [RecParAssign x n2] + (UnknownParameter x, None) -> pure [RecParAssign x None] + (None, UnknownParameter x) -> pure [RecParAssign x None] + _ -> empty + +-- If it is discovered that a record is unboxed, we can assign it's +-- unknown parameter to None +assignOf (UnboxedNoRecurse (Record (UnknownParameter x) _ Unboxed)) + = pure [RecParAssign x None] + assignOf _ = empty notOccurs :: VarName -> Type -> Bool -notOccurs a tau = a `notElem` typeUVs tau +notOccurs a tau = a `notElem` typeUVs tau \ No newline at end of file diff --git a/minigent/test/Example.hs b/minigent/test/Example.hs index 9bceed8a5..9ab9f4eb7 100644 --- a/minigent/test/Example.hs +++ b/minigent/test/Example.hs @@ -25,7 +25,7 @@ rtrim s | Just (s', x) <- B.unsnoc s, isSpace x = rtrim s' updateExpected :: FilePath -> IO () updateExpected f = do phase <- loadConfig - let compile = CLI.compiler phase [CLI.Dump phase CLI.Stdout CLI.PrettyPlain] [f "in.minigent"] + let compile = CLI.compiler phase [CLI.Dump phase CLI.Stdout CLI.PrettyPlain, CLI.NoColour] [f "in.minigent"] (out', (err', _)) <- redirectStdout (redirectStderr (blockExceptions compile)) let out = trim out' err = trim err' @@ -49,7 +49,7 @@ updateExpected f = do example :: FilePath -> IO () example f = do phase <- loadConfig - let compile = CLI.compiler phase [CLI.Dump phase CLI.Stdout CLI.PrettyPlain] [f "in.minigent"] + let compile = CLI.compiler phase [CLI.Dump phase CLI.Stdout CLI.PrettyPlain, CLI.NoColour] [f "in.minigent"] (out', (err', _)) <- redirectStdout (redirectStderr (blockExceptions compile)) let out = trim out' err = trim err' From bb64874bc7d836433f85f9c00ad2b6946330fadb Mon Sep 17 00:00:00 2001 From: Emmet Murray Date: Thu, 12 Dec 2019 17:24:53 +1100 Subject: [PATCH 5/7] Changed sumlist to 'terminate', termination checker and ushow --- .../6_recursive/08-list-sum/in.minigent | 16 +++-- minigent/src/Minigent/CLI.hs | 1 + minigent/src/Minigent/Syntax.hs | 13 +++- minigent/src/Minigent/Syntax/PrettyPrint.hs | 31 +++++++++ minigent/src/Minigent/Termination.hs | 68 +++++++++++++------ 5 files changed, 103 insertions(+), 26 deletions(-) diff --git a/minigent/examples/6_recursive/08-list-sum/in.minigent b/minigent/examples/6_recursive/08-list-sum/in.minigent index f55d213b5..12c7a716b 100644 --- a/minigent/examples/6_recursive/08-list-sum/in.minigent +++ b/minigent/examples/6_recursive/08-list-sum/in.minigent @@ -1,10 +1,14 @@ sumList : mu t { l: < Nil Unit | Cons { data: U32, rest: t! }# >}! -> U32; sumList r = - case r.l of - Nil u -> 0 - | v2 -> - case v2 of - Cons s -> - s.data + sumList s.rest + take r2 { l = z } = r in + case z of + Nil u -> 0 + | v2 -> + case v2 of + Cons s -> + take s2 { rest = x } = s in + s.data + sumList x + end + end end end; \ No newline at end of file diff --git a/minigent/src/Minigent/CLI.hs b/minigent/src/Minigent/CLI.hs index acad857c0..06e791366 100644 --- a/minigent/src/Minigent/CLI.hs +++ b/minigent/src/Minigent/CLI.hs @@ -85,6 +85,7 @@ parsePhase "lexer" = pure Lex parsePhase "parse" = pure Parse parsePhase "reorg" = pure Reorg parsePhase "tc" = pure TC +parsePhase "term" = pure Term parsePhase "cg" = pure CG parsePhase _ = throwError "invalid phase" diff --git a/minigent/src/Minigent/Syntax.hs b/minigent/src/Minigent/Syntax.hs index f649b6d31..d97c67b7c 100644 --- a/minigent/src/Minigent/Syntax.hs +++ b/minigent/src/Minigent/Syntax.hs @@ -30,6 +30,8 @@ module Minigent.Syntax , -- * Constraints Constraint (..) , pattern (:>) + , -- * Assertions + Assertion (..) , -- * Expressions Expr (..) , Op (..) @@ -174,6 +176,15 @@ data Constraint | Unsat -- ^ Trivially false. deriving (Show, Eq) +infixr 0 :<: + +-- | Termination assertions used for detecting termination +data Assertion = + VarName :<: VarName -- ^ Structurally less than + | VarName :~: VarName -- ^ Structurally equal to + deriving (Eq, Ord, Show) + + pattern (:>) t1 t2 = t2 :< t1 -- | A polymorphic type, used for top-level bindings only. @@ -187,4 +198,4 @@ data PolyType = Forall [VarName] [Constraint] Type data RawTopLevel = TypeSig FunName PolyType -- ^ @f : t@ | Equation FunName VarName Expr -- ^ @f x = e@ - deriving (Show, Eq) + deriving (Show, Eq) \ No newline at end of file diff --git a/minigent/src/Minigent/Syntax/PrettyPrint.hs b/minigent/src/Minigent/Syntax/PrettyPrint.hs index 80b292cef..9588ab5fb 100644 --- a/minigent/src/Minigent/Syntax/PrettyPrint.hs +++ b/minigent/src/Minigent/Syntax/PrettyPrint.hs @@ -213,6 +213,9 @@ prettySimpleConstraint c = case c of prettyConstraint cs = vsep (punctuate (space <> annotate S.constraintKeyword ":&:") (map prettySimpleConstraint (flattenConstraint cs))) +prettyAssertion c = case c of + (a :<: b) -> pretty a <+> annotate S.constraintKeyword ":<:" <+> pretty b + (a :~: b) -> pretty a <+> annotate S.constraintKeyword ":~:" <+> pretty b prettyPolyType (Forall [] [] t) = prettyType t prettyPolyType (Forall ts c t) = align (sep [ list (map (prettyType . TypeVar) ts) @@ -236,6 +239,19 @@ debugAssigns newl s = s <> pretty (",\n" :: String) +debugPrettyAssertions + = T.unpack . renderStrict + . layoutPretty defaultLayoutOptions + . vcat . map prettyAssertion + +debugPrettyGoals + = T.unpack . renderStrict + . layoutPretty defaultLayoutOptions + . vcat . map (\x -> + case x of + Nothing -> pretty ("Nothing" :: String) + Just x' -> pretty (x' :: String) + ) debugPrettyType = T.unpack . renderStrict @@ -251,3 +267,18 @@ testPrettyToplevel = T.unpack . renderStrict . unAnnotateS . layoutPretty defaultLayoutOptions . prettyToplevel + +-- For debugging - a print/show combination that escape unicode characters. +-- Taken from https://stackoverflow.com/a/14461928 +uprint :: Show a => a -> IO () +uprint = putStrLn . ushow + +ushow :: Show a => a -> String +ushow x = con (show x) where + con :: String -> String + con [] = [] + con li@(x:xs) | x == '\"' = '\"':str++"\""++(con rest) + | x == '\'' = '\'':char:'\'':(con rest') + | otherwise = x:con xs where + (str,rest):_ = reads li + (char,rest'):_ = reads li \ No newline at end of file diff --git a/minigent/src/Minigent/Termination.hs b/minigent/src/Minigent/Termination.hs index 09cf4c43f..987f49a1d 100644 --- a/minigent/src/Minigent/Termination.hs +++ b/minigent/src/Minigent/Termination.hs @@ -16,12 +16,16 @@ import Minigent.Fresh import Minigent.Syntax import Minigent.Syntax.Utils import Minigent.Environment +import Minigent.Syntax.PrettyPrint import Control.Monad.State.Strict import Data.Maybe (maybeToList) import qualified Data.Map as M import qualified Data.Set as S +import Data.List + +import Debug.Trace -- A directed graph type Node = String @@ -31,19 +35,12 @@ type Graph = M.Map Node [Node] type FreshVar = String type Env = M.Map VarName FreshVar -infixr 0 :<: -data Assertion = - VarName :<: VarName -- ^ Structurally less than - | VarName :~: VarName -- ^ Structurally equal to - deriving (Eq, Ord, Show) - - termCheck :: GlobalEnvironments -> [String] termCheck genvs = M.foldrWithKey go [] (defns genvs) where go :: FunName -> (VarName, Expr) -> [String] -> [String] go f (x,e) errs = - if fst $ runFresh unifVars (init x e) then + if fst $ runFresh unifVars (init f x e) then errs else ("Error: Function " ++ f ++ " cannot be shown to terminate.") : errs @@ -51,18 +48,38 @@ termCheck genvs = M.foldrWithKey go [] (defns genvs) -- Maps the function argument to a name, then runs the termination -- assertion generator. -- Return true if the function terminates - init :: VarName -> Expr -> Fresh VarName Bool - init x e = do + init :: FunName -> VarName -> Expr -> Fresh VarName Bool + init f x e = do alpha <- fresh let env = M.insert x alpha M.empty (a,c) <- termAssertionGen env e + + -- If any goals are Nothing, we cannot proceed. + traceM "Goals:" + traceM $ debugPrettyGoals c + traceM "" + + traceM "Assertions:" + traceM $ debugPrettyAssertions a + traceM "" + let graph = toGraph a - return $ - all (\goal -> hasPathTo alpha goal graph && (not $ hasPathTo goal alpha graph)) c + let goals = noNothing c + + traceM $ ushow $ genDotFile f graph + return $ + -- If any goals are nothing, or our path condition is not met, then we cannot determine if the function terminates + length goals == length c && all (\goal -> hasPathTo alpha goal graph && (not $ hasPathTo goal alpha graph)) goals + noNothing :: [Maybe a] -> [a] + noNothing = foldr (\m l -> + case m of + Nothing -> l + Just x -> x:l + ) [] -termAssertionGen :: Env -> Expr -> Fresh VarName ([Assertion], [VarName]) +termAssertionGen :: Env -> Expr -> Fresh VarName ([Assertion], [Maybe FreshVar]) termAssertionGen env expr = case expr of PrimOp _ es -> @@ -74,8 +91,7 @@ termAssertionGen env expr Apply f e -> do a <- termAssertionGen env f b <- termAssertionGen env e - let c = getv env e - return $ flatten [([], maybeToList c), a, b] + return $ flatten [([], [getv env e]), a, b] Struct fs -> let es = map snd fs @@ -114,7 +130,7 @@ termAssertionGen env expr -- generate assertions let assertions = toAssertion env e1 (alpha :<:) - ++ toAssertion env e2 (beta :~:) + ++ toAssertion env e1 (beta :~:) return $ flatten [(assertions, []), res', res] @@ -184,14 +200,14 @@ termAssertionGen env expr Var v -> Just $ env M.! v _ -> Nothing - join :: [Fresh VarName ([Assertion], [FreshVar])] -> Fresh VarName ([Assertion], [FreshVar]) + join :: [Fresh VarName ([a], [b])] -> Fresh VarName ([a], [b]) join (e:es) = do (a,b) <- e (as,bs) <- join es return (a ++ as, b ++ bs) join [] = return ([],[]) - flatten :: [([Assertion], [FreshVar])] -> ([Assertion], [FreshVar]) + flatten :: [([a], [b])] -> ([a], [b]) flatten (x:xs) = let rest = flatten xs in (fst x ++ fst rest, snd x ++ snd rest) @@ -221,4 +237,18 @@ hasPathTo src dst g n == dst || (notElem n seen && hasPathTo' n d g (S.insert n seen)) - ) nbs \ No newline at end of file + ) nbs + + +-- To use: +-- run `dot -Tpdf graph.dot -o outfile.pdf` +-- where graph.dot is the output from this function. +genDotFile :: String -> Graph -> String +genDotFile name g = + "digraph " ++ name ++ " {\n" ++ intercalate "\n" (edges g) ++ "\n}" + where + pairs :: Graph -> [(Node,Node)] + pairs = concatMap (\(a, bs) -> map (\b -> (a,b)) bs) . M.assocs + + edges :: Graph -> [String] + edges = map (\(a,b) -> "\t" ++ a ++ " -> " ++ b ++ ";") . pairs \ No newline at end of file From b1893a4d95e140b6b7d0b9ab6511cca904b3d3e4 Mon Sep 17 00:00:00 2001 From: Emmet Murray Date: Fri, 13 Dec 2019 12:02:26 +1100 Subject: [PATCH 6/7] Debugging and graph generation support --- minigent/src/Minigent/CLI.hs | 58 ++++++++++++++++++++++------ minigent/src/Minigent/Termination.hs | 53 +++++++++++++------------ 2 files changed, 75 insertions(+), 36 deletions(-) diff --git a/minigent/src/Minigent/CLI.hs b/minigent/src/Minigent/CLI.hs index 06e791366..80394451f 100644 --- a/minigent/src/Minigent/CLI.hs +++ b/minigent/src/Minigent/CLI.hs @@ -40,31 +40,35 @@ import System.FilePath import System.Directory import qualified Data.Map as M import qualified Data.Text as T +import Data.List (intercalate) import Text.Earley import Data.Text.Prettyprint.Doc.Render.Terminal import Data.Text.Prettyprint.Doc (unAnnotateS, unAnnotate, defaultLayoutOptions, layoutPretty, vcat, (<+>), pretty) +import Debug.Trace + -- | The phases of the compiler, ordered in the order listed. -data Phase = Lex | Parse | Reorg | TC | Term | CG deriving (Ord, Enum, Eq) +data Phase = Lex | Parse | Reorg | TC | Term | CG deriving (Ord, Enum, Eq, Show) -- | The way a dump should be formatted when printed. data Format = PrettyColour -- ^ Print with a pretty printer and ANSI colours if printing to stdout | PrettyPlain -- ^ Print with a pretty printer and no colours | Raw -- ^ Print the raw abstract syntax tree (with 'Show') - deriving (Eq) + deriving (Eq, Show) -- | Where a dump should be output data Output = File FilePath | Stdout - deriving (Eq) + deriving (Eq, Show) -- | The various command line arguments of the compiler. data Directive = Dump Phase Output Format | NoColour - deriving (Eq) + | GenTermGraph FilePath + deriving (Eq, Show) singleToken :: MonadError String m => (String -> m a) -> [String] -> m ([String],a) @@ -110,6 +114,10 @@ parseDirectives ("--dump-stdout":rest) = do parseDirectives ("--no-colour":rest) = do (dirs, files) <- parseDirectives rest pure (NoColour:dirs, files) +parseDirectives ("--gen-term-graph":rest) = do + (rest', outFile) <- singleToken parseOutputFilePath rest + (dirs, files) <- parseDirectives rest' + pure ((GenTermGraph outFile):dirs, files) parseDirectives ("--dump":rest) = do (rest', phase) <- singleToken parsePhase rest (rest'', format) <- singleToken parseFormat rest' <|> pure (rest', PrettyPlain) @@ -141,6 +149,7 @@ printHelp = putStrLn $ unlines , " DIRECTIVES - one of: " , " --dump PHASE [FORMAT] FILE (writes the output of the given phase to the given file)" , " --dump-stdout PHASE [FORMAT] (writes the output of the given phase to stdout)" + , " --gen-term-graph FILE (generates a DOT graph for each function and writes them to the given file)" , "" , " FORMAT - one of: pretty, pretty-plain, raw" , " If not provided, --dump will use pretty-plain and --dump-stdout will use pretty" @@ -201,12 +210,14 @@ tcPhase colour envs pure [] go (Right b) = pure [b] -terminationPhase :: GlobalEnvironments -> IO () -terminationPhase envs - = case termCheck envs of - [] -> return () - xs -> -- Error - mapM_ (hPutStrLn stderr) xs +terminationPhase :: Bool -> GlobalEnvironments -> IO [(FunName, [Assertion], String)] +terminationPhase b envs + = let (errs, dumps) = termCheck envs in + case errs of + [] -> return dumps + xs -> do -- Error + mapM_ (hPutStrLn stderr) xs + return dumps cgPhase :: GlobalEnvironments -> IO String @@ -282,6 +293,29 @@ tcDump tops (Dump TC out fmt) = . prettyGlobalEnvs tcDump _ _ = return () +termDump :: [(FunName, [Assertion], String)] -> Directive -> IO () +termDump dumps (Dump Term out fmt) = do + write out $ intercalate "\n" $ map (\(f, as, _) -> "Function " ++ f ++ ":\n" ++ format fmt as) dumps + return () + where + write (File f) = writeFile f + write (Stdout) = putStrLn + + format Raw = ushow -- Necessary for showing unicode + format PrettyColour = T.unpack + . renderStrict + . layoutPretty defaultLayoutOptions + . vcat . map prettyAssertion + format PrettyPlain = T.unpack + . renderStrict + . unAnnotateS + . layoutPretty defaultLayoutOptions + . vcat . map prettyAssertion +termDump dumps (GenTermGraph f) = do + writeFile f $ intercalate "\n" $ map (\(_, _, g) -> g) dumps + return () +termDump _ _ = return () + cgDump :: String -> Directive -> IO () cgDump s (Dump CG out fmt) = write out s where @@ -295,6 +329,7 @@ cgDump _ _ = mempty compiler :: Phase -> [Directive] -> [FilePath] -> IO () compiler phase dirs [] = die "no input files given" compiler phase dirs files = do + traceM $ show dirs input <- unlines <$> mapM readFile files upTo Lex toks <- lexerPhase input @@ -309,7 +344,8 @@ compiler phase dirs files = do binds <- tcPhase (NoColour `notElem` dirs) envs mapM_ (tcDump binds) dirs upTo Term - _ <- terminationPhase envs + funDumps <- terminationPhase False envs + mapM_ (termDump funDumps) dirs upTo CG barf <- cgPhase binds mapM_ (cgDump barf) dirs diff --git a/minigent/src/Minigent/Termination.hs b/minigent/src/Minigent/Termination.hs index 987f49a1d..a621759b6 100644 --- a/minigent/src/Minigent/Termination.hs +++ b/minigent/src/Minigent/Termination.hs @@ -10,7 +10,10 @@ -- -- May be used qualified or unqualified. module Minigent.Termination - ( termCheck ) where + ( termCheck + , genGraphDotFile + , Assertion (..) + ) where import Minigent.Fresh import Minigent.Syntax @@ -35,42 +38,42 @@ type Graph = M.Map Node [Node] type FreshVar = String type Env = M.Map VarName FreshVar -termCheck :: GlobalEnvironments -> [String] -termCheck genvs = M.foldrWithKey go [] (defns genvs) +termCheck :: GlobalEnvironments -> ([String], [(FunName, [Assertion], String)]) +termCheck genvs = M.foldrWithKey go ([],[]) (defns genvs) where - go :: FunName -> (VarName, Expr) -> [String] -> [String] - go f (x,e) errs = - if fst $ runFresh unifVars (init f x e) then - errs - else - ("Error: Function " ++ f ++ " cannot be shown to terminate.") : errs + go :: FunName -> (VarName, Expr) -> ([String], [(FunName, [Assertion], String)]) -> ([String], [(FunName, [Assertion], String)]) + go f (x,e) (errs, dumps) = + let (pass, g, d) = fst $ runFresh unifVars (init f x e) + er = if pass then + errs + else + ("Error: Function " ++ f ++ " cannot be shown to terminate.") : errs + in + (er, (f, g, d):dumps) -- Maps the function argument to a name, then runs the termination -- assertion generator. -- Return true if the function terminates - init :: FunName -> VarName -> Expr -> Fresh VarName Bool + init :: FunName -> VarName -> Expr -> Fresh VarName (Bool, [Assertion], String) init f x e = do alpha <- fresh let env = M.insert x alpha M.empty (a,c) <- termAssertionGen env e - -- If any goals are Nothing, we cannot proceed. - traceM "Goals:" - traceM $ debugPrettyGoals c - traceM "" - - traceM "Assertions:" - traceM $ debugPrettyAssertions a - traceM "" - let graph = toGraph a let goals = noNothing c - - traceM $ ushow $ genDotFile f graph + -- If any goals are nothing, or our path condition is not met, then we cannot determine if the function terminates + let terminates = length goals == length c + && all (\goal -> hasPathTo alpha goal graph + && (not $ hasPathTo goal alpha graph) + ) goals return $ - -- If any goals are nothing, or our path condition is not met, then we cannot determine if the function terminates - length goals == length c && all (\goal -> hasPathTo alpha goal graph && (not $ hasPathTo goal alpha graph)) goals + ( + terminates, + a, + genGraphDotFile f graph + ) noNothing :: [Maybe a] -> [a] noNothing = foldr (\m l -> @@ -243,8 +246,8 @@ hasPathTo src dst g -- To use: -- run `dot -Tpdf graph.dot -o outfile.pdf` -- where graph.dot is the output from this function. -genDotFile :: String -> Graph -> String -genDotFile name g = +genGraphDotFile :: String -> Graph -> String +genGraphDotFile name g = "digraph " ++ name ++ " {\n" ++ intercalate "\n" (edges g) ++ "\n}" where pairs :: Graph -> [(Node,Node)] From 145f0c6233014cb656c78b6717ee8d9c511cf443 Mon Sep 17 00:00:00 2001 From: Emmet Murray Date: Tue, 17 Dec 2019 11:22:16 +1100 Subject: [PATCH 7/7] minigent: update example test files --- .../6_recursive/08-list-sum/expected.out | 38 ++++++++++--------- minigent/src/Minigent/CLI.hs | 1 - 2 files changed, 20 insertions(+), 19 deletions(-) diff --git a/minigent/examples/6_recursive/08-list-sum/expected.out b/minigent/examples/6_recursive/08-list-sum/expected.out index 990385ace..a33e16bc3 100644 --- a/minigent/examples/6_recursive/08-list-sum/expected.out +++ b/minigent/examples/6_recursive/08-list-sum/expected.out @@ -1,20 +1,22 @@ sumList : mu t {l : }! -> U32; -sumList r = case (r : mu t {l : }!).l : of - Nil u -> 0 : U32 - | v2 -> case v2 : of - Cons s -> ((s : {data : U32 - ,rest : rec t!}#).data : U32) + ((sumList[ ] : mu t {l : }! - -> U32) ((s : {data : U32 - ,rest : mu t {l : }!}#).rest : mu t {l : }!) : U32) : U32 - end : U32 +sumList r = take r2 { l = z } = r : mu t {l : }! + in case z : of + Nil u -> 0 : U32 + | v2 -> case v2 : of + Cons s -> take s2 { rest = x } = s : {data : U32 + ,rest : mu t {l : }!}# + in ((s : {data : U32 + ,rest : rec t!}#).data : U32) + ((sumList[ ] : mu t {l : }! + -> U32) (x : mu t {l : }!) : U32) : U32 + end : U32 + end : U32 + end : U32 end : U32; \ No newline at end of file diff --git a/minigent/src/Minigent/CLI.hs b/minigent/src/Minigent/CLI.hs index 80394451f..52f8f8396 100644 --- a/minigent/src/Minigent/CLI.hs +++ b/minigent/src/Minigent/CLI.hs @@ -329,7 +329,6 @@ cgDump _ _ = mempty compiler :: Phase -> [Directive] -> [FilePath] -> IO () compiler phase dirs [] = die "no input files given" compiler phase dirs files = do - traceM $ show dirs input <- unlines <$> mapM readFile files upTo Lex toks <- lexerPhase input