{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

-- Base types: Term, Pred, Spec, Ctx, and classes: HasSpec, Syntax, Semantics, and Logic for the MinModel
module Test.Minimal.Base where

import Constrained.Core (Evidence (..), Var (..), eqVar)
import Constrained.GenT
import Constrained.List hiding (ListCtx)
import Data.Kind
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import Data.String (fromString)
import Data.Typeable
import GHC.Stack
import Prettyprinter

-- ===========================================
-- Terms
-- ===========================================

type AppRequires t dom rng =
  ( Logic t
  , TypeList dom
  , Eq (t dom rng)
  , Show (t dom rng)
  , Typeable dom
  , Typeable rng
  , All HasSpec dom
  , HasSpec rng
  )

data Term a where
  App ::
    forall t dom rng.
    AppRequires t dom rng =>
    t dom rng ->
    List Term dom ->
    Term rng
  Lit :: (Typeable a, Eq a, Show a) => a -> Term a
  V :: HasSpec a => Var a -> Term a

instance Eq (Term a) where
  V Var a
x == :: Term a -> Term a -> Bool
== V Var a
x' = Var a
x Var a -> Var a -> Bool
forall a. Eq a => a -> a -> Bool
== Var a
x'
  Lit a
a == Lit a
b = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
  App (t dom a
w1 :: x1) (List Term dom
ts :: List Term dom1) == App (t dom a
w2 :: x2) (List Term dom
ts' :: List Term dom2) =
    case (forall (a :: [*]) (b :: [*]).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @dom1 @dom2, forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @x1 @x2) of
      (Just dom :~: dom
Refl, Just t dom a :~: t dom a
Refl) ->
        t dom a
w1 t dom a -> t dom a -> Bool
forall a. Eq a => a -> a -> Bool
== t dom a
t dom a
w2
          Bool -> Bool -> Bool
&& List Term dom -> List Term dom -> Bool
forall (as :: [*]).
All HasSpec as =>
List Term as -> List Term as -> Bool
sameTerms List Term dom
ts List Term dom
List Term dom
ts'
      (Maybe (dom :~: dom), Maybe (t dom a :~: t dom a))
_ -> Bool
False
  Term a
_ == Term a
_ = Bool
False

-- | If the list is composed solely of literals, apply the function to get a value
applyFunSym ::
  forall t ds rng.
  (Typeable rng, Eq rng, Show rng, Semantics t) => FunTy ds rng -> List Term ds -> Maybe rng
applyFunSym :: forall (t :: [*] -> * -> *) (ds :: [*]) rng.
(Typeable rng, Eq rng, Show rng, Semantics t) =>
FunTy ds rng -> List Term ds -> Maybe rng
applyFunSym FunTy ds rng
f List Term ds
Nil = rng -> Maybe rng
forall a. a -> Maybe a
Just rng
FunTy ds rng
f
applyFunSym FunTy ds rng
f (Lit a
x :> List Term as1
xs) = forall (t :: [*] -> * -> *) (ds :: [*]) rng.
(Typeable rng, Eq rng, Show rng, Semantics t) =>
FunTy ds rng -> List Term ds -> Maybe rng
applyFunSym @t (FunTy ds rng
a -> FunTy as1 rng
f a
x) List Term as1
xs
applyFunSym FunTy ds rng
_ List Term ds
_ = Maybe rng
forall a. Maybe a
Nothing

reducesToLit :: Term a -> Maybe a
reducesToLit :: forall a. Term a -> Maybe a
reducesToLit (Lit a
n) = a -> Maybe a
forall a. a -> Maybe a
Just a
n
reducesToLit (V Var a
_) = Maybe a
forall a. Maybe a
Nothing
reducesToLit (App (t dom a
f :: t ds r) List Term dom
xs) = forall (t :: [*] -> * -> *) (ds :: [*]) rng.
(Typeable rng, Eq rng, Show rng, Semantics t) =>
FunTy ds rng -> List Term ds -> Maybe rng
applyFunSym @t (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 Term dom
xs

-- How to compare the args of two applications for equality
sameTerms :: All HasSpec as => List Term as -> List Term as -> Bool
sameTerms :: forall (as :: [*]).
All HasSpec as =>
List Term as -> List Term as -> Bool
sameTerms List Term as
Nil List Term as
Nil = Bool
True
sameTerms (Term a
x :> List Term as1
xs) (Term a
y :> List Term as1
ys) = Term a
x Term a -> Term a -> Bool
forall a. Eq a => a -> a -> Bool
== Term a
Term a
y Bool -> Bool -> Bool
&& List Term as1 -> List Term as1 -> Bool
forall (as :: [*]).
All HasSpec as =>
List Term as -> List Term as -> Bool
sameTerms List Term as1
xs List Term as1
List Term as1
ys

-- ===========================================
-- Function Symbol Classes
-- ===========================================

-- | Syntactic operations are ones that have to do with the structure and appearence of the type.
class Syntax (t :: [Type] -> Type -> Type) where
  inFix :: forall dom rng. t dom rng -> Bool
  inFix t dom rng
_ = Bool
False
  name :: forall dom rng. t dom rng -> String

-- | Semantic operations are ones that give the function symbol, meaning as a function.
--   I.e. how to apply the function to a list of arguments and return a value,
--   or to apply meaning preserving rewrite rules.
class Syntax t => Semantics (t :: [Type] -> Type -> Type) where
  semantics :: forall d r. t d r -> FunTy d r -- e.g. FunTy '[a,Int] Bool == a -> Int -> Bool
  rewriteRules ::
    forall ds rng.
    (TypeList ds, Typeable ds, HasSpec rng, All HasSpec ds) =>
    t ds rng -> List Term ds -> Evidence (Typeable rng, Eq rng, Show rng) -> Maybe (Term rng)
  rewriteRules t ds rng
t 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 @t (t ds rng -> FunTy ds rng
forall (d :: [*]) r. t d r -> FunTy d r
forall (t :: [*] -> * -> *) (d :: [*]) r.
Semantics t =>
t d r -> FunTy d r
semantics t ds rng
t) List Term ds
l)

-- | Logical operations are one that support reasoning about how a function symbol
--   relates to logical properties, that we call Spec's
class (Typeable t, Syntax t, Semantics t) => Logic (t :: [Type] -> Type -> Type) where
  {-# MINIMAL propagate | (propagateTypeSpec, propagateMemberSpec) #-}

  propagateTypeSpec ::
    (AppRequires t as b, HasSpec a) =>
    t as b -> ListCtx as (HOLE a) -> TypeSpec b -> [b] -> Spec a
  propagateTypeSpec t as b
f ListCtx as (HOLE a)
ctx TypeSpec b
ts [b]
cant = t as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
forall (as :: [*]) b a.
(AppRequires t as b, HasSpec a) =>
t as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
propagate t as b
f ListCtx as (HOLE a)
ctx (TypeSpec b -> [b] -> Spec b
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec TypeSpec b
ts [b]
cant)

  propagateMemberSpec ::
    (AppRequires t as b, HasSpec a) =>
    t as b -> ListCtx as (HOLE a) -> NonEmpty b -> Spec a
  propagateMemberSpec t as b
f ListCtx as (HOLE a)
ctx NonEmpty b
xs = t as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
forall (as :: [*]) b a.
(AppRequires t as b, HasSpec a) =>
t as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
propagate t as b
f ListCtx as (HOLE a)
ctx (NonEmpty b -> Spec b
forall a. NonEmpty a -> Spec a
MemberSpec NonEmpty b
xs)

  propagate ::
    (AppRequires t as b, HasSpec a) =>
    t as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
  propagate t as b
_ ListCtx as (HOLE a)
_ Spec b
TrueSpec = Spec a
forall a. Spec a
TrueSpec
  propagate t as b
_ ListCtx as (HOLE a)
_ (ErrorSpec NonEmpty String
es) = NonEmpty String -> Spec a
forall a. NonEmpty String -> Spec a
ErrorSpec NonEmpty String
es
  propagate t as b
f ListCtx as (HOLE a)
ctx (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 fn. Term fn -> Binder fn -> Pred
Let (t as b -> List Term as -> Term b
forall (fn :: [*] -> * -> *) (as :: [*]) rng.
AppRequires fn as rng =>
fn as rng -> List Term as -> Term rng
App t 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)
ctx Term a
v')) (Var b
v Var b -> Pred -> Binder b
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
ps)
  propagate t as b
f ListCtx as (HOLE a)
ctx (TypeSpec TypeSpec b
ts [b]
cant) = t as b -> ListCtx as (HOLE a) -> TypeSpec b -> [b] -> Spec a
forall (as :: [*]) b a.
(AppRequires t as b, HasSpec a) =>
t as b -> ListCtx as (HOLE a) -> TypeSpec b -> [b] -> Spec a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b -> ListCtx as (HOLE a) -> TypeSpec b -> [b] -> Spec a
propagateTypeSpec t as b
f ListCtx as (HOLE a)
ctx TypeSpec b
ts [b]
cant
  propagate t as b
f ListCtx as (HOLE a)
ctx (MemberSpec NonEmpty b
xs) = t as b -> ListCtx as (HOLE a) -> NonEmpty b -> Spec a
forall (as :: [*]) b a.
(AppRequires t as b, HasSpec a) =>
t as b -> ListCtx as (HOLE a) -> NonEmpty b -> Spec a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b -> ListCtx as (HOLE a) -> NonEmpty b -> Spec a
propagateMemberSpec t as b
f ListCtx as (HOLE a)
ctx NonEmpty b
xs

-- ===========================
-- Pred
-- ===========================

data Pred where
  ElemPred :: forall a. HasSpec a => Bool -> Term a -> NonEmpty a -> Pred
  And :: [Pred] -> Pred
  Exists :: ((forall b. Term b -> b) -> GE a) -> Binder a -> Pred
  ForAll :: (Container t a, HasSpec t, HasSpec a) => Term t -> Binder a -> Pred
  DependsOn :: (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
  Assert :: Term Bool -> Pred
  TruePred :: Pred
  FalsePred :: NonEmpty String -> Pred
  Case :: HasSpec (Either a b) => Term (Either a b) -> Binder a -> Binder b -> Pred
  Let :: Term a -> Binder a -> Pred
  Subst :: HasSpec a => Var a -> Term a -> Pred -> Pred

data Binder a where
  (:->) :: HasSpec a => Var a -> Pred -> Binder a

class Container t e | t -> e where
  fromForAllSpec :: (HasSpec t, HasSpec e) => Spec e -> Spec t
  forAllToList :: t -> [e]

data Binders as where
  Binds :: All HasSpec as => List Var as -> Pred -> Binders as

data Bind a where
  Bind :: HasSpec a => {forall a. Bind a -> Var a
varBind :: Var a, forall a. Bind a -> Term a
termBind :: Term a} -> Bind a

toBind :: All HasSpec as => List Term as -> List Var as -> List Bind as
toBind :: forall (as :: [*]).
All HasSpec as =>
List Term as -> List Var as -> List Bind as
toBind List Term as
Nil List Var as
Nil = List Bind as
List Bind '[]
forall {k} (f :: k -> *). List f '[]
Nil
toBind (Term a
t :> List Term as1
ts) (Var a
v :> List Var as1
vs) = (Var a -> Term a -> Bind a
forall a. HasSpec a => Var a -> Term a -> Bind a
Bind Var a
v Term a
Term a
t Bind a -> List Bind as1 -> List Bind (a : as1)
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> List Term as1 -> List Var as1 -> List Bind as1
forall (as :: [*]).
All HasSpec as =>
List Term as -> List Var as -> List Bind as
toBind List Term as1
ts List Var as1
List Var as1
vs)

-- ================================
-- Spec
-- ================================

data Spec a where
  TrueSpec :: Spec a
  ErrorSpec :: NonEmpty String -> Spec a
  SuspendedSpec :: HasSpec a => Var a -> Pred -> Spec a -- Maybe we elide this at first
  MemberSpec :: NonEmpty a -> Spec a
  TypeSpec :: HasSpec a => TypeSpec a -> [a] -> Spec a

typeSpec :: HasSpec a => TypeSpec a -> Spec a
typeSpec :: forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec TypeSpec a
ts = TypeSpec a -> [a] -> Spec a
forall a. HasSpec a => TypeSpec a -> [a] -> Spec a
TypeSpec TypeSpec a
ts [a]
forall a. Monoid a => a
mempty

constrained :: forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained :: forall a. HasSpec a => (Term a -> Pred) -> Spec a
constrained Term a -> Pred
body =
  let Var a
x :-> Pred
p = (Term a -> Pred) -> Binder a
forall a. HasSpec a => (Term a -> Pred) -> Binder a
bind Term a -> Pred
body
   in Var a -> Pred -> Spec a
forall a. HasSpec a => Var a -> Pred -> Spec a
SuspendedSpec Var a
x Pred
p

bind :: HasSpec a => (Term a -> Pred) -> Binder a
bind :: forall a. HasSpec a => (Term a -> Pred) -> Binder a
bind Term a -> Pred
bodyf = Var a
newv Var a -> Pred -> Binder a
forall a. HasSpec a => Var a -> Pred -> Binder a
:-> Pred
bodyPred
  where
    bodyPred :: Pred
bodyPred = {- toPred -} Pred
body
    newv :: Var a
newv = Int -> String -> Var a
forall a. Int -> String -> Var a
Var (Pred -> Int
nextVar Pred
bodyPred) String
"v"
    body :: Pred
body = Term a -> Pred
bodyf (Var a -> Term a
forall a. HasSpec a => Var a -> Term a
V Var a
newv)

    nextVar :: Pred -> Int
nextVar Pred
q = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Pred -> Int
bound Pred
q

    boundBinder :: Binder a -> Int
    boundBinder :: forall a. Binder a -> Int
boundBinder (Var a
x :-> Pred
p) = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Var a -> Int
forall a. Var a -> Int
nameOf Var a
x) (Pred -> Int
bound Pred
p)

    bound :: Pred -> Int
bound (ElemPred Bool
_ Term a
_ NonEmpty a
_) = -Int
1
    bound (Subst Var a
x Term a
_ Pred
p) = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Var a -> Int
forall a. Var a -> Int
nameOf Var a
x) (Pred -> Int
bound Pred
p)
    bound (And [Pred]
ps) = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (-Int
1) Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: (Pred -> Int) -> [Pred] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Pred -> Int
bound [Pred]
ps -- (-1) as the default to get 0 as `nextVar p`
    bound (Let Term a
_ Binder a
b) = Binder a -> Int
forall a. Binder a -> Int
boundBinder Binder a
b
    bound (ForAll Term t
_ Binder a
b) = Binder a -> Int
forall a. Binder a -> Int
boundBinder Binder a
b
    bound (Exists (forall b. Term b -> b) -> GE a
_ Binder a
b) = Binder a -> Int
forall a. Binder a -> Int
boundBinder Binder a
b
    bound (Case Term (Either a b)
_ Binder a
ba Binder b
bb) = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Binder a -> Int
forall a. Binder a -> Int
boundBinder Binder a
ba) (Binder b -> Int
forall a. Binder a -> Int
boundBinder Binder b
bb)
    bound Assert {} = -Int
1
    bound Pred
TruePred = -Int
1
    bound FalsePred {} = -Int
1
    bound DependsOn {} = -Int
1

-- ========================================
-- HasSpec
-- ========================================

class (Typeable a, Eq a, Show a, Show (TypeSpec a), Typeable (TypeSpec a)) => HasSpec a where
  -- | The `TypeSpec a` is the type-specific `Spec a`.
  type TypeSpec a

  -- `TypeSpec` behaves sort-of like a monoid with a neutral
  -- element `anySpec` and a `combineSpec` for combining
  -- two `TypeSpec a`. However, in order to provide flexibilty
  -- `combineSpec` takes two `TypeSpec` and constucts a `Spec`. This
  -- avoids e.g. having to have a separate implementation of `ErrorSpec`
  -- and `MemberSpec` in `TypeSpec`.

  anySpec :: TypeSpec a
  combineSpec :: TypeSpec a -> TypeSpec a -> Spec a

  -- | Generate a value that satisfies the `TypeSpec`.
  -- The key property for this generator is soundness:
  --  ∀ a ∈ genFromTypeSpec spec. a `conformsTo` spec
  genFromTypeSpec :: (HasCallStack, MonadGenError m) => TypeSpec a -> GenT m a

  -- | Check conformance to the spec.
  conformsTo :: HasCallStack => a -> TypeSpec a -> Bool

  -- | Convert a spec to predicates:
  -- The key property here is:
  --   ∀ a. a `conformsTo` spec == a `conformsTo` constrained (\t -> toPreds t spec)
  toPreds :: Term a -> TypeSpec a -> Pred

  -- | This is used to detect self inconsistencies in a (TypeSpec t)
  --   guardTypeSpec message ty --> ErrorSpec message, if ty is inconsistent
  guardTypeSpec :: TypeSpec a -> Spec a
  guardTypeSpec TypeSpec a
ty = TypeSpec a -> Spec a
forall a. HasSpec a => TypeSpec a -> Spec a
typeSpec TypeSpec a
ty

-- =========================================
-- Contexts
-- =========================================

data HOLE a b where
  HOLE :: HOLE a a

deriving instance Show (HOLE a b)

-- | Note the arrows (n :|> hole) and (hole :<| n) always point towards the term with
--   type `(c x)`, (i.e. `hole` in the picture above) where the target variable must occur.
data ListCtx (as :: [Type]) (c :: Type -> Type) where
  Unary :: c a -> ListCtx '[a] c
  (:<|) :: c b -> x -> ListCtx '[b, x] c
  (:|>) :: x -> c b -> ListCtx '[x, b] c

data Ctx v (a :: Type) where
  CtxHole :: HasSpec v => Ctx v v
  CtxApp ::
    ( AppRequires fn as b
    , HasSpec b
    , TypeList as
    , Typeable as
    , All HasSpec as
    , Logic fn
    ) =>
    fn as b -> ListCtx as (Ctx v) -> Ctx v b

ctxHasSpec :: Ctx v a -> Evidence (HasSpec a)
ctxHasSpec :: forall v a. Ctx v a -> Evidence (HasSpec a)
ctxHasSpec Ctx v a
CtxHole = Evidence (HasSpec a)
forall (c :: Constraint). c => Evidence c
Evidence
ctxHasSpec CtxApp {} = Evidence (HasSpec a)
forall (c :: Constraint). c => Evidence c
Evidence

-- | From a ListCtx, build a (List Term as), to which the function symbol can be applied.
--   Hole becomes 't', values become `Lit` .
fromListCtx :: All HasSpec as => ListCtx as (HOLE a) -> Term a -> List Term as
fromListCtx :: forall (as :: [*]) a.
All HasSpec as =>
ListCtx as (HOLE a) -> Term a -> List Term as
fromListCtx (Unary HOLE a a
HOLE) Term a
t = Term a
t 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
fromListCtx (HOLE a b
HOLE :<| x
y) Term a
t = Term a
t Term a -> List Term '[x] -> List Term '[a, x]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> x -> Term x
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit x
y Term x -> List Term '[] -> List Term '[x]
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
fromListCtx (x
x :|> HOLE a b
HOLE) Term a
t = x -> Term x
forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit x
x Term x -> List Term '[a] -> List Term '[x, a]
forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> Term a
t 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

--- | Consider the term `((size_ x +. Lit 3) <=. Lit 12)` with a bunch of nested function symbols, with just 1 variable 'x'
--    `(toCtx x term)` builds a context, with exactly one `CtxHole`, replacing the variable `x`
--    `CtxApp <=. (CtxApp +. (CtxApp size_ (Unary CtxHole) :<| 3) :<| 12)`
--    Working our way from outside in, we first propagate (<=.), then (+.), then (size_). This reduces in several steps
--    1) propagateSpec (CtxApp <=. (CtxApp +. (CtxApp size_ (Unary CtxHole) :<| 3) :<| 12)) $  spec
--    2) propagateSpec (CtxApp +. (CtxApp size_ (Unary CtxHole) :<| 3)) $  (propagate <=. (HOLE:<| 12))
--    3) propagateSpec (CtxApp size_ (Unary CtxHole)) $ (propagate +. (HOLE:<| 3) (propagate <=. (HOLE :<| 12)))
--    4) propagateSpec CtxHole $ (propagate size_ Hole (propagate +. (HOLE:<| 3) (propagate <=. (HOLE :<| 12))))
--    5) propagate size_ Hole (propagate +. (HOLE:<| 3) (propagate <=. (HOLE :<| 12)))
--    Note the pattern in the code below. The recursize call to 'propagateSpec' is on the pattern variable `ctx` which is the
--    part of the context pointed to by the arrows (:<|) and (:|>), and this recurive call to `propagateSpec` is
--    applied to a new spec computed by 'propagate', where the variable `ctx` is replaced by HOLE.
--    we end up on line 5), with three nested calls to `propagate`
propagateSpec ::
  forall v a.
  HasSpec v =>
  Ctx v a ->
  Spec a ->
  Spec v
