Skip to content

Commit

Permalink
Add VarName as parameter to Constrained typ constructor
Browse files Browse the repository at this point in the history
  • Loading branch information
paolino committed Sep 22, 2023
1 parent d88001f commit 6acd4eb
Show file tree
Hide file tree
Showing 6 changed files with 27 additions and 21 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -201,7 +201,7 @@ typeFromTyp = go
error "Nested Product is not supported by Haskell"
go (SumN _) =
error "Nested Sum is not supported by Haskell"
go (Constrained typ _) =
go (Constrained _ typ _) =
-- FIXME: Emit a warning.
-- TODO: Add Liquid Haskell support for top-level definitions? 😲
-- Currently no good representation for comments / Liquid Haskell
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ supportsJSON =
isSupportedTyp = everything (&&) isSupported
isSupported (Two fun _ _) =
fun `notElem` [PartialFunction, FiniteSupport]
isSupported (Constrained _ _) =
isSupported Constrained{} =
False
isSupported _ = True

Expand Down Expand Up @@ -203,7 +203,7 @@ schemaFromTyp = go
schemaFromProductN fields
go (SumN constructors) =
schemaFromSumN constructors
go (Constrained _ _) =
go Constrained{} =
error "ConstrainedTyp is not supported by JSON schema"

-- | Map a record type to a JSON schema.
Expand Down
7 changes: 3 additions & 4 deletions lib/fine-types/src/Language/FineTypes/Parser.hs
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ import Language.FineTypes.Typ
, Typ (..)
, TypConst (..)
, TypName
, VarName
)
import Text.Megaparsec
( ParseErrorBundle
Expand Down Expand Up @@ -169,11 +170,11 @@ mkDocumentedDeclaration doc1 name (DocumentedTyp typ fs cs) doc2 =

constrained :: Parser Typ
constrained = braces $ do
_ <- varName
v <- varName
_ <- symbol ":"
typ <- zeroVar
_ <- symbol "|"
Constrained typ <$> constraint
Constrained v typ <$> constraint

abstract :: Parser Typ
abstract = Abstract <$ symbol "_"
Expand Down Expand Up @@ -379,8 +380,6 @@ fieldName =
L.lexeme space
$ many (C.alphaNumChar <|> satisfy (`elem` "_^-"))

type VarName = String

varName :: Parser VarName
varName =
L.lexeme space
Expand Down
12 changes: 7 additions & 5 deletions lib/fine-types/src/Language/FineTypes/Typ.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ module Language.FineTypes.Typ
TypName
, ConstructorName
, FieldName
, VarName
, Typ (..)
, TypConst (..)
, OpOne (..)
Expand All @@ -33,6 +34,7 @@ import qualified Data.List as L
type TypName = String
type ConstructorName = String
type FieldName = String
type VarName = String

-- | A 'Typ' describes a set of values.
--
Expand All @@ -56,7 +58,7 @@ data Typ
| -- | Disjoint union with constructor names.
SumN [(ConstructorName, Typ)]
| -- | A type with a value constraint
Constrained Typ Constraint
Constrained VarName Typ Constraint
deriving (Eq, Ord, Show, Generic)

instance ToExpr Typ
Expand Down Expand Up @@ -138,8 +140,8 @@ everywhere f = every
ProductN [(n, every a) | (n, a) <- nas]
recurse (SumN nas) =
SumN [(n, every a) | (n, a) <- nas]
recurse (Constrained typ c) =
Constrained (every typ) c
recurse (Constrained v typ c) =
Constrained v (every typ) c

-- | Summarise all nodes; top-down, left-to-right.
everything :: (r -> r -> r) -> (Typ -> r) -> (Typ -> r)
Expand All @@ -159,7 +161,7 @@ everything combine f = recurse
L.foldl' combine (f x) [recurse a | (_, a) <- nas]
recurse x@(SumN nas) =
L.foldl' combine (f x) [recurse a | (_, a) <- nas]
recurse x@(Constrained typ _) =
recurse x@(Constrained _ typ _) =
f x `combine` recurse typ

depth :: Typ -> Int
Expand All @@ -169,7 +171,7 @@ depth = \case
Two _ a b -> 1 + max (depth a) (depth b)
ProductN fields -> 1 + maximum (fmap (depth . snd) fields)
SumN constructors -> 1 + maximum (fmap (depth . snd) constructors)
Constrained a _ -> depth a
Constrained _ a _ -> depth a
Abstract -> 0
Var _ -> 0

Expand Down
9 changes: 5 additions & 4 deletions lib/fine-types/src/Language/FineTypes/Typ/Gen.hs
Original file line number Diff line number Diff line change
Expand Up @@ -143,7 +143,8 @@ genConstrainedTyp mode = do
constraintDepth <- choose (1, 2)
c <- genConstraint constraintDepth
typ <- genTyp'
pure $ Constrained typ c
v <- genName
pure $ Constrained v typ c
where
complete = onComplete mode
always = id
Expand Down Expand Up @@ -225,10 +226,10 @@ shrinkTyp = \case
<> (SumN <$> shrinkList shrinkNamed constructors)
Var _ -> []
Abstract -> []
Constrained typ c ->
Constrained v typ c ->
[typ]
<> [Constrained typ' c | typ' <- shrinkTyp typ]
<> [Constrained typ c' | c' <- shrinkConstraint c]
<> [Constrained v typ' c | typ' <- shrinkTyp typ]
<> [Constrained v typ c' | c' <- shrinkConstraint c]

shrinkNamed :: (t, Typ) -> [(t, Typ)]
shrinkNamed (f, t) = (f,) <$> shrinkTyp t
Expand Down
14 changes: 9 additions & 5 deletions lib/fine-types/src/Language/FineTypes/Typ/PrettyPrinter.hs
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ import Language.FineTypes.Typ
, Typ (..)
, TypConst (..)
, TypName
, VarName
)
import Prettyprinter
( Doc
Expand Down Expand Up @@ -58,7 +59,7 @@ requireParens = \case
SumN _ -> False
Var _ -> False
Abstract -> False
Constrained _ _ -> False
Constrained{} -> False

parens :: Doc ann -> Doc ann
parens doc = encloseSep "(" ")" " " [doc]
Expand All @@ -69,12 +70,15 @@ withParens f x = if requireParens x then parens (f x) else f x
prettyConstrainedTyp
:: QueryDocumentation
-> TypName
-> VarName
-> Typ
-> Constraint
-> Doc ann
prettyConstrainedTyp docs typname typ [] = prettyTyp docs typname typ
prettyConstrainedTyp docs typname typ constraint =
"{ x :"
prettyConstrainedTyp docs typname _v typ [] = prettyTyp docs typname typ
prettyConstrainedTyp docs typname v typ constraint =
"{"
<+> pretty v
<+> ":"
<+> prettyTyp docs typname typ
<+> prettyText "|"
<+> prettyConstraint constraint
Expand Down Expand Up @@ -154,7 +158,7 @@ prettyTyp docs typname = \case
SumN constructors -> prettySumN docs typname constructors
Var name -> pretty name
Abstract -> prettyText "_"
Constrained typ c -> prettyConstrainedTyp docs typname typ c
Constrained v typ c -> prettyConstrainedTyp docs typname v typ c
where
prettyTyp' = prettyTyp docs typname

Expand Down

0 comments on commit 6acd4eb

Please sign in to comment.