{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Constrained.Syntax where
import Constrained.Base (
Binder (..),
Forallable,
HasGenHint,
HasSpec,
Hint,
IsPred,
Pred (..),
Specification (..),
Term (..),
Weighted (..),
bind,
explainSpecOpt,
forAllToList,
mapWeighted,
semantics,
toPred,
vsep',
(/>),
)
import Constrained.Core (
Rename (rename),
Value (..),
Var (..),
eqVar,
freshen,
unValue,
)
import Constrained.Env (
Env,
extendEnv,
lookupEnv,
removeVar,
singletonEnv,
)
import Constrained.GenT (
GE (..),
MonadGenError (..),
errorGE,
explain,
fatalError,
)
import Constrained.Generic (
Sum (..),
SumOver,
)
import Constrained.Graph (
Graph (..),
)
import Constrained.List (
List (..),
foldMapList,
mapList,
mapListC,
mapMList,
uncurryList_,
)
import Control.Monad.Identity
import Control.Monad.Writer (Writer, tell)
import Data.Foldable (fold, toList)
import qualified Data.List.NonEmpty as NE
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (fromMaybe, isJust, isNothing)
import qualified Data.Monoid as Monoid
import Data.Orphans ()
import Data.Semigroup (Any (..))
import qualified Data.Semigroup as Semigroup
import Data.Set (Set)
import qualified Data.Set as Set
import Data.String (fromString)
import Data.Typeable
import qualified Language.Haskell.TH as TH
import qualified Language.Haskell.TH.Quote as TH
import Prettyprinter hiding (cat)
import Test.QuickCheck hiding (Args, Fun, Witness, forAll, witness)
import Prelude hiding (pred)
mkNamed :: String -> TH.Q TH.Pat
mkNamed :: String -> Q Pat
mkNamed String
x =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
Exp -> Pat -> Pat
TH.ViewP (Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE forall a b. (a -> b) -> a -> b
$ String -> Name
TH.mkName String
"name") (Lit -> Exp
TH.LitE forall a b. (a -> b) -> a -> b
$ String -> Lit
TH.StringL String
x)) (Name -> Pat
TH.VarP forall a b. (a -> b) -> a -> b
$ String -> Name
TH.mkName String
x)
mkNamedExpr :: String -> TH.Q TH.Exp
mkNamedExpr :: String -> Q Exp
mkNamedExpr String
x =
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
Exp -> Exp -> Exp
TH.AppE (Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE forall a b. (a -> b) -> a -> b
$ String -> Name
TH.mkName String
"name") (Lit -> Exp
TH.LitE forall a b. (a -> b) -> a -> b
$ String -> Lit
TH.StringL String
x)) (Name -> Exp
TH.VarE forall a b. (a -> b) -> a -> b
$ String -> Name
TH.mkName String
x)
var :: TH.QuasiQuoter
var :: QuasiQuoter
var =
TH.QuasiQuoter
{
quotePat :: String -> Q Pat
TH.quotePat = String -> Q Pat
mkNamed forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
varName
,
quoteExp :: String -> Q Exp
TH.quoteExp = String -> Q Exp
mkNamedExpr forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
varName
, quoteDec :: String -> Q [Dec]
TH.quoteDec = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"var should only be used at binding sites and in expressions"
, quoteType :: String -> Q Type
TH.quoteType = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"var should only be used at binding sites and in expressions"
}
where
varName :: String -> String
varName String
s = case String -> [String]
words String
s of
[String
w] -> String
w
[String]
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"expected a single var name"
freeVarNames :: forall t. HasVariables t => t -> Set Int
freeVarNames :: forall t. HasVariables t => t -> Set Int
freeVarNames = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (\(Name Var a
v) -> forall a. Var a -> Int
nameOf Var a
v) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasVariables a => a -> Set Name
freeVarSet
newtype FreeVars = FreeVars {FreeVars -> Map Name Int
unFreeVars :: Map Name Int}
deriving (Int -> FreeVars -> String -> String
[FreeVars] -> String -> String
FreeVars -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [FreeVars] -> String -> String
$cshowList :: [FreeVars] -> String -> String
show :: FreeVars -> String
$cshow :: FreeVars -> String
showsPrec :: Int -> FreeVars -> String -> String
$cshowsPrec :: Int -> FreeVars -> String -> String
Show)
restrictedTo :: FreeVars -> Set Name -> FreeVars
restrictedTo :: FreeVars -> Set Name -> FreeVars
restrictedTo (FreeVars Map Name Int
m) Set Name
nms = Map Name Int -> FreeVars
FreeVars forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map Name Int
m Set Name
nms
memberOf :: Name -> FreeVars -> Bool
memberOf :: Name -> FreeVars -> Bool
memberOf Name
n (FreeVars Map Name Int
m) = forall k a. Ord k => k -> Map k a -> Bool
Map.member Name
n Map Name Int
m
count :: Name -> FreeVars -> Int
count :: Name -> FreeVars -> Int
count Name
n (FreeVars Map Name Int
m) = forall a. a -> Maybe a -> a
fromMaybe Int
0 forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name Int
m
instance Semigroup FreeVars where
FreeVars Map Name Int
fv <> :: FreeVars -> FreeVars -> FreeVars
<> FreeVars Map Name Int
fv' = Map Name Int -> FreeVars
FreeVars forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Num a => a -> a -> a
(+) Map Name Int
fv Map Name Int
fv'
instance Monoid FreeVars where
mempty :: FreeVars
mempty = Map Name Int -> FreeVars
FreeVars forall a. Monoid a => a
mempty
freeVar :: Name -> FreeVars
freeVar :: Name -> FreeVars
freeVar Name
n = Name -> Int -> FreeVars
singleton Name
n Int
1
singleton :: Name -> Int -> FreeVars
singleton :: Name -> Int -> FreeVars
singleton Name
n Int
k = Map Name Int -> FreeVars
FreeVars forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
Map.singleton Name
n Int
k
without :: Foldable t => FreeVars -> t Name -> FreeVars
without :: forall (t :: * -> *). Foldable t => FreeVars -> t Name -> FreeVars
without (FreeVars Map Name Int
m) t Name
remove = Map Name Int -> FreeVars
FreeVars forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Map Name Int
m (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t Name
remove)
class HasVariables a where
freeVars :: a -> FreeVars
freeVarSet :: a -> Set Name
freeVarSet = forall k a. Map k a -> Set k
Map.keysSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeVars -> Map Name Int
unFreeVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasVariables a => a -> FreeVars
freeVars
countOf :: Name -> a -> Int
countOf Name
n = Name -> FreeVars -> Int
count Name
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasVariables a => a -> FreeVars
freeVars
appearsIn :: Name -> a -> Bool
appearsIn Name
n = (forall a. Ord a => a -> a -> Bool
> Int
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> FreeVars -> Int
count Name
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasVariables a => a -> FreeVars
freeVars
instance (HasVariables a, HasVariables b) => HasVariables (a, b) where
freeVars :: (a, b) -> FreeVars
freeVars (a
a, b
b) = forall a. HasVariables a => a -> FreeVars
freeVars a
a forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> FreeVars
freeVars b
b
freeVarSet :: (a, b) -> Set Name
freeVarSet (a
a, b
b) = forall a. HasVariables a => a -> Set Name
freeVarSet a
a forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> Set Name
freeVarSet b
b
countOf :: Name -> (a, b) -> Int
countOf Name
n (a
a, b
b) = forall a. HasVariables a => Name -> a -> Int
countOf Name
n a
a forall a. Num a => a -> a -> a
+ forall a. HasVariables a => Name -> a -> Int
countOf Name
n b
b
appearsIn :: Name -> (a, b) -> Bool
appearsIn Name
n (a
a, b
b) = forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n a
a Bool -> Bool -> Bool
|| forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n b
b
instance HasVariables (List Term as) where
freeVars :: List Term as -> FreeVars
freeVars List Term as
Nil = forall a. Monoid a => a
mempty
freeVars (Term a
x :> List Term as1
xs) = forall a. HasVariables a => a -> FreeVars
freeVars Term a
x forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> FreeVars
freeVars List Term as1
xs
freeVarSet :: List Term as -> Set Name
freeVarSet List Term as
Nil = forall a. Monoid a => a
mempty
freeVarSet (Term a
x :> List Term as1
xs) = forall a. HasVariables a => a -> Set Name
freeVarSet Term a
x forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> Set Name
freeVarSet List Term as1
xs
countOf :: Name -> List Term as -> Int
countOf Name
_ List Term as
Nil = Int
0
countOf Name
n (Term a
x :> List Term as1
xs) = forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term a
x forall a. Num a => a -> a -> a
+ forall a. HasVariables a => Name -> a -> Int
countOf Name
n List Term as1
xs
appearsIn :: Name -> List Term as -> Bool
appearsIn Name
_ List Term as
Nil = Bool
False
appearsIn Name
n (Term a
x :> List Term as1
xs) = forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term a
x Bool -> Bool -> Bool
|| forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n List Term as1
xs
instance HasVariables Name where
freeVars :: Name -> FreeVars
freeVars = Name -> FreeVars
freeVar
freeVarSet :: Name -> Set Name
freeVarSet = forall a. a -> Set a
Set.singleton
countOf :: Name -> Name -> Int
countOf Name
n Name
n'
| Name
n forall a. Eq a => a -> a -> Bool
== Name
n' = Int
1
| Bool
otherwise = Int
0
appearsIn :: Name -> Name -> Bool
appearsIn Name
n Name
n' = Name
n forall a. Eq a => a -> a -> Bool
== Name
n'
instance HasVariables (Term a) where
freeVars :: Term a -> FreeVars
freeVars = \case
Lit {} -> forall a. Monoid a => a
mempty
V Var a
x -> Name -> FreeVars
freeVar (forall a. HasSpec a => Var a -> Name
Name Var a
x)
App t dom a
_ List Term dom
ts -> forall a. HasVariables a => a -> FreeVars
freeVars List Term dom
ts
freeVarSet :: Term a -> Set Name
freeVarSet = \case
Lit {} -> forall a. Monoid a => a
mempty
V Var a
x -> forall a. HasVariables a => a -> Set Name
freeVarSet (forall a. HasSpec a => Var a -> Name
Name Var a
x)
App t dom a
_ List Term dom
ts -> forall a. HasVariables a => a -> Set Name
freeVarSet List Term dom
ts
countOf :: Name -> Term a -> Int
countOf Name
n = \case
Lit {} -> Int
0
V Var a
x -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n (forall a. HasSpec a => Var a -> Name
Name Var a
x)
App t dom a
_ List Term dom
ts -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n List Term dom
ts
appearsIn :: Name -> Term a -> Bool
appearsIn Name
n = \case
Lit {} -> Bool
False
V Var a
x -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n (forall a. HasSpec a => Var a -> Name
Name Var a
x)
App t dom a
_ List Term dom
ts -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n List Term dom
ts
instance HasVariables Pred where
freeVars :: Pred -> FreeVars
freeVars = \case
ElemPred Bool
_ Term a
t NonEmpty a
_ -> forall a. HasVariables a => a -> FreeVars
freeVars Term a
t
GenHint Hint a
_ Term a
t -> forall a. HasVariables a => a -> FreeVars
freeVars Term a
t
Subst Var a
x Term a
t Pred
p -> forall a. HasVariables a => a -> FreeVars
freeVars Term a
t forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> FreeVars
freeVars Pred
p forall (t :: * -> *). Foldable t => FreeVars -> t Name -> FreeVars
`without` [forall a. HasSpec a => Var a -> Name
Name Var a
x]
And [Pred]
ps -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. HasVariables a => a -> FreeVars
freeVars [Pred]
ps
Let Term a
t Binder a
b -> forall a. HasVariables a => a -> FreeVars
freeVars Term a
t forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> FreeVars
freeVars Binder a
b
Exists (forall b. Term b -> b) -> GE a
_ Binder a
b -> forall a. HasVariables a => a -> FreeVars
freeVars Binder a
b
Assert Term Bool
t -> forall a. HasVariables a => a -> FreeVars
freeVars Term Bool
t
Reifies Term b
t' Term a
t a -> b
_ -> forall a. HasVariables a => a -> FreeVars
freeVars Term b
t' forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> FreeVars
freeVars Term a
t
DependsOn Term a
x Term b
y -> forall a. HasVariables a => a -> FreeVars
freeVars Term a
x forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> FreeVars
freeVars Term b
y
ForAll Term t
set Binder a
b -> forall a. HasVariables a => a -> FreeVars
freeVars Term t
set forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> FreeVars
freeVars Binder a
b
Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall a. HasVariables a => a -> FreeVars
freeVars Term (SumOver as)
t forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> FreeVars
freeVars List (Weighted Binder) as
bs
When Term Bool
b Pred
p -> forall a. HasVariables a => a -> FreeVars
freeVars Term Bool
b forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> FreeVars
freeVars Pred
p
Pred
TruePred -> forall a. Monoid a => a
mempty
FalsePred NonEmpty String
_ -> forall a. Monoid a => a
mempty
Monitor {} -> forall a. Monoid a => a
mempty
Explain NonEmpty String
_ Pred
p -> forall a. HasVariables a => a -> FreeVars
freeVars Pred
p
freeVarSet :: Pred -> Set Name
freeVarSet = \case
ElemPred Bool
_ Term a
t NonEmpty a
_ -> forall a. HasVariables a => a -> Set Name
freeVarSet Term a
t
GenHint Hint a
_ Term a
t -> forall a. HasVariables a => a -> Set Name
freeVarSet Term a
t
Subst Var a
x Term a
t Pred
p -> forall a. HasVariables a => a -> Set Name
freeVarSet Term a
t forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => a -> Set a -> Set a
Set.delete (forall a. HasSpec a => Var a -> Name
Name Var a
x) (forall a. HasVariables a => a -> Set Name
freeVarSet Pred
p)
And [Pred]
ps -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. HasVariables a => a -> Set Name
freeVarSet [Pred]
ps
Let Term a
t Binder a
b -> forall a. HasVariables a => a -> Set Name
freeVarSet Term a
t forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> Set Name
freeVarSet Binder a
b
Exists (forall b. Term b -> b) -> GE a
_ Binder a
b -> forall a. HasVariables a => a -> Set Name
freeVarSet Binder a
b
Assert Term Bool
t -> forall a. HasVariables a => a -> Set Name
freeVarSet Term Bool
t
Reifies Term b
t' Term a
t a -> b
_ -> forall a. HasVariables a => a -> Set Name
freeVarSet Term b
t' forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> Set Name
freeVarSet Term a
t
DependsOn Term a
x Term b
y -> forall a. HasVariables a => a -> Set Name
freeVarSet Term a
x forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> Set Name
freeVarSet Term b
y
ForAll Term t
set Binder a
b -> forall a. HasVariables a => a -> Set Name
freeVarSet Term t
set forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> Set Name
freeVarSet Binder a
b
Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall a. HasVariables a => a -> Set Name
freeVarSet Term (SumOver as)
t forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> Set Name
freeVarSet List (Weighted Binder) as
bs
When Term Bool
b Pred
p -> forall a. HasVariables a => a -> Set Name
freeVarSet Term Bool
b forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> Set Name
freeVarSet Pred
p
Explain NonEmpty String
_ Pred
p -> forall a. HasVariables a => a -> Set Name
freeVarSet Pred
p
Pred
TruePred -> forall a. Monoid a => a
mempty
FalsePred NonEmpty String
_ -> forall a. Monoid a => a
mempty
Monitor {} -> forall a. Monoid a => a
mempty
countOf :: Name -> Pred -> Int
countOf Name
n = \case
ElemPred Bool
_ Term a
t NonEmpty a
_ -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term a
t
GenHint Hint a
_ Term a
t -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term a
t
Subst Var a
x Term a
t Pred
p
| Name
n forall a. Eq a => a -> a -> Bool
== forall a. HasSpec a => Var a -> Name
Name Var a
x -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term a
t
| Bool
otherwise -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term a
t forall a. Num a => a -> a -> a
+ forall a. HasVariables a => Name -> a -> Int
countOf Name
n Pred
p
And [Pred]
ps -> forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. HasVariables a => Name -> a -> Int
countOf Name
n) [Pred]
ps
Let Term a
t Binder a
b -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term a
t forall a. Num a => a -> a -> a
+ forall a. HasVariables a => Name -> a -> Int
countOf Name
n Binder a
b
Exists (forall b. Term b -> b) -> GE a
_ Binder a
b -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n Binder a
b
Assert Term Bool
t -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term Bool
t
Reifies Term b
t' Term a
t a -> b
_ -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term b
t' forall a. Num a => a -> a -> a
+ forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term a
t
DependsOn Term a
x Term b
y -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term a
x forall a. Num a => a -> a -> a
+ forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term b
y
ForAll Term t
set Binder a
b -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term t
set forall a. Num a => a -> a -> a
+ forall a. HasVariables a => Name -> a -> Int
countOf Name
n Binder a
b
Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term (SumOver as)
t forall a. Num a => a -> a -> a
+ forall a. HasVariables a => Name -> a -> Int
countOf Name
n List (Weighted Binder) as
bs
When Term Bool
b Pred
p -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term Bool
b forall a. Num a => a -> a -> a
+ forall a. HasVariables a => Name -> a -> Int
countOf Name
n Pred
p
Explain NonEmpty String
_ Pred
p -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n Pred
p
Pred
TruePred -> Int
0
FalsePred NonEmpty String
_ -> Int
0
Monitor {} -> Int
0
appearsIn :: Name -> Pred -> Bool
appearsIn Name
n = \case
ElemPred Bool
_ Term a
t NonEmpty a
_ -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term a
t
GenHint Hint a
_ Term a
t -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term a
t
Subst Var a
x Term a
t Pred
p
| Name
n forall a. Eq a => a -> a -> Bool
== forall a. HasSpec a => Var a -> Name
Name Var a
x -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term a
t
| Bool
otherwise -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term a
t Bool -> Bool -> Bool
|| forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Pred
p
And [Pred]
ps -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n) [Pred]
ps
Let Term a
t Binder a
b -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term a
t Bool -> Bool -> Bool
|| forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Binder a
b
Exists (forall b. Term b -> b) -> GE a
_ Binder a
b -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Binder a
b
Assert Term Bool
t -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term Bool
t
Reifies Term b
t' Term a
t a -> b
_ -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term b
t' Bool -> Bool -> Bool
|| forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term a
t
DependsOn Term a
x Term b
y -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term a
x Bool -> Bool -> Bool
|| forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term b
y
ForAll Term t
set Binder a
b -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term t
set Bool -> Bool -> Bool
|| forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Binder a
b
Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term (SumOver as)
t Bool -> Bool -> Bool
|| forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n List (Weighted Binder) as
bs
When Term Bool
b Pred
p -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term Bool
b Bool -> Bool -> Bool
|| forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Pred
p
Explain NonEmpty String
_ Pred
p -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Pred
p
Pred
TruePred -> Bool
False
FalsePred NonEmpty String
_ -> Bool
False
Monitor {} -> Bool
False
instance HasVariables (Binder a) where
freeVars :: Binder a -> FreeVars
freeVars (Var a
x :-> Pred
p) = forall a. HasVariables a => a -> FreeVars
freeVars Pred
p forall (t :: * -> *). Foldable t => FreeVars -> t Name -> FreeVars
`without` [forall a. HasSpec a => Var a -> Name
Name Var a
x]
freeVarSet :: Binder a -> Set Name
freeVarSet (Var a
x :-> Pred
p) = forall a. Ord a => a -> Set a -> Set a
Set.delete (forall a. HasSpec a => Var a -> Name
Name Var a
x) (forall a. HasVariables a => a -> Set Name
freeVarSet Pred
p)
countOf :: Name -> Binder a -> Int
countOf Name
n (Var a
x :-> Pred
p)
| forall a. HasSpec a => Var a -> Name
Name Var a
x forall a. Eq a => a -> a -> Bool
== Name
n = Int
0
| Bool
otherwise = forall a. HasVariables a => Name -> a -> Int
countOf Name
n Pred
p
appearsIn :: Name -> Binder a -> Bool
appearsIn Name
n (Var a
x :-> Pred
p)
| forall a. HasSpec a => Var a -> Name
Name Var a
x forall a. Eq a => a -> a -> Bool
== Name
n = Bool
False
| Bool
otherwise = forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Pred
p
instance HasVariables (f a) => HasVariables (Weighted f a) where
freeVars :: Weighted f a -> FreeVars
freeVars = forall a. HasVariables a => a -> FreeVars
freeVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing
freeVarSet :: Weighted f a -> Set Name
freeVarSet = forall a. HasVariables a => a -> Set Name
freeVarSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing
countOf :: Name -> Weighted f a -> Int
countOf Name
n = forall a. HasVariables a => Name -> a -> Int
countOf Name
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing
appearsIn :: Name -> Weighted f a -> Bool
appearsIn Name
n = forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing
instance HasVariables (List (Weighted Binder) as) where
freeVars :: List (Weighted Binder) as -> FreeVars
freeVars List (Weighted Binder) as
Nil = forall a. Monoid a => a
mempty
freeVars (Weighted Binder a
a :> List (Weighted Binder) as1
as) = forall a. HasVariables a => a -> FreeVars
freeVars Weighted Binder a
a forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> FreeVars
freeVars List (Weighted Binder) as1
as
freeVarSet :: List (Weighted Binder) as -> Set Name
freeVarSet List (Weighted Binder) as
Nil = forall a. Monoid a => a
mempty
freeVarSet (Weighted Binder a
a :> List (Weighted Binder) as1
as) = forall a. HasVariables a => a -> Set Name
freeVarSet Weighted Binder a
a forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> Set Name
freeVarSet List (Weighted Binder) as1
as
countOf :: Name -> List (Weighted Binder) as -> Int
countOf Name
_ List (Weighted Binder) as
Nil = Int
0
countOf Name
n (Weighted Binder a
x :> List (Weighted Binder) as1
xs) = forall a. HasVariables a => Name -> a -> Int
countOf Name
n Weighted Binder a
x forall a. Num a => a -> a -> a
+ forall a. HasVariables a => Name -> a -> Int
countOf Name
n List (Weighted Binder) as1
xs
appearsIn :: Name -> List (Weighted Binder) as -> Bool
appearsIn Name
_ List (Weighted Binder) as
Nil = Bool
False
appearsIn Name
n (Weighted Binder a
x :> List (Weighted Binder) as1
xs) = forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Weighted Binder a
x Bool -> Bool -> Bool
|| forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n List (Weighted Binder) as1
xs
instance {-# OVERLAPPABLE #-} (Foldable t, HasVariables a) => HasVariables (t a) where
freeVars :: t a -> FreeVars
freeVars = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. HasVariables a => a -> FreeVars
freeVars
freeVarSet :: t a -> Set Name
freeVarSet = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. HasVariables a => a -> Set Name
freeVarSet
countOf :: Name -> t a -> Int
countOf Name
n = forall a. Sum a -> a
Monoid.getSum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a. a -> Sum a
Monoid.Sum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasVariables a => Name -> a -> Int
countOf Name
n)
appearsIn :: Name -> t a -> Bool
appearsIn Name
n = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n)
instance HasVariables a => HasVariables (Set a) where
freeVars :: Set a -> FreeVars
freeVars = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. HasVariables a => a -> FreeVars
freeVars
freeVarSet :: Set a -> Set Name
freeVarSet = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. HasVariables a => a -> Set Name
freeVarSet
countOf :: Name -> Set a -> Int
countOf Name
n = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall a. HasVariables a => Name -> a -> Int
countOf Name
n)
appearsIn :: Name -> Set a -> Bool
appearsIn Name
n = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n)
type Subst = [SubstEntry]
data SubstEntry where
(:=) :: HasSpec a => Var a -> Term a -> SubstEntry
backwardsSubstitution :: forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution :: forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub0 Term a
t =
case Subst -> Term a -> Maybe (Var a)
findMatch Subst
sub0 Term a
t of
Just Var a
x -> forall a. HasSpec a => Var a -> Term a
V Var a
x
Maybe (Var a)
Nothing -> case Term a
t of
Lit a
a -> forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
a
V Var a
x -> forall a. HasSpec a => Var a -> Term a
V Var a
x
App t dom a
f List Term dom
ts -> forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App t dom a
f (forall {k} (c :: k -> Constraint) (as :: [k]) (f :: k -> *)
(g :: k -> *).
All c as =>
(forall (a :: k). c a => f a -> g a) -> List f as -> List g as
mapListC @HasSpec (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub0) List Term dom
ts)
where
findMatch :: Subst -> Term a -> Maybe (Var a)
findMatch :: Subst -> Term a -> Maybe (Var a)
findMatch [] Term a
_ = forall a. Maybe a
Nothing
findMatch (Var a
x := Term a
t' : Subst
sub1) Term a
t1
| forall a b. Term a -> Term b -> Bool
fastInequality Term a
t1 Term a
t' = Subst -> Term a -> Maybe (Var a)
findMatch Subst
sub1 Term a
t1
| Just (Var a
x', Term a
t'') <- forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast (Var a
x, Term a
t')
, Term a
t forall a. Eq a => a -> a -> Bool
== Term a
t'' =
forall a. a -> Maybe a
Just Var a
x'
| Bool
otherwise = Subst -> Term a -> Maybe (Var a)
findMatch Subst
sub1 Term a
t1
fastInequality :: Term a -> Term b -> Bool
fastInequality :: forall a b. Term a -> Term b -> Bool
fastInequality (V (Var Int
i String
_)) (V (Var Int
j String
_)) = Int
i forall a. Eq a => a -> a -> Bool
/= Int
j
fastInequality Lit {} Lit {} = Bool
False
fastInequality (App t dom a
_ List Term dom
as) (App t dom b
_ List Term dom
bs) = forall (as :: [*]) (bs :: [*]).
List Term as -> List Term bs -> Bool
go List Term dom
as List Term dom
bs
where
go :: List Term as -> List Term bs -> Bool
go :: forall (as :: [*]) (bs :: [*]).
List Term as -> List Term bs -> Bool
go List Term as
Nil List Term bs
Nil = Bool
False
go (Term a
a :> List Term as1
as') (Term a
b :> List Term as1
bs') = forall a b. Term a -> Term b -> Bool
fastInequality Term a
a Term a
b Bool -> Bool -> Bool
|| forall (as :: [*]) (bs :: [*]).
List Term as -> List Term bs -> Bool
go List Term as1
as' List Term as1
bs'
go List Term as
_ List Term bs
_ = Bool
True
fastInequality Term a
_ Term b
_ = Bool
True
substituteTerm :: forall a. Subst -> Term a -> Term a
substituteTerm :: forall a. Subst -> Term a -> Term a
substituteTerm Subst
sub = \case
Lit a
a -> forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
a
V Var a
x -> HasSpec a => Subst -> Var a -> Term a
substVar Subst
sub Var a
x
App t dom a
f (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (forall a. Subst -> Term a -> Term a
substituteTerm Subst
sub) -> (List Term dom
ts :: List Term dom)) ->
case forall (as :: [*]). List Term as -> Maybe (List Value as)
fromLits List Term dom
ts of
Just List Value dom
vs -> forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit (forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
uncurryList_ forall a. Value a -> a
unValue (forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t dom a
f) List Value dom
vs)
Maybe (List Value dom)
_ -> forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App t dom a
f List Term dom
ts
where
substVar :: HasSpec a => Subst -> Var a -> Term a
substVar :: HasSpec a => Subst -> Var a -> Term a
substVar [] Var a
x = forall a. HasSpec a => Var a -> Term a
V Var a
x
substVar (Var a
y := Term a
t : Subst
sub1) Var a
x
| Just a :~: a
Refl <- forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var a
y = Term a
t
| Bool
otherwise = HasSpec a => Subst -> Var a -> Term a
substVar Subst
sub1 Var a
x
substituteTerm' :: forall a. Subst -> Term a -> Writer Any (Term a)
substituteTerm' :: forall a. Subst -> Term a -> Writer Any (Term a)
substituteTerm' Subst
sub = \case
Lit a
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
a
V Var a
x -> HasSpec a => Subst -> Var a -> Writer Any (Term a)
substVar Subst
sub Var a
x
App t dom a
f List Term dom
ts ->
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App t dom a
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (as :: [k]).
Applicative m =>
(forall (a :: k). f a -> m (g a)) -> List f as -> m (List g as)
mapMList (forall a. Subst -> Term a -> Writer Any (Term a)
substituteTerm' Subst
sub) List Term dom
ts
where
substVar :: HasSpec a => Subst -> Var a -> Writer Any (Term a)
substVar :: HasSpec a => Subst -> Var a -> Writer Any (Term a)
substVar [] Var a
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Term a
V Var a
x
substVar (Var a
y := Term a
t : Subst
sub1) Var a
x
| Just a :~: a
Refl <- forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var a
y = Term a
t forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Bool -> Any
Any Bool
True)
| Bool
otherwise = HasSpec a => Subst -> Var a -> Writer Any (Term a)
substVar Subst
sub1 Var a
x
substituteBinder :: HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder :: forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm (Var b
y :-> Pred
p) = Var b
y' forall a. HasSpec a => Var a -> Pred -> Binder a
:-> forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm Pred
p'
where
(Var b
y', Pred
p') =
forall a t.
(Typeable a, Rename t) =>
Var a -> t -> Set Int -> (Var a, t)
freshen Var b
y Pred
p (forall a. a -> Set a
Set.singleton (forall a. Var a -> Int
nameOf Var a
x) forall a. Semigroup a => a -> a -> a
<> forall t. HasVariables t => t -> Set Int
freeVarNames Term a
tm forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => a -> Set a -> Set a
Set.delete (forall a. Var a -> Int
nameOf Var b
y) (forall t. HasVariables t => t -> Set Int
freeVarNames Pred
p))
substitutePred :: HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred :: forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm = \case
ElemPred Bool
bool Term a
t NonEmpty a
xs -> forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term a
t) NonEmpty a
xs
GenHint Hint a
h Term a
t -> forall a. HasGenHint a => Hint a -> Term a -> Pred
GenHint Hint a
h (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term a
t)
Subst Var a
x' Term a
t Pred
p -> forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x' Term a
t Pred
p
Assert Term Bool
t -> Term Bool -> Pred
Assert (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term Bool
t)
And [Pred]
ps -> forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (\forall b. Term b -> b
eval -> (forall b. Term b -> b) -> GE a
k (forall b. Term b -> b
eval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm])) (forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm Binder a
b)
Let Term a
t Binder a
b -> forall a. Term a -> Binder a -> Pred
Let (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term a
t) (forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm Binder a
b)
ForAll Term t
t Binder a
b -> forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term t
t) (forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm Binder a
b)
Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term (SumOver as)
t) (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (forall {k1} {k2} (f :: k1 -> *) (a :: k1) (g :: k2 -> *) (b :: k2).
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted forall a b. (a -> b) -> a -> b
$ forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm) List (Weighted Binder) as
bs)
When Term Bool
b Pred
p -> HasSpec Bool => Term Bool -> Pred -> Pred
When (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term Bool
b) (forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm Pred
p)
Reifies Term b
t' Term a
t a -> b
f -> forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
Reifies (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term b
t') (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term a
t) a -> b
f
DependsOn Term a
t Term b
t' -> forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term a
t) (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term b
t')
Pred
TruePred -> Pred
TruePred
FalsePred NonEmpty String
es -> NonEmpty String -> Pred
FalsePred NonEmpty String
es
Monitor (forall b. Term b -> b) -> Property -> Property
m -> ((forall b. Term b -> b) -> Property -> Property) -> Pred
Monitor (\forall b. Term b -> b
eval -> (forall b. Term b -> b) -> Property -> Property
m (forall b. Term b -> b
eval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm]))
Explain NonEmpty String
es Pred
p -> NonEmpty String -> Pred -> Pred
Explain NonEmpty String
es forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm Pred
p
substTerm :: Env -> Term a -> Term a
substTerm :: forall a. Env -> Term a -> Term a
substTerm Env
env = \case
Lit a
a -> forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
a
V Var a
v
| Just a
a <- forall a. Typeable a => Env -> Var a -> Maybe a
lookupEnv Env
env Var a
v -> forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
a
| Bool
otherwise -> forall a. HasSpec a => Var a -> Term a
V Var a
v
App t dom a
f (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (forall a. Env -> Term a -> Term a
substTerm Env
env) -> List Term dom
ts) ->
case forall (as :: [*]). List Term as -> Maybe (List Value as)
fromLits List Term dom
ts of
Just List Value dom
vs -> forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit (forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
uncurryList_ forall a. Value a -> a
unValue (forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t dom a
f) List Value dom
vs)
Maybe (List Value dom)
_ -> forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App t dom a
f List Term dom
ts
substBinder :: Env -> Binder a -> Binder a
substBinder :: forall a. Env -> Binder a -> Binder a
substBinder Env
env (Var a
x :-> Pred
p) = Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Env -> Pred -> Pred
substPred (forall a. Var a -> Env -> Env
removeVar Var a
x Env
env) Pred
p
substPred :: Env -> Pred -> Pred
substPred :: Env -> Pred -> Pred
substPred Env
env = \case
ElemPred Bool
bool Term a
t NonEmpty a
xs -> forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool (forall a. Env -> Term a -> Term a
substTerm Env
env Term a
t) NonEmpty a
xs
GenHint Hint a
h Term a
t -> forall a. HasGenHint a => Hint a -> Term a -> Pred
GenHint Hint a
h (forall a. Env -> Term a -> Term a
substTerm Env
env Term a
t)
Subst Var a
x Term a
t Pred
p -> Env -> Pred -> Pred
substPred Env
env forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p
Assert Term Bool
t -> Term Bool -> Pred
Assert (forall a. Env -> Term a -> Term a
substTerm Env
env Term Bool
t)
Reifies Term b
t' Term a
t a -> b
f -> forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
Reifies (forall a. Env -> Term a -> Term a
substTerm Env
env Term b
t') (forall a. Env -> Term a -> Term a
substTerm Env
env Term a
t) a -> b
f
ForAll Term t
set Binder a
b -> forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll (forall a. Env -> Term a -> Term a
substTerm Env
env Term t
set) (forall a. Env -> Binder a -> Binder a
substBinder Env
env Binder a
b)
Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case (forall a. Env -> Term a -> Term a
substTerm Env
env Term (SumOver as)
t) (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (forall {k1} {k2} (f :: k1 -> *) (a :: k1) (g :: k2 -> *) (b :: k2).
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted forall a b. (a -> b) -> a -> b
$ forall a. Env -> Binder a -> Binder a
substBinder Env
env) List (Weighted Binder) as
bs)
When Term Bool
b Pred
p -> HasSpec Bool => Term Bool -> Pred -> Pred
When (forall a. Env -> Term a -> Term a
substTerm Env
env Term Bool
b) (Env -> Pred -> Pred
substPred Env
env Pred
p)
DependsOn Term a
x Term b
y -> forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn (forall a. Env -> Term a -> Term a
substTerm Env
env Term a
x) (forall a. Env -> Term a -> Term a
substTerm Env
env Term b
y)
Pred
TruePred -> Pred
TruePred
FalsePred NonEmpty String
es -> NonEmpty String -> Pred
FalsePred NonEmpty String
es
And [Pred]
ps -> forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Env -> Pred -> Pred
substPred Env
env forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (\forall b. Term b -> b
eval -> (forall b. Term b -> b) -> GE a
k forall a b. (a -> b) -> a -> b
$ forall b. Term b -> b
eval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Env -> Term a -> Term a
substTerm Env
env) (forall a. Env -> Binder a -> Binder a
substBinder Env
env Binder a
b)
Let Term a
t Binder a
b -> forall a. Term a -> Binder a -> Pred
Let (forall a. Env -> Term a -> Term a
substTerm Env
env Term a
t) (forall a. Env -> Binder a -> Binder a
substBinder Env
env Binder a
b)
Monitor (forall b. Term b -> b) -> Property -> Property
m -> ((forall b. Term b -> b) -> Property -> Property) -> Pred
Monitor (forall b. Term b -> b) -> Property -> Property
m
Explain NonEmpty String
es Pred
p -> NonEmpty String -> Pred -> Pred
Explain NonEmpty String
es forall a b. (a -> b) -> a -> b
$ Env -> Pred -> Pred
substPred Env
env Pred
p
unBind :: a -> Binder a -> Pred
unBind :: forall a. a -> Binder a -> Pred
unBind a
a (Var a
x :-> Pred
p) = Env -> Pred -> Pred
substPred (forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var a
x a
a) Pred
p
data Name where
Name :: HasSpec a => Var a -> Name
deriving instance Show Name
instance Eq Name where
Name Var a
v == :: Name -> Name -> Bool
== Name Var a
v' = forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
v Var a
v'
instance Pretty (Var a) where
pretty :: forall ann. Var a -> Doc ann
pretty = forall a. IsString a => String -> a
fromString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show
instance Pretty Name where
pretty :: forall ann. Name -> Doc ann
pretty (Name Var a
v) = forall a ann. Pretty a => a -> Doc ann
pretty Var a
v
instance Ord Name where
compare :: Name -> Name -> Ordering
compare (Name Var a
v) (Name Var a
v') = forall a. Ord a => a -> a -> Ordering
compare (forall a. Var a -> Int
nameOf Var a
v, forall a. Typeable a => a -> TypeRep
typeOf Var a
v) (forall a. Var a -> Int
nameOf Var a
v', forall a. Typeable a => a -> TypeRep
typeOf Var a
v')
instance Rename Name where
rename :: forall x. Typeable x => Var x -> Var x -> Name -> Name
rename Var x
v Var x
v' (Name Var a
v'') = forall a. HasSpec a => Var a -> Name
Name forall a b. (a -> b) -> a -> b
$ forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Var a
v''
instance Rename (Term a) where
rename :: forall x. Typeable x => Var x -> Var x -> Term a -> Term a
rename Var x
v Var x
v'
| Var x
v forall a. Eq a => a -> a -> Bool
== Var x
v' = forall a. a -> a
id
| Bool
otherwise = \case
Lit a
l -> forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
l
V Var a
v'' -> forall a. HasSpec a => Var a -> Term a
V (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Var a
v'')
App t dom a
f List Term dom
a -> forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App t dom a
f (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' List Term dom
a)
instance Rename Pred where
rename :: forall x. Typeable x => Var x -> Var x -> Pred -> Pred
rename Var x
v Var x
v'
| Var x
v forall a. Eq a => a -> a -> Bool
== Var x
v' = forall a. a -> a
id
| Bool
otherwise = \case
ElemPred Bool
bool Term a
t NonEmpty a
xs -> forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term a
t) NonEmpty a
xs
GenHint Hint a
h Term a
t -> forall a. HasGenHint a => Hint a -> Term a -> Pred
GenHint Hint a
h (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term a
t)
Subst Var a
x Term a
t Pred
p -> forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p
And [Pred]
ps -> [Pred] -> Pred
And (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' [Pred]
ps)
Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (\forall b. Term b -> b
eval -> (forall b. Term b -> b) -> GE a
k forall a b. (a -> b) -> a -> b
$ forall b. Term b -> b
eval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v') (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Binder a
b)
Let Term a
t Binder a
b -> forall a. Term a -> Binder a -> Pred
Let (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term a
t) (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Binder a
b)
Reifies Term b
t' Term a
t a -> b
f -> forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
Reifies (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term b
t') (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term a
t) a -> b
f
Assert Term Bool
t -> Term Bool -> Pred
Assert (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term Bool
t)
DependsOn Term a
x Term b
y -> forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term a
x) (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term b
y)
ForAll Term t
set Binder a
b -> forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term t
set) (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Binder a
b)
Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term (SumOver as)
t) (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' List (Weighted Binder) as
bs)
When Term Bool
b Pred
p -> HasSpec Bool => Term Bool -> Pred -> Pred
When (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term Bool
b) (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Pred
p)
Pred
TruePred -> Pred
TruePred
FalsePred NonEmpty String
es -> NonEmpty String -> Pred
FalsePred NonEmpty String
es
Monitor (forall b. Term b -> b) -> Property -> Property
m -> ((forall b. Term b -> b) -> Property -> Property) -> Pred
Monitor (forall b. Term b -> b) -> Property -> Property
m
Explain NonEmpty String
es Pred
p -> NonEmpty String -> Pred -> Pred
Explain NonEmpty String
es (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Pred
p)
instance Rename (Binder a) where
rename :: forall x. Typeable x => Var x -> Var x -> Binder a -> Binder a
rename Var x
v Var x
v' (Var a
va :-> Pred
psa) = Var a
va' forall a. HasSpec a => Var a -> Pred -> Binder a
:-> forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Pred
psa'
where
(Var a
va', Pred
psa') = forall a t.
(Typeable a, Rename t) =>
Var a -> t -> Set Int -> (Var a, t)
freshen Var a
va Pred
psa (forall a. Ord a => [a] -> Set a
Set.fromList [forall a. Var a -> Int
nameOf Var x
v, forall a. Var a -> Int
nameOf Var x
v'] forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => a -> Set a -> Set a
Set.delete (forall a. Var a -> Int
nameOf Var a
va) (forall t. HasVariables t => t -> Set Int
freeVarNames Pred
psa))
instance Rename (f a) => Rename (Weighted f a) where
rename :: forall x.
Typeable x =>
Var x -> Var x -> Weighted f a -> Weighted f a
rename Var x
v Var x
v' (Weighted Maybe Int
w f a
t) = forall {k} (f :: k -> *) (a :: k). Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
w (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' f a
t)
fromLits :: List Term as -> Maybe (List Value as)
fromLits :: forall (as :: [*]). List Term as -> Maybe (List Value as)
fromLits = forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (as :: [k]).
Applicative m =>
(forall (a :: k). f a -> m (g a)) -> List f as -> m (List g as)
mapMList forall a. Term a -> Maybe (Value a)
fromLit
fromLit :: Term a -> Maybe (Value a)
fromLit :: forall a. Term a -> Maybe (Value a)
fromLit (Lit a
l) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> Value a
Value a
l
fromLit Term a
_ = forall a. Maybe a
Nothing
isLit :: Term a -> Bool
isLit :: forall a. Term a -> Bool
isLit = forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Term a -> Maybe (Value a)
fromLit
name :: String -> Term a -> Term a
name :: forall a. String -> Term a -> Term a
name String
nh (V (Var Int
i String
_)) = forall a. HasSpec a => Var a -> Term a
V (forall a. Int -> String -> Var a
Var Int
i String
nh)
name String
_ Term a
_ = forall a. HasCallStack => String -> a
error String
"applying name to non-var thing! Shame on you!"
named :: String -> Term a -> Term a
named :: forall a. String -> Term a -> Term a
named String
nh t :: Term a
t@(V (Var Int
i String
x)) = if String
x forall a. Eq a => a -> a -> Bool
/= String
"v" then Term a
t else forall a. HasSpec a => Var a -> Term a
V (forall a. Int -> String -> Var a
Var Int
i String
nh)
named String
_ Term a
t = Term a
t
mkCase ::
HasSpec (SumOver as) => Term (SumOver as) -> List (Weighted Binder) as -> Pred
mkCase :: forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
mkCase Term (SumOver as)
tm List (Weighted Binder) as
cs
| Weighted Maybe Int
_ (Var a
x :-> Pred
p) :> List (Weighted Binder) as1
Nil <- List (Weighted Binder) as
cs = forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
Subst Var a
x Term (SumOver as)
tm Pred
p
| All -> Bool
Semigroup.getAll forall a b. (a -> b) -> a -> b
$ forall {k} b (f :: k -> *) (as :: [k]).
Monoid b =>
(forall (a :: k). f a -> b) -> List f as -> b
foldMapList forall {a}. Weighted Binder a -> All
isTrueBinder List (Weighted Binder) as
cs = Pred
TruePred
| All -> Bool
Semigroup.getAll forall a b. (a -> b) -> a -> b
$ forall {k} b (f :: k -> *) (as :: [k]).
Monoid b =>
(forall (a :: k). f a -> b) -> List f as -> b
foldMapList (forall {a}. Binder a -> All
isFalseBinder forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing) List (Weighted Binder) as
cs = NonEmpty String -> Pred
FalsePred (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"mkCase on all False")
| Lit SumOver as
a <- Term (SumOver as)
tm = forall (as :: [*]) r.
SumOver as
-> List Binder as
-> (forall a. HasSpec a => Var a -> a -> Pred -> r)
-> r
runCaseOn SumOver as
a (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing List (Weighted Binder) as
cs) (\Var a
x a
val Pred
p -> Env -> Pred -> Pred
substPred (forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var a
x a
val) Pred
p)
| Bool
otherwise = forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case Term (SumOver as)
tm List (Weighted Binder) as
cs
where
isTrueBinder :: Weighted Binder a -> All
isTrueBinder (Weighted Maybe Int
Nothing (Var a
_ :-> Pred
TruePred)) = Bool -> All
Semigroup.All Bool
True
isTrueBinder Weighted Binder a
_ = Bool -> All
Semigroup.All Bool
False
isFalseBinder :: Binder a -> All
isFalseBinder (Var a
_ :-> FalsePred {}) = Bool -> All
Semigroup.All Bool
True
isFalseBinder Binder a
_ = Bool -> All
Semigroup.All Bool
False
runCaseOn ::
SumOver as ->
List Binder as ->
(forall a. HasSpec a => Var a -> a -> Pred -> r) ->
r
runCaseOn :: forall (as :: [*]) r.
SumOver as
-> List Binder as
-> (forall a. HasSpec a => Var a -> a -> Pred -> r)
-> r
runCaseOn SumOver as
_ List Binder as
Nil forall a. HasSpec a => Var a -> a -> Pred -> r
_ = forall a. HasCallStack => String -> a
error String
"The impossible happened in runCaseOn"
runCaseOn SumOver as
a ((Var a
x :-> Pred
ps) :> List Binder as1
Nil) forall a. HasSpec a => Var a -> a -> Pred -> r
f = forall a. HasSpec a => Var a -> a -> Pred -> r
f Var a
x SumOver as
a Pred
ps
runCaseOn SumOver as
s ((Var a
x :-> Pred
ps) :> bs :: List Binder as1
bs@(Binder a
_ :> List Binder as1
_)) forall a. HasSpec a => Var a -> a -> Pred -> r
f = case SumOver as
s of
SumLeft a
a -> forall a. HasSpec a => Var a -> a -> Pred -> r
f Var a
x a
a Pred
ps
SumRight SumOver (a : as1)
a -> forall (as :: [*]) r.
SumOver as
-> List Binder as
-> (forall a. HasSpec a => Var a -> a -> Pred -> r)
-> r
runCaseOn SumOver (a : as1)
a List Binder as1
bs forall a. HasSpec a => Var a -> a -> Pred -> r
f
letSubexpressionElimination :: HasSpec Bool => Pred -> Pred
letSubexpressionElimination :: HasSpec Bool => Pred -> Pred
letSubexpressionElimination = Subst -> Pred -> Pred
go []
where
adjustSub :: Var a -> Subst -> Subst
adjustSub Var a
x Subst
sub =
[ Var a
x' forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
t
| Var a
x' := Term a
t <- Subst
sub
, forall a. Maybe a -> Bool
isNothing forall a b. (a -> b) -> a -> b
$ forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var a
x'
,
Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Name
Name Var a
x forall a. HasVariables a => Name -> a -> Bool
`appearsIn` Term a
t
]
goBinder :: Subst -> Binder a -> Binder a
goBinder :: forall a. Subst -> Binder a -> Binder a
goBinder Subst
sub (Var a
x :-> Pred
p) = Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Subst -> Pred -> Pred
go (forall {a}. HasSpec a => Var a -> Subst -> Subst
adjustSub Var a
x Subst
sub) Pred
p
go :: Subst -> Pred -> Pred
go Subst
sub = \case
ElemPred Bool
bool Term a
t NonEmpty a
xs -> forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term a
t) NonEmpty a
xs
GenHint Hint a
h Term a
t -> forall a. HasGenHint a => Hint a -> Term a -> Pred
GenHint Hint a
h (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term a
t)
And [Pred]
ps -> [Pred] -> Pred
And (Subst -> Pred -> Pred
go Subst
sub forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
Let Term a
t (Var a
x :-> Pred
p) -> forall a. Term a -> Binder a -> Pred
Let Term a
t' (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Subst -> Pred -> Pred
go (Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
t' forall a. a -> [a] -> [a]
: Subst
sub') Pred
p)
where
t' :: Term a
t' = forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term a
t
sub' :: Subst
sub' = forall {a}. HasSpec a => Var a -> Subst -> Subst
adjustSub Var a
x Subst
sub
Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (forall b. Term b -> b) -> GE a
k (forall a. Subst -> Binder a -> Binder a
goBinder Subst
sub Binder a
b)
Subst Var a
x Term a
t Pred
p -> Subst -> Pred -> Pred
go Subst
sub (forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p)
Assert Term Bool
t -> Term Bool -> Pred
Assert (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term Bool
t)
Reifies Term b
t' Term a
t a -> b
f -> forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
Reifies (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term b
t') (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term a
t) a -> b
f
DependsOn Term a
t Term b
t' -> forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term a
t) (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term b
t')
ForAll Term t
t Binder a
b -> forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term t
t) (forall a. Subst -> Binder a -> Binder a
goBinder Subst
sub Binder a
b)
Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term (SumOver as)
t) (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (forall {k1} {k2} (f :: k1 -> *) (a :: k1) (g :: k2 -> *) (b :: k2).
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted forall a b. (a -> b) -> a -> b
$ forall a. Subst -> Binder a -> Binder a
goBinder Subst
sub) List (Weighted Binder) as
bs)
When Term Bool
b Pred
p -> HasSpec Bool => Term Bool -> Pred -> Pred
When (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term Bool
b) (Subst -> Pred -> Pred
go Subst
sub Pred
p)
Pred
TruePred -> Pred
TruePred
FalsePred NonEmpty String
es -> NonEmpty String -> Pred
FalsePred NonEmpty String
es
Monitor (forall b. Term b -> b) -> Property -> Property
m -> ((forall b. Term b -> b) -> Property -> Property) -> Pred
Monitor (forall b. Term b -> b) -> Property -> Property
m
Explain NonEmpty String
es Pred
p -> NonEmpty String -> Pred -> Pred
Explain NonEmpty String
es forall a b. (a -> b) -> a -> b
$ Subst -> Pred -> Pred
go Subst
sub Pred
p
letFloating :: Pred -> Pred
letFloating :: Pred -> Pred
letFloating = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pred] -> Pred -> [Pred]
go []
where
goBlock :: [Pred] -> [Pred] -> [Pred]
goBlock [Pred]
ctx [Pred]
ps = Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' (forall t. HasVariables t => t -> Set Int
freeVarNames [Pred]
ctx forall a. Semigroup a => a -> a -> a
<> forall t. HasVariables t => t -> Set Int
freeVarNames [Pred]
ps) [Pred]
ctx [Pred]
ps
goBlock' :: Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' Set Int
_ [Pred]
ctx [] = [Pred]
ctx
goBlock' Set Int
fvs [Pred]
ctx (Let Term a
t (Var a
x :-> Pred
p) : [Pred]
ps) =
[forall a. Term a -> Binder a -> Pred
Let Term a
t (Var a
x' forall a. HasSpec a => Var a -> Pred -> Binder a
:-> forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' (forall a. Ord a => a -> Set a -> Set a
Set.insert (forall a. Var a -> Int
nameOf Var a
x') Set Int
fvs) [Pred]
ctx (Pred
p' forall a. a -> [a] -> [a]
: [Pred]
ps)))]
where
(Var a
x', Pred
p') = forall a t.
(Typeable a, Rename t) =>
Var a -> t -> Set Int -> (Var a, t)
freshen Var a
x Pred
p Set Int
fvs
goBlock' Set Int
fvs [Pred]
ctx (And [Pred]
ps : [Pred]
ps') = Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' Set Int
fvs [Pred]
ctx ([Pred]
ps forall a. [a] -> [a] -> [a]
++ [Pred]
ps')
goBlock' Set Int
fvs [Pred]
ctx (Pred
p : [Pred]
ps) = Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' Set Int
fvs (Pred
p forall a. a -> [a] -> [a]
: [Pred]
ctx) [Pred]
ps
goExists ::
HasSpec a =>
[Pred] ->
(Binder a -> Pred) ->
Var a ->
Pred ->
[Pred]
goExists :: forall a.
HasSpec a =>
[Pred] -> (Binder a -> Pred) -> Var a -> Pred -> [Pred]
goExists [Pred]
ctx Binder a -> Pred
ex Var a
x (Let Term a
t (Var a
y :-> Pred
p))
| Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Name
Name Var a
x forall a. HasVariables a => Name -> a -> Bool
`appearsIn` Term a
t =
let (Var a
y', Pred
p') = forall a t.
(Typeable a, Rename t) =>
Var a -> t -> Set Int -> (Var a, t)
freshen Var a
y Pred
p (forall a. Ord a => a -> Set a -> Set a
Set.insert (forall a. Var a -> Int
nameOf Var a
x) forall a b. (a -> b) -> a -> b
$ forall t. HasVariables t => t -> Set Int
freeVarNames Pred
p forall a. Semigroup a => a -> a -> a
<> forall t. HasVariables t => t -> Set Int
freeVarNames Term a
t)
in [Pred] -> Pred -> [Pred]
go [Pred]
ctx (forall a. Term a -> Binder a -> Pred
Let Term a
t (Var a
y' forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Binder a -> Pred
ex (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
p')))
goExists [Pred]
ctx Binder a -> Pred
ex Var a
x Pred
p = Binder a -> Pred
ex (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
p) forall a. a -> [a] -> [a]
: [Pred]
ctx
pushExplain :: NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es (Let Term a
t (Var a
x :-> Pred
p)) = forall a. Term a -> Binder a -> Pred
Let Term a
t (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es Pred
p)
pushExplain NonEmpty String
es (And [Pred]
ps) = [Pred] -> Pred
And (NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
pushExplain NonEmpty String
es (Exists (forall b. Term b -> b) -> GE a
k (Var a
x :-> Pred
p)) =
forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (forall a.
((forall b. Term b -> b) -> GE a)
-> (forall b. Term b -> b) -> GE a
explainSemantics (forall b. Term b -> b) -> GE a
k) (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es Pred
p)
where
explainSemantics ::
forall a.
((forall b. Term b -> b) -> GE a) ->
(forall b. Term b -> b) ->
GE a
explainSemantics :: forall a.
((forall b. Term b -> b) -> GE a)
-> (forall b. Term b -> b) -> GE a
explainSemantics (forall b. Term b -> b) -> GE a
k2 forall b. Term b -> b
env = forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE NonEmpty String
es forall a b. (a -> b) -> a -> b
$ (forall b. Term b -> b) -> GE a
k2 forall b. Term b -> b
env
pushExplain NonEmpty String
es (When Term Bool
b Pred
p) = HasSpec Bool => Term Bool -> Pred -> Pred
When Term Bool
b (NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es Pred
p)
pushExplain NonEmpty String
es Pred
p = NonEmpty String -> Pred -> Pred
explanation NonEmpty String
es Pred
p
go :: [Pred] -> Pred -> [Pred]
go [Pred]
ctx = \case
ElemPred Bool
bool Term a
t NonEmpty a
xs -> forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool Term a
t NonEmpty a
xs forall a. a -> [a] -> [a]
: [Pred]
ctx
And [Pred]
ps0 -> [Pred] -> [Pred] -> [Pred]
goBlock [Pred]
ctx (forall a b. (a -> b) -> [a] -> [b]
map Pred -> Pred
letFloating [Pred]
ps0)
Let Term a
t (Var a
x :-> Pred
p) -> [Pred] -> [Pred] -> [Pred]
goBlock [Pred]
ctx [forall a. Term a -> Binder a -> Pred
Let Term a
t (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred -> Pred
letFloating Pred
p)]
Exists (forall b. Term b -> b) -> GE a
k (Var a
x :-> Pred
p) -> forall a.
HasSpec a =>
[Pred] -> (Binder a -> Pred) -> Var a -> Pred -> [Pred]
goExists [Pred]
ctx (forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (forall b. Term b -> b) -> GE a
k) Var a
x (Pred -> Pred
letFloating Pred
p)
Subst Var a
x Term a
t Pred
p -> [Pred] -> Pred -> [Pred]
go [Pred]
ctx (forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p)
Reifies Term b
t' Term a
t a -> b
f -> forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
Reifies Term b
t' Term a
t a -> b
f forall a. a -> [a] -> [a]
: [Pred]
ctx
Explain NonEmpty String
es Pred
p -> NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es Pred
p forall a. a -> [a] -> [a]
: [Pred]
ctx
ForAll Term t
t (Var a
x :-> Pred
p) -> forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll Term t
t (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred -> Pred
letFloating Pred
p) forall a. a -> [a] -> [a]
: [Pred]
ctx
Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case Term (SumOver as)
t (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (forall {k1} {k2} (f :: k1 -> *) (a :: k1) (g :: k2 -> *) (b :: k2).
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted (\(Var a
x :-> Pred
p) -> Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred -> Pred
letFloating Pred
p)) List (Weighted Binder) as
bs) forall a. a -> [a] -> [a]
: [Pred]
ctx
When Term Bool
b Pred
p -> HasSpec Bool => Term Bool -> Pred -> Pred
When Term Bool
b (Pred -> Pred
letFloating Pred
p) forall a. a -> [a] -> [a]
: [Pred]
ctx
Assert Term Bool
t -> Term Bool -> Pred
Assert Term Bool
t forall a. a -> [a] -> [a]
: [Pred]
ctx
GenHint Hint a
h Term a
t -> forall a. HasGenHint a => Hint a -> Term a -> Pred
GenHint Hint a
h Term a
t forall a. a -> [a] -> [a]
: [Pred]
ctx
DependsOn Term a
t Term b
t' -> forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn Term a
t Term b
t' forall a. a -> [a] -> [a]
: [Pred]
ctx
Pred
TruePred -> Pred
TruePred forall a. a -> [a] -> [a]
: [Pred]
ctx
FalsePred NonEmpty String
es -> NonEmpty String -> Pred
FalsePred NonEmpty String
es forall a. a -> [a] -> [a]
: [Pred]
ctx
Monitor (forall b. Term b -> b) -> Property -> Property
m -> ((forall b. Term b -> b) -> Property -> Property) -> Pred
Monitor (forall b. Term b -> b) -> Property -> Property
m forall a. a -> [a] -> [a]
: [Pred]
ctx
assertExplain ::
IsPred p =>
NE.NonEmpty String ->
p ->
Pred
assertExplain :: forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain NonEmpty String
nes p
p = NonEmpty String -> Pred -> Pred
Explain NonEmpty String
nes (forall p. IsPred p => p -> Pred
toPred p
p)
assert ::
IsPred p =>
p ->
Pred
assert :: forall p. IsPred p => p -> Pred
assert p
p = forall p. IsPred p => p -> Pred
toPred p
p
forAll ::
( Forallable t a
, HasSpec t
, HasSpec a
, IsPred p
) =>
Term t ->
(Term a -> p) ->
Pred
forAll :: forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term t
tm = forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
mkForAll Term t
tm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind
mkForAll ::
( Forallable t a
, HasSpec t
, HasSpec a
) =>
Term t ->
Binder a ->
Pred
mkForAll :: forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
mkForAll (Lit (forall t e. Forallable t e => t -> [e]
forAllToList -> [])) Binder a
_ = Pred
TruePred
mkForAll Term t
_ (Var a
_ :-> Pred
TruePred) = Pred
TruePred
mkForAll Term t
tm Binder a
binder = forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll Term t
tm Binder a
binder
exists ::
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) ->
(Term a -> p) ->
Pred
exists :: forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (forall b. Term b -> b) -> GE a
sem Term a -> p
k =
forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (forall b. Term b -> b) -> GE a
sem forall a b. (a -> b) -> a -> b
$ forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind Term a -> p
k
unsafeExists ::
forall a p.
(HasSpec a, IsPred p) =>
(Term a -> p) ->
Pred
unsafeExists :: forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists = forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
_ -> forall (m :: * -> *) a. MonadGenError m => String -> m a
fatalError String
"unsafeExists")
letBind ::
( HasSpec a
, IsPred p
) =>
Term a ->
(Term a -> p) ->
Pred
letBind :: forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind tm :: Term a
tm@V {} Term a -> p
body = forall p. IsPred p => p -> Pred
toPred (Term a -> p
body Term a
tm)
letBind Term a
tm Term a -> p
body = forall a. Term a -> Binder a -> Pred
Let Term a
tm (forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind Term a -> p
body)
reify ::
( HasSpec a
, HasSpec b
, IsPred p
) =>
Term a ->
(a -> b) ->
(Term b -> p) ->
Pred
reify :: forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term a
t a -> b
f Term b -> p
body =
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ a -> b
f (forall b. Term b -> b
eval Term a
t)) forall a b. (a -> b) -> a -> b
$ \Term b
x ->
[ forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
reifies Term b
x Term a
t a -> b
f
, NonEmpty String -> Pred -> Pred
Explain (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"reify " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term a
t forall a. [a] -> [a] -> [a]
++ String
" somef $")) forall a b. (a -> b) -> a -> b
$ forall p. IsPred p => p -> Pred
toPred (Term b -> p
body Term b
x)
]
assertReified :: (HasSpec Bool, HasSpec a) => Term a -> (a -> Bool) -> Pred
assertReified :: forall a.
(HasSpec Bool, HasSpec a) =>
Term a -> (a -> Bool) -> Pred
assertReified Term a
t a -> Bool
f =
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term a
t a -> Bool
f forall p. IsPred p => p -> Pred
assert
explanation :: NE.NonEmpty String -> Pred -> Pred
explanation :: NonEmpty String -> Pred -> Pred
explanation NonEmpty String
_ p :: Pred
p@DependsOn {} = Pred
p
explanation NonEmpty String
_ Pred
TruePred = Pred
TruePred
explanation NonEmpty String
es (FalsePred NonEmpty String
es') = NonEmpty String -> Pred
FalsePred (NonEmpty String
es forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es')
explanation NonEmpty String
es (Assert Term Bool
t) = NonEmpty String -> Pred -> Pred
Explain NonEmpty String
es forall a b. (a -> b) -> a -> b
$ Term Bool -> Pred
Assert Term Bool
t
explanation NonEmpty String
es Pred
p = NonEmpty String -> Pred -> Pred
Explain NonEmpty String
es Pred
p
monitor :: ((forall a. Term a -> a) -> Property -> Property) -> Pred
monitor :: ((forall b. Term b -> b) -> Property -> Property) -> Pred
monitor = ((forall b. Term b -> b) -> Property -> Property) -> Pred
Monitor
reifies :: (HasSpec a, HasSpec b) => Term b -> Term a -> (a -> b) -> Pred
reifies :: forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
reifies = forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
Reifies
dependsOn :: (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn :: forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn = forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn
lit :: HasSpec a => a -> Term a
lit :: forall a. HasSpec a => a -> Term a
lit = forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit
genHint :: forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint :: forall a. HasGenHint a => Hint a -> Term a -> Pred
genHint = forall a. HasGenHint a => Hint a -> Term a -> Pred
GenHint
envFromPred :: Env -> Pred -> GE Env
envFromPred :: Env -> Pred -> GE Env
envFromPred Env
env Pred
p = case Pred
p of
ElemPred Bool
_bool Term a
_term NonEmpty a
_xs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
Assert {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
DependsOn {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
Monitor {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
TruePred {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
FalsePred {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
GenHint {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
Reifies {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
ForAll {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
Case {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
When Term Bool
_ Pred
pp -> Env -> Pred -> GE Env
envFromPred Env
env Pred
pp
Subst Var a
x Term a
a Pred
pp -> Env -> Pred -> GE Env
envFromPred Env
env (forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
a Pred
pp)
Let Term a
t (Var a
x :-> Pred
pp) -> do
a
v <- forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term a
t
Env -> Pred -> GE Env
envFromPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
v Env
env) Pred
pp
Explain NonEmpty String
_ Pred
pp -> Env -> Pred -> GE Env
envFromPred Env
env Pred
pp
Exists (forall b. Term b -> b) -> GE a
c (Var a
x :-> Pred
pp) -> do
a
v <- (forall b. Term b -> b) -> GE a
c (forall a. GE a -> a
errorGE forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain String
"envFromPred: Exists" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env)
Env -> Pred -> GE Env
envFromPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
v Env
env) Pred
pp
And [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
And (Pred
pp : [Pred]
ps) -> do
Env
env' <- Env -> Pred -> GE Env
envFromPred Env
env Pred
pp
Env -> Pred -> GE Env
envFromPred Env
env' ([Pred] -> Pred
And [Pred]
ps)
runTermE :: forall a. Env -> Term a -> Either (NE.NonEmpty String) a
runTermE :: forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env = \case
Lit a
a -> forall a b. b -> Either a b
Right a
a
V Var a
v -> case forall a. Typeable a => Env -> Var a -> Maybe a
lookupEnv Env
env Var a
v of
Just a
a -> forall a b. b -> Either a b
Right a
a
Maybe a
Nothing -> forall a b. a -> Either a b
Left (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Couldn't find " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Var a
v forall a. [a] -> [a] -> [a]
++ String
" in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Env
env))
App t dom a
f (List Term dom
ts :: List Term dom) -> do
List Identity dom
vs <- forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (as :: [k]).
Applicative m =>
(forall (a :: k). f a -> m (g a)) -> List f as -> m (List g as)
mapMList (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env) List Term dom
ts
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
uncurryList_ forall a. Identity a -> a
runIdentity (forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t dom a
f) List Identity dom
vs
runTerm :: MonadGenError m => Env -> Term a -> m a
runTerm :: forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term a
x = case forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term a
x of
Left NonEmpty String
msgs -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE NonEmpty String
msgs
Right a
val -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
val
data SolverStage where
SolverStage ::
HasSpec a =>
{ ()
stageVar :: Var a
, SolverStage -> [Pred]
stagePreds :: [Pred]
, ()
stageSpec :: Specification a
} ->
SolverStage
instance Pretty SolverStage where
pretty :: forall ann. SolverStage -> Doc ann
pretty SolverStage {[Pred]
Var a
Specification a
stageSpec :: Specification a
stagePreds :: [Pred]
stageVar :: Var a
stageSpec :: ()
stagePreds :: SolverStage -> [Pred]
stageVar :: ()
..} =
forall a ann. Show a => a -> Doc ann
viaShow Var a
stageVar
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"<-"
forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [Doc ann] -> Doc ann
vsep'
( [forall a ann. Pretty a => a -> Doc ann
pretty Specification a
stageSpec | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Specification a -> Bool
isTrueSpec Specification a
stageSpec]
forall a. [a] -> [a] -> [a]
++ [Doc ann
"---" | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pred]
stagePreds, Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Specification a -> Bool
isTrueSpec Specification a
stageSpec]
forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [Pred]
stagePreds
)
data SolverPlan = SolverPlan
{ SolverPlan -> [SolverStage]
solverPlan :: [SolverStage]
, SolverPlan -> Graph Name
solverDependencies :: Graph Name
}
instance Pretty SolverPlan where
pretty :: forall ann. SolverPlan -> Doc ann
pretty SolverPlan {[SolverStage]
Graph Name
solverDependencies :: Graph Name
solverPlan :: [SolverStage]
solverDependencies :: SolverPlan -> Graph Name
solverPlan :: SolverPlan -> [SolverStage]
..} =
Doc ann
"\nSolverPlan"
forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [Doc ann] -> Doc ann
vsep'
[
Doc ann
"\nLinearization:" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [SolverStage] -> Doc ann
prettyLinear [SolverStage]
solverPlan
]
isTrueSpec :: Specification a -> Bool
isTrueSpec :: forall a. Specification a -> Bool
isTrueSpec Specification a
TrueSpec = Bool
True
isTrueSpec Specification a
_ = Bool
False
prettyLinear :: [SolverStage] -> Doc ann
prettyLinear :: forall ann. [SolverStage] -> Doc ann
prettyLinear = forall ann. [Doc ann] -> Doc ann
vsep' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty
regularize :: HasVariables t => Var a -> t -> Var a
regularize :: forall t a. HasVariables t => Var a -> t -> Var a
regularize Var a
v t
t =
case [forall a. Var a -> String
nameHint Var a
v' | Name Var a
v' <- forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall a. HasVariables a => a -> Set Name
freeVarSet t
t, forall a. Var a -> Int
nameOf Var a
v' forall a. Eq a => a -> a -> Bool
== forall a. Var a -> Int
nameOf Var a
v, forall a. Var a -> String
nameHint Var a
v' forall a. Eq a => a -> a -> Bool
/= String
"v"] of
[] -> Var a
v
String
nh : [String]
_ -> Var a
v {nameHint :: String
nameHint = String
nh}
regularizeBinder :: Binder a -> Binder a
regularizeBinder :: forall a. Binder a -> Binder a
regularizeBinder (Var a
x :-> Pred
p) = Var a
x' forall a. HasSpec a => Var a -> Pred -> Binder a
:-> forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x (forall a. HasSpec a => Var a -> Term a
V Var a
x') (Pred -> Pred
regularizeNamesPred Pred
p)
where
x' :: Var a
x' = forall t a. HasVariables t => Var a -> t -> Var a
regularize Var a
x Pred
p
regularizeNamesPred :: Pred -> Pred
regularizeNamesPred :: Pred -> Pred
regularizeNamesPred Pred
pred = case Pred
pred of
ElemPred {} -> Pred
pred
Monitor {} -> Pred
pred
And [Pred]
ps -> [Pred] -> Pred
And forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Pred -> Pred
regularizeNamesPred [Pred]
ps
Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (forall b. Term b -> b) -> GE a
k (forall a. Binder a -> Binder a
regularizeBinder Binder a
b)
Subst Var a
v Term a
t Pred
p -> Pred -> Pred
regularizeNamesPred (forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
v Term a
t Pred
p)
Let Term a
t Binder a
b -> forall a. Term a -> Binder a -> Pred
Let Term a
t (forall a. Binder a -> Binder a
regularizeBinder Binder a
b)
Assert {} -> Pred
pred
Reifies {} -> Pred
pred
DependsOn {} -> Pred
pred
ForAll Term t
t Binder a
b -> forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll Term t
t (forall a. Binder a -> Binder a
regularizeBinder Binder a
b)
Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case Term (SumOver as)
t (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (forall {k1} {k2} (f :: k1 -> *) (a :: k1) (g :: k2 -> *) (b :: k2).
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted forall a. Binder a -> Binder a
regularizeBinder) List (Weighted Binder) as
bs)
When Term Bool
b Pred
p' -> HasSpec Bool => Term Bool -> Pred -> Pred
When Term Bool
b (Pred -> Pred
regularizeNamesPred Pred
p')
GenHint {} -> Pred
pred
TruePred {} -> Pred
pred
FalsePred {} -> Pred
pred
Explain NonEmpty String
es Pred
p' -> NonEmpty String -> Pred -> Pred
Explain NonEmpty String
es (Pred -> Pred
regularizeNamesPred Pred
p')
regularizeNames :: Specification a -> Specification a
regularizeNames :: forall a. Specification a -> Specification a
regularizeNames (ExplainSpec [String]
es Specification a
x) = forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (forall a. Specification a -> Specification a
regularizeNames Specification a
x)
regularizeNames (SuspendedSpec Var a
x Pred
p) =
forall a. HasSpec a => Var a -> Pred -> Specification a
SuspendedSpec Var a
x' Pred
p'
where
Var a
x' :-> Pred
p' = forall a. Binder a -> Binder a
regularizeBinder (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
p)
regularizeNames Specification a
spec = Specification a
spec