From bfd05da1ba31a3a2191374130e588c4bc6327058 Mon Sep 17 00:00:00 2001 From: Arya Irani Date: Thu, 14 Jun 2018 13:31:36 -0400 Subject: [PATCH] refactor towards adding typechecking tests having data declarations --- parser-typechecker/bootstrap/Bootstrap.hs | 32 ++++------- parser-typechecker/src/Unison/Builtin.hs | 10 ++-- parser-typechecker/src/Unison/FileParsers.hs | 53 +++++++++++++++++++ parser-typechecker/src/Unison/Note.hs | 1 + .../tests/Unison/Test/Common.hs | 17 +++++- .../tests/Unison/Test/Typechecker.hs | 25 +++++++++ .../unison-parser-typechecker.cabal | 1 + 7 files changed, 113 insertions(+), 26 deletions(-) create mode 100644 parser-typechecker/src/Unison/FileParsers.hs diff --git a/parser-typechecker/bootstrap/Bootstrap.hs b/parser-typechecker/bootstrap/Bootstrap.hs index cfc306409..1c49bbffd 100644 --- a/parser-typechecker/bootstrap/Bootstrap.hs +++ b/parser-typechecker/bootstrap/Bootstrap.hs @@ -9,6 +9,7 @@ import Data.Foldable (toList) import Data.Maybe (fromMaybe) import Control.Monad.State (evalStateT) import qualified Unison.Builtin as B +import qualified Unison.FileParsers as FileParsers import qualified Unison.Parser as Parser import qualified Unison.Parsers as Parsers import qualified Unison.Term as Term @@ -23,7 +24,10 @@ import qualified Unison.Note as Note import Unison.Note (Noted) import Unison.Reference (Reference) import Unison.Symbol (Symbol) +import Unison.Term (Term) import Unison.Type (Type) +import Unison.UnisonFile (UnisonFile) +import Unison.Var (Var) import Debug.Trace (trace) main :: IO () @@ -32,26 +36,12 @@ main = do case args of [sourceFile, outputFile] -> do unisonFile <- Parsers.unsafeReadAndParseFile Parser.penv0 sourceFile - let dataDecls = Map.fromList . toList $ UF.dataDeclarations unisonFile - -- let t = B.resolveBuiltins B.builtinTerms Term.builtin $ UF.term unisonFile - let t = Term.bindBuiltins B.builtinTerms B.builtinTypes $ UF.term unisonFile - typ <- Note.run $ Typechecker.synthesize termLookup (dataDeclLookup dataDecls) t - putStrLn ("typechecked as " ++ show typ) - let bs = runPutS $ flip evalStateT 0 $ Codecs.serializeFile unisonFile - BS.writeFile outputFile bs + let (t, typeNote) = FileParsers.synthesizeFile unisonFile + case typeNote of + Left e -> putStrLn $ show e + Right typ -> do + putStrLn ("typechecked as " ++ show typ) + let bs = runPutS $ flip evalStateT 0 $ Codecs.serializeFile unisonFile + BS.writeFile outputFile bs _ -> putStrLn "usage: bootstrap " - -termLookup :: Applicative f => Reference -> Noted f (Type Symbol) -termLookup h = fromMaybe (missing h) (pure <$> Map.lookup h B.builtins) - -dataDeclLookup :: Applicative f - => Map Reference (DataDeclaration Symbol) - -> Reference - -> Noted f (DataDeclaration Symbol) -dataDeclLookup dataDecls h = - let _ = trace $ "dataDeclLookup: " ++ show h in - fromMaybe (missingD h) (pure <$> Map.lookup h dataDecls) - -missing h = Note.failure $ "no match looking up type of term reference: " ++ show h -missingD h = Note.failure $ "no match looking up type of data declaration reference: " ++ show h diff --git a/parser-typechecker/src/Unison/Builtin.hs b/parser-typechecker/src/Unison/Builtin.hs index 071f61c1c..d31999926 100644 --- a/parser-typechecker/src/Unison/Builtin.hs +++ b/parser-typechecker/src/Unison/Builtin.hs @@ -1,4 +1,7 @@ {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ExplicitForAll #-} module Unison.Builtin where import Control.Arrow ((&&&)) @@ -6,7 +9,6 @@ import qualified Data.Map as Map import qualified Unison.Parser as Parser import qualified Unison.Parsers as Parsers -- remove this dependency on Parsers import qualified Unison.Reference as R -import Unison.Symbol (Symbol) import Unison.Term (Term) import qualified Unison.Term as Term import Unison.Type (Type) @@ -30,8 +32,8 @@ bindBuiltins = Term.bindBuiltins builtinTerms builtinTypes bindTypeBuiltins :: Var v => Type v -> Type v bindTypeBuiltins = Type.bindBuiltins builtinTypes -builtinTerms :: Var v => [(v, Term v)] -builtinTerms = (toSymbol &&& Term.ref) <$> Map.keys builtins +builtinTerms :: forall v. Var v => [(v, Term v)] +builtinTerms = (toSymbol &&& Term.ref) <$> Map.keys (builtins @v) builtinTypes :: Var v => [(v, Type v)] builtinTypes = (Var.named &&& (Type.ref . R.Builtin)) <$> @@ -41,7 +43,7 @@ toSymbol :: Var v => R.Reference -> v toSymbol (R.Builtin txt) = Var.named txt toSymbol _ = error "unpossible" -builtins :: Map.Map R.Reference (Type Symbol) +builtins :: Var v => Map.Map R.Reference (Type v) builtins = Map.fromList $ [ (R.Builtin name, t typ) | (name, typ) <- diff --git a/parser-typechecker/src/Unison/FileParsers.hs b/parser-typechecker/src/Unison/FileParsers.hs new file mode 100644 index 000000000..a3b06bff4 --- /dev/null +++ b/parser-typechecker/src/Unison/FileParsers.hs @@ -0,0 +1,53 @@ +{-# Language OverloadedStrings #-} +module Unison.FileParsers where + +import Data.Map (Map) +import Data.Functor.Identity (runIdentity) +import qualified Data.Foldable as Foldable +import qualified Data.Map as Map +import qualified Data.Maybe as Maybe +import qualified Debug.Trace as Trace +import qualified Unison.Builtin as B +import qualified Unison.Note as Note +import qualified Unison.Parser as Parser +import qualified Unison.Parsers as Parsers +import qualified Unison.Term as Term +import qualified Unison.Typechecker as Typechecker +import qualified Unison.UnisonFile as UF +import Unison.DataDeclaration (DataDeclaration) +import Unison.Note (Noted) +import Unison.Reference (Reference) +import Unison.Term (Term) +import Unison.Type (Type) +import Unison.UnisonFile (UnisonFile) +import Unison.Var (Var) + +parseAndSynthesizeAsFile :: Var v => FilePath -> String + -> (Term v, Either String (Type v)) +parseAndSynthesizeAsFile filename s = + synthesizeFile . Parsers.unsafeGetRight $ + Parsers.parseFile filename s Parser.penv0 + +synthesizeFile :: Var v => UnisonFile v -> (Term v, Either String (Type v)) +synthesizeFile unisonFile = + let dataDecls = Map.fromList . Foldable.toList $ UF.dataDeclarations unisonFile + t = Term.bindBuiltins B.builtinTerms B.builtinTypes $ UF.term unisonFile + n = Note.attemptRun $ Typechecker.synthesize termLookup (dataDeclLookup dataDecls) t + in (t, runIdentity n) + +termLookup :: (Applicative f, Var v) => Reference -> Noted f (Type v) +termLookup h = Maybe.fromMaybe (missing h) (pure <$> Map.lookup h B.builtins) + +dataDeclLookup :: Applicative f + => Map Reference (DataDeclaration v) + -> Reference + -> Noted f (DataDeclaration v) +dataDeclLookup dataDecls h = + let _ = Trace.trace $ "dataDeclLookup: " ++ show h in + Maybe.fromMaybe (missingD h) (pure <$> Map.lookup h dataDecls) + +missing :: (Applicative m, Show a) => a -> Noted m b +missing h = Note.failure $ "no match looking up type of term reference: " ++ show h + +missingD :: (Applicative m, Show a) => a -> Noted m b +missingD h = Note.failure $ "no match looking up type of data declaration reference: " ++ show h diff --git a/parser-typechecker/src/Unison/Note.hs b/parser-typechecker/src/Unison/Note.hs index f418c5525..d76034000 100644 --- a/parser-typechecker/src/Unison/Note.hs +++ b/parser-typechecker/src/Unison/Note.hs @@ -10,6 +10,7 @@ newtype Note = Note [String] -- | Monad transformer for adding notes newtype Noted m a = Noted { unnote :: m (Either Note a) } +-- todo: don't use this; it's broken. -Arya & Runar run :: Monad m => Noted m a -> m a run (Noted m) = m >>= \e -> case e of Left (Note stack) -> fail ("\n" ++ intercalate "\n" stack) diff --git a/parser-typechecker/tests/Unison/Test/Common.hs b/parser-typechecker/tests/Unison/Test/Common.hs index 0c1adf50d..aad8b4634 100644 --- a/parser-typechecker/tests/Unison/Test/Common.hs +++ b/parser-typechecker/tests/Unison/Test/Common.hs @@ -3,6 +3,9 @@ module Unison.Test.Common where import Unison.Term (Term) import Unison.Type (Type) import Unison.Symbol (Symbol) +import Unison.FileParsers (parseAndSynthesizeAsFile) +import Control.Arrow (second) +import Data.Maybe (isJust) import qualified Data.Map as Map import qualified Unison.Builtin as B import qualified Unison.Note as N @@ -11,11 +14,20 @@ import qualified Unison.Typechecker as Typechecker tm :: String -> Term Symbol tm = B.tm +file :: String -> (Term Symbol, Either String (Type Symbol)) +file = parseAndSynthesizeAsFile "" + +fileTerm :: String -> Term Symbol +fileTerm = fst . parseAndSynthesizeAsFile "" + +fileTermType :: String -> (Term Symbol, Maybe (Type Symbol)) +fileTermType = second (either (const Nothing) Just) . parseAndSynthesizeAsFile "" + t :: String -> Type Symbol t = B.t typechecks :: String -> Bool -typechecks = typechecks' . tm +typechecks = typechecks' . fst . file typechecks' :: Term Symbol -> Bool typechecks' term = let @@ -26,6 +38,9 @@ typechecks' term = let Left _e -> False Right _ -> True +fileTypeChecks :: String -> Bool +fileTypeChecks = isJust . snd . fileTermType + check' :: Term Symbol -> Type Symbol -> Bool check' term typ = let typeOf r = maybe (fail $ "no type for: " ++ show r) pure $ Map.lookup r B.builtins diff --git a/parser-typechecker/tests/Unison/Test/Typechecker.hs b/parser-typechecker/tests/Unison/Test/Typechecker.hs index de2258c13..1749b68c8 100644 --- a/parser-typechecker/tests/Unison/Test/Typechecker.hs +++ b/parser-typechecker/tests/Unison/Test/Typechecker.hs @@ -50,5 +50,30 @@ test = scope "typechecker" . tests $ |> Stream.take 10 |> Stream.fold-left +0 (+_Int64) |] "Int64" + -- some pattern-matching tests we want to perform: +-- Unbound + -- , c [r|type Optional a = None | Some a + -- case Some 3 of + -- x -> 1 + -- |] "UInt64" + -- , f [r|type Optional a = None | Some a + -- case Some 3 of + -- x -> 1 + -- y -> "boo" + -- |] +-- Var +-- Boolean !Bool +-- Int64 !Int64 +-- UInt64 !Word64 +-- Float !Double +-- Constructor !Reference !Int [Pattern] +-- As Pattern +-- nested ones +-- multiple cases +-- guards + +-- EffectPure Pattern +-- EffectBind !Reference !Int [Pattern] Pattern-- ] where c tm typ = scope tm $ expect $ check tm typ + -- f s = scope s (expect . not . check . fileTypeChecks $ s) diff --git a/parser-typechecker/unison-parser-typechecker.cabal b/parser-typechecker/unison-parser-typechecker.cabal index 7f5b3047b..de9f96bd0 100644 --- a/parser-typechecker/unison-parser-typechecker.cabal +++ b/parser-typechecker/unison-parser-typechecker.cabal @@ -39,6 +39,7 @@ library Unison.Codecs Unison.DataDeclaration Unison.FileParser + Unison.FileParsers Unison.Hash Unison.Hashable Unison.Kind