propagateSpec :: forall v a. HasSpec v => Ctx v a -> Spec a -> Spec v
propagateSpec Ctx v a
context Spec a
spec = case Ctx v a
context of
  Ctx v a
CtxHole -> Spec v
Spec a
spec
  CtxApp fn as a
f (Unary Ctx v a
ctx) | Evidence (HasSpec a)
Evidence <- Ctx v a -> Evidence (HasSpec a)
forall v a. Ctx v a -> Evidence (HasSpec a)
ctxHasSpec Ctx v a
ctx -> Ctx v a -> Spec a -> Spec v
forall v a. HasSpec v => Ctx v a -> Spec a -> Spec v
propagateSpec Ctx v a
ctx (fn as a -> ListCtx as (HOLE a) -> Spec a -> Spec a
forall (as :: [*]) b a.
(AppRequires fn as b, HasSpec a) =>
fn as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
propagate fn as a
f (HOLE a a -> ListCtx '[a] (HOLE a)
forall (c :: * -> *) fn. c fn -> ListCtx '[fn] c
Unary HOLE a a
forall a. HOLE a a
HOLE) Spec a
spec)
  CtxApp fn as a
f (Ctx v b
ctx :<| x
v) | Evidence (HasSpec b)
Evidence <- Ctx v b -> Evidence (HasSpec b)
forall v a. Ctx v a -> Evidence (HasSpec a)
ctxHasSpec Ctx v b
ctx -> Ctx v b -> Spec b -> Spec v
forall v a. HasSpec v => Ctx v a -> Spec a -> Spec v
propagateSpec Ctx v b
ctx (fn as a -> ListCtx as (HOLE b) -> Spec a -> Spec b
forall (as :: [*]) b a.
(AppRequires fn as b, HasSpec a) =>
fn as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
propagate fn as a
f (HOLE b b
forall a. HOLE a a
HOLE HOLE b b -> x -> ListCtx '[b, x] (HOLE b)
forall (c :: * -> *) fn as. c fn -> as -> ListCtx '[fn, as] c
:<| x
v) Spec a
spec)
  CtxApp fn as a
