{-# 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 #-}
-- Rename instances
{-# OPTIONS_GHC -Wno-orphans #-}

-- | This module contains operations and tranformations on Syntax, Term, Pred, etc.
--    1) Computing Free Variables
--    2) Substitution
--    3) Renaming
--    4) internal helper functions
--    5) Syntacic only transformations
module Constrained.Syntax where

import Constrained.AbstractSyntax
import Constrained.Base (
  Binder,
  Forallable,
  HasGenHint,
  HasSpec,
  Hint,
  HintF (..),
  IsPred,
  Pred,
  Specification,
  Term,
  bind,
  explainSpecOpt,
  forAllToList,
  toPred,
 )
import Constrained.Core (
  Rename (rename),
  Value (..),
  Var (..),
  eqVar,
  freshen,
  unValue,
 )
import Constrained.Env (
  Env,
  extendEnv,
  lookupEnv,
  removeVar,
  singletonEnv,
 )
import Constrained.FunctionSymbol
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 Constrained.PrettyUtils
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)

-- ==========================================================
-- Variables
-- ==========================================================

mkNamed :: String -> TH.Q TH.Pat
mkNamed :: String -> Q Pat
mkNamed String
x =
  Pat -> Q Pat
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat -> Q Pat) -> Pat -> Q Pat
forall a b. (a -> b) -> a -> b
$
    Exp -> Pat -> Pat
TH.ViewP (Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE (Name -> Exp) -> Name -> Exp
forall a b. (a -> b) -> a -> b
$ String -> Name
TH.mkName String
"name") (Lit -> Exp
TH.LitE (Lit -> Exp) -> Lit -> Exp
forall a b. (a -> b) -> a -> b
$ String -> Lit
TH.StringL String
x)) (Name -> Pat
TH.VarP (Name -> Pat) -> Name -> Pat
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 =
  Exp -> Q Exp
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Q Exp) -> Exp -> Q Exp
forall a b. (a -> b) -> a -> b
$
    Exp -> Exp -> Exp
TH.AppE (Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE (Name -> Exp) -> Name -> Exp
forall a b. (a -> b) -> a -> b
$ String -> Name
TH.mkName String
"name") (Lit -> Exp
TH.LitE (Lit -> Exp) -> Lit -> Exp
forall a b. (a -> b) -> a -> b
$ String -> Lit
TH.StringL String
x)) (Name -> Exp
TH.VarE (Name -> Exp) -> Name -> Exp
forall a b. (a -> b) -> a -> b
$ String -> Name
TH.mkName String
x)

var :: TH.QuasiQuoter
var :: QuasiQuoter
var =
  TH.QuasiQuoter
    { -- Parses variables e.g. `constrained $ \ [var| x |] [var| y |] -> ...` from the strings " x " and " y "
      -- and replaces them with `name "x" -> x` and `name "y" -> y`
      quotePat :: String -> Q Pat
TH.quotePat = String -> Q Pat
mkNamed (String -> Q Pat) -> (String -> String) -> String -> Q Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
varName
    , -- Parses variables in expressions like `assert $ [var| x |] + 3 <. 10` and replaces them with `name "x" x`
      quoteExp :: String -> Q Exp
TH.quoteExp = String -> Q Exp
mkNamedExpr (String -> Q Exp) -> (String -> String) -> String -> Q Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
varName
    , quoteDec :: String -> Q [Dec]
TH.quoteDec = Q [Dec] -> String -> Q [Dec]
forall a b. a -> b -> a
const (Q [Dec] -> String -> Q [Dec]) -> Q [Dec] -> String -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ String -> Q [Dec]
forall a. String -> Q a
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 = Q Type -> String -> Q Type
forall a b. a -> b -> a
const (Q Type -> String -> Q Type) -> Q Type -> String -> Q Type
forall a b. (a -> b) -> a -> b
$ String -> Q Type
forall a. String -> Q a
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]
_ -> String -> String
forall a. String -> [a]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"expected a single var name"

-- ============================================================
-- 1) Free variables and variable names
-- ============================================================

freeVarNames :: forall t. HasVariables t => t -> Set Int
freeVarNames :: forall t. HasVariables t => t -> Set Int
freeVarNames = (Name -> Int) -> Set Name -> Set Int
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (\(Name Var a
v) -> Var a -> Int
forall a. Var a -> Int
nameOf Var a
v) (Set Name -> Set Int) -> (t -> Set Name) -> t -> Set Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Set Name
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
(Int -> FreeVars -> String -> String)
-> (FreeVars -> String)
-> ([FreeVars] -> String -> String)
-> Show FreeVars
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> FreeVars -> String -> String
showsPrec :: Int -> FreeVars -> String -> String
$cshow :: FreeVars -> String
show :: FreeVars -> String
$cshowList :: [FreeVars] -> String -> String
showList :: [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 (Map Name Int -> FreeVars) -> Map Name Int -> FreeVars
forall a b. (a -> b) -> a -> b
$ Map Name Int -> Set Name -> Map Name Int
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) = Name -> Map Name Int -> Bool
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) = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
0 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ Name -> Map Name Int -> Maybe Int
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 (Map Name Int -> FreeVars) -> Map Name Int -> FreeVars
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Int) -> Map Name Int -> Map Name Int -> Map Name Int
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Int -> Int -> Int
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 Map Name Int
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 (Map Name Int -> FreeVars) -> Map Name Int -> FreeVars
forall a b. (a -> b) -> a -> b
$ Name -> Int -> Map Name Int
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 (Map Name Int -> FreeVars) -> Map Name Int -> FreeVars
forall a b. (a -> b) -> a -> b
$ (Name -> Map Name Int -> Map Name Int)
-> Map Name Int -> [Name] -> Map Name Int
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Name -> Map Name Int -> Map Name Int
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Map Name Int
m (t Name -> [Name]
forall a. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t Name
remove)

class HasVariables a where
  freeVars :: a -> FreeVars
  freeVarSet :: a -> Set Name
  freeVarSet = Map Name Int -> Set Name
forall k a. Map k a -> Set k
Map.keysSet (Map Name Int -> Set Name) -> (a -> Map Name Int) -> a -> Set Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeVars -> Map Name Int
unFreeVars (FreeVars -> Map Name Int) -> (a -> FreeVars) -> a -> Map Name Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars
  countOf :: Name -> a -> Int
  countOf Name
n = Name -> FreeVars -> Int
count Name
n (FreeVars -> Int) -> (a -> FreeVars) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars
  appearsIn :: Name -> a -> Bool
  appearsIn Name
n = (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Int -> Bool) -> (a -> Int) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> FreeVars -> Int
count Name
n (FreeVars -> Int) -> (a -> FreeVars) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> FreeVars
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) = a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars a
a FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> b -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars b
b
  freeVarSet :: (a, b) -> Set Name
freeVarSet (a
a, b
b) = a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet a
a Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> b -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet b
b
  countOf :: Name -> (a, b) -> Int
countOf Name
n (a
a, b
b) = Name -> a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n a
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> b -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n b
b
  appearsIn :: Name -> (a, b) -> Bool
appearsIn Name
n (a
a, b
b) = Name -> a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n a
a Bool -> Bool -> Bool
|| Name -> b -> 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 = FreeVars
forall a. Monoid a => a
mempty
  freeVars (Term a
x :> List Term as1
xs) = Term a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Term a
x FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> List Term as1 -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars List Term as1
xs
  freeVarSet :: List Term as -> Set Name
freeVarSet List Term as
Nil = Set Name
forall a. Monoid a => a
mempty
  freeVarSet (Term a
x :> List Term as1
xs) = Term a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Term a
x Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> List Term as1 -> Set Name
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) = Name -> Term a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term a
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> List Term as1 -> Int
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) = Name -> Term a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term a
x Bool -> Bool -> Bool
|| Name -> List Term as1 -> 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 = Name -> Set Name
forall a. a -> Set a
Set.singleton
  countOf :: Name -> Name -> Int
countOf Name
n Name
n'
    | Name
n Name -> Name -> Bool
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n'

instance HasVariables (Term a) where
  freeVars :: Term a -> FreeVars
freeVars = \case
    Lit {} -> FreeVars
forall a. Monoid a => a
mempty
    V Var a
x -> Name -> FreeVars
freeVar (Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x)
    App t dom a
_ List Term dom
ts -> List Term dom -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars List Term dom
ts
  freeVarSet :: Term a -> Set Name
freeVarSet = \case
    Lit {} -> Set Name
forall a. Monoid a => a
mempty
    V Var a
x -> Name -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet (Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x)
    App t dom a
_ List Term dom
ts -> List Term dom -> Set Name
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 -> Name -> Name -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n (Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x)
    App t dom a
_ List Term dom
ts -> Name -> List Term dom -> Int
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 -> Name -> Name -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n (Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x)
    App t dom a
_ List Term dom
ts -> Name -> List Term dom -> Bool
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
_ TermD Deps a
t NonEmpty a
_ -> TermD Deps a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars TermD Deps a
t
    GenHint HintD Deps a
_ TermD Deps a
t -> TermD Deps a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars TermD Deps a
t
    Subst Var a
x TermD Deps a
t Pred
p -> TermD Deps a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars TermD Deps a
t FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> Pred -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Pred
p FreeVars -> [Name] -> FreeVars
forall (t :: * -> *). Foldable t => FreeVars -> t Name -> FreeVars
`without` [Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x]
    And [Pred]
ps -> (Pred -> FreeVars) -> [Pred] -> FreeVars
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Pred -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars [Pred]
ps
    Let TermD Deps a
t BinderD Deps a
b -> TermD Deps a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars TermD Deps a
t FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> BinderD Deps a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars BinderD Deps a
b
    Exists (forall b. TermD Deps b -> b) -> GE a
_ BinderD Deps a
b -> BinderD Deps a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars BinderD Deps a
b
    Assert TermD Deps Bool
t -> TermD Deps Bool -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars TermD Deps Bool
t
    Reifies TermD Deps b
t' TermD Deps a
t a -> b
_ -> TermD Deps b -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars TermD Deps b
t' FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> TermD Deps a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars TermD Deps a
t
    DependsOn TermD Deps a
x TermD Deps b
y -> TermD Deps a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars TermD Deps a
x FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> TermD Deps b -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars TermD Deps b
y
    ForAll TermD Deps t
set BinderD Deps e
b -> TermD Deps t -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars TermD Deps t
set FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> BinderD Deps e -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars BinderD Deps e
b
    Case TermD Deps (SumOver as)
t List (Weighted (BinderD Deps)) as
bs -> TermD Deps (SumOver as) -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars TermD Deps (SumOver as)
t FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> List (Weighted (BinderD Deps)) as -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars List (Weighted (BinderD Deps)) as
bs
    When TermD Deps Bool
b Pred
p -> TermD Deps Bool -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars TermD Deps Bool
b FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> Pred -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Pred
p
    Pred
TruePred -> FreeVars
forall a. Monoid a => a
mempty
    FalsePred NonEmpty String
_ -> FreeVars
forall a. Monoid a => a
mempty
    Monitor {} -> FreeVars
forall a. Monoid a => a
mempty
    Explain NonEmpty String
_ Pred
p -> Pred -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Pred
p
  freeVarSet :: Pred -> Set Name
freeVarSet = \case
    ElemPred Bool
_ TermD Deps a
t NonEmpty a
_ -> TermD Deps a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet TermD Deps a
t
    GenHint HintD Deps a
_ TermD Deps a
t -> TermD Deps a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet TermD Deps a
t
    Subst Var a
x TermD Deps a
t Pred
p -> TermD Deps a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet TermD Deps a
t Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
Set.delete (Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x) (Pred -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Pred
p)
    And [Pred]
ps -> (Pred -> Set Name) -> [Pred] -> Set Name
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Pred -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet [Pred]
ps
    Let TermD Deps a
t BinderD Deps a
b -> TermD Deps a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet TermD Deps a
t Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> BinderD Deps a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet BinderD Deps a
b
    Exists (forall b. TermD Deps b -> b) -> GE a
_ BinderD Deps a
b -> BinderD Deps a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet BinderD Deps a
b
    Assert TermD Deps Bool
t -> TermD Deps Bool -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet TermD Deps Bool
t
    Reifies TermD Deps b
t' TermD Deps a
t a -> b
_ -> TermD Deps b -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet TermD Deps b
t' Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> TermD Deps a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet TermD Deps a
t
    DependsOn TermD Deps a
