From 927d2d8f56fb36d4d2f295b6f1f534dfb3678ec2 Mon Sep 17 00:00:00 2001 From: Maximilian Algehed Date: Thu, 4 Sep 2025 09:39:44 +0200 Subject: [PATCH] remove minimal implementation --- constrained-generators.cabal | 26 - testlib/Test/Minimal/Base.hs | 501 ------------- testlib/Test/Minimal/Model.hs | 1228 -------------------------------- testlib/Test/Minimal/Syntax.hs | 1023 -------------------------- testlib/Test/Minimal/Tuple.hs | 356 --------- 5 files changed, 3134 deletions(-) delete mode 100644 testlib/Test/Minimal/Base.hs delete mode 100644 testlib/Test/Minimal/Model.hs delete mode 100644 testlib/Test/Minimal/Syntax.hs delete mode 100644 testlib/Test/Minimal/Tuple.hs diff --git a/constrained-generators.cabal b/constrained-generators.cabal index 0998370..a271f63 100644 --- a/constrained-generators.cabal +++ b/constrained-generators.cabal @@ -121,32 +121,6 @@ library examples prettyprinter, random, -library testlib - exposed-modules: - Test.Minimal.Base - Test.Minimal.Model - Test.Minimal.Syntax - Test.Minimal.Tuple - - hs-source-dirs: testlib - default-language: Haskell2010 - ghc-options: - -Wall - -Wcompat - -Wincomplete-record-updates - -Wincomplete-uni-patterns - -Wpartial-fields - -Wredundant-constraints - -Wunused-packages - - build-depends: - QuickCheck >=2.14, - base >=4.18 && <5, - constrained-generators, - containers, - mtl, - prettyprinter, - test-suite constrained type: exitcode-stdio-1.0 main-is: Tests.hs diff --git a/testlib/Test/Minimal/Base.hs b/testlib/Test/Minimal/Base.hs deleted file mode 100644 index 501595a..0000000 --- a/testlib/Test/Minimal/Base.hs +++ /dev/null @@ -1,501 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} - --- Base types: Term, Pred, Spec, Ctx, and classes: HasSpec, Syntax, Semantics, and Logic for the MinModel -module Test.Minimal.Base where - -import Constrained.Core (Evidence (..), Var (..), eqVar) -import Constrained.GenT -import Constrained.List hiding (ListCtx) -import Data.Kind -import Data.List.NonEmpty (NonEmpty (..)) -import qualified Data.List.NonEmpty as NE -import Data.String (fromString) -import Data.Typeable -import GHC.Stack -import Prettyprinter - --- =========================================== --- Terms --- =========================================== - -type AppRequires t dom rng = - ( Logic t - , TypeList dom - , Eq (t dom rng) - , Show (t dom rng) - , Typeable dom - , Typeable rng - , All HasSpec dom - , HasSpec rng - ) - -data Term a where - App :: - forall t dom rng. - AppRequires t dom rng => - t dom rng -> - List Term dom -> - Term rng - Lit :: (Typeable a, Eq a, Show a) => a -> Term a - V :: HasSpec a => Var a -> Term a - -instance Eq (Term a) where - V x == V x' = x == x' - Lit a == Lit b = a == b - App (w1 :: x1) (ts :: List Term dom1) == App (w2 :: x2) (ts' :: List Term dom2) = - case (eqT @dom1 @dom2, eqT @x1 @x2) of - (Just Refl, Just Refl) -> - w1 == w2 - && sameTerms ts ts' - _ -> False - _ == _ = False - --- | If the list is composed solely of literals, apply the function to get a value -applyFunSym :: - forall t ds rng. - (Typeable rng, Eq rng, Show rng, Semantics t) => FunTy ds rng -> List Term ds -> Maybe rng -applyFunSym f Nil = Just f -applyFunSym f (Lit x :> xs) = applyFunSym @t (f x) xs -applyFunSym _ _ = Nothing - -reducesToLit :: Term a -> Maybe a -reducesToLit (Lit n) = Just n -reducesToLit (V _) = Nothing -reducesToLit (App (f :: t ds r) xs) = applyFunSym @t (semantics f) xs - --- How to compare the args of two applications for equality -sameTerms :: All HasSpec as => List Term as -> List Term as -> Bool -sameTerms Nil Nil = True -sameTerms (x :> xs) (y :> ys) = x == y && sameTerms xs ys - --- =========================================== --- Function Symbol Classes --- =========================================== - --- | Syntactic operations are ones that have to do with the structure and appearence of the type. -class Syntax (t :: [Type] -> Type -> Type) where - inFix :: forall dom rng. t dom rng -> Bool - inFix _ = False - name :: forall dom rng. t dom rng -> String - --- | Semantic operations are ones that give the function symbol, meaning as a function. --- I.e. how to apply the function to a list of arguments and return a value, --- or to apply meaning preserving rewrite rules. -class Syntax t => Semantics (t :: [Type] -> Type -> Type) where - semantics :: forall d r. t d r -> FunTy d r -- e.g. FunTy '[a,Int] Bool == a -> Int -> Bool - rewriteRules :: - forall ds rng. - (TypeList ds, Typeable ds, HasSpec rng, All HasSpec ds) => - t ds rng -> List Term ds -> Evidence (Typeable rng, Eq rng, Show rng) -> Maybe (Term rng) - rewriteRules t l Evidence = Lit <$> (applyFunSym @t (semantics t) l) - --- | Logical operations are one that support reasoning about how a function symbol --- relates to logical properties, that we call Spec's -class (Typeable t, Syntax t, Semantics t) => Logic (t :: [Type] -> Type -> Type) where - {-# MINIMAL propagate | (propagateTypeSpec, propagateMemberSpec) #-} - - propagateTypeSpec :: - (AppRequires t as b, HasSpec a) => - t as b -> ListCtx as (HOLE a) -> TypeSpec b -> [b] -> Spec a - propagateTypeSpec f ctx ts cant = propagate f ctx (TypeSpec ts cant) - - propagateMemberSpec :: - (AppRequires t as b, HasSpec a) => - t as b -> ListCtx as (HOLE a) -> NonEmpty b -> Spec a - propagateMemberSpec f ctx xs = propagate f ctx (MemberSpec xs) - - propagate :: - (AppRequires t as b, HasSpec a) => - t as b -> ListCtx as (HOLE a) -> Spec b -> Spec a - propagate _ _ TrueSpec = TrueSpec - propagate _ _ (ErrorSpec es) = ErrorSpec es - propagate f ctx (SuspendedSpec v ps) = constrained $ \v' -> Let (App f (fromListCtx ctx v')) (v :-> ps) - propagate f ctx (TypeSpec ts cant) = propagateTypeSpec f ctx ts cant - propagate f ctx (MemberSpec xs) = propagateMemberSpec f ctx xs - --- =========================== --- Pred --- =========================== - -data Pred where - ElemPred :: forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred - And :: [Pred] -> Pred - Exists :: ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred - ForAll :: (Container t a, HasSpec t, HasSpec a) => Term t -> Binder a -> Pred - DependsOn :: (HasSpec a, HasSpec b) => Term a -> Term b -> Pred - Assert :: Term Bool -> Pred - TruePred :: Pred - FalsePred :: NonEmpty String -> Pred - Case :: HasSpec (Either a b) => Term (Either a b) -> Binder a -> Binder b -> Pred - Let :: Term a -> Binder a -> Pred - Subst :: HasSpec a => Var a -> Term a -> Pred -> Pred - -data Binder a where - (:->) :: HasSpec a => Var a -> Pred -> Binder a - -class Container t e | t -> e where - fromForAllSpec :: (HasSpec t, HasSpec e) => Spec e -> Spec t - forAllToList :: t -> [e] - -data Binders as where - Binds :: All HasSpec as => List Var as -> Pred -> Binders as - -data Bind a where - Bind :: HasSpec a => {varBind :: Var a, termBind :: Term a} -> Bind a - -toBind :: All HasSpec as => List Term as -> List Var as -> List Bind as -toBind Nil Nil = Nil -toBind (t :> ts) (v :> vs) = (Bind v t :> toBind ts vs) - --- ================================ --- Spec --- ================================ - -data Spec a where - TrueSpec :: Spec a - ErrorSpec :: NonEmpty String -> Spec a - SuspendedSpec :: HasSpec a => Var a -> Pred -> Spec a -- Maybe we elide this at first - MemberSpec :: NonEmpty a -> Spec a - TypeSpec :: HasSpec a => TypeSpec a -> [a] -> Spec a - -typeSpec :: HasSpec a => TypeSpec a -> Spec a -typeSpec ts = TypeSpec ts mempty - -constrained :: forall a. HasSpec a => (Term a -> Pred) -> Spec a -constrained body = - let x :-> p = bind body - in SuspendedSpec x p - -bind :: HasSpec a => (Term a -> Pred) -> Binder a -bind bodyf = newv :-> bodyPred - where - bodyPred = {- toPred -} body - newv = Var (nextVar bodyPred) "v" - body = bodyf (V newv) - - nextVar q = 1 + bound q - - boundBinder :: Binder a -> Int - boundBinder (x :-> p) = max (nameOf x) (bound p) - - bound (ElemPred _ _ _) = -1 - bound (Subst x _ p) = max (nameOf x) (bound p) - bound (And ps) = maximum $ (-1) : map bound ps -- (-1) as the default to get 0 as `nextVar p` - bound (Let _ b) = boundBinder b - bound (ForAll _ b) = boundBinder b - bound (Exists _ b) = boundBinder b - bound (Case _ ba bb) = max (boundBinder ba) (boundBinder bb) - bound Assert {} = -1 - bound TruePred = -1 - bound FalsePred {} = -1 - bound DependsOn {} = -1 - --- ======================================== --- HasSpec --- ======================================== - -class (Typeable a, Eq a, Show a, Show (TypeSpec a), Typeable (TypeSpec a)) => HasSpec a where - -- | The `TypeSpec a` is the type-specific `Spec a`. - type TypeSpec a - - -- `TypeSpec` behaves sort-of like a monoid with a neutral - -- element `anySpec` and a `combineSpec` for combining - -- two `TypeSpec a`. However, in order to provide flexibilty - -- `combineSpec` takes two `TypeSpec` and constucts a `Spec`. This - -- avoids e.g. having to have a separate implementation of `ErrorSpec` - -- and `MemberSpec` in `TypeSpec`. - - anySpec :: TypeSpec a - combineSpec :: TypeSpec a -> TypeSpec a -> Spec a - - -- | Generate a value that satisfies the `TypeSpec`. - -- The key property for this generator is soundness: - -- ∀ a ∈ genFromTypeSpec spec. a `conformsTo` spec - genFromTypeSpec :: (HasCallStack, MonadGenError m) => TypeSpec a -> GenT m a - - -- | Check conformance to the spec. - conformsTo :: HasCallStack => a -> TypeSpec a -> Bool - - -- | Convert a spec to predicates: - -- The key property here is: - -- ∀ a. a `conformsTo` spec == a `conformsTo` constrained (\t -> toPreds t spec) - toPreds :: Term a -> TypeSpec a -> Pred - - -- | This is used to detect self inconsistencies in a (TypeSpec t) - -- guardTypeSpec message ty --> ErrorSpec message, if ty is inconsistent - guardTypeSpec :: TypeSpec a -> Spec a - guardTypeSpec ty = typeSpec ty - --- ========================================= --- Contexts --- ========================================= - -data HOLE a b where - HOLE :: HOLE a a - -deriving instance Show (HOLE a b) - --- | Note the arrows (n :|> hole) and (hole :<| n) always point towards the term with --- type `(c x)`, (i.e. `hole` in the picture above) where the target variable must occur. -data ListCtx (as :: [Type]) (c :: Type -> Type) where - Unary :: c a -> ListCtx '[a] c - (:<|) :: c b -> x -> ListCtx '[b, x] c - (:|>) :: x -> c b -> ListCtx '[x, b] c - -data Ctx v (a :: Type) where - CtxHole :: HasSpec v => Ctx v v - CtxApp :: - ( AppRequires fn as b - , HasSpec b - , TypeList as - , Typeable as - , All HasSpec as - , Logic fn - ) => - fn as b -> ListCtx as (Ctx v) -> Ctx v b - -ctxHasSpec :: Ctx v a -> Evidence (HasSpec a) -ctxHasSpec CtxHole = Evidence -ctxHasSpec CtxApp {} = Evidence - --- | From a ListCtx, build a (List Term as), to which the function symbol can be applied. --- Hole becomes 't', values become `Lit` . -fromListCtx :: All HasSpec as => ListCtx as (HOLE a) -> Term a -> List Term as -fromListCtx (Unary HOLE) t = t :> Nil -fromListCtx (HOLE :<| y) t = t :> Lit y :> Nil -fromListCtx (x :|> HOLE) t = Lit x :> t :> Nil - ---- | Consider the term `((size_ x +. Lit 3) <=. Lit 12)` with a bunch of nested function symbols, with just 1 variable 'x' --- `(toCtx x term)` builds a context, with exactly one `CtxHole`, replacing the variable `x` --- `CtxApp <=. (CtxApp +. (CtxApp size_ (Unary CtxHole) :<| 3) :<| 12)` --- Working our way from outside in, we first propagate (<=.), then (+.), then (size_). This reduces in several steps --- 1) propagateSpec (CtxApp <=. (CtxApp +. (CtxApp size_ (Unary CtxHole) :<| 3) :<| 12)) $ spec --- 2) propagateSpec (CtxApp +. (CtxApp size_ (Unary CtxHole) :<| 3)) $ (propagate <=. (HOLE:<| 12)) --- 3) propagateSpec (CtxApp size_ (Unary CtxHole)) $ (propagate +. (HOLE:<| 3) (propagate <=. (HOLE :<| 12))) --- 4) propagateSpec CtxHole $ (propagate size_ Hole (propagate +. (HOLE:<| 3) (propagate <=. (HOLE :<| 12)))) --- 5) propagate size_ Hole (propagate +. (HOLE:<| 3) (propagate <=. (HOLE :<| 12))) --- Note the pattern in the code below. The recursize call to 'propagateSpec' is on the pattern variable `ctx` which is the --- part of the context pointed to by the arrows (:<|) and (:|>), and this recurive call to `propagateSpec` is --- applied to a new spec computed by 'propagate', where the variable `ctx` is replaced by HOLE. --- we end up on line 5), with three nested calls to `propagate` -propagateSpec :: - forall v a. - HasSpec v => - Ctx v a -> - Spec a -> - Spec v -propagateSpec context spec = case context of - CtxHole -> spec - CtxApp f (Unary ctx) | Evidence <- ctxHasSpec ctx -> propagateSpec ctx (propagate f (Unary HOLE) spec) - CtxApp f (ctx :<| v) | Evidence <- ctxHasSpec ctx -> propagateSpec ctx (propagate f (HOLE :<| v) spec) - CtxApp f (v :|> ctx) | Evidence <- ctxHasSpec ctx -> propagateSpec ctx (propagate f (v :|> HOLE) spec) - --- Construct a Ctx for a variable 'v', which should occur exactly once in the given Term. -toCtx :: - forall m v a. - (Typeable v, Show v, MonadGenError m, HasCallStack) => - Var v -> Term a -> m (Ctx v a) -toCtx v = go - where - go :: forall b. Term b -> m (Ctx v b) - go (Lit i) = - fatalErrorNE $ - NE.fromList - [ "toCtx applied to literal: (Lit " ++ show i ++ ")" - , "A context is always constructed from an (App f xs) term" - , "with a single occurence of the target variable " ++ show v ++ "@(" ++ show (typeOf v) ++ ")" - ] - go t@(App f xs) = CtxApp f <$> toCtxList (show t) v xs - go (V v') - | Just Refl <- eqVar v v' = pure $ CtxHole - | otherwise = - fatalErrorNE $ - NE.fromList - [ "A context is always constructed from an (App f xs) term with a single target variable" - , "which in this case is: " ++ show v ++ " :: (" ++ show (typeOf v) ++ ")" - , "Instead we found an unknown variable: " ++ show v' ++ " :: (" ++ show (typeOf v') ++ ")" - ] - -toCtxList :: - forall m v as. - (Show v, Typeable v, MonadGenError m, HasCallStack) => - String -> Var v -> List Term as -> m (ListCtx as (Ctx v)) -toCtxList termName v Nil = fatalErrorNE $ ("toCtxList without hole, for variable " ++ show v) :| [termName] -toCtxList termName v (V v' :> Nil) - | Just Refl <- eqVar v v' = pure $ Unary CtxHole - | otherwise = - fatalErrorNE $ - NE.fromList - [ "A context is always constructed from an (App f xs) term," - , "with a single occurence of the target variable " ++ show v ++ "@(" ++ show (typeOf v) ++ ")" - , "Instead we found an unknown variable " ++ show v' ++ "@(" ++ show (typeOf v') ++ ")" - , "in an application: " ++ termName - ] -toCtxList termName v (x :> y :> Nil) - | Just i <- reducesToLit x = do hole <- toCtx v y; pure $ (i :|> hole) - | Just i <- reducesToLit y = do hole <- toCtx v x; pure $ (hole :<| i) - | otherwise = - fatalErrorNE $ - "toCtx applied to an App with 2 parameters." - :| [ termName - , "The target variable we are searching for is " ++ show v - , "One of these parameters must reduce to a literal, which is not the case." - , "If both are non-literals, then term could have two variables, which is not allowed." - ] -toCtxList termName v xs = - fatalErrorNE $ - NE.fromList - [ "toCtx applied to an App with more than 2 parameters" - , termName - , "The target variable we are searching for is " ++ show v - , "All function symbols should have 1 or 2 parameters" - , "This one appears to accept " ++ show (lengthList xs) ++ "." - ] - --- =================================================================== --- Pretty Printer Helper functions --- =================================================================== - -data WithPrec a = WithPrec Int a - -parensIf :: Bool -> Doc ann -> Doc ann -parensIf True = parens -parensIf False = id - -prettyPrec :: Pretty (WithPrec a) => Int -> a -> Doc ann -prettyPrec p = pretty . WithPrec p - -ppList :: - forall f as ann. - All HasSpec as => -- can we use something other than All HasSpec as here? We know Function Symbol HERE - (forall a. HasSpec a => f a -> Doc ann) -> - List f as -> - [Doc ann] -ppList _ Nil = [] -ppList pp (a :> as) = pp a : ppList pp as - -ppList_ :: forall f as ann. (forall a. f a -> Doc ann) -> List f as -> [Doc ann] -ppList_ _ Nil = [] -ppList_ pp (a :> as) = pp a : ppList_ pp as - -prettyType :: forall t x. Typeable t => Doc x -prettyType = fromString $ show (typeRep (Proxy @t)) - -vsep' :: [Doc ann] -> Doc ann -vsep' = align . mconcat . punctuate hardline - -(/>) :: Doc ann -> Doc ann -> Doc ann -h /> cont = hang 2 $ sep [h, align cont] - -infixl 5 /> - -short :: forall a x. (Show a, Typeable a) => [a] -> Doc x -short [] = "[]" -short [x] = - let raw = show x - refined = if length raw <= 20 then raw else take 20 raw ++ " ... " - in "[" <+> fromString refined <+> "]" -short xs = - let raw = show xs - in if length raw <= 50 - then fromString raw - else "([" <+> viaShow (length xs) <+> "elements ...] @" <> prettyType @a <> ")" - -showType :: forall t. Typeable t => String -showType = show (typeRep (Proxy @t)) - --- ========================================================================== --- Pretty and Show instances --- ========================================================================== - --- ------------ Term ----------------- -instance Pretty (WithPrec (Term a)) where - pretty (WithPrec p t) = case t of - Lit n -> fromString $ showsPrec p n "" - V x -> viaShow x - App x Nil -> viaShow x - App f as - | inFix f - , a :> b :> Nil <- as -> - parensIf (p > 9) $ prettyPrec 10 a <+> viaShow f <+> prettyPrec 10 b - | otherwise -> parensIf (p > 10) $ viaShow f <+> align (fillSep (ppList (prettyPrec 11) as)) - -instance Pretty (Term a) where - pretty = prettyPrec 0 - -instance Show (Term a) where - showsPrec p t = shows $ pretty (WithPrec p t) - --- ------------ Pred ----------------- - -instance Pretty Pred where - pretty = \case - ElemPred True term vs -> - align $ - sep - [ "MemberPred" - , parens (pretty term) - , if length vs <= 2 - then brackets (fillSep (punctuate "," (map viaShow (NE.toList vs)))) - else "(" <> viaShow (length vs) <> " items)" - ] - ElemPred False term vs -> align $ sep ["notMemberPred", pretty term, fillSep (punctuate "," (map viaShow (NE.toList vs)))] - -- Exists _ (x :-> p) -> align $ sep ["exists" <+> viaShow x <+> "in", pretty p] - Let t (x :-> p) -> align $ sep ["let" <+> viaShow x <+> "=" /> pretty t <+> "in", pretty p] - And ps -> braces $ vsep' $ map pretty ps - Exists _ (x :-> p) -> align $ sep ["exists" <+> viaShow x <+> "in", pretty p] - Assert t -> "assert $" <+> pretty t - -- Reifies t' t _ -> "reifies" <+> pretty (WithPrec 11 t') <+> pretty (WithPrec 11 t) - DependsOn a b -> pretty a <+> "<-" /> pretty b - ForAll t (x :-> p) -> "forall" <+> viaShow x <+> "in" <+> pretty t <+> "$" /> pretty p - Case t as bs -> "case" <+> pretty t <+> "of" /> vsep' [pretty as, 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 - TruePred -> "True" - FalsePred {} -> "False" - --- Monitor {} -> "monitor" --- Explain es p -> "Explain" <+> viaShow (NE.toList es) <+> "$" /> pretty p - -instance Show Pred where - show = show . pretty - -instance Pretty (Binder a) where - pretty (x :-> p) = viaShow x <+> "->" <+> pretty p - --- ------------ Specifications ----------------- - -instance HasSpec a => Pretty (WithPrec (Spec a)) where - pretty (WithPrec d s) = case s of - ErrorSpec es -> "ErrorSpec" /> vsep' (map fromString (NE.toList es)) - TrueSpec -> fromString $ "TrueSpec @(" ++ showType @a ++ ")" - MemberSpec xs -> "MemberSpec" <+> short (NE.toList xs) - SuspendedSpec x p -> parensIf (d > 10) $ "constrained $ \\" <+> viaShow x <+> "->" /> pretty p - -- TODO: require pretty for `TypeSpec` to make this much nicer - TypeSpec ts cant -> - parensIf (d > 10) $ - "TypeSpec" - /> vsep - [ fromString (showsPrec 11 ts "") - , viaShow cant - ] - -instance HasSpec a => Pretty (Spec a) where - pretty = pretty . WithPrec 0 - -instance HasSpec a => Show (Spec a) where - showsPrec d = shows . pretty . WithPrec d diff --git a/testlib/Test/Minimal/Model.hs b/testlib/Test/Minimal/Model.hs deleted file mode 100644 index 5eeddee..0000000 --- a/testlib/Test/Minimal/Model.hs +++ /dev/null @@ -1,1228 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE ImportQualifiedPost #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PatternSynonyms #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE ViewPatterns #-} --- HasSpec instances for known types Integer, Bool, Set , (,) -{-# OPTIONS_GHC -Wno-orphans #-} - -module Test.Minimal.Model where - -import Constrained.Core ( - Evidence (..), - Var (..), - eqVar, - freshen, - unionWithMaybe, - ) -import Constrained.Env (Env) -import Constrained.Env qualified as Env -import Constrained.GenT -import Constrained.Graph qualified as Graph -import Constrained.List hiding (ListCtx) -import Control.Monad (guard) -import Control.Monad.Writer (Writer, runWriter, tell) -import Data.Foldable (fold) -import Data.Foldable qualified as Foldable (fold) -import Data.Kind -import Data.List (nub, partition, (\\)) -import Data.List.NonEmpty (NonEmpty (..)) -import Data.List.NonEmpty qualified as NE -import Data.Maybe (isNothing, listToMaybe, maybeToList) -import Data.Semigroup (Any (..)) -import Data.Set (Set) -import Data.Set qualified as Set -import Data.Typeable -import GHC.Stack -import Prettyprinter -import Test.Minimal.Base -import Test.Minimal.Syntax -import Test.QuickCheck hiding (forAll) - --- ==================================================== --- Now some concrete examples --- 1) Introduce the function symbols --- 2) Give the Syntax, Semantics, and Logic instances --- 3) Give the HasSpec instance --- ==================================================== - --- ======== Integer example ============== - -data IntegerSym (dom :: [Type]) rng where - PlusW :: IntegerSym '[Integer, Integer] Integer - MinusW :: IntegerSym '[Integer, Integer] Integer - NegateW :: IntegerSym '[Integer] Integer - LessOrEqW :: IntegerSym '[Integer, Integer] Bool - GreaterOrEqW :: IntegerSym '[Integer, Integer] Bool - -deriving instance Eq (IntegerSym dom rng) - -instance Show (IntegerSym dom rng) where show = name - -instance Syntax IntegerSym where - name PlusW = "+." - name MinusW = "-." - name NegateW = "negate_" - name LessOrEqW = "<=." - name GreaterOrEqW = ">=." - inFix NegateW = False - inFix _ = True - -instance Semantics IntegerSym where - semantics PlusW = (+) - semantics MinusW = (-) - semantics NegateW = negate - semantics LessOrEqW = (<=) - semantics GreaterOrEqW = (>=) - -instance Logic IntegerSym where - propagate tag ctx spec = case (tag, ctx, spec) of - (_, _, TrueSpec) -> TrueSpec - (_, _, ErrorSpec xs) -> ErrorSpec xs - (f, context, SuspendedSpec v ps) -> - constrained $ \v' -> Let (App f (fromListCtx context v')) (v :-> ps) - (LessOrEqW, HOLE :<| l, bspec) -> - caseBoolSpec bspec $ \case True -> leqSpec l; False -> gtSpec l - (LessOrEqW, l :|> HOLE, bspec) -> - caseBoolSpec bspec $ \case True -> geqSpec l; False -> ltSpec l - (GreaterOrEqW, HOLE :<| x, spec1) -> - propagate LessOrEqW (x :|> HOLE) spec1 - (GreaterOrEqW, x :|> HOLE, spec2) -> - propagate LessOrEqW (HOLE :<| x) spec2 - (NegateW, Unary HOLE, TypeSpec interval cant) -> typeSpec (negateRange interval) <> notMemberSpec (map negate cant) - (NegateW, Unary HOLE, MemberSpec xs) -> MemberSpec $ NE.nub $ fmap negate xs - (PlusW, HOLE :<| n, TypeSpec (Interval lo hi) bad) -> - TypeSpec (Interval ((minus n) <$> lo) ((minus n) <$> hi)) (map (minus n) bad) - (PlusW, HOLE :<| n, MemberSpec xs) -> - MemberSpec (fmap (minus n) xs) - (PlusW, n :|> HOLE, TypeSpec (Interval lo hi) bad) -> - TypeSpec (Interval ((minus n) <$> lo) ((minus n) <$> hi)) (map (minus n) bad) - (PlusW, n :|> HOLE, MemberSpec xs) -> MemberSpec (fmap (minus n) xs) - (MinusW, HOLE :<| n, TypeSpec (Interval lo hi) bad) -> - TypeSpec (Interval ((+ n) <$> lo) ((+ n) <$> hi)) (map (+ n) bad) - (MinusW, HOLE :<| n, MemberSpec xs) -> - MemberSpec (fmap (+ n) xs) - (MinusW, n :|> HOLE, TypeSpec (Interval lo hi) bad) -> - TypeSpec (negateRange (Interval ((minus n) <$> lo) ((minus n) <$> hi))) (map (minus n) bad) - (MinusW, n :|> HOLE, MemberSpec xs) -> - MemberSpec (fmap (minus n) xs) - -negateRange :: Range -> Range -negateRange (Interval ml mu) = Interval (negate <$> mu) (negate <$> ml) - -minus :: Integer -> Integer -> Integer -minus n x = n - x - -geqSpec :: Integer -> Spec Integer -geqSpec n = typeSpec (Interval (Just n) Nothing) - -leqSpec :: Integer -> Spec Integer -leqSpec n = typeSpec (Interval Nothing (Just n)) - -gtSpec :: Integer -> Spec Integer -gtSpec n = typeSpec (Interval (Just (n + 1)) Nothing) - -ltSpec :: Integer -> Spec Integer -ltSpec n = typeSpec (Interval Nothing (Just (n - 1))) - -(<=.) :: Term Integer -> Term Integer -> Term Bool -(<=.) x y = App LessOrEqW (x :> y :> Nil) - -(>=.) :: Term Integer -> Term Integer -> Term Bool -(>=.) x y = App GreaterOrEqW (x :> y :> Nil) - -(+.) :: Term Integer -> Term Integer -> Term Integer -(+.) x y = App PlusW (x :> y :> Nil) - -(-.) :: Term Integer -> Term Integer -> Term Integer -(-.) x y = App MinusW (x :> y :> Nil) - -negate_ :: Term Integer -> Term Integer -negate_ x = App NegateW (x :> Nil) - --- ========================= --- HasSpec Integer instance - -data Range = Interval (Maybe Integer) (Maybe Integer) deriving (Eq, Show) - -instance Semigroup Range where - Interval ml mu <> Interval ml' mu' = - Interval - (unionWithMaybe max ml ml') - (unionWithMaybe min mu mu') - -instance Monoid Range where - mempty = Interval Nothing Nothing - -instance HasSpec Integer where - type TypeSpec Integer = Range - - -- \| From -∞ to +∞ - anySpec = Interval Nothing Nothing - - -- \| Catch inconsistencies after using Monoid operation of the two Ranges. - combineSpec s s' = guardTypeSpec (s <> s') - - -- \| In Interval where the lo bound is greater than the hi bound is inconsistent - guardTypeSpec r@(Interval (Just n) (Just m)) - | n > m = ErrorSpec (pure ("lower bound greater than upper bound\n" ++ show r)) - | otherwise = typeSpec r - guardTypeSpec range = typeSpec range - - genFromTypeSpec (Interval ml mu) = do - n <- sizeT - chooseT =<< constrainInterval ml mu (fromIntegral n) - - conformsTo i (Interval ml mu) = maybe True (<= i) ml && maybe True (i <=) mu - - toPreds v (Interval ml mu) = - Foldable.fold $ - [Assert $ Lit l <=. v | l <- maybeToList ml] - ++ [Assert $ v <=. Lit u | u <- maybeToList mu] - -constrainInterval :: - MonadGenError m => Maybe Integer -> Maybe Integer -> Integer -> m (Integer, Integer) -constrainInterval ml mu qcSize = - case (ml, mu) of - (Nothing, Nothing) -> pure (-qcSize', qcSize') - (Just l, Nothing) - | l < 0 -> pure (max l (negate qcSize'), qcSize') - | otherwise -> pure (l, l + 2 * qcSize') - (Nothing, Just u) - | u > 0 -> pure (negate qcSize', min u qcSize') - | otherwise -> pure (u - qcSize' - qcSize', u) - (Just l, Just u) - | l > u -> genError ("bad interval: " ++ show l ++ " " ++ show u) - | u < 0 -> pure (safeSub l (safeSub l u qcSize') qcSize', u) - | l >= 0 -> pure (l, safeAdd u (safeAdd u l qcSize') qcSize') - -- TODO: this is a bit suspect if the bounds are lopsided - | otherwise -> pure (max l (-qcSize'), min u qcSize') - where - qcSize' = abs $ fromInteger qcSize - -- FIX THIS TO WORK just on Integer, Should be much simpler, as Integer has no undeflow or overflow. - safeSub l a b - | a - b > a = l - | otherwise = max l (a - b) - safeAdd u a b - | a + b < a = u - | otherwise = min u (a + b) - --- ========== Bool example ================== - -data BoolSym (dom :: [Type]) rng where - NotW :: BoolSym '[Bool] Bool - -deriving instance Eq (BoolSym dom rng) - -instance Show (BoolSym dom rng) where show = name - -instance Syntax BoolSym where - name NotW = "not_" - inFix _ = False - -instance Semantics BoolSym where - semantics NotW = not - -instance Logic BoolSym where - propagate _ _ TrueSpec = TrueSpec - propagate _ _ (ErrorSpec msgs) = ErrorSpec msgs - propagate NotW (Unary HOLE) (SuspendedSpec v ps) = - constrained $ \v' -> Let (App NotW (v' :> Nil)) (v :-> ps) - propagate NotW (Unary HOLE) spec = - caseBoolSpec spec (equalSpec . not) - -not_ :: Term Bool -> Term Bool -not_ x = App NotW (x :> Nil) - --- ========================= --- HasSpec Bool instance - -instance HasSpec Bool where - type TypeSpec Bool = Set Bool - - anySpec = Set.fromList [False, True] - - combineSpec s s' = typeSpec (Set.union s s') - - genFromTypeSpec set - | Set.null set = fatalError "genFromTypeSpec @Set where the typeSpec is Set.empty" - | otherwise = oneofT (map pure (Set.toList set)) - - guardTypeSpec s - | Set.null s = ErrorSpec $ pure "guardTypeSpec @Set where the typeSpec is Set.empty" - | otherwise = TypeSpec s [] - - conformsTo i set = Set.member i set - - toPreds v set = case Set.toList set of - [] -> FalsePred (pure "toPreds @Set where the typeSpec is Set.empty") - (x : xs) -> ElemPred True v (x :| xs) - --- ========== Set example ======================= - -data SetSym (dom :: [Type]) rng where - MemberW :: (HasSpec a, Ord a) => SetSym [a, Set a] Bool - SizeW :: (HasSpec a, Ord a) => SetSym '[Set a] Integer - SubsetW :: (HasSpec a, Ord a) => SetSym [Set a, Set a] Bool - -deriving instance Eq (SetSym dom rng) - -instance Show (SetSym dom rng) where show = name - -instance Syntax SetSym where - name MemberW = "member_" - name SizeW = "size_" - name SubsetW = "subset_" - inFix _ = False - -instance Semantics SetSym where - semantics MemberW = Set.member - semantics SizeW = setSize - semantics SubsetW = Set.isSubsetOf - - rewriteRules SubsetW (Lit s :> _ :> Nil) Evidence | null s = Just $ Lit True - rewriteRules SubsetW (x :> Lit s :> Nil) Evidence | null s = Just $ x ==. Lit Set.empty - rewriteRules MemberW (t :> Lit s :> Nil) Evidence - | null s = Just $ Lit False - | [a] <- Set.toList s = Just $ t ==. Lit a - rewriteRules t l Evidence = Lit <$> (applyFunSym @SetSym (semantics t) l) - -instance Logic SetSym where - propagate tag ctx spec = case (tag, ctx, spec) of - (_, _, TrueSpec) -> TrueSpec - (_, _, ErrorSpec es) -> ErrorSpec es - (f, context, SuspendedSpec v ps) -> constrained $ \v' -> Let (App f (fromListCtx context v')) (v :-> ps) - (MemberW, HOLE :<| (s :: Set a), spec1) -> - caseBoolSpec spec1 $ \case - True -> memberSpec (Set.toList s) (pure "propagateSpecFun on (Member x s) where s is Set.empty") - False -> notMemberSpec s - (MemberW, e :|> HOLE, spec2) -> - caseBoolSpec spec2 $ \case - True -> typeSpec $ SetSpec (Set.singleton e) mempty mempty - False -> typeSpec $ SetSpec mempty (notEqualSpec e) mempty - (SizeW, Unary HOLE, spec3) -> typeSpec (SetSpec mempty mempty spec3) - (SubsetW, HOLE :<| big, spec4) -> caseBoolSpec spec4 $ \case - True -> constrained $ \small -> - And - [ Assert $ size_ small <=. Lit (setSize big) - , forAll small $ \x -> Assert $ member_ x (Lit big) - ] - False -> constrained $ \small -> - exists (\eval -> headGE $ Set.difference big (eval small)) $ \e -> - And - [ -- set `DependsOn` e, - Assert $ not_ $ member_ e (Lit big) - , Assert $ member_ e small - ] - (SubsetW, small :|> HOLE, spec5) -> caseBoolSpec spec5 $ \case - True -> typeSpec $ SetSpec small TrueSpec mempty - False -> constrained $ \big -> - exists (\eval -> headGE $ Set.difference (eval big) small) $ \e -> - And - [ -- set `DependsOn` e, - Assert $ member_ e (Lit small) - , Assert $ not_ $ member_ e big - ] - -setSize :: Set a -> Integer -setSize = toInteger . Set.size - -size_ :: (HasSpec s, Ord s) => Term (Set s) -> Term Integer -size_ s = App SizeW (s :> Nil) - -subset_ :: (HasSpec s, Ord s) => Term (Set s) -> Term (Set s) -> Term Bool -subset_ s1 s2 = App SubsetW (s1 :> s2 :> Nil) - -member_ :: (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool -member_ x y = App MemberW (x :> y :> Nil) - --- Helpers for the `HasSpec (Set s)` instance - -instance Ord s => Container (Set s) s where - fromForAllSpec e = typeSpec $ SetSpec mempty e TrueSpec - forAllToList = Set.toList - -data SetSpec a = SetSpec {setMust :: Set a, setAll :: Spec a, setCount :: Spec Integer} - deriving (Show) - -guardSetSpec :: (HasSpec a, Ord a) => SetSpec a -> Spec (Set a) -guardSetSpec (SetSpec must elemS ((<> geqSpec 0) -> size)) - | Just u <- knownUpperBound size - , u < 0 = - ErrorSpec (("guardSetSpec: negative size " ++ show u) :| []) - | not (all (`conformsToSpec` elemS) must) = - ErrorSpec (("Some 'must' items do not conform to 'element' spec: " ++ show elemS) :| []) - | isErrorLike size = ErrorSpec ("guardSetSpec: error in size" :| []) - | isErrorLike (geqSpec (setSize must) <> size) = - ErrorSpec $ - ("Must set size " ++ show (setSize must) ++ ", is inconsistent with SetSpec size" ++ show size) - :| [] - | otherwise = typeSpec (SetSpec must elemS size) - -knownUpperBound :: Spec Integer -> Maybe Integer -knownUpperBound TrueSpec = Nothing -knownUpperBound (MemberSpec as) = Just $ maximum as -knownUpperBound ErrorSpec {} = Nothing -knownUpperBound SuspendedSpec {} = Nothing -knownUpperBound (TypeSpec (Interval lo hi) cant) = upper lo hi - where - upper _ Nothing = Nothing - upper Nothing (Just b) = listToMaybe $ [b, b - 1 ..] \\ cant - upper (Just a) (Just b) - | a == b = a <$ guard (a `notElem` cant) - | otherwise = listToMaybe $ [b, b - 1 .. a] \\ cant - -instance (Ord a, HasSpec a) => Semigroup (SetSpec a) where - SetSpec must es size <> SetSpec must' es' size' = - SetSpec (must <> must') (es <> es') (size <> size') - -instance (Ord a, HasSpec a) => Monoid (SetSpec a) where - mempty = SetSpec mempty mempty TrueSpec - --- ========================= --- HasSpec Set instance - -instance (Container (Set a) a, Ord a, HasSpec a) => HasSpec (Set a) where - type TypeSpec (Set a) = SetSpec a - - anySpec = SetSpec Set.empty TrueSpec TrueSpec - - combineSpec x y = guardSetSpec (x <> y) - - conformsTo s (SetSpec must es size) = - and - [ setSize s `conformsToSpec` size - , must `Set.isSubsetOf` s - , all (`conformsToSpec` es) s - ] - - toPreds s (SetSpec m es size) = - Foldable.fold $ - -- Don't include this if the must set is empty - [Assert $ subset_ (Lit m) s | not $ Set.null m] - ++ [ forAll s (\e -> satisfies e es) - , satisfies (size_ s) size - ] - - guardTypeSpec = guardSetSpec - - genFromTypeSpec (SetSpec must e _) - | any (not . (`conformsToSpec` e)) must = - genErrorNE - ( NE.fromList - [ "Failed to generate set" - , "Some element in the must set does not conform to the elem specification" - , "Unconforming elements from the must set:" - , unlines (map (\x -> " " ++ show x) (filter (not . (`conformsToSpec` e)) (Set.toList must))) - , "Element Specifcation" - , " " ++ show e - ] - ) - -- Special case when elemS is a MemberSpec. - -- Just union 'must' with enough elements of 'xs' to meet 'szSpec' - genFromTypeSpec (SetSpec must (MemberSpec xs) szSpec) = do - let szSpec' = szSpec <> geqSpec (setSize must) -- <> maxSpec (cardinality elemS) - choices <- pureGen $ shuffle (NE.toList xs \\ Set.toList must) - size <- fromInteger <$> genFromSpecT szSpec' - let additions = Set.fromList $ take (size - Set.size must) choices - pure (Set.union must additions) - genFromTypeSpec (SetSpec must elemS szSpec) = do - let szSpec' = szSpec <> geqSpec (setSize must) -- <> maxSpec (cardinality elemS) - sizecount <- - explain "Choose a size for the Set to be generated" $ - genFromSpecT szSpec' - let targetSize = sizecount - setSize must - explainNE - ( NE.fromList - [ "Choose size count = " ++ show sizecount - , "szSpec' = " ++ show szSpec' - , "Picking items not in must = " ++ show (Set.toList must) - , "that also meet the element test: " - , " " ++ show elemS - ] - ) - $ go 100 targetSize must - where - go _ n s | n <= 0 = pure s - go tries n s = do - e <- - explainNE - ( NE.fromList - [ "Generate set member at type " ++ showType @a - , " number of items starting with = " ++ show (Set.size must) - , " number of items left to pick = " ++ show n - , " number of items already picked = " ++ show (Set.size s) - ] - ) - $ withMode Strict - $ suchThatWithTryT tries (genFromSpecT elemS) (`Set.notMember` s) - - go tries (n - 1) (Set.insert e s) - --- ========== Pairs example ======================= - -pattern Pair :: - forall c. () => forall a b. (c ~ (a, b), HasSpec a, HasSpec b) => Term a -> Term b -> Term c -pattern Pair x y <- App (getWitness -> Just PairW) (x :> y :> Nil) - -data PairSym (dom :: [Type]) rng where - FstW :: PairSym '[(a, b)] a - SndW :: PairSym '[(a, b)] b - PairW :: PairSym '[a, b] (a, b) - -deriving instance Eq (PairSym dom rng) - -instance Show (PairSym dom rng) where show = name - -instance Syntax PairSym where - name FstW = "fst_" - name SndW = "snd_" - name PairW = "pair_" - inFix _ = False - -instance Semantics PairSym where - semantics FstW = fst - semantics SndW = snd - semantics PairW = (,) - rewriteRules FstW (Pair x _ :> Nil) Evidence = Just x - rewriteRules SndW (Pair _ y :> Nil) Evidence = Just y - rewriteRules t l Evidence = Lit <$> applyFunSym @PairSym (semantics t) l - -instance Logic PairSym where - propagateTypeSpec FstW (Unary HOLE) ts cant = typeSpec $ Cartesian (TypeSpec ts cant) TrueSpec - propagateTypeSpec SndW (Unary HOLE) ts cant = typeSpec $ Cartesian TrueSpec (TypeSpec ts cant) - propagateTypeSpec PairW (a :|> HOLE) sc@(Cartesian sa sb) cant - | a `conformsToSpec` sa = sb <> foldMap notEqualSpec (sameFst a cant) - | otherwise = - ErrorSpec - ( NE.fromList - ["propagate (pair_ " ++ show a ++ " HOLE) has conformance failure on a", show (TypeSpec sc cant)] - ) - propagateTypeSpec PairW (HOLE :<| b) sc@(Cartesian sa sb) cant - | b `conformsToSpec` sb = sa <> foldMap notEqualSpec (sameSnd b cant) - | otherwise = - ErrorSpec - ( NE.fromList - ["propagate (pair_ HOLE " ++ show b ++ ") has conformance failure on b", show (TypeSpec sc cant)] - ) - - propagateMemberSpec FstW (Unary HOLE) es = typeSpec $ Cartesian (MemberSpec es) TrueSpec - propagateMemberSpec SndW (Unary HOLE) es = typeSpec $ Cartesian TrueSpec (MemberSpec es) - propagateMemberSpec PairW (a :|> HOLE) es = - case (nub (sameFst a (NE.toList es))) of - (w : ws) -> MemberSpec (w :| ws) - [] -> - ErrorSpec $ - NE.fromList - [ "propagate (pair_ HOLE " ++ show a ++ ") on (MemberSpec " ++ show (NE.toList es) - , "Where " ++ show a ++ " does not appear as the fst component of anything in the MemberSpec." - ] - propagateMemberSpec PairW (HOLE :<| b) es = - case (nub (sameSnd b (NE.toList es))) of - (w : ws) -> MemberSpec (w :| ws) - [] -> - ErrorSpec $ - NE.fromList - [ "propagate (pair_ HOLE " ++ show b ++ ") on (MemberSpec " ++ show (NE.toList es) - , "Where " ++ show b ++ " does not appear as the snd component of anything in the MemberSpec." - ] - -sameFst :: Eq a1 => a1 -> [(a1, a2)] -> [a2] -sameFst a ps = [b | (a', b) <- ps, a == a'] - -sameSnd :: Eq a1 => a1 -> [(a2, a1)] -> [a2] -sameSnd b ps = [a | (a, b') <- ps, b == b'] - -fst_ :: (HasSpec a, HasSpec b) => Term (a, b) -> Term a -fst_ x = App FstW (x :> Nil) - -snd_ :: (HasSpec a, HasSpec b) => Term (a, b) -> Term b -snd_ x = App SndW (x :> Nil) - -pair_ :: (HasSpec a, HasSpec b) => Term a -> Term b -> Term (a, b) -pair_ a b = App PairW (a :> b :> Nil) - --- ========== The Pair (a,b) HasSpec instance - -data PairSpec a b = Cartesian (Spec a) (Spec b) - -instance (HasSpec a, HasSpec b) => Show (PairSpec a b) where - show (Cartesian l r) = "(Cartesian " ++ "(" ++ show l ++ ") (" ++ show r ++ "))" - -instance (HasSpec a, HasSpec b) => Semigroup (PairSpec a b) where - (Cartesian x y) <> (Cartesian a b) = Cartesian (x <> a) (y <> b) - -instance (HasSpec a, HasSpec b) => Monoid (PairSpec a b) where mempty = Cartesian mempty mempty - -guardPair :: forall a b. (HasSpec a, HasSpec b) => Spec a -> Spec b -> Spec (a, b) -guardPair specA specB = handleErrors specA specB (\s t -> typeSpec (Cartesian s t)) - -instance (HasSpec a, HasSpec b) => HasSpec (a, b) where - type TypeSpec (a, b) = PairSpec a b - - anySpec = Cartesian mempty mempty - - combineSpec (Cartesian a b) (Cartesian a' b') = guardPair (a <> a') (b <> b') - - conformsTo (a, b) (Cartesian sa sb) = conformsToSpec a sa && conformsToSpec b sb - - guardTypeSpec (Cartesian x y) = guardPair x y - - genFromTypeSpec (Cartesian sa sb) = (,) <$> genFromSpecT sa <*> genFromSpecT sb - - toPreds x (Cartesian sf ss) = - satisfies (fst_ x) sf - <> satisfies (snd_ x) ss - --- ========== Either example ======================= - -data EitherSym (dom :: [Type]) rng where - LeftW :: EitherSym '[a] (Either a b) - RightW :: EitherSym '[b] (Either a b) - -deriving instance Eq (EitherSym dom rng) - -instance Show (EitherSym dom rng) where show = name - -instance Syntax EitherSym where - name LeftW = "left_" - name RightW = "right_" - inFix _ = False - -instance Semantics EitherSym where - semantics LeftW = Left - semantics RightW = Right - -instance Logic EitherSym where - propagateTypeSpec LeftW (Unary HOLE) (SumSpec sl _) cant = sl <> foldMap notEqualSpec [a | Left a <- cant] - propagateTypeSpec RightW (Unary HOLE) (SumSpec _ sr) cant = sr <> foldMap notEqualSpec [a | Right a <- cant] - - propagateMemberSpec LeftW (Unary HOLE) es = - case [a | Left a <- NE.toList es] of - (x : xs) -> MemberSpec (x :| xs) - [] -> - ErrorSpec $ - pure $ - "propMemberSpec (left_ HOLE) on (MemberSpec es) with no Left in es: " ++ show (NE.toList es) - propagateMemberSpec RightW (Unary HOLE) es = - case [a | Right a <- NE.toList es] of - (x : xs) -> MemberSpec (x :| xs) - [] -> - ErrorSpec $ - pure $ - "propagate (Right HOLE) on (MemberSpec es) with no Right in es: " ++ show (NE.toList es) - -left_ :: (HasSpec a, HasSpec b) => Term a -> Term (Either a b) -left_ x = App LeftW (x :> Nil) - -right_ :: (HasSpec a, HasSpec b) => Term b -> Term (Either a b) -right_ x = App RightW (x :> Nil) - --- ========== The Either HasSpec instance - -data SumSpec a b = SumSpec a b - -deriving instance (Eq a, Eq b) => Eq (SumSpec a b) - -deriving instance (Show a, Show b) => Show (SumSpec a b) - -guardSum :: forall a b. (HasSpec a, HasSpec b) => Spec a -> Spec b -> Spec (Either a b) -guardSum (ErrorSpec es) (ErrorSpec fs) = ErrorSpec (es <> fs) -guardSum (ErrorSpec es) _ = ErrorSpec (NE.cons "sum error on left" es) -guardSum _ (ErrorSpec es) = ErrorSpec (NE.cons "sum error on right" es) -guardSum s s' = typeSpec $ SumSpec s s' - -instance (HasSpec a, HasSpec b) => HasSpec (Either a b) where - type TypeSpec (Either a b) = SumSpec (Spec a) (Spec b) - - anySpec = SumSpec mempty mempty - - combineSpec (SumSpec a b) (SumSpec c d) = guardSum (a <> c) (b <> d) - - conformsTo (Left a) (SumSpec sa _) = conformsToSpec a sa - conformsTo (Right b) (SumSpec _ sb) = conformsToSpec b sb - - toPreds x (SumSpec a b) = Case x (bind $ \y -> satisfies y a) (bind $ \y -> satisfies y b) - - genFromTypeSpec (SumSpec (simplifySpec -> sa) (simplifySpec -> sb)) - | emptyA, emptyB = genError "genFromTypeSpec @SumSpec: empty" - | emptyA = Right <$> genFromSpecT sb - | emptyB = Left <$> genFromSpecT sa - | otherwise = oneofT [Left <$> genFromSpecT sa, Right <$> genFromSpecT sb] - where - emptyA = isErrorLike sa - emptyB = isErrorLike sb - --- ========== List example =================== - -data ListSym (dom :: [Type]) rng where - ElemW :: Eq a => ListSym [a, [a]] Bool - LengthW :: ListSym '[[a]] Integer - -instance Syntax ListSym where - name ElemW = "elem_" - name LengthW = "length_" - inFix _ = False - -instance Semantics ListSym where - semantics ElemW = elem - semantics LengthW = toInteger . length - --- ========================================================================= --- User Facing functions --- ==================================================================== - --- | Generalize `genFromTypeSpec` from `TypeSpec t` to `Spec t` --- Generate a value that satisfies the spec. This function can fail if the --- spec is inconsistent, there is a dependency error, or if the underlying --- generators are not flexible enough. -genFromSpecT :: - forall a m. (HasCallStack, HasSpec a, MonadGenError m) => Spec a -> GenT m a -genFromSpecT (simplifySpec -> spec) = case spec of - MemberSpec as -> explain ("genFromSpecT on spec" ++ show spec) $ pureGen (elements (NE.toList as)) - TrueSpec -> genFromSpecT (typeSpec $ anySpec @a) - SuspendedSpec x p - -- NOTE: If `x` isn't free in `p` we still have to try to generate things - -- from `p` to make sure `p` is sat and then we can throw it away. A better - -- approach would be to only do this in the case where we don't know if `p` - -- is sat. The proper way to implement such a sat check is to remove - -- sat-but-unnecessary variables in the optimiser. - | not $ Name x `appearsIn` p -> do - !_ <- genFromPreds mempty p - genFromSpecT TrueSpec - | otherwise -> do - env <- genFromPreds mempty p - Env.find env x - TypeSpec s cant -> do - mode <- getMode - explainNE - ( NE.fromList - [ "genFromSpecT on (TypeSpec tspec cant) at type " ++ showType @a - , "tspec = " - , show s - , "cant = " ++ show cant - , "with mode " ++ show mode - ] - ) - $ - -- TODO: we could consider giving `cant` as an argument to `genFromTypeSpec` if this - -- starts giving us trouble. - genFromTypeSpec s `suchThatT` (`notElem` cant) - ErrorSpec e -> genErrorNE e - --- | A version of `genFromSpecT` that simply errors if the generator fails -genFromSpec :: forall a. (HasCallStack, HasSpec a) => Spec a -> Gen a -genFromSpec spec = do - res <- catchGen $ genFromSpecT @a @GE spec - either (error . ('\n' :) . catMessages) pure res - --- | A version of `genFromSpecT` that runs in the IO monad. Good for debugging. -debugSpec :: forall a. HasSpec a => Spec a -> IO () -debugSpec spec = do - ans <- generate $ genFromGenT $ inspect (genFromSpecT spec) - let f x = putStrLn (unlines (NE.toList x)) - ok x = - if conformsToSpec x spec - then putStrLn "True" - else putStrLn "False, perhaps there is an unsafeExists in the spec?" - case ans of - FatalError xs -> mapM_ f xs - GenError xs -> mapM_ f xs - Result x -> print spec >> print (simplifySpec spec) >> print x >> ok x - --- | Generate a satisfying `Env` for a `p : Pred fn`. The `Env` contains values for --- all the free variables in `flattenPred p`. -genFromPreds :: forall m. MonadGenError m => Env -> Pred -> GenT m Env --- TODO: remove this once optimisePred does a proper fixpoint computation -genFromPreds env0 (optimisePred . optimisePred -> preds) = - {- explain1 (show $ "genFromPreds fails\nPreds are:" /> pretty preds) -} do - -- NOTE: this is just lazy enough that the work of flattening, - -- computing dependencies, and linearizing is memoized in - -- properties that use `genFromPreds`. - plan <- runGE $ prepareLinearization preds - go env0 plan - where - go :: Env -> SolverPlan -> GenT m Env - go env plan | isEmptyPlan plan = pure env - go env plan = explain (show $ "Stepping the plan:" /> vsep [pretty env, pretty (substPlan env plan)]) $ do - (env', plan') <- stepPlan env plan - go env' plan' - --- ============================================================= --- Simplifcation --- ============================================================= - -simplifySpec :: HasSpec a => Spec a -> Spec a -simplifySpec spec = case applyNameHints spec of - SuspendedSpec x p -> - let optP = optimisePred p - in fromGESpec $ - explain - ("\nWhile calling simplifySpec on var " ++ show x ++ "\noptP=\n" ++ show optP ++ "\n") - (computeSpecSimplified x optP) - MemberSpec xs -> MemberSpec xs - ErrorSpec es -> ErrorSpec es - TypeSpec ts cant -> TypeSpec ts cant - TrueSpec -> TrueSpec - --- | Turn 'GenError' into 'ErrorSpec', and FatalError into 'error' -fromGESpec :: HasCallStack => GE (Spec a) -> Spec a -fromGESpec ge = case ge of - Result s -> s - GenError xs -> ErrorSpec (catMessageList xs) - FatalError es -> error $ catMessages es - -------- Stages of simplifying ------------------------------- - --- TODO: it might be necessary to run aggressiveInlining again after the let floating etc. -optimisePred :: Pred -> Pred -optimisePred p = - simplifyPred - . letSubexpressionElimination - . letFloating - . aggressiveInlining - . simplifyPred - $ p - -aggressiveInlining :: Pred -> Pred -aggressiveInlining pred0 - | inlined = aggressiveInlining pInlined - | otherwise = pred0 - where - (pInlined, Any inlined) = runWriter $ go (freeVars pred0) [] pred0 - - underBinder fvs x p = fvs `without` [Name x] <> singleton (Name x) (countOf (Name x) p) - - underBinderSub sub x = - [ x' := t - | x' := t <- sub - , isNothing $ eqVar x x' - ] - - -- NOTE: this is safe because we only use the `Subst` when it results in a literal so there - -- is no risk of variable capture. - goBinder :: FreeVars -> Subst -> Binder a -> Writer Any (Binder a) - goBinder fvs sub (x :-> p) = (x :->) <$> go (underBinder fvs x p) (underBinderSub sub x) p - - -- Check that the name `n` is only ever used as the only variable - -- in the expressions where it appears. This ensures that it doesn't - -- interact with anything. - onlyUsedUniquely n p = case p of - Assert t - | n `appearsIn` t -> Set.size (freeVarSet t) == 1 - | otherwise -> True - And ps -> all (onlyUsedUniquely n) ps - -- TODO: we can (and should) probably add a bunch of cases to this. - _ -> False - - go fvs sub pred2 = case pred2 of - ElemPred bool t xs - | not (isLit t) - , Lit a <- substituteAndSimplifyTerm sub t -> do - tell $ Any True - pure $ ElemPred bool (Lit a) xs - | otherwise -> pure $ ElemPred bool t xs - Subst x t p -> go fvs sub (substitutePred x t p) - ForAll set b - | not (isLit set) - , Lit a <- substituteAndSimplifyTerm sub set -> do - tell $ Any True - pure $ foldMap (`unBind` b) (forAllToList a) - | otherwise -> ForAll set <$> goBinder fvs sub b - Case t as bs - | not (isLit t) - , Lit a <- substituteAndSimplifyTerm sub t -> do - tell $ Any True - pure $ runCaseOn a as bs $ \x v p -> substPred (Env.singleton x v) p - | otherwise -> Case t <$> (goBinder fvs sub as) <*> (goBinder fvs sub bs) - Let t (x :-> p) - | all (\n -> count n fvs <= 1) (freeVarSet t) -> do - tell $ Any True - pure $ substitutePred x t p - | onlyUsedUniquely (Name x) p -> do - tell $ Any True - pure $ substitutePred x t p - | not $ Name x `appearsIn` p -> do - tell $ Any True - pure p - | not (isLit t) - , Lit a <- substituteAndSimplifyTerm sub t -> do - tell $ Any True - pure $ unBind a (x :-> p) - | otherwise -> Let t . (x :->) <$> go (underBinder fvs x p) (x := t : sub) p - Exists k b -> Exists k <$> goBinder fvs sub b - And ps -> Foldable.fold <$> mapM (go fvs sub) ps - Assert t - | not (isLit t) - , Lit b <- substituteAndSimplifyTerm sub t -> do - tell $ Any True - pure $ toPred b - | otherwise -> pure pred2 - DependsOn t t' - | not (isLit t) - , Lit {} <- substituteAndSimplifyTerm sub t -> do - tell $ Any True - pure $ TruePred - | not (isLit t') - , Lit {} <- substituteAndSimplifyTerm sub t' -> do - tell $ Any True - pure $ TruePred - | otherwise -> pure pred2 - TruePred -> pure pred2 - FalsePred {} -> pure pred2 - --- ================================================================================== - --- | Lifts 'propagateSpec' to take a Monadic 'Ctx' -propagateSpecM :: - forall v a m. - (Monad m, HasSpec v) => - Spec a -> - m (Ctx v a) -> - m (Spec v) -propagateSpecM spec ctxM = do ctx <- ctxM; pure $ propagateSpec ctx spec - --- | Precondition: the `Pred` defines the `Var a` --- Runs in `GE` in order for us to have detailed context on failure. -computeSpecSimplified :: - forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a) -computeSpecSimplified x pred3 = localGESpec $ case simplifyPred pred3 of - And ps -> do - spec <- fold <$> mapM (computeSpecSimplified x) ps - case spec of - SuspendedSpec y ps' -> pure $ SuspendedSpec y $ simplifyPred ps' - s -> pure s - ElemPred True t xs -> propagateSpecM (MemberSpec xs) (toCtx x t) - ElemPred False (t :: Term b) xs -> propagateSpecM (TypeSpec @b (anySpec @b) (NE.toList xs)) (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 - Let t b -> pure $ SuspendedSpec x (Let t b) - Exists k b -> pure $ SuspendedSpec x (Exists k b) - Assert (Lit True) -> pure mempty - Assert (Lit False) -> genError (show pred3) - Assert t -> propagateSpecM (equalSpec True) (toCtx x t) - ForAll (Lit s) b -> fold <$> mapM (\val -> computeSpec x $ unBind val b) (forAllToList s) - ForAll t b -> do - bSpec <- computeSpecBinderSimplified b - propagateSpecM (fromForAllSpec bSpec) (toCtx x t) - Case (Lit val) as bs -> runCaseOn val as bs $ \va vaVal psa -> computeSpec x (substPred (Env.singleton va vaVal) psa) - Case t as bs -> do - simpAs <- computeSpecBinderSimplified as - simpBs <- computeSpecBinderSimplified bs - propagateSpecM (typeSpec (SumSpec simpAs simpBs)) (toCtx x t) - -- Impossible cases that should be ruled out by the dependency analysis and linearizer - DependsOn {} -> - fatalErrorNE $ - NE.fromList - [ "The impossible happened in computeSpec: DependsOn" - , " " ++ show x - , show $ indent 2 (pretty pred3) - ] - where - -- We want `genError` to turn into `ErrorSpec` and we want `FatalError` to turn into `FatalError` - localGESpec ge = case ge of - (GenError xs) -> Result $ ErrorSpec (catMessageList xs) - (FatalError es) -> FatalError es - (Result v) -> Result v - --- | Precondition: the `Pred fn` defines the `Var a`. --- Runs in `GE` in order for us to have detailed context on failure. -computeSpec :: - forall a. (HasSpec a, HasCallStack) => Var a -> Pred -> GE (Spec a) -computeSpec x p = computeSpecSimplified x (simplifyPred p) - -computeSpecBinder :: Binder a -> GE (Spec a) -computeSpecBinder (x :-> p) = computeSpec x p - -computeSpecBinderSimplified :: Binder a -> GE (Spec a) -computeSpecBinderSimplified (x :-> p) = computeSpecSimplified x p - --- ---------------------- Building a plan ----------------------------------- - -substStage :: Env -> SolverStage -> SolverStage -substStage env (SolverStage y ps spec) = normalizeSolverStage $ SolverStage y (substPred env <$> ps) spec - -normalizeSolverStage :: SolverStage -> SolverStage -normalizeSolverStage (SolverStage x ps spec) = SolverStage x ps'' (spec <> spec') - where - (ps', ps'') = partition ((1 ==) . Set.size . freeVarSet) ps - spec' = fromGESpec $ computeSpec x (And ps') - -type Hints = DependGraph - -type DependGraph = Graph.Graph Name - -dependency :: HasVariables t => Name -> t -> DependGraph -dependency x (freeVarSet -> xs) = Graph.dependency x xs - -irreflexiveDependencyOn :: - forall t t'. (HasVariables t, HasVariables t') => t -> t' -> DependGraph -irreflexiveDependencyOn (freeVarSet -> xs) (freeVarSet -> ys) = Graph.irreflexiveDependencyOn xs ys - -noDependencies :: HasVariables t => t -> DependGraph -noDependencies (freeVarSet -> xs) = Graph.noDependencies xs - -respecting :: Hints -> DependGraph -> DependGraph -respecting hints g = g `Graph.subtractGraph` Graph.opGraph hints - -solvableFrom :: Name -> Set Name -> DependGraph -> Bool -solvableFrom x s g = - let less = Graph.dependencies x g - in s `Set.isSubsetOf` less && not (x `Set.member` less) - --- TODO: here we can compute both the explicit hints (i.e. constraints that --- define the order of two variables) and any whole-program smarts. -computeHints :: [Pred] -> Hints -computeHints ps = - Graph.transitiveClosure $ fold [x `irreflexiveDependencyOn` y | DependsOn x y <- ps] - -saturatePred :: Pred -> [Pred] -saturatePred p = [p] - --- | Linearize a predicate, turning it into a list of variables to solve and --- their defining constraints such that each variable can be solved independently. -prepareLinearization :: Pred -> GE SolverPlan -prepareLinearization p = do - let preds = concatMap saturatePred $ flattenPred p - hints = computeHints preds - graph = Graph.transitiveClosure $ hints <> respecting hints (foldMap computeDependencies preds) - plan <- - explainNE - ( NE.fromList - [ "Linearizing" - , show $ " preds: " <> pretty preds - , show $ " graph: " <> pretty graph - ] - ) - $ linearize preds graph - pure $ backPropagation $ SolverPlan plan graph - --- | Flatten nested `Let`, `Exists`, and `And` in a `Pred fn`. `Let` and --- `Exists` bound variables become free in the result. -flattenPred :: Pred -> [Pred] -flattenPred pIn = go (freeVarNames pIn) [pIn] - where - go _ [] = [] - go fvs (p : ps) = case p of - And ps' -> go fvs (ps' ++ ps) - -- NOTE: the order of the arguments to `==.` here are important. - -- The whole point of `Let` is that it allows us to solve all of `t` - -- before we solve the variables in `t`. - Let t b -> goBinder fvs b ps (\x -> (Assert (t ==. (V x)) :)) - Exists _ b -> goBinder fvs b ps (const id) - _ -> p : go fvs ps - - goBinder :: - Set Int -> - Binder a -> - [Pred] -> - (HasSpec a => Var a -> [Pred] -> [Pred]) -> - [Pred] - goBinder fvs (x :-> p) ps k = k x' $ go (Set.insert (nameOf x') fvs) (p' : ps) - where - (x', p') = freshen x p fvs - --- Consider: A + B = C + D --- We want to fail if A and B are independent. --- Consider: A + B = A + C, A <- B --- Here we want to consider this constraint defining for A -linearize :: - MonadGenError m => [Pred] -> DependGraph -> m [SolverStage] -linearize preds graph = do - sorted <- case Graph.topsort graph of - Left cycleX -> - fatalError - ( show $ - "linearize: Dependency cycle in graph:" - /> vsep' - [ "cycle:" /> pretty cycleX - , "graph:" /> pretty graph - ] - ) - Right sorted -> pure sorted - go sorted [(freeVarSet ps, ps) | ps <- filter isRelevantPred preds] - where - isRelevantPred TruePred = False - isRelevantPred DependsOn {} = False - isRelevantPred (Assert (Lit True)) = False - isRelevantPred _ = True - - go [] [] = pure [] - go [] ps - | null $ foldMap fst ps = - case checkPredsE (pure "Linearizing fails") mempty (map snd ps) of - Nothing -> pure [] - Just msgs -> genErrorNE msgs - | otherwise = - fatalErrorNE $ - NE.fromList - [ "Dependency error in `linearize`: " - , show $ indent 2 $ "graph: " /> pretty graph - , show $ - indent 2 $ - "the following left-over constraints are not defining constraints for a unique variable:" - /> vsep' (map (pretty . snd) ps) - ] - go (n@(Name x) : ns) ps = do - let (nps, ops) = partition (isLastVariable n . fst) ps - (normalizeSolverStage (SolverStage x (map snd nps) mempty) :) <$> go ns ops - - isLastVariable n set = n `Set.member` set && solvableFrom n (Set.delete n set) graph - --- ================================= --- Operations on Stages and Plans - --- | Does nothing if the variable is not in the plan already. -mergeSolverStage :: SolverStage -> [SolverStage] -> [SolverStage] -mergeSolverStage (SolverStage x ps spec) plan = - [ case eqVar x y of - Just Refl -> - SolverStage - y - (ps ++ ps') - ( addToErrorSpec - ( NE.fromList - ( [ "Solving var " ++ show x ++ " fails." - , "Merging the Specs" - , " 1. " ++ show spec - , " 2. " ++ show spec' - ] - ) - ) - (spec <> spec') - ) - Nothing -> stage - | stage@(SolverStage y ps' spec') <- plan - ] - -prettyPlan :: HasSpec a => Spec a -> Doc ann -prettyPlan (simplifySpec -> spec) - | SuspendedSpec _ p <- spec - , Result plan <- prepareLinearization p = - vsep' - [ "Simplified spec:" /> pretty spec - , pretty plan - ] - | otherwise = "Simplfied spec:" /> pretty spec - -printPlan :: HasSpec a => Spec a -> IO () -printPlan = print . prettyPlan - -isEmptyPlan :: SolverPlan -> Bool -isEmptyPlan (SolverPlan plan _) = null plan - -stepPlan :: MonadGenError m => Env -> SolverPlan -> GenT m (Env, SolverPlan) -stepPlan env plan@(SolverPlan [] _) = pure (env, plan) -stepPlan env p@(SolverPlan (SolverStage x ps spec : pl) gr) = do - (spec', specs) <- runGE - $ explain - (show (pretty env) ++ "\nStep " ++ show x ++ show (pretty p)) - $ do - ispecs <- mapM (computeSpec x) ps - pure $ (fold ispecs, ispecs) - val <- - genFromSpecT - ( addToErrorSpec - ( NE.fromList - ( ( "\nStepPlan for variable: " - ++ show x - ++ " fails to produce Specification, probably overconstrained." - ++ "PS = " - ++ unlines (map show ps) - ) - : ("Original spec " ++ show spec) - : "Predicates" - : zipWith - (\pred1 specx -> " pred " ++ show pred1 ++ " -> " ++ show specx) - ps - specs - ) - ) - (spec <> spec') - ) - let env1 = Env.extend x val env - pure (env1, backPropagation $ SolverPlan (substStage env1 <$> pl) (Graph.deleteNode (Name x) gr)) - -computeDependencies :: Pred -> DependGraph -computeDependencies = \case - ElemPred _bool term _xs -> computeTermDependencies term - Subst x t p -> computeDependencies (substitutePred x t p) - Assert t -> computeTermDependencies t - ForAll set b -> - let innerG = computeBinderDependencies b - in innerG <> set `irreflexiveDependencyOn` Graph.nodes innerG - DependsOn x y -> x `irreflexiveDependencyOn` y - Case t as bs -> noDependencies t <> computeBinderDependencies as <> computeBinderDependencies bs - TruePred -> mempty - FalsePred {} -> mempty - And ps -> foldMap computeDependencies ps - Exists _ b -> computeBinderDependencies b - Let t b -> noDependencies t <> computeBinderDependencies b - -computeBinderDependencies :: Binder a -> DependGraph -computeBinderDependencies (x :-> p) = - Graph.deleteNode (Name x) $ computeDependencies p - -computeTermDependencies :: Term a -> DependGraph -computeTermDependencies = fst . computeTermDependencies' - -computeTermDependencies' :: Term a -> (DependGraph, Set Name) -computeTermDependencies' = \case - (App _ args) -> go args - Lit {} -> (mempty, mempty) - (V x) -> (noDependencies (Name x), Set.singleton (Name x)) - where - go :: List Term as -> (DependGraph, Set Name) - go Nil = (mempty, mempty) - go (t :> ts) = - let (gr, ngr) = go ts - (tgr, ntgr) = computeTermDependencies' t - in (ntgr `irreflexiveDependencyOn` ngr <> tgr <> gr, ngr <> ntgr) - --- | Push as much information we can backwards through the plan. -backPropagation :: SolverPlan -> SolverPlan --- backPropagation (SolverPlan _plan _graph) = -backPropagation (SolverPlan initplan graph) = SolverPlan (go [] (reverse initplan)) graph - where - go acc [] = acc - go acc (s@(SolverStage (x :: Var a) ps spec) : plan) = go (s : acc) plan' - where - newStages = concatMap (newStage spec) ps - plan' = foldr mergeSolverStage plan newStages - -- Note use of the Term Pattern Equal - newStage specl (Assert (Equal (V x') t)) = - termVarEqCases specl x' t - newStage specr (Assert (Equal t (V x'))) = - termVarEqCases specr x' t - newStage _ _ = [] - - termVarEqCases :: HasSpec b => Spec a -> Var b -> Term b -> [SolverStage] - termVarEqCases (MemberSpec vs) x' t - | Set.singleton (Name x) == freeVarSet t = - [SolverStage x' [] $ MemberSpec (NE.nub (fmap (\v -> errorGE $ runTerm (Env.singleton x v) t) vs))] - termVarEqCases specx x' t - | Just Refl <- eqVar x x' - , [Name y] <- Set.toList $ freeVarSet t - , Result ctx <- toCtx y t = - [SolverStage y [] (propagateSpec ctx specx)] - termVarEqCases _ _ _ = [] - -spec9 :: Spec (Set Integer) -spec9 = constrained $ \x -> Assert $ (size_ x +. Lit 3) <=. Lit 12 diff --git a/testlib/Test/Minimal/Syntax.hs b/testlib/Test/Minimal/Syntax.hs deleted file mode 100644 index d76433e..0000000 --- a/testlib/Test/Minimal/Syntax.hs +++ /dev/null @@ -1,1023 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE ImportQualifiedPost #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PatternSynonyms #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE ViewPatterns #-} --- Monoid Pred and Spec, Pretty and ReName instances -{-# OPTIONS_GHC -Wno-orphans #-} - --- Syntactic operations on types: Term, Pred, Spec, Ctx, etc. -module Test.Minimal.Syntax where - -import Constrained.Core ( - Evidence (..), - Rename (rename), - Value (..), - Var (..), - eqVar, - freshen, - unValue, - ) -import Constrained.Env (Env) -import Constrained.Env qualified as Env -import Constrained.GenT -import Constrained.Graph -import Constrained.List hiding (ListCtx) -import Control.Monad.Identity -import Control.Monad.Writer (Writer, runWriter, tell) -import Data.Foldable qualified as Foldable (fold, toList) -import Data.Kind -import Data.List (intersect, nub) -import Data.List.NonEmpty (NonEmpty (..)) -import Data.List.NonEmpty qualified as NE -import Data.Map.Strict (Map) -import Data.Map.Strict qualified as Map -import Data.Maybe (catMaybes, fromMaybe, isJust, isNothing, listToMaybe) -import Data.Monoid qualified as Monoid -import Data.Semigroup (Any (..), sconcat) -import Data.Set (Set) -import Data.Set qualified as Set -import Data.String (fromString) -import Data.Typeable -import Prettyprinter -import Test.Minimal.Base - --- ======================================= --- Tools for building Spec - -forAll :: (Container t a, HasSpec t, HasSpec a) => Term t -> (Term a -> Pred) -> Pred -forAll tm = mkForAll tm . bind - --- forSome :: (Container t a, HasSpec t, HasSpec a) => Term t -> (Term a -> Pred) -> Pred --- forSome tm = mkForSome tm . bind - -mkForAll :: - (Container t a, HasSpec t, HasSpec a) => - Term t -> Binder a -> Pred -mkForAll (Lit (forAllToList -> [])) _ = TruePred -mkForAll _ (_ :-> TruePred) = TruePred -mkForAll tm binder = ForAll tm binder - -exists :: - forall a. - HasSpec a => - ((forall b. Term b -> b) -> GE a) -> - (Term a -> Pred) -> - Pred -exists sem k = - Exists sem $ bind k - -unsafeExists :: - forall a. - HasSpec a => - (Term a -> Pred) -> - Pred -unsafeExists = exists (\_ -> fatalError "unsafeExists") - -notMemberSpec :: forall a f. (HasSpec a, Foldable f) => f a -> Spec a -notMemberSpec x = TypeSpec (anySpec @a) (Foldable.toList x) - -isErrorLike :: forall a. Spec a -> Bool -isErrorLike spec = isJust (hasError spec) - -hasError :: forall a. Spec a -> Maybe (NonEmpty String) -hasError (ErrorSpec ss) = Just ss -hasError (TypeSpec x _) = - case guardTypeSpec @a x of - ErrorSpec ss -> Just ss - _ -> Nothing -hasError _ = Nothing - --- | Given two 'Spec', return an 'ErrorSpec' if one or more is an 'ErrorSpec' --- If neither is an 'ErrorSpec' apply the continuation 'f' -handleErrors :: Spec a -> Spec b -> (Spec a -> Spec b -> Spec c) -> Spec c -handleErrors spec1 spec2 f = case (hasError spec1, hasError spec2) of - (Just m1, Just m2) -> ErrorSpec (m1 <> m2) - (Just m1, _) -> ErrorSpec m1 - (_, Just m2) -> ErrorSpec m2 - (Nothing, Nothing) -> f spec1 spec2 - --- ========================================================= --- Conformance of Pred and Spec - --- | Add the explanations, if it's an ErrorSpec, else drop them -addToErrorSpec :: NE.NonEmpty String -> Spec a -> Spec a -addToErrorSpec es (ErrorSpec es') = ErrorSpec (es <> es') -addToErrorSpec _ s = s - --- | return a MemberSpec or ans ErrorSpec depending on if 'xs' the null list or not -memberSpec :: [a] -> NE.NonEmpty String -> Spec a -memberSpec xs messages = - case NE.nonEmpty xs of - Nothing -> ErrorSpec messages - Just ys -> MemberSpec ys - -satisfies :: forall a. HasSpec a => Term a -> Spec a -> Pred -satisfies _ TrueSpec = TruePred -satisfies e (MemberSpec nonempty) = ElemPred True e nonempty -satisfies t (SuspendedSpec x p) = Subst x t p -satisfies e (TypeSpec s cant) = case cant of - [] -> toPreds e s - (c : cs) -> ElemPred False e (c :| cs) <> toPreds e s -satisfies _ (ErrorSpec e) = FalsePred e - -runTermE :: forall a. Env -> Term a -> Either (NE.NonEmpty String) a -runTermE env = \case - Lit a -> Right a - V v -> case Env.lookup env v of - Just a -> Right a - Nothing -> Left (pure ("Couldn't find " ++ show v ++ " in " ++ show env)) - App f (ts :: List Term dom) -> do - vs <- mapMList (fmap Identity . runTermE env) ts - pure $ uncurryList_ runIdentity (semantics f) vs - -runTerm :: MonadGenError m => Env -> Term a -> m a -runTerm env x = case runTermE env x of - Left msgs -> fatalErrorNE msgs - Right val -> pure val - -conformsToSpec :: forall a. HasSpec a => a -> Spec a -> Bool -conformsToSpec _ TrueSpec = True -conformsToSpec a (MemberSpec as) = elem a as -conformsToSpec a (TypeSpec s cant) = notElem a cant && conformsTo a s -conformsToSpec a (SuspendedSpec v ps) = case checkPredE (Env.singleton v a) (pure "checkPredE") ps of - Nothing -> True - Just _ -> False -conformsToSpec _ (ErrorSpec _) = False - -checkPredE :: Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String) -checkPredE env msgs = \case - p@(ElemPred bool t xs) -> - case runTermE env t of - Left message -> Just (msgs <> message) - Right v -> case (elem v xs, bool) of - (True, True) -> Nothing - (True, False) -> Just ("notElemPred reduces to True" :| [show p]) - (False, True) -> Just ("elemPred reduces to False" :| [show p]) - (False, False) -> Nothing - Subst x t p -> checkPredE env msgs $ substitutePred x t p - Assert t -> case runTermE env t of - Right True -> Nothing - Right False -> - Just - (msgs <> pure ("Assert " ++ show t ++ " returns False") <> pure ("\nenv=\n" ++ show (pretty env))) - Left es -> Just (msgs <> es) - ForAll t (x :-> p) -> case runTermE env t of - Left es -> Just $ (msgs <> NE.fromList ["checkPredE: ForAll fails to run."] <> es) - Right set -> - let answers = - catMaybes - [ checkPredE env' (pure "Some items in ForAll fail") p - | v <- forAllToList set - , let env' = Env.extend x v env - ] - in case answers of - [] -> Nothing - (y : ys) -> Just (NE.nub (sconcat (y NE.:| ys))) - Case t a b -> case runTermE env t of - Right v -> runCaseOn v a b (\x val ps -> checkPredE (Env.extend x val env) msgs ps) - Left es -> Just (msgs <> pure "checkPredE: Case fails" <> es) - Let t (x :-> p) -> case runTermE env t of - Right val -> checkPredE (Env.extend x val env) msgs p - Left es -> Just (msgs <> pure "checkPredE: Let fails" <> es) - DependsOn {} -> Nothing - TruePred -> Nothing - FalsePred es -> Just (msgs <> pure "checkPredE: FalsePred" <> es) - And ps -> - case catMaybes (fmap (checkPredE env (pure "Some items in And fail")) ps) of - [] -> Nothing - (x : xs) -> Just (msgs <> NE.nub (sconcat (x NE.:| xs))) - Exists k (x :-> p) -> - let eval :: forall b. Term b -> b - eval term = case runTermE env term of - Right v -> v - Left es -> error $ unlines $ NE.toList (msgs <> es) - in case k eval of - Result a -> checkPredE (Env.extend x a env) msgs p - FatalError es -> Just (msgs <> catMessageList es) - GenError es -> Just (msgs <> catMessageList es) - -runCaseOn :: - Either a b -> Binder a -> Binder b -> (forall x. HasSpec x => Var x -> x -> Pred -> r) -> r -runCaseOn (Left a) (x :-> xps) (_ :-> _) f = f x a xps -runCaseOn (Right b) (_ :-> _) (y :-> yps) f = f y b yps - --- | Like checkPred, But it takes [Pred] rather than a single Pred, --- and it builds a much more involved explanation if it fails. --- Does the Pred evaluate to True under the given Env? --- If it doesn't, an involved explanation appears in the (Just message) --- If it does, then it returns Nothing -checkPredsE :: - NE.NonEmpty String -> - Env -> - [Pred] -> - Maybe (NE.NonEmpty String) -checkPredsE msgs env ps = - case catMaybes (fmap (checkPredE env msgs) ps) of - [] -> Nothing - (x : xs) -> Just (NE.nub (sconcat (x NE.:| xs))) - --- ========================================================== --- Semigroup and Monoid instances for Syntax Pred and Spec - -instance Semigroup Pred where - FalsePred xs <> FalsePred ys = FalsePred (xs <> ys) - FalsePred es <> _ = FalsePred es - _ <> FalsePred es = FalsePred es - TruePred <> p = p - p <> TruePred = p - p <> p' = And (unpackPred p ++ unpackPred p') - where - unpackPred (And ps) = ps - unpackPred x = [x] - -instance Monoid Pred where - mempty = TruePred - --- Spec instance - -instance HasSpec a => Semigroup (Spec a) where - TrueSpec <> s = s - s <> TrueSpec = s - ErrorSpec e <> ErrorSpec e' = - ErrorSpec - ( e - <> pure ("------ spec <> spec ------ @" ++ showType @a) - <> e' - ) - ErrorSpec e <> _ = ErrorSpec e - _ <> ErrorSpec e = ErrorSpec e - MemberSpec as <> MemberSpec as' = - addToErrorSpec - ( NE.fromList - ["Intersecting: ", " MemberSpec " ++ show (NE.toList as), " MemberSpec " ++ show (NE.toList as')] - ) - ( memberSpec - (nub $ intersect (NE.toList as) (NE.toList as')) - (pure "Empty intersection") - ) - ms@(MemberSpec as) <> ts@TypeSpec {} = - memberSpec - (nub $ NE.filter (`conformsToSpec` ts) as) - ( NE.fromList - [ "The two " ++ showType @a ++ " Specs are inconsistent." - , " " ++ show ms - , " " ++ show ts - ] - ) - TypeSpec s cant <> MemberSpec as = MemberSpec as <> TypeSpec s cant - SuspendedSpec v p <> SuspendedSpec v' p' = SuspendedSpec v (p <> rename v' v p') - SuspendedSpec v ps <> s = SuspendedSpec v (ps <> satisfies (V v) s) - s <> SuspendedSpec v ps = SuspendedSpec v (ps <> satisfies (V v) s) - TypeSpec s cant <> TypeSpec s' cant' = case combineSpec s s' of - -- NOTE: This might look like an unnecessary case, but doing - -- it like this avoids looping. - TypeSpec s'' cant'' -> TypeSpec s'' (cant <> cant' <> cant'') - s'' -> s'' <> notMemberSpec (cant <> cant') - -instance HasSpec a => Monoid (Spec a) where - mempty = TrueSpec - --- ================================================== --- Syntactic operation Renaming --- ================================================== - --- Name - -data Name where - Name :: HasSpec a => Var a -> Name - -deriving instance Show Name - -instance Eq Name where - Name v == Name v' = isJust $ eqVar v v' - --- Instances - -instance Pretty (Var a) where - pretty = fromString . show - -instance Pretty Name where - pretty (Name v) = pretty v - -instance Ord Name where - compare (Name v) (Name v') = compare (nameOf v, typeOf v) (nameOf v', typeOf v') - -instance Rename Name where - rename v v' (Name v'') = Name $ rename v v' v'' - -instance Rename (Term a) where - rename v v' - | v == v' = id - | otherwise = \case - Lit l -> Lit l - V v'' -> V (rename v v' v'') - App f a -> App f (rename v v' a) - -instance Rename Pred where - rename v v' - | v == v' = id - | otherwise = \case - ElemPred bool t xs -> ElemPred bool (rename v v' t) xs - Subst x t p -> rename v v' $ substitutePred x t p - And ps -> And (rename v v' ps) - Exists k b -> Exists (\eval -> k $ eval . rename v v') (rename v v' b) - Let t b -> Let (rename v v' t) (rename v v' b) - DependsOn x y -> DependsOn (rename v v' x) (rename v v' y) - Assert t -> Assert (rename v v' t) - ForAll set b -> ForAll (rename v v' set) (rename v v' b) - Case t a b -> Case (rename v v' t) (rename v v' a) (rename v v' b) - TruePred -> TruePred - FalsePred es -> FalsePred es - -instance Rename (Binder a) where - rename v v' (va :-> psa) = va' :-> rename v v' psa' - where - (va', psa') = freshen va psa (Set.fromList [nameOf v, nameOf v'] <> Set.delete (nameOf va) (freeVarNames psa)) - --- ============================================================ --- Syntactic operation: Free variables and variable names --- ============================================================ - -freeVarNames :: forall t. HasVariables t => t -> Set Int -freeVarNames = Set.mapMonotonic (\(Name v) -> nameOf v) . freeVarSet - -newtype FreeVars = FreeVars {unFreeVars :: Map Name Int} - deriving (Show) - -restrictedTo :: FreeVars -> Set Name -> FreeVars -restrictedTo (FreeVars m) nms = FreeVars $ Map.restrictKeys m nms - -memberOf :: Name -> FreeVars -> Bool -memberOf n (FreeVars m) = Map.member n m - -count :: Name -> FreeVars -> Int -count n (FreeVars m) = fromMaybe 0 $ Map.lookup n m - -instance Semigroup FreeVars where - FreeVars fv <> FreeVars fv' = FreeVars $ Map.unionWith (+) fv fv' - -instance Monoid FreeVars where - mempty = FreeVars mempty - -freeVar :: Name -> FreeVars -freeVar n = singleton n 1 - -singleton :: Name -> Int -> FreeVars -singleton n k = FreeVars $ Map.singleton n k - -without :: Foldable t => FreeVars -> t Name -> FreeVars -without (FreeVars m) remove = FreeVars $ foldr Map.delete m (Foldable.toList remove) - -class HasVariables a where - freeVars :: a -> FreeVars - freeVarSet :: a -> Set Name - freeVarSet = Map.keysSet . unFreeVars . freeVars - countOf :: Name -> a -> Int - countOf n = count n . freeVars - appearsIn :: Name -> a -> Bool - appearsIn n = (> 0) . count n . freeVars - -instance (HasVariables a, HasVariables b) => HasVariables (a, b) where - freeVars (a, b) = freeVars a <> freeVars b - freeVarSet (a, b) = freeVarSet a <> freeVarSet b - countOf n (a, b) = countOf n a + countOf n b - appearsIn n (a, b) = appearsIn n a || appearsIn n b - -instance HasVariables (List Term as) where - freeVars Nil = mempty - freeVars (x :> xs) = freeVars x <> freeVars xs - freeVarSet Nil = mempty - freeVarSet (x :> xs) = freeVarSet x <> freeVarSet xs - countOf _ Nil = 0 - countOf n (x :> xs) = countOf n x + countOf n xs - appearsIn _ Nil = False - appearsIn n (x :> xs) = appearsIn n x || appearsIn n xs - -instance HasVariables Name where - freeVars = freeVar - freeVarSet = Set.singleton - countOf n n' - | n == n' = 1 - | otherwise = 0 - appearsIn n n' = n == n' - -instance HasVariables (Term a) where - freeVars = \case - Lit {} -> mempty - V x -> freeVar (Name x) - App _ ts -> freeVars ts - freeVarSet = \case - Lit {} -> mempty - V x -> freeVarSet (Name x) - App _ ts -> freeVarSet ts - countOf n = \case - Lit {} -> 0 - V x -> countOf n (Name x) - App _ ts -> countOf n ts - appearsIn n = \case - Lit {} -> False - V x -> appearsIn n (Name x) - App _ ts -> appearsIn n ts - -instance HasVariables Pred where - freeVars = \case - ElemPred _ t _ -> freeVars t - -- GenHint _ t -> freeVars t - Subst x t p -> freeVars t <> freeVars p `without` [Name x] - And ps -> foldMap freeVars ps - Exists _ b -> freeVars b - Let t b -> freeVars t <> freeVars b - -- Exists _ b -> freeVars b - Assert t -> freeVars t - -- Reifies t' t _ -> freeVars t' <> freeVars t - DependsOn x y -> freeVars x <> freeVars y - ForAll set b -> freeVars set <> freeVars b - Case t as bs -> freeVars t <> freeVars as <> freeVars bs - -- When b p -> freeVars b <> freeVars p - TruePred -> mempty - FalsePred _ -> mempty - - -- Monitor {} -> mempty - -- Explain _ p -> freeVars p - freeVarSet = \case - ElemPred _ t _ -> freeVarSet t - -- GenHint _ t -> freeVarSet t - Subst x t p -> freeVarSet t <> Set.delete (Name x) (freeVarSet p) - And ps -> foldMap freeVarSet ps - Exists _ b -> freeVarSet b - Let t b -> freeVarSet t <> freeVarSet b - -- Exists _ b -> freeVarSet b - Assert t -> freeVarSet t - -- Reifies t' t _ -> freeVarSet t' <> freeVarSet t - DependsOn x y -> freeVarSet x <> freeVarSet y - ForAll set b -> freeVarSet set <> freeVarSet b - Case t a b -> freeVarSet t <> freeVarSet a <> freeVarSet b - -- When b p -> freeVarSet b <> freeVarSet p - -- Explain _ p -> freeVarSet p - TruePred -> mempty - FalsePred _ -> mempty - - -- Monitor {} -> mempty - countOf n = \case - ElemPred _ t _ -> countOf n t - -- GenHint _ t -> countOf n t - Subst x t p - | n == Name x -> countOf n t - | otherwise -> countOf n t + countOf n p - And ps -> sum $ map (countOf n) ps - Let t b -> countOf n t + countOf n b - Exists _ b -> countOf n b - Assert t -> countOf n t - -- Reifies t' t _ -> countOf n t' + countOf n t - DependsOn x y -> countOf n x + countOf n y - ForAll set b -> countOf n set + countOf n b - Case t a b -> countOf n t + countOf n a + countOf n b - -- When b p -> countOf n b + countOf n p - -- Explain _ p -> countOf n p - TruePred -> 0 - FalsePred _ -> 0 - - -- Monitor {} -> 0 - appearsIn n = \case - ElemPred _ t _ -> appearsIn n t - -- GenHint _ t -> appearsIn n t - Subst x t p - | n == Name x -> appearsIn n t - | otherwise -> appearsIn n t || appearsIn n p - And ps -> any (appearsIn n) ps - Let t b -> appearsIn n t || appearsIn n b - Exists _ b -> appearsIn n b - Assert t -> appearsIn n t - -- Reifies t' t _ -> appearsIn n t' || appearsIn n t - DependsOn x y -> appearsIn n x || appearsIn n y - ForAll set b -> appearsIn n set || appearsIn n b - Case t a b -> appearsIn n t || appearsIn n a || appearsIn n b - -- When b p -> appearsIn n b || appearsIn n p - -- Explain _ p -> appearsIn n p - TruePred -> False - FalsePred _ -> False - --- Monitor {} -> False - -instance HasVariables (Binder a) where - freeVars (x :-> p) = freeVars p `without` [Name x] - freeVarSet (x :-> p) = Set.delete (Name x) (freeVarSet p) - countOf n (x :-> p) - | Name x == n = 0 - | otherwise = countOf n p - appearsIn n (x :-> p) - | Name x == n = False - | otherwise = appearsIn n p - -instance {-# OVERLAPPABLE #-} (Foldable t, HasVariables a) => HasVariables (t a) where - freeVars = foldMap freeVars - freeVarSet = foldMap freeVarSet - countOf n = Monoid.getSum . foldMap (Monoid.Sum . countOf n) - appearsIn n = any (appearsIn n) - -instance HasVariables a => HasVariables (Set a) where - freeVars = foldMap freeVars - freeVarSet = foldMap freeVarSet - countOf n = sum . Set.map (countOf n) - appearsIn n = any (appearsIn n) - --- ========================================================= --- Helpers - -fromLits :: List Term as -> Maybe (List Value as) -fromLits = mapMList fromLit - -fromLit :: Term a -> Maybe (Value a) -fromLit (Lit l) = pure $ Value l --- fromLit (To x) = (Value . toSimpleRep . unValue) <$> fromLit x -- MAYBE we don't want to do this? --- fromLit (From x) = (Value . fromSimpleRep . unValue) <$> fromLit x -- Why not apply unary functions to Lit ? -fromLit _ = Nothing - -isLit :: Term a -> Bool -isLit = isJust . fromLit - --- ================================================================= --- Syntactic operations Substitutions --- ============================================================ - -type Subst = [SubstEntry] - -data SubstEntry where - (:=) :: HasSpec a => Var a -> Term a -> SubstEntry - -backwardsSubstitution :: forall a. HasSpec a => Subst -> Term a -> Term a -backwardsSubstitution sub0 t = - case findMatch sub0 t of - -- TODO: what about multiple matches?? - Just x -> V x - Nothing -> case t of - Lit a -> Lit a - V x -> V x - App f ts -> App f (mapListC @HasSpec (backwardsSubstitution sub0) ts) - where - findMatch :: Subst -> Term a -> Maybe (Var a) - findMatch [] _ = Nothing - findMatch (x := t' : sub1) t1 - | fastInequality t1 t' = findMatch sub1 t1 - | Just (x', t'') <- cast (x, t') - , t == t'' = - Just x' - | otherwise = findMatch sub1 t1 - --- | Sound but not complete inequality on terms -fastInequality :: Term a -> Term b -> Bool -fastInequality (V (Var i _)) (V (Var j _)) = i /= j -fastInequality Lit {} Lit {} = False -fastInequality (App _ as) (App _ bs) = go as bs - where - go :: List Term as -> List Term bs -> Bool - go Nil Nil = False - go (a :> as') (b :> bs') = fastInequality a b || go as' bs' - go _ _ = True -fastInequality _ _ = True - --- =================================================================== - -substituteTerm :: forall a. Subst -> Term a -> Term a -substituteTerm sub = \case - Lit a -> Lit a - V x -> substVar sub x - App f (mapList (substituteTerm sub) -> (ts :: List Term dom)) -> - case fromLits ts of - Just vs -> Lit (uncurryList_ unValue (semantics f) vs) - _ -> App f ts - where - substVar :: HasSpec a => Subst -> Var a -> Term a - substVar [] x = V x - substVar (y := t : sub1) x - | Just Refl <- eqVar x y = t - | otherwise = substVar sub1 x - -substituteTerm' :: forall a. Subst -> Term a -> Writer Any (Term a) -substituteTerm' sub = \case - Lit a -> pure $ Lit a - V x -> substVar sub x - App f ts -> - App f <$> mapMList (substituteTerm' sub) ts - where - substVar :: HasSpec a => Subst -> Var a -> Writer Any (Term a) - substVar [] x = pure $ V x - substVar (y := t : sub1) x - | Just Refl <- eqVar x y = t <$ tell (Any True) - | otherwise = substVar sub1 x - -substituteBinder :: HasSpec a => Var a -> Term a -> Binder b -> Binder b -substituteBinder x tm (y :-> p) = y' :-> substitutePred x tm p' - where - (y', p') = - freshen y p (Set.singleton (nameOf x) <> freeVarNames tm <> Set.delete (nameOf y) (freeVarNames p)) - -substitutePred :: HasSpec a => Var a -> Term a -> Pred -> Pred -substitutePred x tm = \case - ElemPred bool t xs -> ElemPred bool (substituteTerm [x := tm] t) xs - -- GenHint h t -> GenHint h (substituteTerm [x := tm] t) - Subst x' t p -> substitutePred x tm $ substitutePred x' t p - Assert t -> Assert (substituteTerm [x := tm] t) - And ps -> Foldable.fold (substitutePred x tm <$> ps) - Exists k b -> Exists (\eval -> k (eval . substituteTerm [x := tm])) (substituteBinder x tm b) - Let t b -> Let (substituteTerm [x := tm] t) (substituteBinder x tm b) - ForAll t b -> ForAll (substituteTerm [x := tm] t) (substituteBinder x tm b) - Case t as bs -> Case (substituteTerm [x := tm] t) (substituteBinder x tm as) (substituteBinder x tm bs) - -- When b p -> When (substituteTerm [x := tm] b) (substitutePred x tm p) - -- Reifies t' t f -> Reifies (substituteTerm [x := tm] t') (substituteTerm [x := tm] t) f - DependsOn t t' -> DependsOn (substituteTerm [x := tm] t) (substituteTerm [x := tm] t') - TruePred -> TruePred - FalsePred es -> FalsePred es - --- Monitor m -> Monitor (\eval -> m (eval . substituteTerm [x := tm])) --- Explain es p -> Explain es $ substitutePred x tm p - --- ===================================================== --- Substituion under an Env, rather than a single Var --- It takes Values in the Env, and makes them Literals in the Term. - -substTerm :: Env -> Term a -> Term a -substTerm env = \case - Lit a -> Lit a - V v - | Just a <- Env.lookup env v -> Lit a - | otherwise -> V v - App f (mapList (substTerm env) -> ts) -> - case fromLits ts of - Just vs -> Lit (uncurryList_ unValue (semantics f) vs) - _ -> App f ts - -substBinder :: Env -> Binder a -> Binder a -substBinder env (x :-> p) = x :-> substPred (Env.remove x env) p - -substPred :: Env -> Pred -> Pred -substPred env = \case - ElemPred bool t xs -> ElemPred bool (substTerm env t) xs - -- GenHint h t -> GenHint h (substTerm env t) - Subst x t p -> substPred env $ substitutePred x t p - Assert t -> Assert (substTerm env t) - -- Reifies t' t f -> Reifies (substTerm env t') (substTerm env t) f - ForAll set b -> ForAll (substTerm env set) (substBinder env b) - Case t as bs -> Case (substTerm env t) (substBinder env as) (substBinder env bs) - -- When b p -> When (substTerm env b) (substPred env p) - DependsOn x y -> DependsOn (substTerm env x) (substTerm env y) - TruePred -> TruePred - FalsePred es -> FalsePred es - And ps -> Foldable.fold (substPred env <$> ps) - Exists k b -> Exists (\eval -> k $ eval . substTerm env) (substBinder env b) - Let t b -> Let (substTerm env t) (substBinder env b) - -substSpec :: Env -> Spec a -> Spec a -substSpec env (SuspendedSpec v p) = SuspendedSpec v (substPred env p) -substSpec _ spec = spec - -substSolverStage :: Env -> SolverStage -> SolverStage -substSolverStage env (SolverStage var preds spec) = SolverStage var (map (substPred env) preds) (substSpec env spec) - -substPlan :: Env -> SolverPlan -> SolverPlan -substPlan env (SolverPlan stages deps) = SolverPlan (map (substSolverStage env) stages) deps - --- Monitor m -> Monitor m --- Explain es p -> Explain es $ substPred env p - -unBind :: a -> Binder a -> Pred -unBind a (x :-> p) = substPred (Env.singleton x a) p - --- ================================================== --- Syntactic operation Regularizing --- ================================================== - -liftNameHintToBinder :: HasVariables t => Var a -> t -> Var a -liftNameHintToBinder v t = - case [nameHint v' | Name v' <- Set.toList $ freeVarSet t, nameOf v' == nameOf v, nameHint v' /= "v"] of - [] -> v - nh : _ -> v {nameHint = nh} - -liftNameHintToBinderBinder :: Binder a -> Binder a -liftNameHintToBinderBinder (x :-> p) = x' :-> substitutePred x (V x') (applyNameHintsPred p) - where - x' = liftNameHintToBinder x p - -applyNameHintsPred :: Pred -> Pred -applyNameHintsPred pred0 = case pred0 of - ElemPred {} -> pred0 - And ps -> And $ map applyNameHintsPred ps - Exists k b -> Exists k (liftNameHintToBinderBinder b) - Subst v t p -> applyNameHintsPred (substitutePred v t p) - Let t b -> Let t (liftNameHintToBinderBinder b) - Assert {} -> pred0 - ForAll t b -> ForAll t (liftNameHintToBinderBinder b) - Case t as bs -> Case t (liftNameHintToBinderBinder as) (liftNameHintToBinderBinder bs) - TruePred {} -> pred0 - FalsePred {} -> pred0 - DependsOn {} -> pred0 - --- Explain es p' -> Explain es (applyNameHintsPred p') - -applyNameHints :: Spec a -> Spec a -applyNameHints (SuspendedSpec x p) = SuspendedSpec x' p' - where - x' :-> p' = liftNameHintToBinderBinder (x :-> p) -applyNameHints spec = spec - --- ====================================================== --- Simplify - --- | Apply a substitution and simplify the resulting term if the --- substitution changed the term. -substituteAndSimplifyTerm :: Subst -> Term a -> Term a -substituteAndSimplifyTerm sub t = - case runWriter $ substituteTerm' sub t of - (t', Any b) - | b -> simplifyTerm t' - | otherwise -> t' - --- | Simplify a Term, if the Term is an 'App', apply the rewrite rules --- chosen by the (Semantics t) instance attached to the App --- to the function witness 'f' -simplifyTerm :: forall a. Term a -> Term a -simplifyTerm = \case - V v -> V v - Lit l -> Lit l - App (f :: t bs a) (mapList simplifyTerm -> ts) - | Just vs <- fromLits ts -> Lit $ uncurryList_ unValue (semantics f) vs - | Just t <- rewriteRules f ts (Evidence @(Typeable a, Eq a, Show a)) -> simplifyTerm t - | otherwise -> App f ts - -simplifyPred :: Pred -> Pred -simplifyPred = \case - -- If the term simplifies away to a literal, that means there is no - -- more generation to do so we can get rid of `GenHint` - p@(ElemPred bool t xs) -> case simplifyTerm t of - Lit x -> case (elem x xs, bool) of - (True, True) -> TruePred - (True, False) -> FalsePred ("notElemPred reduces to True" :| [show p]) - (False, True) -> FalsePred ("elemPred reduces to False" :| [show p]) - (False, False) -> TruePred - t' -> ElemPred bool t' xs - Subst x t p -> simplifyPred $ substitutePred x t p - Assert t -> Assert $ simplifyTerm t - ForAll (ts :: Term t) (b :: Binder a) -> case simplifyTerm ts of - Lit as -> foldMap (`unBind` b) (forAllToList as) - set' -> case simplifyBinder b of - (_ :-> TruePred) -> TruePred - b' -> ForAll set' b' - Case t as@(_ :-> _) bs@(_ :-> _) -> mkCase (simplifyTerm t) (simplifyBinder as) (simplifyBinder bs) - TruePred -> TruePred - FalsePred es -> FalsePred es - And ps -> Foldable.fold (simplifyPreds ps) - Let t b -> case simplifyTerm t of - t'@App {} -> Let t' (simplifyBinder b) - -- Variable or literal - t' | x :-> p <- b -> simplifyPred $ substitutePred x t' p - Exists k b -> case simplifyBinder b of - _ :-> TruePred -> TruePred - -- This is to get rid of exisentials like: - -- `constrained $ \ x -> exists $ \ y -> [x ==. y, y + 2 <. 10]` - x :-> p | Just t <- pinnedBy x p -> simplifyPred $ substitutePred x t p - b' -> Exists k b' - DependsOn _ Lit {} -> TruePred - DependsOn Lit {} _ -> TruePred - DependsOn x y -> DependsOn x y - -mkCase :: - HasSpec (Either a b) => Term (Either a b) -> Binder a -> Binder b -> Pred -mkCase tm as bs - -- TODO: all equal maybe? - | isTrueBinder as && isTrueBinder bs = TruePred - | isFalseBinder as && isFalseBinder bs = FalsePred (pure "mkCase on all False") - | Lit a <- tm = runCaseOn a as bs (\x val p -> substPred (Env.singleton x val) p) - | otherwise = Case tm as bs - where - isTrueBinder (_ :-> TruePred) = True - isTrueBinder (_ :-> _) = False - - isFalseBinder (_ :-> FalsePred {}) = True - isFalseBinder (_ :-> _) = False - -simplifyPreds :: [Pred] -> [Pred] -simplifyPreds = go [] . map simplifyPred - where - go acc [] = reverse acc - go _ (FalsePred err : _) = [FalsePred err] - go acc (TruePred : ps) = go acc ps - go acc (p : ps) = go (p : acc) ps - -simplifyBinder :: Binder a -> Binder a -simplifyBinder (x :-> p) = x :-> simplifyPred p - -toPred :: Bool -> Pred -toPred True = TruePred -toPred False = FalsePred (pure "toPred False") - --- ================================================================= - --- TODO: this can probably be cleaned up and generalized along with generalizing --- to make sure we float lets in some missing cases. -letFloating :: Pred -> Pred -letFloating = Foldable.fold . go [] - where - goBlock ctx ps = goBlock' (freeVarNames ctx <> freeVarNames ps) ctx ps - - goBlock' _ ctx [] = ctx - goBlock' fvs ctx (Let t (x :-> p) : ps) = - -- We can do `goBlock'` here because we've already done let floating - -- on the inner `p` - [Let t (x' :-> Foldable.fold (goBlock' (Set.insert (nameOf x') fvs) ctx (p' : ps)))] - where - (x', p') = freshen x p fvs - goBlock' fvs ctx (And ps : ps') = goBlock' fvs ctx (ps ++ ps') - goBlock' fvs ctx (p : ps) = goBlock' fvs (p : ctx) ps - - go ctx = \case - ElemPred bool t xs -> ElemPred bool t xs : ctx - And ps0 -> goBlock ctx (map letFloating ps0) - Exists k (x :-> p) -> goExists ctx (Exists k) x (letFloating p) - Let t (x :-> p) -> goBlock ctx [Let t (x :-> letFloating p)] - Subst x t p -> go ctx (substitutePred x t p) - ForAll t (x :-> p) -> ForAll t (x :-> letFloating p) : ctx - Case t (x :-> px) (y :-> py) -> Case t (x :-> letFloating px) (y :-> letFloating py) : ctx - Assert t -> Assert t : ctx - TruePred -> TruePred : ctx - FalsePred es -> FalsePred es : ctx - DependsOn t t' -> DependsOn t t' : ctx - - goExists :: HasSpec a => [Pred] -> (Binder a -> Pred) -> Var a -> Pred -> [Pred] - goExists ctx ex x (Let t (y :-> p)) - | not $ Name x `appearsIn` t = - let (y', p') = freshen y p (Set.insert (nameOf x) $ freeVarNames p <> freeVarNames t) - in go ctx (Let t (y' :-> ex (x :-> p'))) - goExists ctx ex x p = ex (x :-> p) : ctx - --- Common subexpression elimination but only on terms that are already let-bound. -letSubexpressionElimination :: HasSpec Bool => Pred -> Pred -letSubexpressionElimination = go [] - where - adjustSub x sub = - [ x' := t - | x' := t <- sub - , isNothing $ eqVar x x' - , -- TODO: possibly freshen the binder where - -- `x` appears instead? - not $ Name x `appearsIn` t - ] - - goBinder :: Subst -> Binder a -> Binder a - goBinder sub (x :-> p) = x :-> go (adjustSub x sub) p - - go sub = \case - ElemPred bool t xs -> ElemPred bool (backwardsSubstitution sub t) xs - And ps -> And (go sub <$> ps) - Exists k b -> Exists k (goBinder sub b) - Let t (x :-> p) -> Let t' (x :-> go (x := t' : sub') p) - where - t' = backwardsSubstitution sub t - sub' = adjustSub x sub - Subst x t p -> go sub (substitutePred x t p) - Assert t -> Assert (backwardsSubstitution sub t) - ForAll t b -> ForAll (backwardsSubstitution sub t) (goBinder sub b) - Case t as bs -> Case (backwardsSubstitution sub t) (goBinder sub as) (goBinder sub bs) - TruePred -> TruePred - FalsePred es -> FalsePred es - DependsOn t t' -> DependsOn (backwardsSubstitution sub t) (backwardsSubstitution sub t') - --- =============================================================================== --- Syntax for Solving : stages and plans --- =============================================================================== - -data SolverStage where - SolverStage :: - HasSpec a => - { stageVar :: Var a - , stagePreds :: [Pred] - , stageSpec :: Spec a - } -> - SolverStage - -instance Pretty SolverStage where - pretty SolverStage {..} = - (viaShow stageVar <+> "<-") - /> vsep' - ( [pretty stageSpec | not $ isTrueSpec stageSpec] - ++ (map pretty stagePreds) - ++ ["---"] - ) - -data SolverPlan = SolverPlan - { solverPlan :: [SolverStage] - , solverDependencies :: Graph Name - } - -instance Pretty SolverPlan where - pretty SolverPlan {..} = - "\nSolverPlan" - /> vsep' - [ -- "\nDependencies:" /> pretty solverDependencies, -- Might be usefull someday - "Linearization:" /> prettyLinear solverPlan - ] - -isTrueSpec :: Spec a -> Bool -isTrueSpec TrueSpec = True -isTrueSpec _ = False - -prettyLinear :: [SolverStage] -> Doc ann -prettyLinear = vsep' . map pretty - --- ========================================================== --- The equality function symbol (==.) - -data EqSym :: [Type] -> Type -> Type where - EqualW :: (Eq a, HasSpec a) => EqSym '[a, a] Bool - -deriving instance Eq (EqSym dom rng) - -instance Show (EqSym d r) where - show EqualW = "==." - -instance Syntax EqSym where - inFix EqualW = True - name EqualW = "==." - -instance Semantics EqSym where - semantics EqualW = (==) - - rewriteRules EqualW (t :> t' :> Nil) Evidence - | t == t' = Just $ Lit True - rewriteRules t@EqualW l Evidence = Lit <$> (applyFunSym @EqSym (semantics t) l) - --- We don't need a HasSpec instance, since we can make equality specs at any type --- using just MemberSpec and TypeSpec - -equalSpec :: a -> Spec a -equalSpec = MemberSpec . pure - -notEqualSpec :: forall a. HasSpec a => a -> Spec a -notEqualSpec n = TypeSpec (anySpec @a) [n] - -caseBoolSpec :: (HasSpec Bool, HasSpec a) => Spec Bool -> (Bool -> Spec a) -> Spec a -caseBoolSpec spec cont = case possibleValues spec of - [] -> ErrorSpec (NE.fromList ["No possible values in caseBoolSpec"]) - [b] -> cont b - _ -> mempty - where - possibleValues s = filter (flip conformsToSpec s) [True, False] - -instance Logic EqSym where - propagate tag ctx spec = case (tag, ctx, spec) of - (_, _, TrueSpec) -> TrueSpec - (_, _, ErrorSpec msgs) -> ErrorSpec msgs - (f, context, SuspendedSpec v ps) -> constrained $ \v' -> Let (App f (fromListCtx context v')) (v :-> ps) - (EqualW, HOLE :<| s, bspec) -> caseBoolSpec bspec $ \case - True -> equalSpec s - False -> notEqualSpec s - (EqualW, s :|> HOLE, bspec) -> caseBoolSpec bspec $ \case - True -> equalSpec s - False -> notEqualSpec s - -infix 4 ==. - -(==.) :: (HasSpec Bool, HasSpec a) => Term a -> Term a -> Term Bool -(==.) x y = App EqualW (x :> y :> Nil) - -getWitness :: forall t t' d r. (AppRequires t d r, Typeable t') => t d r -> Maybe (t' d r) -getWitness = cast - -pattern Equal :: - forall b. - () => - forall a. - (b ~ Bool, Eq a, HasSpec a) => - Term a -> - Term a -> - Term b -pattern Equal x y <- - ( App - (getWitness -> Just EqualW) - (x :> y :> Nil) - ) - --- | Is the variable x pinned to some free term in p? (free term --- meaning that all the variables in the term are free in p). --- --- TODO: complete this with more cases! -pinnedBy :: forall a. HasSpec a => Var a -> Pred -> Maybe (Term a) --- pinnedBy x (Assert (App (extractFn @EqFn @fn -> Just EqualW) (t :> t' :> Nil))) -pinnedBy x (Assert (Equal t t')) - | V x' <- t, Just Refl <- eqVar x x' = Just t' - | V x' <- t', Just Refl <- eqVar x x' = Just t -pinnedBy x (And ps) = listToMaybe $ catMaybes $ map (pinnedBy x) ps -pinnedBy _ _ = Nothing diff --git a/testlib/Test/Minimal/Tuple.hs b/testlib/Test/Minimal/Tuple.hs deleted file mode 100644 index b2e7bc6..0000000 --- a/testlib/Test/Minimal/Tuple.hs +++ /dev/null @@ -1,356 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE QuasiQuotes #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE ViewPatterns #-} --- HasSpec instances for known types such as (a,b,c), (a,b,c,d) i.e. tuples. -{-# OPTIONS_GHC -Wno-orphans #-} - -module Test.Minimal.Tuple where - -import Constrained.GenT -import Constrained.List hiding (ListCtx) -import Data.Kind -import qualified Data.List.NonEmpty as NE -import Data.Set (Set) -import Test.Minimal.Base -import Test.Minimal.Model -import Test.Minimal.Syntax - --- import Data.Coerce --- import Data.Typeable - --- ======================================================= --- Experiment to see if we can build tuples, using only the binary tuple --- as the base case. The only compilcated part is the `combineSpec` which --- uses `guardTypeSpec` to merge the simple sub cases on smaller tuples. - -instance (HasSpec a, HasSpec b, HasSpec c) => HasSpec (a, b, c) where - type TypeSpec (a, b, c) = (Spec a, Spec (b, c)) - - anySpec = (mempty @(Spec a), mempty @(Spec (b, c))) - - combineSpec (a, b) (a', b') = guardTypeSpec (a <> a', b <> b') - - conformsTo (a, b, c) (sa, sbc) = conformsToSpec a sa && conformsToSpec (b, c) sbc - - guardTypeSpec (a, bc) = - handleErrors - a - bc - ( \x y -> case (x :: Spec a, y :: Spec (b, c)) of - (MemberSpec xs, MemberSpec ys) -> - -- Given two MemberSpec, build one MemberSpec, by joining all combinations - MemberSpec - ( NE.fromList - [ (a', b', c') - | a' <- NE.toList xs - , (b', c') <- NE.toList ys - ] - ) - (specA, specBC) -> constrained $ \p -> And [satisfies (head3_ p) specA, satisfies (tail3_ p) specBC] - ) - - genFromTypeSpec (a, bc) = f <$> genFromSpecT a <*> genFromSpecT bc - where - f a' (b', c') = (a', b', c') - - toPreds x (a, bc) = satisfies (head3_ x) a <> satisfies (tail3_ x) bc - -head3_ :: All HasSpec '[a, b, c] => Term (a, b, c) -> Term a -head3_ x = App Head3W (x :> Nil) - -tail3_ :: All HasSpec '[a, b, c] => Term (a, b, c) -> Term (b, c) -tail3_ x = App Tail3W (x :> Nil) - --- ======================================================= - -instance (HasSpec a, HasSpec b, HasSpec c, HasSpec d) => HasSpec (a, b, c, d) where - type TypeSpec (a, b, c, d) = (Spec a, Spec (b, c, d)) - - anySpec = (mempty @(Spec a), mempty @(Spec (b, c, d))) - - combineSpec (a, bcd) (a', bcd') = guardTypeSpec (a <> a', bcd <> bcd') - - conformsTo (a, b, c, d) (sA, sBCD) = conformsToSpec a sA && conformsToSpec (b, c, d) sBCD - - guardTypeSpec (a, bcd) = - handleErrors - a - bcd - ( \x y -> case (x, y) of - (MemberSpec xs, MemberSpec ys) -> - MemberSpec - ( NE.fromList - [ (s, b, c, d) - | s <- NE.toList xs - , (b, c, d) <- NE.toList ys - ] - ) - (specA, specBCD) -> constrained $ \ps -> And [satisfies (head4_ ps) specA, satisfies (tail4_ ps) specBCD] - ) - - genFromTypeSpec (a, bcd) = f <$> genFromSpecT a <*> genFromSpecT bcd - where - f a' (b, c, d) = (a', b, c, d) - - toPreds x (a, bcd) = satisfies (head4_ x) a <> satisfies (tail4_ x) bcd - -head4_ :: All HasSpec '[a, b, c, d] => Term (a, b, c, d) -> Term a -head4_ x = App Head4W (x :> Nil) - -tail4_ :: All HasSpec '[a, b, c, d] => Term (a, b, c, d) -> Term (b, c, d) -tail4_ x = App Tail4W (x :> Nil) - --- ====================================================================== --- We need some function symbols, to break Bigger tuples into sub-tuples - -data TupleSym (ds :: [Type]) r where - Head3W :: All HasSpec '[a, b, c] => TupleSym '[(a, b, c)] a - Tail3W :: All HasSpec '[a, b, c] => TupleSym '[(a, b, c)] (b, c) - Head4W :: All HasSpec '[a, b, c, d] => TupleSym '[(a, b, c, d)] a - Tail4W :: All HasSpec '[a, b, c, d] => TupleSym '[(a, b, c, d)] (b, c, d) - -deriving instance Eq (TupleSym ds r) - -instance Show (TupleSym ds r) where show = name - -instance Syntax TupleSym where - inFix _ = False - name Head3W = "head3_" - name Tail3W = "tail3_" - name Head4W = "head4_" - name Tail4W = "tail4_" - -instance Semantics TupleSym where - semantics Head3W = \(a, _b, _c) -> a - semantics Tail3W = \(_a, b, c) -> (b, c) - semantics Head4W = \(a, _b, _c, _d) -> a - semantics Tail4W = \(_a, b, c, d) -> (b, c, d) - -instance Logic TupleSym where - propagate _ _ TrueSpec = TrueSpec - propagate _ _ (ErrorSpec msgs) = ErrorSpec msgs - propagate symW (Unary HOLE) (SuspendedSpec v ps) = - constrained $ \v' -> Let (App symW (v' :> Nil)) (v :-> ps) - propagate Head3W (Unary HOLE) specA = anyTail3 specA - propagate Tail3W (Unary HOLE) specBC = anyHead3 specBC - propagate Head4W (Unary HOLE) specA = anyTail4 specA - propagate Tail4W (Unary HOLE) specBCD = anyHead4 specBCD - -anyHead3 :: forall a b c. (HasSpec a, HasSpec b, HasSpec c) => Spec (b, c) -> Spec (a, b, c) -anyHead3 specBC = typeSpec @(a, b, c) (mempty @(Spec a), specBC) - -anyTail3 :: forall a b c. (HasSpec a, HasSpec b, HasSpec c) => Spec a -> Spec (a, b, c) -anyTail3 specA = typeSpec (specA, mempty @(Spec (b, c))) - -anyHead4 :: - forall a b c d. (HasSpec a, HasSpec b, HasSpec c, HasSpec d) => Spec (b, c, d) -> Spec (a, b, c, d) -anyHead4 specBCD = typeSpec (mempty @(Spec a), specBCD) - -anyTail4 :: - forall a b c d. (HasSpec a, HasSpec b, HasSpec c, HasSpec d) => Spec a -> Spec (a, b, c, d) -anyTail4 specA = typeSpec (specA, mempty @(Spec (b, c, d))) - --- ====================================================================== --- The Match class, with function `match` makes using all tuples uniform --- For any n-tuple, supply `match` with an n-ary function to bring into --- scope 'n' variables with type Term, which can be used to make Pred --- Note how the binary case is the inductive step, and the others just --- call the `match` with one less item in the tuple. - -class Match t (ts :: [Type]) | t -> ts where - match :: All HasSpec ts => Term t -> FunTy (MapList Term ts) Pred -> Pred - --- Base case where binary tuple. -instance Match (a, b) '[a, b] where - match ab f = - Let - (fst_ ab) - ( bind $ \ft -> - Let (snd_ ab) (bind $ \st -> f ft st) - ) - --- Inductive case for ternary tuple, calls 'match' for binary tuple. -instance Match (a, b, c) '[a, b, c] where - match abc f = - Let - (head3_ abc) - ( bind $ \a -> - Let - (tail3_ abc) - (bind $ \bc -> match @(b, c) bc (f a)) - ) - --- Inductive case for quadary tuple, calls 'match' for ternary tuple. -instance Match (a, b, c, d) '[a, b, c, d] where - match abcd f = - Let - (head4_ abcd) - ( bind $ \a -> - Let - (tail4_ abcd) - (bind $ \bcd -> match @(b, c, d) bcd (f a)) - ) - --- ========================================================= --- Here are some examples, Notice how the arity of the function --- passed to `match` changes as the width of the tuples changes. - -spec2 :: Spec (Integer, Integer) -spec2 = constrained $ \x -> - match x $ \a b -> Assert $ a <=. b - -spec3 :: Spec (Integer, Integer, Integer) -spec3 = constrained $ \v4 -> - match v4 $ \v3 v1 v0 -> And [Assert $ v3 <=. v1, Assert $ v1 <=. v0] - -spec4 :: Spec (Integer, Integer, Integer, Integer) -spec4 = constrained $ \x -> - match x $ \a b c d -> And [Assert $ a <=. b, Assert $ b <=. c, Assert $ c <=. d] - --- ======================================================== - -{- -class TypeList ts where - uncurryList :: FunTy (MapList f ts) r -> List f ts -> r - uncurryList_ :: (forall a. f a -> a) - -> FunTy ts r -> List f ts -> r - curryList :: (List f ts -> r) -> FunTy (MapList f ts) r - curryList_ :: (forall a. a -> f a) - -> (List f ts -> r) -> FunTy ts r - unfoldList :: (forall a (as :: [*]). List f as -> f a) -> List f ts --} - --- | Fold over a (List Term ts) with 'getTermsize' which consumes a Term component for each element of the list -ex1 :: Maybe Int -ex1 = uncurryList getTermsize1 args1 - where - args1 :: List Term '[Int, Bool, String] - args1 = Lit 5 :> Lit True :> Lit "abc" :> Nil - getTermsize1 :: Term Int -> Term Bool -> Term String -> Maybe Int - getTermsize1 (Lit n) (Lit b) (Lit s) = Just $ if b then n else length s - getTermsize1 _ _ _ = Nothing - --- Fold over a list with two parts 'unLit' and 'getSize' -ex2 :: Int -ex2 = uncurryList_ unLit getsize2 args2 - where - unLit :: forall a. Term a -> a - unLit (Lit n) = n - unLit _ = error "unLit on non literal" - getsize2 :: Int -> Bool -> String -> Int - getsize2 n b s = if b then n else length s - args2 :: List Term '[Int, Bool, String] - args2 = Lit 5 :> Lit True :> Lit "abc" :> Nil - --- Construct a function from a List and function on that list. -ex3 :: Term a -> Term b -> Term c -> String -ex3 = curryList crush - where - crush :: (List Term '[a, b, c] -> String) - crush (a :> b :> c :> Nil) = show a ++ show b ++ show c - --- Construct a function over from a -ex4 :: Int -> Bool -> String -> Int -ex4 = curryList_ one totalLength - where - totalLength :: List [] '[Int, Bool, String] -> Int - totalLength (n :> b :> s :> Nil) = length n + length b + length s - one :: a -> [a] - one x = [x] - -ex5 :: Spec (Set Integer) -ex5 = constrained $ \s -> Assert (size_ s ==. Lit 104) - --- ========================================================================== - -data Sum3 a b c where - Inj3_1 :: a -> Sum3 a b c - Inj3_2 :: b -> Sum3 a b c - Inj3_3 :: c -> Sum3 a b c - -deriving instance (Show a, Show b, Show c) => Show (Sum3 a b c) - -deriving instance (Eq a, Eq b, Eq c) => Eq (Sum3 a b c) - -foo_ :: Term (Sum3 a b c) -> Term a -foo_ = undefined - -bar_ = undefined - -bar_ :: Term (Sum3 a b c) -> Term (Either b c) -guardSum3 :: - forall a b c. (HasSpec a, HasSpec b, HasSpec c) => Spec a -> Spec (Either b c) -> Spec (Sum3 a b c) -guardSum3 (ErrorSpec es) (ErrorSpec fs) = ErrorSpec (es <> fs) -guardSum3 (ErrorSpec es) _ = ErrorSpec (NE.cons "Sum3 error on left" es) -guardSum3 _ (ErrorSpec es) = ErrorSpec (NE.cons "Sum3 error on right" es) -guardSum3 s s' = typeSpec $ SumSpec s s' - -instance (HasSpec a, HasSpec b, HasSpec c) => HasSpec (Sum3 a b c) where - type TypeSpec (Sum3 a b c) = SumSpec (Spec a) (Spec (Either b c)) - - anySpec = SumSpec TrueSpec TrueSpec - - combineSpec (SumSpec x y) (SumSpec a b) = guardSum3 (x <> a) (y <> b) - - conformsTo (Inj3_1 a) (SumSpec as _) = conformsToSpec a as - conformsTo (Inj3_2 b) (SumSpec _ es) = conformsToSpec (Left b) es - conformsTo (Inj3_3 c) (SumSpec _ es) = conformsToSpec (Right c) es - - toPreds x (SumSpec a es) = satisfies (foo_ x) a <> satisfies (bar_ x) es - - genFromTypeSpec (SumSpec (simplifySpec -> sa) (simplifySpec -> sb)) - | emptyA, emptyB = genError "genFromTypeSpec @SumSpec: empty" - | emptyA = Inj3_1 <$> genFromSpecT sa - | emptyB = select <$> genFromSpecT sb - | otherwise = oneofT [Inj3_1 <$> genFromSpecT sa, select <$> genFromSpecT sb] - where - emptyA = isErrorLike sa - emptyB = isErrorLike sb - select :: Either b c -> Sum3 a b c - select (Left x) = Inj3_2 x - select (Right x) = Inj3_3 x - --- ==================================================== - -coerce_ :: Term (E3 a b c) -> Term (Either a (Either b c)) -coerce_ = undefined - -newtype E3 a b c = E3 (Either a (Either b c)) - deriving (Eq, Show) via Either a (Either b c) - -{- -instance (HasSpec a, HasSpec b, HasSpec c) => HasSpec (E3 a b c) where - type TypeSpec (E3 a b c) = TypeSpec (Either a (Either b c)) - - anySpec = SumSpec TrueSpec TrueSpec - - combineSpec (SumSpec x y) (SumSpec a b) = typeSpec (SumSpec (x <> a) (y <> b)) - - conformsTo (E3 (Left x)) (SumSpec a b) = conformsToSpec x a - conformsTo (E3 (Right x)) (SumSpec a b) = conformsToSpec x b - - toPreds x (SumSpec a b) = Case (coerce_ x) - (bind $ \y -> satisfies y a) - (bind $ \y -> satisfies y b) - -flipp :: (Eq b, Typeable b, Show b, HasSpec b, Coercible a b) => Term a -> Term b -flipp (Lit x) = Lit (coerce x) -flipp (V x) = V (coerce x) --- flipp (App c xs) = App (coerce c) xs --}