f (x
v :|> Ctx v b
ctx) | Evidence (HasSpec b)
Evidence <- Ctx v b -> Evidence (HasSpec b)
forall v a. Ctx v a -> Evidence (HasSpec a)
ctxHasSpec Ctx v b
ctx -> Ctx v b -> Spec b -> Spec v
forall v a. HasSpec v => Ctx v a -> Spec a -> Spec v
propagateSpec Ctx v b
ctx (fn as a -> ListCtx as (HOLE b) -> Spec a -> Spec b
forall (as :: [*]) b a.
(AppRequires fn as b, HasSpec a) =>
fn as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
forall (t :: [*] -> * -> *) (as :: [*]) b a.
(Logic t, AppRequires t as b, HasSpec a) =>
t as b -> ListCtx as (HOLE a) -> Spec b -> Spec a
propagate fn as a
f (x
v x -> HOLE b b -> ListCtx '[x, b] (HOLE b)
forall fn (c :: * -> *) as. fn -> c as -> ListCtx '[fn, as] c
:|> HOLE b b
forall a. HOLE a a
HOLE) Spec a
spec)

-- Construct a Ctx for a variable 'v', which should occur exactly once in the given Term.
toCtx ::
  forall m v a.
  (Typeable v, Show v, MonadGenError m, HasCallStack) =>
  Var v -> Term a -> m (Ctx v a)
