diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,14 @@ # Change Log +## 0.1.2.0 + +- added type synonyms +- let bindings can now be annotated with types +- support field renaming during record matches +- added a text append primitive +- added a list uncons primitive +- added example List and Text library modules + ## 0.1.1.0 - API convenience functions for building record/variant HasValue instances. diff --git a/Prelude.x b/Prelude.x deleted file mode 100644 --- a/Prelude.x +++ /dev/null @@ -1,108 +0,0 @@ --- --- Expresso Prelude --- -let - - id = x -> x; - const = x y -> x; - flip = f x y -> (f y x); - - ---------------------------------------------------------------- - -- List operations - - map = f -> foldr (x xs -> f x :: xs) []; - filter = f -> foldr (x xs -> if f x then (x::xs) else xs); - length = foldr (const (n -> 1 + n)) 0; - foldl = f z xs -> foldr (x xsf r -> xsf (f r x)) id xs z; - reverse = foldl (xs x -> x :: xs) []; - concat = xss -> foldr (xs ys -> xs ++ ys) [] xss; - intersperse = sep xs -> - let f = x xs -> (if null xs then [x] else x :: sep :: xs) - in foldr f [] xs; - intercalate = xs xss -> concat (intersperse xs xss); - - ---------------------------------------------------------------- - -- Maybe operations - smart constructors create closed variants - - just = x -> Just x - : forall a. a -> ; - - nothing = Nothing{} - : forall a. ; - - maybe = b f m -> case m of { Just a -> f a, Nothing{} -> b } - : forall a b. b -> (a -> b) -> -> b; - - isJust = maybe False (const True); - isNothing = maybe True (const False); - fromMaybe = x -> maybe x id; - listToMaybe = foldr (x -> const (just x)) nothing; - maybeToList = maybe [] (x -> [x]); - catMaybes = xs -> concat (map maybeToList xs); - mapMaybe = f -> maybe nothing (just << f); - - ---------------------------------------------------------------- - -- Either operations - smart constructors create closed variants - - left = x -> Left x - : forall a b. a -> ; - - right = x -> Right x - : forall a b. b -> ; - - either = f g m -> case m of { Left a -> f a, Right b -> g b } - : forall a b c. (a -> c) -> (b -> c) -> -> c; - - ---------------------------------------------------------------- - -- Logical operations - - and = foldr (x y -> x && y) True; - or = foldr (x y -> x || y) False; - any = p -> or << map p; - all = p -> and << map p; - - elem = x -> any (x' -> x' == x); - notElem = x -> all (x' -> x' /= x); - - ---------------------------------------------------------------- - -- Dynamic binding - - withOverride = overrides f self -> overrides (f self); - mkOverridable = f -> { override_ = overrides -> (withOverride overrides f) | fix f}; - - override = r overrides -> mkOverridable (r.override_ overrides) - - --- Exports -in { id - , const - , map - , filter - , length - , foldl - , reverse - , concat - , intercalate - , intersperse - , just - , nothing - , maybe - , isJust - , isNothing - , fromMaybe - , listToMaybe - , maybeToList - , catMaybes - , mapMaybe - , left - , right - , either - , and - , or - , any - , all - , elem - , notElem - , mkOverridable - , override - } diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -15,9 +15,9 @@ - Structural typing with extensible records and variants - Lazy evaluation - Convenient use from Haskell (a type class for marshalling values) -- Haskell-inspired syntax +- Whitespace insensitive syntax - Type annotations to support first-class modules and schema validation use cases -- Built-in support for ints, double, bools, chars, maybes and lists +- Built-in support for ints, double, bools, chars and lists ## Installation @@ -97,6 +97,10 @@ λ> let sqmag = r -> r.x*r.x + r.y*r.y +When matching on record arguments, sometimes it can be necessary to supply a new name to bind the values of a field to, for example: + + λ> let add = {x=r, y=s} {x=u, y=v} -> {x = r + u, y = s + v} + ### Record restriction We can remove a field by using the restriction primitive `\`. For example, the following will type-check: @@ -135,21 +139,21 @@ Records with polymorphic functions can be passed as lambda arguments and remain polymorphic using *higher-rank polymorphism*. To accomplish this, we must provide Expresso with a suitable type annotation of the argument. For example: let f = (m : forall a. { reverse : [a] -> [a] |_}) -> - {l = m.reverse [True, False], r = m.reverse "abc" } + {l = m.reverse [True, False], r = m.reverse [1,2,3] } The function `f` above takes a "module" `m` containing a polymorphic function `reverse`. We annotate `m` with a type by using a single colon `:` followed by the type we are expecting. Note the underscore `_` in the tail of the record. This is a *type wildcard*, meaning we have specified a *partial type signature*. This type wildcard allows us to pass an arbitrary module containing a `reverse` function with this signature. To see the full type signature of `f`, we can use the Expresso REPL: λ> :t f forall r. (r\reverse) => (forall a. {reverse : [a] -> [a] | r}) -> - {l : [Bool], r : [Char]} + {l : [Bool], r : [Int]} Note that the `r`, representing the rest of the module fields, is a top-level quantifier. The type wildcard is especially useful here, as it allows us to avoid creating a top-level signature for the entire function and explicitly naming this row variable. More generally, type wildcards allow us to leave parts of a type signature unspecified. Function `f` can now of course be applied to any module satisfying the type signature: - λ> f (import "Prelude.x") - {l = [False, True], r = "cba"} + λ> f (import "List.x") + {l = [False, True], r = [3,2,1]} ### Difference records and concatenation @@ -207,12 +211,17 @@ We will often need to create closed variant types. For example, we may want to create a structural type analogous to Haskell's `Maybe a`, having only two constructors: `Nothing` and `Just`. This can be accomplished using smart constructors with type annotations. In the Prelude, we define the equivalent constructors `just` and `nothing`, as well as a fold `maybe` over this closed set: - just = x -> Just x : forall a. a -> ; + type Maybe a = ; - nothing = Nothing{} : forall a. ; + just : forall a. a -> Maybe a + = x -> Just x; + nothing : forall a. Maybe a + = Nothing{}; + maybe = b f m -> case m of { Just a -> f a, Nothing{} -> b } +Note that we declare and use a type synonym `Maybe a` to avoid repeating the type ``. Type synonyms can be included at the top of any file and have global scope. ### Variant embedding @@ -258,7 +267,7 @@ A simple type annotation ` : ` , will not suffice for "schema validation". For example, consider this attempt at validating an integer against a schema that permits everything: - 1 : forall a. a -- FAILS + 1 : forall a. a -- DOES NOT TYPE CHECK! The above fails to type check since the left-hand-side is inferred as the most general type (here a concrete int) and the right-hand-side must be less so. @@ -293,7 +302,7 @@ Turing equivalence is introduced via a single `fix` primitive, which can be easily removed or disabled. `fix` can be useful to achieve open recursive records and dynamic binding (à la Nix). - λ> let r = mkOverridable (self -> {x = "foo", y = self.x ++ "bar"}) + λ> let r = mkOverridable (self -> {x = "foo", y = self.x <> "bar"}) λ> r {override_ = , x = "foo", y = "foobar"} @@ -307,7 +316,7 @@ Expresso can be used as a typed configuration file format from within Haskell programs. As an example, let's consider a hypothetical small config file for a backup program: let awsTemplate = - { location ="s3://s3-eu-west-2.amazonaws.com/atavachron-backup" + { location ="s3://s3-eu-west-1.amazonaws.com/tim-backup" , include = [] , exclude = [] } @@ -315,8 +324,14 @@ { cachePath = Default{} , taskThreads = Override 2 , profiles = - [ { name = "pictures", source = "~/Pictures" | awsTemplate } - , { name = "music", source = "~/Music", exclude := ["**/*.m4a"] | awsTemplate } + [ { name = "pictures" + , source = "~/Pictures" + | awsTemplate + } + , { name = "music" + , source = "~/Music" + , exclude := ["**/*.m4a"] + | awsTemplate } ] } diff --git a/expresso.cabal b/expresso.cabal --- a/expresso.cabal +++ b/expresso.cabal @@ -1,5 +1,5 @@ Name: expresso -Version: 0.1.1.0 +Version: 0.1.2.0 Cabal-Version: >= 1.10 License: BSD3 License-File: LICENSE @@ -16,8 +16,13 @@ Please refer to README.md for more information. Build-Type: Simple Bug-Reports: https://github.com/willtim/Expresso/issues -Extra-Source-Files: +Data-Files: Prelude.x + List.x + Text.x +Data-Dir: + lib +Extra-Source-Files: CHANGELOG.md README.md @@ -25,11 +30,6 @@ Type: git Location: https://github.com/willtim/Expresso -Flag terminfo - Description: On POSIX systems, build with the terminfo lib for detecting terminal width. - Manual: False - Default: True - Library Hs-Source-Dirs: src Default-Language: Haskell2010 @@ -45,8 +45,6 @@ template-haskell >= 2.13.0 && < 2.15, unordered-containers >= 0.2.9 && < 0.3, wl-pprint >= 1.2.1 && < 1.3 - if (!(os(windows))) && (flag(terminfo)) - Build-Depends: terminfo >= 0.4 && < 0.5 Exposed-Modules: Expresso Expresso.TH.QQ @@ -70,8 +68,6 @@ Default-Language: Haskell2010 Build-Depends: base, containers, hashable, mtl, parsec, wl-pprint, text, unordered-containers, haskeline, directory, filepath - if (!(os(windows))) && (flag(terminfo)) - Build-Depends: terminfo Other-Modules: Expresso.Parser Expresso.Eval @@ -81,6 +77,7 @@ Expresso.Pretty Expresso.Utils Expresso + Paths_expresso ghc-options: -threaded -rtsopts -Wall -fwarn-tabs -funbox-strict-fields -fno-warn-orphans @@ -97,8 +94,6 @@ Build-Depends: base, containers, hashable, mtl, parsec, wl-pprint, text, unordered-containers, haskeline, directory, filepath, expresso, tasty, tasty-hunit - if (!(os(windows))) && (flag(terminfo)) - Build-Depends: terminfo Other-Modules: Expresso Expresso.Eval @@ -108,3 +103,4 @@ Expresso.Type Expresso.TypeCheck Expresso.Utils + Paths_expresso diff --git a/lib/List.x b/lib/List.x new file mode 100644 --- /dev/null +++ b/lib/List.x @@ -0,0 +1,145 @@ +-- +-- Expresso additional List operations +-- +let + + {..} = import "Prelude.x"; + + reverse + : forall a. [a] -> [a] + = foldl (xs x -> x :: xs) []; + + tails + : forall a. [a] -> [[a]] + = fix (r xs -> + case uncons xs of + { Nothing{} -> [[]] + , Just{tail=xs'} -> xs :: r xs' + }); + + intersperse + : forall a. a -> [a] -> [a] + = sep xs -> + let f = x xs -> (if null xs then [x] else x :: sep :: xs) + in foldr f [] xs; + + intercalate + : forall a. [a] -> [[a]] -> [a] + = xs xss -> concat (intersperse xs xss); + + dropWhile + : forall a. (a -> Bool) -> [a] -> [a] + = p -> xs -> foldr (x r b -> + if b && p x then r True else x::r False) (const []) xs True; + + dropWhileEnd + : forall a. (a -> Bool) -> [a] -> [a] + = p -> foldr (x xs -> if null xs && p x then [] else x :: xs) []; + + takeWhile + : forall a. (a -> Bool) -> [a] -> [a] + = p -> foldr (x xs -> if p x then x :: xs else []) []; + + takeWhileEnd + : forall a. (a -> Bool) -> [a] -> [a] + = p -> reverse << takeWhile p << reverse; + + isPrefixOf + : forall a. Eq a => [a] -> [a] -> Bool + = fix (r xs ys -> + case uncons xs of + { Nothing{} -> True + , Just {head=x, tail=xs'} -> + case uncons ys of + { Nothing{} -> False + , Just {head=y, tail=ys'} -> + x==y && r xs' ys' + } + }); + + isSuffixOf + : forall a. Eq a => [a] -> [a] -> Bool + = xs ys -> isPrefixOf (reverse xs) (reverse ys); + + stripPrefix + : forall a. Eq a => [a] -> [a] -> Maybe [a] + = fix (r xs ys -> + case uncons xs of + { Nothing{} -> Just ys + , Just{head=x,tail=xs'} -> + case uncons ys of + { Nothing{} -> Nothing{} + , Just {head=y, tail=ys'} -> + if x==y then r xs' ys' else Nothing{} + } + }); + + stripSuffix + : forall a. Eq a => [a] -> [a] -> Maybe [a] + = xs ys -> stripPrefix (reverse xs) (reverse ys); + + dropPrefix + : forall a. Eq a => [a] -> [a] -> [a] + = xs ys -> fromMaybe ys (stripPrefix xs ys); + + dropSuffix + : forall a. Eq a => [a] -> [a] -> [a] + = xs ys -> fromMaybe ys (stripSuffix xs ys); + + zipWith + : forall a b c. (a -> b -> c) -> [a] -> [b] -> [c] + = f -> fix (r xs ys -> + case uncons xs of + { Nothing{} -> [] + , Just{head=x,tail=xs'} -> + case uncons ys of + { Nothing{} -> [] + , Just {head=y, tail=ys'} -> + f x y :: r xs' ys' + } + }); + + zip : forall a b. [a] -> [b] -> [{l:a, r:b}] + = zipWith (a b -> { l = a, r = b }); + + + replace + : forall a. Eq a => [a] -> [a] -> [a] -> [a] + = fix (r from to xs -> + if null from then xs + else case stripPrefix from xs of + { Just xs' -> to ++ r from to xs' + , Nothing{} -> case uncons xs of + { Nothing{} -> [] + , Just{head=x, tail=xs'} -> + x :: r from to xs' + }}) + + -- Prelude re-exports +in { foldr + , null + , map + , filter + , length + , foldl + , concat + + -- Exports + , reverse + , tails + , intersperse + , intercalate + , dropWhile + , dropWhileEnd + , takeWhile + , takeWhileEnd + , isPrefixOf + , isSuffixOf + , stripPrefix + , stripSuffix + , dropPrefix + , dropSuffix + , zipWith + , zip + , replace + } diff --git a/lib/Prelude.x b/lib/Prelude.x new file mode 100644 --- /dev/null +++ b/lib/Prelude.x @@ -0,0 +1,111 @@ +-- +-- Expresso Prelude +-- + +type Maybe a = ; +type Either a b = ; + +let + id = x -> x; + const = x y -> x; + flip = f x y -> (f y x); + + ---------------------------------------------------------------- + -- Basic list operations + + foldr = f z -> fix (r xs -> + case uncons xs of + { Nothing{} -> z + , Just {head, tail} -> f head (r tail) + }); + null = xs -> case uncons xs of { Nothing{} -> True, Just{} -> False }; + map = f -> foldr (x xs -> f x :: xs) []; + filter = f -> foldr (x xs -> if f x then (x::xs) else xs); + length = foldr (const (n -> 1 + n)) 0; + foldl = f z xs -> foldr (x xsf r -> xsf (f r x)) id xs z; + concat = xss -> foldr (xs ys -> xs ++ ys) [] xss; + + ---------------------------------------------------------------- + -- Maybe operations - smart constructors create closed variants + + just : forall a. a -> Maybe a + = x -> Just x; + + nothing : forall a. Maybe a + = Nothing{}; + + maybe : forall a b. b -> (a -> b) -> Maybe a -> b + = b f m -> case m of { Just a -> f a, Nothing{} -> b }; + + isJust = maybe False (const True); + isNothing = maybe True (const False); + fromMaybe = x -> maybe x id; + listToMaybe = foldr (x -> const (just x)) nothing; + maybeToList = maybe [] (x -> [x]); + catMaybes = xs -> concat (map maybeToList xs); + mapMaybe = f -> maybe nothing (just << f); + + ---------------------------------------------------------------- + -- Either operations - smart constructors create closed variants + + left : forall a b. a -> Either a b + = x -> Left x; + + right : forall a b. b -> Either a b + = x -> Right x; + + either : forall a b c. (a -> c) -> (b -> c) -> Either a b -> c + = f g m -> case m of { Left a -> f a, Right b -> g b }; + + ---------------------------------------------------------------- + -- Logical operations + + and = foldr (x y -> x && y) True; + or = foldr (x y -> x || y) False; + any = p -> or << map p; + all = p -> and << map p; + + elem = x -> any (x' -> x' == x); + notElem = x -> all (x' -> x' /= x); + + ---------------------------------------------------------------- + -- Dynamic binding + + withOverride = overrides f self -> overrides (f self); + mkOverridable = f -> { override_ = overrides -> (withOverride overrides f) | fix f}; + + override = r overrides -> mkOverridable (r.override_ overrides) + + +-- Exports +in { id + , const + , foldr + , null + , map + , filter + , length + , foldl + , concat + , just + , nothing + , maybe + , isJust + , isNothing + , fromMaybe + , listToMaybe + , maybeToList + , catMaybes + , mapMaybe + , left + , right + , either + , and + , or + , any + , all + , elem + , notElem + , mkOverridable + , override + } diff --git a/lib/Text.x b/lib/Text.x new file mode 100644 --- /dev/null +++ b/lib/Text.x @@ -0,0 +1,119 @@ +-- +-- Expresso Text Library +-- +let + {..} = import "Prelude.x"; + list = import "List.x"; + + isEmpty + : Text -> Bool + = t -> t == ""; + + length + : Text -> Int + = unpack >> list.length; + + isSpace + : Char -> Bool + = c -> c == ' '; + + isNewLine + : Char -> Bool + = c -> c == '\n'; + + isUpper + : Char -> Bool + = c -> c >= 'A' && c <= 'Z'; + + isLower + : Char -> Bool + = c -> c >= 'a' && c <= 'z'; + + isDigit + : Char -> Bool + = c -> c >= '0' && c <= '9'; + + isAlpha + : Char -> Bool + = c -> isUpper c || isLower c; + + isAlphaNum + : Char -> Bool + = c -> isAlpha c || isDigit c; + + concat + : [Text] -> Text + = list.foldr (t t' -> t <> t') ""; + + intercalate + : Text -> [Text] -> Text + = s -> map unpack + >> list.intersperse (unpack s) + >> map pack + >> concat; + + unwords + : [Text] -> Text + = intercalate " "; + + isPrefixOf + : Text -> Text -> Bool + = s s' -> list.isPrefixOf (unpack s) (unpack s'); + + isSuffixOf + : Text -> Text -> Bool + = s s' -> list.isSuffixOf (unpack s) (unpack s'); + + stripPrefix + : Text -> Text -> Maybe Text + = s s' -> mapMaybe pack (list.stripPrefix (unpack s) (unpack s')); + + stripSuffix + : Text -> Text -> Maybe Text + = s s' -> mapMaybe pack (list.stripSuffix (unpack s) (unpack s')); + + dropPrefix + : Text -> Text -> Text + = s s' -> pack (list.dropPrefix (unpack s) (unpack s')); + + dropSuffix + : Text -> Text -> Text + = s s' -> pack (list.dropSuffix (unpack s) (unpack s')); + + replace + : Text -> Text -> Text -> Text + = from to xs -> + if isEmpty from + then error "replace: first argument must not be empty" + else pack (list.replace (unpack from) (unpack to) (unpack xs)); + + -- Trim spaces from both sides of the given text + trim + : Text -> Text + = unpack + >> list.dropWhile isSpace + >> list.dropWhileEnd isSpace + >> pack + +-- Exports +in { isEmpty + , length + , isSpace + , isNewLine + , isUpper + , isLower + , isDigit + , isAlpha + , isAlphaNum + , concat + , intercalate + , unwords + , isPrefixOf + , isSuffixOf + , stripPrefix + , stripSuffix + , dropPrefix + , dropSuffix + , replace + , trim + } diff --git a/src/Expresso.hs b/src/Expresso.hs --- a/src/Expresso.hs +++ b/src/Expresso.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE PatternSynonyms #-} {-# OPTIONS_GHC -Wno-unused-top-binds #-} @@ -25,6 +26,7 @@ , HasValue(..) , Import(..) , Name + , SynonymDecl(..) , Thunk(..) , TIState , Type @@ -54,7 +56,10 @@ , evalWithEnv , initEnvironments , installBinding + , installSynonyms + , uninstallSynonym , runEvalM + , setLibDirs , showType , showValue , showValue' @@ -76,9 +81,11 @@ ) where import Control.Monad ((>=>)) -import Control.Monad.Except (ExceptT(..), runExceptT, throwError) +import Control.Monad.Except ( MonadError, ExceptT(..), runExceptT + , throwError) -import Expresso.Eval (Env, EvalM, HasValue(..), Thunk(..), Value(..), insertEnv, runEvalM) +import Expresso.Eval ( Env, EvalM, HasValue(..), Thunk(..), Value(..) + , insertEnv, runEvalM) import Expresso.TypeCheck (TIState, initTIState) import Expresso.Pretty (render) import Expresso.Syntax @@ -90,14 +97,16 @@ -- | Type and term environments. data Environments = Environments - { envsTypeEnv :: !TypeEnv - , envsTIState :: !TIState - , envsTermEnv :: !Env + { envsLibDirs :: ![FilePath] + , envsTypeEnv :: !TypeEnv + , envsSynonyms :: !Synonyms + , envsTIState :: !TIState + , envsTermEnv :: !Env } --- | Empty initial type and term environments. +-- | Empty initial environments. initEnvironments :: Environments -initEnvironments = Environments mempty initTIState mempty +initEnvironments = Environments [] mempty mempty initTIState mempty -- | Install a binding using the supplied name, type and term. -- Useful for extending the set of built-in functions. @@ -109,9 +118,10 @@ -- | Query the type of an expression using the supplied type environment. typeOfWithEnv :: Environments -> ExpI -> IO (Either String Type) -typeOfWithEnv (Environments tEnv tState _) ei = runExceptT $ do - e <- Parser.resolveImports ei - ExceptT $ return $ inferTypes tEnv tState e +typeOfWithEnv (Environments libDirs tEnv syns tState _) ei = runExceptT $ do + (e, ss) <- Parser.resolveImports libDirs ei + syns' <- insertSynonyms ss syns + ExceptT $ return $ inferTypes tEnv syns' tState e -- | Query the type of an expression. typeOf :: ExpI -> IO (Either String Type) @@ -120,7 +130,7 @@ -- | Parse an expression and query its type. typeOfString :: String -> IO (Either String Type) typeOfString str = runExceptT $ do - top <- ExceptT $ return $ Parser.parse "" str + (_, top) <- ExceptT $ return $ Parser.parse "" str ExceptT $ typeOf top -- | Evaluate an expression using the supplied type and term environments. @@ -129,10 +139,11 @@ => Environments -> ExpI -> IO (Either String a) -evalWithEnv (Environments tEnv tState env) ei = runExceptT $ do - e <- Parser.resolveImports ei - _sigma <- ExceptT . return $ inferTypes tEnv tState e - ExceptT $ runEvalM . (Eval.eval env >=> Eval.proj) $ e +evalWithEnv (Environments libDirs tEnv syns tState env) ei = runExceptT $ do + (e, ss) <- Parser.resolveImports libDirs ei + syns' <- insertSynonyms ss syns + _sigma <- ExceptT . return $ inferTypes tEnv syns' tState e + ExceptT $ runEvalM . (Eval.eval env >=> Eval.proj) $ e -- | Evaluate the contents of the supplied file path; and optionally -- validate using a supplied type (schema). @@ -145,8 +156,9 @@ -- so that foreign functions and their types can be installed respectively. evalFile' :: HasValue a => Environments -> Maybe Type -> FilePath -> IO (Either String a) evalFile' envs mty path = runExceptT $ do - top <- ExceptT $ Parser.parse path <$> readFile path - ExceptT $ evalWithEnv envs (maybe id validate mty $ top) + (ss, top) <- ExceptT $ Parser.parse path <$> readFile path + envs' <- installSynonyms ss envs + ExceptT $ evalWithEnv envs' (maybe id validate mty $ top) -- | Parse an expression and evaluate it; optionally -- validate using a supplied type (schema). @@ -159,8 +171,9 @@ -- so that foreign functions and their types can be installed respectively. evalString' :: HasValue a => Environments -> Maybe Type -> String -> IO (Either String a) evalString' envs mty str = runExceptT $ do - top <- ExceptT $ return $ Parser.parse "" str - ExceptT $ evalWithEnv envs (maybe id validate mty $ top) + (ss, top) <- ExceptT $ return $ Parser.parse "" str + envs' <- installSynonyms ss envs + ExceptT $ evalWithEnv envs' (maybe id validate mty $ top) -- | Add a validating type signature section to the supplied expression. validate :: Type -> ExpI -> ExpI @@ -172,18 +185,20 @@ bind :: Environments -> Bind Name + -> Maybe Type -> ExpI -> EvalM Environments -bind (Environments tEnv tState env) b ei = do - e <- Parser.resolveImports ei +bind (Environments libDirs tEnv syns tState env) b mty ei = do + (e, ss) <- Parser.resolveImports libDirs ei + syns' <- insertSynonyms ss syns let (res'e, tState') = - TypeCheck.runTI (TypeCheck.tcDecl (getAnn ei) b e) tEnv tState + TypeCheck.runTI (TypeCheck.tcDecl (getAnn ei) b mty e) tEnv syns' tState case res'e of Left err -> throwError err Right tEnv' -> do thunk <- Eval.mkThunk $ Eval.eval env e env' <- Eval.bind env b thunk - return $ Environments tEnv' tState' env' + return $ Environments libDirs tEnv' syns' tState' env' -- | Pretty print the supplied type. showType :: Type -> String @@ -201,6 +216,36 @@ dumpTypeEnv :: Environments -> [(Name, Sigma)] dumpTypeEnv = typeEnvToList . envsTypeEnv -inferTypes :: TypeEnv -> TIState -> Exp -> Either String Type -inferTypes tEnv tState e = - fst $ TypeCheck.runTI (TypeCheck.typeCheck e) tEnv tState +inferTypes + :: TypeEnv + -> Synonyms + -> TIState + -> Exp + -> Either String Type +inferTypes tEnv syns tState e = + fst $ TypeCheck.runTI (TypeCheck.typeCheck e) tEnv syns tState + +-- | Set the library paths used when resolving relative imports. +setLibDirs :: [FilePath] -> Environments -> Environments +setLibDirs libDirs envs = + envs { envsLibDirs = libDirs } + +-- | Install the supplied type synonym declarations. +installSynonyms + :: MonadError String m + => [SynonymDecl] + -> Environments + -> m Environments +installSynonyms ss envs = do + syns' <- insertSynonyms ss (envsSynonyms envs) + return $ envs { envsSynonyms = syns' } + +-- | Used by the REPL, deletes any previous definition. +uninstallSynonym + :: SynonymDecl + -> Environments + -> Environments +uninstallSynonym s envs = + let syns' = deleteSynonym (synonymName s) + $ envsSynonyms envs + in envs { envsSynonyms = syns' } diff --git a/src/Expresso/Eval.hs b/src/Expresso/Eval.hs --- a/src/Expresso/Eval.hs +++ b/src/Expresso/Eval.hs @@ -1,557 +1,567 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PatternGuards #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE TypeSynonymInstances #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE ViewPatterns #-} -{-# OPTIONS_GHC -Wno-unused-top-binds #-} - --- | --- Module : Expresso.Eval --- Copyright : (c) Tim Williams 2017-2019 --- License : BSD3 --- --- Maintainer : info@timphilipwilliams.com --- Stability : experimental --- Portability : portable --- --- A lazy evaluator. --- --- The front-end syntax is simple, so we evaluate it directly. --- -module Expresso.Eval( - Env - , EvalM - , HasValue(..) - , Thunk(..) - , Value(..) - , bind - , choice - , eval - , insertEnv - , mkRecord - , mkStrictLam - , mkStrictLam2 - , mkStrictLam3 - , mkThunk - , mkVariant - , ppValue - , ppValue' - , runEvalM - , typeMismatch - , unit - , (.:) - , (.=) -) -where - -import Control.Monad.Except -import Data.Foldable (foldrM) -import Data.HashMap.Strict (HashMap) -import Data.IORef -import Data.Ord -import Data.Text (Text) -import qualified Data.Text as T -import qualified Data.HashMap.Strict as HashMap -import qualified Data.List as List - -import Expresso.Syntax -import Expresso.Type -import Expresso.Pretty -import Expresso.Utils (cata, (:*:)(..), K(..)) - --- | A call-by-need environment. --- Using a HashMap makes it easy to support record wildcards. -newtype Env = Env { unEnv :: HashMap Name Thunk } deriving (Semigroup, Monoid) - -type EvalM a = ExceptT String IO a - --- | A potentially unevaluated value. -newtype Thunk = Thunk { force :: EvalM Value } - -instance Show Thunk where - show _ = "" - -mkThunk :: EvalM Value -> EvalM Thunk -mkThunk ev = do - ref <- liftIO $ newIORef Nothing - return $ Thunk $ do - mv <- liftIO $ readIORef ref - case mv of - Nothing -> do - v <- ev - liftIO $ writeIORef ref (Just v) - return v - Just v -> return v - --- | Type for an evaluated term. -data Value - = VLam !(Thunk -> EvalM Value) - | VInt !Integer - | VDbl !Double - | VBool !Bool - | VChar !Char - | VText !Text - | VList ![Value] -- lists are strict - | VRecord !(HashMap Label Thunk) -- field order no defined - | VVariant !Label !Thunk - --- | This does *not* evaluate deeply -ppValue :: Value -> Doc -ppValue (VLam _) = "" -ppValue (VInt i) = integer i -ppValue (VDbl d) = double d -ppValue (VBool b) = if b then "True" else "False" -ppValue (VChar c) = text $ '\'' : c : '\'' : [] -ppValue (VText s) = string (show $ T.unpack s) -ppValue (VList xs) = bracketsList $ map ppValue xs -ppValue (VRecord m) = bracesList $ map ppEntry $ HashMap.keys m - where - ppEntry l = text l <+> "=" <+> "" -ppValue (VVariant l _) = text l <+> "" - --- | This evaluates deeply -ppValue' :: Value -> EvalM Doc -ppValue' (VRecord m) = (bracesList . map ppEntry . HashMap.toList) - <$> mapM (force >=> ppValue') m - where - ppEntry (l, v) = text l <+> text "=" <+> v -ppValue' (VVariant l t) = (text l <+>) <$> (force >=> ppParensValue) t -ppValue' v = return $ ppValue v - -ppParensValue :: Value -> EvalM Doc -ppParensValue v = - case v of - VVariant{} -> parens <$> ppValue' v - _ -> ppValue' v - -extractChar :: Value -> Maybe Char -extractChar (VChar c) = Just c -extractChar _ = Nothing - --- | Run the EvalM evaluation computation. -runEvalM :: EvalM a -> IO (Either String a) -runEvalM = runExceptT - --- | Partial variant of @runEvalM@. -runEvalM' :: EvalM a -> IO a -runEvalM' = fmap (either error id) . runExceptT - -eval :: Env -> Exp -> EvalM Value -eval env e = cata alg e env - where - alg :: (ExpF Name Bind Type :*: K Pos) (Env -> EvalM Value) - -> Env - -> EvalM Value - alg (EVar v :*: _) env = lookupValue env v >>= force - alg (EApp f x :*: K pos) env = do - f' <- f env - x' <- mkThunk (x env) - evalApp pos f' x' - alg (ELam b e1 :*: _ ) env = evalLam env b e1 - alg (EAnnLam b _ e1 :*: _) env = evalLam env b e1 - alg (ELet b e1 e2 :*: _) env = do - t <- mkThunk $ e1 env - env' <- bind env b t - e2 env' - alg (EPrim p :*: K pos) _ = return $ evalPrim pos p - alg (EAnn e _ :*: _) env = e env - -evalLam :: Env -> Bind Name -> (Env -> EvalM Value) -> EvalM Value -evalLam env b e = return $ VLam $ \x -> - bind env b x >>= e - -evalApp :: Pos -> Value -> Thunk -> EvalM Value -evalApp _ (VLam f) t = f t -evalApp pos fv _ = - throwError $ show pos ++ " : Expected a function, but got: " ++ - show (ppValue fv) - -evalPrim :: Pos -> Prim -> Value -evalPrim pos p = case p of - Int i -> VInt i - Dbl d -> VDbl d - Bool b -> VBool b - Char c -> VChar c - Text s -> VText s - Show -> mkStrictLam $ \v -> VText . T.pack . show <$> ppValue' v - -- Trace - ErrorPrim -> VLam $ \s -> do - msg <- proj' s - throwError $ "error (" ++ show pos ++ "): " ++ msg - - ArithPrim Add -> mkStrictLam2 $ numOp pos (+) - ArithPrim Sub -> mkStrictLam2 $ numOp pos (-) - ArithPrim Mul -> mkStrictLam2 $ numOp pos (*) - ArithPrim Div -> mkStrictLam2 $ \v1 v2 -> - case (v1, v2) of - (VInt x, VInt y) -> return $ VInt $ x `div` y - (VDbl x, VDbl y) -> return $ VDbl $ x / y - _ -> failOnValues pos [v1, v2] - - RelPrim RGT -> mkStrictLam2 $ \v1 v2 -> - (VBool . (==GT)) <$> compareValues pos v1 v2 - - RelPrim RGTE -> mkStrictLam2 $ \v1 v2 -> - (VBool . (`elem` [GT, EQ])) <$> compareValues pos v1 v2 - - RelPrim RLT -> mkStrictLam2 $ \v1 v2 -> - (VBool . (==LT)) <$> compareValues pos v1 v2 - - RelPrim RLTE -> mkStrictLam2 $ \v1 v2 -> - (VBool . (`elem` [LT, EQ])) <$> compareValues pos v1 v2 - - Eq -> mkStrictLam2 $ \v1 v2 -> - VBool <$> equalValues pos v1 v2 - - NEq -> mkStrictLam2 $ \v1 v2 -> - (VBool . not) <$> equalValues pos v1 v2 - - Not -> VLam $ \v -> VBool <$> proj' v - And -> VLam $ \v1 -> return $ VLam $ \v2 -> - VBool <$> ((&&) <$> proj' v1 <*> proj' v2) - - Or -> VLam $ \v1 -> return $ VLam $ \v2 -> - VBool <$> ((||) <$> proj' v1 <*> proj' v2) - - Double -> mkStrictLam $ \v -> - case v of - VInt i -> return $ VDbl $ fromInteger i - _ -> failOnValues pos [v] - Floor -> mkStrictLam $ \v -> - case v of - VDbl d -> return $ VInt $ floor d - _ -> failOnValues pos [v] - Ceiling -> mkStrictLam $ \v -> - case v of - VDbl d -> return $ VInt $ ceiling d - _ -> failOnValues pos [v] - - Neg -> mkStrictLam $ \v -> - case v of - VInt i -> return $ VInt $ negate i - VDbl d -> return $ VDbl $ negate d - _ -> failOnValues pos [v] - - Mod -> mkStrictLam $ \v1 -> return $ mkStrictLam $ \v2 -> - case (v1, v2) of - (VInt x, VInt y) -> return $ VInt $ x `mod` y - _ -> failOnValues pos [v1, v2] - - Cond -> VLam $ \c -> return $ VLam $ \t -> return $ VLam $ \f -> - proj' c >>= \c -> if c then force t else force f - FixPrim -> mkStrictLam $ \f -> fix (evalApp pos f <=< mkThunk) - - -- We cannot yet define operators like this in the language - FwdComp -> mkStrictLam2 $ \f g -> - return $ VLam $ \x -> - mkThunk (evalApp pos f x) >>= evalApp pos g - BwdComp -> mkStrictLam2 $ \f g -> - return $ VLam $ \x -> - mkThunk (evalApp pos g x) >>= evalApp pos f - - Pack -> mkStrictLam $ packChars pos - Unpack -> mkStrictLam $ unpackChars pos - - ListEmpty -> VList [] - ListNull -> VLam $ \xs -> - (VBool . (null :: [Value] -> Bool)) <$> proj' xs - ListCons -> VLam $ \x -> return $ VLam $ \xs -> - VList <$> ((:) <$> force x <*> proj' xs) - ListAppend -> VLam $ \xs -> return $ VLam $ \ys -> - VList <$> ((++) <$> proj' xs <*> proj' ys) - ListFoldr -> mkStrictLam $ \f -> - return $ VLam $ \z -> return $ VLam $ \xs -> do - let g a b = do g' <- evalApp pos f (Thunk $ return a) - evalApp pos g' (Thunk $ return b) - z' <- force z - xs' <- proj' xs :: EvalM [Value] - foldrM g z' xs' - - RecordExtend l -> VLam $ \v -> return $ VLam $ \r -> - (VRecord . HashMap.insert l v) <$> proj' r - RecordRestrict l -> VLam $ \r -> - (VRecord . HashMap.delete l) <$> proj' r - RecordSelect l -> VLam $ \r -> do - r' <- proj' r - let err = throwError $ show pos ++ " : " ++ l ++ " not found" - maybe err force (HashMap.lookup l r') - RecordEmpty -> VRecord mempty - - VariantInject l -> VLam $ \v -> - return $ VVariant l v - VariantEmbed _ -> VLam force - VariantElim l -> mkStrictLam $ \f -> return $ mkStrictLam2 $ \k s -> do - case s of - VVariant l' t | l==l' -> evalApp pos f t - | otherwise -> evalApp pos k (Thunk $ return s) - v -> throwError $ show pos ++ " : Expected a variant, but got: " ++ - show (ppValue v) - Absurd -> VLam $ \v -> force v >> throwError "The impossible happened!" - p -> error $ show pos ++ " : Unsupported Prim: " ++ show p - --- non-strict bind -bind :: Env -> Bind Name -> Thunk -> EvalM Env -bind env b t = case b of - Arg n -> return $ insertEnv n t env - _ -> bind' env b t - --- strict bind -bind' :: Env -> Bind Name -> Thunk -> EvalM Env -bind' env b t = do - v <- force t - case (b, v) of - (Arg n, _) -> - return $ insertEnv n (Thunk $ return v) env - (RecArg ns, VRecord m) | Just vs <- mapM (\n -> HashMap.lookup n m) ns -> - return $ env <> (mkEnv $ zip ns vs) - (RecWildcard, VRecord m) -> - return $ env <> Env m - _ -> throwError $ "Cannot bind the pair: " ++ show b ++ " = " ++ show (ppValue v) - -insertEnv :: Name -> Thunk -> Env -> Env -insertEnv n t (Env m) = Env $ HashMap.insert n t m - -lookupEnv :: Name -> Env -> Maybe Thunk -lookupEnv n (Env m) = HashMap.lookup n m - -mkEnv :: [(Name, Thunk)] -> Env -mkEnv = Env . HashMap.fromList - -lookupValue :: Env -> Name -> EvalM Thunk -lookupValue env n = maybe err return $ lookupEnv n env - where - err = throwError $ "Not found: " ++ show n - -failOnValues :: Pos -> [Value] -> EvalM a -failOnValues pos vs = throwError $ show pos ++ " : Unexpected value(s) : " ++ - show (parensList (map ppValue vs)) - --- | Make a strict Expresso lambda value (forced arguments) from a --- Haskell function (on Expresso values). -mkStrictLam :: (Value -> EvalM Value) -> Value -mkStrictLam f = VLam $ \x -> force x >>= f - --- | As @mkStrictLam@, but accepts Haskell functions with two curried arguments. -mkStrictLam2 :: (Value -> Value -> EvalM Value) -> Value -mkStrictLam2 f = mkStrictLam $ \v -> return $ mkStrictLam $ f v - --- | As @mkStrictLam@, but accepts Haskell functions with three curried arguments. -mkStrictLam3 :: (Value -> Value -> Value -> EvalM Value) -> Value -mkStrictLam3 f = mkStrictLam $ \v -> return $ mkStrictLam2 $ f v - --- | Force (evaluate) thunk and then project out the Haskell value. -proj' :: HasValue a => Thunk -> EvalM a -proj' = force >=> proj - -numOp :: Pos -> (forall a. Num a => a -> a -> a) -> Value -> Value -> EvalM Value -numOp _ op (VInt x) (VInt y) = return $ VInt $ x `op` y -numOp _ op (VDbl x) (VDbl y) = return $ VDbl $ x `op` y -numOp p _ v1 v2 = failOnValues p [v1, v2] - --- NB: evaluates deeply -equalValues :: Pos -> Value -> Value -> EvalM Bool -equalValues _ (VInt i1) (VInt i2) = return $ i1 == i2 -equalValues _ (VDbl d1) (VDbl d2) = return $ d1 == d2 -equalValues _ (VBool b1) (VBool b2) = return $ b1 == b2 -equalValues _ (VChar c1) (VChar c2) = return $ c1 == c2 -equalValues _ (VText s1) (VText s2) = return $ s1 == s2 -equalValues p (VList xs) (VList ys) - | length xs == length ys = and <$> zipWithM (equalValues p) xs ys - | otherwise = return False -equalValues p (VRecord m1) (VRecord m2) = do - (ls1, vs1) <- unzip . recordValues <$> mapM force m1 - (ls2, vs2) <- unzip . recordValues <$> mapM force m2 - if length ls1 == length ls2 && length vs1 == length vs2 - then and <$> zipWithM (equalValues p) vs1 vs2 - else return False -equalValues p (VVariant l1 v1) (VVariant l2 v2) - | l1 == l2 = join $ equalValues p <$> force v1 <*> force v2 - | otherwise = return False -equalValues p v1 v2 = failOnValues p [v1, v2] - --- NB: evaluates deeply -compareValues :: Pos -> Value -> Value -> EvalM Ordering -compareValues _ (VInt i1) (VInt i2) = return $ compare i1 i2 -compareValues _ (VDbl d1) (VDbl d2) = return $ compare d1 d2 -compareValues _ (VBool b1) (VBool b2) = return $ compare b1 b2 -compareValues _ (VChar c1) (VChar c2) = return $ compare c1 c2 -compareValues _ (VText s1) (VText s2) = return $ compare s1 s2 -compareValues p (VList xs) (VList ys) = go xs ys - where - go :: [Value] -> [Value] -> EvalM Ordering - go [] [] = return EQ - go (_:_) [] = return GT - go [] (_:_) = return LT - go (x:xs') (y:ys') = do - c <- compareValues p x y - if c == EQ - then go xs' ys' - else return c -compareValues p v1 v2 = failOnValues p [v1, v2] - --- | Used for equality of records, sorts values by key -recordValues :: HashMap Label a -> [(Label, a)] -recordValues = List.sortBy (comparing fst) . HashMap.toList - -packChars :: Pos -> Value -> EvalM Value -packChars pos (VList xs) - | Just cs <- mapM extractChar xs = return . VText . T.pack $ cs - | otherwise = failOnValues pos xs -packChars pos v = failOnValues pos [v] - -unpackChars :: Pos -> Value -> EvalM Value -unpackChars _ (VText s) = return . VList . map VChar . T.unpack $ s -unpackChars pos v = failOnValues pos [v] - ------------------------------------------------------------- --- HasValue class and instances - -instance (HasValue a, HasValue b) => HasValue (a -> EvalM b) where - proj (VLam f) = return $ \x -> do - r <- f (Thunk $ return $ inj x) - proj r - proj v = typeMismatch "VLam" v - inj f = VLam $ \v -> proj' v >>= fmap inj . f - --- | A class of Haskell types that can be projected from or injected --- into Expresso values. -class HasValue a where - proj :: Value -> EvalM a - inj :: a -> Value - -instance HasValue Value where - proj v = return v - inj = id - -instance HasValue Integer where - proj (VInt i) = return i - proj v = typeMismatch "VInt" v - inj = VInt - -instance HasValue Double where - proj (VDbl d) = return d - proj v = typeMismatch "VDbl" v - inj = VDbl - -instance HasValue Bool where - proj (VBool b) = return b - proj v = typeMismatch "VBool" v - inj = VBool - -instance HasValue Char where - proj (VChar c) = return c - proj v = typeMismatch "VChar" v - inj = VChar - -instance HasValue String where - proj (VText s) = return $ T.unpack s - proj v = typeMismatch "VText" v - inj = VText . T.pack - -instance HasValue Text where - proj (VText s) = return s - proj v = typeMismatch "VText" v - inj = VText - -instance HasValue a => HasValue (Maybe a) where - proj = choice [ ("Just", fmap Just . proj) - , ("Nothing", const $ pure Nothing) - ] - inj (Just x) = mkVariant "Just" (inj x) - inj Nothing = mkVariant "Nothing" unit - -instance {-# OVERLAPS #-} HasValue a => HasValue [a] where - proj (VList xs) = mapM proj xs - proj v = typeMismatch "VList" v - inj = VList . map inj - -instance {-# OVERLAPS #-} HasValue [Value] where - proj (VList xs) = return xs - proj v = typeMismatch "VList" v - inj = VList - -instance HasValue a => HasValue (HashMap Name a) where - proj (VRecord m) = mapM proj' m - proj v = typeMismatch "VRecord" v - inj = VRecord . fmap (Thunk . return . inj) - -instance {-# OVERLAPS #-} HasValue a => HasValue [(Name, a)] where - proj v = HashMap.toList <$> proj v - inj = inj . HashMap.fromList - -instance {-# OVERLAPS #-} HasValue (HashMap Name Thunk) where - proj (VRecord m) = return m - proj v = typeMismatch "VRecord" v - inj = VRecord - -instance {-# OVERLAPS #-} HasValue [(Name, Thunk)] where - proj v = HashMap.toList <$> proj v - inj = inj . HashMap.fromList - -instance {-# OVERLAPS #-} (HasValue a, HasValue b) => HasValue (a -> b) where - proj _ = throwError "proj not supported for pure functions" - inj f = mkStrictLam $ fmap (inj . f) . proj - -instance {-# OVERLAPS #-} (HasValue a, HasValue b, HasValue c) => HasValue (a -> b -> c) where - proj _ = throwError "proj not supported for pure functions" - inj f = inj $ \x -> inj (f x) - -instance {-# OVERLAPS #-} (HasValue a, HasValue b, HasValue c, HasValue d) => HasValue (a -> b -> c -> d) where - proj _ = throwError "proj not supported for pure functions" - inj f = inj $ \x -> inj (f x) - -instance {-# OVERLAPS #-} (HasValue a, HasValue b) => HasValue (a -> IO b) where - proj (VLam f) = return $ \x -> runEvalM' $ f (Thunk . return . inj $ x) >>= proj - proj v = typeMismatch "VLam" v - inj f = mkStrictLam $ \v -> proj v >>= \x -> inj <$> liftIO (f x) - -instance {-# OVERLAPS #-} (HasValue a, HasValue b, HasValue c) => HasValue (a -> b -> IO c) where - proj v = proj v >>= \f -> return $ \x -> f x - inj f = inj $ \x -> inj (f x) - -instance {-# OVERLAPS #-} (HasValue a, HasValue b, HasValue c, HasValue d) => HasValue (a -> b -> c -> IO d) where - proj v = proj v >>= \f -> return $ \x -> f x - inj f = inj $ \x -> inj (f x) - --- | Throw a type mismatch error. -typeMismatch :: String -> Value -> EvalM a -typeMismatch expected v = throwError $ "Type mismatch: expected a " ++ expected ++ - ", but got: " ++ show (ppValue v) - --- | Project out a record field, fail with a type mismatch if it is not present. -(.:) :: HasValue a => Value -> Name -> EvalM a -(.:) (VRecord m) k = case HashMap.lookup k m of - Nothing -> throwError $ "Record label " ++ show k ++ " not present" - Just v -> proj' v -(.:) v _ = typeMismatch "VRecord" v - --- | Pair up a field name and a value. Intended to be used with @mkRecord@ or @mkVariant@. -(.=) :: Name -> Value -> (Name, Thunk) -(.=) k v = (k, Thunk . return $ v) - --- | Convenience for implementing @proj@ for a sum type. -choice :: HasValue a => [(Name, Value -> EvalM a)] -> Value -> EvalM a -choice alts = \case - VVariant k v - | Just f <- HashMap.lookup k m -> force v >>= f - | otherwise -> throwError $ "Missing label in alternatives: " ++ show k - v -> typeMismatch "VVariant" v - where - m = HashMap.fromList alts - --- | Convenience constructor for a record value. -mkRecord :: [(Name, Thunk)] -> Value -mkRecord = VRecord . HashMap.fromList - --- | Convenience constructor for a variant value. -mkVariant :: Name -> Value -> Value -mkVariant name = VVariant name . Thunk . return - --- | Unit value. Equivalent to @()@ in Haskell. -unit :: Value -unit = VRecord mempty +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -Wno-unused-top-binds #-} + +-- | +-- Module : Expresso.Eval +-- Copyright : (c) Tim Williams 2017-2019 +-- License : BSD3 +-- +-- Maintainer : info@timphilipwilliams.com +-- Stability : experimental +-- Portability : portable +-- +-- A lazy evaluator. +-- +-- The front-end syntax is simple, so we evaluate it directly. +-- +module Expresso.Eval( + Env + , EvalM + , HasValue(..) + , Thunk(..) + , Value(..) + , bind + , choice + , eval + , insertEnv + , mkRecord + , mkStrictLam + , mkStrictLam2 + , mkStrictLam3 + , mkThunk + , mkVariant + , ppValue + , ppValue' + , runEvalM + , typeMismatch + , unit + , (.:) + , (.=) +) +where + +import Control.Monad.Except +import Data.Foldable (foldrM) +import Data.HashMap.Strict (HashMap) +import Data.IORef +import Data.Ord +import Data.Text (Text) +import qualified Data.Text as T +import qualified Data.HashMap.Strict as HashMap +import qualified Data.List as List + +import Expresso.Syntax +import Expresso.Type +import Expresso.Pretty +import Expresso.Utils (cata, (:*:)(..), K(..)) + +-- | A call-by-need environment. +-- Using a HashMap makes it easy to support record wildcards. +newtype Env = Env { unEnv :: HashMap Name Thunk } deriving (Semigroup, Monoid) + +type EvalM a = ExceptT String IO a + +-- | A potentially unevaluated value. +newtype Thunk = Thunk { force :: EvalM Value } + +instance Show Thunk where + show _ = "" + +mkThunk :: EvalM Value -> EvalM Thunk +mkThunk ev = do + ref <- liftIO $ newIORef Nothing + return $ Thunk $ do + mv <- liftIO $ readIORef ref + case mv of + Nothing -> do + v <- ev + liftIO $ writeIORef ref (Just v) + return v + Just v -> return v + +-- | Type for an evaluated term. +data Value + = VLam !(Thunk -> EvalM Value) + | VInt !Integer + | VDbl !Double + | VBool !Bool + | VChar !Char + | VText !Text + | VList ![Value] -- lists are strict + | VRecord !(HashMap Label Thunk) -- field order no defined + | VVariant !Label !Thunk + +-- | This does *not* evaluate deeply +ppValue :: Value -> Doc +ppValue (VLam _) = "" +ppValue (VInt i) = integer i +ppValue (VDbl d) = double d +ppValue (VBool b) = if b then "True" else "False" +ppValue (VChar c) = text $ '\'' : c : '\'' : [] +ppValue (VText s) = string (show $ T.unpack s) +ppValue (VList xs) = bracketsList $ map ppValue xs +ppValue (VRecord m) = bracesList $ map ppEntry $ HashMap.keys m + where + ppEntry l = text l <+> "=" <+> "" +ppValue (VVariant l _) = text l <+> "" + +-- | This evaluates deeply +ppValue' :: Value -> EvalM Doc +ppValue' (VRecord m) = (bracesList . map ppEntry . HashMap.toList) + <$> mapM (force >=> ppValue') m + where + ppEntry (l, v) = text l <+> text "=" <+> v +ppValue' (VVariant l t) = (text l <+>) <$> (force >=> ppParensValue) t +ppValue' v = return $ ppValue v + +ppParensValue :: Value -> EvalM Doc +ppParensValue v = + case v of + VVariant{} -> parens <$> ppValue' v + _ -> ppValue' v + +extractChar :: Value -> Maybe Char +extractChar (VChar c) = Just c +extractChar _ = Nothing + +-- | Run the EvalM evaluation computation. +runEvalM :: EvalM a -> IO (Either String a) +runEvalM = runExceptT + +-- | Partial variant of @runEvalM@. +runEvalM' :: EvalM a -> IO a +runEvalM' = fmap (either error id) . runExceptT + +eval :: Env -> Exp -> EvalM Value +eval env e = cata alg e env + where + alg :: (ExpF Name Bind Type :*: K Pos) (Env -> EvalM Value) + -> Env + -> EvalM Value + alg (EVar v :*: _) env = lookupValue env v >>= force + alg (EApp f x :*: K pos) env = do + f' <- f env + x' <- mkThunk (x env) + evalApp pos f' x' + alg (ELam b e1 :*: _ ) env = evalLam env b e1 + alg (EAnnLam b _ e1 :*: _) env = evalLam env b e1 + alg (ELet b e1 e2 :*: _) env = evalLet env b e1 e2 + alg (EAnnLet b _ e1 e2 :*: _) env = evalLet env b e1 e2 + alg (EPrim p :*: K pos) _ = return $ evalPrim pos p + alg (EAnn e _ :*: _) env = e env + +evalLam :: Env -> Bind Name -> (Env -> EvalM Value) -> EvalM Value +evalLam env b e = return $ VLam $ \x -> + bind env b x >>= e + +evalLet + :: Env + -> Bind Name + -> (Env -> EvalM Value) + -> (Env -> EvalM Value) + -> EvalM Value +evalLet env b e1 e2 = do + t <- mkThunk $ e1 env + env' <- bind env b t + e2 env' + +evalApp :: Pos -> Value -> Thunk -> EvalM Value +evalApp _ (VLam f) t = f t +evalApp pos fv _ = + throwError $ show pos ++ " : Expected a function, but got: " ++ + show (ppValue fv) + +evalPrim :: Pos -> Prim -> Value +evalPrim pos p = case p of + Int i -> VInt i + Dbl d -> VDbl d + Bool b -> VBool b + Char c -> VChar c + Text s -> VText s + Show -> mkStrictLam $ \v -> VText . T.pack . show <$> ppValue' v + -- Trace + ErrorPrim -> VLam $ \s -> do + msg <- proj' s + throwError $ "error (" ++ show pos ++ "): " ++ msg + + ArithPrim Add -> mkStrictLam2 $ numOp pos (+) + ArithPrim Sub -> mkStrictLam2 $ numOp pos (-) + ArithPrim Mul -> mkStrictLam2 $ numOp pos (*) + ArithPrim Div -> mkStrictLam2 $ \v1 v2 -> + case (v1, v2) of + (VInt x, VInt y) -> return $ VInt $ x `div` y + (VDbl x, VDbl y) -> return $ VDbl $ x / y + _ -> failOnValues pos [v1, v2] + + RelPrim RGT -> mkStrictLam2 $ \v1 v2 -> + (VBool . (==GT)) <$> compareValues pos v1 v2 + + RelPrim RGTE -> mkStrictLam2 $ \v1 v2 -> + (VBool . (`elem` [GT, EQ])) <$> compareValues pos v1 v2 + + RelPrim RLT -> mkStrictLam2 $ \v1 v2 -> + (VBool . (==LT)) <$> compareValues pos v1 v2 + + RelPrim RLTE -> mkStrictLam2 $ \v1 v2 -> + (VBool . (`elem` [LT, EQ])) <$> compareValues pos v1 v2 + + Eq -> mkStrictLam2 $ \v1 v2 -> + VBool <$> equalValues pos v1 v2 + + NEq -> mkStrictLam2 $ \v1 v2 -> + (VBool . not) <$> equalValues pos v1 v2 + + Not -> VLam $ \v -> VBool <$> proj' v + And -> VLam $ \v1 -> return $ VLam $ \v2 -> + VBool <$> ((&&) <$> proj' v1 <*> proj' v2) + + Or -> VLam $ \v1 -> return $ VLam $ \v2 -> + VBool <$> ((||) <$> proj' v1 <*> proj' v2) + + Double -> mkStrictLam $ \v -> + case v of + VInt i -> return $ VDbl $ fromInteger i + _ -> failOnValues pos [v] + Floor -> mkStrictLam $ \v -> + case v of + VDbl d -> return $ VInt $ floor d + _ -> failOnValues pos [v] + Ceiling -> mkStrictLam $ \v -> + case v of + VDbl d -> return $ VInt $ ceiling d + _ -> failOnValues pos [v] + + Neg -> mkStrictLam $ \v -> + case v of + VInt i -> return $ VInt $ negate i + VDbl d -> return $ VDbl $ negate d + _ -> failOnValues pos [v] + + Mod -> mkStrictLam $ \v1 -> return $ mkStrictLam $ \v2 -> + case (v1, v2) of + (VInt x, VInt y) -> return $ VInt $ x `mod` y + _ -> failOnValues pos [v1, v2] + + Cond -> VLam $ \c -> return $ VLam $ \t -> return $ VLam $ \f -> + proj' c >>= \c -> if c then force t else force f + FixPrim -> mkStrictLam $ \f -> fix (evalApp pos f <=< mkThunk) + + -- We cannot yet define operators like this in the language + FwdComp -> mkStrictLam2 $ \f g -> + return $ VLam $ \x -> + mkThunk (evalApp pos f x) >>= evalApp pos g + BwdComp -> mkStrictLam2 $ \f g -> + return $ VLam $ \x -> + mkThunk (evalApp pos g x) >>= evalApp pos f + + Pack -> mkStrictLam $ packChars pos + Unpack -> mkStrictLam $ unpackChars pos + TextAppend -> VLam $ \xs -> return $ VLam $ \ys -> + VText <$> ((<>) <$> proj' xs <*> proj' ys) + + ListEmpty -> VList [] + ListCons -> VLam $ \x -> return $ VLam $ \xs -> + VList <$> ((:) <$> force x <*> proj' xs) + ListUncons -> mkStrictLam $ \case + VList (x:xs) -> + return $ mkVariant "Just" (mkRecord + [ ("head", Thunk $ return x) + , ("tail", Thunk . return $ VList xs)]) + VList [] -> return $ mkVariant "Nothing" unit + v -> failOnValues pos [v] + ListAppend -> VLam $ \xs -> return $ VLam $ \ys -> + VList <$> ((++) <$> proj' xs <*> proj' ys) + + RecordExtend l -> VLam $ \v -> return $ VLam $ \r -> + (VRecord . HashMap.insert l v) <$> proj' r + RecordRestrict l -> VLam $ \r -> + (VRecord . HashMap.delete l) <$> proj' r + RecordSelect l -> VLam $ \r -> do + r' <- proj' r + let err = throwError $ show pos ++ " : " ++ l ++ " not found" + maybe err force (HashMap.lookup l r') + RecordEmpty -> VRecord mempty + + VariantInject l -> VLam $ \v -> + return $ VVariant l v + VariantEmbed _ -> VLam force + VariantElim l -> mkStrictLam $ \f -> return $ mkStrictLam2 $ \k s -> do + case s of + VVariant l' t | l==l' -> evalApp pos f t + | otherwise -> evalApp pos k (Thunk $ return s) + v -> throwError $ show pos ++ " : Expected a variant, but got: " ++ + show (ppValue v) + Absurd -> VLam $ \v -> force v >> throwError "The impossible happened!" + p -> error $ show pos ++ " : Unsupported Prim: " ++ show p + +-- non-strict bind +bind :: Env -> Bind Name -> Thunk -> EvalM Env +bind env b t = case b of + Arg n -> return $ insertEnv n t env + _ -> bind' env b t + +-- strict bind +bind' :: Env -> Bind Name -> Thunk -> EvalM Env +bind' env b t = do + v <- force t + case (b, v) of + (Arg n, _) -> + return $ insertEnv n (Thunk $ return v) env + (RecArg (unzip -> (ls, ns)), VRecord m) + | Just vs <- mapM (\l -> HashMap.lookup l m) ls -> + return $ (mkEnv $ zip ns vs) <> env + (RecWildcard, VRecord m) -> + return $ Env m <> env + _ -> throwError $ "Cannot bind the pair: " ++ show b ++ " = " ++ show (ppValue v) + +insertEnv :: Name -> Thunk -> Env -> Env +insertEnv n t (Env m) = Env $ HashMap.insert n t m + +lookupEnv :: Name -> Env -> Maybe Thunk +lookupEnv n (Env m) = HashMap.lookup n m + +mkEnv :: [(Name, Thunk)] -> Env +mkEnv = Env . HashMap.fromList + +lookupValue :: Env -> Name -> EvalM Thunk +lookupValue env n = maybe err return $ lookupEnv n env + where + err = throwError $ "Not found: " ++ show n + +failOnValues :: Pos -> [Value] -> EvalM a +failOnValues pos vs = throwError $ show pos ++ " : Unexpected value(s) : " ++ + show (parensList (map ppValue vs)) + +-- | Make a strict Expresso lambda value (forced arguments) from a +-- Haskell function (on Expresso values). +mkStrictLam :: (Value -> EvalM Value) -> Value +mkStrictLam f = VLam $ \x -> force x >>= f + +-- | As @mkStrictLam@, but accepts Haskell functions with two curried arguments. +mkStrictLam2 :: (Value -> Value -> EvalM Value) -> Value +mkStrictLam2 f = mkStrictLam $ \v -> return $ mkStrictLam $ f v + +-- | As @mkStrictLam@, but accepts Haskell functions with three curried arguments. +mkStrictLam3 :: (Value -> Value -> Value -> EvalM Value) -> Value +mkStrictLam3 f = mkStrictLam $ \v -> return $ mkStrictLam2 $ f v + +-- | Force (evaluate) thunk and then project out the Haskell value. +proj' :: HasValue a => Thunk -> EvalM a +proj' = force >=> proj + +numOp :: Pos -> (forall a. Num a => a -> a -> a) -> Value -> Value -> EvalM Value +numOp _ op (VInt x) (VInt y) = return $ VInt $ x `op` y +numOp _ op (VDbl x) (VDbl y) = return $ VDbl $ x `op` y +numOp p _ v1 v2 = failOnValues p [v1, v2] + +-- NB: evaluates deeply +equalValues :: Pos -> Value -> Value -> EvalM Bool +equalValues _ (VInt i1) (VInt i2) = return $ i1 == i2 +equalValues _ (VDbl d1) (VDbl d2) = return $ d1 == d2 +equalValues _ (VBool b1) (VBool b2) = return $ b1 == b2 +equalValues _ (VChar c1) (VChar c2) = return $ c1 == c2 +equalValues _ (VText s1) (VText s2) = return $ s1 == s2 +equalValues p (VList xs) (VList ys) + | length xs == length ys = and <$> zipWithM (equalValues p) xs ys + | otherwise = return False +equalValues p (VRecord m1) (VRecord m2) = do + (ls1, vs1) <- unzip . recordValues <$> mapM force m1 + (ls2, vs2) <- unzip . recordValues <$> mapM force m2 + if length ls1 == length ls2 && length vs1 == length vs2 + then and <$> zipWithM (equalValues p) vs1 vs2 + else return False +equalValues p (VVariant l1 v1) (VVariant l2 v2) + | l1 == l2 = join $ equalValues p <$> force v1 <*> force v2 + | otherwise = return False +equalValues p v1 v2 = failOnValues p [v1, v2] + +-- NB: evaluates deeply +compareValues :: Pos -> Value -> Value -> EvalM Ordering +compareValues _ (VInt i1) (VInt i2) = return $ compare i1 i2 +compareValues _ (VDbl d1) (VDbl d2) = return $ compare d1 d2 +compareValues _ (VBool b1) (VBool b2) = return $ compare b1 b2 +compareValues _ (VChar c1) (VChar c2) = return $ compare c1 c2 +compareValues _ (VText s1) (VText s2) = return $ compare s1 s2 +compareValues p (VList xs) (VList ys) = go xs ys + where + go :: [Value] -> [Value] -> EvalM Ordering + go [] [] = return EQ + go (_:_) [] = return GT + go [] (_:_) = return LT + go (x:xs') (y:ys') = do + c <- compareValues p x y + if c == EQ + then go xs' ys' + else return c +compareValues p v1 v2 = failOnValues p [v1, v2] + +-- | Used for equality of records, sorts values by key +recordValues :: HashMap Label a -> [(Label, a)] +recordValues = List.sortBy (comparing fst) . HashMap.toList + +packChars :: Pos -> Value -> EvalM Value +packChars pos (VList xs) + | Just cs <- mapM extractChar xs = return . VText . T.pack $ cs + | otherwise = failOnValues pos xs +packChars pos v = failOnValues pos [v] + +unpackChars :: Pos -> Value -> EvalM Value +unpackChars _ (VText s) = return . VList . map VChar . T.unpack $ s +unpackChars pos v = failOnValues pos [v] + +------------------------------------------------------------ +-- HasValue class and instances + +instance (HasValue a, HasValue b) => HasValue (a -> EvalM b) where + proj (VLam f) = return $ \x -> do + r <- f (Thunk $ return $ inj x) + proj r + proj v = typeMismatch "VLam" v + inj f = VLam $ \v -> proj' v >>= fmap inj . f + +-- | A class of Haskell types that can be projected from or injected +-- into Expresso values. +class HasValue a where + proj :: Value -> EvalM a + inj :: a -> Value + +instance HasValue Value where + proj v = return v + inj = id + +instance HasValue Integer where + proj (VInt i) = return i + proj v = typeMismatch "VInt" v + inj = VInt + +instance HasValue Double where + proj (VDbl d) = return d + proj v = typeMismatch "VDbl" v + inj = VDbl + +instance HasValue Bool where + proj (VBool b) = return b + proj v = typeMismatch "VBool" v + inj = VBool + +instance HasValue Char where + proj (VChar c) = return c + proj v = typeMismatch "VChar" v + inj = VChar + +instance HasValue String where + proj (VText s) = return $ T.unpack s + proj v = typeMismatch "VText" v + inj = VText . T.pack + +instance HasValue Text where + proj (VText s) = return s + proj v = typeMismatch "VText" v + inj = VText + +instance HasValue a => HasValue (Maybe a) where + proj = choice [ ("Just", fmap Just . proj) + , ("Nothing", const $ pure Nothing) + ] + inj (Just x) = mkVariant "Just" (inj x) + inj Nothing = mkVariant "Nothing" unit + +instance {-# OVERLAPS #-} HasValue a => HasValue [a] where + proj (VList xs) = mapM proj xs + proj v = typeMismatch "VList" v + inj = VList . map inj + +instance {-# OVERLAPS #-} HasValue [Value] where + proj (VList xs) = return xs + proj v = typeMismatch "VList" v + inj = VList + +instance HasValue a => HasValue (HashMap Name a) where + proj (VRecord m) = mapM proj' m + proj v = typeMismatch "VRecord" v + inj = VRecord . fmap (Thunk . return . inj) + +instance {-# OVERLAPS #-} HasValue a => HasValue [(Name, a)] where + proj v = HashMap.toList <$> proj v + inj = inj . HashMap.fromList + +instance {-# OVERLAPS #-} HasValue (HashMap Name Thunk) where + proj (VRecord m) = return m + proj v = typeMismatch "VRecord" v + inj = VRecord + +instance {-# OVERLAPS #-} HasValue [(Name, Thunk)] where + proj v = HashMap.toList <$> proj v + inj = inj . HashMap.fromList + +instance {-# OVERLAPS #-} (HasValue a, HasValue b) => HasValue (a -> b) where + proj _ = throwError "proj not supported for pure functions" + inj f = mkStrictLam $ fmap (inj . f) . proj + +instance {-# OVERLAPS #-} (HasValue a, HasValue b, HasValue c) => HasValue (a -> b -> c) where + proj _ = throwError "proj not supported for pure functions" + inj f = inj $ \x -> inj (f x) + +instance {-# OVERLAPS #-} (HasValue a, HasValue b, HasValue c, HasValue d) => HasValue (a -> b -> c -> d) where + proj _ = throwError "proj not supported for pure functions" + inj f = inj $ \x -> inj (f x) + +instance {-# OVERLAPS #-} (HasValue a, HasValue b) => HasValue (a -> IO b) where + proj (VLam f) = return $ \x -> runEvalM' $ f (Thunk . return . inj $ x) >>= proj + proj v = typeMismatch "VLam" v + inj f = mkStrictLam $ \v -> proj v >>= \x -> inj <$> liftIO (f x) + +instance {-# OVERLAPS #-} (HasValue a, HasValue b, HasValue c) => HasValue (a -> b -> IO c) where + proj v = proj v >>= \f -> return $ \x -> f x + inj f = inj $ \x -> inj (f x) + +instance {-# OVERLAPS #-} (HasValue a, HasValue b, HasValue c, HasValue d) => HasValue (a -> b -> c -> IO d) where + proj v = proj v >>= \f -> return $ \x -> f x + inj f = inj $ \x -> inj (f x) + +-- | Throw a type mismatch error. +typeMismatch :: String -> Value -> EvalM a +typeMismatch expected v = throwError $ "Type mismatch: expected a " ++ expected ++ + ", but got: " ++ show (ppValue v) + +-- | Project out a record field, fail with a type mismatch if it is not present. +(.:) :: HasValue a => Value -> Name -> EvalM a +(.:) (VRecord m) k = case HashMap.lookup k m of + Nothing -> throwError $ "Record label " ++ show k ++ " not present" + Just v -> proj' v +(.:) v _ = typeMismatch "VRecord" v + +-- | Pair up a field name and a value. Intended to be used with @mkRecord@ or @mkVariant@. +(.=) :: Name -> Value -> (Name, Thunk) +(.=) k v = (k, Thunk . return $ v) + +-- | Convenience for implementing @proj@ for a sum type. +choice :: HasValue a => [(Name, Value -> EvalM a)] -> Value -> EvalM a +choice alts = \case + VVariant k v + | Just f <- HashMap.lookup k m -> force v >>= f + | otherwise -> throwError $ "Missing label in alternatives: " ++ show k + v -> typeMismatch "VVariant" v + where + m = HashMap.fromList alts + +-- | Convenience constructor for a record value. +mkRecord :: [(Name, Thunk)] -> Value +mkRecord = VRecord . HashMap.fromList + +-- | Convenience constructor for a variant value. +mkVariant :: Name -> Value -> Value +mkVariant name = VVariant name . Thunk . return + +-- | Unit value. Equivalent to @()@ in Haskell. +unit :: Value +unit = VRecord mempty diff --git a/src/Expresso/Parser.hs b/src/Expresso/Parser.hs --- a/src/Expresso/Parser.hs +++ b/src/Expresso/Parser.hs @@ -1,5 +1,6 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TupleSections #-} {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} @@ -17,8 +18,11 @@ module Expresso.Parser where import Control.Applicative +import qualified Control.Exception as Ex import Control.Monad import Control.Monad.Except +import Control.Monad.Writer +import Data.Bifunctor import Data.Maybe import Text.Parsec hiding (many, optional, parse, (<|>)) import Text.Parsec.Language (emptyDef) @@ -29,7 +33,11 @@ import qualified Text.Parsec.Expr as P import qualified Text.Parsec.Token as P -import Expresso.Pretty (Doc, (<+>), render, parensList, text, dquotes, vcat) +import System.FilePath +import System.Directory + +import Expresso.Pretty ( Doc, (<+>), render, parensList + , text, dquotes, vcat) import Expresso.Syntax import Expresso.Type import Expresso.Utils @@ -37,21 +45,73 @@ ------------------------------------------------------------ -- Resolve imports -resolveImports :: ExpI -> ExceptT String IO Exp -resolveImports = cataM alg where - alg (InR (K (Import path)) :*: _) = do - res <- ExceptT $ readFile path >>= return . parse path - resolveImports res - alg (InL e :*: pos) = return $ Fix (e :*: pos) +resolveImports + :: [FilePath] + -> ExpI + -- NB: ExceptT models expected failures, e.g. file not found + -> ExceptT String IO (Exp, [SynonymDecl]) +resolveImports libDirs = runWriterT . go + where + go :: ExpI -> WriterT [SynonymDecl] (ExceptT String IO) Exp + go = cataM alg + where + alg (InR (K (Import path)) :*: _) = do + (syns, e) <- lift $ do + str <- importFile path + ExceptT . return $ parse path str + tell syns + go e + alg (InL e :*: pos) = return $ Fix (e :*: pos) + -- importFile searches the provided library dirs, unless + -- an absolute path is provided. + importFile :: FilePath -> ExceptT String IO String + importFile path + | isAbsolute path = readFile' path + | otherwise = do + mfp <- lift $ findFirst libDirs + case mfp of + Just fp -> readFile' fp + Nothing -> throwError $ unwords $ + [ "Could not find imported file" + , "'" ++ path ++ "'" + , "in the following library directories:" + , show libDirs + ] + where + findFirst :: [FilePath] -> IO (Maybe FilePath) + findFirst [] = return Nothing + findFirst (dir:dirs) = do + let fp = dir path + exists <- doesFileExist fp + if exists + then return (Just fp) + else findFirst dirs + + readFile' :: FilePath -> ExceptT String IO String + readFile' fp = + ExceptT $ bimap (show :: Ex.SomeException -> String) id + <$> Ex.try (readFile fp) + ------------------------------------------------------------ -- Parser -parse :: SourceName -> String -> Either String ExpI -parse src = showError . P.parse (topLevel pExp) src +parse + :: SourceName + -> String + -> Either String ([SynonymDecl], ExpI) +parse src = showError . P.parse (topLevel pTopLevel) src topLevel p = whiteSpace *> p <* P.eof +pTopLevel = (,) <$> many (pSynonymDecl <* semi) <*> pExp + +pSynonymDecl = SynonymDecl + <$> getPosition + <*> (reserved "type" *> upperIdentifier) + <*> many pTyVar + <*> (reservedOp "=" *> pType) + pExp = addTypeAnnot <$> getPosition <*> pExp' @@ -79,8 +139,9 @@ <*> (reserved "in" *> pExp)) "let expression" -pLetDecl = (,) <$> pLetBind - <*> (reservedOp "=" *> pExp <* whiteSpace) +pLetDecl = (,,) <$> pLetBind + <*> optionMaybe (reservedOp ":" *> pTypeAnn) + <*> (reservedOp "=" *> pExp <* whiteSpace) pLam = mkLam <$> getPosition @@ -90,11 +151,11 @@ pAnnLam = mkAnnLam <$> getPosition - <*> try (many1 pAnnBind <* reservedOp "->" <* whiteSpace) + <*> try (many1 (parens pAnnBind) <* reservedOp "->" <* whiteSpace) <*> pExp' "lambda expression with type annotated argument" -pAnnBind = parens $ (,) <$> pBind <*> (reservedOp ":" *> pTypeAnn) +pAnnBind = (,) <$> pBind <*> (reservedOp ":" *> pTypeAnn) pAtom = pPrim <|> try pVar <|> parens (pSection <|> pExp) @@ -102,7 +163,7 @@ pSigSection = mkSigSection <$> getPosition <*> (reservedOp ":" *> pTypeAnn) -pVar = mkVar <$> getPosition <*> identifier +pVar = mkVar <$> getPosition <*> lowerIdentifier pPrim = pNumber <|> pBool <|> @@ -148,6 +209,7 @@ ] , [ binary "++" ListAppend P.AssocLeft , binary "::" ListCons P.AssocRight + , binary "<>" TextAppend P.AssocLeft ] , [ binary "==" Eq P.AssocLeft , binary "/=" NEq P.AssocLeft @@ -166,8 +228,7 @@ [ fun "error" ErrorPrim , fun "show" Show , fun "not" Not - , fun "foldr" ListFoldr - , fun "null" ListNull + , fun "uncons" ListUncons , fun "fix" FixPrim , fun "double" Double , fun "floor" Floor @@ -205,12 +266,17 @@ <$> getPosition <*> stringLiteral -pBind = Arg <$> identifier - <|> RecArg <$> pFieldPuns +pBind = Arg <$> lowerIdentifier + <|> RecArg <$> pFieldBind pLetBind = try (RecWildcard <$ reservedOp "{..}") <|> pBind -pFieldPuns = braces $ pRecordLabel `sepBy` comma +pFieldBind = braces $ pFieldBind' `sepBy` comma + where + pFieldBind' + = mkFieldBind + <$> pRecordLabel + <*> optionMaybe (reservedOp "=" *> lowerIdentifier) data Entry = Extend Label ExpI | Update Label ExpI @@ -278,6 +344,10 @@ <*> ((,) <$> getPosition <*> pExp) `sepBy` comma "list expression" +mkFieldBind :: Name -> Maybe Name -> (Name, Name) +mkFieldBind l (Just n) = (l, n) +mkFieldBind l Nothing = (l, l) + mkImport :: Pos -> FilePath -> ExpI mkImport pos path = withAnn pos $ InR $ K $ Import path @@ -334,8 +404,11 @@ mkVar :: Pos -> Name -> ExpI mkVar pos name = withPos pos (EVar name) -mkLet :: (Pos, (Bind Name, ExpI)) -> ExpI -> ExpI -mkLet (pos, (b, e1)) e2 = withPos pos (ELet b e1 e2) +mkLet :: (Pos, (Bind Name, Maybe Type, ExpI)) -> ExpI -> ExpI +mkLet (pos, (b, mty, e1)) e2 = withPos pos $ + case mty of + Nothing -> ELet b e1 e2 + Just t -> EAnnLet b t e1 e2 mkTertiaryOp :: Pos -> Prim -> ExpI -> ExpI -> ExpI -> ExpI mkTertiaryOp pos p x y z = mkApp pos (mkPrim pos p) [x, y, z] @@ -396,6 +469,7 @@ <|> pTBool <|> pTChar <|> pTText + <|> pTSynonym <|> pTRecord <|> pTVariant <|> pTList @@ -462,6 +536,11 @@ <$> getPosition <*> (pTyVar <|> pTWildcard) +pTSynonym = (\pos name -> withAnn pos . TSynonymF name) + <$> getPosition + <*> upperIdentifier + <*> many pType' + pTInt = pTCon TIntF "Int" pTDbl = pTCon TDblF "Double" pTBool = pTCon TBoolF "Bool" @@ -534,6 +613,7 @@ ] , P.reservedNames = [ "let", "in", "if", "then", "else", "case", "of" , "True", "False", "forall", "Eq", "Ord", "Num" + , "type" ] , P.caseSensitive = True } diff --git a/src/Expresso/Syntax.hs b/src/Expresso/Syntax.hs --- a/src/Expresso/Syntax.hs +++ b/src/Expresso/Syntax.hs @@ -46,13 +46,14 @@ | ELam (b v) r | EAnnLam (b v) t r | ELet (b v) r r + | EAnnLet (b v) t r r | EAnn r t deriving (Show, Functor, Foldable, Traversable) -- | Binders data Bind v = Arg v - | RecArg [v] + | RecArg [(v,v)] | RecWildcard deriving Show @@ -85,11 +86,11 @@ | BwdComp | Pack | Unpack + | TextAppend | ListEmpty | ListCons - | ListNull -- needed if list elems have no equality defined + | ListUncons | ListAppend - | ListFoldr | RecordEmpty -- a.k.a. Unit | RecordSelect Label | RecordExtend Label diff --git a/src/Expresso/TH/QQ.hs b/src/Expresso/TH/QQ.hs --- a/src/Expresso/TH/QQ.hs +++ b/src/Expresso/TH/QQ.hs @@ -12,7 +12,7 @@ -- -- Quasi-quoters for defining Expresso types in Haskell. -- -module Expresso.TH.QQ (expressoType) where +module Expresso.TH.QQ (expressoType, expressoTypeSyn) where import Control.Exception @@ -27,8 +27,12 @@ -- | Expresso Quasi-Quoter for type declarations. expressoType :: QuasiQuoter -expressoType = def { quoteExp = genTypeDecl } +expressoType = def { quoteExp = genTypeAnn } +-- | Expresso Quasi-Quoter for type synonym declarations. +expressoTypeSyn :: QuasiQuoter +expressoTypeSyn = def { quoteExp = genTypeSynDecl } + def :: QuasiQuoter def = QuasiQuoter { quoteExp = failure "expressions" @@ -40,10 +44,16 @@ failure kind = fail $ "This quasi-quoter does not support splicing " ++ kind -genTypeDecl :: String -> ExpQ -genTypeDecl str = do +genTypeAnn :: String -> ExpQ +genTypeAnn str = do l <- location' c <- runIO $ parseIO (P.setPosition l *> topLevel pTypeAnn) str + dataToExpQ (const Nothing) c + +genTypeSynDecl :: String -> ExpQ +genTypeSynDecl str = do + l <- location' + c <- runIO $ parseIO (P.setPosition l *> topLevel pSynonymDecl) str dataToExpQ (const Nothing) c -- | find the current location in the Haskell source file and convert it to parsec @SourcePos@. diff --git a/src/Expresso/Type.hs b/src/Expresso/Type.hs --- a/src/Expresso/Type.hs +++ b/src/Expresso/Type.hs @@ -2,12 +2,14 @@ {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} @@ -27,9 +29,10 @@ -- module Expresso.Type where -import Text.Parsec (SourcePos) -import Text.Parsec.Pos (newPos) - +import Control.Monad +import Control.Monad.Except +import Data.Data +import Data.Foldable (fold) import Data.IntMap (IntMap) import Data.Map (Map) import Data.Set (Set) @@ -37,8 +40,8 @@ import qualified Data.IntMap as IM import qualified Data.Set as S -import Data.Data -import Data.Foldable (fold) +import Text.Parsec (SourcePos) +import Text.Parsec.Pos (newPos) import Expresso.Pretty import Expresso.Utils @@ -67,6 +70,7 @@ = TForAllF [TyVar] r | TVarF TyVar | TMetaVarF MetaTv + | TSynonymF Name [r] | TIntF | TDblF | TBoolF @@ -126,6 +130,66 @@ typeEnvToList :: TypeEnv -> [(Name, Sigma)] typeEnvToList (TypeEnv m) = M.toList m +-- | Global map of type synonym definitions. +newtype Synonyms = Synonyms { unSynonym :: Map Name SynonymDecl } + deriving (Semigroup, Monoid) + +-- | A type synonym definition. +data SynonymDecl = SynonymDecl + { synonymPos :: Pos + , synonymName :: Name + , synonymParams :: [TyVar] + , synonymBody :: Type + } deriving (Show, Typeable, Data) + +-- | Lookup and expand a type synonym. +-- Returns Nothing if the lookup or expansion failed. +lookupSynonym :: Name -> [Type] -> Synonyms -> Maybe Sigma +lookupSynonym name args (Synonyms m) = do + SynonymDecl{..} <- M.lookup name m + guard $ length synonymParams == length args + return $ substTyVar synonymParams args synonymBody + +-- | Used by the REPL. +deleteSynonym :: Name -> Synonyms -> Synonyms +deleteSynonym name (Synonyms m) = + Synonyms $ M.delete name m + +-- | Checks for duplicate synonym names and free variables. +insertSynonyms + :: MonadError String m + => [SynonymDecl] + -> Synonyms + -> m Synonyms +insertSynonyms ss (Synonyms m) = + Synonyms <$> foldM f m ss + where + f m syn + | Just syn' <- M.lookup (synonymName syn) m + -- check that it's not a benign re-import of the same synonym + , (fields syn /= fields syn') = + throwError $ unwords + [ "Duplicate synonyms with name" + , "'" ++ synonymName syn ++ "'" + , "at" + , show syn --(synonymPos syn) + , "and" + , show syn' -- (synonymPos syn') + ] + | fvs <- ftv (synonymBody syn) + S.\\ S.fromList (synonymParams syn) + , not (S.null fvs) = + throwError $ unwords + [ "Free variables in type synonym definition:" + , "'" ++ synonymName syn ++ "'" + , "at" + , show (synonymPos syn) + ] + | otherwise = return $ M.insert (synonymName syn) syn m + + -- strip positional annotations + fields (SynonymDecl _ name vars body) = (name, vars, stripAnn body) + instance View TypeF Type where proj = left . unFix inj e = Fix (e :*: K dummyPos) @@ -144,6 +208,8 @@ TVar v = inj (TVarF v) pattern TMetaVar v <- (proj -> (TMetaVarF v)) where TMetaVar v = inj (TMetaVarF v) +pattern TSynonym v ts <- (proj -> (TSynonymF v ts)) where + TSynonym v ts = inj (TSynonymF v ts) pattern TInt <- (proj -> TIntF) where TInt = inj TIntF pattern TDbl <- (proj -> TDblF) where @@ -286,6 +352,7 @@ rowToMap (TRowExtend l t r) = M.insert l t (rowToMap r) rowToMap TRowEmpty = M.empty rowToMap TVar{} = M.empty -- default any row vars to empty row +rowToMap TMetaVar{} = M.empty rowToMap t = error $ "Unexpected row type: " ++ show (ppType t) @@ -293,8 +360,8 @@ -- Constraints -- | True if the supplied type of kind Star satisfies the supplied constraint -satisfies :: Type -> Constraint -> Bool -satisfies t c = +satisfies :: Synonyms -> Type -> Constraint -> Bool +satisfies syns t c = case (infer t, c) of (CNone, CNone) -> True (CStar{}, CNone) -> True @@ -303,25 +370,30 @@ (c1, c2) -> error $ "satisfies: kind mismatch: " ++ show (c1, c2) where infer :: Type -> Constraint - infer (TForAll _ t) = infer t - infer (TVar v) = tyvarConstraint v - infer (TMetaVar m) = metaConstraint m - infer TInt = CStar CNum - infer TDbl = CStar CNum - infer TBool = CStar COrd - infer TChar = CStar COrd - infer TText = CStar COrd - infer TFun{} = CNone - infer (TList t) = minC (CStar COrd) (infer t) - infer (TRecord r) = - maybe CNone (minC (CStar CEq)) $ inferFromRow r - infer (TVariant r) = + infer (TForAll _ t) = infer t + infer (TVar v) = tyvarConstraint v + infer (TMetaVar m) = metaConstraint m + infer (TSynonym n ts) = + maybe CNone infer $ lookupSynonym n ts syns + infer TInt = CStar CNum + infer TDbl = CStar CNum + infer TBool = CStar COrd + infer TChar = CStar COrd + infer TText = CStar COrd + infer TFun{} = CNone + infer (TList t) = minC (CStar COrd) $ infer t + infer (TRecord r) = -- NB: unit supports equality + maybe (CStar CEq) (minC (CStar CEq)) $ inferFromRow r + infer (TVariant r) = -- NB: void does not support equality maybe CNone (minC (CStar CEq)) $ inferFromRow r infer t = error $ "satisfies/infer: unexpected type: " ++ show t + -- infer star constraints from row types inferFromRow :: Type -> Maybe Constraint inferFromRow TVar{} = Nothing inferFromRow TMetaVar{} = Nothing + inferFromRow (TSynonym n ts) = + lookupSynonym n ts syns >>= inferFromRow inferFromRow TRowEmpty = Nothing inferFromRow (TRowExtend _ t r) = Just $ maybe (infer t) (minC (infer t)) $ inferFromRow r @@ -356,9 +428,10 @@ atomicPrec = 3 -- Precedence of t precType :: Type -> Precedence -precType (TForAll _ _) = topPrec -precType (TFun _ _) = arrPrec -precType _ = atomicPrec +precType (TForAll _ _) = topPrec +precType (TFun _ _) = arrPrec +precType (TSynonym _ _) = tcPrec +precType _ = atomicPrec -- | Print with parens if precedence arg > precedence of type itself ppType' :: Precedence -> Type -> Doc @@ -370,6 +443,9 @@ ppType (TForAll vs t) = ppForAll (vs, t) ppType (TVar v) = text $ tyvarName v ppType (TMetaVar v) = "v" <> int (metaUnique v) +ppType (TSynonym n ts) + | null ts = text n + | otherwise = text n <+> hsep (map (ppType' tcPrec) ts) ppType TInt = "Int" ppType TDbl = "Double" ppType TBool = "Bool" @@ -395,7 +471,7 @@ ppForAll :: ([TyVar], Type) -> Doc ppForAll (vars, t) | null vars = ppType' topPrec t - | otherwise = "forall" <+> (catBy space $ map (ppType . TVar) vars) <> dot + | otherwise = "forall" <+> (hsep $ map (ppType . TVar) vars) <> dot <> (let cs = concatMap ppConstraint vars in if null cs then mempty else space <> (parensList cs <+> "=>")) <+> ppType' topPrec t diff --git a/src/Expresso/TypeCheck.hs b/src/Expresso/TypeCheck.hs --- a/src/Expresso/TypeCheck.hs +++ b/src/Expresso/TypeCheck.hs @@ -8,6 +8,7 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -fmax-pmcheck-iterations=10000000 #-} -- | -- Module : Expresso.TypeCheck @@ -59,15 +60,26 @@ , tiSubst :: Subst } -type TI a = ExceptT String (ReaderT TypeEnv (State TIState)) a +data TIEnv = TIEnv + { tiTypeEnv :: TypeEnv + , tiSynonyms :: Synonyms + } +type TI a = ExceptT String (ReaderT TIEnv (State TIState)) a + -- | Type check the supplied expression. typeCheck :: Exp -> TI Sigma typeCheck e = tcRho e Nothing >>= inferSigma (getAnn e) -- | Run the type inference monad. -runTI :: TI a -> TypeEnv -> TIState -> (Either String a, TIState) -runTI t tEnv tState = runState (runReaderT (runExceptT t) tEnv) tState +runTI + :: TI a + -> TypeEnv + -> Synonyms + -> TIState + -> (Either String a, TIState) +runTI t tEnv syns tState = + runState (runReaderT (runExceptT t) (TIEnv tEnv syns)) tState -- | Initial state of the inference engine. initTIState :: TIState @@ -100,7 +112,8 @@ return $ MetaTv i prefix c getEnvTypes :: TI [Sigma] -getEnvTypes = (M.elems . unTypeEnv <$> ask) >>= mapM substType +getEnvTypes = + (M.elems . unTypeEnv <$> asks tiTypeEnv) >>= mapM substType substType :: Type -> TI Type substType t = do @@ -109,14 +122,15 @@ lookupVar :: Pos -> Name -> TI Sigma lookupVar pos name = do - TypeEnv env <- ask + TypeEnv env <- asks tiTypeEnv case M.lookup name env of Just s -> return s Nothing -> throwError $ show $ ppPos pos <+> ": unbound variable:" <+> text name extendEnv :: M.Map Name Sigma -> TI a -> TI a -extendEnv binds = local (TypeEnv binds <>) +extendEnv binds = + local $ \e -> e { tiTypeEnv = TypeEnv binds <> tiTypeEnv e } -- | Quantify over the specified type variables (all flexible). quantify :: Pos -> [MetaTv] -> Rho -> Sigma @@ -185,6 +199,19 @@ mgu t r@(TMetaVar v) = varBind (getAnn r) v t mgu (TVar u) (TVar v) | u == v = return nullSubst +mgu t1@(TSynonym n1 ts1) t2@(TSynonym n2 ts2) -- no need to expand + | n1 == n2 = mconcat <$> zipWithM mgu ts1 ts2 + | otherwise = throwError' + [ "Type synonyms do not unify:" + , ppPos (getAnn t1) <+> ":" <+> ppType t1 + , ppPos (getAnn t2) <+> ":" <+> ppType t2 + ] +mgu l@(TSynonym n1 ts1) t2 = do + t1 <- expandSynonym (getAnn l) n1 ts1 + mgu t1 t2 +mgu t1 r@(TSynonym n2 ts2) = do + t2 <- expandSynonym (getAnn r) n2 ts2 + mgu t1 t2 mgu TInt TInt = return nullSubst mgu TDbl TDbl = return nullSubst mgu TBool TBool = return nullSubst @@ -203,11 +230,21 @@ , ppPos (getAnn t2) <+> ":" <+> ppType t2 ] +expandSynonym :: Pos -> Name -> [Type] -> TI Type +expandSynonym pos name args = do + syns <- asks tiSynonyms + case lookupSynonym name args syns of + Just ty -> return ty + Nothing -> throwError' + [ "Could not expand type synonym:" + , ppPos pos <+> ":" <+> ppType (TSynonym name args) + ] + unifyRow :: Type -> Type -> TI Subst unifyRow row1@TRowExtend{} row2@TRowEmpty = throwError' $ - [ ppPos (getAnn row1) <+> ": cannot insert the label(s)" + [ ppPos (getAnn row1) <+> ": unexpected row label(s)" <+> hcat (L.intersperse comma (map text . M.keys . rowToMap $ row1)) - , "into row introduced at" <+> ppPos (getAnn row2) + , "at" <+> ppPos (getAnn row2) ] unifyRow row1@(TRowExtend label1 fieldTy1 rowTail1) row2@TRowExtend{} = do -- apply side-condition to ensure termination @@ -246,18 +283,20 @@ , "occurs in" , ppPos (getAnn t) <+> ppType t ] - | otherwise = + | otherwise = do + syns <- asks tiSynonyms case metaConstraint u of CNone -> return $ u |-> t CStar c - | t `satisfies` metaConstraint u -> return $ u |-> t + | satisfies syns t (metaConstraint u) -> + return $ u |-> t | otherwise -> - throwError' - [ "The type:" - , ppPos (getAnn t) <+> ":" <+> ppType t - , "does not satisfy the constraint:" - , ppPos pos <+> ":" <+> ppStarConstraint c - ] + throwError' + [ "The type:" + , ppPos (getAnn t) <+> ":" <+> ppType t + , "does not satisfy the constraint:" + , ppPos pos <+> ":" <+> ppStarConstraint c + ] CRow{} -> varBindRow (getAnn t) u t -- | bind the row tyvar to the row type, as long as the row type does not @@ -324,7 +363,7 @@ alg (EPrim prim :*: K pos) mty = do let sigma = tcPrim pos prim instSigma pos sigma mty - alg (ELam b e :*: K pos) Nothing = do -- TODO see Mu tCheckPats? + alg (ELam b e :*: K pos) Nothing = do varT <- newMetaVar pos CNone 'a' binds <- tcBinds pos b $ Just varT extendEnv binds $ do @@ -358,6 +397,13 @@ binds <- tcBinds pos b (Just t1) >>= mapM (inferSigma pos) extendEnv binds $ e2 mty + alg (EAnnLet b varT e1 e2 :*: K pos) mty = do + varT <- instWildcards varT + t1 <- e1 Nothing + subsCheck pos t1 varT + binds <- tcBinds pos b $ Just varT + extendEnv binds $ + e2 mty alg (EAnn e annT :*: K pos) mty = do annT <- instWildcards annT checkSigma pos e annT @@ -403,13 +449,14 @@ tcBinds :: Pos -> Bind Name -> Maybe Rho -> TI (M.Map Name Type) tcBinds pos arg Nothing = newMetaVar pos CNone 'a' >>= tcBinds pos arg . Just -tcBinds _ (Arg x) (Just ty) = - return $ M.singleton x ty -tcBinds pos (RecArg xs) (Just ty) = do - tvs <- mapM (const $ newMetaVar pos CNone 'l') xs - r <- newMetaVar pos (lacks xs) 'r' -- implicit tail - unify ty (TRecord $ mkRowType r $ zip xs tvs) - return $ M.fromList $ zip xs tvs +tcBinds _ (Arg n) (Just ty) = + return $ M.singleton n ty +tcBinds pos (RecArg bs) (Just ty) = do + let (ls, ns) = unzip bs + tvs <- mapM (const $ newMetaVar pos CNone 'l') ls + r <- newMetaVar pos (lacks ls) 'r' -- implicit tail + unify ty (TRecord $ mkRowType r $ zip ls tvs) + return $ M.fromList $ zip ns tvs tcBinds pos RecWildcard (Just ty) = do s <- gets tiSubst case apply s ty of @@ -460,11 +507,17 @@ return (argT, resT) -- used by the Repl -tcDecl :: Pos -> Bind Name -> Exp -> TI TypeEnv -tcDecl pos b e = do +tcDecl :: Pos -> Bind Name -> Maybe Type -> Exp -> TI TypeEnv +tcDecl pos b Nothing e = do t <- tcRho e Nothing binds <- tcBinds pos b (Just t) >>= mapM (inferSigma pos) - extendEnv binds ask + extendEnv binds (asks tiTypeEnv) +tcDecl pos b (Just varT) e = do + varT <- instWildcards varT + t <- tcRho e Nothing + subsCheck pos t varT + binds <- tcBinds pos b $ Just varT + extendEnv binds (asks tiTypeEnv) tcPrim :: Pos -> Prim -> Type tcPrim pos prim = annotate pos $ case prim of @@ -525,6 +578,7 @@ (TFun (TVar a) (TVar c))) Pack -> TFun (TList TChar) TText Unpack -> TFun TText (TList TChar) + TextAppend -> TFun TText (TFun TText TText) Cond -> let a = newTyVar CNone 'a' in TForAll [a] $ TFun TBool @@ -538,21 +592,23 @@ in TForAll [a] $ TFun (TVar a) (TFun (TList (TVar a)) (TList (TVar a))) - ListFoldr -> - let a = newTyVar CNone 'a' - b = newTyVar CNone 'b' - in TForAll [a,b] $ TFun (TFun (TVar a) (TFun (TVar b) (TVar b))) - (TFun (TVar b) - (TFun (TList (TVar a)) - (TVar b))) - ListNull -> - let a = newTyVar CNone 'a' - in TForAll [a] $ TFun (TList (TVar a)) TBool + ListUncons -> + let a = newTyVar CNone 'a' + listT = TList (TVar a) + resT = TRecord $ TRowExtend "head" (TVar a) + $ TRowExtend "tail" listT + $ TRowEmpty + unitT = TRecord TRowEmpty + in TForAll [a] $ TFun listT + (TVariant $ TRowExtend "Just" resT + $ TRowExtend "Nothing" unitT + $ TRowEmpty) ListAppend -> let a = newTyVar CNone 'a' in TForAll [a] $ TFun (TList (TVar a)) (TFun (TList (TVar a)) - (TList (TVar a))) -- TODO + (TList (TVar a))) + RecordEmpty -> TRecord TRowEmpty (RecordSelect label) -> let a = newTyVar CNone 'a' diff --git a/src/Repl.hs b/src/Repl.hs --- a/src/Repl.hs +++ b/src/Repl.hs @@ -1,4 +1,5 @@ {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} -- | -- Module : Main @@ -15,9 +16,10 @@ import Control.Applicative import Control.Monad (forM_) -import Control.Monad.IO.Class +import Control.Monad.Except import Control.Monad.State.Strict import Data.Char +import Data.Version import System.Console.Haskeline (InputT) import System.Console.Haskeline.MonadException () import System.Directory @@ -27,11 +29,13 @@ import qualified Text.Parsec as P import Expresso -import Expresso.Parser ( pExp, pLetDecl, topLevel +import Expresso.Parser ( pExp, pLetDecl, pSynonymDecl, topLevel , reserved, reservedOp, stringLiteral ) import Expresso.Utils +import Paths_expresso + ps1 :: String ps1 = "λ" @@ -41,11 +45,13 @@ { stateMode :: Mode , stateBuffer :: [String] , stateEnv :: Environments + , stateLibDirs :: [FilePath] } data Command = Peek ExpI | Type ExpI + | Load FilePath | ChangeCWD FilePath | BeginMulti | Reset @@ -56,18 +62,20 @@ data Line = Command Command | Term ExpI - | Decl (Bind Name) ExpI + | Decl (Bind Name) (Maybe Type) ExpI + | TypeDecl SynonymDecl | NoOp type Repl = InputT (StateT ReplState IO) main :: IO () main = do - cwd <- liftIO getCurrentDirectory - let preludePath = cwd "Prelude.x" - runRepl $ do + preludePath <- liftIO $ getDataFileName "Prelude.x" + currentDir <- liftIO getCurrentDirectory + let libDirs = [takeDirectory preludePath, currentDir] + runRepl libDirs $ do mapM_ spew - [ "Expresso REPL" + [ unwords ["Expresso", showVersion version, "REPL"] , "Type :help or :h for a list of commands" ] HL.catch @@ -103,38 +111,41 @@ process :: String -> Repl () process str = do case parseLine str of - Left err -> spew err - Right (Command c) -> doCommand c - Right (Term e) -> doEval showValue' e - Right (Decl b e) -> doDecl b e - Right NoOp -> return () + Left err -> spew err + Right (Command c) -> doCommand c + Right (Term e) -> doEval showValue' e + Right (Decl b mty e) -> doDecl b mty e + Right (TypeDecl syn) -> doTypeDecl syn + Right NoOp -> return () `HL.catch` handler where handler :: HL.SomeException -> Repl () handler ex = spew $ "Caught exception: " ++ show ex -runRepl :: Repl a -> IO a -runRepl m = do +runRepl :: [FilePath] -> Repl a -> IO a +runRepl libDirs m = do historyFile <- ( ".expresso_history") <$> getHomeDirectory let settings = HL.defaultSettings {HL.historyFile = Just historyFile} - evalStateT (HL.runInputT settings m) emptyReplState + evalStateT (HL.runInputT settings m) (emptyReplState libDirs) -emptyReplState :: ReplState -emptyReplState = ReplState - { stateMode = SingleLine - , stateBuffer = mempty - , stateEnv = initEnvironments +emptyReplState :: [FilePath] -> ReplState +emptyReplState libDirs = ReplState + { stateMode = SingleLine + , stateBuffer = mempty + , stateEnv = setLibDirs libDirs initEnvironments + , stateLibDirs = libDirs } loadPrelude :: FilePath -> Repl () loadPrelude path = do - doDecl RecWildcard $ Fix (InR (K (Import path)) :*: K dummyPos) - spew $ "Loaded Prelude from " ++ path + spew $ "Loading Prelude from " ++ path + doLoad path doCommand :: Command -> Repl () doCommand c = case c of Peek e -> doEval (return . showValue) e Type e -> doTypeOf e + Load path -> doLoad path ChangeCWD path -> liftIO $ setCurrentDirectory path Quit -> lift $ modify (setMode Quitting) BeginMulti -> lift $ modify (setMode MultiLine) @@ -145,6 +156,7 @@ , "" , " evaluate an expression" , ":peek evaluate, but not deeply" + , ":load import record expression as a module" , ":{\\n ..lines.. \\n:}\\n multiline command" , ":cd change current working directory" , ":type show the type of " @@ -163,14 +175,30 @@ Left err -> spew err Right val -> liftIO (pp val) >>= spew -doDecl :: Bind Name -> ExpI -> Repl () -doDecl b e = do +doLoad :: FilePath -> Repl () +doLoad path = + doDecl RecWildcard Nothing + $ Fix (InR (K (Import path)) :*: K dummyPos) + +doDecl :: Bind Name -> Maybe Type -> ExpI -> Repl () +doDecl b mty e = do envs <- lift $ gets stateEnv - envs'e <- liftIO $ runEvalM $ bind envs b e + envs'e <- liftIO $ runEvalM $ bind envs b mty e case envs'e of Left err -> spew err Right envs' -> lift $ modify (setEnv envs') +doTypeDecl :: SynonymDecl -> Repl () +doTypeDecl syn = do + envs <- lift $ gets stateEnv + let envs'e = runExcept + . installSynonyms [syn] + . uninstallSynonym syn + $ envs + case envs'e of + Left err -> spew err + Right envs' -> lift $ modify (setEnv envs') + doTypeOf :: ExpI -> Repl () doTypeOf e = do envs <- lift $ gets stateEnv @@ -180,7 +208,9 @@ Right sigma -> spew (showType sigma) doReset :: Repl () -doReset = lift $ modify (setEnv $ stateEnv emptyReplState) +doReset = lift $ do + libDirs <- gets stateLibDirs + modify (setEnv $ setLibDirs libDirs initEnvironments) doDumpEnv :: Repl () doDumpEnv = do @@ -194,19 +224,24 @@ | otherwise = showError $ P.parse (topLevel pLine) "" str pLine :: Parser Line -pLine = pCommand <|> P.try pTerm <|> pDecl +pLine = pCommand <|> P.try pTerm <|> pDecl <|> pTypeDecl pTerm :: Parser Line pTerm = Term <$> pExp pDecl :: Parser Line -pDecl = uncurry Decl <$> (reserved "let" *> pLetDecl) +pDecl = (\(b, mt, e) -> Decl b mt e) + <$> (reserved "let" *> pLetDecl) +pTypeDecl :: Parser Line +pTypeDecl = TypeDecl <$> pSynonymDecl + pCommand :: Parser Line pCommand = Command <$> (reservedOp ":" *> p) where p = (reserved "peek" <|> reserved "p") *> (Peek <$> pExp) <|> (reserved "type" <|> reserved "t") *> (Type <$> pExp) + <|> (reserved "load" <|> reserved "l") *> (Load <$> pFilePath) <|> reserved "cd" *> (ChangeCWD <$> pFilePath) <|> (reserved "reset" <|> reserved "r") *> pure Reset <|> (reserved "env" <|> reserved "e") *> pure DumpEnv diff --git a/src/Tests.hs b/src/Tests.hs --- a/src/Tests.hs +++ b/src/Tests.hs @@ -7,6 +7,8 @@ import Expresso +import Paths_expresso + main = defaultMain unitTests unitTests = testGroup @@ -133,7 +135,7 @@ rankNTests = testGroup "Rank-N polymorphism" [ hasValue "let f = (g : forall a. a -> a) -> {l = g True, r = g 1} in f (x -> x) == {l = True, r = 1}" True - , hasValue "let f = g -> {l = g True, r = g 1} : (forall a. a -> a) -> {l : Bool, r : Int } in f (x -> x) == {l = True, r = 1}" True , hasValue "let f = (m : forall a. { reverse : [a] -> [a] |_}) -> {l = m.reverse [True, False], r = pack (m.reverse (unpack \"abc\")) } in f (import \"Prelude.x\") == {l = [False, True], r = \"cba\"}" True + , hasValue "let f = g -> {l = g True, r = g 1} : (forall a. a -> a) -> {l : Bool, r : Int } in f (x -> x) == {l = True, r = 1}" True , hasValue "let f = (m : forall a. { reverse : [a] -> [a] |_}) -> {l = m.reverse [True, False], r = pack (m.reverse (unpack \"abc\")) } in f (import \"List.x\") == {l = [False, True], r = \"cba\"}" True ] lazyTests = testGroup @@ -145,7 +147,9 @@ hasValue :: (Eq a, Show a, HasValue a) => String -> a -> TestTree hasValue str expected = testCase str $ do - result <- evalString Nothing str + libDir <- getDataDir + let envs = setLibDirs [libDir] initEnvironments + result <- evalString' envs Nothing str case result of Left err -> assertFailure err Right actual -> assertEqual "" expected actual