{-# 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.Base (
  Binder (..),
  Forallable,
  HasGenHint,
  HasSpec,
  Hint,
  IsPred,
  Pred (..),
  Specification (..),
  Term (..),
  Weighted (..),
  bind,
  explainSpecOpt,
  forAllToList,
  mapWeighted,
  semantics,
  toPred,
  vsep',
  (/>),
 )
import Constrained.Core (
  Rename (rename),
  Value (..),
  Var (..),
  eqVar,
  freshen,
  unValue,
 )
import Constrained.Env (
  Env,
  extendEnv,
  lookupEnv,
  removeVar,
  singletonEnv,
 )
import Constrained.GenT (
  GE (..),
  MonadGenError (..),
  errorGE,
  explain,
  fatalError,
 )
import Constrained.Generic (
  Sum (..),
  SumOver,
 )
import Constrained.Graph (
  Graph (..),
 )
import Constrained.List (
  List (..),
  foldMapList,
  mapList,
  mapListC,
  mapMList,
  uncurryList_,
 )

import Control.Monad.Identity
import Control.Monad.Writer (Writer, tell)
import Data.Foldable (fold, toList)
import qualified Data.List.NonEmpty as NE
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (fromMaybe, isJust, isNothing)
import qualified Data.Monoid as Monoid
import Data.Orphans ()
import Data.Semigroup (Any (..))
import qualified Data.Semigroup as Semigroup
import Data.Set (Set)
import qualified Data.Set as Set
import Data.String (fromString)
import Data.Typeable
import qualified Language.Haskell.TH as TH
import qualified Language.Haskell.TH.Quote as TH
import Prettyprinter hiding (cat)
import Test.QuickCheck hiding (Args, Fun, Witness, forAll, witness)
import Prelude hiding (pred)

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

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

mkNamedExpr :: String -> TH.Q TH.Exp
mkNamedExpr :: String -> Q Exp
mkNamedExpr String
x =
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    Exp -> Exp -> Exp
TH.AppE (Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE forall a b. (a -> b) -> a -> b
$ String -> Name
TH.mkName String
"name") (Lit -> Exp
TH.LitE forall a b. (a -> b) -> a -> b
$ String -> Lit
TH.StringL String
x)) (Name -> Exp
TH.VarE forall a b. (a -> b) -> a -> b
$ String -> Name
TH.mkName String
x)

var :: TH.QuasiQuoter
var :: QuasiQuoter
var =
  TH.QuasiQuoter
    { -- 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 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
varName
    , quoteDec :: String -> Q [Dec]
TH.quoteDec = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"var should only be used at binding sites and in expressions"
    , quoteType :: String -> Q Type
TH.quoteType = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"var should only be used at binding sites and in expressions"
    }
  where
    varName :: String -> String
varName String
s = case String -> [String]
words String
s of
      [String
w] -> String
w
      [String]
_ -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"expected a single var name"

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

freeVarNames :: forall t. HasVariables t => t -> Set Int
freeVarNames :: forall t. HasVariables t => t -> Set Int
freeVarNames = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (\(Name Var a
v) -> forall a. Var a -> Int
nameOf Var a
v) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasVariables a => a -> Set Name
freeVarSet

newtype FreeVars = FreeVars {FreeVars -> Map Name Int
unFreeVars :: Map Name Int}
  deriving (Int -> FreeVars -> String -> String
[FreeVars] -> String -> String
FreeVars -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [FreeVars] -> String -> String
$cshowList :: [FreeVars] -> String -> String
show :: FreeVars -> String
$cshow :: FreeVars -> String
showsPrec :: Int -> FreeVars -> String -> String
$cshowsPrec :: Int -> FreeVars -> String -> String
Show)

restrictedTo :: FreeVars -> Set Name -> FreeVars
restrictedTo :: FreeVars -> Set Name -> FreeVars
restrictedTo (FreeVars Map Name Int
m) Set Name
nms = Map Name Int -> FreeVars
FreeVars forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map Name Int
m Set Name
nms

memberOf :: Name -> FreeVars -> Bool
memberOf :: Name -> FreeVars -> Bool
memberOf Name
n (FreeVars Map Name Int
m) = forall k a. Ord k => k -> Map k a -> Bool
Map.member Name
n Map Name Int
m

count :: Name -> FreeVars -> Int
count :: Name -> FreeVars -> Int
count Name
n (FreeVars Map Name Int
m) = forall a. a -> Maybe a -> a
fromMaybe Int
0 forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name Int
m

instance Semigroup FreeVars where
  FreeVars Map Name Int
fv <> :: FreeVars -> FreeVars -> FreeVars
<> FreeVars Map Name Int
fv' = Map Name Int -> FreeVars
FreeVars forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Num a => a -> a -> a
(+) Map Name Int
fv Map Name Int
fv'

instance Monoid FreeVars where
  mempty :: FreeVars
mempty = Map Name Int -> FreeVars
FreeVars forall a. Monoid a => a
mempty

freeVar :: Name -> FreeVars
freeVar :: Name -> FreeVars
freeVar Name
n = Name -> Int -> FreeVars
singleton Name
n Int
1

singleton :: Name -> Int -> FreeVars
singleton :: Name -> Int -> FreeVars
singleton Name
n Int
k = Map Name Int -> FreeVars
FreeVars forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
Map.singleton Name
n Int
k

without :: Foldable t => FreeVars -> t Name -> FreeVars
without :: forall (t :: * -> *). Foldable t => FreeVars -> t Name -> FreeVars
without (FreeVars Map Name Int
m) t Name
remove = Map Name Int -> FreeVars
FreeVars forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Map Name Int
m (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t Name
remove)

class HasVariables a where
  freeVars :: a -> FreeVars
  freeVarSet :: a -> Set Name
  freeVarSet = forall k a. Map k a -> Set k
Map.keysSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. FreeVars -> Map Name Int
unFreeVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasVariables a => a -> FreeVars
freeVars
  countOf :: Name -> a -> Int
  countOf Name
n = Name -> FreeVars -> Int
count Name
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasVariables a => a -> FreeVars
freeVars
  appearsIn :: Name -> a -> Bool
  appearsIn Name
