expresso 0.1.1.0 → 0.1.2.0
raw patch · 16 files changed
+1441/−837 lines, 16 filesdep −terminfoPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependencies removed: terminfo
API changes (from Hackage documentation)
+ Expresso: EAnnLet :: b v -> t -> r -> r -> ExpF v b t r
+ Expresso: SynonymDecl :: Pos -> Name -> [TyVar] -> Type -> SynonymDecl
+ Expresso: TSynonymF :: Name -> [r] -> TypeF r
+ Expresso: [synonymBody] :: SynonymDecl -> Type
+ Expresso: [synonymName] :: SynonymDecl -> Name
+ Expresso: [synonymParams] :: SynonymDecl -> [TyVar]
+ Expresso: [synonymPos] :: SynonymDecl -> Pos
+ Expresso: data SynonymDecl
+ Expresso: installSynonyms :: MonadError String m => [SynonymDecl] -> Environments -> m Environments
+ Expresso: setLibDirs :: [FilePath] -> Environments -> Environments
+ Expresso: uninstallSynonym :: SynonymDecl -> Environments -> Environments
+ Expresso.TH.QQ: expressoTypeSyn :: QuasiQuoter
- Expresso: RecArg :: [v] -> Bind v
+ Expresso: RecArg :: [(v, v)] -> Bind v
- Expresso: bind :: Environments -> Bind Name -> ExpI -> EvalM Environments
+ Expresso: bind :: Environments -> Bind Name -> Maybe Type -> ExpI -> EvalM Environments
Files
- CHANGELOG.md +9/−0
- Prelude.x +0/−108
- README.md +28/−13
- expresso.cabal +9/−13
- lib/List.x +145/−0
- lib/Prelude.x +111/−0
- lib/Text.x +119/−0
- src/Expresso.hs +71/−26
- src/Expresso/Eval.hs +567/−557
- src/Expresso/Parser.hs +101/−21
- src/Expresso/Syntax.hs +4/−3
- src/Expresso/TH/QQ.hs +14/−4
- src/Expresso/Type.hs +100/−24
- src/Expresso/TypeCheck.hs +94/−38
- src/Repl.hs +63/−28
- src/Tests.hs +6/−2
CHANGELOG.md view
@@ -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.
− Prelude.x
@@ -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 -> <Just : a, Nothing : {}>;-- nothing = Nothing{}- : forall a. <Just : a, Nothing : {}>;-- maybe = b f m -> case m of { Just a -> f a, Nothing{} -> b }- : forall a b. b -> (a -> b) -> <Just : 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 = x -> Left x- : forall a b. a -> <Left : a, Right : b>;-- right = x -> Right x- : forall a b. b -> <Left : a, Right : b>;-- either = f g m -> case m of { Left a -> f a, Right b -> g b }- : forall a b c. (a -> c) -> (b -> c) -> <Left : a, Right : b> -> 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- }
README.md view
@@ -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 -> <Just : a, Nothing : {}>;+ type Maybe a = <Just : a, Nothing : {}>; - nothing = Nothing{} : forall a. <Just : a, Nothing : {}>;+ 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 `<Just : a, Nothing : {}>`. 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 `<term> : <type>` , 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_ = <Lambda>, 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 } ] }
expresso.cabal view
@@ -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
+ lib/List.x view
@@ -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+ }
+ lib/Prelude.x view
@@ -0,0 +1,111 @@+--+-- Expresso Prelude+--++type Maybe a = <Just : a, Nothing : {}>;+type Either a b = <Left : a, Right : 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+ }
+ lib/Text.x view
@@ -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+ }
src/Expresso.hs view
@@ -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 "<unknown>" str+ (_, top) <- ExceptT $ return $ Parser.parse "<unknown>" 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 "<unknown>" str- ExceptT $ evalWithEnv envs (maybe id validate mty $ top)+ (ss, top) <- ExceptT $ return $ Parser.parse "<unknown>" 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' }
src/Expresso/Eval.hs view
@@ -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 _ = "<Thunk>" - -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 _) = "<Lambda>" -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 <+> "=" <+> "<Thunk>" -ppValue (VVariant l _) = text l <+> "<Thunk>" - --- | 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 _ = "<Thunk>"++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 _) = "<Lambda>"+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 <+> "=" <+> "<Thunk>"+ppValue (VVariant l _) = text l <+> "<Thunk>"++-- | 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
src/Expresso/Parser.hs view
@@ -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 }
src/Expresso/Syntax.hs view
@@ -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
src/Expresso/TH/QQ.hs view
@@ -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@.
src/Expresso/Type.hs view
@@ -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
src/Expresso/TypeCheck.hs view
@@ -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'
src/Repl.hs view
@@ -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 @@ , "" , "<expression> evaluate an expression" , ":peek <expression> evaluate, but not deeply"+ , ":load <filename> import record expression as a module" , ":{\\n ..lines.. \\n:}\\n multiline command" , ":cd <path> change current working directory" , ":type <term> show the type of <term>"@@ -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) "<interactive>" 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
src/Tests.hs view
@@ -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