{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
-- Monoid Pred and Spec, Pretty and ReName instances
{-# OPTIONS_GHC -Wno-orphans #-}

-- Syntactic operations on types: Term, Pred, Spec, Ctx, etc.
module Test.Minimal.Syntax where

import Constrained.Core (
  Evidence (..),
  Rename (rename),
  Value (..),
  Var (..),
  eqVar,
  freshen,
  unValue,
 )
import Constrained.Env
import Constrained.GenT
import Constrained.Graph
import Constrained.List hiding (ListCtx)
import Control.Monad.Identity
import Control.Monad.Writer (Writer, runWriter, tell)
import qualified Data.Foldable as Foldable (fold, toList)
import Data.Kind
import Data.List (intersect, nub)
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (catMaybes, fromMaybe, isJust, isNothing, listToMaybe)
import qualified Data.Monoid as Monoid
import Data.Semigroup (Any (..), sconcat)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.String (fromString)
import Data.Typeable
import Prettyprinter
import Test.Minimal.Base

-- =======================================
-- Tools for building Spec

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

-- forSome :: (Container t a, HasSpec t, HasSpec a) => Term t -> (Term a -> Pred) -> Pred
-- forSome tm = mkForSome tm . bind

mkForAll ::
  (Container t a, HasSpec t, HasSpec a) =>
  Term t -> Binder a -> Pred
mkForAll :: forall t a.
(Container t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
mkForAll (Lit (t -> [a]
forall t e. Container 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 = Term t -> Binder a -> Pred
forall t a.
(Container t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll Term t
tm Binder a
binder

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

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

notMemberSpec :: forall a f. (HasSpec a, Foldable f) => f a -> Spec a
notMemberSpec :: forall a (f :: * -> *). (HasSpec a, Foldable f) => f a -> Spec a
notMemberSpec f a
x = TypeSpec a -> [a] -> Spec a
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec (forall a. HasSpec a => TypeSpec a
anySpec @a) (f a -> [a]
forall a. f a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList f a
x)

isErrorLike :: forall a. Spec a -> Bool
isErrorLike :: forall a. Spec a -> Bool
isErrorLike Spec a
spec = Maybe (NonEmpty String) -> Bool
forall a. Maybe a -> Bool
isJust (Spec a -> Maybe (NonEmpty String)
forall a. Spec a -> Maybe (NonEmpty String)
hasError Spec a
spec)

hasError :: forall a. Spec a -> Maybe (NonEmpty String)
hasError :: forall a. Spec a -> Maybe (NonEmpty String)
hasError (ErrorSpec NonEmpty String
ss) = NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just NonEmpty String
ss
hasError (TypeSpec TypeSpec a
x [a]
_) =
  case forall a. HasSpec a => TypeSpec a -> Spec a
guardTypeSpec @a TypeSpec a
x of
    ErrorSpec NonEmpty String
ss -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just NonEmpty String
ss
    Spec a
_ -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
hasError Spec a
_ = Maybe (NonEmpty String)
forall a. Maybe a
Nothing

-- | Given two 'Spec', return an 'ErrorSpec' if one or more is an 'ErrorSpec'
--   If neither is an 'ErrorSpec' apply the continuation 'f'
handleErrors :: Spec a -> Spec b -> (Spec a -> Spec b -> Spec c) -> Spec c
handleErrors :: forall a b c.
Spec a -> Spec b -> (Spec a -> Spec b -> Spec c) -> Spec c
handleErrors Spec a
spec1 Spec b
spec2 Spec a -> Spec b -> Spec c
f = case (Spec a -> Maybe (NonEmpty String)
forall a. Spec a -> Maybe (NonEmpty String)
hasError Spec a
spec1, Spec b -> Maybe (NonEmpty String)
forall a. Spec a -> Maybe (NonEmpty String)
hasError Spec b
spec2) of
  (Just NonEmpty String
m1, Just NonEmpty String
m2) -> NonEmpty String -> Spec c
forall a. NonEmpty String -> Spec a
ErrorSpec (NonEmpty String
m1 NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
m2)
  (Just NonEmpty String
m1, Maybe (NonEmpty String)
_) -> NonEmpty String -> Spec c
forall a. NonEmpty String -> Spec a
ErrorSpec NonEmpty String
m1
  (Maybe (NonEmpty String)
_, Just NonEmpty String
m2) -> NonEmpty String -> Spec c
forall a. NonEmpty String -> Spec a
ErrorSpec NonEmpty String
m2
  (Maybe (NonEmpty String)
Nothing, Maybe (NonEmpty String)
Nothing) -> Spec a -> Spec b -> Spec c
f Spec a
spec1 Spec b
spec2

-- =========================================================
-- Conformance of Pred and Spec

-- | Add the explanations, if it's an ErrorSpec, else drop them
addToErrorSpec :: NE.NonEmpty String -> Spec a -> Spec a
addToErrorSpec :: forall a. NonEmpty String -> Spec a -> Spec a
addToErrorSpec NonEmpty String
es (ErrorSpec NonEmpty String
es') = NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec (NonEmpty String
es NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es')
addToErrorSpec NonEmpty String
_ Spec a
s = Spec a
s

-- | return a MemberSpec or ans ErrorSpec depending on if 'xs' the null list or not
memberSpecList :: [a] -> NE.NonEmpty String -> Spec a
memberSpecList :: forall a. [a] -> NonEmpty String -> Spec a
memberSpecList [a]
xs NonEmpty String
messages =
  case [a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
NE.nonEmpty [a]
xs of
    Maybe (NonEmpty a)
Nothing -> NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec NonEmpty String
messages
    Just NonEmpty a
ys -> NonEmpty a -> Spec a
forall a. NonEmpty a -> Spec a
MemberSpec NonEmpty a
ys

satisfies :: forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies :: forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies Term a
_ Spec a
TrueSpec = Pred
TruePred
satisfies Term a
e (MemberSpec NonEmpty a
nonempty) = Bool -> Term a -> NonEmpty a -> Pred
forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
True Term a
e NonEmpty a
nonempty
satisfies Term a
t (SuspendedSpec Var a
x Pred
p) = Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
Subst Var a
x Term a
t Pred
p
satisfies Term a
e (TypeSpec TypeSpec a
s [a]
cant) = case [a]
cant of
  [] -> Term a -> TypeSpec a -> Pred
forall a. HasSpec a => Term a -> TypeSpec a -> Pred
toPreds Term a
e TypeSpec a
s
  (a
c : [a]
cs) -> Bool -> Term a -> NonEmpty a -> Pred
forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
False Term a
e (a
c a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
cs) Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term a -> TypeSpec a -> Pred
forall a. HasSpec a => Term a -> TypeSpec a -> Pred
toPreds Term a
e TypeSpec a
s
satisfies Term a
_ (ErrorSpec NonEmpty String
e) = NonEmpty String -> Pred
FalsePred NonEmpty String
e

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

runTerm :: MonadGenError m => Env -> Term a -> m a
runTerm :: forall (m :: * -> *) a. MonadGenError m => Env -> Term a -> m a
runTerm Env
env Term a
x = case Env -> Term a -> Either (NonEmpty String) a
forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term a
x of
  Left NonEmpty String
msgs -> NonEmpty String -> m a
forall a. HasCallStack => NonEmpty String -> m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE NonEmpty String
msgs
  Right a
val -> a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
val

conformsToSpec :: forall a. HasSpec a => a -> Spec a -> Bool
conformsToSpec :: forall a. HasSpec a => a -> Spec a -> Bool
conformsToSpec a
_ Spec a
TrueSpec = Bool
True
conformsToSpec a
a (MemberSpec NonEmpty a
as) = a -> NonEmpty a -> Bool
forall a. Eq a => a -> NonEmpty a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
a NonEmpty a
as
conformsToSpec a
a (TypeSpec TypeSpec a
s [a]
cant) = a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem a
a [a]
cant Bool -> Bool -> Bool
&& a -> TypeSpec a -> Bool
forall a. (HasSpec a, HasCallStack) => a -> TypeSpec a -> Bool
conformsTo a
a TypeSpec a
s
conformsToSpec a
a (SuspendedSpec Var a
v Pred
ps) = case Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE (Var a -> a -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var a
v a
a) (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"checkPredE") Pred
ps of
  Maybe (NonEmpty String)
Nothing -> Bool
True
  Just NonEmpty String
_ -> Bool
False
conformsToSpec a
_ (ErrorSpec NonEmpty String
_) = Bool
False

checkPredE :: Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE :: Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE Env
env NonEmpty String
msgs = \case
  p :: Pred
p@(ElemPred Bool
bool Term a
t NonEmpty a
xs) ->
    case Env -> Term a -> Either (NonEmpty String) a
forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term a
t of
      Left NonEmpty String
message -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
message)
      Right a
v -> case (a -> NonEmpty a -> Bool
forall a. Eq a => a -> NonEmpty a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
v NonEmpty a
xs, Bool
bool) of
        (Bool
True, Bool
True) -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
        (Bool
True, Bool
False) -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (String
"notElemPred reduces to True" String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [Pred -> String
forall a. Show a => a -> String
show Pred
p])
        (Bool
False, Bool
True) -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (String
"elemPred reduces to False" String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [Pred -> String
forall a. Show a => a -> String
show Pred
p])
        (Bool
False, Bool
False) -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
  Subst Var a
x Term a
t Pred
p -> Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE Env
env NonEmpty String
msgs (Pred -> Maybe (NonEmpty String))
-> Pred -> Maybe (NonEmpty String)
forall a b. (a -> b) -> a -> b
$ Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p
  Assert Term Bool
t -> case Env -> Term Bool -> Either (NonEmpty String) Bool
forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term Bool
t of
    Right Bool
True -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
    Right Bool
False ->
      NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just
        (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"Assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term Bool -> String
forall a. Show a => a -> String
show Term Bool
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" returns False") NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"\nenv=\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Env -> Doc Any
forall ann. Env -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Env
env)))
    Left NonEmpty String
es -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
  ForAll Term t
t (Var a
x :-> Pred
p) -> case Env -> Term t -> Either (NonEmpty String) t
forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term t
t of
    Left NonEmpty String
es -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String -> Maybe (NonEmpty String))
-> NonEmpty String -> Maybe (NonEmpty String)
forall a b. (a -> b) -> a -> b
$ (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String
"checkPredE: ForAll fails to run."] NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
    Right t
set ->
      let answers :: [NonEmpty String]
answers =
            [Maybe (NonEmpty String)] -> [NonEmpty String]
forall a. [Maybe a] -> [a]
catMaybes
              [ Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE Env
env' (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Some items in ForAll fail") Pred
p
              | a
v <- t -> [a]
forall t e. Container t e => t -> [e]
forAllToList t
set
              , let env' :: Env
env' = Var a -> a -> Env -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
v Env
env
              ]
       in case [NonEmpty String]
answers of
            [] -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
            (NonEmpty String
y : [NonEmpty String]
ys) -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String -> NonEmpty String
forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub (NonEmpty (NonEmpty String) -> NonEmpty String
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty String
y NonEmpty String -> [NonEmpty String] -> NonEmpty (NonEmpty String)
forall a. a -> [a] -> NonEmpty a
NE.:| [NonEmpty String]
ys)))
  Case Term (Either a b)
t Binder a
a Binder b
b -> case Env -> Term (Either a b) -> Either (NonEmpty String) (Either a b)
forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term (Either a b)
t of
    Right Either a b
v -> Either a b
-> Binder a
-> Binder b
-> (forall x.
    HasSpec x =>
    Var x -> x -> Pred -> Maybe (NonEmpty String))
-> Maybe (NonEmpty String)
forall a b r.
Either a b
-> Binder a
-> Binder b
-> (forall x. HasSpec x => Var x -> x -> Pred -> r)
-> r
runCaseOn Either a b
v Binder a
a Binder b
b (\Var x
x x
val Pred
ps -> Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE (Var x -> x -> Env -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var x
x x
val Env
env) NonEmpty String
msgs Pred
ps)
    Left NonEmpty String
es -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"checkPredE: Case fails" NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
  Let Term a
t (Var a
x :-> Pred
p) -> case Env -> Term a -> Either (NonEmpty String) a
forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term a
t of
    Right a
val -> Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE (Var a -> a -> Env -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
val Env
env) NonEmpty String
msgs Pred
p
    Left NonEmpty String
es -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"checkPredE: Let fails" NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
  DependsOn {} -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
  Pred
TruePred -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
  FalsePred NonEmpty String
es -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"checkPredE: FalsePred" NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
  And [Pred]
ps ->
    case [Maybe (NonEmpty String)] -> [NonEmpty String]
forall a. [Maybe a] -> [a]
catMaybes ((Pred -> Maybe (NonEmpty String))
-> [Pred] -> [Maybe (NonEmpty String)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE Env
env (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Some items in And  fail")) [Pred]
ps) of
      [] -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
      (NonEmpty String
x : [NonEmpty String]
xs) -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String -> NonEmpty String
forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub (NonEmpty (NonEmpty String) -> NonEmpty String
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty String
x NonEmpty String -> [NonEmpty String] -> NonEmpty (NonEmpty String)
forall a. a -> [a] -> NonEmpty a
NE.:| [NonEmpty String]
xs)))
  Exists (forall b. Term b -> b) -> GE a
k (Var a
x :-> Pred
p) ->
    let eval :: forall b. Term b -> b
        eval :: forall b. Term b -> b
eval Term b
term = case Env -> Term b -> Either (NonEmpty String) b
forall a. Env -> Term a -> Either (NonEmpty String) a
runTermE Env
env Term b
term of
          Right b
v -> b
v
          Left NonEmpty String
es -> String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ NonEmpty String -> [String]
forall a. NonEmpty a -> [a]
NE.toList (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
es)
     in case (forall b. Term b -> b) -> GE a
k Term b -> b
forall b. Term b -> b
eval of
          Result a
a -> Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE (Var a -> a -> Env -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env -> Env
extendEnv Var a
x a
a Env
env) NonEmpty String
msgs Pred
p
          FatalError NonEmpty (NonEmpty String)
es -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty (NonEmpty String) -> NonEmpty String
catMessageList NonEmpty (NonEmpty String)
es)
          GenError NonEmpty (NonEmpty String)