n = (forall a. Ord a => a -> a -> Bool
> Int
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> FreeVars -> Int
count Name
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasVariables a => a -> FreeVars
freeVars

instance (HasVariables a, HasVariables b) => HasVariables (a, b) where
  freeVars :: (a, b) -> FreeVars
freeVars (a
a, b
b) = forall a. HasVariables a => a -> FreeVars
freeVars a
a forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> FreeVars
freeVars b
b
  freeVarSet :: (a, b) -> Set Name
freeVarSet (a
a, b
b) = forall a. HasVariables a => a -> Set Name
freeVarSet a
a forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> Set Name
freeVarSet b
b
  countOf :: Name -> (a, b) -> Int
countOf Name
n (a
a, b
b) = forall a. HasVariables a => Name -> a -> Int
countOf Name
n a
a forall a. Num a => a -> a -> a
+ forall a. HasVariables a => Name -> a -> Int
countOf Name
n b
b
  appearsIn :: Name -> (a, b) -> Bool
appearsIn Name
n (a
a, b
b) = forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n a
a Bool -> Bool -> Bool
|| forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n b
b

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

instance HasVariables Name where
  freeVars :: Name -> FreeVars
freeVars = Name -> FreeVars
freeVar
  freeVarSet :: Name -> Set Name
freeVarSet = forall a. a -> Set a
Set.singleton
  countOf :: Name -> Name -> Int
countOf Name
n Name
n'
    | Name
n forall a. Eq a => a -> a -> Bool
== Name
n' = Int
1
    | Bool
otherwise = Int
0
  appearsIn :: Name -> Name -> Bool
appearsIn Name
n Name
n' = Name
n forall a. Eq a => a -> a -> Bool
== Name
n'

instance HasVariables (Term a) where
  freeVars :: Term a -> FreeVars
freeVars = \case
    Lit {} -> forall a. Monoid a => a
mempty
    V Var a
x -> Name -> FreeVars
freeVar (forall a. HasSpec a => Var a -> Name
Name Var a
x)
    App t dom a
_ List Term dom
ts -> forall a. HasVariables a => a -> FreeVars
freeVars List Term dom
ts
  freeVarSet :: Term a -> Set Name
freeVarSet = \case
    Lit {} -> forall a. Monoid a => a
mempty
    V Var a
x -> forall a. HasVariables a => a -> Set Name
freeVarSet (forall a. HasSpec a => Var a -> Name
Name Var a
x)
    App t dom a
_ List Term dom
ts -> forall a. HasVariables a => a -> Set Name
freeVarSet List Term dom
ts
  countOf :: Name -> Term a -> Int
countOf Name
n = \case
    Lit {} -> Int
0
    V Var a
x -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n (forall a. HasSpec a => Var a -> Name
Name Var a
x)
    App t dom a
_ List Term dom
ts -> forall a. HasVariables a => Name -> a -> Int
countOf Name
n List Term dom
ts
  appearsIn :: Name -> Term a -> Bool
appearsIn Name
n = \case
    Lit {} -> Bool
False
    V Var a
x -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n (forall a. HasSpec a => Var a -> Name
Name Var a
x)
    App t dom a
_ List Term dom
ts -> forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n List Term dom
ts

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

instance HasVariables (Binder a) where
  freeVars :: Binder a -> FreeVars
freeVars (Var a
x :-> Pred
p) = forall a. HasVariables a => a -> FreeVars
freeVars Pred
p forall (t :: * -> *). Foldable t => FreeVars -> t Name -> FreeVars
`without` [forall a. HasSpec a => Var a -> Name
Name Var a
x]
  freeVarSet :: Binder a -> Set Name
freeVarSet (Var a
x :-> Pred
p) = forall a. Ord a => a -> Set a -> Set a
Set.delete (forall a. HasSpec a => Var a -> Name
Name Var a
x) (forall a. HasVariables a => a -> Set Name
freeVarSet Pred
p)
  countOf :: Name -> Binder a -> Int
countOf Name
n (Var a
x :-> Pred
p)
    | forall a. HasSpec a => Var a -> Name
Name Var a
x forall a. Eq a => a -> a -> Bool
== Name
n = Int
0
    | Bool
otherwise = forall a. HasVariables a => Name -> a -> Int
countOf Name
n Pred
p
  appearsIn :: Name -> Binder a -> Bool
appearsIn Name
n (Var a
x :-> Pred
p)
    | forall a. HasSpec a => Var a -> Name
Name Var a
x forall a. Eq a => a -> a -> Bool
== Name
n = Bool
False
    | Bool
otherwise = forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Pred
p

instance HasVariables (f a) => HasVariables (Weighted f a) where
  freeVars :: Weighted f a -> FreeVars
freeVars = forall a. HasVariables a => a -> FreeVars
freeVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing
  freeVarSet :: Weighted f a -> Set Name
freeVarSet = forall a. HasVariables a => a -> Set Name
freeVarSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing
  countOf :: Name -> Weighted f a -> Int
countOf Name
n = forall a. HasVariables a => Name -> a -> Int
countOf Name
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing
  appearsIn :: Name -> Weighted f a -> Bool
appearsIn Name
n = forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing

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

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

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

-- =================================================================
-- 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 -> forall a. HasSpec a => Var a -> Term a
V Var a
x
    Maybe (Var a)
Nothing -> case Term a
t of
      Lit a
a -> forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
a
      V Var a
x -> forall a. HasSpec a => Var a -> Term a
V Var a
x
      App t dom a
f List Term dom
ts -> forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App t dom a
f (forall {k} (c :: k -> Constraint) (as :: [k]) (f :: k -> *)
       (g :: k -> *).
All c as =>
(forall (a :: k). c a => f a -> g a) -> List f as -> List g as
mapListC @HasSpec (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub0) List Term dom
ts)
  where
    findMatch :: Subst -> Term a -> Maybe (Var a)
    findMatch :: Subst -> Term a -> Maybe (Var a)
findMatch [] Term a
_ = forall a. Maybe a
Nothing
    findMatch (Var a
x := Term a
t' : Subst
sub1) Term a
t1
      | forall a b. Term a -> Term b -> Bool
fastInequality Term a
t1 Term a
t' = Subst -> Term a -> Maybe (Var a)
findMatch Subst
sub1 Term a
t1
      | Just (Var a
x', Term a
t'') <- forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast (Var a
x, Term a
t')
      , Term a
t forall a. Eq a => a -> a -> Bool
== Term a
t'' =
          forall a. a -> Maybe a
Just Var a
x'
      | Bool
otherwise = Subst -> Term a -> Maybe (Var a)
findMatch Subst
sub1 Term a
t1

-- | Sound but not complete inequality on terms
fastInequality :: Term a -> Term b -> Bool
fastInequality :: forall a b. Term a -> Term b -> Bool
fastInequality (V (Var Int
i String
_)) (V (Var Int
j String
_)) = Int
i forall a. Eq a => a -> a -> Bool
/= Int
j
fastInequality Lit {} Lit {} = Bool
False
fastInequality (App t dom a
_ List Term dom
as) (App t dom b
_ List Term dom
bs) = forall (as :: [*]) (bs :: [*]).
List Term as -> List Term bs -> Bool
go List Term dom
as List Term dom
bs
  where
    go :: List Term as -> List Term bs -> Bool
    go :: forall (as :: [*]) (bs :: [*]).
List Term as -> List Term bs -> Bool
go List Term as
Nil List Term bs
Nil = Bool
False
    go (Term a
a :> List Term as1
as') (Term a
b :> List Term as1
bs') = forall a b. Term a -> Term b -> Bool
fastInequality Term a
a Term a
b Bool -> Bool -> Bool
|| forall (as :: [*]) (bs :: [*]).
List Term as -> List Term bs -> Bool
go List Term as1
as' List Term as1
bs'
    go List Term as
_ List Term bs
_ = Bool
True
fastInequality Term a
_ Term b
_ = Bool
True

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

substituteTerm :: forall a. Subst -> Term a -> Term a
substituteTerm :: forall a. Subst -> Term a -> Term a
substituteTerm Subst
sub = \case
  Lit a
a -> forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
a
  V Var a
x -> HasSpec a => Subst -> Var a -> Term a
substVar Subst
sub Var a
x
  App t dom a
f (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (forall a. Subst -> Term a -> Term a
substituteTerm Subst
sub) -> (List Term dom
ts :: List Term dom)) ->
    case forall (as :: [*]). List Term as -> Maybe (List Value as)
fromLits List Term dom
ts of
      Just List Value dom
vs -> forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit (forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
uncurryList_ forall a. Value a -> a
unValue (forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t dom a
f) List Value dom
vs)
      Maybe (List Value dom)
_ -> forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App t dom a
f List Term dom
ts
  where
    substVar :: HasSpec a => Subst -> Var a -> Term a
    substVar :: HasSpec a => Subst -> Var a -> Term a
substVar [] Var a
x = forall a. HasSpec a => Var a -> Term a
V Var a
x
    substVar (Var a
y := Term a
t : Subst
sub1) Var a
x
      | Just a :~: a
Refl <- forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var a
y = Term a
t
      | Bool
otherwise = HasSpec a => Subst -> Var a -> Term a
substVar Subst
sub1 Var a
x

substituteTerm' :: forall a. Subst -> Term a -> Writer Any (Term a)
substituteTerm' :: forall a. Subst -> Term a -> Writer Any (Term a)
substituteTerm' Subst
sub = \case
  Lit a
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
a
  V Var a
x -> HasSpec a => Subst -> Var a -> Writer Any (Term a)
substVar Subst
sub Var a
x
  App t dom a
f List Term dom
ts ->
    forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App t dom a
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (as :: [k]).
Applicative m =>
(forall (a :: k). f a -> m (g a)) -> List f as -> m (List g as)
mapMList (forall a. Subst -> Term a -> Writer Any (Term a)
substituteTerm' Subst
sub) List Term dom
ts
  where
    substVar :: HasSpec a => Subst -> Var a -> Writer Any (Term a)
    substVar :: HasSpec a => Subst -> Var a -> Writer Any (Term a)
substVar [] Var a
x = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Term a
V Var a
x
    substVar (Var a
y := Term a
t : Subst
sub1) Var a
x
      | Just a :~: a
Refl <- forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var a
y = Term a
t forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Bool -> Any
Any Bool
True)
      | Bool
otherwise = HasSpec a => Subst -> Var a -> Writer Any (Term a)
substVar Subst
sub1 Var a
x

substituteBinder :: HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder :: forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm (Var b
y :-> Pred
p) = Var b
y' forall a. HasSpec a => Var a -> Pred -> Binder a
:-> forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm Pred
p'
  where
    (Var b
y', Pred
p') =
      forall a t.
(Typeable a, Rename t) =>
Var a -> t -> Set Int -> (Var a, t)
freshen Var b
y Pred
p (forall a. a -> Set a
Set.singleton (forall a. Var a -> Int
nameOf Var a
x) forall a. Semigroup a => a -> a -> a
<> forall t. HasVariables t => t -> Set Int
freeVarNames Term a
tm forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => a -> Set a -> Set a
Set.delete (forall a. Var a -> Int
nameOf Var b
y) (forall t. HasVariables t => t -> Set Int
freeVarNames Pred
p))

substitutePred :: HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred :: forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm = \case
  ElemPred Bool
bool Term a
t NonEmpty a
xs -> forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term a
t) NonEmpty a
xs
  GenHint Hint a
h Term a
t -> forall a. HasGenHint a => Hint a -> Term a -> Pred
GenHint Hint a
h (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term a
t)
  Subst Var a
x' Term a
t Pred
p -> forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x' Term a
t Pred
p
  Assert Term Bool
t -> Term Bool -> Pred
Assert (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term Bool
t)
  And [Pred]
ps -> forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
  Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (\forall b. Term b -> b
eval -> (forall b. Term b -> b) -> GE a
k (forall b. Term b -> b
eval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm])) (forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm Binder a
b)
  Let Term a
t Binder a
b -> forall a. Term a -> Binder a -> Pred
Let (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term a
t) (forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm Binder a
b)
  ForAll Term t
t Binder a
b -> forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term t
t) (forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm Binder a
b)
  Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term (SumOver as)