toCtx :: forall (m :: * -> *) v a.
(Typeable v, Show v, MonadGenError m, HasCallStack) =>
Var v -> Term a -> m (Ctx v a)
toCtx Var v
v = Term a -> m (Ctx v a)
forall b. Term b -> m (Ctx v b)
go
  where
    go :: forall b. Term b -> m (Ctx v b)
    go :: forall b. Term b -> m (Ctx v b)
go (Lit b
i) =
      NonEmpty String -> m (Ctx v b)
forall a. HasCallStack => NonEmpty String -> m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE (NonEmpty String -> m (Ctx v b)) -> NonEmpty String -> m (Ctx v b)
forall a b. (a -> b) -> a -> b
$
        [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
          [ String
"toCtx applied to literal: (Lit " String -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show b
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
          , String
"A context is always constructed from an (App f xs) term"
          , String
"with a single occurence of the target variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var v -> String
forall a. Show a => a -> String
show Var v
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"@(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (Var v -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Var v
v) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
          ]
    go t :: Term b
t@(App t dom b
f List Term dom
xs) = t dom b -> ListCtx dom (Ctx v) -> Ctx v b
forall (fn :: [*] -> * -> *) (as :: [*]) b v.
(AppRequires fn as b, HasSpec b, TypeList as, Typeable as,
 All HasSpec as, Logic fn) =>