es -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String
msgs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty (NonEmpty String) -> NonEmpty String
catMessageList NonEmpty (NonEmpty String)
es)

runCaseOn ::
  Either a b -> Binder a -> Binder b -> (forall x. HasSpec x => Var x -> x -> Pred -> r) -> r
runCaseOn :: forall a b r.
Either a b
-> Binder a
-> Binder b
-> (forall x. HasSpec x => Var x -> x -> Pred -> r)
-> r
runCaseOn (Left a
a) (Var a
x :-> Pred
xps) (Var b
_ :-> Pred
_) forall x. HasSpec x => Var x -> x -> Pred -> r
f = Var a -> a -> Pred -> r
forall x. HasSpec x => Var x -> x -> Pred -> r
f Var a
x a
a Pred
xps
runCaseOn (Right b
b) (Var a
_ :-> Pred
_) (Var b
y :-> Pred
yps) forall x. HasSpec x => Var x -> x -> Pred -> r
f = Var b -> b -> Pred -> r
forall x. HasSpec x => Var x -> x -> Pred -> r
f Var b
y b
b Pred
yps

-- | Like checkPred, But it takes [Pred] rather than a single Pred,
--   and it builds a much more involved explanation if it fails.
--   Does the Pred evaluate to True under the given Env?
--   If it doesn't, an involved explanation appears in the (Just message)
--   If it does, then it returns Nothing
checkPredsE ::
  NE.NonEmpty String ->
  Env ->
  [Pred] ->
  Maybe (NE.NonEmpty String)
checkPredsE :: NonEmpty String -> Env -> [Pred] -> Maybe (NonEmpty String)
checkPredsE NonEmpty String
msgs Env
env [Pred]
ps =
  case [Maybe (NonEmpty String)] -> [NonEmpty String]
forall a. [Maybe a] -> [a]
catMaybes ((Pred -> Maybe (NonEmpty String))
-> [Pred] -> [Maybe (NonEmpty String)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> NonEmpty String -> Pred -> Maybe (NonEmpty String)
checkPredE Env
env NonEmpty String
msgs) [Pred]
ps) of
    [] -> Maybe (NonEmpty String)
forall a. Maybe a
Nothing
    (NonEmpty String
x : [NonEmpty String]
xs) -> NonEmpty String -> Maybe (NonEmpty String)
forall a. a -> Maybe a
Just (NonEmpty String -> NonEmpty String
forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub (NonEmpty (NonEmpty String) -> NonEmpty String
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty String
x NonEmpty String -> [NonEmpty String] -> NonEmpty (NonEmpty String)
forall a. a -> [a] -> NonEmpty a
NE.:| [NonEmpty String]
xs)))

-- ==========================================================
-- Semigroup and Monoid instances for Syntax Pred and Spec

instance Semigroup Pred where
  FalsePred NonEmpty String
xs <> :: Pred -> Pred -> Pred
<> FalsePred NonEmpty String
ys = NonEmpty String -> Pred
FalsePred (NonEmpty String
xs NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
ys)
  FalsePred NonEmpty String
es <> Pred
_ = NonEmpty String -> Pred
FalsePred NonEmpty String
es
  Pred
_ <> FalsePred NonEmpty String
es = NonEmpty String -> Pred
FalsePred NonEmpty String
es
  Pred
TruePred <> Pred
p = Pred
p
  Pred
p <> Pred
TruePred = Pred
p
  Pred
p <> Pred
p' = [Pred] -> Pred
And (Pred -> [Pred]
unpackPred Pred
p [Pred] -> [Pred] -> [Pred]
forall a. [a] -> [a] -> [a]
++ Pred -> [Pred]
unpackPred Pred
p')
    where
      unpackPred :: Pred -> [Pred]
unpackPred (And [Pred]
ps) = [Pred]
ps
      unpackPred Pred
x = [Pred
x]

instance Monoid Pred where
  mempty :: Pred
mempty = Pred
TruePred

-- Spec instance

instance HasSpec a => Semigroup (Spec a) where
  Spec a
TrueSpec <> :: Spec a -> Spec a -> Spec a
<> Spec a
s = Spec a
s
  Spec a
s <> Spec a
TrueSpec = Spec a
s
  ErrorSpec NonEmpty String
e <> ErrorSpec NonEmpty String
e' =
    NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec
      ( NonEmpty String
e
          NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"------ spec <> spec ------ @" String -> String -> String
forall a. [a] -> [a] -> [a]
++ forall t. Typeable t => String
showType @a)
          NonEmpty String -> NonEmpty String -> NonEmpty String
forall a. Semigroup a => a -> a -> a
<> NonEmpty String
e'
      )
  ErrorSpec NonEmpty String
e <> Spec a
_ = NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec NonEmpty String
e
  Spec a
_ <> ErrorSpec NonEmpty String
e = NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec NonEmpty String
e
  MemberSpec NonEmpty a
as <> MemberSpec NonEmpty a
as' =
    NonEmpty String -> Spec a -> Spec a