t) (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (forall {k1} {k2} (f :: k1 -> *) (a :: k1) (g :: k2 -> *) (b :: k2).
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted forall a b. (a -> b) -> a -> b
$ forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm) List (Weighted Binder) as
bs)
  When Term Bool
b Pred
p -> HasSpec Bool => Term Bool -> Pred -> Pred
When (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term Bool
b) (forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm Pred
p)
  Reifies Term b
t' Term a
t a -> b
f -> forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
Reifies (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term b
t') (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term a
t) a -> b
f
  DependsOn Term a
t Term b
t' -> forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term a
t) (forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term b
t')
  Pred
TruePred -> Pred
TruePred
  FalsePred NonEmpty String
es -> NonEmpty String -> Pred
FalsePred NonEmpty String
es
  Monitor (forall b. Term b -> b) -> Property -> Property
m -> ((forall b. Term b -> b) -> Property -> Property) -> Pred
Monitor (\forall b. Term b -> b
eval -> (forall b. Term b -> b) -> Property -> Property
m (forall b. Term b -> b
eval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm]))
  Explain NonEmpty String
es Pred
p -> NonEmpty String -> Pred -> Pred
Explain NonEmpty String
es forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm Pred
p

-- =====================================================
-- 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 -> forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
a
  V Var a
v
    | Just a
a <- forall a. Typeable a => Env -> Var a -> Maybe a
lookupEnv Env
env Var a
v -> forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
a
    | Bool
otherwise -> forall a. HasSpec a => Var a -> Term a
V Var a
v
  App t dom a
f (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (forall a. Env -> Term a -> Term a
substTerm Env
env) -> List Term dom
ts) ->
    case forall (as :: [*]). List Term as -> Maybe (List Value as)
fromLits List Term dom
ts of
      Just List Value dom
vs -> forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit (forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
uncurryList_ forall a. Value a -> a
unValue (forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t dom a
f) List Value dom
vs)
      Maybe (List Value dom)
_ -> forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App t dom a
f List Term dom
ts

substBinder :: Env -> Binder a -> Binder a
substBinder :: forall a. Env -> Binder a -> Binder a
substBinder Env
env (Var a
x :-> Pred
p) = Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Env -> Pred -> Pred
substPred (forall a. Var a -> Env -> Env
removeVar Var a
x Env
env) Pred
p

substPred :: Env -> Pred -> Pred
substPred :: Env -> Pred -> Pred
substPred Env
env = \case
  ElemPred Bool
bool Term a
t NonEmpty a
xs -> forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool (forall a. Env -> Term a -> Term a
substTerm Env
env Term a
t) NonEmpty a
xs
  GenHint Hint a
h Term a
t -> forall a. HasGenHint a => Hint a -> Term a -> Pred
GenHint Hint a
h (forall a. Env -> Term a -> Term a
substTerm Env
env Term a
t)
  Subst Var a
x Term a
t Pred
p -> Env -> Pred -> Pred
substPred Env
env forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p
  Assert Term Bool