fn as b -> ListCtx as (Ctx v) -> Ctx v b
CtxApp t dom b
f (ListCtx dom (Ctx v) -> Ctx v b)
-> m (ListCtx dom (Ctx v)) -> m (Ctx v b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Var v -> List Term dom -> m (ListCtx dom (Ctx v))
forall (m :: * -> *) v (as :: [*]).
(Show v, Typeable v, MonadGenError m, HasCallStack) =>
String -> Var v -> List Term as -> m (ListCtx as (Ctx v))
toCtxList (Term b -> String
forall a. Show a => a -> String
show Term b
t) Var v
v List Term dom
xs
    go (V Var b
v')
      | Just v :~: b
Refl <- Var v -> Var b -> Maybe (v :~: b)
forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var v
v Var b
v' = Ctx v b -> m (Ctx v b)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ctx v b -> m (Ctx v b)) -> Ctx v b -> m (Ctx v b)
forall a b. (a -> b) -> a -> b
$ Ctx v v
Ctx v b
forall v. HasSpec v => Ctx v v
CtxHole
      | Bool
otherwise =
          NonEmpty String -> m (Ctx v b)
forall a. HasCallStack => NonEmpty String -> m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE (NonEmpty String -> m (Ctx v b)) -> NonEmpty String -> m (Ctx v b)
forall a b. (a -> b) -> a -> b
$
            [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
              [ String
"A context is always constructed from an (App f xs) term with a single target variable"
              , String
"which in this case is: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var v -> String
forall a. Show a => a -> String
show Var v
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (Var v -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Var v
v) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
              , String
"Instead we found an unknown variable: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var b -> String
forall a. Show a => a -> String
show Var b
v' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (Var b -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Var b
v') String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
              ]

toCtxList ::
  forall m v as.
  (Show v, Typeable v, MonadGenError m, HasCallStack) =>
  String -> Var v -> List Term as -> m (ListCtx as (Ctx v))
toCtxList :: forall (m :: * -> *) v (as :: [*]).
(Show v, Typeable v, MonadGenError m, HasCallStack) =>
String -> Var v -> List Term as -> m (ListCtx as (Ctx v))
toCtxList String
termName Var v
v List Term as
Nil = NonEmpty String -> m (ListCtx as (Ctx v))
forall a. HasCallStack => NonEmpty String -> m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE (NonEmpty String -> m (ListCtx as (Ctx v)))
-> NonEmpty String -> m (ListCtx as (Ctx v))
forall a b. (a -> b) -> a -> b
$ (String
"toCtxList without hole, for variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var v -> String
forall a. Show a => a -> String
show Var v
v) String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [String
termName]
toCtxList String
termName Var v
v (V Var a
v' :> List Term as1
Nil)
  | Just v :~: a
Refl <- Var v -> Var a -> Maybe (v :~: a)
forall a a'.
(Typeable a, Typeable a') =>
Var a -> Var a' -> Maybe (a :~: a')
eqVar Var v
v Var a
v' = ListCtx as (Ctx v) -> m (ListCtx as (Ctx v))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ListCtx as (Ctx v) -> m (ListCtx as (Ctx v)))
-> ListCtx as (Ctx v) -> m (ListCtx as (Ctx v))
forall a b. (a -> b) -> a -> b
$ Ctx v v -> ListCtx '[v] (Ctx v)
forall (c :: * -> *) fn. c fn -> ListCtx '[fn] c
Unary Ctx v v
forall v. HasSpec v => Ctx v v
CtxHole
  | Bool
otherwise =
      NonEmpty String -> m (ListCtx as (Ctx v))
forall a. HasCallStack => NonEmpty String -> m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE (NonEmpty String -> m (ListCtx as (Ctx v)))
-> NonEmpty String -> m (ListCtx as (Ctx v))
forall a b. (a -> b) -> a -> b
$
        [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
          [ String
"A context is always constructed from an (App f xs) term,"
          , String
"with a single occurence of the target variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var v -> String
forall a. Show a => a -> String
show Var v
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"@(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (Var v -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Var v
v) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
          , String
"Instead we found an unknown variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var a -> String
forall a. Show a => a -> String
show Var a
v' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"@(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (Var a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Var a
v') String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
          , String
"in an application: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
termName
          ]
toCtxList String
termName Var v
v (Term a
x :> Term a
y :> List Term as1
Nil)
  | Just a
i <- Term a -> Maybe a
forall a. Term a -> Maybe a
reducesToLit Term a
x = do Ctx v a
hole <- Var v -> Term a -> m (Ctx v a)
forall (m :: * -> *) v a.
(Typeable v, Show v, MonadGenError m, HasCallStack) =>
Var v -> Term a -> m (Ctx v a)
toCtx Var v
v Term a
y; ListCtx as (Ctx v) -> m (ListCtx as (Ctx v))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ListCtx as (Ctx v) -> m (ListCtx as (Ctx v)))
-> ListCtx as (Ctx v) -> m (ListCtx as (Ctx v))
forall a b. (a -> b) -> a -> b
$ (a
i a -> Ctx v a -> ListCtx '[a, a] (Ctx v)
forall fn (c :: * -> *) as. fn -> c as -> ListCtx '[fn, as] c
:|> Ctx v a
hole)
  | Just a
i <- Term a -> Maybe a
forall a. Term a -> Maybe a
reducesToLit Term a
y = do Ctx v a
hole <- Var v -> Term a -> m (Ctx v a)
forall (m :: * -> *) v a.
(Typeable v, Show v, MonadGenError m, HasCallStack) =>
Var v -> Term a -> m (Ctx v a)
toCtx Var v
v Term a
x; ListCtx as (Ctx v) -> m (ListCtx as (Ctx v))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ListCtx as (Ctx v) -> m (ListCtx as (Ctx v)))
-> ListCtx as (Ctx v) -> m (ListCtx as (Ctx v))
forall a b. (a -> b) -> a -> b
$ (Ctx v a
hole Ctx v a -> a -> ListCtx '[a, a] (Ctx v)
forall (c :: * -> *) fn as. c fn -> as -> ListCtx '[fn, as] c
:<| a
i)
  | Bool
otherwise =
      NonEmpty String -> m (ListCtx as (Ctx v))
forall a. HasCallStack => NonEmpty String -> m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE (NonEmpty String -> m (ListCtx as (Ctx v)))
-> NonEmpty String -> m (ListCtx as (Ctx v))
forall a b. (a -> b) -> a -> b
$
        String
"toCtx applied to an App with 2 parameters."
          String -> [String] -> NonEmpty String
forall a. a -> [a] -> NonEmpty a
:| [ String
termName
             , String
"The target variable we are searching for is " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var v -> String
forall a. Show a => a -> String
show Var v
v
             , String
"One of these parameters must reduce to a literal, which is not the case."
             , String
"If both are non-literals, then term could have two variables, which is not allowed."
             ]
toCtxList String
termName Var v
v List Term as
xs =
  NonEmpty String -> m (ListCtx as (Ctx v))
forall a. HasCallStack => NonEmpty String -> m a
forall (m :: * -> *) a.
(MonadGenError m, HasCallStack) =>
NonEmpty String -> m a
fatalErrorNE (NonEmpty String -> m (ListCtx as (Ctx v)))
-> NonEmpty String -> m (ListCtx as (Ctx v))
forall a b. (a -> b) -> a -> b
$
    [String] -> NonEmpty String
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList
      [ String
"toCtx applied to an App with more than 2 parameters"
      , String
termName
      , String
"The target variable we are searching for is " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var v -> String
forall a. Show a => a -> String
show Var v
v
      , String
"All function symbols should have 1 or 2 parameters"
      , String
"This one appears to accept " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (List Term as -> Int
forall {k} (f :: k -> *) (as :: [k]). List f as -> Int
lengthList List Term as
xs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
      ]

-- ===================================================================
-- Pretty Printer Helper functions
-- ===================================================================

data WithPrec a = WithPrec Int a

parensIf :: Bool -> Doc ann -> Doc ann
parensIf :: forall ann. Bool -> Doc ann -> Doc ann
parensIf Bool
True = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens
parensIf Bool
False = Doc ann -> Doc ann
forall a. a -> a
id

prettyPrec :: Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec :: forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
p = WithPrec a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. WithPrec a -> Doc ann
pretty (WithPrec a -> Doc ann) -> (a -> WithPrec a) -> a -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> WithPrec a
forall a. Int -> a -> WithPrec a
WithPrec Int
p

ppList ::
  forall f as ann.
  All HasSpec as => -- can we use something other than All HasSpec as here? We know Function Symbol HERE
  (forall a. HasSpec a => f a -> Doc ann) ->
  List f as ->
  [Doc ann]
ppList :: forall (f :: * -> *) (as :: [*]) ann.
All HasSpec as =>
(forall a. HasSpec a => f a -> Doc ann) -> List f as -> [Doc ann]
ppList forall a. HasSpec a => f a -> Doc ann
_ List f as
Nil = []
ppList forall a. HasSpec a => f a -> Doc ann
pp (f a
a :> List f as1
as) = f a -> Doc ann
forall a. HasSpec a => f a -> Doc ann
pp f a
a Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (forall a. HasSpec a => f a -> Doc ann) -> List f as1 -> [Doc ann]
forall (f :: * -> *) (as :: [*]) ann.
All HasSpec as =>
(forall a. HasSpec a => f a -> Doc ann) -> List f as -> [Doc ann]
ppList f a -> Doc ann
forall a. HasSpec a => f a -> Doc ann
pp List f as1
as

ppList_ :: forall f as ann. (forall a. f a -> Doc ann) -> List f as -> [Doc ann]
ppList_ :: forall (f :: * -> *) (as :: [*]) ann.
(forall a. f a -> Doc ann) -> List f as -> [Doc ann]
ppList_ forall a. f a -> Doc ann
_ List f as
Nil = []
ppList_ forall a. f a -> Doc ann
pp (f a
a :> List f as1
as) = f a -> Doc ann
forall a. f a -> Doc ann
pp f a
a Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (forall a. f a -> Doc ann) -> List f as1 -> [Doc ann]
forall (f :: * -> *) (as :: [*]) ann.
(forall a. f a -> Doc ann) -> List f as -> [Doc ann]
ppList_ f a -> Doc ann
forall a. f a -> Doc ann
pp List f as1
as

prettyType :: forall t x. Typeable t => Doc x
prettyType :: forall t x. Typeable t => Doc x
prettyType = String -> Doc x
forall a. IsString a => String -> a
fromString (String -> Doc x) -> String -> Doc x
forall a b. (a -> b) -> a -> b
$ TypeRep -> String
forall a. Show a => a -> String
show (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t))

vsep' :: [Doc ann] -> Doc ann
vsep' :: forall ann. [Doc ann] -> Doc ann
vsep' = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (Doc ann -> Doc ann)
-> ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc ann] -> Doc ann
forall a. Monoid a => [a] -> a
mconcat ([Doc ann] -> Doc ann)
-> ([Doc ann] -> [Doc ann]) -> [Doc ann] -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
hardline