forall a. NonEmpty String -> Spec a -> Spec a
addToErrorSpec
      ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
          [String
"Intersecting: ", String
"  MemberSpec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as), String
"  MemberSpec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as')]
      )
      ( [a] -> NonEmpty String -> Spec a
forall a. [a] -> NonEmpty String -> Spec a
memberSpecList
          ([a] -> [a]
forall a. Eq a => [a] -> [a]
nub ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
intersect (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as) (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
as'))
          (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"Empty intersection")
      )
  ms :: Spec a
ms@(MemberSpec NonEmpty a
as) <> ts :: Spec a
ts@TypeSpec {} =
    [a] -> NonEmpty String -> Spec a
forall a. [a] -> NonEmpty String -> Spec a
memberSpecList
      ([a] -> [a]
forall a. Eq a => [a] -> [a]
nub ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ (a -> Bool) -> NonEmpty a -> [a]
forall a. (a -> Bool) -> NonEmpty a -> [a]
NE.filter (a -> Spec a -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
`conformsToSpec` Spec a
ts) NonEmpty a
as)
      ( [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
          [ String
"The two " String -> String -> String
forall a. [a] -> [a] -> [a]
++ forall t. Typeable t => String
showType @a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" Specs are inconsistent."
          , String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Spec a -> String
forall a. Show a => a -> String
show Spec a
ms
          , String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Spec a -> String
forall a. Show a => a -> String
show Spec a
ts
          ]
      )
  TypeSpec TypeSpec a
s [a]
cant <> MemberSpec NonEmpty a
as = NonEmpty a -> Spec a
forall a. NonEmpty a -> Spec a
MemberSpec NonEmpty a
as Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> TypeSpec a -> [a] -> Spec a
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec TypeSpec a
s [a]
cant
  SuspendedSpec Var a
v Pred
p <> SuspendedSpec Var a
v' Pred
p' = Var a -> Pred -> Spec a
forall a. HasSpec a => Var a -> Pred -> Spec a
SuspendedSpec Var a
v (Pred
p Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Var a -> Var a -> Pred -> Pred
forall x. Typeable x => Var x -> Var x -> Pred -> Pred
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var a
v' Var a
v Pred
p')
  SuspendedSpec Var a
v Pred
ps <> Spec a
s = Var a -> Pred -> Spec a
forall a. HasSpec a => Var a -> Pred -> Spec a
SuspendedSpec Var a
v (Pred
ps Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term a -> Spec a -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies (Var a -> Term a
forall a. HasSpec a => Var a -> Term a
V Var a
v) Spec a
s)
  Spec a
s <> SuspendedSpec Var a
v Pred
ps = Var a -> Pred -> Spec a
forall a. HasSpec a => Var a -> Pred -> Spec a
SuspendedSpec Var a
v (Pred
ps Pred -> Pred -> Pred
forall a. Semigroup a => a -> a -> a
<> Term a -> Spec a -> Pred
forall a. HasSpec a => Term a -> Spec a -> Pred
satisfies (Var a -> Term a
forall a. HasSpec a => Var a -> Term a
V Var a
v) Spec a
s)
  TypeSpec TypeSpec a
s [a]
cant <> TypeSpec TypeSpec a
s' [a]
cant' = case TypeSpec a -> TypeSpec a -> Spec a
forall a. HasSpec a => TypeSpec a -> TypeSpec a -> Spec a
combineSpec TypeSpec a
s TypeSpec a
s' of
    -- NOTE: This might look like an unnecessary case, but doing
    -- it like this avoids looping.
    TypeSpec TypeSpec a
s'' [a]
cant'' -> TypeSpec a -> [a] -> Spec a
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec TypeSpec a
s'' ([a]
cant [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [a]
cant' [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [a]
cant'')
    Spec a
s'' -> Spec a
s'' Spec a -> Spec a -> Spec a
forall a. Semigroup a => a -> a -> a
<> [a] -> Spec a
forall a (f :: * -> *). (HasSpec a, Foldable f) => f a -> Spec a
notMemberSpec ([a]
cant [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [a]
cant')

instance HasSpec a => Monoid (Spec a) where
  mempty :: Spec a
mempty = Spec a
forall a. Spec a
TrueSpec

-- ==================================================
-- Syntactic operation Renaming
-- ==================================================

-- Name

data Name where
  Name :: HasSpec a => Var a -> Name

deriving instance Show Name

instance Eq Name where
  Name Var a
v == :: Name -> Name -> Bool
== Name Var a
v' = Maybe (a :~: a) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (a :~: a) -> Bool) -> Maybe (a :~: a) -> Bool
forall a b. (a -> b) -> a -> b
$ Var a -> Var a -> Maybe (a :~: a)
forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
v Var a
v'

-- Instances

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

instance Pretty Name where
  pretty :: forall ann. Name -> Doc ann
pretty (Name Var a
v) = Var a -> Doc ann
forall ann. Var a -> Doc ann
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') = (Int, TypeRep) -> (Int, TypeRep) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Var a -> Int
forall a. Var a -> Int
nameOf Var a
v, Var a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Var a
v) (Var a -> Int
forall a. Var a -> Int
nameOf Var a
v', Var a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Var a
v')

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

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

instance Rename Pred where
  rename :: forall x. Typeable x => Var x -> Var x -> Pred -> Pred
rename Var x
v Var x
v'
    | Var x
v Var x -> Var x -> Bool
forall a. Eq a => a -> a -> Bool
== Var x
v' = Pred -> Pred
forall a. a -> a
id
    | Bool
otherwise = \case
        ElemPred Bool
bool Term a
t NonEmpty a
xs -> Bool -> Term a -> NonEmpty a -> Pred
forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool (Var x -> Var x -> Term a -> Term a
forall x. Typeable x => Var x -> Var x -> Term a -> Term a
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
        Subst Var a
x Term a
t Pred
p -> Var x -> Var x -> Pred -> Pred
forall x. Typeable x => Var x -> Var x -> Pred -> Pred
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Var a -> Term a -> Pred -> Pred
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 (Var x -> Var x -> [Pred] -> [Pred]
forall x. Typeable x => Var x -> Var x -> [Pred] -> [Pred]
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' [Pred]
ps)
        Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
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) -> GE a)
-> (forall b. Term b -> b) -> GE a
forall a b. (a -> b) -> a -> b
$ Term b -> b
forall b. Term b -> b
eval (Term b -> b) -> (Term b -> Term b) -> Term b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var x -> Var x -> Term b -> Term b
forall x. Typeable x => Var x -> Var x -> Term b -> Term b
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v') (Var x -> Var x -> Binder a -> Binder a
forall x. Typeable x => Var x -> Var x -> Binder a -> Binder a
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 -> Term a -> Binder a -> Pred
forall a. Term a -> Binder a -> Pred
Let (Var x -> Var x -> Term a -> Term a
forall x. Typeable x => Var x -> Var x -> Term a -> Term a
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term a
t) (Var x -> Var x -> Binder a -> Binder a
forall x. Typeable x => Var x -> Var x -> Binder a -> Binder a
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Binder a
b)
        DependsOn Term a
x Term b
y -> Term a -> Term b -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn (Var x -> Var x -> Term a -> Term a
forall x. Typeable x => Var x -> Var x -> Term a -> Term a
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term a
x) (Var x -> Var x -> Term b -> Term b
forall x. Typeable x => Var x -> Var x -> Term b -> Term b
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term b
y)
        Assert Term Bool
t -> Term Bool -> Pred
Assert (Var x -> Var x -> Term Bool -> Term Bool
forall x. Typeable x => Var x -> Var x -> Term Bool -> Term Bool
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term Bool
t)
        ForAll Term t
set Binder a
b -> Term t -> Binder a -> Pred
forall t a.
(Container t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll (Var x -> Var x -> Term t -> Term t
forall x. Typeable x => Var x -> Var x -> Term t -> Term t
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term t
set) (Var x -> Var x -> Binder a -> Binder a
forall x. Typeable x => Var x -> Var x -> Binder a -> Binder a
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 (Either a b)
t Binder a
a Binder b
b -> Term (Either a b) -> Binder a -> Binder b -> Pred
forall a b.
HasSpec (Either a b) =>
Term (Either a b) -> Binder a -> Binder b -> Pred
Case (Var x -> Var x -> Term (Either a b) -> Term (Either a b)
forall x.
Typeable x =>
Var x -> Var x -> Term (Either a b) -> Term (Either a b)
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Term (Either a b)
t) (Var x -> Var x -> Binder a -> Binder a
forall x. Typeable x => Var x -> Var x -> Binder a -> Binder a
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Binder a
a) (Var x -> Var x -> Binder b -> Binder b
forall x. Typeable x => Var x -> Var x -> Binder b -> Binder b
forall a x. (Rename a, Typeable x) => Var x -> Var x -> a -> a
rename Var x
v Var x
v' Binder b
b)
        Pred
TruePred -> Pred
TruePred
        FalsePred NonEmpty String
es -> NonEmpty String -> Pred
FalsePred NonEmpty String
es

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

-- ============================================================
-- Syntactic operation: Free variables and variable names
-- ============================================================

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance HasVariables Pred where
  freeVars :: Pred -> FreeVars
freeVars = \case
    ElemPred Bool
_ Term a
t NonEmpty a
_ -> Term a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Term a
t
    -- GenHint _ t -> freeVars t
    Subst Var a
x Term a
t Pred
p -> Term a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Term a
t FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> Pred -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Pred
p FreeVars -> [Name] -> FreeVars
forall (t :: * -> *). Foldable t => FreeVars -> t Name -> FreeVars
`without` [Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x]
    And [Pred]
ps -> (Pred -> FreeVars) -> [Pred] -> FreeVars
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Pred -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars [Pred]
ps
    Exists (forall b. Term b -> b) -> GE a
_ Binder a
b -> Binder a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Binder a
b
    Let Term a
t Binder a
b -> Term a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Term a
t FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> Binder a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Binder a
b
    -- Exists _ b -> freeVars b
    Assert Term Bool
t -> Term Bool -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Term Bool
t
    -- Reifies t' t _ -> freeVars t' <> freeVars t
    DependsOn Term a
x Term b
y -> Term a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Term a
x FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> Term b -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Term b
y
    ForAll Term t
set Binder a
b -> Term t -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Term t
set FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> Binder a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Binder a
b
    Case Term (Either a b)
t Binder a
as Binder b
bs -> Term (Either a b) -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Term (Either a b)
t FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> Binder a -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Binder a
as FreeVars -> FreeVars -> FreeVars
forall a. Semigroup a => a -> a -> a
<> Binder b -> FreeVars
forall a. HasVariables a => a -> FreeVars
freeVars Binder b
bs
    -- When b p -> freeVars b <> freeVars p
    Pred
TruePred -> FreeVars
forall a. Monoid a => a
mempty
    FalsePred NonEmpty String
_ -> FreeVars
forall a. Monoid a => a
mempty

  -- Monitor {} -> mempty
  -- Explain _ p -> freeVars p
  freeVarSet :: Pred -> Set Name
freeVarSet = \case
    ElemPred Bool
_ Term a
t NonEmpty a
_ -> Term a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Term a
t
    -- GenHint _ t -> freeVarSet t
    Subst Var a
x Term a
t Pred
p -> Term a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Term a
t Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Name -> Set Name -> Set Name
forall a. Ord a => a -> Set a -> Set a
Set.delete (Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x) (Pred -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Pred
p)
    And [Pred]
ps -> (Pred -> Set Name) -> [Pred] -> Set Name
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Pred -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet [Pred]
ps
    Exists (forall b. Term b -> b) -> GE a
_ Binder a
b -> Binder a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Binder a
b
    Let Term a
t Binder a
b -> Term a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Term a
t Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Binder a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Binder a
b
    -- Exists _ b -> freeVarSet b
    Assert Term Bool
t -> Term Bool -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Term Bool
t
    -- Reifies t' t _ -> freeVarSet t' <> freeVarSet t
    DependsOn Term a
x Term b
y -> Term a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Term a
x Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Term b -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Term b
y
    ForAll Term t
set Binder a
b -> Term t -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Term t
set Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Binder a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Binder a
b
    Case Term (Either a b)
t Binder a
a Binder b
b -> Term (Either a b) -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Term (Either a b)
t Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Binder a -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Binder a
a Set Name -> Set Name -> Set Name
forall a. Semigroup a => a -> a -> a
<> Binder b -> Set Name
forall a. HasVariables a => a -> Set Name
freeVarSet Binder b
b
    -- When b p -> freeVarSet b <> freeVarSet p
    -- Explain _ p -> freeVarSet p
    Pred
TruePred -> Set Name
forall a. Monoid a => a
mempty
    FalsePred NonEmpty String
_ -> Set Name
forall a. Monoid a => a
mempty

  -- Monitor {} -> mempty
  countOf :: Name -> Pred -> Int
countOf Name
n = \case
    ElemPred Bool
_ Term a
t NonEmpty a
_ -> Name -> Term a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term a
t
    -- GenHint _ t -> countOf n t
    Subst Var a
x Term a
t Pred
p
      | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x -> Name -> Term a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term a
t
      | Bool
otherwise -> Name -> Term a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term a
t Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> Pred -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Pred
p
    And [Pred]
ps -> [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (Pred -> Int) -> [Pred] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Pred -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n) [Pred]
ps
    Let Term a
t Binder a
b -> Name -> Term a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term a
t Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> Binder a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Binder a
b
    Exists (forall b. Term b -> b) -> GE a
_ Binder a
b -> Name -> Binder a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Binder a
b
    Assert Term Bool
t -> Name -> Term Bool -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term Bool
t
    -- Reifies t' t _ -> countOf n t' + countOf n t
    DependsOn Term a
x Term b
y -> Name -> Term a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term a
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> Term b -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term b
y
    ForAll Term t
set Binder a
b -> Name -> Term t -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term t
set Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> Binder a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Binder a
b
    Case Term (Either a b)
t Binder a
a Binder b
b -> Name -> Term (Either a b) -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Term (Either a b)
t Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> Binder a -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Binder a
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Name -> Binder b -> Int
forall a. HasVariables a => Name -> a -> Int
countOf Name
n Binder b
b
    -- When b p -> countOf n b + countOf n p
    -- Explain _ p -> countOf n p
    Pred
TruePred -> Int
0
    FalsePred NonEmpty String
_ -> Int
0

  -- Monitor {} -> 0
  appearsIn :: Name -> Pred -> Bool
appearsIn Name
n = \case
    ElemPred Bool
_ Term a
t NonEmpty a
_ -> Name -> Term a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term a
t
    -- GenHint _ t -> appearsIn n t
    Subst Var a
x Term a
t Pred
p
      | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Var a -> Name
forall a. HasSpec a => Var a -> Name
Name Var a
x -> Name -> Term a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term a
t
      | Bool
otherwise -> Name -> Term a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term a
t Bool -> Bool -> Bool
|| Name -> Pred -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Pred
p
    And [Pred]
ps -> (Pred -> Bool) -> [Pred] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> Pred -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n) [Pred]
ps
    Let Term a
t Binder a
b -> Name -> Term a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term a
t Bool -> Bool -> Bool
|| Name -> Binder a -> 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 -> Name -> Binder a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Binder a
b
    Assert Term Bool
t -> Name -> Term Bool -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term Bool
t
    -- Reifies t' t _ -> appearsIn n t' || appearsIn n t
    DependsOn Term a
x Term b
y -> Name -> Term a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term a
x Bool -> Bool -> Bool
|| Name -> Term b -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term b
y
    ForAll Term t
set Binder a
b -> Name -> Term t -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term t
set Bool -> Bool -> Bool
|| Name -> Binder a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Binder a
b
    Case Term (Either a b)
t Binder a
a Binder b
b -> Name -> Term (Either a b) -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Term (Either a b)
t Bool -> Bool -> Bool
|| Name -> Binder a -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Binder a
a Bool -> Bool -> Bool
|| Name -> Binder b -> Bool
forall a. HasVariables a => Name -> a -> Bool
appearsIn Name
n Binder b
b
    -- When b p -> appearsIn n b || appearsIn n p
    -- Explain _ p -> appearsIn n p
    Pred
TruePred -> Bool
False
    FalsePred NonEmpty String
_ -> Bool
False

-- Monitor {} -> False

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

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

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

-- =========================================================
-- Helpers

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

fromLit :: Term a -> Maybe (Value a)
fromLit :: forall a. Term a -> Maybe (Value a)
fromLit (Lit a
l) = Value a -> Maybe (Value a)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value a -> Maybe (Value a)) -> Value a -> Maybe (Value a)
forall a b. (a -> b) -> a -> b
$ a -> Value a
forall a. Show a => a -> Value a
Value a
l
-- fromLit (To x) = (Value . toSimpleRep . unValue) <$> fromLit x -- MAYBE we don't want to do this?
-- fromLit (From x) = (Value . fromSimpleRep . unValue) <$> fromLit x -- Why not apply unary functions to Lit ?
fromLit Term a
_ = Maybe (Value a)
forall a. Maybe a
Nothing

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

-- =================================================================
-- Syntactic operations Substitutions
-- ============================================================

type Subst = [SubstEntry]

data SubstEntry where
  (:=) :: HasSpec a => Var a -> Term a -> SubstEntry

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

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

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

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

substitutePred :: HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred :: forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm = \case
  ElemPred Bool
bool Term a
t NonEmpty a
xs -> Bool -> Term a -> NonEmpty a -> Pred
forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool (Subst -> Term a -> Term a
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term a
t) NonEmpty a
xs
  -- GenHint h t -> GenHint h (substituteTerm [x := tm] t)
  Subst Var a
x' Term a
t Pred
p -> Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Var a -> Term a -> Pred -> Pred
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 (Subst -> Term Bool -> Term Bool
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term Bool
t)
  And [Pred]
ps -> [Pred] -> Pred
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Foldable.fold (Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
tm (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
  Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
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 (Term b -> b
forall b. Term b -> b
eval (Term b -> b) -> (Term b -> Term b) -> Term b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> Term b -> Term b
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm])) (Var a -> Term a -> Binder a -> Binder a
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 -> Term a -> Binder a -> Pred
forall a. Term a -> Binder a -> Pred
Let (Subst -> Term a -> Term a
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term a
t) (Var a -> Term a -> Binder a -> Binder a
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 -> Term t -> Binder a -> Pred
forall t a.
(Container t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll (Subst -> Term t -> Term t
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term t
t) (Var a -> Term a -> Binder a -> Binder a
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 (Either a b)
t Binder a
as Binder b
bs -> Term (Either a b) -> Binder a -> Binder b -> Pred
forall a b.
HasSpec (Either a b) =>
Term (Either a b) -> Binder a -> Binder b -> Pred
Case (Subst -> Term (Either a b) -> Term (Either a b)
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term (Either a b)
t) (Var a -> Term a -> Binder a -> Binder a
forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm Binder a
as) (Var a -> Term a -> Binder b -> Binder b
forall a b. HasSpec a => Var a -> Term a -> Binder b -> Binder b
substituteBinder Var a
x Term a
tm Binder b
bs)
  -- When b p -> When (substituteTerm [x := tm] b) (substitutePred x tm p)
  -- Reifies t' t f -> Reifies (substituteTerm [x := tm] t') (substituteTerm [x := tm] t) f
  DependsOn Term a
t Term b
t' -> Term a -> Term b -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn (Subst -> Term a -> Term a
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term a
t) (Subst -> Term b -> Term b
forall a. Subst -> Term a -> Term a
substituteTerm [Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
tm] Term b
t')
  Pred
TruePred -> Pred
TruePred
  FalsePred NonEmpty String
es -> NonEmpty String -> Pred
FalsePred NonEmpty String
es

-- Monitor m -> Monitor (\eval -> m (eval . substituteTerm [x := tm]))
-- Explain es p -> Explain es $ substitutePred x tm p

-- =====================================================
-- Substituion under an Env, rather than a single Var
-- It takes Values in the Env, and makes them Literals in the Term.

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

substPred :: Env -> Pred -> Pred
substPred :: Env -> Pred -> Pred
substPred Env
env = \case
  ElemPred Bool
bool Term a
t NonEmpty a
xs -> Bool -> Term a -> NonEmpty a -> Pred
forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool (Env -> Term a -> Term a
forall a. Env -> Term a -> Term a
substTerm Env
env Term a
t) NonEmpty a
xs
  -- GenHint h t -> GenHint h (substTerm env t)
  Subst Var a
x Term a
t Pred
p -> Env -> Pred -> Pred
substPred Env
env (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p
  Assert Term Bool
t -> Term Bool -> Pred
Assert (Env -> Term Bool -> Term Bool
forall a. Env -> Term a -> Term a
substTerm Env
env Term Bool
t)
  -- Reifies t' t f -> Reifies (substTerm env t') (substTerm env t) f
  ForAll Term t
set Binder a
b -> Term t -> Binder a -> Pred
forall t a.
(Container t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll (Env -> Term t -> Term t
forall a. Env -> Term a -> Term a
substTerm Env
env Term t
set) (Env -> Binder a -> Binder a
forall a. Env -> Binder a -> Binder a
substBinder Env
env Binder a
b)
  Case Term (Either a b)
t Binder a
as Binder b
bs -> Term (Either a b) -> Binder a -> Binder b -> Pred
forall a b.
HasSpec (Either a b) =>
Term (Either a b) -> Binder a -> Binder b -> Pred
Case (Env -> Term (Either a b) -> Term (Either a b)
forall a. Env -> Term a -> Term a
substTerm Env
env Term (Either a b)
t) (Env -> Binder a -> Binder a
forall a. Env -> Binder a -> Binder a
substBinder Env
env Binder a
as) (Env -> Binder b -> Binder b
forall a. Env -> Binder a -> Binder a
substBinder Env
env Binder b
bs)
  -- When b p -> When (substTerm env b) (substPred env p)
  DependsOn Term a
x Term b
y -> Term a -> Term b -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn (Env -> Term a -> Term a
forall a. Env -> Term a -> Term a
substTerm Env
env Term a
x) (Env -> Term b -> Term b
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 -> [Pred] -> Pred
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Foldable.fold (Env -> Pred -> Pred
substPred Env
env (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
  Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
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) -> GE a)
-> (forall b. Term b -> b) -> GE a
forall a b. (a -> b) -> a -> b
$ Term b -> b
forall b. Term b -> b
eval (Term b -> b) -> (Term b -> Term b) -> Term b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Term b -> Term b
forall a. Env -> Term a -> Term a
substTerm Env
env) (Env -> Binder a -> Binder a
forall a. Env -> Binder a -> Binder a
substBinder Env
env Binder a
b)
  Let Term a
t Binder a
b -> Term a -> Binder a -> Pred
forall a. Term a -> Binder a -> Pred
Let (Env -> Term a -> Term a
forall a. Env -> Term a -> Term a
substTerm Env
env Term a
t) (Env -> Binder a -> Binder a
forall a. Env -> Binder a -> Binder a
substBinder Env
env Binder a
b)

substSpec :: Env -> Spec a -> Spec a
substSpec :: forall a. Env -> Spec a -> Spec a
substSpec Env
env (SuspendedSpec Var a
v Pred
p) = Var a -> Pred -> Spec a
forall a. HasSpec a => Var a -> Pred -> Spec a
SuspendedSpec Var a
v (Env -> Pred -> Pred
substPred Env
env Pred
p)
substSpec Env
_ Spec a
spec = Spec a
spec

substSolverStage :: Env -> SolverStage -> SolverStage
substSolverStage :: Env -> SolverStage -> SolverStage
substSolverStage Env
env (SolverStage Var a
var [Pred]
preds Spec a
spec) = Var a -> [Pred] -> Spec a -> SolverStage
forall a. HasSpec a => Var a -> [Pred] -> Spec a -> SolverStage
SolverStage Var a
var ((Pred -> Pred) -> [Pred] -> [Pred]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> Pred -> Pred
substPred Env
env) [Pred]
preds) (Env -> Spec a -> Spec a
forall a. Env -> Spec a -> Spec a
substSpec Env
env Spec a
spec)

substPlan :: Env -> SolverPlan -> SolverPlan
substPlan :: Env -> SolverPlan -> SolverPlan
substPlan Env
env (SolverPlan [SolverStage]
stages Graph Name
deps) = [SolverStage] -> Graph Name -> SolverPlan
SolverPlan ((SolverStage -> SolverStage) -> [SolverStage] -> [SolverStage]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> SolverStage -> SolverStage
substSolverStage Env
env) [SolverStage]
stages) Graph Name
deps

-- Monitor m -> Monitor m
-- Explain es p -> Explain es $ substPred env p

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

-- ==================================================
-- Syntactic operation Regularizing
-- ==================================================

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

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

regularizeNamesPred :: Pred -> Pred
regularizeNamesPred :: Pred -> Pred
regularizeNamesPred Pred
pred0 = case Pred
pred0 of
  ElemPred {} -> Pred
pred0
  And [Pred]
ps -> [Pred] -> Pred
And ([Pred] -> Pred) -> [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ (Pred -> Pred) -> [Pred] -> [Pred]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> Pred
regularizeNamesPred [Pred]
ps
  Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (forall b. Term b -> b) -> GE a
k (Binder a -> Binder a
forall a. Binder a -> Binder a
regularizeBinder Binder a
b)
  Subst Var a
v Term a
t Pred
p -> Pred -> Pred
regularizeNamesPred (Var a -> Term a -> Pred -> Pred
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 -> Term a -> Binder a -> Pred
forall a. Term a -> Binder a -> Pred
Let Term a
t (Binder a -> Binder a
forall a. Binder a -> Binder a
regularizeBinder Binder a
b)
  Assert {} -> Pred
pred0
  ForAll Term t
t Binder a
b -> Term t -> Binder a -> Pred
forall t a.
(Container t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll Term t
t (Binder a -> Binder a
forall a. Binder a -> Binder a
regularizeBinder Binder a
b)
  Case Term (Either a b)
t Binder a
as Binder b
bs -> Term (Either a b) -> Binder a -> Binder b -> Pred
forall a b.
HasSpec (Either a b) =>
Term (Either a b) -> Binder a -> Binder b -> Pred
Case Term (Either a b)
t (Binder a -> Binder a
forall a. Binder a -> Binder a
regularizeBinder Binder a
as) (Binder b -> Binder b
forall a. Binder a -> Binder a
regularizeBinder Binder b
bs)
  TruePred {} -> Pred
pred0
  FalsePred {} -> Pred
pred0
  DependsOn {} -> Pred
pred0

-- Explain es p' -> Explain es (regularizeNamesPred p')

regularizeNames :: Spec a -> Spec a
regularizeNames :: forall a. Spec a -> Spec a
regularizeNames (SuspendedSpec Var a
x Pred
p) = Var a -> Pred -> Spec a
forall a. HasSpec a => Var a -> Pred -> Spec a
SuspendedSpec Var a
x' Pred
p'
  where
    Var a
x' :-> Pred
p' = Binder a -> Binder a
forall a. Binder a -> Binder a
regularizeBinder (Var a
x Var a -> Pred -> Binder a
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
p)
regularizeNames Spec a
spec = Spec a
spec

-- ======================================================
-- Simplify

-- | Apply a substitution and simplify the resulting term if the
-- substitution changed the term.
substituteAndSimplifyTerm :: Subst -> Term a -> Term a
substituteAndSimplifyTerm :: forall a. Subst -> Term a -> Term a
substituteAndSimplifyTerm Subst
sub Term a
t =
  case Writer Any (Term a) -> (Term a, Any)
forall w a. Writer w a -> (a, w)
runWriter (Writer Any (Term a) -> (Term a, Any))
-> Writer Any (Term a) -> (Term a, Any)
forall a b. (a -> b) -> a -> b
$ Subst -> Term a -> Writer Any (Term a)
forall a. Subst -> Term a -> Writer Any (Term a)
substituteTerm' Subst
sub Term a
t of
    (Term a
t', Any Bool
b)
      | Bool
b -> Term a -> Term a
forall a. Term a -> Term a
simplifyTerm Term a
t'
      | Bool
otherwise -> Term a
t'

-- | Simplify a Term, if the Term is an 'App', apply the rewrite rules
--   chosen by the (Semantics t)  instance attached to the App
--   to the function witness 'f'
simplifyTerm :: forall a. Term a -> Term a
simplifyTerm :: forall a. Term a -> Term a
simplifyTerm = \case
  V Var a
v -> Var a -> Term a
forall a. HasSpec a => Var a -> Term a
V Var a
v
  Lit a
l -> a -> Term a
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit a
l
  App (t dom a
f :: t bs a) ((forall a. Term a -> Term a) -> List Term dom -> List Term dom
forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList Term a -> Term a
forall a. Term a -> Term a
simplifyTerm -> List Term dom
ts)
    | Just List Value dom
vs <- List Term dom -> Maybe (List Value dom)
forall (as :: [*]). List Term as -> Maybe (List Value as)
fromLits List Term dom
ts -> a -> Term a
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ (forall a. Value a -> a) -> FunTy dom a -> List Value dom -> a
forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(forall a. f a -> a) -> FunTy ts r -> List f ts -> r
forall (f :: * -> *) r.
(forall a. f a -> a) -> FunTy dom r -> List f dom -> r
uncurryList_ Value a -> a
forall a. Value a -> a
unValue (t dom a -> FunTy dom a
forall (d :: [*]) r. t d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t dom a
f) List Value dom
vs
    | Just Term a
t <- t dom a
-> List Term dom
-> Evidence (Typeable a, Eq a, Show a)
-> Maybe (Term a)
forall (ds :: [*]) rng.
(TypeList ds, Typeable ds, HasSpec rng, All HasSpec ds) =>
t ds rng
-> List Term ds
-> Evidence (Typeable rng, Eq rng, Show rng)
-> Maybe (Term rng)
forall (t :: [*] -> * -> *) (ds :: [*]) rng.
(Semantics t, TypeList ds, Typeable ds, HasSpec rng,
 All HasSpec ds) =>
t ds rng
-> List Term ds
-> Evidence (Typeable rng, Eq rng, Show rng)
-> Maybe (Term rng)
rewriteRules t dom a
f List Term dom
ts (forall (c :: Constraint). c => Evidence c
Evidence @(Typeable a, Eq a, Show a)) -> Term a -> Term a
forall a. Term a -> Term a
simplifyTerm Term a
t
    | Bool
otherwise -> t dom a -> List Term dom -> Term a
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

simplifyPred :: Pred -> Pred
simplifyPred :: Pred -> Pred
simplifyPred = \case
  -- If the term simplifies away to a literal, that means there is no
  -- more generation to do so we can get rid of `GenHint`
  p :: Pred
p@(ElemPred Bool
bool Term a
t NonEmpty a
xs) -> case Term a -> Term a
forall a. Term a -> Term a
simplifyTerm Term a
t of
    Lit a
x -> case (a -> NonEmpty a -> Bool
forall a. Eq a => a -> NonEmpty a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
x NonEmpty a
xs, Bool
bool) of
      (Bool
True, Bool
True) -> Pred
TruePred
      (Bool
True, Bool
False) -> NonEmpty String -> Pred
FalsePred (String
"notElemPred reduces to True" String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [Pred -> String
forall a. Show a => a -> String
show Pred
p])
      (Bool
False, Bool
True) -> NonEmpty String -> Pred
FalsePred (String
"elemPred reduces to False" String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [Pred -> String
forall a. Show a => a -> String
show Pred
p])
      (Bool
False, Bool
False) -> Pred
TruePred
    Term a
t' -> Bool -> Term a -> NonEmpty a -> Pred
forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool Term a
t' NonEmpty a
xs
  Subst Var a
x Term a
t Pred
p -> Pred -> Pred
simplifyPred (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p
  Assert Term Bool
t -> Term Bool -> Pred
Assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
forall a. Term a -> Term a
simplifyTerm Term Bool
t
  ForAll (Term t
ts :: Term t) (Binder a
b :: Binder a) -> case Term t -> Term t
forall a. Term a -> Term a
simplifyTerm Term t
ts of
    Lit t
as -> (a -> Pred) -> [a] -> Pred
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (a -> Binder a -> Pred
forall a. a -> Binder a -> Pred
`unBind` Binder a
b) (t -> [a]
forall t e. Container t e => t -> [e]
forAllToList t
as)
    Term t
set' -> case Binder a -> Binder a
forall a. Binder a -> Binder a
simplifyBinder Binder a
b of
      (Var a
_ :-> Pred
TruePred) -> Pred
TruePred
      Binder a
b' -> Term t -> Binder a -> Pred
forall t a.
(Container t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll Term t
set' Binder a
b'
  Case Term (Either a b)
t as :: Binder a
as@(Var a
_ :-> Pred
_) bs :: Binder b
bs@(Var b
_ :-> Pred
_) -> Term (Either a b) -> Binder a -> Binder b -> Pred
forall a b.
HasSpec (Either a b) =>
Term (Either a b) -> Binder a -> Binder b -> Pred
mkCase (Term (Either a b) -> Term (Either a b)
forall a. Term a -> Term a
simplifyTerm Term (Either a b)
t) (Binder a -> Binder a
forall a. Binder a -> Binder a
simplifyBinder Binder a
as) (Binder b -> Binder b
forall a. Binder a -> Binder a
simplifyBinder Binder b
bs)
  Pred
TruePred -> Pred
TruePred
  FalsePred NonEmpty String
es -> NonEmpty String -> Pred
FalsePred NonEmpty String
es
  And [Pred]
ps -> [Pred] -> Pred
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Foldable.fold ([Pred] -> [Pred]
simplifyPreds [Pred]
ps)
  Let Term a
t Binder a
b -> case Term a -> Term a
forall a. Term a -> Term a
simplifyTerm Term a
t of
    t' :: Term a
t'@App {} -> Term a -> Binder a -> Pred
forall a. Term a -> Binder a -> Pred
Let Term a
t' (Binder a -> Binder a
forall a. Binder a -> Binder a
simplifyBinder Binder a
b)
    -- Variable or literal
    Term a
t' | Var a
x :-> Pred
p <- Binder a
b -> Pred -> Pred
simplifyPred (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t' Pred
p
  Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> case Binder a -> Binder a
forall a. Binder a -> Binder a
simplifyBinder Binder a
b of
    Var a
_ :-> Pred
TruePred -> Pred
TruePred
    -- This is to get rid of exisentials like:
    -- `constrained $ \ x -> exists $ \ y -> [x ==. y, y + 2 <. 10]`
    Var a
x :-> Pred
p | Just Term a
t <- Var a -> Pred -> Maybe (Term a)
forall a. HasSpec a => Var a -> Pred -> Maybe (Term a)
pinnedBy Var a
x Pred
p -> Pred -> Pred
simplifyPred (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p
    Binder a
b' -> ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (forall b. Term b -> b) -> GE a
k Binder a
b'
  DependsOn Term a
_ Lit {} -> Pred
TruePred
  DependsOn Lit {} Term b
_ -> Pred
TruePred
  DependsOn Term a
x Term b
y -> Term a -> Term b -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn Term a
x Term b
y

mkCase ::
  HasSpec (Either a b) => Term (Either a b) -> Binder a -> Binder b -> Pred
mkCase :: forall a b.
HasSpec (Either a b) =>
Term (Either a b) -> Binder a -> Binder b -> Pred
mkCase Term (Either a b)
tm Binder a
as Binder b
bs
  -- TODO: all equal maybe?
  | Binder a -> Bool
forall {a}. Binder a -> Bool
isTrueBinder Binder a
as Bool -> Bool -> Bool
&& Binder b -> Bool
forall {a}. Binder a -> Bool
isTrueBinder Binder b
bs = Pred
TruePred
  | Binder a -> Bool
forall {a}. Binder a -> Bool
isFalseBinder Binder a
as Bool -> Bool -> Bool
&& Binder b -> Bool
forall {a}. Binder a -> Bool
isFalseBinder Binder b
bs = NonEmpty String -> Pred
FalsePred (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"mkCase on all False")
  | Lit Either a b
a <- Term (Either a b)
tm = Either a b
-> Binder a
-> Binder b
-> (forall x. HasSpec x => Var x -> x -> Pred -> Pred)
-> Pred
forall a b r.
Either a b
-> Binder a
-> Binder b
-> (forall x. HasSpec x => Var x -> x -> Pred -> r)
-> r
runCaseOn Either a b
a Binder a
as Binder b
bs (\Var x
x x
val Pred
p -> Env -> Pred -> Pred
substPred (Var x -> x -> Env
forall a. (Typeable a, Show a) => Var a -> a -> Env
singletonEnv Var x
x x
val) Pred
p)
  | Bool
otherwise = Term (Either a b) -> Binder a -> Binder b -> Pred
forall a b.
HasSpec (Either a b) =>
Term (Either a b) -> Binder a -> Binder b -> Pred
Case Term (Either a b)
tm Binder a
as Binder b
bs
  where
    isTrueBinder :: Binder a -> Bool
isTrueBinder (Var a
_ :-> Pred
TruePred) = Bool
True
    isTrueBinder (Var a
_ :-> Pred
_) = Bool
False

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

simplifyPreds :: [Pred] -> [Pred]
simplifyPreds :: [Pred] -> [Pred]
simplifyPreds = [Pred] -> [Pred] -> [Pred]
go [] ([Pred] -> [Pred]) -> ([Pred] -> [Pred]) -> [Pred] -> [Pred]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pred -> Pred) -> [Pred] -> [Pred]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> Pred
simplifyPred
  where
    go :: [Pred] -> [Pred] -> [Pred]
go [Pred]
acc [] = [Pred] -> [Pred]
forall a. [a] -> [a]
reverse [Pred]
acc
    go [Pred]
_ (FalsePred NonEmpty String
err : [Pred]
_) = [NonEmpty String -> Pred
FalsePred NonEmpty String
err]
    go [Pred]
acc (Pred
TruePred : [Pred]
ps) = [Pred] -> [Pred] -> [Pred]
go [Pred]
acc [Pred]
ps
    go [Pred]
acc (Pred
p : [Pred]
ps) = [Pred] -> [Pred] -> [Pred]
go (Pred
p Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
acc) [Pred]
ps

simplifyBinder :: Binder a -> Binder a
simplifyBinder :: forall a. Binder a -> Binder a
simplifyBinder (Var a
x :-> Pred
p) = Var a
x Var a -> Pred -> Binder a
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred -> Pred
simplifyPred Pred
p

toPred :: Bool -> Pred
toPred :: Bool -> Pred
toPred Bool
True = Pred
TruePred
toPred Bool
False = NonEmpty String -> Pred
FalsePred (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"toPred False")

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

-- TODO: this can probably be cleaned up and generalized along with generalizing
-- to make sure we float lets in some missing cases.
letFloating :: Pred -> Pred
letFloating :: Pred -> Pred
letFloating = [Pred] -> Pred
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Foldable.fold ([Pred] -> Pred) -> (Pred -> [Pred]) -> Pred -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pred] -> Pred -> [Pred]
go []
  where
    goBlock :: [Pred] -> [Pred] -> [Pred]
goBlock [Pred]
ctx [Pred]
ps = Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' ([Pred] -> Set Int
forall t. HasVariables t => t -> Set Int
freeVarNames [Pred]
ctx Set Int -> Set Int -> Set Int
forall a. Semigroup a => a -> a -> a
<> [Pred] -> Set Int
forall t. HasVariables t => t -> Set Int
freeVarNames [Pred]
ps) [Pred]
ctx [Pred]
ps

    goBlock' :: Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' Set Int
_ [Pred]
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`
      [Term a -> Binder a -> Pred
forall a. Term a -> Binder a -> Pred
Let Term a
t (Var a
x' Var a -> Pred -> Binder a
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> [Pred] -> Pred
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
Foldable.fold (Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' (Int -> Set Int -> Set Int
forall a. Ord a => a -> Set a -> Set a
Set.insert (Var a -> Int
forall a. Var a -> Int
nameOf Var a
x') Set Int
fvs) [Pred]
ctx (Pred
p' Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ps)))]
      where
        (Var a
x', Pred
p') = Var a -> Pred -> Set Int -> (Var a, Pred)
forall a t.
(Typeable a, Rename t) =>
Var a -> t -> Set Int -> (Var a, t)
freshen Var a
x Pred
p Set Int
fvs
    goBlock' Set Int
fvs [Pred]
ctx (And [Pred]
ps : [Pred]
ps') = Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' Set Int
fvs [Pred]
ctx ([Pred]
ps [Pred] -> [Pred] -> [Pred]
forall a. [a] -> [a] -> [a]
++ [Pred]
ps')
    goBlock' Set Int
fvs [Pred]
ctx (Pred
p : [Pred]
ps) = Set Int -> [Pred] -> [Pred] -> [Pred]
goBlock' Set Int
fvs (Pred
p Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx) [Pred]
ps

    go :: [Pred] -> Pred -> [Pred]
go [Pred]
ctx = \case
      ElemPred Bool
bool Term a
t NonEmpty a
xs -> Bool -> Term a -> NonEmpty a -> Pred
forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool Term a
t NonEmpty a
xs Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      And [Pred]
ps0 -> [Pred] -> [Pred] -> [Pred]
goBlock [Pred]
ctx ((Pred -> Pred) -> [Pred] -> [Pred]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> Pred
letFloating [Pred]
ps0)
      Exists (forall b. Term b -> b) -> GE a
k (Var a
x :-> Pred
p) -> [Pred] -> (Binder a -> Pred) -> Var a -> Pred -> [Pred]
forall a.
HasSpec a =>
[Pred] -> (Binder a -> Pred) -> Var a -> Pred -> [Pred]
goExists [Pred]
ctx (((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
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)
      Let Term a
t (Var a
x :-> Pred
p) -> [Pred] -> [Pred] -> [Pred]
goBlock [Pred]
ctx [Term a -> Binder a -> Pred
forall a. Term a -> Binder a -> Pred
Let Term a
t (Var a
x Var a -> Pred -> Binder a
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred -> Pred
letFloating Pred
p)]
      Subst Var a
x Term a
t Pred
p -> [Pred] -> Pred -> [Pred]
go [Pred]
ctx (Var a -> Term a -> Pred -> Pred
forall a. HasSpec a => Var a -> Term a -> Pred -> Pred
substitutePred Var a
x Term a
t Pred
p)
      ForAll Term t
t (Var a
x :-> Pred
p) -> Term t -> Binder a -> Pred
forall t a.
(Container t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll Term t
t (Var a
x Var a -> Pred -> Binder a
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred -> Pred
letFloating Pred
p) Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      Case Term (Either a b)
t (Var a
x :-> Pred
px) (Var b
y :-> Pred
py) -> Term (Either a b) -> Binder a -> Binder b -> Pred
forall a b.
HasSpec (Either a b) =>
Term (Either a b) -> Binder a -> Binder b -> Pred
Case Term (Either a b)
t (Var a
x Var a -> Pred -> Binder a
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred -> Pred
letFloating Pred
px) (Var b
y Var b -> Pred -> Binder b
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred -> Pred
letFloating Pred
py) Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      Assert Term Bool
t -> Term Bool -> Pred
Assert Term Bool
t Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      Pred
TruePred -> Pred
TruePred Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      FalsePred NonEmpty String
es -> NonEmpty String -> Pred
FalsePred NonEmpty String
es Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx
      DependsOn Term a
t Term b
t' -> Term a -> Term b -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn Term a
t Term b
t' Pred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
: [Pred]
ctx

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

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

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

    go :: Subst -> Pred -> Pred
go Subst
sub = \case
      ElemPred Bool
bool Term a
t NonEmpty a
xs -> Bool -> Term a -> NonEmpty a -> Pred
forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
ElemPred Bool
bool (Subst -> Term a -> Term a
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term a
t) NonEmpty a
xs
      And [Pred]
ps -> [Pred] -> Pred
And (Subst -> Pred -> Pred
go Subst
sub (Pred -> Pred) -> [Pred] -> [Pred]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred]
ps)
      Exists (forall b. Term b -> b) -> GE a
k Binder a
b -> ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
forall a. ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
Exists (forall b. Term b -> b) -> GE a
k (Subst -> Binder a -> Binder a
forall a. Subst -> Binder a -> Binder a
goBinder Subst
sub Binder a
b)
      Let Term a
t (Var a
x :-> Pred
p) -> Term a -> Binder a -> Pred
forall a. Term a -> Binder a -> Pred
Let Term a
t' (Var a
x Var a -> Pred -> Binder a
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Subst -> Pred -> Pred
go (Var a
x Var a -> Term a -> SubstEntry
forall a. HasSpec a => Var a -> Term a -> SubstEntry
:= Term a
t' SubstEntry -> Subst -> Subst
forall a. a -> [a] -> [a]
: Subst
sub') Pred
p)
        where
          t' :: Term a
t' = Subst -> Term a -> Term a
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term a
t
          sub' :: Subst
sub' = Var a -> Subst -> Subst
forall {a}. HasSpec a => Var a -> Subst -> Subst
adjustSub Var a
x Subst
sub
      Subst Var a
x Term a
t Pred
p -> Subst -> Pred -> Pred
go Subst
sub (Var a -> Term a -> Pred -> Pred
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 (Subst -> Term Bool -> Term Bool
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term Bool
t)
      ForAll Term t
t Binder a
b -> Term t -> Binder a -> Pred
forall t a.
(Container t a, HasSpec t, HasSpec a) =>
Term t -> Binder a -> Pred
ForAll (Subst -> Term t -> Term t
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term t
t) (Subst -> Binder a -> Binder a
forall a. Subst -> Binder a -> Binder a
goBinder Subst
sub Binder a
b)
      Case Term (Either a b)
t Binder a
as Binder b
bs -> Term (Either a b) -> Binder a -> Binder b -> Pred
forall a b.
HasSpec (Either a b) =>
Term (Either a b) -> Binder a -> Binder b -> Pred
Case (Subst -> Term (Either a b) -> Term (Either a b)
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term (Either a b)
t) (Subst -> Binder a -> Binder a
forall a. Subst -> Binder a -> Binder a
goBinder Subst
sub Binder a
as) (Subst -> Binder b -> Binder b
forall a. Subst -> Binder a -> Binder a
goBinder Subst
sub Binder b
bs)
      Pred
TruePred -> Pred
TruePred
      FalsePred NonEmpty String
es -> NonEmpty String -> Pred
FalsePred NonEmpty String
es
      DependsOn Term a
t Term b
t' -> Term a -> Term b -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
DependsOn (Subst -> Term a -> Term a
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term a
t) (Subst -> Term b -> Term b
forall a. HasSpec a => Subst -> Term a -> Term a
backwardsSubstitution Subst
sub Term b
t')

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

data SolverStage where
  SolverStage ::
    HasSpec a =>
    { ()
stageVar :: Var a
    , SolverStage -> [Pred]
stagePreds :: [Pred]
    , ()
stageSpec :: Spec a
    } ->
    SolverStage

instance Pretty SolverStage where
  pretty :: forall ann. SolverStage -> Doc ann
pretty SolverStage {[Pred]
Var a
Spec a
stageVar :: ()
stagePreds :: SolverStage -> [Pred]
stageSpec :: ()
stageVar :: Var a
stagePreds :: [Pred]
stageSpec :: Spec a
..} =
    (Var a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Var a
stageVar Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"<-")
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
/> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep'
        ( [Spec a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Spec a -> Doc ann
pretty Spec a
stageSpec | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Spec a -> Bool
forall a. Spec a -> Bool
isTrueSpec Spec a
stageSpec]
            [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ ((Pred -> Doc ann) -> [Pred] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Pred -> Doc ann
pretty [Pred]
stagePreds)
            [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [Doc ann
"---"]
        )

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

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

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

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

-- ==========================================================
-- The equality function symbol (==.)

data EqSym :: [Type] -> Type -> Type where
  EqualW :: (Eq a, HasSpec a) => EqSym '[a, a] Bool

deriving instance Eq (EqSym dom rng)

instance Show (EqSym d r) where
  show :: EqSym d r -> String
show EqSym d r
EqualW = String
"==."

instance Syntax EqSym where
  inFix :: forall (dom :: [*]) rng. EqSym dom rng -> Bool
inFix EqSym dom rng
EqualW = Bool
True
  name :: forall (d :: [*]) r. EqSym d r -> String
name EqSym dom rng
EqualW = String
"==."

instance Semantics EqSym where
  semantics :: forall (d :: [*]) r. EqSym d r -> FunTy d r
semantics EqSym d r
EqualW = FunTy d r
a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

  rewriteRules :: forall (ds :: [*]) rng.
(TypeList ds, Typeable ds, HasSpec rng, All HasSpec ds) =>
EqSym ds rng
-> List Term ds
-> Evidence (Typeable rng, Eq rng, Show rng)
-> Maybe (Term rng)
rewriteRules EqSym ds rng
EqualW (Term a
t :> Term a
t' :> List Term as1
Nil) Evidence (Typeable rng, Eq rng, Show rng)
Evidence
    | Term a
t Term a -> Term a -> Bool
forall a. Eq a => a -> a -> Bool
== Term a
Term a
t' = Term rng -> Maybe (Term rng)
forall a. a -> Maybe a
Just (Term rng -> Maybe (Term rng)) -> Term rng -> Maybe (Term rng)
forall a b. (a -> b) -> a -> b
$ rng -> Term rng
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit rng
Bool
True
  rewriteRules t :: EqSym ds rng
t@EqSym ds rng
EqualW List Term ds
l Evidence (Typeable rng, Eq rng, Show rng)
Evidence = rng -> Term rng
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit (rng -> Term rng) -> Maybe rng -> Maybe (Term rng)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: [*] -> * -> *) (ds :: [*]) rng.
(Typeable rng, Eq rng, Show rng, Semantics t) =>
FunTy ds rng -> List Term ds -> Maybe rng
applyFunSym @EqSym (EqSym ds rng -> FunTy ds rng
forall (d :: [*]) r. EqSym d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics EqSym ds rng
t) List Term ds
l)

-- We don't need a HasSpec instance, since we can make equality specs at any type
-- using just MemberSpec and TypeSpec

equalSpec :: a -> Spec a
equalSpec :: forall a. a -> Spec a
equalSpec = NonEmpty a -> Spec a
forall a. NonEmpty a -> Spec a
MemberSpec (NonEmpty a -> Spec a) -> (a -> NonEmpty a) -> a -> Spec a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> NonEmpty a
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

notEqualSpec :: forall a. HasSpec a => a -> Spec a
notEqualSpec :: forall a. HasSpec a => a -> Spec a
notEqualSpec a
n = TypeSpec a -> [a] -> Spec a
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec (forall a. HasSpec a => TypeSpec a
anySpec @a) [a
n]

caseBoolSpec :: (HasSpec Bool, HasSpec a) => Spec Bool -> (Bool -> Spec a) -> Spec a
caseBoolSpec :: forall a.
(HasSpec Bool, HasSpec a) =>
Spec Bool -> (Bool -> Spec a) -> Spec a
caseBoolSpec Spec Bool
spec Bool -> Spec a
cont = case Spec Bool -> [Bool]
possibleValues Spec Bool
spec of
  [] -> NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec ([String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [String
"No possible values in caseBoolSpec"])
  [Bool
b] -> Bool -> Spec a
cont Bool
b
  [Bool]
_ -> Spec a
forall a. Monoid a => a
mempty
  where
    possibleValues :: Spec Bool -> [Bool]
possibleValues Spec Bool
s = (Bool -> Bool) -> [Bool] -> [Bool]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Bool -> Spec Bool -> Bool) -> Spec Bool -> Bool -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Bool -> Spec Bool -> Bool
forall a. HasSpec a => a -> Spec a -> Bool
conformsToSpec Spec Bool
s) [Bool
True, Bool
False]

instance Logic EqSym where
  propagate :: forall (as :: [*]) b a.
(AppRequires EqSym as b, HasSpec a) =>
EqSym as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
propagate EqSym as b
tag ListCtx as (HOLE a)
ctx Spec b
spec = case (EqSym as b
tag, ListCtx as (HOLE a)
ctx, Spec b
spec) of
    (EqSym as b
_, ListCtx as (HOLE a)
_, Spec b
TrueSpec) -> Spec a
forall a. Spec a
TrueSpec
    (EqSym as b
_, ListCtx as (HOLE a)
_, ErrorSpec NonEmpty String
msgs) -> NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec NonEmpty String
msgs
    (EqSym as b
f, ListCtx as (HOLE a)
context, SuspendedSpec Var b
v Pred
ps) -> (Term a -> Pred) -> Spec a
forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained ((Term a -> Pred) -> Spec a) -> (Term a -> Pred) -> Spec a
forall a b. (a -> b) -> a -> b
$ \Term a
v' -> Term b -> Binder b -> Pred
forall a. Term a -> Binder a -> Pred
Let (EqSym as b -> List Term as -> Term b
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App EqSym as b
f (ListCtx as (HOLE a) -> Term a -> List Term as
forall (as :: [*]) a.
All HasSpec as =>
ListCtx as (HOLE a) -> Term a -> List Term as
fromListCtx ListCtx as (HOLE a)
context Term a
v')) (Var b
v Var b -> Pred -> Binder b
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
    (EqSym as b
EqualW, HOLE a b
HOLE :<| x
s, Spec b
bspec) -> Spec Bool -> (Bool -> Spec a) -> Spec a
forall a.
(HasSpec Bool, HasSpec a) =>
Spec Bool -> (Bool -> Spec a) -> Spec a
caseBoolSpec Spec b
Spec Bool
bspec ((Bool -> Spec a) -> Spec a) -> (Bool -> Spec a) -> Spec a
forall a b. (a -> b) -> a -> b
$ \case
      Bool
True -> a -> Spec a
forall a. a -> Spec a
equalSpec a
x
s
      Bool
False -> a -> Spec a
forall a. HasSpec a => a -> Spec a
notEqualSpec a
x
s
    (EqSym as b
EqualW, x
s :|> HOLE a b
HOLE, Spec b
bspec) -> Spec Bool -> (Bool -> Spec a) -> Spec a
forall a.
(HasSpec Bool, HasSpec a) =>
Spec Bool -> (Bool -> Spec a) -> Spec a
caseBoolSpec Spec b
Spec Bool
bspec ((Bool -> Spec a) -> Spec a) -> (Bool -> Spec a) -> Spec a
forall a b. (a -> b) -> a -> b
$ \case
      Bool
True -> a -> Spec a
forall a. a -> Spec a
equalSpec a
x
s
      Bool
False -> a -> Spec a
forall a. HasSpec a => a -> Spec a
notEqualSpec a
x
s

infix 4 ==.

(==.) :: (HasSpec Bool, HasSpec a) => Term a -> Term a -> Term Bool
==. :: forall a.
(HasSpec Bool, HasSpec a) =>
Term a -> Term a -> Term Bool
(==.) Term a
x Term a
y = EqSym '[a, a] Bool -> List Term '[a, a] -> Term Bool
forall (t :: [*] -> * -> *) (dom :: [*]) a.
AppRequires t dom a =>
t dom a -> List Term dom -> Term a
App EqSym '[a, a] Bool
forall a. (Eq a, HasSpec a) => EqSym '[a, a] Bool
EqualW (Term a
x Term a -> List Term '[a] -> List Term '[a, a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term a
y Term a -> List Term '[] -> List Term '[a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term '[]
forall {k} (f :: k -> *). List f '[]
Nil)

getWitness :: forall t t' d r. (AppRequires t d r, Typeable t') => t d r -> Maybe (t' d r)
getWitness :: forall (t :: [*] -> * -> *) (t' :: [*] -> * -> *) (d :: [*]) r.
(AppRequires t d r, Typeable t') =>
t d r -> Maybe (t' d r)
getWitness = t d r -> Maybe (t' d r)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast

pattern Equal ::
  forall b.
  () =>
  forall a.
  (b ~ Bool, Eq a, HasSpec a) =>
  Term a ->
  Term a ->
  Term b
pattern $mEqual :: forall {r} {b}.
Term b
-> (forall {a}.
    (b ~ Bool, Eq a, HasSpec a) =>
    Term a -> Term a -> r)
-> ((# #) -> r)
-> r
Equal x y <-
  ( App
      (getWitness -> Just EqualW)
      (x :> y :> Nil)
    )

-- | Is the variable x pinned to some free term in p? (free term
-- meaning that all the variables in the term are free in p).
--
-- TODO: complete this with more cases!
pinnedBy :: forall a. HasSpec a => Var a -> Pred -> Maybe (Term a)
-- pinnedBy x (Assert (App (extractFn @EqFn @fn -> Just EqualW) (t :> t' :> Nil)))
pinnedBy :: forall a. HasSpec a => Var a -> Pred -> Maybe (Term a)
pinnedBy Var a
x (Assert (Equal Term a
t Term a
t'))
  | V Var a
x' <- Term a
t, Just a :~: a
Refl <- Var a -> Var a -> Maybe (a :~: a)
forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var a
x' = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
Term a
t'
  | V Var a
x' <- Term a
t', Just a :~: a
Refl <- Var a -> Var a -> Maybe (a :~: a)
forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var a
x Var a
x' = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
Term a
t
pinnedBy Var a
x (And [Pred]
ps) = [Term a] -> Maybe (Term a)
forall a. [a] -> Maybe a
listToMaybe ([Term a] -> Maybe (Term a)) -> [Term a] -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ [Maybe (Term a)] -> [Term a]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (Term a)] -> [Term a]) -> [Maybe (Term a)] -> [Term a]
forall a b. (a -> b) -> a -> b
$ (Pred -> Maybe (Term a)) -> [Pred] -> [Maybe (Term a)]
forall a b. (a -> b) -> [a] -> [b]
map (Var a -> Pred -> Maybe (Term a)
forall a. HasSpec a => Var a -> Pred -> Maybe (Term a)
pinnedBy Var a
x) [Pred]
ps
pinnedBy Var a
_ Pred
_ = Maybe (Term a)
forall a. Maybe a
Nothing