t -> Term Bool -> Pred
Assert (forall a. Env -> Term a -> Term a
substTerm Env
env Term Bool
t)
  Reifies Term b
t' Term a
t a -> b
f -> forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
Reifies (forall a. Env -> Term a -> Term a
substTerm Env
env Term b
t') (forall a. Env -> Term a -> Term a
substTerm Env
env Term a
t) a -> b
f
  ForAll Term t
set Binder a
b -> forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll (forall a. Env -> Term a -> Term a
substTerm Env
env Term t
set) (forall a. Env -> Binder a -> Binder a
substBinder Env
env Binder a
b)
  Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case (forall a. Env -> Term a -> Term a
substTerm Env
env Term (SumOver as)
t) (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (forall {k1} {k2} (f :: k1 -> *) (a :: k1) (g :: k2 -> *) (b :: k2).
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted forall a b. (a -> b) -> a -> b
$ forall a. Env -> Binder a -> Binder a
substBinder Env
env) List (Weighted Binder) as
bs)
  When Term Bool
b Pred
p -> HasSpec Bool => Term Bool -> Pred -> Pred
When (forall a. Env -> Term a -> Term a
substTerm Env
env Term Bool
b) (Env -> Pred -> Pred
substPred Env
env Pred
p)
  DependsOn Term a
x Term b
y -> forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn (forall a. Env -> Term a -> Term a
substTerm Env
env Term a
x) (forall a. Env -> Term a -> Term a
substTerm Env
env Term b
y)
  Pred
TruePred -> Pred
TruePred
  FalsePred NonEmpty String
es -> NonEmpty String -> Pred
FalsePred NonEmpty String
es
  And [Pred]
ps -> forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Env -> Pred -> Pred
substPred Env
env forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
  Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (\forall b. Term b -> b
eval -> (forall b. Term b -> b) -> GE a
k forall a b. (a -> b) -> a -> b
$ forall b. Term b -> b
eval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Env -> Term a -> Term a
substTerm Env
env) (forall a. Env -> Binder a -> Binder a
substBinder Env
env Binder a
b)
  Let Term a
t Binder a
b -> forall a. Term a -> Binder a -> Pred
Let (forall a. Env -> Term a -> Term a
substTerm Env
env Term a
t) (forall a. Env -> Binder a -> Binder a
substBinder Env
env Binder a
b)
  Monitor (forall b. Term b -> b) -> Property -> Property
m -> ((forall b. Term b -> b) -> Property -> Property) -> Pred
Monitor (forall b. Term b -> b) -> Property -> Property
m
  Explain NonEmpty String
es Pred
p -> NonEmpty String -> Pred -> Pred
Explain NonEmpty String
es forall a b. (a -> b) -> a -> b
$ Env -> Pred -> Pred
substPred Env
env Pred
p

unBind :: a -> Binder a -> Pred
unBind :: forall a. a -> Binder a -> Pred
unBind a
a (Var a
x :-> Pred
p) = Env -> Pred -> Pred
substPred (forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var a
x a
a) Pred
p

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

-- Instances

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

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

instance Ord Name where
  compare :: Name -> Name -> Ordering
compare (Name Var a
v) (Name Var a
v') = forall a. Ord a => a -> a -> Ordering
compare (forall a. Var a -> Int
nameOf Var a
v, forall a. Typeable a => a -> TypeRep
typeOf Var a
v) (forall a. Var a -> Int
nameOf Var a
v', forall a. Typeable a => a -> TypeRep
typeOf Var a
v')

instance Rename Name where
  rename :: forall x. Typeable x => Var x -> Var x -> Name -> Name
rename Var x
v Var x
v' (Name Var a
v'') = forall a. HasSpec a => Var a -> Name
Name forall a b. (a -> b) -> a -> b
$ forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Var a
v''

instance Rename (Term a) where
  rename :: forall x. Typeable x => Var x -> Var x -> Term a -> Term a
rename Var x
v Var x
v'
    | Var x
v forall a. Eq a => a -> a -> Bool
== Var x
v' = forall a. a -> a
id
    | Bool
otherwise = \case
        Lit a
l -> forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
l
        V Var a
v'' -> forall a. HasSpec a => Var a -> Term a
V (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Var a
v'')
        App t dom a
f List Term dom
a -> forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App t dom a
f (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' List Term dom
a)

instance Rename Pred where
  rename :: forall x. Typeable x => Var x -> Var x -> Pred -> Pred
rename Var x
v Var x
v'
    | Var x
v forall a. Eq a => a -> a -> Bool
== Var x
v' = forall a. a -> a
id
    | Bool
otherwise = \case
        ElemPred Bool
bool Term a
t NonEmpty a
xs -> forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term a
t) NonEmpty a
xs
        GenHint Hint a
h Term a
t -> forall a. HasGenHint a => Hint a -> Term a -> Pred
GenHint Hint a
h (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term a
t)
        Subst Var a
x Term a
t Pred
p -> forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p
        And [Pred]
ps -> [Pred] -> Pred
And (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' [Pred]
ps)
        Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (\forall b. Term b -> b
eval -> (forall b. Term b -> b) -> GE a
k forall a b. (a -> b) -> a -> b
$ forall b. Term b -> b
eval forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v') (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Binder a
b)
        Let Term a
t Binder a
b -> forall a. Term a -> Binder a -> Pred
Let (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term a
t) (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Binder a
b)
        Reifies Term b
t' Term a
t a -> b
f -> forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
Reifies (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term b
t') (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term a
t) a -> b
f
        Assert Term Bool
t -> Term Bool -> Pred
Assert (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term Bool
t)
        DependsOn Term a
x Term b
y -> forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term a
x) (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term b
y)
        ForAll Term t
set Binder a
b -> forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term t
set) (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Binder a
b)
        Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term (SumOver as)
t) (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' List (Weighted Binder) as
bs)
        When Term Bool
b Pred
p -> HasSpec Bool => Term Bool -> Pred -> Pred
When (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term Bool
b) (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Pred
p)
        Pred
TruePred -> Pred
TruePred
        FalsePred NonEmpty String
es -> NonEmpty String -> Pred
FalsePred NonEmpty String
es
        Monitor (forall b. Term b -> b) -> Property -> Property
m -> ((forall b. Term b -> b) -> Property -> Property) -> Pred
Monitor (forall b. Term b -> b) -> Property -> Property
m
        Explain NonEmpty String
es Pred
p -> NonEmpty String -> Pred -> Pred
Explain NonEmpty String
es (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Pred
p)

instance Rename (Binder a) where
  rename :: forall x. Typeable x => Var x -> Var x -> Binder a -> Binder a
