some more docs

Author: MaximilianAlgehed

docs/constrained-generators/DesignPrinciples.md

@@ -250,7 +250,7 @@ data PredD deps where
     TermD deps Bool ->
     PredD deps ->
     PredD deps
-  GenHint ::
+  GenHintD ::
     ( HasGenHintD deps a
     , Show a
     , Show (HintD deps a)
@@ -321,7 +321,7 @@ instance Pretty (PredD deps) where
     Case t bs -> "case" <+> pretty t <+> "of" /> vsep' (ppList pretty bs)
     When b p -> "whenTrue" <+> pretty (WithPrec 11 b) <+> "$" /> pretty p
     Subst x t p -> "[" <> pretty t <> "/" <> viaShow x <> "]" <> pretty p
-    GenHint h t -> "genHint" <+> fromString (showsPrec 11 h "") <+> "$" <+> pretty t
+    GenHintD h t -> "genHint" <+> fromString (showsPrec 11 h "") <+> "$" <+> pretty t
     TruePred -> "True"
     FalsePred {} -> "False"
     Monitor {} -> "monitor"

libs/constrained-generators/src/Constrained/AbstractSyntax.hs

@@ -33,53 +33,62 @@ module Constrained.Base (
   pattern (:>:),
   pattern Unary,
 
-  -- * Useful function symbols
+  toCtx,
+  flipCtx,
+  fromListCtx,
+
+  -- * Useful function symbols and patterns for building custom rewrite rules
   fromGeneric_,
   toGeneric_,
 
-  -- * TODO: documentme
-  HasSpec (..),
-  propagateSpec,
   pattern ToGeneric,
   pattern FromGeneric,
+
+  -- * Syntax for building specifications
   constrained,
-  appFun,
-  errorLikeMessage,
-  isErrorLike,
   notMemberSpec,
   notEqualSpec,
+  typeSpec,
   addToErrorSpec,
-  memberSpecList,
-  toCtx,
-  flipCtx,
-  BinaryShow (..),
-  name,
+  memberSpec,
   fromSimpleRepSpec,
   toSimpleRepSpec,
-  toPred,
-  forAllToList,
   explainSpec,
-  bind,
+
+  -- * Instantiated types and helper patterns
   Term,
   Specification,
   Pred,
-  IsPred,
-  HintF (..),
   Binder,
+
+  pattern TypeSpec,
+  pattern GenHint,
+
+  -- * Constraints and classes
+  HasSpec (..),
   HasGenHint (..),
   Forallable,
-  pattern TypeSpec,
-  typeSpec,
+  AppRequires,
+  GenericallyInstantiated,
+  GenericRequires,
+
+  -- * TODO: documentme
+  propagateSpec,
+  appFun,
+  errorLikeMessage,
+  isErrorLike,
+  BinaryShow (..),
+  name,
+  toPred,
+  forAllToList,
+  bind,
+  IsPred,
   equalSpec,
   appTerm,
-  GenericRequires,
   HOLE (..),
-  AppRequires,
   fromForAllSpec,
   Fun (..),
-  GenericallyInstantiated,
   BaseW (..),
-  fromListCtx,
 ) where
 
 import Constrained.AbstractSyntax
@@ -129,22 +138,38 @@ instance Dependencies Deps where
 
 type Binder = BinderD Deps
 
+-- | All the constraints needed for application in the first order term languge
 type AppRequires t as b = AppRequiresD Deps t as b
 
+-- | Predicates over `Term`s
 type Pred = PredD Deps
 
+-- | First-order language of variables, literals, and application
 type Term = TermD Deps
 
+-- | Specifications for generators instantiated with the `HasSpec` et al actual
+-- classes
 type Specification = SpecificationD Deps
 
+-- | Pattern match out a `TypeSpec` and the can't-"set" - avoids some tedious
+-- pitfalls related to the `Deps` and `Dependencies` trick
 pattern TypeSpec :: () => HasSpec a => TypeSpec a -> [a] -> Specification a
 pattern TypeSpec ts cant = TypeSpecD (TypeSpecF ts) cant
 
 {-# COMPLETE ExplainSpec, MemberSpec, ErrorSpec, SuspendedSpec, TypeSpec, TrueSpec #-}
 
+-- | Build a specifiation from just a `TypeSpec`, useful internal function when
+-- writing `Logic` instances
 typeSpec :: HasSpec a => TypeSpec a -> Specification a
 typeSpec ts = TypeSpec ts mempty
 
+-- | Pattern match out a `Hint` and the `Term` it applies to - avoids some
+-- tedious pitfalls related to the `Deps` and `Dependencies` trick
+pattern GenHint :: () => HasGenHint a => Hint a -> Term a -> Pred
+pattern GenHint h t = GenHintD (HintF h) t
+
+{-# COMPLETE ElemPred, Monitor, And, Exists, Subst, Let, Assert, Reifies, DependsOn, ForAll, Case, When, GenHint, TruePred, FalsePred, Explain #-}
+
 -- ====================================================================
 
 -- | A First-order typed logic has 4 components
@@ -735,7 +760,7 @@ bind bodyf = newv :-> bodyPred
     bound (Case _ cs) = getMax $ foldMapList (Max . boundBinder . thing) cs
     bound (When _ p) = bound p
     bound Reifies {} = -1
-    bound GenHint {} = -1
+    bound GenHintD {} = -1
     bound Assert {} = -1
     bound DependsOn {} = -1
     bound TruePred = -1
@@ -793,27 +818,33 @@ instance IsPred (Term Bool) where
 -- ============================================================
 -- Simple Widely used operations on Specification
 
--- | return a MemberSpec or ans ErrorSpec depending on if 'xs' the null list or not
-memberSpecList :: [a] -> NE.NonEmpty String -> Specification a
-memberSpecList xs messages =
+-- | return a MemberSpec or ans ErrorSpec depending on if 'xs' is null or not
+memberSpec :: Foldable f => f a -> NE.NonEmpty String -> Specification a
+memberSpec (toList -> xs) messages =
   case NE.nonEmpty xs of
     Nothing -> ErrorSpec messages
     Just ys -> MemberSpec ys
 
+-- | Attach an explanation to a specification in order to track issues with satisfiability
 explainSpec :: [String] -> Specification a -> Specification a
 explainSpec [] x = x
 explainSpec es (ExplainSpec es' spec) = ExplainSpec (es ++ es') spec
 explainSpec es spec = ExplainSpec es spec
 
+-- | A "discrete" specification satisfied by exactly one element
 equalSpec :: a -> Specification a
 equalSpec = MemberSpec . pure
 
+-- | Anything but this
 notEqualSpec :: forall a. HasSpec a => a -> Specification a
 notEqualSpec = TypeSpec (emptySpec @a) . pure
 
+-- | Anything but these
 notMemberSpec :: forall a f. (HasSpec a, Foldable f) => f a -> Specification a
 notMemberSpec = typeSpecOpt (emptySpec @a) . toList
 
+-- | Build a `Specification` using predicates, e.g.
+-- > constrained $ \ x -> assert $ x `elem_` lit [1..10 :: Int]
 constrained ::
   forall a p.
   (IsPred p, HasSpec a) =>
@@ -823,6 +854,7 @@ constrained body =
   let x :-> p = bind body
    in SuspendedSpec x p
 
+-- | Sound but not complete check for empty `Specification`s
 isErrorLike :: forall a. Specification a -> Bool
 isErrorLike (ExplainSpec _ s) = isErrorLike s
 isErrorLike ErrorSpec {} = True
@@ -832,6 +864,7 @@ isErrorLike (TypeSpec x _) =
     Just _ -> True
 isErrorLike _ = False
 
+-- | Get the error message of an `isErrorLike` `Specification`
 errorLikeMessage :: forall a. Specification a -> NE.NonEmpty String
 errorLikeMessage (ErrorSpec es) = es
 errorLikeMessage (TypeSpec x _) =

libs/constrained-generators/src/Constrained/Base.hs

@@ -252,12 +252,12 @@ instance HasSpec a => Semigroup (Specification a) where
       ( NE.fromList
           ["Intersecting: ", "  MemberSpec " ++ show (NE.toList as), "  MemberSpec " ++ show (NE.toList as')]
       )
-      ( memberSpecList
+      ( memberSpec
           (nub $ intersect (NE.toList as) (NE.toList as'))
           (pure "Empty intersection")
       )
   ms@(MemberSpec as) <> ts@TypeSpec {} =
-    memberSpecList
+    memberSpec
       (nub $ NE.filter (`conformsToSpec` ts) as)
       ( NE.fromList
           [ "The two " ++ showType @a ++ " Specifications are inconsistent."

libs/constrained-generators/src/Constrained/Conformance.hs

@@ -336,7 +336,7 @@ computeSpecSimplified x pred3 = localGESpec $ case simplifyPred pred3 of
   ElemPred True t xs -> propagateSpec (MemberSpec xs) <$> toCtx x t
   ElemPred False (t :: Term b) xs -> propagateSpec (TypeSpec @b (emptySpec @b) (NE.toList xs)) <$> toCtx x t
   Monitor {} -> pure mempty
-  GenHint (HintF h) t -> propagateSpec (giveHint h) <$> toCtx x t
+  GenHint h t -> propagateSpec (giveHint h) <$> toCtx x t
   Subst x' t p' -> computeSpec x (substitutePred x' t p') -- NOTE: this is impossible as it should have gone away already
   TruePred -> pure mempty
   FalsePred es -> genErrorNE es

libs/constrained-generators/src/Constrained/Generation.hs

@@ -36,7 +36,7 @@ import Constrained.Base (
   explainSpec,
   flipCtx,
   fromSimpleRepSpec,
-  memberSpecList,
+  memberSpec,
   notMemberSpec,
   typeSpec,
   pattern TypeSpec,
@@ -359,7 +359,7 @@ nubOrd =
 -- | Builds a MemberSpec, but returns an Error spec if the list is empty
 nubOrdMemberSpec :: Ord a => String -> [a] -> Specification a
 nubOrdMemberSpec message xs =
-  memberSpecList
+  memberSpec
     (nubOrd xs)
     ( NE.fromList
         [ "In call to nubOrdMemberSpec"
@@ -751,7 +751,7 @@ instance Logic IntW where
   propagateTypeSpec NegateW (Unary HOLE) ts cant = negateSpec ts <> notMemberSpec (map negate cant)
 
   propagateMemberSpec AddW (HOLE :<: i) es =
-    memberSpecList
+    memberSpec
       (nub $ mapMaybe (safeSubtract i) (NE.toList es))
       ( NE.fromList
           [ "propagateSpecFn on (" ++ show i ++ " +. HOLE)"

libs/constrained-generators/src/Constrained/NumOrd.hs

@@ -163,7 +163,7 @@ instance Logic ElemW where
     constrained $ \v' -> Let (App ElemW (Lit x :> v' :> Nil)) (v :-> ps)
   propagate ElemW (HOLE :<: es) spec =
     caseBoolSpec spec $ \case
-      True -> memberSpecList (nub es) (pure "propagate on (elem_ x []), The empty list, [], has no solution")
+      True -> memberSpec (nub es) (pure "propagate on (elem_ x []), The empty list, [], has no solution")
       False -> notMemberSpec es
   propagate ElemW (e :>: HOLE) spec =
     caseBoolSpec spec $ \case

libs/constrained-generators/src/Constrained/Spec/List.hs

@@ -364,7 +364,7 @@ instance Logic MapW where
     if Nothing `conformsToSpec` spec
       then notMemberSpec [k | (k, v) <- Map.toList m, not $ Just v `conformsToSpec` spec]
       else
-        memberSpecList
+        memberSpec
           (Map.keys $ Map.filter ((`conformsToSpec` spec) . Just) m)
           ( NE.fromList
               [ "propagate (lookup HOLE ms) on (MemberSpec ms)"

libs/constrained-generators/src/Constrained/Spec/Map.hs

@@ -325,7 +325,7 @@ instance Logic SetW where
                 typeSpec
                   ( SetSpec
                       (Set.difference e s)
-                      ( memberSpecList
+                      ( memberSpec
                           (Set.toList e)
                           (pure "propagateSpec (union_ s HOLE) on (MemberSpec [e]) where e is the empty set")
                       )
@@ -364,7 +364,7 @@ instance Logic SetW where
             ]
   propagate MemberW ctx spec
     | (HOLE :? Value s :> Nil) <- ctx = caseBoolSpec spec $ \case
-        True -> memberSpecList (Set.toList s) (pure "propagateSpecFun on (Member x s) where s is Set.empty")
+        True -> memberSpec (Set.toList s) (pure "propagateSpecFun on (Member x s) where s is Set.empty")
         False -> notMemberSpec s
     | (Value e :! Unary HOLE) <- ctx = caseBoolSpec spec $ \case
         True -> typeSpec $ SetSpec (Set.singleton e) mempty mempty
@@ -389,7 +389,7 @@ instance Logic SetW where
             Nothing
             (Set.toList xs)
             TrueSpec
-            ( memberSpecList
+            ( memberSpec
                 (Set.toList xs)
                 (pure "propagateSpec (fromList_ HOLE) on (MemberSpec xs) where the set 'xs' is empty")
             )

libs/constrained-generators/src/Constrained/Spec/Set.hs

@@ -195,7 +195,7 @@ genNumList elemSIn foldSIn = do
 
     buildMemberSpec _ 0 es _ =
       pure
-        ( memberSpecList
+        ( memberSpec
             (Set.toList es)
             (pure "In genNumList, in buildMemberSpec 'es' is the empty list, can't make a MemberSpec from that")
         )
@@ -409,7 +409,7 @@ narrowByFuelAndSize fuel size specpair =
             possible x = x == u || xMinP <= u - x
             xs' = filter possible xs
       , xs' /= xs =
-          Just (memberSpecList (nubOrd xs') (pure ("None of " ++ show xs ++ " are possible")), foldS)
+          Just (memberSpec (nubOrd xs') (pure ("None of " ++ show xs ++ " are possible")), foldS)
       -- The lower bound on the number of elements is too low
       | Just e <- knownLowerBound elemS
       , e > 0