Add Note constructor
This commit is contained in:
Gabriel Gonzalez
parent
fa6619d892
commit
2909f8871b
|
|
@ -318,6 +318,7 @@ import Data.ByteString.Lazy (ByteString)
|
|||
import Data.Text.Lazy (Text)
|
||||
import Data.Vector (Vector)
|
||||
import Dhall.Core (Expr(..))
|
||||
import Dhall.Parser (Src)
|
||||
import Dhall.TypeCheck (X)
|
||||
import GHC.Generics
|
||||
import Numeric.Natural (Natural)
|
||||
|
|
@ -386,8 +387,8 @@ input (Type {..}) bytes = do
|
|||
> input :: Type a -> Text -> IO a
|
||||
-}
|
||||
data Type a = Type
|
||||
{ extract :: Expr X -> Maybe a
|
||||
, expected :: Expr X
|
||||
{ extract :: Expr X X -> Maybe a
|
||||
, expected :: Expr Src X
|
||||
}
|
||||
deriving (Functor)
|
||||
|
||||
|
|
|
|||
|
|
@ -51,6 +51,7 @@ module Dhall.Core (
|
|||
#else
|
||||
import Control.Applicative (Applicative(..), (<$>))
|
||||
#endif
|
||||
import Data.Bifunctor (Bifunctor(..))
|
||||
import Data.Foldable
|
||||
import Data.Map (Map)
|
||||
import Data.Monoid ((<>))
|
||||
|
|
@ -157,38 +158,38 @@ instance Buildable Var where
|
|||
build = buildVar
|
||||
|
||||
-- | Syntax tree for expressions
|
||||
data Expr a
|
||||
data Expr s a
|
||||
-- | > Const c ~ c
|
||||
= Const Const
|
||||
-- | > Var (V x 0) ~ x
|
||||
-- > Var (V x n) ~ x@n
|
||||
| Var Var
|
||||
-- | > Lam x A b ~ λ(x : A) -> b
|
||||
| Lam Text (Expr a) (Expr a)
|
||||
| Lam Text (Expr s a) (Expr s a)
|
||||
-- | > Pi "_" A B ~ A -> B
|
||||
-- > Pi x A B ~ ∀(x : A) -> B
|
||||
| Pi Text (Expr a) (Expr a)
|
||||
| Pi Text (Expr s a) (Expr s a)
|
||||
-- | > App f a ~ f a
|
||||
| App (Expr a) (Expr a)
|
||||
| App (Expr s a) (Expr s a)
|
||||
-- | > Let x Nothing r e ~ let x = r in e
|
||||
-- > Let x (Just t) r e ~ let x : t = r in e
|
||||
| Let Text (Maybe (Expr a)) (Expr a) (Expr a)
|
||||
| Let Text (Maybe (Expr s a)) (Expr s a) (Expr s a)
|
||||
-- | > Annot x t ~ x : t
|
||||
| Annot (Expr a) (Expr a)
|
||||
| Annot (Expr s a) (Expr s a)
|
||||
-- | > Bool ~ Bool
|
||||
| Bool
|
||||
-- | > BoolLit b ~ b
|
||||
| BoolLit Bool
|
||||
-- | > BoolAnd x y ~ x && y
|
||||
| BoolAnd (Expr a) (Expr a)
|
||||
| BoolAnd (Expr s a) (Expr s a)
|
||||
-- | > BoolOr x y ~ x || y
|
||||
| BoolOr (Expr a) (Expr a)
|
||||
| BoolOr (Expr s a) (Expr s a)
|
||||
-- | > BoolEQ x y ~ x == y
|
||||
| BoolEQ (Expr a) (Expr a)
|
||||
| BoolEQ (Expr s a) (Expr s a)
|
||||
-- | > BoolNE x y ~ x /= y
|
||||
| BoolNE (Expr a) (Expr a)
|
||||
| BoolNE (Expr s a) (Expr s a)
|
||||
-- | > BoolIf x y z ~ if x then y else z
|
||||
| BoolIf (Expr a) (Expr a) (Expr a)
|
||||
| BoolIf (Expr s a) (Expr s a) (Expr s a)
|
||||
-- | > Natural ~ Natural
|
||||
| Natural
|
||||
-- | > NaturalLit n ~ +n
|
||||
|
|
@ -204,9 +205,9 @@ data Expr a
|
|||
-- | > NaturalOdd ~ Natural/odd
|
||||
| NaturalOdd
|
||||
-- | > NaturalPlus x y ~ x + y
|
||||
| NaturalPlus (Expr a) (Expr a)
|
||||
| NaturalPlus (Expr s a) (Expr s a)
|
||||
-- | > NaturalTimes x y ~ x * y
|
||||
| NaturalTimes (Expr a) (Expr a)
|
||||
| NaturalTimes (Expr s a) (Expr s a)
|
||||
-- | > Integer ~ Integer
|
||||
| Integer
|
||||
-- | > IntegerLit n ~ n
|
||||
|
|
@ -220,11 +221,11 @@ data Expr a
|
|||
-- | > TextLit t ~ t
|
||||
| TextLit Builder
|
||||
-- | > TextAppend x y ~ x ++ y
|
||||
| TextAppend (Expr a) (Expr a)
|
||||
| TextAppend (Expr s a) (Expr s a)
|
||||
-- | > List ~ List
|
||||
| List
|
||||
-- | > ListLit t [x, y, z] ~ [x, y, z] : List t
|
||||
| ListLit (Expr a) (Vector (Expr a))
|
||||
| ListLit (Expr s a) (Vector (Expr s a))
|
||||
-- | > ListBuild ~ List/build
|
||||
| ListBuild
|
||||
-- | > ListFold ~ List/fold
|
||||
|
|
@ -243,33 +244,35 @@ data Expr a
|
|||
| Maybe
|
||||
-- | > MaybeLit t [e] ~ [e] : Maybe t
|
||||
-- > MaybeLit t [] ~ [] : Maybe t
|
||||
| MaybeLit (Expr a) (Vector (Expr a))
|
||||
| MaybeLit (Expr s a) (Vector (Expr s a))
|
||||
-- | > MaybeFold ~ Maybe/fold
|
||||
| MaybeFold
|
||||
-- | > Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }
|
||||
| Record (Map Text (Expr a))
|
||||
| Record (Map Text (Expr s a))
|
||||
-- | > RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }
|
||||
| RecordLit (Map Text (Expr a))
|
||||
| RecordLit (Map Text (Expr s a))
|
||||
-- | > Union [(k1, t1), (k2, t2)] ~ < k1 : t1, k2 : t2 >
|
||||
| Union (Map Text (Expr a))
|
||||
| Union (Map Text (Expr s a))
|
||||
-- | > UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1, k2 : t2, k3 : t3 >
|
||||
| UnionLit Text (Expr a) (Map Text (Expr a))
|
||||
| UnionLit Text (Expr s a) (Map Text (Expr s a))
|
||||
-- | > Merge x y ~ x ∧ y
|
||||
| Merge (Expr a) (Expr a)
|
||||
| Merge (Expr s a) (Expr s a)
|
||||
-- | > Apply x y t ~ apply x y : t
|
||||
| Apply (Expr a) (Expr a) (Expr a)
|
||||
| Apply (Expr s a) (Expr s a) (Expr s a)
|
||||
-- | > Field e x ~ e.x
|
||||
| Field (Expr a) Text
|
||||
| Field (Expr s a) Text
|
||||
-- | > Note s x ~ e
|
||||
| Note s (Expr s a)
|
||||
-- | > Embed path ~ path
|
||||
| Embed a
|
||||
deriving (Functor, Foldable, Traversable, Show)
|
||||
|
||||
instance Applicative Expr where
|
||||
instance Applicative (Expr s) where
|
||||
pure = Embed
|
||||
|
||||
(<*>) = Control.Monad.ap
|
||||
|
||||
instance Monad Expr where
|
||||
instance Monad (Expr s) where
|
||||
return = pure
|
||||
|
||||
Const c >>= _ = Const c
|
||||
|
|
@ -321,9 +324,65 @@ instance Monad Expr where
|
|||
Merge x y >>= k = Merge (x >>= k) (y >>= k)
|
||||
Apply x y t >>= k = Apply (x >>= k) (y >>= k) (t >>= k)
|
||||
Field r x >>= k = Field (r >>= k) x
|
||||
Note a b >>= k = Note a (b >>= k)
|
||||
Embed r >>= k = k r
|
||||
|
||||
instance IsString (Expr a)
|
||||
instance Bifunctor Expr where
|
||||
first _ (Const a ) = Const a
|
||||
first _ (Var a ) = Var a
|
||||
first k (Lam a b c ) = Lam a (first k b) (first k c)
|
||||
first k (Pi a b c ) = Pi a (first k b) (first k c)
|
||||
first k (App a b ) = App (first k a) (first k b)
|
||||
first k (Let a b c d ) = Let a (fmap (first k) b) (first k c) (first k d)
|
||||
first k (Annot a b ) = Annot (first k a) (first k b)
|
||||
first _ Bool = Bool
|
||||
first _ (BoolLit a ) = BoolLit a
|
||||
first k (BoolAnd a b ) = BoolAnd (first k a) (first k b)
|
||||
first k (BoolOr a b ) = BoolOr (first k a) (first k b)
|
||||
first k (BoolEQ a b ) = BoolEQ (first k a) (first k b)
|
||||
first k (BoolNE a b ) = BoolNE (first k a) (first k b)
|
||||
first k (BoolIf a b c ) = BoolIf (first k a) (first k b) (first k c)
|
||||
first _ Natural = Natural
|
||||
first _ (NaturalLit a ) = NaturalLit a
|
||||
first _ NaturalFold = NaturalFold
|
||||
first _ NaturalBuild = NaturalBuild
|
||||
first _ NaturalIsZero = NaturalIsZero
|
||||
first _ NaturalEven = NaturalEven
|
||||
first _ NaturalOdd = NaturalOdd
|
||||
first k (NaturalPlus a b ) = NaturalPlus (first k a) (first k b)
|
||||
first k (NaturalTimes a b) = NaturalTimes (first k a) (first k b)
|
||||
first _ Integer = Integer
|
||||
first _ (IntegerLit a ) = IntegerLit a
|
||||
first _ Double = Double
|
||||
first _ (DoubleLit a ) = DoubleLit a
|
||||
first _ Text = Text
|
||||
first _ (TextLit a ) = TextLit a
|
||||
first k (TextAppend a b ) = TextAppend (first k a) (first k b)
|
||||
first _ List = List
|
||||
first k (ListLit a b ) = ListLit (first k a) (fmap (first k) b)
|
||||
first _ ListBuild = ListBuild
|
||||
first _ ListFold = ListFold
|
||||
first _ ListLength = ListLength
|
||||
first _ ListHead = ListHead
|
||||
first _ ListLast = ListLast
|
||||
first _ ListIndexed = ListIndexed
|
||||
first _ ListReverse = ListReverse
|
||||
first _ Maybe = Maybe
|
||||
first k (MaybeLit a b ) = MaybeLit (first k a) (fmap (first k) b)
|
||||
first _ MaybeFold = MaybeFold
|
||||
first k (Record a ) = Record (fmap (first k) a)
|
||||
first k (RecordLit a ) = RecordLit (fmap (first k) a)
|
||||
first k (Union a ) = Union (fmap (first k) a)
|
||||
first k (UnionLit a b c ) = UnionLit a (first k b) (fmap (first k) c)
|
||||
first k (Merge a b ) = Merge (first k a) (first k b)
|
||||
first k (Apply a b c ) = Apply (first k a) (first k b) (first k c)
|
||||
first k (Field a b ) = Field (first k a) b
|
||||
first k (Note a b ) = Note (k a) (first k b)
|
||||
first _ (Embed a ) = Embed a
|
||||
|
||||
second = fmap
|
||||
|
||||
instance IsString (Expr s a)
|
||||
where
|
||||
fromString str = Var (fromString str)
|
||||
|
||||
|
|
@ -364,14 +423,14 @@ buildText :: Builder -> Builder
|
|||
buildText a = build (show a)
|
||||
|
||||
-- | Builder corresponding to the @Expr0@ parser in "Dhall.Parser"
|
||||
buildExpr0 :: Buildable a => Expr a -> Builder
|
||||
buildExpr0 :: Buildable a => Expr s a -> Builder
|
||||
buildExpr0 (Annot a b) =
|
||||
buildExpr1 a <> " : " <> buildExpr0 b
|
||||
buildExpr0 a =
|
||||
buildExpr1 a
|
||||
|
||||
-- | Builder corresponding to the @Expr1@ parser in "Dhall.Parser"
|
||||
buildExpr1 :: Buildable a => Expr a -> Builder
|
||||
buildExpr1 :: Buildable a => Expr s a -> Builder
|
||||
buildExpr1 (Lam a b c) =
|
||||
"λ("
|
||||
<> buildLabel a
|
||||
|
|
@ -437,32 +496,32 @@ buildExpr1 a =
|
|||
buildExpr2 a
|
||||
|
||||
-- | Builder corresponding to the @Expr2@ parser in "Dhall.Parser"
|
||||
buildExpr2 :: Buildable a => Expr a -> Builder
|
||||
buildExpr2 :: Buildable a => Expr s a -> Builder
|
||||
buildExpr2 (BoolEQ a b) = buildExpr2 a <> " == " <> buildExpr2 b
|
||||
buildExpr2 (BoolNE a b) = buildExpr2 a <> " /= " <> buildExpr2 b
|
||||
buildExpr2 a = buildExpr3 a
|
||||
|
||||
-- | Builder corresponding to the @Expr3@ parser in "Dhall.Parser"
|
||||
buildExpr3 :: Buildable a => Expr a -> Builder
|
||||
buildExpr3 :: Buildable a => Expr s a -> Builder
|
||||
buildExpr3 (BoolOr a b) = buildExpr3 a <> " || " <> buildExpr3 b
|
||||
buildExpr3 (NaturalPlus a b) = buildExpr3 a <> " + " <> buildExpr3 b
|
||||
buildExpr3 (TextAppend a b) = buildExpr3 a <> " ++ " <> buildExpr3 b
|
||||
buildExpr3 a = buildExpr4 a
|
||||
|
||||
-- | Builder corresponding to the @Expr4@ parser in "Dhall.Parser"
|
||||
buildExpr4 :: Buildable a => Expr a -> Builder
|
||||
buildExpr4 :: Buildable a => Expr s a -> Builder
|
||||
buildExpr4 (BoolAnd a b) = buildExpr4 a <> " && " <> buildExpr4 b
|
||||
buildExpr4 (NaturalTimes a b) = buildExpr4 a <> " * " <> buildExpr4 b
|
||||
buildExpr4 (Merge a b) = buildExpr4 a <> " ∧ " <> buildExpr4 b
|
||||
buildExpr4 a = buildExpr5 a
|
||||
|
||||
-- | Builder corresponding to the @Expr5@ parser in "Dhall.Parser"
|
||||
buildExpr5 :: Buildable a => Expr a -> Builder
|
||||
buildExpr5 :: Buildable a => Expr s a -> Builder
|
||||
buildExpr5 (App a b) = buildExpr5 a <> " " <> buildExpr6 b
|
||||
buildExpr5 a = buildExpr6 a
|
||||
|
||||
-- | Builder corresponding to the @Expr6@ parser in "Dhall.Parser"
|
||||
buildExpr6 :: Buildable a => Expr a -> Builder
|
||||
buildExpr6 :: Buildable a => Expr s a -> Builder
|
||||
buildExpr6 (Var a) =
|
||||
buildVar a
|
||||
buildExpr6 (Const k) =
|
||||
|
|
@ -545,54 +604,54 @@ buildVar (V x 0) = buildLabel x
|
|||
buildVar (V x n) = buildLabel x <> "@" <> buildNumber n
|
||||
|
||||
-- | Builder corresponding to the @Elems@ parser in "Dhall.Parser"
|
||||
buildElems :: Buildable a => [Expr a] -> Builder
|
||||
buildElems :: Buildable a => [Expr s a] -> Builder
|
||||
buildElems [] = ""
|
||||
buildElems [a] = buildExpr0 a
|
||||
buildElems (a:bs) = buildExpr0 a <> ", " <> buildElems bs
|
||||
|
||||
-- | Builder corresponding to the @RecordLit@ parser in "Dhall.Parser"
|
||||
buildRecordLit :: Buildable a => Map Text (Expr a) -> Builder
|
||||
buildRecordLit :: Buildable a => Map Text (Expr s a) -> Builder
|
||||
buildRecordLit a | Data.Map.null a =
|
||||
"{=}"
|
||||
buildRecordLit a =
|
||||
"{ " <> buildFieldValues (Data.Map.toList a) <> " }"
|
||||
|
||||
-- | Builder corresponding to the @FieldValues@ parser in "Dhall.Parser"
|
||||
buildFieldValues :: Buildable a => [(Text, Expr a)] -> Builder
|
||||
buildFieldValues :: Buildable a => [(Text, Expr s a)] -> Builder
|
||||
buildFieldValues [] = ""
|
||||
buildFieldValues [a] = buildFieldValue a
|
||||
buildFieldValues (a:bs) = buildFieldValue a <> ", " <> buildFieldValues bs
|
||||
|
||||
-- | Builder corresponding to the @FieldValue@ parser in "Dhall.Parser"
|
||||
buildFieldValue :: Buildable a => (Text, Expr a) -> Builder
|
||||
buildFieldValue :: Buildable a => (Text, Expr s a) -> Builder
|
||||
buildFieldValue (a, b) = buildLabel a <> " = " <> buildExpr0 b
|
||||
|
||||
-- | Builder corresponding to the @Record@ parser in "Dhall.Parser"
|
||||
buildRecord :: Buildable a => Map Text (Expr a) -> Builder
|
||||
buildRecord :: Buildable a => Map Text (Expr s a) -> Builder
|
||||
buildRecord a | Data.Map.null a =
|
||||
"{}"
|
||||
buildRecord a =
|
||||
"{ " <> buildFieldTypes (Data.Map.toList a) <> " }"
|
||||
|
||||
-- | Builder corresponding to the @FieldTypes@ parser in "Dhall.Parser"
|
||||
buildFieldTypes :: Buildable a => [(Text, Expr a)] -> Builder
|
||||
buildFieldTypes :: Buildable a => [(Text, Expr s a)] -> Builder
|
||||
buildFieldTypes [] = ""
|
||||
buildFieldTypes [a] = buildFieldType a
|
||||
buildFieldTypes (a:bs) = buildFieldType a <> ", " <> buildFieldTypes bs
|
||||
|
||||
-- | Builder corresponding to the @FieldType@ parser in "Dhall.Parser"
|
||||
buildFieldType :: Buildable a => (Text, Expr a) -> Builder
|
||||
buildFieldType :: Buildable a => (Text, Expr s a) -> Builder
|
||||
buildFieldType (a, b) = buildLabel a <> " : " <> buildExpr0 b
|
||||
|
||||
-- | Builder corresponding to the @Union@ parser in "Dhall.Parser"
|
||||
buildUnion :: Buildable a => Map Text (Expr a) -> Builder
|
||||
buildUnion :: Buildable a => Map Text (Expr s a) -> Builder
|
||||
buildUnion a | Data.Map.null a =
|
||||
"<>"
|
||||
buildUnion a =
|
||||
"< " <> buildAlternativeTypes (Data.Map.toList a) <> " >"
|
||||
|
||||
-- | Builder corresponding to the @AlternativeTypes@ parser in "Dhall.Parser"
|
||||
buildAlternativeTypes :: Buildable a => [(Text, Expr a)] -> Builder
|
||||
buildAlternativeTypes :: Buildable a => [(Text, Expr s a)] -> Builder
|
||||
buildAlternativeTypes [] =
|
||||
""
|
||||
buildAlternativeTypes [a] =
|
||||
|
|
@ -601,11 +660,11 @@ buildAlternativeTypes (a:bs) =
|
|||
buildAlternativeType a <> " | " <> buildAlternativeTypes bs
|
||||
|
||||
-- | Builder corresponding to the @AlternativeType@ parser in "Dhall.Parser"
|
||||
buildAlternativeType :: Buildable a => (Text, Expr a) -> Builder
|
||||
buildAlternativeType :: Buildable a => (Text, Expr s a) -> Builder
|
||||
buildAlternativeType (a, b) = buildLabel a <> " : " <> buildExpr0 b
|
||||
|
||||
-- | Builder corresponding to the @UnionLit@ parser in "Dhall.Parser"
|
||||
buildUnionLit :: Buildable a => Text -> Expr a -> Map Text (Expr a) -> Builder
|
||||
buildUnionLit :: Buildable a => Text -> Expr s a -> Map Text (Expr s a) -> Builder
|
||||
buildUnionLit a b c
|
||||
| Data.Map.null c =
|
||||
"< "
|
||||
|
|
@ -623,7 +682,7 @@ buildUnionLit a b c
|
|||
<> " >"
|
||||
|
||||
-- | Generates a syntactically valid Dhall program
|
||||
instance Buildable a => Buildable (Expr a)
|
||||
instance Buildable a => Buildable (Expr s a)
|
||||
where
|
||||
build = buildExpr0
|
||||
|
||||
|
|
@ -688,7 +747,7 @@ instance Buildable a => Buildable (Expr a)
|
|||
descend into a lambda or let expression that binds a variable of the same
|
||||
name in order to avoid shifting the bound variables by mistake.
|
||||
-}
|
||||
shift :: Integer -> Var -> Expr a -> Expr a
|
||||
shift :: Integer -> Var -> Expr s a -> Expr t a
|
||||
shift _ _ (Const a) = Const a
|
||||
shift d (V x n) (Var (V x' n')) = Var (V x' n'')
|
||||
where
|
||||
|
|
@ -812,6 +871,9 @@ shift d v (Apply a b c) = Apply a' b' c'
|
|||
shift d v (Field a b) = Field a' b
|
||||
where
|
||||
a' = shift d v a
|
||||
shift d v (Note _ b) = b'
|
||||
where
|
||||
b' = shift d v b
|
||||
-- The Dhall compiler enforces that all embedded values are closed expressions
|
||||
-- and `shift` does nothing to a closed expression
|
||||
shift _ _ (Embed p) = Embed p
|
||||
|
|
@ -820,7 +882,7 @@ shift _ _ (Embed p) = Embed p
|
|||
|
||||
> subst x C B ~ B[x := C]
|
||||
-}
|
||||
subst :: Var -> Expr a -> Expr a -> Expr a
|
||||
subst :: Var -> Expr s a -> Expr t a -> Expr s a
|
||||
subst _ _ (Const a) = Const a
|
||||
subst (V x n) e (Lam y _A b) = Lam y _A' b'
|
||||
where
|
||||
|
|
@ -931,6 +993,9 @@ subst x e (Apply a b c) = Apply a' b' c'
|
|||
subst x e (Field a b) = Field a' b
|
||||
where
|
||||
a' = subst x e a
|
||||
subst x e (Note _ b) = b'
|
||||
where
|
||||
b' = subst x e b
|
||||
-- The Dhall compiler enforces that all embedded values are closed expressions
|
||||
-- and `subst` does nothing to a closed expression
|
||||
subst _ _ (Embed p) = Embed p
|
||||
|
|
@ -944,7 +1009,7 @@ subst _ _ (Embed p) = Embed p
|
|||
However, `normalize` will not fail if the expression is ill-typed and will
|
||||
leave ill-typed sub-expressions unevaluated.
|
||||
-}
|
||||
normalize :: Expr a -> Expr a
|
||||
normalize :: Expr s a -> Expr t a
|
||||
normalize e = case e of
|
||||
Const k -> Const k
|
||||
Var v -> Var v
|
||||
|
|
@ -1184,7 +1249,7 @@ normalize e = case e of
|
|||
RecordLit kvsX ->
|
||||
case y of
|
||||
RecordLit kvsY ->
|
||||
RecordLit (Data.Map.union kvsX kvsY)
|
||||
RecordLit (fmap normalize (Data.Map.union kvsX kvsY))
|
||||
_ -> Merge x' y'
|
||||
_ -> Merge x' y'
|
||||
where
|
||||
|
|
@ -1211,6 +1276,7 @@ normalize e = case e of
|
|||
Just v -> normalize v
|
||||
Nothing -> Field (RecordLit (fmap normalize kvs)) x
|
||||
r' -> Field r' x
|
||||
Note _ e' -> normalize e'
|
||||
Embed a -> Embed a
|
||||
where
|
||||
internalError :: forall b . b
|
||||
|
|
@ -1230,12 +1296,12 @@ $text
|
|||
```
|
||||
|])
|
||||
where
|
||||
-- This is to avoid a `Show` constraint on the @a@ in the type of
|
||||
-- This is to avoid a `Show` constraint on the @a@ and @s@ in the type of
|
||||
-- `normalize`. In theory, this might change a failing repro case into
|
||||
-- a successful one, but the risk of that is low enough to not warrant
|
||||
-- the `Show` constraint. I care more about proving at the type level
|
||||
-- that the @a@ parameter is never used
|
||||
e' = fmap (\_ -> ()) e
|
||||
-- that the @a@ and @s@ type parameters are never used
|
||||
e' = bimap (\_ -> ()) (\_ -> ()) e
|
||||
|
||||
text = "normalize (" <> Data.Text.pack (show e') <> ")"
|
||||
|
||||
|
|
|
|||
|
|
@ -96,6 +96,7 @@ import Filesystem as Filesystem
|
|||
import Lens.Micro (Lens')
|
||||
import Lens.Micro.Mtl (zoom)
|
||||
import Dhall.Core (Expr, Path(..))
|
||||
import Dhall.Parser (Src)
|
||||
import Dhall.TypeCheck (X(..))
|
||||
import Network.HTTP.Client (Manager)
|
||||
import Prelude hiding (FilePath)
|
||||
|
|
@ -182,7 +183,7 @@ instance Show e => Show (Imported e) where
|
|||
|
||||
data Status = Status
|
||||
{ _stack :: [Path]
|
||||
, _cache :: Map Path (Expr X)
|
||||
, _cache :: Map Path (Expr Src X)
|
||||
, _manager :: Maybe Manager
|
||||
}
|
||||
|
||||
|
|
@ -192,7 +193,7 @@ canonicalizeAll = map canonicalize . List.tails
|
|||
stack :: Lens' Status [Path]
|
||||
stack k s = fmap (\x -> s { _stack = x }) (k (_stack s))
|
||||
|
||||
cache :: Lens' Status (Map Path (Expr X))
|
||||
cache :: Lens' Status (Map Path (Expr Src X))
|
||||
cache k s = fmap (\x -> s { _cache = x }) (k (_cache s))
|
||||
|
||||
manager :: Lens' Status (Maybe Manager)
|
||||
|
|
@ -299,7 +300,7 @@ clean = strip . Filesystem.collapse
|
|||
This also returns the true final path (i.e. explicit "/@" at the end for
|
||||
directories)
|
||||
-}
|
||||
loadDynamic :: Path -> StateT Status IO (Expr Path)
|
||||
loadDynamic :: Path -> StateT Status IO (Expr Src Path)
|
||||
loadDynamic p = do
|
||||
paths <- zoom stack State.get
|
||||
|
||||
|
|
@ -357,7 +358,7 @@ loadDynamic p = do
|
|||
Right expr -> return expr
|
||||
|
||||
-- | Load a `Path` as a \"static\" expression (with all imports resolved)
|
||||
loadStatic :: Path -> StateT Status IO (Expr X)
|
||||
loadStatic :: Path -> StateT Status IO (Expr Src X)
|
||||
loadStatic path = do
|
||||
paths <- zoom stack State.get
|
||||
|
||||
|
|
@ -421,9 +422,9 @@ loadStatic path = do
|
|||
load
|
||||
:: Maybe Path
|
||||
-- ^ Starting path
|
||||
-> Expr Path
|
||||
-> Expr Src Path
|
||||
-- ^ Expression to resolve
|
||||
-> IO (Expr X)
|
||||
-> IO (Expr Src X)
|
||||
load here expr =
|
||||
State.evalStateT (fmap join (traverse loadStatic expr)) status
|
||||
where
|
||||
|
|
|
|||
|
|
@ -10,6 +10,7 @@ module Dhall.Parser (
|
|||
exprFromBytes
|
||||
|
||||
-- * Types
|
||||
, Src(..)
|
||||
, ParseError(..)
|
||||
) where
|
||||
|
||||
|
|
@ -349,6 +350,8 @@ Import
|
|||
{ URL $1 }
|
||||
|
||||
{
|
||||
data Src = Src deriving (Typeable)
|
||||
|
||||
parseError :: Token -> Alex a
|
||||
parseError token = do
|
||||
(AlexPn _ line column, _, bytes, _) <- Dhall.Lexer.alexGetInput
|
||||
|
|
@ -388,7 +391,7 @@ instance Exception ParseError
|
|||
{-| Parse an expression from a `ByteString` containing a UTF8-encoded Dhall
|
||||
program
|
||||
-}
|
||||
exprFromBytes :: ByteString -> Either ParseError (Expr Path)
|
||||
exprFromBytes :: ByteString -> Either ParseError (Expr Src Path)
|
||||
exprFromBytes bytes = case Dhall.Lexer.runAlex bytes expr of
|
||||
Left str -> Left (ParseError (Data.Text.Lazy.pack str))
|
||||
Right e -> Right e
|
||||
|
|
|
|||
|
|
@ -16,7 +16,6 @@ module Dhall.TypeCheck (
|
|||
) where
|
||||
|
||||
import Control.Exception (Exception)
|
||||
import Control.Monad.Trans.State.Strict (State)
|
||||
import Data.Foldable (forM_)
|
||||
import Data.Monoid ((<>))
|
||||
import Data.Set (Set)
|
||||
|
|
@ -38,7 +37,7 @@ import qualified Dhall.Context
|
|||
import qualified Dhall.Core
|
||||
import qualified NeatInterpolation
|
||||
|
||||
axiom :: Const -> Either TypeError Const
|
||||
axiom :: Const -> Either (TypeError s) Const
|
||||
axiom Type = return Kind
|
||||
axiom Kind = Left (TypeError Dhall.Context.empty (Const Kind) (Untyped Kind))
|
||||
|
||||
|
|
@ -59,13 +58,12 @@ match (V xL nL) (V xR nR) ((xL', xR'):xs) =
|
|||
nL' = if xL == xL' then nL - 1 else nL
|
||||
nR' = if xR == xR' then nR - 1 else nR
|
||||
|
||||
propEqual :: Expr X -> Expr X -> Bool
|
||||
propEqual :: Expr s X -> Expr t X -> Bool
|
||||
propEqual eL0 eR0 =
|
||||
State.evalState
|
||||
(go (Dhall.Core.normalize eL0) (Dhall.Core.normalize eR0))
|
||||
[]
|
||||
where
|
||||
go :: Expr X -> Expr X -> State [(Text, Text)] Bool
|
||||
go (Const Type) (Const Type) = return True
|
||||
go (Const Kind) (Const Kind) = return True
|
||||
go (Var vL) (Var vR) = do
|
||||
|
|
@ -120,7 +118,7 @@ propEqual eL0 eR0 =
|
|||
is not necessary for just type-checking. If you actually care about the
|
||||
returned type then you may want to `normalize` it afterwards.
|
||||
-}
|
||||
typeWith :: Context (Expr X) -> Expr X -> Either TypeError (Expr X)
|
||||
typeWith :: Context (Expr s X) -> Expr s X -> Either (TypeError s) (Expr s X)
|
||||
typeWith _ (Const c ) = do
|
||||
fmap Const (axiom c)
|
||||
typeWith ctx e@(Var (V x n) ) = do
|
||||
|
|
@ -477,6 +475,10 @@ typeWith ctx e@(Field r x ) = do
|
|||
Just t' -> return t'
|
||||
Nothing -> Left (TypeError ctx e (MissingField x t))
|
||||
_ -> Left (TypeError ctx e (NotARecord x r t))
|
||||
typeWith ctx (Note s e' ) = case typeWith ctx e' of
|
||||
Left (TypeError ctx' (Note _ e'') m) -> Left (TypeError ctx' (Note s e'') m)
|
||||
Left (TypeError ctx' e'' m) -> Left (TypeError ctx' (Note s e'') m)
|
||||
Right r -> Right r
|
||||
typeWith _ (Embed p ) = do
|
||||
absurd p
|
||||
|
||||
|
|
@ -484,7 +486,7 @@ typeWith _ (Embed p ) = do
|
|||
expression must be closed (i.e. no free variables), otherwise type-checking
|
||||
will fail.
|
||||
-}
|
||||
typeOf :: Expr X -> Either TypeError (Expr X)
|
||||
typeOf :: Expr s X -> Either (TypeError s) (Expr s X)
|
||||
typeOf = typeWith Dhall.Context.empty
|
||||
|
||||
-- | Like `Data.Void.Void`, except with a shorter inferred type
|
||||
|
|
@ -497,46 +499,46 @@ instance Buildable X where
|
|||
build = absurd
|
||||
|
||||
-- | The specific type error
|
||||
data TypeMessage
|
||||
data TypeMessage s
|
||||
= UnboundVariable
|
||||
| InvalidInputType (Expr X)
|
||||
| InvalidOutputType (Expr X)
|
||||
| NotAFunction (Expr X)
|
||||
| TypeMismatch (Expr X) (Expr X)
|
||||
| AnnotMismatch (Expr X) (Expr X) (Expr X)
|
||||
| InvalidInputType (Expr s X)
|
||||
| InvalidOutputType (Expr s X)
|
||||
| NotAFunction (Expr s X)
|
||||
| TypeMismatch (Expr s X) (Expr s X)
|
||||
| AnnotMismatch (Expr s X) (Expr s X) (Expr s X)
|
||||
| Untyped Const
|
||||
| InvalidListElement Int Int (Expr X) (Expr X) (Expr X)
|
||||
| InvalidListType Bool (Expr X)
|
||||
| InvalidMaybeElement (Expr X) (Expr X) (Expr X)
|
||||
| InvalidListElement Int Int (Expr s X) (Expr s X) (Expr s X)
|
||||
| InvalidListType Bool (Expr s X)
|
||||
| InvalidMaybeElement (Expr s X) (Expr s X) (Expr s X)
|
||||
| InvalidMaybeLiteral Int
|
||||
| InvalidMaybeType (Expr X)
|
||||
| InvalidPredicate (Expr X) (Expr X)
|
||||
| IfBranchMismatch (Expr X) (Expr X) (Expr X) (Expr X)
|
||||
| InvalidFieldType Text (Expr X)
|
||||
| InvalidAlternativeType Text (Expr X)
|
||||
| InvalidMaybeType (Expr s X)
|
||||
| InvalidPredicate (Expr s X) (Expr s X)
|
||||
| IfBranchMismatch (Expr s X) (Expr s X) (Expr s X) (Expr s X)
|
||||
| InvalidFieldType Text (Expr s X)
|
||||
| InvalidAlternativeType Text (Expr s X)
|
||||
| DuplicateField Text
|
||||
| MustMergeARecord (Expr X) (Expr X)
|
||||
| MustMergeARecord (Expr s X) (Expr s X)
|
||||
| FieldCollision (Set Text)
|
||||
| MustApplyARecord (Expr X) (Expr X)
|
||||
| MustApplyToUnion (Expr X)
|
||||
| MustApplyARecord (Expr s X) (Expr s X)
|
||||
| MustApplyToUnion (Expr s X)
|
||||
| UnusedHandler (Set Text)
|
||||
| MissingHandler (Set Text)
|
||||
| HandlerInputTypeMismatch Text (Expr X) (Expr X)
|
||||
| HandlerOutputTypeMismatch Text (Expr X) (Expr X)
|
||||
| HandlerNotAFunction Text (Expr X)
|
||||
| NotARecord Text (Expr X) (Expr X)
|
||||
| MissingField Text (Expr X)
|
||||
| CantAnd Bool (Expr X) (Expr X)
|
||||
| CantOr Bool (Expr X) (Expr X)
|
||||
| CantEQ Bool (Expr X) (Expr X)
|
||||
| CantNE Bool (Expr X) (Expr X)
|
||||
| CantTextAppend Bool (Expr X) (Expr X)
|
||||
| CantAdd Bool (Expr X) (Expr X)
|
||||
| CantMultiply Bool (Expr X) (Expr X)
|
||||
| NoDependentTypes (Expr X) (Expr X)
|
||||
| HandlerInputTypeMismatch Text (Expr s X) (Expr s X)
|
||||
| HandlerOutputTypeMismatch Text (Expr s X) (Expr s X)
|
||||
| HandlerNotAFunction Text (Expr s X)
|
||||
| NotARecord Text (Expr s X) (Expr s X)
|
||||
| MissingField Text (Expr s X)
|
||||
| CantAnd Bool (Expr s X) (Expr s X)
|
||||
| CantOr Bool (Expr s X) (Expr s X)
|
||||
| CantEQ Bool (Expr s X) (Expr s X)
|
||||
| CantNE Bool (Expr s X) (Expr s X)
|
||||
| CantTextAppend Bool (Expr s X) (Expr s X)
|
||||
| CantAdd Bool (Expr s X) (Expr s X)
|
||||
| CantMultiply Bool (Expr s X) (Expr s X)
|
||||
| NoDependentTypes (Expr s X) (Expr s X)
|
||||
deriving (Show)
|
||||
|
||||
instance Buildable TypeMessage where
|
||||
instance Buildable (TypeMessage s) where
|
||||
build UnboundVariable =
|
||||
Builder.fromText [NeatInterpolation.text|
|
||||
Error: Unbound variable
|
||||
|
|
@ -1335,7 +1337,7 @@ Your function type is invalid because the input is a term of type:
|
|||
indent :: Data.Text.Text -> Data.Text.Text
|
||||
indent = Data.Text.unlines . fmap (" " <>) . Data.Text.lines
|
||||
|
||||
buildBooleanOperator :: Text -> Bool -> Expr X -> Expr X -> Builder
|
||||
buildBooleanOperator :: Text -> Bool -> Expr s X -> Expr s X -> Builder
|
||||
buildBooleanOperator operator b expr0 expr1 =
|
||||
Builder.fromText [NeatInterpolation.text|
|
||||
Error: Cannot use `($txt2)` on a value that's not a `Bool`
|
||||
|
|
@ -1358,7 +1360,7 @@ You provided this argument:
|
|||
then [NeatInterpolation.text|$txt0 $txt2 ...|]
|
||||
else [NeatInterpolation.text|... $txt2 $txt0|]
|
||||
|
||||
buildNaturalOperator :: Text -> Bool -> Expr X -> Expr X -> Builder
|
||||
buildNaturalOperator :: Text -> Bool -> Expr s X -> Expr s X -> Builder
|
||||
buildNaturalOperator operator b expr0 expr1 =
|
||||
Builder.fromText [NeatInterpolation.text|
|
||||
Error: Cannot use `($txt2)` on a value that's not a `Natural`
|
||||
|
|
@ -1402,18 +1404,18 @@ Example:
|
|||
_ -> mempty
|
||||
|
||||
-- | A structured type error that includes context
|
||||
data TypeError = TypeError
|
||||
{ context :: Context (Expr X)
|
||||
, current :: Expr X
|
||||
, typeMessage :: TypeMessage
|
||||
data TypeError s = TypeError
|
||||
{ context :: Context (Expr s X)
|
||||
, current :: Expr s X
|
||||
, typeMessage :: TypeMessage s
|
||||
} deriving (Typeable)
|
||||
|
||||
instance Show TypeError where
|
||||
instance Show (TypeError s) where
|
||||
show = Text.unpack . Dhall.Core.pretty
|
||||
|
||||
instance Exception TypeError
|
||||
instance Typeable s => Exception (TypeError s)
|
||||
|
||||
instance Buildable TypeError where
|
||||
instance Buildable (TypeError s) where
|
||||
build (TypeError ctx expr msg)
|
||||
= "\n"
|
||||
<> ( if Text.null (Builder.toLazyText (buildContext ctx))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user