ehmry/dhall-haskell
ehmry/dhall-haskell
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Add support for Maybe

Browse Source
This commit is contained in:
Gabriel Gonzalez 2016-09-08 17:02:11 -07:00
parent c268c84080
commit c5967955f9
3 changed files with 77 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

61
src/Dhall/Core.hs
View File

@ -59,10 +59,10 @@ import qualified Data.List
import qualified Data.Map
import qualified Data.Text.Lazy as Text
import qualified Data.Text.Lazy.Builder as Builder
import qualified Filesystem.Path.CurrentOS as Filesystem
import qualified Dhall.Context as Context
import qualified Data.Vector
import qualified Data.Vector.Mutable
import qualified Dhall.Context as Context
import qualified Filesystem.Path.CurrentOS as Filesystem
{-| Constants for the calculus of constructions
@ -193,6 +193,12 @@ data Expr a
| TextLit Text
-- | > TextAppend x y ~ x ++ y
| TextAppend (Expr a) (Expr a)
-- | > Maybe a ~ Maybe a
| Maybe (Expr a)
-- | > Nothing ~ Nothing
| Nothing_
-- | > Just_ ~ Just
| Just_
-- | > List t ~ [ t ]
| List (Expr a)
-- | > ListLit t [x, y, z] ~ [ x, y, z : t ]
@ -250,6 +256,9 @@ instance Monad Expr where
Text >>= _ = Text
TextLit t >>= _ = TextLit t
TextAppend l r >>= k = TextAppend (l >>= k) (r >>= k)
Maybe t >>= k = Maybe (t >>= k)
Nothing_ >>= _ = Nothing_
Just_ >>= _ = Just_
List t >>= k = List (t >>= k)
ListLit t es >>= k = ListLit (t >>= k) es'
where
@ -326,6 +335,9 @@ instance Eq a => Eq (Expr a) where
go (TextAppend xL yL) (TextAppend xR yR) = do
b1 <- go xL xR
if b1 then go yL yR else return False
go (Maybe tL) (Maybe tR) = go tL tR
go Nothing_ Nothing_ = return True
go Just_ Just_ = return True
go (List tL) (List tR) = go tL tR
go (ListLit tL esL) (ListLit tR esR) = do
b1 <- go tL tR
@ -428,6 +440,13 @@ instance Buildable a => Buildable (Expr a)
Text -> "Text"
TextLit t -> build (show t)
TextAppend x y -> go True False x <> " ++ " <> go True False y
Maybe t ->
(if parenApp then "(" else "")
<> "Maybe "
<> go True True t
<> (if parenApp then ")" else "")
Nothing_ -> "Nothing"
Just_ -> "Just"
List t -> "[ " <> go False False t <> " ]"
ListLit t es ->
if null es
@ -474,6 +493,8 @@ data TypeMessage
| AnnotMismatch (Expr X) (Expr X)
| Untyped Const
| InvalidElement Int (Expr X) (Expr X) (Expr X)
| InvalidMaybeTypeParam (Expr X) (Expr X)
| InvalidListTypeParam (Expr X) (Expr X)
| InvalidListType (Expr X) (Expr X)
| InvalidFieldType (Expr X)
| NotARecord (Expr X)
@ -510,10 +531,26 @@ instance Buildable TypeMessage where
<> "Inferred type: " <> build expr2 <> "\n"
build (Untyped c ) =
"Error: " <> build c <> " has no type\n"
build (InvalidMaybeTypeParam t k ) =
"Error: Invalid optional type\n"
<> "\n"
-- TODO: Wrap in parentheses if necessary
<> "Invalid type: Maybe " <> build t <> "\n"
<> " ^\n"
<> "Expected kind: *\n"
<> "Actual kind: " <> build k <> "\n"
build (InvalidListTypeParam t k ) =
"Error: Invalid list type\n"
<> "\n"
<> "Invalid type: [ " <> build t <> " ]\n"
<> " ^\n"
<> "Expected kind: *\n"
<> "Actual kind: " <> build k <> "\n"
build (InvalidListType t k ) =
"Error: Type of the wrong kind for list elements\n"
<> "\n" <> "Invalid type: [nil " <> build t <> " ...\n"
<> " ^\n"
<> "\n"
<> "Invalid type: [ ... : " <> build t <> " ]\n"
<> " ^\n"
<> "Expected kind: *\n"
<> "Actual kind: " <> build k <> "\n"
build (InvalidElement n x t t' ) =
@ -651,6 +688,7 @@ subst x e (BoolOr l r) = BoolOr (subst x e l) (subst x e r)
subst x e (NaturalPlus l r) = NaturalPlus (subst x e l) (subst x e r)
subst x e (NaturalTimes l r) = NaturalTimes (subst x e l) (subst x e r)
subst x e (TextAppend l r) = TextAppend (subst x e l) (subst x e r)
subst x e (Maybe t ) = Maybe (subst x e t)
subst x e (List t ) = List (subst x e t)
subst x e (ListLit t es ) = ListLit (subst x e t) es'
where
@ -817,11 +855,21 @@ typeWith ctx e@(TextAppend l r ) = do
Text -> return ()
_ -> Left (TypeError ctx e (CantAppend r tr))
return Text
typeWith ctx e@(Maybe t ) = do
s <- fmap normalize (typeWith ctx t)
case s of
Const Star -> return ()
_ -> Left (TypeError ctx e (InvalidMaybeTypeParam t s))
return (Const Star)
typeWith _ Nothing_ = do
return (Pi "a" (Const Star) (Maybe "a"))
typeWith _ Just_ = do
return (Pi "a" (Const Star) (Pi "_" "a" (Maybe "a")))
typeWith ctx e@(List t ) = do
s <- fmap normalize (typeWith ctx t)
case normalize s of
case s of
Const Star -> return ()
_ -> Left (TypeError ctx e (InvalidListType t s))
_ -> Left (TypeError ctx e (InvalidListTypeParam t s))
return (Const Star)
typeWith ctx e@(ListLit t xs ) = do
s <- fmap normalize (typeWith ctx t)
@ -988,6 +1036,7 @@ normalize e = case e of
where
x' = normalize x
y' = normalize y
Maybe t -> Maybe (normalize t)
List t -> List (normalize t)
ListLit t es -> ListLit (normalize t) (fmap normalize es)
RecordLit kvs -> RecordLit (fmap normalize kvs)

19
src/Dhall/Lexer.x
View File

@ -26,6 +26,7 @@ import Prelude hiding (FilePath)
import qualified Control.Monad.Trans.State.Strict as State
import qualified Data.Text.Lazy as Text
import qualified Dhall.Core
import qualified Filesystem.Path.CurrentOS as Filesystem
}
@ -81,6 +82,9 @@ tokens :-
"Integer" { \_ -> yield Integer }
"Double" { \_ -> yield Double }
"Text" { \_ -> yield Text }
"Maybe" { \_ -> yield Maybe }
"Nothing" { \_ -> yield Nothing_ }
"Just" { \_ -> yield Just_ }
"List/build" { \_ -> yield ListBuild }
"List/fold" { \_ -> yield ListFold }
$fst $labelchar* | "(" $opchar+ ")" { \t -> yield (Label t) }
@ -163,11 +167,11 @@ data AlexInput = AlexInput
alexGetByte :: AlexInput -> Maybe (Word8,AlexInput)
alexGetByte (AlexInput c bytes text) = case bytes of
b:ytes -> Just (b, AlexInput c ytes text)
b:ytes -> Prelude.Just (b, AlexInput c ytes text)
[] -> case Text.uncons text of
Nothing -> Nothing
Just (t, ext) -> case encode t of
(b, ytes) -> Just (b, AlexInput t ytes ext)
Prelude.Nothing -> Prelude.Nothing
Prelude.Just (t, ext) -> case encode t of
(b, ytes) -> Prelude.Just (b, AlexInput t ytes ext)
alexInputPrevChar :: AlexInput -> Char
alexInputPrevChar = prevChar
@ -185,8 +189,8 @@ lexExpr text = for (go (AlexInput '\n' [] text)) tag
yield (LocatedToken token pos)
go input = case alexScan input 0 of
AlexEOF -> return Nothing
AlexError (AlexInput _ _ text) -> return (Just text)
AlexEOF -> return Prelude.Nothing
AlexError (AlexInput _ _ text) -> return (Prelude.Just text)
AlexSkip input' len -> do
lift (column += len)
go input'
@ -237,6 +241,9 @@ data Token
| Text
| Double
| DoubleLit Double
| Maybe
| Nothing_
| Just_
| ListBuild
| ListFold
| TextLit Text

12
src/Dhall/Parser.hs
View File

@ -27,7 +27,7 @@ import Filesystem.Path.CurrentOS (FilePath)
import Dhall.Core (Const(..), Path(..), Let(..), Expr(..))
import Dhall.Lexer (LocatedToken(..), Position(..), Token)
import Numeric.Natural (Natural)
import Prelude hiding (FilePath)
import Prelude hiding (FilePath, Maybe(..))
import Text.Earley
import qualified Data.Map
@ -35,6 +35,7 @@ import qualified Data.Vector
import qualified Pipes.Prelude as Pipes
import qualified Data.Text.Lazy as Text
import qualified Dhall.Lexer as Lexer
import qualified Prelude
match :: Token -> Prod r Token LocatedToken Token
match t = fmap Lexer.token (satisfy predicate) <?> t
@ -153,6 +154,9 @@ expr = mdo
bexpr <- rule
( (App <$> bexpr <*> aexpr)
<|> ( Maybe
<$> (match Lexer.Maybe *> bexpr)
)
<|> ( BoolAnd
<$> bexpr
<*> (match Lexer.And *> bexpr)
@ -186,6 +190,8 @@ expr = mdo
<|> (match Lexer.Integer *> pure Integer)
<|> (match Lexer.Double *> pure Double)
<|> (match Lexer.Text *> pure Text)
<|> (match Lexer.Nothing_ *> pure Nothing_)
<|> (match Lexer.Just_ *> pure Just_)
<|> (match Lexer.ListBuild *> pure ListBuild)
<|> (match Lexer.ListFold *> pure ListFold)
<|> ( List
@ -295,8 +301,8 @@ exprFromText text = evalState (runExceptT m) (Lexer.P 1 0)
m = do
(locatedTokens, mtxt) <- lift (Pipes.toListM' (Lexer.lexExpr text))
case mtxt of
Nothing -> return ()
Just txt -> do
Prelude.Nothing -> return ()
Prelude.Just txt -> do
pos <- lift get
throwE (ParseError pos (Lexing txt))
let (parses, Report _ needed found) =