(/>) :: Doc ann -> Doc ann -> Doc ann
Doc ann
h /> :: forall ann. Doc ann -> Doc ann -> Doc ann
/> Doc ann
cont = Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
hang Int
2 (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
sep [Doc ann
h, Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align Doc ann
cont]

infixl 5 />

short :: forall a x. (Show a, Typeable a) => [a] -> Doc x
short :: forall a x. (Show a, Typeable a) => [a] -> Doc x
short [] = Doc x
"[]"
short [a
x] =
  let raw :: String
raw = a -> String
forall a. Show a => a -> String
show a
x
      refined :: String
refined = if String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
raw Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
20 then String
raw else Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
20 String
raw String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ... "
   in Doc x
"[" Doc x -> Doc x -> Doc x
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc x
forall a. IsString a => String -> a
fromString String
refined Doc x -> Doc x -> Doc x
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc x
"]"
short [a]
xs =
  let raw :: String
raw = [a] -> String
forall a. Show a => a -> String
show [a]
xs
   in if String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
raw Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
50
        then String -> Doc x
forall a. IsString a => String -> a
fromString String
raw
        else Doc x
"([" Doc x -> Doc x -> Doc x
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc x
forall a ann. Show a => a -> Doc ann
viaShow ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs) Doc x -> Doc x -> Doc x
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc x
"elements ...] @" Doc x -> Doc x -> Doc x
forall a. Semigroup a => a -> a -> a
<> forall t x. Typeable t => Doc x
prettyType @a Doc x -> Doc x -> Doc x
forall a. Semigroup a => a -> a -> a
<> Doc x
")"

