mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-23 16:28:02 +03:00
refactor towards adding typechecking tests having data declarations
This commit is contained in:
parent
8152bcd329
commit
bfd05da1ba
@ -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 <in-file.u> <out-file.ub>"
|
||||
|
||||
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
|
||||
|
@ -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) <-
|
||||
|
53
parser-typechecker/src/Unison/FileParsers.hs
Normal file
53
parser-typechecker/src/Unison/FileParsers.hs
Normal file
@ -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
|
@ -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)
|
||||
|
@ -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
|
||||
|
@ -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)
|
||||
|
@ -39,6 +39,7 @@ library
|
||||
Unison.Codecs
|
||||
Unison.DataDeclaration
|
||||
Unison.FileParser
|
||||
Unison.FileParsers
|
||||
Unison.Hash
|
||||
Unison.Hashable
|
||||
Unison.Kind
|
||||
|
Loading…
Reference in New Issue
Block a user