x TermD Deps b
y -> TermD Deps a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet TermD Deps a
x Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> TermD Deps b -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet TermD Deps b
y
    ForAll TermD Deps t
set BinderD Deps e
b -> TermD Deps t -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet TermD Deps t
set Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> BinderD Deps e -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet BinderD Deps e
b
    Case TermD Deps (SumOver as)
t List (Weighted (BinderD Deps)) as
bs -> TermD Deps (SumOver as) -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet TermD Deps (SumOver as)
t Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> List (Weighted (BinderD Deps)) as -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet List (Weighted (BinderD Deps)) as
bs
    When TermD Deps Bool
b Pred
p -> TermD Deps Bool -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet TermD Deps Bool
b Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Pred -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Pred
p
    Explain NonEmpty String
_ Pred
p -> Pred -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Pred
p
    Pred
TruePred -> Set Name
forall a. Monoid a => a
mempty
    FalsePred NonEmpty String
_ -> Set Name
forall a. Monoid a => a
mempty
    Monitor {} -> Set Name
forall a. Monoid a => a
mempty
  countOf :: Name -> Pred -> Int
countOf Name
n = \case
    ElemPred Bool
_ TermD Deps a
t NonEmpty a
_ -> Name -> TermD Deps a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n TermD Deps a
t
    GenHint HintD Deps a
_ TermD Deps a
t -> Name -> TermD Deps a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n TermD Deps a
t
    Subst Var a
x TermD Deps a
t Pred
p
      | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x -> Name -> TermD Deps a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n TermD Deps a
t
      | Bool
otherwise -> Name -> TermD Deps a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n TermD Deps a
t Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> Pred -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Pred
p
    And [Pred]
ps -> [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (Pred -> Int) -> [Pred] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Pred -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n) [Pred]
ps
    Let TermD Deps a
t BinderD Deps a
b -> Name -> TermD Deps a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n TermD Deps a
t Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> BinderD Deps a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n BinderD Deps a
b
    Exists (forall b. TermD Deps b -> b) -> GE a
_ BinderD Deps a
b -> Name -> BinderD Deps a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n BinderD Deps a
b
    Assert TermD Deps Bool
t -> Name -> TermD Deps Bool -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n TermD Deps Bool
t
    Reifies TermD Deps b
t' TermD Deps a
t a -> b
_ -> Name -> TermD Deps b -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n TermD Deps b
t' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> TermD Deps a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n TermD Deps a
t
    DependsOn TermD Deps a
x TermD Deps b
y -> Name -> TermD Deps a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n TermD Deps a
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> TermD Deps b -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n TermD Deps b
y
    ForAll TermD Deps t
set BinderD Deps e
b -> Name -> TermD Deps t -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n TermD Deps t
set Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> BinderD Deps e -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n BinderD Deps e
b
    Case TermD Deps (SumOver as)
t List (Weighted (BinderD Deps)) as
bs -> Name -> TermD Deps (SumOver as) -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n TermD Deps (SumOver as)
t Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> List (Weighted (BinderD Deps)) as -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n List (Weighted (BinderD Deps)) as
bs
    When TermD Deps Bool
b Pred
p -> Name -> TermD Deps Bool -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n TermD Deps Bool
b Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> Pred -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Pred
p
    Explain NonEmpty String
_ Pred
p -> Name -> Pred -> Int
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
_ TermD Deps a
t NonEmpty a
_ -> Name -> TermD Deps a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n TermD Deps a
t
    GenHint HintD Deps a
_ TermD Deps a
t -> Name -> TermD Deps a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n TermD Deps a
t
    Subst Var a
x TermD Deps a
t Pred
p
      | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x -> Name -> TermD Deps a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n TermD Deps a
t
      | Bool
otherwise -> Name -> TermD Deps a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n TermD Deps a
t Bool -> Bool -> Bool
|| Name -> Pred -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Pred
p
    And [Pred]
ps -> (Pred -> Bool) -> [Pred] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> Pred -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n) [Pred]
ps
    Let TermD Deps a
t BinderD Deps a
b -> Name -> TermD Deps a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n TermD Deps a
t Bool -> Bool -> Bool
|| Name -> BinderD Deps a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n BinderD Deps a
b
    Exists (forall b. TermD Deps b -> b) -> GE a
_ BinderD Deps a
b -> Name -> BinderD Deps a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n BinderD Deps a
b
    Assert TermD Deps Bool
t -> Name -> TermD Deps Bool -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n TermD Deps Bool
t
    Reifies TermD Deps b
t' TermD Deps a
t a -> b
_ -> Name -> TermD Deps b -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n TermD Deps b
t' Bool -> Bool -> Bool
|| Name -> TermD Deps a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n TermD Deps a
t
    DependsOn TermD Deps a
x TermD Deps b
y -> Name -> TermD Deps a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n TermD Deps a
x Bool -> Bool -> Bool
|| Name -> TermD Deps b -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n TermD Deps b
y
    ForAll TermD Deps t
set BinderD Deps e
b -> Name -> TermD Deps t -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n TermD Deps t
set Bool -> Bool -> Bool
|| Name -> BinderD Deps e -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n BinderD Deps e
b
    Case TermD Deps (SumOver as)
t List (Weighted (BinderD Deps)) as
bs -> Name -> TermD Deps (SumOver as) -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n TermD Deps (SumOver as)
t Bool -> Bool -> Bool
|| Name -> List (Weighted (BinderD Deps)) as -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n List (Weighted (BinderD Deps)) as
bs
    When TermD Deps Bool
b Pred
p -> Name -> TermD Deps Bool -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n TermD Deps Bool
b Bool -> Bool -> Bool
|| Name -> Pred -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Pred
p
    Explain NonEmpty String
_ Pred
p -> Name -> Pred -> Bool
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) = Pred -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Pred
p FreeVars -> [Name] -> FreeVars
forall (t :: * -> *). Foldable t => FreeVars -> t Name -> FreeVars
`without` [Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x]
  freeVarSet :: Binder a -> Set Name
freeVarSet (Var a
x :-> Pred
p) = Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
Set.delete (Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x) (Pred -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Pred
p)
  countOf :: Name -> Binder a -> Int
countOf Name
n (Var a
x :-> Pred
p)
    | Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n = Int
0
    | Bool
otherwise = Name -> Pred -> Int
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)
    | Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n = Bool
False
    | Bool
otherwise = Name -> Pred -> Bool
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 = f a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars (f a -> FreeVars)
-> (Weighted f a -> f a) -> Weighted f a -> FreeVars
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Weighted f a -> f a
forall (f :: * -> *) a. Weighted f a -> f a
thing
  freeVarSet :: Weighted f a -> Set Name
freeVarSet = f a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet (f a -> Set Name)
-> (Weighted f a -> f a) -> Weighted f a -> Set Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Weighted f a -> f a
forall (f :: * -> *) a. Weighted f a -> f a
thing
  countOf :: Name -> Weighted f a -> Int
countOf Name
n = Name -> f a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n (f a -> Int) -> (Weighted f a -> f a) -> Weighted f a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Weighted f a -> f a
forall (f :: * -> *) a. Weighted f a -> f a
thing
  appearsIn :: Name -> Weighted f a -> Bool
appearsIn Name
n = Name -> f a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n (f a -> Bool) -> (Weighted f a -> f a) -> Weighted f a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Weighted f a -> f a
forall (f :: * -> *) a. Weighted f a -> f a
thing

instance HasVariables (List (Weighted Binder) as) where
  freeVars :: List (Weighted (BinderD Deps)) as -> FreeVars
freeVars List (Weighted (BinderD Deps)) as
Nil = FreeVars
forall a. Monoid a => a
mempty
  freeVars (Weighted (BinderD Deps) a
a :> List (Weighted (BinderD Deps)) as1
as) = Weighted (BinderD Deps) a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Weighted (BinderD Deps) a
a FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> List (Weighted (BinderD Deps)) as1 -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars List (Weighted (BinderD Deps)) as1
as
  freeVarSet :: List (Weighted (BinderD Deps)) as -> Set Name
freeVarSet List (Weighted (BinderD Deps)) as
Nil = Set Name
forall a. Monoid a => a
mempty
  freeVarSet (Weighted (BinderD Deps) a
a :> List (Weighted (BinderD Deps)) as1
as) = Weighted (BinderD Deps) a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Weighted (BinderD Deps) a
a Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> List (Weighted (BinderD Deps)) as1 -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet List (Weighted (BinderD Deps)) as1
as
  countOf :: Name -> List (Weighted (BinderD Deps)) as -> Int
countOf Name
_ List (Weighted (BinderD Deps)) as
Nil = Int
0
  countOf Name
n (Weighted (BinderD Deps) a
x :> List (Weighted (BinderD Deps)) as1
xs) = Name -> Weighted (BinderD Deps) a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Weighted (BinderD Deps) a
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> List (Weighted (BinderD Deps)) as1 -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n List (Weighted (BinderD Deps)) as1
xs
  appearsIn :: Name -> List (Weighted (BinderD Deps)) as -> Bool
appearsIn Name
_ List (Weighted (BinderD Deps)) as
Nil = Bool
False
  appearsIn Name
n (Weighted (BinderD Deps) a
x :> List (Weighted (BinderD Deps)) as1
xs) = Name -> Weighted (BinderD Deps) a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Weighted (BinderD Deps) a
x Bool -> Bool -> Bool
|| Name -> List (Weighted (BinderD Deps)) as1 -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n List (Weighted (BinderD Deps)) as1
xs

instance {-# OVERLAPPABLE #-} (Foldable t, HasVariables a) => HasVariables (t a) where
  freeVars :: t a -> FreeVars
freeVars = (a -> FreeVars) -> t a -> FreeVars
forall m a. Monoid m => (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars
  freeVarSet :: t a -> Set Name
freeVarSet = (a -> Set Name) -> t a -> Set Name
forall m a. Monoid m => (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet
  countOf :: Name -> t a -> Int
countOf Name
n = Sum Int -> Int
forall a. Sum a -> a
Monoid.getSum (Sum Int -> Int) -> (t a -> Sum Int) -> t a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Sum Int) -> t a -> Sum Int
forall m a. Monoid m => (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Int -> Sum Int
forall a. a -> Sum a
Monoid.Sum (Int -> Sum Int) -> (a -> Int) -> a -> Sum Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n)
  appearsIn :: Name -> t a -> Bool
appearsIn Name
n = (a -> Bool) -> t a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n)

instance HasVariables a => HasVariables (Set a) where
  freeVars :: Set a -> FreeVars
freeVars = (a -> FreeVars) -> Set a -> FreeVars
forall m a. Monoid m => (a -> m) -> Set a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars
  freeVarSet :: Set a -> Set Name
freeVarSet = (a -> Set Name) -> Set a -> Set Name
forall m a. Monoid m => (a -> m) -> Set a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet
  countOf :: Name -> Set a -> Int
countOf Name
n = Set Int -> Int
forall a. Num a => Set a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (Set Int -> Int) -> (Set a -> Set Int) -> Set a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Int) -> Set a -> Set Int
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Name -> a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n)
  appearsIn :: Name -> Set a -> Bool
appearsIn Name
n = (a -> Bool) -> Set a -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n)

-- =================================================================
-- 2) 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 :: 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
    -- TODO: what about multiple matches??
    Just Var a
x -> Var a -> Term a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V Var a
x
    Maybe (Var a)
Nothing -> case Term a
t of
      Lit a
a -> a -> Term a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
a
      V Var a
x -> Var a -> Term a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V Var a
x
      App t dom a
f List Term dom
ts -> t dom a -> List Term dom -> Term a
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps 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
forall (c :: * -> Constraint) (as :: [*]) (f :: * -> *)
       (g :: * -> *).