showType :: forall t. Typeable t => String
showType :: forall t. Typeable t => String
showType = TypeRep -> String
forall a. Show a => a -> String
show (Proxy t -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @t))

-- ==========================================================================
-- Pretty and Show instances
-- ==========================================================================

-- ------------ Term -----------------
instance Pretty (WithPrec (Term a)) where
  pretty :: forall ann. WithPrec (Term a) -> Doc ann
pretty (WithPrec Int
p Term a
t) = case Term a
t of
    Lit a
n -> String -> Doc ann
forall a. IsString a => String -> a
fromString (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$ Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p a
n String
""
    V Var a
x -> Var a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Var a
x
    App t dom a
x List Term dom
Nil -> t dom a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow t dom a
x
    App t dom a
f List Term dom
as
      | t dom a -> Bool
forall (dom :: [*]) rng. t dom rng -> Bool
forall (t :: [*] -> * -> *) (dom :: [*]) rng.
Syntax t =>
t dom rng -> Bool
inFix t dom a
f
      , Term a
a :> Term a
b :> List Term as1
Nil <- List Term dom
as ->
          Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Int -> Term a -> Doc ann
forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 Term a
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> t dom a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow t dom a
f Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Term a -> Doc ann
forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
10 Term a
b
      | Bool
otherwise -> Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ t dom a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow t dom a
f Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
fillSep ((forall a. HasSpec a => Term a -> Doc ann)
-> List Term dom -> [Doc ann]
forall (f :: * -> *) (as :: [*]) ann.
All HasSpec as =>
(forall a. HasSpec a => f a -> Doc ann) -> List f as -> [Doc ann]
ppList (Int -> Term a -> Doc ann
forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
11) List Term dom
as))

instance Pretty (Term a) where
  pretty :: forall ann. Term a -> Doc ann
pretty = Int -> Term a -> Doc ann
forall a ann. Pretty (WithPrec a) => Int -> a -> Doc ann
prettyPrec Int
0

instance Show (Term a) where
  showsPrec :: Int -> Term a -> ShowS
showsPrec Int
p Term a
t = Doc Any -> ShowS
forall a. Show a => a -> ShowS
shows (Doc Any -> ShowS) -> Doc Any -> ShowS
forall a b. (a -> b) -> a -> b
$ WithPrec (Term a) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. WithPrec (Term a) -> Doc ann
pretty (Int -> Term a -> WithPrec (Term a)
forall a. Int -> a -> WithPrec a
WithPrec Int
p Term a
t)

-- ------------ Pred -----------------

instance Pretty Pred where
  pretty :: forall ann. Pred -> Doc ann
pretty = \case
    ElemPred Bool