rename Var x
v Var x
v' (Var a
va :-> Pred
psa) = Var a
va' forall a. HasSpec a => Var a -> Pred -> Binder a
:-> forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Pred
psa'
    where
      (Var a
va', Pred
psa') = forall a t.
(Typeable a, Rename t) =>
Var a -> t -> Set Int -> (Var a, t)
freshen Var a
va Pred
psa (forall a. Ord a => [a] -> Set a
Set.fromList [forall a. Var a -> Int
nameOf Var x
v, forall a. Var a -> Int
nameOf Var x
v'] forall a. Semigroup a => a -> a -> a
<> forall a. Ord a => a -> Set a -> Set a
Set.delete (forall a. Var a -> Int
nameOf Var a
va) (forall t. HasVariables t => t -> Set Int
freeVarNames Pred
psa))

instance Rename (f a) => Rename (Weighted f a) where
  rename :: forall x.
Typeable x =>
Var x -> Var x -> Weighted f a -> Weighted f a
rename Var x
v Var x
v' (Weighted Maybe Int
w f a
t) = forall {k} (f :: k -> *) (a :: k). Maybe Int -> f a -> Weighted f a
Weighted Maybe Int
w (forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' f a
t)

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

fromLits :: List Term as -> Maybe (List Value as)
fromLits :: forall (as :: [*]). List Term as -> Maybe (List Value as)
fromLits = forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (as :: [k]).
Applicative m =>
(forall (a :: k). f a -> m (g a)) -> List f as -> m (List g as)
mapMList forall a. Term a -> Maybe (Value a)
fromLit

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

isLit :: Term a -> Bool
isLit :: forall a. Term a -> Bool
isLit = forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Term a -> Maybe (Value a)
fromLit

name :: String -> Term a -> Term a
name :: forall a. String -> Term a -> Term a
name String
nh (V (Var Int
i String
_)) = forall a. HasSpec a => Var a -> Term a
V (forall a. Int -> String -> Var a
Var Int
i String
nh)
name String
_ Term a
_ = forall a. HasCallStack => String -> a
error String
"applying name to non-var thing! Shame on you!"

-- | 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 forall a. Eq a => a -> a -> Bool
/= String
"v" then Term a
t else forall a. HasSpec a => Var a -> Term a
V (forall a. Int -> String -> Var a
Var Int
i String
nh)
named String
_ Term a
t = Term a
t

mkCase ::
  HasSpec (SumOver as) => Term (SumOver as) -> List (Weighted Binder) as -> Pred
mkCase :: forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
mkCase Term (SumOver as)
tm List (Weighted Binder) as
cs
  | Weighted Maybe Int
_ (Var a
x :-> Pred
p) :> List (Weighted Binder) as1
Nil <- List (Weighted Binder) as
cs = forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
Subst Var a
x Term (SumOver as)
tm Pred
p
  -- TODO: all equal maybe?
  | All -> Bool
Semigroup.getAll forall a b. (a -> b) -> a -> b
$ forall {k} b (f :: k -> *) (as :: [k]).
Monoid b =>
(forall (a :: k). f a -> b) -> List f as -> b
foldMapList forall {a}. Weighted Binder a -> All
isTrueBinder List (Weighted Binder) as
cs = Pred
TruePred
  | All -> Bool
Semigroup.getAll forall a b. (a -> b) -> a -> b
$ forall {k} b (f :: k -> *) (as :: [k]).
Monoid b =>
(forall (a :: k). f a -> b) -> List f as -> b
foldMapList (forall {a}. Binder a -> All
isFalseBinder forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing) List (Weighted Binder) as
cs = NonEmpty String -> Pred
FalsePred (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"mkCase on all False")
  | Lit SumOver as
a <- Term (SumOver as)
tm = forall (as :: [*]) r.
SumOver as
-> List Binder as
-> (forall a. HasSpec a => Var a -> a -> Pred -> r)
-> r
runCaseOn SumOver as
a (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList forall {k} (f :: k -> *) (a :: k). Weighted f a -> f a
thing List (Weighted Binder) as
cs) (\Var a
x a
val Pred
p -> Env -> Pred -> Pred
substPred (forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var a
x a
val) Pred
p)
  | Bool
otherwise = forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case Term (SumOver as)
tm List (Weighted Binder) as
cs
  where
    isTrueBinder :: Weighted Binder a -> All
isTrueBinder (Weighted Maybe Int
Nothing (Var a
_ :-> Pred
TruePred)) = Bool -> All
Semigroup.All Bool
True
    isTrueBinder Weighted Binder a
_ = Bool -> All
Semigroup.All Bool
False

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

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

-- ================================================
-- 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 :: Var a -> Subst -> Subst
adjustSub Var a
x Subst
sub =
      [ Var a
x' forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
t
      | Var a
x' := Term a
t <- Subst
sub
      , forall a. Maybe a -> Bool
isNothing forall a b. (a -> b) -> a -> b
$ forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var a
x'
      , -- TODO: possibly freshen the binder where
      -- `x` appears instead?
      Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Name
Name Var a
x forall a. HasVariables a => Name -> a -> Bool
`appearsIn` Term a
t
      ]

    goBinder :: Subst -> Binder a -> Binder a
    goBinder :: forall a. Subst -> Binder a -> Binder a
goBinder Subst
sub (Var a
x :-> Pred
p) = Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Subst -> Pred -> Pred
go (forall {a}. HasSpec a => Var a -> Subst -> Subst
adjustSub Var a
x Subst
sub) Pred
p

    go :: Subst -> Pred -> Pred
go Subst
sub = \case
      ElemPred Bool
bool Term a
t NonEmpty a
xs -> forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term a
t) NonEmpty a
xs
      GenHint Hint a
h Term a
t -> forall a. HasGenHint a => Hint a -> Term a -> Pred
GenHint Hint a
h (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term a
t)
      And [Pred]
ps -> [Pred] -> Pred
And (Subst -> Pred -> Pred
go Subst
sub forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
      Let Term a
t (Var a
x :-> Pred
p) -> forall a. Term a -> Binder a -> Pred
Let Term a
t' (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Subst -> Pred -> Pred
go (Var a
x forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
t' forall a. a -> [a] -> [a]
: Subst
sub') Pred
p)
        where
          t' :: Term a
t' = forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term a
t
          sub' :: Subst
sub' = forall {a}. HasSpec a => Var a -> Subst -> Subst
adjustSub Var a
x Subst
sub
      Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (forall b. Term b -> b) -> GE a
k (forall a. Subst -> Binder a -> Binder a
goBinder Subst
sub Binder a
b)
      Subst Var a
x Term a
t Pred
p -> Subst -> Pred -> Pred
go Subst
sub (forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p)
      Assert Term Bool
t -> Term Bool -> Pred
Assert (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term Bool
t)
      Reifies Term b
t' Term a
t a -> b
f -> forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
Reifies (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term b
t') (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term a
t) a -> b
f
      -- 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 Term a
t Term b
t' -> forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term a
t) (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term b
t')
      ForAll Term t
t Binder a
b -> forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term t
t) (forall a. Subst -> Binder a -> Binder a
goBinder Subst
sub Binder a
b)
      Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term (SumOver as)
t) (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (forall {k1} {k2} (f :: k1 -> *) (a :: k1) (g :: k2 -> *) (b :: k2).
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted forall a b. (a -> b) -> a -> b
$ forall a. Subst -> Binder a -> Binder a
goBinder Subst
sub) List (Weighted Binder) as
bs)
      When Term Bool
b Pred
p -> HasSpec Bool => Term Bool -> Pred -> Pred
When (forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term Bool
b) (Subst -> Pred -> Pred
go Subst
sub Pred
p)
      Pred
TruePred -> Pred
TruePred
      FalsePred NonEmpty String