All c as =>
(forall a. c a => f a -> g a) -> List f as -> List g as
mapListC @HasSpec (Subst -> TermD Deps a -> TermD Deps a
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
_ = Maybe (Var a)
forall a. Maybe a
Nothing
    findMatch (Var a
x := Term a
t' : Subst
sub1) Term a
t1
      | Term a -> Term a -> Bool
forall deps a b. TermD deps a -> TermD deps 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'') <- (Var a, Term a) -> Maybe (Var a, Term a)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast (Var a
x, Term a
t')
      , Term a
t Term a -> Term a -> Bool
forall a. Eq a => a -> a -> Bool
== Term a
t'' =
          Var a -> Maybe (Var a)
forall a. a -> Maybe a
Just Var a
x'
      | Bool
otherwise = Subst -> Term a -> Maybe (Var a)
findMatch Subst
sub1 Term a
t1

-- ===================================================================

substituteTerm :: forall a. Subst -> Term a -> Term a
substituteTerm :: forall a. Subst -> Term a -> Term a
substituteTerm Subst
sub = \case
  Lit a
a -> a -> Term a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
a
  V Var a
x -> Subst -> Var a -> Term a
HasSpec a => Subst -> Var a -> Term a
substVar Subst
sub Var a
x
  App t dom a
f ((forall a. TermD Deps a -> TermD Deps a)
-> List Term dom -> List Term dom
forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (Subst -> TermD Deps a -> TermD Deps a
forall a. Subst -> Term a -> Term a
substituteTerm Subst
sub) -> (List Term dom
ts :: List Term dom)) ->
    case List Term dom -> Maybe (List Value dom)
forall (as :: [*]). List Term as -> Maybe (List Value as)
fromLits List Term dom
ts of
      Just List Value dom
vs -> a -> Term a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit ((forall a. Value a -> a) -> FunTy dom a -> List Value dom -> a
forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
forall (f :: * -> *) r.
(forall a. f a -> a) -> FunTy dom r -> List f dom -> r
uncurryList_ Value a -> a
forall a. Value a -> a
unValue (t dom a -> FunTy dom a
forall (d :: [*]) r. t d r -> FunTy d r
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)
_ -> t dom a -> List Term dom -> Term a
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps 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 = Var a -> Term a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V Var a
x
    substVar (Var a
y := Term a
t : Subst
sub1) Var a
x
      | Just a :~: a
Refl <- Var a -> Var a -> Maybe (a :~: a)
forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var a
y = Term a
Term a
t
      | Bool
otherwise = Subst -> Var a -> Term a
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 -> Term a -> Writer Any (Term a)
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term a -> Writer Any (Term a)) -> Term a -> Writer Any (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
a
  V Var a
x -> Subst -> Var a -> Writer Any (Term a)
HasSpec a => Subst -> Var a -> Writer Any (Term a)
substVar Subst
sub Var a
x
  App t dom a
f List Term dom
ts ->
    t dom a -> List Term dom -> Term a
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App t dom a
f (List Term dom -> Term a)
-> WriterT Any Identity (List Term dom) -> Writer Any (Term a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. TermD Deps a -> WriterT Any Identity (TermD Deps a))
-> List Term dom -> WriterT Any Identity (List Term dom)
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 (Subst -> TermD Deps a -> WriterT Any Identity (TermD Deps a)
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 = Term a -> Writer Any (Term a)
forall a. a -> WriterT Any Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term a -> Writer Any (Term a)) -> Term a -> Writer Any (Term a)
forall a b. (a -> b) -> a -> b
$ Var a -> Term a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V Var a
x
    substVar (Var a
y := Term a
t : Subst
sub1) Var a
x
      | Just a :~: a
Refl <- Var a -> Var a -> Maybe (a :~: a)
forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var a
y = Term a
Term a
t Term a -> WriterT Any Identity () -> Writer Any (Term a)
forall a b. a -> WriterT Any Identity b -> WriterT Any Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Any -> WriterT Any Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Bool -> Any
Any Bool
True)
      | Bool
otherwise = Subst -> Var a -> Writer Any (Term a)
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' Var b -> Pred -> BinderD Deps b
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Var a -> Term a -> Pred -> Pred
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') =
      Var b -> Pred -> Set Int -> (Var b, Pred)
forall a t.
(Typeable a, Rename t) =>
Var a -> t -> Set Int -> (Var a, t)
freshen Var b
y Pred
p (Int -> Set Int
forall a. a -> Set a
Set.singleton (Var a -> Int
forall a. Var a -> Int
nameOf Var a
x) Set Int -> Set Int -> Set Int
forall a. Semigroup a => a -> a -> a
<> Term a -> Set Int
forall t. HasVariables t => t -> Set Int
freeVarNames Term a
tm Set Int -> Set Int -> Set Int
forall a. Semigroup a => a -> a -> a
<> Int -> Set Int -> Set Int
forall a. Ord a => a -> Set a -> Set a
Set.delete (Var b -> Int
forall a. Var a -> Int
nameOf Var b
y) (Pred -> Set Int
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 TermD Deps a
t NonEmpty a
xs -> Bool -> TermD Deps a -> NonEmpty a -> Pred
forall deps a.
(HasSpecD deps a, Show a) =>
Bool -> TermD deps a -> NonEmpty a -> PredD deps
ElemPred Bool
bool (Subst -> TermD Deps a -> TermD Deps a
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] TermD Deps a
t) NonEmpty a
xs
  GenHint HintD Deps a
h TermD Deps a
t -> HintD Deps a -> TermD Deps a -> Pred
forall deps a.
(HasGenHintD deps a, Show a, Show (HintD deps a)) =>
HintD deps a -> TermD deps a -> PredD deps
GenHint HintD Deps a
h (Subst -> TermD Deps a -> TermD Deps a
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] TermD Deps a
t)
  Subst Var a
x' TermD Deps a
t Pred
p -> Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Var a -> TermD Deps a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x' TermD Deps a
t Pred
p
  Assert TermD Deps Bool
t -> TermD Deps Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Subst -> TermD Deps Bool -> TermD Deps Bool
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] TermD Deps Bool
t)
  And [Pred]
ps -> [Pred] -> Pred
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
  Exists (forall b. TermD Deps b -> b) -> GE a
k BinderD Deps a
b -> ((forall b. TermD Deps b -> b) -> GE a) -> BinderD Deps a -> Pred
forall deps a.
((forall b. TermD deps b -> b) -> GE a)
-> BinderD deps a -> PredD deps
Exists (\forall b. TermD Deps b -> b
eval -> (forall b. TermD Deps b -> b) -> GE a
k (TermD Deps b -> b
forall b. TermD Deps b -> b
eval (TermD Deps b -> b)
-> (TermD Deps b -> TermD Deps b) -> TermD Deps b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> TermD Deps b -> TermD Deps b
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm])) (Var a -> Term a -> BinderD Deps a -> BinderD Deps a
forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm BinderD Deps a
b)
  Let TermD Deps a
t BinderD Deps a
b -> TermD Deps a -> BinderD Deps a -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let (Subst -> TermD Deps a -> TermD Deps a
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] TermD Deps a
t) (Var a -> Term a -> BinderD Deps a -> BinderD Deps a
forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm BinderD Deps a
b)
  ForAll TermD Deps t
t BinderD Deps e
b -> TermD Deps t -> BinderD Deps e -> Pred
forall deps t e.
(ForallableD deps t e, HasSpecD deps t, HasSpecD deps e, Show t,
 Show e) =>
TermD deps t -> BinderD deps e -> PredD deps
ForAll (Subst -> TermD Deps t -> TermD Deps t
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] TermD Deps t
t) (Var a -> Term a -> BinderD Deps e -> BinderD Deps e
forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm BinderD Deps e
b)
  Case TermD Deps (SumOver as)
t List (Weighted (BinderD Deps)) as
bs -> TermD Deps (SumOver as)
-> List (Weighted (BinderD Deps)) as -> Pred
forall deps (as :: [*]).
(HasSpecD deps (SumOver as), Show (SumOver as)) =>
TermD deps (SumOver as)
-> List (Weighted (BinderD deps)) as -> PredD deps
Case (Subst -> TermD Deps (SumOver as) -> TermD Deps (SumOver as)
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] TermD Deps (SumOver as)
t) ((forall a. Weighted (BinderD Deps) a -> Weighted (BinderD Deps) a)
-> List (Weighted (BinderD Deps)) as
-> List (Weighted (BinderD Deps)) as
forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList ((BinderD Deps a -> BinderD Deps a)
-> Weighted (BinderD Deps) a -> Weighted (BinderD Deps) a
forall (f :: * -> *) a (g :: * -> *) b.
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted ((BinderD Deps a -> BinderD Deps a)
 -> Weighted (BinderD Deps) a -> Weighted (BinderD Deps) a)
-> (BinderD Deps a -> BinderD Deps a)
-> Weighted (BinderD Deps) a
-> Weighted (BinderD Deps) a
forall a b. (a -> b) -> a -> b
$ Var a -> Term a -> BinderD Deps a -> BinderD Deps a
forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm) List (Weighted (BinderD Deps)) as
bs)
  When TermD Deps Bool
b Pred
p -> TermD Deps Bool -> Pred -> Pred
forall deps. TermD deps Bool -> PredD deps -> PredD deps
When (Subst -> TermD Deps Bool -> TermD Deps Bool
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] TermD Deps Bool
b) (Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm Pred
p)
  Reifies TermD Deps b
t' TermD Deps a
t a -> b
f -> TermD Deps b -> TermD Deps a -> (a -> b) -> Pred
forall deps a b.
(HasSpecD deps a, HasSpecD deps b, Show a, Show b) =>
TermD deps b -> TermD deps a -> (a -> b) -> PredD deps
Reifies (Subst -> TermD Deps b -> TermD Deps b
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] TermD Deps b
t') (Subst -> TermD Deps a -> TermD Deps a
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] TermD Deps a
t) a -> b
f
  DependsOn TermD Deps a
t TermD Deps b
t' -> TermD Deps a -> TermD Deps b -> Pred
forall deps a b.
(HasSpecD deps a, HasSpecD deps b, Show a, Show b) =>
TermD deps a -> TermD deps b -> PredD deps
DependsOn (Subst -> TermD Deps a -> TermD Deps a
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] TermD Deps a
t) (Subst -> TermD Deps b -> TermD Deps b
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] TermD Deps b
t')
  Pred
TruePred -> Pred
forall deps. PredD deps
TruePred
  FalsePred NonEmpty String
es -> NonEmpty String -> Pred
forall deps. NonEmpty String -> PredD deps
FalsePred NonEmpty String
es
  Monitor (forall b. TermD Deps b -> b) -> Property -> Property
m -> ((forall b. TermD Deps b -> b) -> Property -> Property) -> Pred
forall deps.
((forall b. TermD deps b -> b) -> Property -> Property)
-> PredD deps
Monitor (\forall b. TermD Deps b -> b
eval -> (forall b. TermD Deps b -> b) -> Property -> Property
m (TermD Deps a -> a
forall b. TermD Deps b -> b
eval (TermD Deps a -> a)
-> (TermD Deps a -> TermD Deps a) -> TermD Deps a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> TermD Deps a -> TermD Deps a
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm]))
  Explain NonEmpty String