True Term a
term NonEmpty a
vs ->
      Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
        [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
sep
          [ Doc ann
"MemberPred"
          , Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Term a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term a -> Doc ann
pretty Term a
term)
          , if NonEmpty a -> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty a
vs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
2
              then Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
fillSep (Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
"," ((a -> Doc ann) -> [a] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
vs))))
              else Doc ann
"(" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Int -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (NonEmpty a -> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty a
vs) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
" items)"
          ]
    ElemPred Bool
False Term a
term NonEmpty a
vs -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
sep [Doc ann
"notMemberPred", Term a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term a -> Doc ann
pretty Term a
term, [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
fillSep (Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
"," ((a -> Doc ann) -> [a] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
vs)))]
    -- Exists _ (x :-> p) -> align $ sep ["exists" <+> viaShow x <+> "in", pretty p]
    Let Term a
t (Var a
x :-> Pred
p) -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
sep [Doc ann
"let" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Var a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Var a
x 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
/> Term a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term a -> Doc ann
pretty Term a
t Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"in", Pred -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Pred -> Doc ann
pretty Pred
p]
    And [Pred]
ps -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
braces (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep' ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ (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]
ps
    Exists (forall b. Term b -> b) -> GE a
_ (Var a
x :-> Pred
p) -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
align (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
sep [Doc ann
"exists" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Var a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Var a
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"in", Pred -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Pred -> Doc ann
pretty Pred
p]
    Assert Term Bool
t -> Doc ann
"assert $" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term Bool -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term Bool -> Doc ann
pretty Term Bool
t
    -- Reifies t' t _ -> "reifies" <+> pretty (WithPrec 11 t') <+> pretty (WithPrec 11 t)
    DependsOn Term a
a Term b
b -> Term a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term a -> Doc ann
pretty Term a
a 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
/> Term b -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term b -> Doc ann
pretty Term b
b
    ForAll Term t
t (Var a
x :-> Pred
p) -> Doc ann
"forall" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Var a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Var a
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"in" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term t -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term t -> Doc ann
pretty Term t
t 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
/> Pred -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Pred -> Doc ann
pretty Pred
p
    Case Term (Either a b)
t Binder a
as Binder b
bs -> Doc ann
"case" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term (Either a b) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term (Either a b) -> Doc ann
pretty Term (Either a b)
t Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"of" 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' [Binder a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Binder a -> Doc ann
pretty Binder a
as, Binder b -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Binder b -> Doc ann
pretty Binder b
bs]
    -- When b p -> "whenTrue" <+> pretty (WithPrec 11 b) <+> "$" /> pretty p
    Subst Var a
x Term a
t Pred
p -> Doc ann
"[" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Term a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Term a -> Doc ann
pretty Term a
t Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"/" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Var a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Var a
x Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"]" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Pred -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Pred -> Doc ann
pretty Pred
p
    -- GenHint h t -> "genHint" <+> fromString (showsPrec 11 h "") <+> "$" <+> pretty t
    Pred
TruePred -> Doc ann
"True"
    FalsePred {} -> Doc ann
"False"

-- Monitor {} -> "monitor"
-- Explain es p -> "Explain" <+> viaShow (NE.toList es) <+> "$" /> pretty p

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

instance Pretty (Binder a) where
  pretty :: forall ann. Binder a -> Doc ann
pretty (Var a
x :-> Pred
p) = Var a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Var a
x 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
<+> Pred -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Pred -> Doc ann
pretty Pred
p

-- ------------ Specifications -----------------

instance HasSpec a => Pretty (WithPrec (Spec a)) where
  pretty :: forall ann. WithPrec (Spec a) -> Doc ann
pretty (WithPrec Int
d Spec a
s) = case Spec a
s of
    ErrorSpec NonEmpty String
es -> Doc ann
"ErrorSpec" 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' ((String -> Doc ann) -> [String] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc ann
forall a. IsString a => String -> a
fromString (NonEmpty String -> [String]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty String
es))
    Spec a
TrueSpec -> String -> Doc ann
forall a. IsString a => String -> a
fromString (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$ String
"TrueSpec @(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ forall t. Typeable t => String
showType @a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
    MemberSpec NonEmpty a
xs -> Doc ann
"MemberSpec" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [a] -> Doc ann
forall a x. (Show a, Typeable a) => [a] -> Doc x
short (NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty a
xs)
    SuspendedSpec Var a
x Pred
p -> Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann
"constrained $ \\" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Var a -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Var a
x 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
/> Pred -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Pred -> Doc ann
pretty Pred
p
    -- TODO: require pretty for `TypeSpec` to make this much nicer
    TypeSpec TypeSpec a
ts [a]
cant ->
      Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
parensIf (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
        Doc ann
"TypeSpec"
          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
            [ String -> Doc ann
forall a. IsString a => String -> a
fromString (Int -> TypeSpec a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 TypeSpec a
ts String
"")
            , [a] -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow [a]
cant
            ]

instance HasSpec a => Pretty (Spec a) where
  pretty :: forall ann. Spec a -> Doc ann
pretty = WithPrec (Spec a) -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. WithPrec (Spec a) -> Doc ann
pretty (WithPrec (Spec a) -> Doc ann)
-> (Spec a -> WithPrec (Spec a)) -> Spec a -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Spec a -> WithPrec (Spec a)
forall a. Int -> a -> WithPrec a
WithPrec Int
0

instance HasSpec a => Show (Spec a) where
  showsPrec :: Int -> Spec a -> ShowS
showsPrec Int
d = Doc Any -> ShowS
forall a. Show a => a -> ShowS
shows (Doc Any -> ShowS) -> (Spec a -> Doc Any) -> Spec a -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WithPrec (Spec a) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. WithPrec (Spec a) -> Doc ann
pretty (WithPrec (Spec a) -> Doc Any)
-> (Spec a -> WithPrec (Spec a)) -> Spec a -> Doc Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Spec a -> WithPrec (Spec a)
forall a. Int -> a -> WithPrec a
WithPrec Int
d