es -> NonEmpty String -> Pred
FalsePred NonEmpty String
es
      Monitor (forall b. Term b -> b) -> Property -> Property
m -> ((forall b. Term b -> b) -> Property -> Property) -> Pred
Monitor (forall b. Term b -> b) -> Property -> Property
m
      Explain NonEmpty String
es Pred
p -> NonEmpty String -> Pred -> Pred
Explain NonEmpty String
es forall a b. (a -> b) -> a -> b
$ Subst -> Pred -> Pred
go Subst
sub Pred
p

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

    goBlock' :: Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' Set Int
_ [Pred]
ctx [] = [Pred]
ctx
    goBlock' Set Int
fvs [Pred]
ctx (Let Term a
t (Var a
x :-> Pred
p) : [Pred]
ps) =
      -- We can do `goBlock'` here because we've already done let floating
      -- on the inner `p`
      [forall a. Term a -> Binder a -> Pred
Let Term a
t (Var a
x' forall a. HasSpec a => Var a -> Pred -> Binder a
:-> forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' (forall a. Ord a => a -> Set a -> Set a
Set.insert (forall a. Var a -> Int
nameOf Var a
x') Set Int
fvs) [Pred]
ctx (Pred
p' forall a. a -> [a] -> [a]
: [Pred]
ps)))]
      where
        (Var a
x', Pred
p') = forall a t.
(Typeable a, Rename t) =>
Var a -> t -> Set Int -> (Var a, t)
freshen Var a
x Pred
p Set Int
fvs
    goBlock' Set Int
fvs [Pred]
ctx (And [Pred]
ps : [Pred]
ps') = Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' Set Int
fvs [Pred]
ctx ([Pred]
ps forall a. [a] -> [a] -> [a]
++ [Pred]
ps')
    goBlock' Set Int
fvs [Pred]
ctx (Pred
p : [Pred]
ps) = Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' Set Int
fvs (Pred
p forall a. a -> [a] -> [a]
: [Pred]
ctx) [Pred]
ps

    goExists ::
      HasSpec a =>
      [Pred] ->
      (Binder a -> Pred) ->
      Var a ->
      Pred ->
      [Pred]
    goExists :: forall a.
HasSpec a =>
[Pred] -> (Binder a -> Pred) -> Var a -> Pred -> [Pred]
goExists [Pred]
ctx Binder a -> Pred
ex Var a
x (Let Term a
t (Var a
y :-> Pred
p))
      | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => Var a -> Name
Name Var a
x forall a. HasVariables a => Name -> a -> Bool
`appearsIn` Term a
t =
          let (Var a
y', Pred
p') = forall a t.
(Typeable a, Rename t) =>
Var a -> t -> Set Int -> (Var a, t)
freshen Var a
y Pred
p (forall a. Ord a => a -> Set a -> Set a
Set.insert (forall a. Var a -> Int
nameOf Var a
x) forall a b. (a -> b) -> a -> b
$ forall t. HasVariables t => t -> Set Int
freeVarNames Pred
p forall a. Semigroup a => a -> a -> a
<> forall t. HasVariables t => t -> Set Int
freeVarNames Term a
t)
           in [Pred] -> Pred -> [Pred]
go [Pred]
ctx (forall a. Term a -> Binder a -> Pred
Let Term a
t (Var a
y' forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Binder a -> Pred
ex (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
p')))
    goExists [Pred]
ctx Binder a -> Pred
ex Var a
x Pred
p = Binder a -> Pred
ex (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
p) forall a. a -> [a] -> [a]
: [Pred]
ctx

    pushExplain :: NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es (Let Term a
t (Var a
x :-> Pred
p)) = forall a. Term a -> Binder a -> Pred
Let Term a
t (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es Pred
p)
    pushExplain NonEmpty String
es (And [Pred]
ps) = [Pred] -> Pred
And (NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
    pushExplain NonEmpty String
es (Exists (forall b. Term b -> b) -> GE a
k (Var a
x :-> Pred
p)) =
      forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (forall a.
((forall b. Term b -> b) -> GE a)
-> (forall b. Term b -> b) -> GE a
explainSemantics (forall b. Term b -> b) -> GE a
k) (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es Pred
p)
      where
        -- 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. Term b -> b) -> GE a)
-> (forall b. Term b -> b) -> GE a
explainSemantics (forall b. Term b -> b) -> GE a
k2 forall b. Term b -> b
env = forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a -> m a
explainNE NonEmpty String
es forall a b. (a -> b) -> a -> b
$ (forall b. Term b -> b) -> GE a
k2 forall b. Term b -> b
env
    -- 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 Term Bool
b Pred
p) = HasSpec Bool => Term Bool -> Pred -> Pred
When Term Bool
b (NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es Pred
p)
    pushExplain NonEmpty String
es Pred
p = NonEmpty String -> Pred -> Pred
explanation NonEmpty String
es Pred
p

    go :: [Pred] -> Pred -> [Pred]
go [Pred]
ctx = \case
      ElemPred Bool
bool Term a
t NonEmpty a
xs -> forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool Term a
t NonEmpty a
xs forall a. a -> [a] -> [a]
: [Pred]
ctx
      And [Pred]
ps0 -> [Pred] -> [Pred] -> [Pred]
goBlock [Pred]
ctx (forall a b. (a -> b) -> [a] -> [b]
map Pred -> Pred
letFloating [Pred]
ps0)
      Let Term a
t (Var a
x :-> Pred
p) -> [Pred] -> [Pred] -> [Pred]
goBlock [Pred]
ctx [forall a. Term a -> Binder a -> Pred
Let Term a
t (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred -> Pred
letFloating Pred
p)]
      Exists (forall b. Term b -> b) -> GE a
k (Var a
x :-> Pred
p) -> forall a.
HasSpec a =>
[Pred] -> (Binder a -> Pred) -> Var a -> Pred -> [Pred]
goExists [Pred]
ctx (forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (forall b. Term b -> b) -> GE a
k) Var a
x (Pred -> Pred
letFloating Pred
p)
      Subst Var a
x Term a
t Pred
p -> [Pred] -> Pred -> [Pred]
go [Pred]
ctx (forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p)
      Reifies Term b
t' Term a
t a -> b
f -> forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
Reifies Term b
t' Term a
t a -> b
f forall a. a -> [a] -> [a]
: [Pred]
ctx
      Explain NonEmpty String
es Pred
p -> NonEmpty String -> Pred -> Pred
pushExplain NonEmpty String
es Pred
p forall a. a -> [a] -> [a]
: [Pred]
ctx
      -- TODO: float let through forall if possible
      ForAll Term t
t (Var a
x :-> Pred
p) -> forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll Term t
t (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred -> Pred
letFloating Pred
p) forall a. a -> [a] -> [a]
: [Pred]
ctx
      -- TODO: float let through the cases if possible
      Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case Term (SumOver as)
t (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (forall {k1} {k2} (f :: k1 -> *) (a :: k1) (g :: k2 -> *) (b :: k2).
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted (\(Var a
x :-> Pred
p) -> Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred -> Pred
letFloating Pred
p)) List (Weighted Binder) as
bs) forall a. a -> [a] -> [a]
: [Pred]
ctx
      -- TODO: float let through if possible
      When Term Bool
b Pred
p -> HasSpec Bool => Term Bool -> Pred -> Pred
When Term Bool
b (Pred -> Pred
letFloating Pred
p) forall a. a -> [a] -> [a]
: [Pred]
ctx
      -- Boring cases
      Assert Term Bool
t -> Term Bool -> Pred
Assert Term Bool
t forall a. a -> [a] -> [a]
: [Pred]
ctx
      GenHint Hint a
h Term a
t -> forall a. HasGenHint a => Hint a -> Term a -> Pred
GenHint Hint a
h Term a
t forall a. a -> [a] -> [a]
: [Pred]
ctx
      DependsOn Term a
t Term b
t' -> forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn Term a
t Term b
t' forall a. a -> [a] -> [a]
: [Pred]
ctx
      Pred
TruePred -> Pred
TruePred forall a. a -> [a] -> [a]
: [Pred]
ctx
      FalsePred NonEmpty String
es -> NonEmpty String -> Pred
FalsePred NonEmpty String
es forall a. a -> [a] -> [a]
: [Pred]
ctx
      Monitor (forall b. Term b -> b) -> Property -> Property
m -> ((forall b. Term b -> b) -> Property -> Property) -> Pred
Monitor (forall b. Term b -> b) -> Property -> Property
m forall a. a -> [a] -> [a]
: [Pred]
ctx

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

assert ::
  IsPred p =>
  p ->
  Pred
assert :: forall p. IsPred p => p -> Pred
assert p
p = forall p. IsPred p => p -> Pred
toPred p
p

forAll ::
  ( Forallable t a
  , HasSpec t
  , HasSpec a
  , IsPred p
  ) =>
  Term t ->
  (Term a -> p) ->
  Pred
forAll :: forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term t
tm = forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
mkForAll Term t
tm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind

mkForAll ::
  ( Forallable t a
  , HasSpec t
  , HasSpec a
  ) =>
  Term t ->
  Binder a ->
  Pred
mkForAll :: forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
mkForAll (Lit (forall t e. Forallable t e => t -> [e]
forAllToList -> [])) Binder a
_ = Pred
TruePred
mkForAll Term t
_ (Var a
_ :-> Pred
TruePred) = Pred
TruePred
mkForAll Term t
tm Binder a
binder = forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll Term t
tm Binder a
binder

exists ::
  forall a p.
  (HasSpec a, IsPred p) =>
  ((forall b. Term b -> b) -> GE a) ->
  (Term a -> p) ->
  Pred
exists :: forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (forall b. Term b -> b) -> GE a
sem Term a -> p
k =
  forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (forall b. Term b -> b) -> GE a
sem forall a b. (a -> b) -> a -> b
$ forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind Term a -> p
k

unsafeExists ::
  forall a p.
  (HasSpec a, IsPred p) =>
  (Term a -> p) ->
  Pred
unsafeExists :: forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Pred
unsafeExists = forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
_ -> forall (m :: * -> *) a. MonadGenError m => String -> m a
fatalError String
"unsafeExists")

letBind ::
  ( HasSpec a
  , IsPred p
  ) =>
  Term a ->
  (Term a -> p) ->
  Pred
letBind :: forall a p.
(HasSpec a, IsPred p) =>
Term a -> (Term a -> p) -> Pred
letBind tm :: Term a
tm@V {} Term a -> p
body = forall p. IsPred p => p -> Pred
toPred (Term a -> p
body Term a
tm)
letBind Term a
tm Term a -> p
body = forall a. Term a -> Binder a -> Pred
Let Term a
tm (forall a p. (HasSpec a, IsPred p) => (Term a -> p) -> Binder a
bind Term a -> p
body)

reify ::
  ( HasSpec a
  , HasSpec b
  , IsPred p
  ) =>
  Term a ->
  (a -> b) ->
  (Term b -> p) ->
  Pred
reify :: forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term a
t a -> b
f Term b -> p
body =
  forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists (\forall b. Term b -> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ a -> b
f (forall b. Term b -> b
eval Term a
t)) forall a b. (a -> b) -> a -> b
$ \Term b
x ->
    [ forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
reifies Term b
x Term a
t a -> b
f
    , NonEmpty String -> Pred -> Pred
Explain (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"reify " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term a
t forall a. [a] -> [a] -> [a]
++ String
" somef $")) forall a b. (a -> b) -> a -> b
$ forall p. IsPred p => p -> Pred
toPred (Term b -> p
body Term b
x)
    ]

-- | 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 =
  forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term a
t a -> Bool
f forall p. IsPred p => p -> Pred
assert

-- | 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
TruePred
explanation NonEmpty String
es (FalsePred NonEmpty String
es') = NonEmpty String -> Pred
FalsePred (NonEmpty String
es forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es')
explanation NonEmpty String
es (Assert Term Bool
t) = NonEmpty String -> Pred -> Pred
Explain NonEmpty String
es forall a b. (a -> b) -> a -> b
$ Term Bool -> Pred
Assert Term Bool
t
explanation NonEmpty String
es Pred
p = NonEmpty String -> Pred -> Pred
Explain NonEmpty String
es Pred
p

-- | 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. Term b -> b) -> Property -> Property) -> Pred
monitor = ((forall b. Term b -> b) -> Property -> Property) -> Pred
Monitor

reifies :: (HasSpec a, HasSpec b) => Term b -> Term a -> (a -> b) -> Pred
reifies :: forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
reifies = forall a b.
(HasSpec a, HasSpec b) =>
Term b -> Term a -> (a -> b) -> Pred
Reifies

dependsOn :: (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn :: forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn = forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn

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

genHint :: forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint :: forall a. HasGenHint a => Hint a -> Term a -> Pred
genHint = forall a. HasGenHint a => Hint a -> Term a -> Pred
GenHint

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

-- 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 Term a
_term NonEmpty a
_xs -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  -- NOTE: these don't bind anything
  Assert {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  DependsOn {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  Monitor {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  TruePred {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  FalsePred {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  GenHint {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  -- NOTE: this is ok because the variables either come from an `Exists`, a `Let`, or from
  -- the top level
  Reifies {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  -- NOTE: variables in here shouldn't escape to the top level
  ForAll {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  Case {} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  -- These can introduce binders that show up in the plan
  When Term Bool
_ Pred
pp -> Env -> Pred -> GE Env
envFromPred Env
env Pred
pp
  Subst Var a
x Term a
a Pred
pp -> Env -> Pred -> GE Env
envFromPred Env
env (forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
a Pred
pp)
  Let Term a
t (Var a
x :-> Pred
pp) -> do
    a
v <- forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term a
t
    Env -> Pred -> GE Env
envFromPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
v Env
env) Pred
pp
  Explain NonEmpty String
_ Pred
pp -> Env -> Pred -> GE Env
envFromPred Env
env Pred
pp
  Exists (forall b. Term b -> b) -> GE a
c (Var a
x :-> Pred
pp) -> do
    a
v <- (forall b. Term b -> b) -> GE a
c (forall a. GE a -> a
errorGE forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadGenError m => String -> m a -> m a
explain String
"envFromPred: Exists" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env)
    Env -> Pred -> GE Env
envFromPred (forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
v Env
env) Pred
pp
  And [] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Env
env
  And (Pred
pp : [Pred]
ps) -> do
    Env
env' <- Env -> Pred -> GE Env
envFromPred Env
env Pred
pp
    Env -> Pred -> GE Env
envFromPred Env
env' ([Pred] -> Pred
And [Pred]
ps)

-- ============================================================
-- A bit more than just syntax, but it is used here
-- Either it doesn't evaluate successfully: Left (NE.NonEmpty whatWentWrong),
-- or it does: Right thevalue

runTermE :: forall a. Env -> Term a -> Either (NE.NonEmpty String) a
runTermE :: forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env = \case
  Lit a
a -> forall a b. b -> Either a b
Right a
a
  V Var a
v -> case forall a. Typeable a => Env -> Var a -> Maybe a
lookupEnv Env
env Var a
v of
    Just a
a -> forall a b. b -> Either a b
Right a
a
    Maybe a
Nothing -> forall a b. a -> Either a b
Left (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Couldn't find " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Var a
v forall a. [a] -> [a] -> [a]
++ String
" in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Env
env))
  App t dom a
f (List Term dom
ts :: List Term dom) -> do
    List Identity dom
vs <- forall {k} (m :: * -> *) (f :: k -> *) (g :: k -> *) (as :: [k]).
Applicative m =>
(forall (a :: k). f a -> m (g a)) -> List f as -> m (List g as)
mapMList (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Identity a
Identity forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env) List Term dom
ts
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
uncurryList_ forall a. Identity a -> a
runIdentity (forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t dom a
f) List Identity dom
vs

-- TODO: Why on gods earth is this in a module called `Syntax`?!
-- Because we don't want a module named `Semantics` with just 15 lines
runTerm :: MonadGenError m => Env -> Term a -> m a
runTerm :: forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term a
x = case forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term a
x of
  Left NonEmpty String
msgs -> forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE NonEmpty String
msgs
  Right a
val -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
val

-- ===============================================================================
-- 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
stageSpec :: Specification a
stagePreds :: [Pred]
stageVar :: Var a
stageSpec :: ()
stagePreds :: SolverStage -> [Pred]
stageVar :: ()
..} =
    forall a ann. Show a => a -> Doc ann
viaShow Var a
stageVar
      forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"<-"
        forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [Doc ann] -> Doc ann
vsep'
          ( [forall a ann. Pretty a => a -> Doc ann
pretty Specification a
stageSpec | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Specification a -> Bool
isTrueSpec Specification a
stageSpec]
              forall a. [a] -> [a] -> [a]
++ [Doc ann
"---" | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pred]
stagePreds, Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. Specification a -> Bool
isTrueSpec Specification a
stageSpec]
              forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
pretty [Pred]
stagePreds
          )

data SolverPlan = SolverPlan
  { SolverPlan -> [SolverStage]
solverPlan :: [SolverStage]
  , SolverPlan -> Graph Name
solverDependencies :: Graph Name
  }

instance Pretty SolverPlan where
  pretty :: forall ann. SolverPlan -> Doc ann
pretty SolverPlan {[SolverStage]
Graph Name
solverDependencies :: Graph Name
solverPlan :: [SolverStage]
solverDependencies :: SolverPlan -> Graph Name
solverPlan :: SolverPlan -> [SolverStage]
..} =
    Doc ann
"\nSolverPlan"
      forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [Doc ann] -> Doc ann
vsep'
        [ -- "\nDependencies:" /> pretty solverDependencies, -- Might be usefull someday
          Doc ann
"\nLinearization:" forall ann. Doc ann -> Doc ann -> Doc ann
/> forall ann. [SolverStage] -> Doc ann
prettyLinear [SolverStage]
solverPlan
        ]

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

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

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

regularizeBinder :: Binder a -> Binder a
regularizeBinder :: forall a. Binder a -> Binder a
regularizeBinder (Var a
x :-> Pred
p) = Var a
x' forall a. HasSpec a => Var a -> Pred -> Binder a
:-> forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x (forall a. HasSpec a => Var a -> Term a
V Var a
x') (Pred -> Pred
regularizeNamesPred Pred
p)
  where
    x' :: Var a
x' = forall t a. HasVariables t => Var a -> t -> Var a
regularize Var a
x Pred
p

regularizeNamesPred :: Pred -> Pred
regularizeNamesPred :: Pred -> Pred
regularizeNamesPred Pred
pred = case Pred
pred of
  ElemPred {} -> Pred
pred
  Monitor {} -> Pred
pred
  And [Pred]
ps -> [Pred] -> Pred
And forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Pred -> Pred
regularizeNamesPred [Pred]
ps
  Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (forall b. Term b -> b) -> GE a
k (forall a. Binder a -> Binder a
regularizeBinder Binder a
b)
  Subst Var a
v Term a
t Pred
p -> Pred -> Pred
regularizeNamesPred (forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
v Term a
t Pred
p)
  Let Term a
t Binder a
b -> forall a. Term a -> Binder a -> Pred
Let Term a
t (forall a. Binder a -> Binder a
regularizeBinder Binder a
b)
  Assert {} -> Pred
pred
  Reifies {} -> Pred
pred
  DependsOn {} -> Pred
pred
  ForAll Term t
t Binder a
b -> forall t a.
(Forallable t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll Term t
t (forall a. Binder a -> Binder a
regularizeBinder Binder a
b)
  Case Term (SumOver as)
t List (Weighted Binder) as
bs -> forall (as :: [*]).
HasSpec (SumOver as) =>
Term (SumOver as) -> List (Weighted Binder) as -> Pred
Case Term (SumOver as)
t (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (forall {k1} {k2} (f :: k1 -> *) (a :: k1) (g :: k2 -> *) (b :: k2).
(f a -> g b) -> Weighted f a -> Weighted g b
mapWeighted forall a. Binder a -> Binder a
regularizeBinder) List (Weighted Binder) as
bs)
  When Term Bool
b Pred
p' -> HasSpec Bool => Term Bool -> Pred -> Pred
When Term Bool
b (Pred -> Pred
regularizeNamesPred Pred
p')
  GenHint {} -> Pred
pred
  TruePred {} -> Pred
pred
  FalsePred {} -> Pred
pred
  Explain NonEmpty String
es Pred
p' -> NonEmpty String -> Pred -> Pred
Explain NonEmpty String
es (Pred -> Pred
regularizeNamesPred Pred
p')

regularizeNames :: Specification a -> Specification a
regularizeNames :: forall a. Specification a -> Specification a
regularizeNames (ExplainSpec [String]
es Specification a
x) = forall a. [String] -> Specification a -> Specification a
explainSpecOpt [String]
es (forall a. Specification a -> Specification a
regularizeNames Specification a
x)
regularizeNames (SuspendedSpec Var a
x Pred
p) =
  forall a. HasSpec a => Var a -> Pred -> Specification a
SuspendedSpec Var a
x' Pred
p'
  where
    Var a
x' :-> Pred
p' = forall a. Binder a -> Binder a
regularizeBinder (Var a
x forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
p)
regularizeNames Specification a
spec = Specification a
spec