From 6580a4cbf1d51cb2dab03503d8e68c102b7dcb22 Mon Sep 17 00:00:00 2001 From: Gabriel Gonzalez Date: Thu, 15 Sep 2016 09:03:12 -0700 Subject: [PATCH] Change `[ a ]` to `List a` --- src/Dhall.hs | 80 ++++++---------------------------------------- src/Dhall/Core.hs | 66 +++++++++++--------------------------- src/Dhall/Lexer.x | 2 ++ src/Dhall/Parser.y | 5 +-- 4 files changed, 32 insertions(+), 121 deletions(-) diff --git a/src/Dhall.hs b/src/Dhall.hs index 6c55426..873a2b7 100644 --- a/src/Dhall.hs +++ b/src/Dhall.hs @@ -52,7 +52,7 @@ -- -- > $ ./example -- > example: --- > Expression: 1 : {{ bar : [ Double ], foo : Integer }} +-- > Expression: 1 : {{ bar : List Double, foo : Integer }} -- > -- > Error: Expression's inferred type does not match annotated type -- > @@ -72,7 +72,7 @@ -- > You or the interpreter annotated this expression: -- > ↳ 1 -- > ... with this type or kind: --- > ↳ {{ bar : [ Double ], foo : Integer }} +-- > ↳ {{ bar : List Double, foo : Integer }} -- > ... but the inferred type of the expression is actually this type or kind: -- > ↳ Integer -- @@ -105,7 +105,7 @@ -- is: -- -- > $ dhall typecheck < makeBools --- > forall (n : Bool) → [ Bool ] +-- > forall (n : Bool) → List Bool -- -- This says that @makeBools@ is a function of one argument named @n@ of type -- `Bool` that returns a `Vector` of `Bool`s. @@ -138,7 +138,7 @@ -- > $ dhall -- > ./makeBools False -- > --- > [ Bool ] +-- > List Bool -- > -- > [ False, False, True, False : Bool ] -- @@ -250,7 +250,7 @@ -- > $ dhall -- > [ ./bool1 , ./bool2 , ./both : Bool ] -- > --- > [ Bool ] +-- > List Bool -- > -- > [ True, False, False : Bool ] -- @@ -305,8 +305,6 @@ module Dhall , double , text , vector - , pair2 - , pair3 -- * Re-exports , Vector @@ -369,12 +367,12 @@ input (Type {..}) bytes = do You can produce `Type`s either explicitly: -> example :: Type (Double, Text) -> example = pair2 double text +> example :: Type (Vector Text) +> example = vector text ... or implicitly using `auto`: -> example :: Type (Double, Text) +> example :: Type (Vector Text) > example = auto You can consume `Type`s using the `input` function: @@ -462,61 +460,7 @@ vector (Type extractIn expectedIn) = Type extractOut expectedOut where extractOut (ListLit _ es) = traverse extractIn es - expectedOut = List expectedIn - -{-| Decode a 2-tuple - ->>> input (pair2 integer integer) "{ _1 = 1, _2 = 2 }" -(1,2) --} -pair2 :: Type a -> Type b -> Type (a, b) -pair2 - (Type extractA expectedA) - (Type extractB expectedB) = Type {..} - where - extract (RecordLit m) = do - eA <- Data.Map.lookup "_1" m - vA <- extractA eA - eB <- Data.Map.lookup "_2" m - vB <- extractB eB - return (vA, vB) - extract _ = empty - - expected = Record (Data.Map.fromList kts) - where - kts = - [ ("_1", expectedA) - , ("_2", expectedB) - ] - -{-| Decode a 3-tuple - ->>> input (pair3 integer integer integer) "{ _1 = 1, _2 = 2, _3 = 3 }" -(1,2,3) --} -pair3 :: Type a -> Type b -> Type c -> Type (a, b, c) -pair3 - (Type extractA expectedA) - (Type extractB expectedB) - (Type extractC expectedC) = Type {..} - where - extract (RecordLit m) = do - eA <- Data.Map.lookup "_1" m - vA <- extractA eA - eB <- Data.Map.lookup "_2" m - vB <- extractB eB - eC <- Data.Map.lookup "_3" m - vC <- extractC eC - return (vA, vB, vC) - extract _ = empty - - expected = Record (Data.Map.fromList kts) - where - kts = - [ ("_1", expectedA) - , ("_2", expectedB) - , ("_3", expectedC) - ] + expectedOut = App List expectedIn {-| Any value that implements `Interpret` can be automatically decoded based on the inferred return type of `input` @@ -551,12 +495,6 @@ instance Interpret Text where instance Interpret a => Interpret (Vector a) where auto = vector auto -instance (Interpret a, Interpret b) => Interpret (a, b) where - auto = pair2 auto auto - -instance (Interpret a, Interpret b, Interpret c) => Interpret (a, b, c) where - auto = pair3 auto auto auto - class GenericInterpret f where genericAuto :: Type (f a) diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs index b6e1fd7..77ee384 100644 --- a/src/Dhall/Core.hs +++ b/src/Dhall/Core.hs @@ -192,8 +192,8 @@ data Expr a | TextLit Text -- | > TextAppend x y ~ x <> y | TextAppend (Expr a) (Expr a) - -- | > List t ~ [ t ] - | List (Expr a) + -- | > List ~ List + | List -- | > ListLit t [x, y, z] ~ [ x, y, z : t ] | ListLit (Expr a) (Vector (Expr a)) -- | > ListBuild ~ List/build @@ -251,7 +251,7 @@ instance Monad Expr where Text >>= _ = Text TextLit t >>= _ = TextLit t TextAppend l r >>= k = TextAppend (l >>= k) (r >>= k) - List t >>= k = List (t >>= k) + List >>= _ = List ListLit t es >>= k = ListLit (t >>= k) es' where es' = do @@ -304,7 +304,7 @@ propEqual eL0 eR0 = State.evalState (go (normalize eL0) (normalize eR0)) [] go Integer Integer = return True go Double Double = return True go Text Text = return True - go (List tL) (List tR) = go tL tR + go List List = return True go (Record ktsL0) (Record ktsR0) = do let loop ((kL, tL):ktsL) ((kR, tR):ktsR) | kL == kR = do @@ -397,8 +397,8 @@ buildExpr5 ListBuild = "List/build" buildExpr5 ListFold = "List/fold" -buildExpr5 (List a) = - "[ " <> buildExpr1 a <> " ]" +buildExpr5 List = + "List" buildExpr5 (BoolLit True) = "True" buildExpr5 (BoolLit False) = @@ -487,7 +487,6 @@ data TypeMessage | AnnotMismatch (Expr X) (Expr X) (Expr X) | Untyped Const | InvalidElement Int Int (Expr X) (Expr X) (Expr X) - | InvalidListTypeParam (Expr X) | InvalidListType Bool (Expr X) | InvalidPredicate (Expr X) (Expr X) | IfBranchMismatch (Expr X) (Expr X) (Expr X) (Expr X) @@ -683,30 +682,6 @@ the compiler cannot infer what `Kind` belongs to where txt = Text.toStrict (pretty c) - build (InvalidListTypeParam expr) = - Builder.fromText [NeatInterpolation.text| -Error: Invalid type of list - -Explanation: You can wrap any type `a` in brackets to generate the type of a -list of `a`s: `[ a ]`. For example, `[ Bool ]` denotes a list of `Bool`s. - -Only types can be wrapped in brackets to generated an optional type. You -*cannot* wrap terms or kinds in brackets: - - [ True ] -- This is not a valid type of list because `True` is not a type - [ Type ] -- This is not a valid type of list because `Type` is not a type - -If you meant to create a 1-element list, then include the element type at the -end of the list to indicate that you meant a list term and not a list type: - - [ True : Bool ] -- This is a valid 1-element list term - -The following expression you provided is not a valid element type for a list: -↳ $txt -|] - where - txt = Text.toStrict (pretty expr) - build (InvalidPredicate expr0 expr1) = Builder.fromText [NeatInterpolation.text| Error: Invalid predicate for `if` @@ -1131,7 +1106,6 @@ subst x e (BoolIf x' y z ) = BoolIf (subst x e x') (subst x e y) (subst x e z) 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 (List t ) = List (subst x e t) subst x e (ListLit t es ) = ListLit (subst x e t) es' where es' = do @@ -1306,12 +1280,8 @@ typeWith ctx e@(TextAppend l r ) = do Text -> return () _ -> Left (TypeError ctx e (CantAppend False r tr)) return Text -typeWith ctx e@(List t ) = do - s <- fmap normalize (typeWith ctx t) - case s of - Const Type -> return () - _ -> Left (TypeError ctx e (InvalidListTypeParam t)) - return (Const Type) +typeWith _ List = do + return (Pi "_" (Const Type) (Const Type)) typeWith ctx e@(ListLit t xs ) = do s <- fmap normalize (typeWith ctx t) case s of @@ -1326,7 +1296,7 @@ typeWith ctx e@(ListLit t xs ) = do let nf_t = normalize t let nf_t' = normalize t' Left (TypeError ctx e (InvalidElement i n x nf_t nf_t')) ) - return (List t) + return (App List t) typeWith _ ListBuild = do return (Pi "a" (Const Type) @@ -1334,28 +1304,28 @@ typeWith _ ListBuild = do (Pi "list" (Const Type) (Pi "cons" (Pi "head" "a" (Pi "tail" "list" "list")) (Pi "nil" "list" "list") ) ) - (List "a") ) ) + (App List "a") ) ) typeWith _ ListFold = do return (Pi "a" (Const Type) - (Pi "_" (List "a") + (Pi "_" (App List "a") (Pi "list" (Const Type) (Pi "cons" (Pi "head" "a" (Pi "tail" "list" "list")) (Pi "nil" "list" "list")) ) ) ) typeWith ctx e@(ListConcat l r ) = do tl <- fmap normalize (typeWith ctx l) el <- case tl of - List el -> return el - _ -> Left (TypeError ctx e (CantConcat True l tl)) + App List el -> return el + _ -> Left (TypeError ctx e (CantConcat True l tl)) tr <- fmap normalize (typeWith ctx r) er <- case tr of - List er -> return er - _ -> Left (TypeError ctx e (CantConcat False r tr)) + App List er -> return er + _ -> Left (TypeError ctx e (CantConcat False r tr)) if propEqual el er then return () else Left (TypeError ctx e (ElementMismatch el er)) - return (List el) + return (App List el) typeWith ctx e@(Record kts ) = do let process (k, t) = do s <- fmap normalize (typeWith ctx t) @@ -1411,7 +1381,8 @@ normalize e = case e of | check -> ListLit t (buildVector k') | otherwise -> App f' a' where - labeled = normalize (App (App (App k (List t)) "Cons") "Nil") + labeled = + normalize (App (App (App k (App List t)) "Cons") "Nil") k' cons nil = go labeled where @@ -1495,7 +1466,6 @@ normalize e = case e of where x' = normalize x y' = normalize y - List t -> List (normalize t) ListLit t es -> ListLit (normalize t) (fmap normalize es) ListConcat x y -> case x' of diff --git a/src/Dhall/Lexer.x b/src/Dhall/Lexer.x index d490a55..e1b9394 100644 --- a/src/Dhall/Lexer.x +++ b/src/Dhall/Lexer.x @@ -86,6 +86,7 @@ tokens :- "Integer" { emit Integer } "Double" { emit Double } "Text" { emit Text } + "List" { emit List } "List/build" { emit ListBuild } "List/fold" { emit ListFold } \" ([^\"] | \\.)* \" { capture (TextLit . str) } @@ -191,6 +192,7 @@ data Token | Text | Double | DoubleLit Double + | List | ListBuild | ListFold | TextLit Text diff --git a/src/Dhall/Parser.y b/src/Dhall/Parser.y index e803932..01e7176 100644 --- a/src/Dhall/Parser.y +++ b/src/Dhall/Parser.y @@ -75,6 +75,7 @@ import qualified NeatInterpolation 'Integer' { Dhall.Lexer.Integer } 'Double' { Dhall.Lexer.Double } 'Text' { Dhall.Lexer.Text } + 'List' { Dhall.Lexer.List } 'List/build' { Dhall.Lexer.ListBuild } 'List/fold' { Dhall.Lexer.ListFold } text { Dhall.Lexer.TextLit $$ } @@ -159,12 +160,12 @@ Expr5 { Double } | 'Text' { Text } + | 'List' + { List } | 'List/build' { ListBuild } | 'List/fold' { ListFold } - | '[' Expr1 ']' - { List $2 } | 'True' { BoolLit True } | 'False'