es Pred
p -> NonEmpty String -> Pred -> Pred
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain NonEmpty String
es (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm Pred
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 :: forall a. Env -> Term a -> Term a
substTerm Env
env = \case
  Lit a
a -> a -> Term a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
a
  V Var a
v
    | Just a
a <- Env -> Var a -> Maybe a
forall a. Typeable a => Env -> Var a -> Maybe a
lookupEnv Env
env Var a
v -> a -> Term a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
a
    | Bool
otherwise -> Var a -> Term a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V Var a
v
  App t dom a
f ((forall a. TermD Deps a -> TermD Deps a)
-> List Term dom -> List Term dom
forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (Env -> TermD Deps a -> TermD Deps a
forall a. Env -> Term a -> Term a
substTerm Env
env) -> List Term dom
ts) ->
    case List Term dom -> Maybe (List Value dom)
forall (as :: [*]). List Term as -> Maybe (List Value as)
fromLits List Term dom
ts of
      Just List Value dom
vs -> a -> Term a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit ((forall a. Value a -> a) -> FunTy dom a -> List Value dom -> a
forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
forall (f :: * -> *) r.
(forall a. f a -> a) -> FunTy dom r -> List f dom -> r
uncurryList_ Value a -> a
forall a. Value a -> a
unValue (t dom a -> FunTy dom a
forall (d :: [*]) r. t d r -> FunTy d r
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)
_ -> t dom a -> List Term dom -> Term a
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps 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 Var a -> Pred -> BinderD Deps a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Env -> Pred -> Pred
substPred (Var a -> Env -> Env
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 TermD Deps a
t NonEmpty a
xs -> Bool -> TermD Deps a -> NonEmpty a -> Pred
forall deps a.
(HasSpecD deps a, Show a) =>
Bool -> TermD deps a -> NonEmpty a -> PredD deps
ElemPred Bool
bool (Env -> TermD Deps a -> TermD Deps a
forall a. Env -> Term a -> Term a
substTerm Env
env TermD Deps a
t) NonEmpty a
xs
  GenHint HintD Deps a
h TermD Deps a
t -> HintD Deps a -> TermD Deps a -> Pred
forall deps a.
(HasGenHintD deps a, Show a, Show (HintD deps a)) =>
HintD deps a -> TermD deps a -> PredD deps
GenHint HintD Deps a
h (Env -> TermD Deps a -> TermD Deps a
forall a. Env -> Term a -> Term a
substTerm Env
env TermD Deps a
t)
  Subst Var a
x TermD Deps a
t Pred
p -> Env -> Pred -> Pred
substPred Env
env (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Var a -> TermD Deps a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x TermD Deps a
t Pred
p
  Assert TermD Deps Bool
t -> TermD Deps Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Env -> TermD Deps Bool -> TermD Deps Bool
forall a. Env -> Term a -> Term a
substTerm Env
env TermD Deps Bool
t)
  Reifies TermD Deps b
t' TermD Deps a
t a -> b
f -> TermD Deps b -> TermD Deps a -> (a -> b) -> Pred
forall deps a b.
(HasSpecD deps a, HasSpecD deps b, Show a, Show b) =>
TermD deps b -> TermD deps a -> (a -> b) -> PredD deps
Reifies (Env -> TermD Deps b -> TermD Deps b
forall a. Env -> Term a -> Term a
substTerm Env
env TermD Deps b
t') (Env -> TermD Deps a -> TermD Deps a
forall a. Env -> Term a -> Term a
substTerm Env
env TermD Deps a
t) a -> b
f
  ForAll TermD Deps t
set BinderD Deps e
b -> TermD Deps t -> BinderD Deps e -> Pred
forall deps t e.
(ForallableD deps t e, HasSpecD deps t, HasSpecD deps e, Show t,
 Show e) =>
TermD deps t -> BinderD deps e -> PredD deps
ForAll (Env -> TermD Deps t -> TermD Deps t
forall a. Env -> Term a -> Term a
substTerm Env
env TermD Deps t
set) (Env -> BinderD Deps e -> BinderD Deps e
forall a. Env -> Binder a -> Binder a
substBinder Env
env BinderD Deps e
b)
  Case TermD Deps (SumOver as)
t List (Weighted (BinderD Deps)) as
bs -> TermD Deps (SumOver as)
-> List (Weighted (BinderD Deps)) as -> Pred
forall deps (as :: [*]).
(HasSpecD deps (SumOver as), Show (SumOver as)) =>
TermD deps (SumOver as)
-> List (Weighted (BinderD deps)) as -> PredD deps
Case (Env -> TermD Deps (SumOver as) -> TermD Deps (SumOver as)
forall a. Env -> Term a -> Term a
substTerm Env
env TermD Deps (SumOver as)
t) ((forall a. Weighted (BinderD Deps) a -> Weighted (BinderD Deps) a)
-> List (Weighted (BinderD Deps)) as
-> List (Weighted (BinderD Deps)) as
forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList ((BinderD Deps a -> BinderD Deps a)
-> Weighted (BinderD Deps) a -> Weighted (BinderD Deps) a
forall (f :: * -> *) a (g :: * -> *) b.
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted ((BinderD Deps a -> BinderD Deps a)
 -> Weighted (BinderD Deps) a -> Weighted (BinderD Deps) a)
-> (BinderD Deps a -> BinderD Deps a)
-> Weighted (BinderD Deps) a
-> Weighted (BinderD Deps) a
forall a b. (a -> b) -> a -> b
$ Env -> BinderD Deps a -> BinderD Deps a
forall a. Env -> Binder a -> Binder a
substBinder Env
env) List (Weighted (BinderD Deps)) as
bs)
  When TermD Deps Bool
b Pred
p -> TermD Deps Bool -> Pred -> Pred
forall deps. TermD deps Bool -> PredD deps -> PredD deps
When (Env -> TermD Deps Bool -> TermD Deps Bool
forall a. Env -> Term a -> Term a
substTerm Env
env TermD Deps Bool
b) (Env -> Pred -> Pred
substPred Env
env Pred
p)
  DependsOn TermD Deps a
x TermD Deps b
y -> TermD Deps a -> TermD Deps b -> Pred
forall deps a b.
(HasSpecD deps a, HasSpecD deps b, Show a, Show b) =>
TermD deps a -> TermD deps b -> PredD deps
DependsOn (Env -> TermD Deps a -> TermD Deps a
forall a. Env -> Term a -> Term a
substTerm Env
env TermD Deps a
x) (Env -> TermD Deps b -> TermD Deps b
forall a. Env -> Term a -> Term a
substTerm Env
env TermD Deps b
y)
  Pred
TruePred -> Pred
forall deps. PredD deps
TruePred
  FalsePred NonEmpty String
es -> NonEmpty String -> Pred
forall deps. NonEmpty String -> PredD deps
FalsePred NonEmpty String
es
  And [Pred]
ps -> [Pred] -> Pred
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Env -> Pred -> Pred
substPred Env
env (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
  Exists (forall b. TermD Deps b -> b) -> GE a
k BinderD Deps a
b -> ((forall b. TermD Deps b -> b) -> GE a) -> BinderD Deps a -> Pred
forall deps a.
((forall b. TermD deps b -> b) -> GE a)
-> BinderD deps a -> PredD deps
Exists (\forall b. TermD Deps b -> b
eval -> (forall b. TermD Deps b -> b) -> GE a
k ((forall b. TermD Deps b -> b) -> GE a)
-> (forall b. TermD Deps b -> b) -> GE a
forall a b. (a -> b) -> a -> b
$ TermD Deps b -> b
forall b. TermD Deps b -> b
eval (TermD Deps b -> b)
-> (TermD Deps b -> TermD Deps b) -> TermD Deps b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> TermD Deps b -> TermD Deps b
forall a. Env -> Term a -> Term a
substTerm Env
env) (Env -> BinderD Deps a -> BinderD Deps a
forall a. Env -> Binder a -> Binder a
substBinder Env
env BinderD Deps a
b)
  Let TermD Deps a
t BinderD Deps a
b -> TermD Deps a -> BinderD Deps a -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let (Env -> TermD Deps a -> TermD Deps a
forall a. Env -> Term a -> Term a
substTerm Env
env TermD Deps a
t) (Env -> BinderD Deps a -> BinderD Deps a
forall a. Env -> Binder a -> Binder a
substBinder Env
env BinderD Deps a
b)
  Monitor (forall b. TermD Deps b -> b) -> Property -> Property
m -> ((forall b. TermD Deps b -> b) -> Property -> Property) -> Pred
forall deps.
((forall b. TermD deps b -> b) -> Property -> Property)
-> PredD deps
Monitor (forall b. TermD Deps b -> b) -> Property -> Property
m
  Explain NonEmpty String
es Pred
p -> NonEmpty String -> Pred -> Pred
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain NonEmpty String
es (Pred -> Pred) -> Pred -> Pred
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 (Var a -> a -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var a
x a
a) Pred
p

-- ==========================================================
-- Renaming
-- ============================================================

-- Name

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' = Maybe (a :~: a) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (a :~: a) -> Bool) -> Maybe (a :~: a) -> Bool
forall a b. (a -> b) -> a -> b
$ Var a -> Var a -> Maybe (a :~: a)
forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
v Var a
v'

-- Instances

instance Pretty (Var a) where
  pretty :: forall ann. Var a -> Doc ann
pretty = String -> Doc ann
forall a. IsString a => String -> a
fromString (String -> Doc ann) -> (Var a -> String) -> Var a -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var a -> String
forall a. Show a => a -> String
show

instance Pretty Name where
  pretty :: forall ann. Name -> Doc ann
pretty (Name Var a
v) = Var a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Var a -> Doc ann
pretty Var a
v

instance Ord Name where
  compare :: Name -> Name -> Ordering
compare (Name Var a
v) (Name Var a
v') = (Int, TypeRep) -> (Int, TypeRep) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Var a -> Int
forall a. Var a -> Int
nameOf Var a
v, Var a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Var a
v) (Var a -> Int
forall a. Var a -> Int
nameOf Var a
v', Var a -> TypeRep
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'') = Var a -> Name
forall a. HasSpec a => Var a -> Name
Name (Var a -> Name) -> Var a -> Name
forall a b. (a -> b) -> a -> b
$ Var x -> Var x -> Var a -> Var a
forall x. Typeable x => Var x -> Var x -> Var a -> Var a
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 Var x -> Var x -> Bool
forall a. Eq a => a -> a -> Bool
== Var x
v' = Term a -> Term a
forall a. a -> a
id
    | Bool
otherwise = \case
        Lit a
l -> a -> Term a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit a
l
        V Var a
v'' -> Var a -> Term a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V (Var x -> Var x -> Var a -> Var a
forall x. Typeable x => Var x -> Var x -> Var a -> Var a
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 -> t dom a -> List Term dom -> Term a
forall deps (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequiresD deps t dom a =>
t dom a -> List (TermD deps) dom -> TermD deps a
App t dom a
f (Var x -> Var x -> List Term dom -> List Term dom
forall x.
Typeable x =>
Var x -> Var x -> List Term dom -> List Term dom
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 Var x -> Var x -> Bool
forall a. Eq a => a -> a -> Bool
== Var x
v' = Pred -> Pred
forall a. a -> a
id
    | Bool
otherwise = \case
        ElemPred Bool
bool TermD Deps a
t NonEmpty a
xs -> Bool -> TermD Deps a -> NonEmpty a -> Pred
forall deps a.
(HasSpecD deps a, Show a) =>
Bool -> TermD deps a -> NonEmpty a -> PredD deps
ElemPred Bool
bool (Var x -> Var x -> TermD Deps a -> TermD Deps a
forall x.
Typeable x =>
Var x -> Var x -> TermD Deps a -> TermD Deps a
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' TermD Deps a
t) NonEmpty a
xs
        GenHint HintD Deps a
h TermD Deps a
t -> HintD Deps a -> TermD Deps a -> Pred
forall deps a.
(HasGenHintD deps a, Show a, Show (HintD deps a)) =>
HintD deps a -> TermD deps a -> PredD deps
GenHint HintD Deps a
h (Var x -> Var x -> TermD Deps a -> TermD Deps a
forall x.
Typeable x =>
Var x -> Var x -> TermD Deps a -> TermD Deps a
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' TermD Deps a
t)
        Subst Var a
x TermD Deps a
t Pred
p -> Var x -> Var x -> Pred -> Pred
forall x. Typeable x => Var x -> Var x -> Pred -> Pred
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Var a -> TermD Deps a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x TermD Deps a
t Pred
p
        And [Pred]
ps -> [Pred] -> Pred
forall deps. [PredD deps] -> PredD deps
And (Var x -> Var x -> [Pred] -> [Pred]
forall x. Typeable x => Var x -> Var x -> [Pred] -> [Pred]
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. TermD Deps b -> b) -> GE a
k BinderD Deps a
b -> ((forall b. TermD Deps b -> b) -> GE a) -> BinderD Deps a -> Pred
forall deps a.
((forall b. TermD deps b -> b) -> GE a)
-> BinderD deps a -> PredD deps
Exists (\forall b. TermD Deps b -> b
eval -> (forall b. TermD Deps b -> b) -> GE a
k ((forall b. TermD Deps b -> b) -> GE a)
-> (forall b. TermD Deps b -> b) -> GE a
forall a b. (a -> b) -> a -> b
$ TermD Deps b -> b
forall b. TermD Deps b -> b
eval (TermD Deps b -> b)
-> (TermD Deps b -> TermD Deps b) -> TermD Deps b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var x -> Var x -> TermD Deps b -> TermD Deps b
forall x.
Typeable x =>
Var x -> Var x -> TermD Deps b -> TermD Deps b
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v') (Var x -> Var x -> BinderD Deps a -> BinderD Deps a
forall x.
Typeable x =>
Var x -> Var x -> BinderD Deps a -> BinderD Deps a
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' BinderD Deps a
b)
        Let TermD Deps a
t BinderD Deps a
b -> TermD Deps a -> BinderD Deps a -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let (Var x -> Var x -> TermD Deps a -> TermD Deps a
forall x.
Typeable x =>
Var x -> Var x -> TermD Deps a -> TermD Deps a
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' TermD Deps a
t) (Var x -> Var x -> BinderD Deps a -> BinderD Deps a
forall x.
Typeable x =>
Var x -> Var x -> BinderD Deps a -> BinderD Deps a
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' BinderD Deps a
b)
        Reifies TermD Deps b
t' TermD Deps a
t a -> b
f -> TermD Deps b -> TermD Deps a -> (a -> b) -> Pred
forall deps a b.
(HasSpecD deps a, HasSpecD deps b, Show a, Show b) =>
TermD deps b -> TermD deps a -> (a -> b) -> PredD deps
Reifies (Var x -> Var x -> TermD Deps b -> TermD Deps b
forall x.
Typeable x =>
Var x -> Var x -> TermD Deps b -> TermD Deps b
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' TermD Deps b
t') (Var x -> Var x -> TermD Deps a -> TermD Deps a
forall x.
Typeable x =>
Var x -> Var x -> TermD Deps a -> TermD Deps a
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' TermD Deps a
t) a -> b
f
        Assert TermD Deps Bool
t -> TermD Deps Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Var x -> Var x -> TermD Deps Bool -> TermD Deps Bool
forall x.
Typeable x =>
Var x -> Var x -> TermD Deps Bool -> TermD Deps Bool
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' TermD Deps Bool
t)
        DependsOn TermD Deps a
x TermD Deps b
y -> TermD Deps a -> TermD Deps b -> Pred
forall deps a b.
(HasSpecD deps a, HasSpecD deps b, Show a, Show b) =>
TermD deps a -> TermD deps b -> PredD deps
DependsOn (Var x -> Var x -> TermD Deps a -> TermD Deps a
forall x.
Typeable x =>
Var x -> Var x -> TermD Deps a -> TermD Deps a
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' TermD Deps a
x) (Var x -> Var x -> TermD Deps b -> TermD Deps b
forall x.
Typeable x =>
Var x -> Var x -> TermD Deps b -> TermD Deps b
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' TermD Deps b
y)
        ForAll TermD Deps t
set BinderD Deps e
b -> TermD Deps t -> BinderD Deps e -> Pred
forall deps t e.
(ForallableD deps t e, HasSpecD deps t, HasSpecD deps e, Show t,
 Show e) =>
TermD deps t -> BinderD deps e -> PredD deps
ForAll (Var x -> Var x -> TermD Deps t -> TermD Deps t
forall x.
Typeable x =>
Var x -> Var x -> TermD Deps t -> TermD Deps t
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' TermD Deps t
set) (Var x -> Var x -> BinderD Deps e -> BinderD Deps e
forall x.
Typeable x =>
Var x -> Var x -> BinderD Deps e -> BinderD Deps e
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' BinderD Deps e
b)
        Case TermD Deps (SumOver as)
t List (Weighted (BinderD Deps)) as
bs -> TermD Deps (SumOver as)
-> List (Weighted (BinderD Deps)) as -> Pred
forall deps (as :: [*]).
(HasSpecD deps (SumOver as), Show (SumOver as)) =>
TermD deps (SumOver as)
-> List (Weighted (BinderD deps)) as -> PredD deps
Case (Var x
-> Var x -> TermD Deps (SumOver as) -> TermD Deps (SumOver as)
forall x.
Typeable x =>
Var x
-> Var x -> TermD Deps (SumOver as) -> TermD Deps (SumOver as)
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' TermD Deps (SumOver as)
t) (Var x
-> Var x
-> List (Weighted (BinderD Deps)) as
-> List (Weighted (BinderD Deps)) as
forall x.
Typeable x =>
Var x
-> Var x
-> List (Weighted (BinderD Deps)) as
-> List (Weighted (BinderD Deps)) as
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' List (Weighted (BinderD Deps)) as
bs)
        When TermD Deps Bool
b Pred
p -> TermD Deps Bool -> Pred -> Pred
forall deps. TermD deps Bool -> PredD deps -> PredD deps
When (Var x -> Var x -> TermD Deps Bool -> TermD Deps Bool
forall x.
Typeable x =>
Var x -> Var x -> TermD Deps Bool -> TermD Deps Bool
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' TermD Deps Bool
b) (Var x -> Var x -> Pred -> Pred
forall x. Typeable x => Var x -> Var x -> Pred -> Pred
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
forall deps. PredD deps
TruePred
        FalsePred NonEmpty String
es -> NonEmpty String -> Pred
forall deps. NonEmpty String -> PredD deps
FalsePred NonEmpty String
es
        Monitor (forall b. TermD Deps b -> b) -> Property -> Property
m -> ((forall b. TermD Deps b -> b) -> Property -> Property) -> Pred
forall deps.
((forall b. TermD deps b -> b) -> Property -> Property)
-> PredD deps
Monitor (forall b. TermD Deps b -> b) -> Property -> Property
m
        Explain NonEmpty String
es Pred
p -> NonEmpty String -> Pred -> Pred
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain NonEmpty String
es (Var x -> Var x -> Pred -> Pred
forall x. Typeable x => Var x -> Var x -> Pred -> Pred
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' Var a -> Pred -> Binder a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Var x -> Var x -> Pred -> Pred
forall x. Typeable x => Var x -> Var x -> Pred -> Pred
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') = Var a -> Pred -> Set Int -> (Var a, Pred)
forall a t.
(Typeable a, Rename t) =>
Var a -> t -> Set Int -> (Var a, t)
freshen Var a
va Pred
psa ([Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Var x -> Int
forall a. Var a -> Int
nameOf Var x
v, Var x -> Int
forall a. Var a -> Int
nameOf Var x
v'] Set Int -> Set Int -> Set Int
forall a. Semigroup a => a -> a -> a
<> Int -> Set Int -> Set Int
forall a. Ord a => a -> Set a -> Set a
Set.delete (Var a -> Int
forall a. Var a -> Int
nameOf Var a
va) (Pred -> Set Int
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) = Maybe Int -> f a -> Weighted f a
forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
w (Var x -> Var x -> f a -> f a
forall x. Typeable x => Var x -> Var x -> f a -> f a
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' f a
t)

-- ============================================================================
-- 4) Internals
-- ============================================================================

fromLits :: List Term as -> Maybe (List Value as)
fromLits :: forall (as :: [*]). List Term as -> Maybe (List Value as)
fromLits = (forall a. TermD Deps a -> Maybe (Value a))
-> List Term as -> Maybe (List Value as)
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 Term a -> Maybe (Value a)
forall a. TermD Deps a -> Maybe (Value a)
fromLit

fromLit :: Term a -> Maybe (Value a)
fromLit :: forall a. TermD Deps a -> Maybe (Value a)
fromLit (Lit a
l) = Value a -> Maybe (Value a)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value a -> Maybe (Value a)) -> Value a -> Maybe (Value a)
forall a b. (a -> b) -> a -> b
$ a -> Value a
forall a. Show a => a -> Value a
Value a
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 TermD Deps a
_ = Maybe (Value a)
forall a. Maybe a
Nothing

isLit :: Term a -> Bool
isLit :: forall a. Term a -> Bool
isLit = Maybe (Value a) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Value a) -> Bool)
-> (Term a -> Maybe (Value a)) -> Term a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term a -> Maybe (Value a)
forall a. TermD Deps 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
_)) = Var a -> TermD Deps a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V (Int -> String -> Var a
forall a. Int -> String -> Var a
Var Int
i String
nh)
name String
_ TermD Deps a
_ = String -> TermD Deps a
forall a. HasCallStack => String -> a
error String
"applying name to non-var thing! Shame on you!"

-- | Give a Term a nameHint, if its a Var, and doesn't already have one,
--  otherwise return the Term unchanged.
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 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"v" then Term a
t else Var a -> Term a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V (Int -> String -> Var a
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 (BinderD Deps)) as -> Pred
mkCase Term (SumOver as)
tm List (Weighted (BinderD Deps)) as
cs
  | Weighted Maybe Int
_ (Var a
x :-> Pred
p) :> List (Weighted (BinderD Deps)) as1
Nil <- List (Weighted (BinderD Deps)) as
cs = Var a -> TermD Deps a -> Pred -> Pred
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> TermD deps a -> PredD deps -> PredD deps
Subst Var a
x TermD Deps a
Term (SumOver as)
tm Pred
p
  -- TODO: all equal maybe?
  | All -> Bool
Semigroup.getAll (All -> Bool) -> All -> Bool
forall a b. (a -> b) -> a -> b
$ (forall a. Weighted (BinderD Deps) a -> All)
-> List (Weighted (BinderD Deps)) as -> All
forall {k} b (f :: k -> *) (as :: [k]).
Monoid b =>
(forall (a :: k). f a -> b) -> List f as -> b
foldMapList Weighted (BinderD Deps) a -> All
forall a. Weighted (BinderD Deps) a -> All
forall {deps} {a}. Weighted (BinderD deps) a -> All
isTrueBinder List (Weighted (BinderD Deps)) as
cs = Pred
forall deps. PredD deps
TruePred
  | All -> Bool
Semigroup.getAll (All -> Bool) -> All -> Bool
forall a b. (a -> b) -> a -> b
$ (forall a. Weighted (BinderD Deps) a -> All)
-> List (Weighted (BinderD Deps)) as -> All
forall {k} b (f :: k -> *) (as :: [k]).
Monoid b =>
(forall (a :: k). f a -> b) -> List f as -> b
foldMapList (BinderD Deps a -> All
forall {deps} {a}. BinderD deps a -> All
isFalseBinder (BinderD Deps a -> All)
-> (Weighted (BinderD Deps) a -> BinderD Deps a)
-> Weighted (BinderD Deps) a
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Weighted (BinderD Deps) a -> BinderD Deps a
forall (f :: * -> *) a. Weighted f a -> f a
thing) List (Weighted (BinderD Deps)) as
cs = NonEmpty String -> Pred
forall deps. NonEmpty String -> PredD deps
FalsePred (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"mkCase on all False")
  | Lit SumOver as
a <- Term (SumOver as)
tm = SumOver as
-> List (BinderD Deps) as
-> (forall a. (Typeable a, Show a) => Var a -> a -> Pred -> Pred)
-> Pred
forall (as :: [*]) r.
SumOver as
-> List (BinderD Deps) as
-> (forall a. (Typeable a, Show a) => Var a -> a -> Pred -> r)
-> r
runCaseOn SumOver as
a ((forall a. Weighted (BinderD Deps) a -> Binder a)
-> List (Weighted (BinderD Deps)) as -> List (BinderD Deps) as
forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList Weighted (BinderD Deps) a -> Binder a
forall a. Weighted (BinderD Deps) a -> Binder a
forall (f :: * -> *) a. Weighted f a -> f a
thing List (Weighted (BinderD Deps)) as
cs) (\Var a
x a
val Pred
p -> Env -> Pred -> Pred
substPred (Var a -> a -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var a
x a
val) Pred
p)
  | Bool
otherwise = Term (SumOver as) -> List (Weighted (BinderD Deps)) as -> Pred
forall deps (as :: [*]).
(HasSpecD deps (SumOver as), Show (SumOver as)) =>
TermD deps (SumOver as)
-> List (Weighted (BinderD deps)) as -> PredD deps
Case Term (SumOver as)
tm List (Weighted (BinderD Deps)) as
cs
  where
    isTrueBinder :: Weighted (BinderD deps) a -> All
isTrueBinder (Weighted Maybe Int
Nothing (Var a
_ :-> PredD deps
TruePred)) = Bool -> All
Semigroup.All Bool
True
    isTrueBinder Weighted (BinderD deps) a
_ = Bool -> All
Semigroup.All Bool
False

    isFalseBinder :: BinderD deps a -> All
isFalseBinder (Var a
_ :-> FalsePred {}) = Bool -> All
Semigroup.All Bool
True
    isFalseBinder BinderD deps a
_ = Bool -> All
Semigroup.All Bool
False

runCaseOn ::
  SumOver as ->
  List Binder as ->
  (forall a. (Typeable a, Show a) => Var a -> a -> Pred -> r) ->
  r
runCaseOn :: forall (as :: [*]) r.
SumOver as
-> List (BinderD Deps) as
-> (forall a. (Typeable a, Show a) => Var a -> a -> Pred -> r)
-> r
runCaseOn SumOver as
_ List (BinderD Deps) as
Nil forall a. (Typeable a, Show a) => Var a -> a -> Pred -> r
_ = String -> r
forall a. HasCallStack => String -> a
error String
"The impossible happened in runCaseOn"
runCaseOn SumOver as
a ((Var a
x :-> Pred
ps) :> List (BinderD Deps) as1
Nil) forall a. (Typeable a, Show a) => Var a -> a -> Pred -> r
f = Var a -> a -> Pred -> r
forall a. (Typeable a, Show a) => Var a -> a -> Pred -> r
f Var a
x a
SumOver as
a Pred
ps
runCaseOn SumOver as
s ((Var a
x :-> Pred
ps) :> bs :: List (BinderD Deps) as1
bs@(Binder a
_ :> List (BinderD Deps) as1
_)) forall a. (Typeable a, Show a) => Var a -> a -> Pred -> r
f = case SumOver as
s of
  SumLeft a
a -> Var a -> a -> Pred -> r
forall a. (Typeable a, Show a) => Var a -> a -> Pred -> r
f Var a
x a
a Pred
ps
  SumRight SumOver (a : as1)
a -> SumOver as1
-> List (BinderD Deps) as1
-> (forall a. (Typeable a, Show a) => Var a -> a -> Pred -> r)
-> r
forall (as :: [*]) r.
SumOver as
-> List (BinderD Deps) as
-> (forall a. (Typeable a, Show a) => Var a -> a -> Pred -> r)
-> r
runCaseOn SumOver as1
SumOver (a : as1)
a List (BinderD Deps) as1
bs Var a -> a -> Pred -> r
forall a. (Typeable a, Show a) => Var a -> a -> Pred -> r
f

-- ================================================
-- 5) Simple Syntax only transformation of terms.
-- There are other transformation that involve simplifying
-- but they are in module TheKnot
-- ==================================================

-- Common subexpression elimination but only on terms that are already let-bound.
letSubexpressionElimination :: HasSpec Bool => Pred -> Pred
letSubexpressionElimination :: HasSpec Bool => Pred -> Pred
letSubexpressionElimination = Subst -> Pred -> Pred
go []
  where
    adjustSub :: HasSpec a => Var a -> Subst -> Subst
    adjustSub :: forall a. HasSpec a => Var a -> Subst -> Subst
adjustSub Var a
x Subst
sub =
      [ Var a
x' Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
t
      | Var a
x' := Term a
t <- Subst
sub
      , Maybe (a :~: a) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (a :~: a) -> Bool) -> Maybe (a :~: a) -> Bool
forall a b. (a -> b) -> a -> b
$ Var a -> Var a -> Maybe (a :~: a)
forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var a
x'
      , -- TODO: possibly freshen the binder where
      -- `x` appears instead?
      Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x Name -> Term a -> Bool
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 Var a -> Pred -> BinderD Deps a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Subst -> Pred -> Pred
go (Var a -> Subst -> Subst
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 TermD Deps a
t NonEmpty a
xs -> Bool -> TermD Deps a -> NonEmpty a -> Pred
forall deps a.
(HasSpecD deps a, Show a) =>
Bool -> TermD deps a -> NonEmpty a -> PredD deps
ElemPred Bool
bool (Subst -> TermD Deps a -> TermD Deps a
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub TermD Deps a
t) NonEmpty a
xs
      GenHint HintD Deps a
h TermD Deps a
t -> HintD Deps a -> TermD Deps a -> Pred
forall deps a.
(HasGenHintD deps a, Show a, Show (HintD deps a)) =>
HintD deps a -> TermD deps a -> PredD deps
GenHint HintD Deps a
h (Subst -> TermD Deps a -> TermD Deps a
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub TermD Deps a
t)
      And [Pred]
ps -> [Pred] -> Pred
forall deps. [PredD deps] -> PredD deps
And (Subst -> Pred -> Pred
go Subst
sub (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
      Let TermD Deps a
t (Var a
x :-> Pred
p) -> TermD Deps a -> BinderD Deps a -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let TermD Deps a
t' (Var a
x Var a -> Pred -> BinderD Deps a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Subst -> Pred -> Pred
go (Var a
x Var a -> TermD Deps a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= TermD Deps a
t' SubstEntry -> Subst -> Subst
forall a. a -> [a] -> [a]
: Subst
sub') Pred
p)
        where
          t' :: TermD Deps a
t' = Subst -> TermD Deps a -> TermD Deps a
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub TermD Deps a
t
          sub' :: Subst
sub' = Var a -> Subst -> Subst
forall a. HasSpec a => Var a -> Subst -> Subst
adjustSub Var a
x Subst
sub
      Exists (forall b. TermD Deps b -> b) -> GE a
k BinderD Deps a
b -> ((forall b. TermD Deps b -> b) -> GE a) -> BinderD Deps a -> Pred
forall deps a.
((forall b. TermD deps b -> b) -> GE a)
-> BinderD deps a -> PredD deps
Exists (forall b. TermD Deps b -> b) -> GE a
k (Subst -> BinderD Deps a -> BinderD Deps a
forall a. Subst -> Binder a -> Binder a
goBinder Subst
sub BinderD Deps a
b)
      Subst Var a
x TermD Deps a
t Pred
p -> Subst -> Pred -> Pred
go Subst
sub (Var a -> TermD Deps a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x TermD Deps a
t Pred
p)
      Assert TermD Deps Bool
t -> TermD Deps Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert (Subst -> TermD Deps Bool -> TermD Deps Bool
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub TermD Deps Bool
t)
      Reifies TermD Deps b
t' TermD Deps a
t a -> b
f -> TermD Deps b -> TermD Deps a -> (a -> b) -> Pred
forall deps a b.
(HasSpecD deps a, HasSpecD deps b, Show a, Show b) =>
TermD deps b -> TermD deps a -> (a -> b) -> PredD deps
Reifies (Subst -> TermD Deps b -> TermD Deps b
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub TermD Deps b
t') (Subst -> TermD Deps a -> TermD Deps a
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub TermD Deps a
t) a -> b
f
      -- NOTE: this is a tricky case. One possible thing to do here is to keep the old `DependsOn t t'`
      -- and have the new DependsOn if `backwardsSubstitution` changed something. With this semantics you
      -- risk running into unintuitive behaviour if you have something like:
      -- ```
      -- let x = y + z in
      --  {y + z `dependsOn` w
      --   assert $ w <. y + 2
      --   ...}
      -- ```
      -- This will be rewritten as:
      -- ```
      -- let x = y + z in
      --  {z `dependsOn` w
      --   assert $ w <. y + 2
      --   ...}
      -- ```
      -- which changes the dependency order of `w` and `y`. However, fixing
      -- this behaviour in turn makes it more difficult to detect when
      -- variables are no longer used after being substituted away - which
      -- blocks some other optimizations. As we strongly encourage users not to
      -- use `letBind` in their own code most users will never encounter this issue
      -- so the tradeoff is probably worth it.
      DependsOn TermD Deps a
t TermD Deps b
t' -> TermD Deps a -> TermD Deps b -> Pred
forall deps a b.
(HasSpecD deps a, HasSpecD deps b, Show a, Show b) =>
TermD deps a -> TermD deps b -> PredD deps
DependsOn (Subst -> TermD Deps a -> TermD Deps a
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub TermD Deps a
t) (Subst -> TermD Deps b -> TermD Deps b
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub TermD Deps b
t')
      ForAll TermD Deps t
t BinderD Deps e
b -> TermD Deps t -> BinderD Deps e -> Pred
forall deps t e.
(ForallableD deps t e, HasSpecD deps t, HasSpecD deps e, Show t,
 Show e) =>
TermD deps t -> BinderD deps e -> PredD deps
ForAll (Subst -> TermD Deps t -> TermD Deps t
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub TermD Deps t
t) (Subst -> BinderD Deps e -> BinderD Deps e
forall a. Subst -> Binder a -> Binder a
goBinder Subst
sub BinderD Deps e
b)
      Case TermD Deps (SumOver as)
t List (Weighted (BinderD Deps)) as
bs -> TermD Deps (SumOver as)
-> List (Weighted (BinderD Deps)) as -> Pred
forall deps (as :: [*]).
(HasSpecD deps (SumOver as), Show (SumOver as)) =>
TermD deps (SumOver as)
-> List (Weighted (BinderD deps)) as -> PredD deps
Case (Subst -> TermD Deps (SumOver as) -> TermD Deps (SumOver as)
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub TermD Deps (SumOver as)
t) ((forall a. Weighted (BinderD Deps) a -> Weighted (BinderD Deps) a)
-> List (Weighted (BinderD Deps)) as
-> List (Weighted (BinderD Deps)) as
forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList ((BinderD Deps a -> BinderD Deps a)
-> Weighted (BinderD Deps) a -> Weighted (BinderD Deps) a
forall (f :: * -> *) a (g :: * -> *) b.
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted ((BinderD Deps a -> BinderD Deps a)
 -> Weighted (BinderD Deps) a -> Weighted (BinderD Deps) a)
-> (BinderD Deps a -> BinderD Deps a)
-> Weighted (BinderD Deps) a
-> Weighted (BinderD Deps) a
forall a b. (a -> b) -> a -> b
$ Subst -> BinderD Deps a -> BinderD Deps a
forall a. Subst -> Binder a -> Binder a
goBinder Subst
sub) List (Weighted (BinderD Deps)) as
bs)
      When TermD Deps Bool
b Pred
p -> TermD Deps Bool -> Pred -> Pred
forall deps. TermD deps Bool -> PredD deps -> PredD deps
When (Subst -> TermD Deps Bool -> TermD Deps Bool
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub TermD Deps Bool
b) (Subst -> Pred -> Pred
go Subst
sub Pred
p)
      Pred
TruePred -> Pred
forall deps. PredD deps
TruePred
      FalsePred NonEmpty String
es -> NonEmpty String -> Pred
forall deps. NonEmpty String -> PredD deps
FalsePred NonEmpty String
es
      Monitor (forall b. TermD Deps b -> b) -> Property -> Property
m -> ((forall b. TermD Deps b -> b) -> Property -> Property) -> Pred
forall deps.
((forall b. TermD deps b -> b) -> Property -> Property)
-> PredD deps
Monitor (forall b. TermD Deps b -> b) -> Property -> Property
m
      Explain NonEmpty String
es Pred
p -> NonEmpty String -> Pred -> Pred
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain NonEmpty String
es (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Subst -> Pred -> Pred
go Subst
sub Pred
p

-- 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 :: Pred -> Pred
letFloating = [Pred] -> Pred
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold ([Pred] -> Pred) -> (Pred -> [Pred]) -> Pred -> Pred
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' ([Pred] -> Set Int
forall t. HasVariables t => t -> Set Int
freeVarNames [Pred]
ctx Set Int -> Set Int -> Set Int
forall a. Semigroup a => a -> a -> a
<> [Pred] -> Set Int
forall t. HasVariables t => t -> Set Int
freeVarNames [Pred]
ps) [Pred]
ctx [Pred]
ps

    goBlock' :: Set Int -> [Pred] -> [Pred] -> [Pred]
    goBlock' :: Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' Set Int
_ [Pred]
ctx [] = [Pred]
ctx
    goBlock' Set Int
fvs [Pred]
ctx (Let TermD Deps a
t (Var a
x :-> Pred
p) : [Pred]
ps) =
      -- We can do `goBlock'` here because we've already done let floating
      -- on the inner `p`
      [TermD Deps a -> BinderD Deps a -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let TermD Deps a
t (Var a
x' Var a -> Pred -> BinderD Deps a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> [Pred] -> Pred
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' (Int -> Set Int -> Set Int
forall a. Ord a => a -> Set a -> Set a
Set.insert (Var a -> Int
forall a. Var a -> Int
nameOf Var a
x') Set Int
fvs) [Pred]
ctx (Pred
p' Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ps)))]
      where
        (Var a
x', Pred
p') = Var a -> Pred -> Set Int -> (Var a, Pred)
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 [Pred] -> [Pred] -> [Pred]
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 Pred -> [Pred] -> [Pred]
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 TermD Deps a
t (Var a
y :-> Pred
p))
      | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x Name -> TermD Deps a -> Bool
forall a. HasVariables a => Name -> a -> Bool
`appearsIn` TermD Deps a
t =
          let (Var a
y', Pred
p') = Var a -> Pred -> Set Int -> (Var a, Pred)
forall a t.
(Typeable a, Rename t) =>
Var a -> t -> Set Int -> (Var a, t)
freshen Var a
y Pred
p (Int -> Set Int -> Set Int
forall a. Ord a => a -> Set a -> Set a
Set.insert (Var a -> Int
forall a. Var a -> Int
nameOf Var a
x) (Set Int -> Set Int) -> Set Int -> Set Int
forall a b. (a -> b) -> a -> b
$ Pred -> Set Int
forall t. HasVariables t => t -> Set Int
freeVarNames Pred
p Set Int -> Set Int -> Set Int
forall a. Semigroup a => a -> a -> a
<> TermD Deps a -> Set Int
forall t. HasVariables t => t -> Set Int
freeVarNames TermD Deps a
t)
           in [Pred] -> Pred -> [Pred]
go [Pred]
ctx (TermD Deps a -> BinderD Deps a -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let TermD Deps a
t (Var a
y' Var a -> Pred -> BinderD Deps a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Binder a -> Pred
ex (Var a
x Var a -> Pred -> Binder a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Pred
p')))
    goExists [Pred]
ctx Binder a -> Pred
ex Var a
x Pred
p = Binder a -> Pred
ex (Var a
x Var a -> Pred -> Binder a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Pred
p) Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx

    pushExplain :: NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es (Let TermD Deps a
t (Var a
x :-> Pred
p)) = TermD Deps a -> BinderD Deps a -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let TermD Deps a
t (Var a
x Var a -> Pred -> BinderD Deps a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es Pred
p)
    pushExplain NonEmpty String
es (And [Pred]
ps) = [Pred] -> Pred
forall deps. [PredD deps] -> PredD deps
And (NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
    pushExplain NonEmpty String
es (Exists (forall b. TermD Deps b -> b) -> GE a
k (Var a
x :-> Pred
p)) =
      ((forall b. TermD Deps b -> b) -> GE a) -> BinderD Deps a -> Pred
forall deps a.
((forall b. TermD deps b -> b) -> GE a)
-> BinderD deps a -> PredD deps
Exists (((forall b. TermD Deps b -> b) -> GE a)
-> (forall b. TermD Deps b -> b) -> GE a
forall a.
((forall b. TermD Deps b -> b) -> GE a)
-> (forall b. TermD Deps b -> b) -> GE a
explainSemantics (forall b. TermD Deps b -> b) -> GE a
k) (Var a
x Var a -> Pred -> BinderD Deps a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es Pred
p)
      where
        -- TODO: Unfortunately this is necessary on ghc 8.10.7
        explainSemantics ::
          forall a.
          ((forall b. Term b -> b) -> GE a) ->
          (forall b. Term b -> b) ->
          GE a
        explainSemantics :: forall a.
((forall b. TermD Deps b -> b) -> GE a)
-> (forall b. TermD Deps b -> b) -> GE a
explainSemantics (forall b. TermD Deps b -> b) -> GE a
k2 forall b. TermD Deps b -> b
env = NonEmpty String -> GE a -> GE a
forall a. HasCallStack => NonEmpty String -> GE a -> GE a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE NonEmpty String
es (GE a -> GE a) -> GE a -> GE a
forall a b. (a -> b) -> a -> b
$ (forall b. TermD Deps b -> b) -> GE a
k2 Term b -> b
forall b. TermD Deps b -> b
env
    -- TODO: possibly one wants to have a `Term` level explanation in case
    -- the `b` propagates to ErrorSpec for some reason?
    pushExplain NonEmpty String
es (When TermD Deps Bool
b Pred
p) = TermD Deps Bool -> Pred -> Pred
forall deps. TermD deps Bool -> PredD deps -> PredD deps
When TermD Deps 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 TermD Deps a
t NonEmpty a
xs -> Bool -> TermD Deps a -> NonEmpty a -> Pred
forall deps a.
(HasSpecD deps a, Show a) =>
Bool -> TermD deps a -> NonEmpty a -> PredD deps
ElemPred Bool
bool TermD Deps a
t NonEmpty a
xs Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      And [Pred]
ps0 -> [Pred] -> [Pred] -> [Pred]
goBlock [Pred]
ctx ((Pred -> Pred) -> [Pred] -> [Pred]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> Pred
letFloating [Pred]
ps0)
      Let TermD Deps a
t (Var a
x :-> Pred
p) -> [Pred] -> [Pred] -> [Pred]
goBlock [Pred]
ctx [TermD Deps a -> BinderD Deps a -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let TermD Deps a
t (Var a
x Var a -> Pred -> BinderD Deps a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Pred -> Pred
letFloating Pred
p)]
      Exists (forall b. TermD Deps b -> b) -> GE a
k (Var a
x :-> Pred
p) -> [Pred] -> (BinderD Deps a -> Pred) -> Var a -> Pred -> [Pred]
forall a.
HasSpec a =>
[Pred] -> (Binder a -> Pred) -> Var a -> Pred -> [Pred]
goExists [Pred]
ctx (((forall b. TermD Deps b -> b) -> GE a) -> BinderD Deps a -> Pred
forall deps a.
((forall b. TermD deps b -> b) -> GE a)
-> BinderD deps a -> PredD deps
Exists (forall b. TermD Deps b -> b) -> GE a
k) Var a
x (Pred -> Pred
letFloating Pred
p)
      Subst Var a
x TermD Deps a
t Pred
p -> [Pred] -> Pred -> [Pred]
go [Pred]
ctx (Var a -> TermD Deps a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x TermD Deps a
t Pred
p)
      Reifies TermD Deps b
t' TermD Deps a
t a -> b
f -> TermD Deps b -> TermD Deps a -> (a -> b) -> Pred
forall deps a b.
(HasSpecD deps a, HasSpecD deps b, Show a, Show b) =>
TermD deps b -> TermD deps a -> (a -> b) -> PredD deps
Reifies TermD Deps b
t' TermD Deps a
t a -> b
f Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      Explain NonEmpty String
es Pred
p -> NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es Pred
p Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      -- TODO: float let through forall if possible
      ForAll TermD Deps t
t (Var e
x :-> Pred
p) -> TermD Deps t -> BinderD Deps e -> Pred
forall deps t e.
(ForallableD deps t e, HasSpecD deps t, HasSpecD deps e, Show t,
 Show e) =>
TermD deps t -> BinderD deps e -> PredD deps
ForAll TermD Deps t
t (Var e
x Var e -> Pred -> BinderD Deps e
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Pred -> Pred
letFloating Pred
p) Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      -- TODO: float let through the cases if possible
      Case TermD Deps (SumOver as)
t List (Weighted (BinderD Deps)) as
bs -> TermD Deps (SumOver as)
-> List (Weighted (BinderD Deps)) as -> Pred
forall deps (as :: [*]).
(HasSpecD deps (SumOver as), Show (SumOver as)) =>
TermD deps (SumOver as)
-> List (Weighted (BinderD deps)) as -> PredD deps
Case TermD Deps (SumOver as)
t ((forall a. Weighted (BinderD Deps) a -> Weighted (BinderD Deps) a)
-> List (Weighted (BinderD Deps)) as
-> List (Weighted (BinderD Deps)) as
forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList ((BinderD Deps a -> BinderD Deps a)
-> Weighted (BinderD Deps) a -> Weighted (BinderD Deps) a
forall (f :: * -> *) a (g :: * -> *) b.
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted (\(Var a
x :-> Pred
p) -> Var a
x Var a -> Pred -> BinderD Deps a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Pred -> Pred
letFloating Pred
p)) List (Weighted (BinderD Deps)) as
bs) Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      -- TODO: float let through if possible
      When TermD Deps Bool
b Pred
p -> TermD Deps Bool -> Pred -> Pred
forall deps. TermD deps Bool -> PredD deps -> PredD deps
When TermD Deps Bool
b (Pred -> Pred
letFloating Pred
p) Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      -- Boring cases
      Assert TermD Deps Bool
t -> TermD Deps Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert TermD Deps Bool
t Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      GenHint HintD Deps a
h TermD Deps a
t -> HintD Deps a -> TermD Deps a -> Pred
forall deps a.
(HasGenHintD deps a, Show a, Show (HintD deps a)) =>
HintD deps a -> TermD deps a -> PredD deps
GenHint HintD Deps a
h TermD Deps a
t Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      DependsOn TermD Deps a
t TermD Deps b
t' -> TermD Deps a -> TermD Deps b -> Pred
forall deps a b.
(HasSpecD deps a, HasSpecD deps b, Show a, Show b) =>
TermD deps a -> TermD deps b -> PredD deps
DependsOn TermD Deps a
t TermD Deps b
t' Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      Pred
TruePred -> Pred
forall deps. PredD deps
TruePred Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      FalsePred NonEmpty String
es -> NonEmpty String -> Pred
forall deps. NonEmpty String -> PredD deps
FalsePred NonEmpty String
es Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      Monitor (forall b. TermD Deps b -> b) -> Property -> Property
m -> ((forall b. TermD Deps b -> b) -> Property -> Property) -> Pred
forall deps.
((forall b. TermD deps b -> b) -> Property -> Property)
-> PredD deps
Monitor (forall b. TermD Deps b -> b) -> Property -> Property
m Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx

-- ========================================================================
-- For the API

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
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain NonEmpty String
nes (p -> Pred
forall p. IsPred p => p -> Pred
toPred p
p)

assert ::
  IsPred p =>
  p ->
  Pred
assert :: forall p. IsPred p => p -> Pred
assert p
p = p -> Pred
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 = Term t -> Binder a -> Pred
forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
mkForAll Term t
tm (Binder a -> Pred)
-> ((Term a -> p) -> Binder a) -> (Term a -> p) -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term a -> p) -> Binder a
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 (t -> [a]
forall t e. Forallable t e => t -> [e]
forAllToList -> [])) Binder a
_ = Pred
forall deps. PredD deps
TruePred
mkForAll TermD Deps t
_ (Var a
_ :-> Pred
TruePred) = Pred
forall deps. PredD deps
TruePred
mkForAll TermD Deps t
tm Binder a
binder = TermD Deps t -> Binder a -> Pred
forall deps t e.
(ForallableD deps t e, HasSpecD deps t, HasSpecD deps e, Show t,
 Show e) =>
TermD deps t -> BinderD deps e -> PredD deps
ForAll TermD Deps 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. TermD Deps b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (forall b. TermD Deps b -> b) -> GE a
sem Term a -> p
k =
  ((forall b. TermD Deps b -> b) -> GE a) -> BinderD Deps a -> Pred
forall deps a.
((forall b. TermD deps b -> b) -> GE a)
-> BinderD deps a -> PredD deps
Exists (forall b. TermD Deps b -> b) -> GE a
sem (BinderD Deps a -> Pred) -> BinderD Deps a -> Pred
forall a b. (a -> b) -> a -> b
$ (Term a -> p) -> BinderD Deps a
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 b. TermD Deps b -> b) -> GE a) -> (Term a -> p) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. TermD Deps b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. TermD Deps b -> b
_ -> String -> GE a
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 = p -> Pred
forall p. IsPred p => p -> Pred
toPred (Term a -> p
body Term a
tm)
letBind Term a
tm Term a -> p
body = Term a -> BinderD Deps a -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let Term a
tm ((Term a -> p) -> BinderD Deps a
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 b. TermD Deps b -> b) -> GE b)
-> (Term b -> [Pred]) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. TermD Deps b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. TermD Deps b -> b
eval -> b -> GE b
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> GE b) -> b -> GE b
forall a b. (a -> b) -> a -> b
$ a -> b
f (Term a -> a
forall b. TermD Deps b -> b
eval Term a
t)) ((Term b -> [Pred]) -> Pred) -> (Term b -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term b
x ->
    [ Term b -> Term a -> (a -> b) -> Pred
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
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"reify " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term a -> String
forall a. Show a => a -> String
show Term a
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" somef $")) (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ p -> Pred
forall p. IsPred p => p -> Pred
toPred (Term b -> p
body Term b
x)
    ]

-- | requires (HasSpec Bool)
assertReified :: (HasSpec Bool, HasSpec a) => Term a -> (a -> Bool) -> Pred
-- Note, it is necessary to introduce the extra variable from the `exists` here
-- to make things like `assertRealMultiple` work, if you don't have it then the
-- `reifies` isn't a defining constraint for anything any more.
assertReified :: forall a.
(HasSpec Bool, HasSpec a) =>
Term a -> (a -> Bool) -> Pred
assertReified Term a
t a -> Bool
f =
  Term a -> (a -> Bool) -> (TermD Deps Bool -> Pred) -> Pred
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 TermD Deps Bool -> Pred
forall p. IsPred p => p -> Pred
assert

-- | Wrap an 'Explain' around a Pred, unless there is a simpler form.
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
forall deps. PredD deps
TruePred
explanation NonEmpty String
es (FalsePred NonEmpty String
es') = NonEmpty String -> Pred
forall deps. NonEmpty String -> PredD deps
FalsePred (NonEmpty String
es NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es')
explanation NonEmpty String
es (Assert TermD Deps Bool
t) = NonEmpty String -> Pred -> Pred
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain NonEmpty String
es (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps Bool -> Pred
forall deps. TermD deps Bool -> PredD deps
Assert TermD Deps Bool
t
explanation NonEmpty String
es Pred
p = NonEmpty String -> Pred -> Pred
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain NonEmpty String
es Pred
p

-- | Add QuickCheck monitoring (e.g. 'Test.QuickCheck.collect' or 'Test.QuickCheck.counterexample')
--   to a predicate. To use the monitoring in a property call 'monitorSpec' on the 'Specification'
--   containing the monitoring and a value generated from the specification.
monitor :: ((forall a. Term a -> a) -> Property -> Property) -> Pred
monitor :: ((forall b. TermD Deps b -> b) -> Property -> Property) -> Pred
monitor = ((forall b. TermD Deps b -> b) -> Property -> Property) -> Pred
forall deps.
((forall b. TermD deps b -> b) -> Property -> Property)
-> PredD deps
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 = TermD Deps b -> TermD Deps a -> (a -> b) -> Pred
forall deps a b.
(HasSpecD deps a, HasSpecD deps b, Show a, Show b) =>
TermD deps b -> TermD deps a -> (a -> b) -> PredD deps
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 = TermD Deps a -> TermD Deps b -> Pred
forall deps a b.
(HasSpecD deps a, HasSpecD deps b, Show a, Show b) =>
TermD deps a -> TermD deps b -> PredD deps
DependsOn

-- lit :: (Typeable a, Eq a, Show a) => a -> Term a
lit :: HasSpec a => a -> Term a
lit :: forall a. HasSpec a => a -> Term a
lit = a -> TermD Deps a
forall a deps. (Typeable a, Eq a, Show a) => a -> TermD deps a
Lit

genHint :: forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint :: forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint = HintD Deps t -> Term t -> Pred
HintF t -> Term t -> Pred
forall deps a.
(HasGenHintD deps a, Show a, Show (HintD deps a)) =>
HintD deps a -> TermD deps a -> PredD deps
GenHint (HintF t -> Term t -> Pred)
-> (Hint t -> HintF t) -> Hint t -> Term t -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hint t -> HintF t
forall a. Hint a -> HintF a
HintF

-- ==============================================================================

-- Construct an environment for all variables that show up on the top level
-- (i.e. ones bound in `let` and `exists`) from an environment for all the free
-- variables in the pred. The environment you get out of this function is
-- _bigger_ than the environment you put in. From
-- ```
-- let y = x + 1 in let z = y + 1 in foo x y z
-- ```
-- and an environment with `{x -> 1}` you would get `{x -> 1, y -> 2, z -> 3}`
-- out.
envFromPred :: Env -> Pred -> GE Env
envFromPred :: Env -> Pred -> GE Env
envFromPred Env
env Pred
p = case Pred
p of
  ElemPred Bool
_bool TermD Deps a
_term NonEmpty a
_xs -> Env -> GE Env
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  -- NOTE: these don't bind anything
  Assert {} -> Env -> GE Env
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  DependsOn {} -> Env -> GE Env
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  Monitor {} -> Env -> GE Env
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  TruePred {} -> Env -> GE Env
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  FalsePred {} -> Env -> GE Env
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  GenHint {} -> Env -> GE Env
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  -- NOTE: this is ok because the variables either come from an `Exists`, a `Let`, or from
  -- the top level
  Reifies {} -> Env -> GE Env
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  -- NOTE: variables in here shouldn't escape to the top level
  ForAll {} -> Env -> GE Env
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  Case {} -> Env -> GE Env
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  -- These can introduce binders that show up in the plan
  When TermD Deps Bool
_ Pred
pp -> Env -> Pred -> GE Env
envFromPred Env
env Pred
pp
  Subst Var a
x TermD Deps a
a Pred
pp -> Env -> Pred -> GE Env
envFromPred Env
env (Var a -> TermD Deps a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x TermD Deps a
a Pred
pp)
  Let TermD Deps a
t (Var a
x :-> Pred
pp) -> do
    a
v <- Env -> TermD Deps a -> GE a
forall (m :: * -> *) deps a.
MonadGenError m =>
Env -> TermD deps a -> m a
runTerm Env
env TermD Deps a
t
    Env -> Pred -> GE Env
envFromPred (Var a -> a -> Env -> Env
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. TermD Deps b -> b) -> GE a
c (Var a
x :-> Pred
pp) -> do
    a
v <- (forall b. TermD Deps b -> b) -> GE a
c (GE b -> b
forall a. GE a -> a
errorGE (GE b -> b) -> (TermD Deps b -> GE b) -> TermD Deps b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> GE b -> GE b
forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain String
"envFromPred: Exists" (GE b -> GE b) -> (TermD Deps b -> GE b) -> TermD Deps b -> GE b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> TermD Deps b -> GE b
forall (m :: * -> *) deps a.
MonadGenError m =>
Env -> TermD deps a -> m a
runTerm Env
env)
    Env -> Pred -> GE Env
envFromPred (Var a -> a -> Env -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
v Env
env) Pred
pp
  And [] -> Env -> GE Env
forall a. a -> GE a
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
forall deps. [PredD deps] -> PredD deps
And [Pred]
ps)

-- ===============================================================================
-- Syntax for Solving : stages and plans

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
stageVar :: ()
stagePreds :: SolverStage -> [Pred]
stageSpec :: ()
stageVar :: Var a
stagePreds :: [Pred]
stageSpec :: Specification a
..} =
    Var a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Var a
stageVar
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"<-"
        Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
/> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep'
          ( [Specification a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Specification a -> Doc ann
pretty Specification a
stageSpec | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Specification a -> Bool
forall a. Specification a -> Bool
isTrueSpec Specification a
stageSpec]
              [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [Doc ann
"---" | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Pred] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pred]
stagePreds, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Specification a -> Bool
forall a. Specification a -> Bool
isTrueSpec Specification a
stageSpec]
              [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ (Pred -> Doc ann) -> [Pred] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Pred -> 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
solverPlan :: SolverPlan -> [SolverStage]
solverDependencies :: SolverPlan -> Graph Name
solverPlan :: [SolverStage]
solverDependencies :: Graph Name
..} =
    Doc ann
"\nSolverPlan"
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
/> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep'
        [ -- "\nDependencies:" /> pretty solverDependencies, -- Might be usefull someday
          Doc ann
"\nLinearization:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
/> [SolverStage] -> Doc ann
forall ann. [SolverStage] -> Doc ann
prettyLinear [SolverStage]
solverPlan
        ]

isTrueSpec :: Specification a -> Bool
isTrueSpec :: forall a. Specification a -> Bool
isTrueSpec SpecificationD Deps a
TrueSpec = Bool
True
isTrueSpec SpecificationD Deps a
_ = Bool
False

prettyLinear :: [SolverStage] -> Doc ann
prettyLinear :: forall ann. [SolverStage] -> Doc ann
prettyLinear = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep' ([Doc ann] -> Doc ann)
-> ([SolverStage] -> [Doc ann]) -> [SolverStage] -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SolverStage -> Doc ann) -> [SolverStage] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map SolverStage -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. SolverStage -> Doc ann
pretty

-- ==========================================
-- Regularizing

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 [Var a -> String
forall a. Var a -> String
nameHint Var a
v' | Name Var a
v' <- Set Name -> [Name]
forall a. Set a -> [a]
Set.toList (Set Name -> [Name]) -> Set Name -> [Name]
forall a b. (a -> b) -> a -> b
$ t -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet t
t, Var a -> Int
forall a. Var a -> Int
nameOf Var a
v' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Var a -> Int
forall a. Var a -> Int
nameOf Var a
v, Var a -> String
forall a. Var a -> String
nameHint Var a
v' String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"v"] of
    [] -> Var a
v
    String
nh : [String]
_ -> Var a
v {nameHint = nh}

regularizeBinder :: Binder a -> Binder a
regularizeBinder :: forall a. Binder a -> Binder a
regularizeBinder (Var a
x :-> Pred
p) = Var a
x' Var a -> Pred -> BinderD Deps a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x (Var a -> Term a
forall deps a.
(HasSpecD deps a, Typeable a) =>
Var a -> TermD deps a
V Var a
x') (Pred -> Pred
regularizeNamesPred Pred
p)
  where
    x' :: Var a
x' = Var a -> Pred -> Var a
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
forall deps. [PredD deps] -> PredD deps
And ([Pred] -> Pred) -> [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ (Pred -> Pred) -> [Pred] -> [Pred]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> Pred
regularizeNamesPred [Pred]
ps
  Exists (forall b. TermD Deps b -> b) -> GE a
k BinderD Deps a
b -> ((forall b. TermD Deps b -> b) -> GE a) -> BinderD Deps a -> Pred
forall deps a.
((forall b. TermD deps b -> b) -> GE a)
-> BinderD deps a -> PredD deps
Exists (forall b. TermD Deps b -> b) -> GE a
k (BinderD Deps a -> BinderD Deps a
forall a. Binder a -> Binder a
regularizeBinder BinderD Deps a
b)
  Subst Var a
v TermD Deps a
t Pred
p -> Pred -> Pred
regularizeNamesPred (Var a -> TermD Deps a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
v TermD Deps a
t Pred
p)
  Let TermD Deps a
t BinderD Deps a
b -> TermD Deps a -> BinderD Deps a -> Pred
forall deps a. TermD deps a -> BinderD deps a -> PredD deps
Let TermD Deps a
t (BinderD Deps a -> BinderD Deps a
forall a. Binder a -> Binder a
regularizeBinder BinderD Deps a
b)
  Assert {} -> Pred
pred
  Reifies {} -> Pred
pred
  DependsOn {} -> Pred
pred
  ForAll TermD Deps t
t BinderD Deps e
b -> TermD Deps t -> BinderD Deps e -> Pred
forall deps t e.
(ForallableD deps t e, HasSpecD deps t, HasSpecD deps e, Show t,
 Show e) =>
TermD deps t -> BinderD deps e -> PredD deps
ForAll TermD Deps t
t (BinderD Deps e -> BinderD Deps e
forall a. Binder a -> Binder a
regularizeBinder BinderD Deps e
b)
  Case TermD Deps (SumOver as)
t List (Weighted (BinderD Deps)) as
bs -> TermD Deps (SumOver as)
-> List (Weighted (BinderD Deps)) as -> Pred
forall deps (as :: [*]).
(HasSpecD deps (SumOver as), Show (SumOver as)) =>
TermD deps (SumOver as)
-> List (Weighted (BinderD deps)) as -> PredD deps
Case TermD Deps (SumOver as)
t ((forall a. Weighted (BinderD Deps) a -> Weighted (BinderD Deps) a)
-> List (Weighted (BinderD Deps)) as
-> List (Weighted (BinderD Deps)) as
forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList ((BinderD Deps a -> BinderD Deps a)
-> Weighted (BinderD Deps) a -> Weighted (BinderD Deps) a
forall (f :: * -> *) a (g :: * -> *) b.
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted BinderD Deps a -> BinderD Deps a
forall a. Binder a -> Binder a
regularizeBinder) List (Weighted (BinderD Deps)) as
bs)
  When TermD Deps Bool
b Pred
p' -> TermD Deps Bool -> Pred -> Pred
forall deps. TermD deps Bool -> PredD deps -> PredD deps
When TermD Deps 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
forall deps. NonEmpty String -> PredD deps -> PredD deps
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 SpecificationD Deps a
x) = [String] -> SpecificationD Deps a -> SpecificationD Deps a
forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (SpecificationD Deps a -> SpecificationD Deps a
forall a. Specification a -> Specification a
regularizeNames SpecificationD Deps a
x)
regularizeNames (SuspendedSpec Var a
x Pred
p) =
  Var a -> Pred -> SpecificationD Deps a
forall deps a.
HasSpecD deps a =>
Var a -> PredD deps -> SpecificationD deps a
SuspendedSpec Var a
x' Pred
p'
  where
    Var a
x' :-> Pred
p' = BinderD Deps a -> BinderD Deps a
forall a. Binder a -> Binder a
regularizeBinder (Var a
x Var a -> Pred -> BinderD Deps a
forall deps a.
(HasSpecD deps a, Show a) =>
Var a -> PredD deps -> BinderD deps a
:-> Pred
p)
regularizeNames SpecificationD Deps a
spec = SpecificationD Deps a
spec