{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

-- | This module provides some necessary instances
-- of `Functions` that aren't needed in `Constrained.Base`
-- (which is already big enough) but which are necessary
-- to use the framework.
module Constrained.Instances where

import Data.Typeable

import Constrained.Base
import Constrained.Core
import Constrained.List
import Constrained.Spec.Generics ()
import Constrained.Univ

instance
  ( Typeable fn
  , Functions (fn (Fix fn)) (Fix fn)
  ) =>
  Functions (Fix fn) (Fix fn)
  where
  propagateSpecFun :: forall (as :: [*]) a b.
(TypeList as, Typeable as, HasSpec (Fix fn) a, HasSpec (Fix fn) b,
 All (HasSpec (Fix fn)) as) =>
Fix fn as b
-> ListCtx Value as (HOLE a)
-> Specification (Fix fn) b
-> Specification (Fix fn) a
propagateSpecFun (Fix fn (Fix fn) as b
fn) ListCtx Value as (HOLE a)
ctx Specification (Fix fn) b
spec = forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn a,
 HasSpec fn b, All (HasSpec fn) as) =>
f as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun fn (Fix fn) as b
fn ListCtx Value as (HOLE a)
ctx Specification (Fix fn) b
spec
  rewriteRules :: forall (as :: [*]) b.
(TypeList as, Typeable as, HasSpec (Fix fn) b,
 All (HasSpec (Fix fn)) as) =>
Fix fn as b -> List (Term (Fix fn)) as -> Maybe (Term (Fix fn) b)
rewriteRules (Fix fn (Fix fn) as b
fn) = forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn b,
 All (HasSpec fn) as) =>
f as b -> List (Term fn) as -> Maybe (Term fn b)
rewriteRules fn (Fix fn) as b
fn
  mapTypeSpec :: forall a b.
(HasSpec (Fix fn) a, HasSpec (Fix fn) b) =>
Fix fn '[a] b -> TypeSpec (Fix fn) a -> Specification (Fix fn) b
mapTypeSpec (Fix fn (Fix fn) '[a] b
fn) = forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) a b.
(Functions f fn, HasSpec fn a, HasSpec fn b) =>
f '[a] b -> TypeSpec fn a -> Specification fn b
mapTypeSpec fn (Fix fn) '[a] b
fn

instance
  ( Typeable fn
  , Typeable fn'
  , Typeable fnU
  , Functions (fn fnU) fnU
  , Functions (fn' fnU) fnU
  ) =>
  Functions (Oneof fn fn' fnU) fnU
  where
  propagateSpecFun :: forall (as :: [*]) a b.
(TypeList as, Typeable as, HasSpec fnU a, HasSpec fnU b,
 All (HasSpec fnU) as) =>
Oneof fn fn' fnU as b
-> ListCtx Value as (HOLE a)
-> Specification fnU b
-> Specification fnU a
propagateSpecFun (OneofLeft fn fnU as b
fn) = forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn a,
 HasSpec fn b, All (HasSpec fn) as) =>
f as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun fn fnU as b
fn
  propagateSpecFun (OneofRight fn' fnU as b
fn) = forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn a,
 HasSpec fn b, All (HasSpec fn) as) =>
f as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun fn' fnU as b
fn

  rewriteRules :: forall (as :: [*]) b.
(TypeList as, Typeable as, HasSpec fnU b, All (HasSpec fnU) as) =>
Oneof fn fn' fnU as b -> List (Term fnU) as -> Maybe (Term fnU b)
rewriteRules (OneofLeft fn fnU as b
fn) = forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn b,
 All (HasSpec fn) as) =>
f as b -> List (Term fn) as -> Maybe (Term fn b)
rewriteRules fn fnU as b
fn
  rewriteRules (OneofRight fn' fnU as b
fn) = forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn b,
 All (HasSpec fn) as) =>
f as b -> List (Term fn) as -> Maybe (Term fn b)
rewriteRules fn' fnU as b
fn

  mapTypeSpec :: forall a b.
(HasSpec fnU a, HasSpec fnU b) =>
Oneof fn fn' fnU '[a] b -> TypeSpec fnU a -> Specification fnU b
mapTypeSpec (OneofLeft fn fnU '[a] b
fn) = forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) a b.
(Functions f fn, HasSpec fn a, HasSpec fn b) =>
f '[a] b -> TypeSpec fn a -> Specification fn b
mapTypeSpec fn fnU '[a] b
fn
  mapTypeSpec (OneofRight fn' fnU '[a] b
fn) = forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) a b.
(Functions f fn, HasSpec fn a, HasSpec fn b) =>
f '[a] b -> TypeSpec fn a -> Specification fn b
mapTypeSpec fn' fnU '[a] b
fn

instance BaseUniverse fn => Functions (EqFn fn) fn where
  propagateSpecFun :: forall (as :: [*]) a b.
(TypeList as, Typeable as, HasSpec fn a, HasSpec fn b,
 All (HasSpec fn) as) =>
EqFn fn as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun EqFn fn as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty String
err) = forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec NonEmpty String
err
  propagateSpecFun EqFn fn as b
fn (ListCtx List Value as
pre HOLE a a
HOLE List Value as'
suf) (SuspendedSpec Var b
v Pred fn
ps) =
    forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
v' ->
      let args :: List (Term fn) (Append as (a : as'))
args = forall {a} (f :: a -> *) (as :: [a]) (bs :: [a]).
List f as -> List f bs -> List f (Append as bs)
appendList (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (\(Value a
a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit a
a) List Value as
pre) (Term fn a
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (\(Value a
a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit a
a) List Value as'
suf)
       in forall (fn :: [*] -> * -> *) a. Term fn a -> Binder fn a -> Pred fn
Let (forall (as :: [*]) (fn :: [*] -> * -> *) a.
(Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn a,
 BaseUniverse fn) =>
fn as a -> List (Term fn) as -> Term fn a
App (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn EqFn fn as b
fn) List (Term fn) (Append as (a : as'))
args) (Var b
v forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Pred fn -> Binder fn a
:-> Pred fn
ps)
  propagateSpecFun EqFn fn as b
Equal ListCtx Value as (HOLE a)
ctx Specification fn b
spec
    | HOLE a a
HOLE :? Value a
a :> List Value as1
Nil <- ListCtx Value as (HOLE a)
ctx =
        forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn a,
 HasSpec fn b, All (HasSpec fn) as) =>
f as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun @(EqFn fn) @fn forall a (fn :: [*] -> * -> *). Eq a => EqFn fn '[a, a] Bool
Equal (forall a. Show a => a -> Value a
Value a
a forall (f :: * -> *) a (as1 :: [*]) (c :: * -> *).
f a -> ListCtx f as1 c -> ListCtx f (a : as1) c
:! forall (c :: * -> *) a (f :: * -> *). c a -> ListCtx f '[a] c
NilCtx forall a. HOLE a a
HOLE) Specification fn b
spec
    | Value a
a :! NilCtx HOLE a a
HOLE <- ListCtx Value as (HOLE a)
ctx = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn Bool
-> (Bool -> Specification fn a) -> Specification fn a
caseBoolSpec Specification fn b
spec forall a b. (a -> b) -> a -> b
$ \case
        Bool
True -> forall a (fn :: [*] -> * -> *). a -> Specification fn a
equalSpec a
a
        Bool
False -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a
notEqualSpec a
a

  rewriteRules :: forall (as :: [*]) b.
(TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) =>
EqFn fn as b -> List (Term fn) as -> Maybe (Term fn b)
rewriteRules EqFn fn as b
Equal (Term fn a
t :> Term fn a
t' :> List (Term fn) as1
Nil)
    | Term fn a
t forall a. Eq a => a -> a -> Bool
== Term fn a
t' = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Bool
True
    | Bool
otherwise = forall a. Maybe a
Nothing

  mapTypeSpec :: forall a b.
(HasSpec fn a, HasSpec fn b) =>
EqFn fn '[a] b -> TypeSpec fn a -> Specification fn b
mapTypeSpec EqFn fn '[a] b
f TypeSpec fn a
_ = case EqFn fn '[a] b
f of {}

instance BaseUniverse fn => Functions (BoolFn fn) fn where
  propagateSpecFun :: forall (as :: [*]) a b.
(TypeList as, Typeable as, HasSpec fn a, HasSpec fn b,
 All (HasSpec fn) as) =>
BoolFn fn as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun BoolFn fn as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty String
err) = forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec NonEmpty String
err
  propagateSpecFun BoolFn fn as b
fn (ListCtx List Value as
pre HOLE a a
HOLE List Value as'
suf) (SuspendedSpec Var b
v Pred fn
ps) =
    forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
v' ->
      let args :: List (Term fn) (Append as (a : as'))
args = forall {a} (f :: a -> *) (as :: [a]) (bs :: [a]).
List f as -> List f bs -> List f (Append as bs)
appendList (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (\(Value a
a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit a
a) List Value as
pre) (Term fn a
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (\(Value a
a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit a
a) List Value as'
suf)
       in forall (fn :: [*] -> * -> *) a. Term fn a -> Binder fn a -> Pred fn
Let (forall (as :: [*]) (fn :: [*] -> * -> *) a.
(Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn a,
 BaseUniverse fn) =>
fn as a -> List (Term fn) as -> Term fn a
App (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn BoolFn fn as b
fn) List (Term fn) (Append as (a : as'))
args) (Var b
v forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Pred fn -> Binder fn a
:-> Pred fn
ps)
  propagateSpecFun BoolFn fn as b
Not (NilCtx HOLE a Bool
HOLE) Specification fn b
spec = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn Bool
-> (Bool -> Specification fn a) -> Specification fn a
caseBoolSpec Specification fn b
spec (forall a (fn :: [*] -> * -> *). a -> Specification fn a
equalSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not)
  propagateSpecFun BoolFn fn as b
Or (HOLE a a
HOLE :? Value (Bool
s :: Bool) :> List Value as1
Nil) Specification fn b
spec = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn Bool
-> (Bool -> Specification fn a) -> Specification fn a
caseBoolSpec Specification fn b
spec (forall (fn :: [*] -> * -> *). Bool -> Bool -> Specification fn Bool
okOr Bool
s)
  propagateSpecFun BoolFn fn as b
Or (Value (Bool
s :: Bool) :! NilCtx HOLE a Bool
HOLE) Specification fn b
spec = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Specification fn Bool
-> (Bool -> Specification fn a) -> Specification fn a
caseBoolSpec Specification fn b
spec (forall (fn :: [*] -> * -> *). Bool -> Bool -> Specification fn Bool
okOr Bool
s)

  mapTypeSpec :: forall a b.
(HasSpec fn a, HasSpec fn b) =>
BoolFn fn '[a] b -> TypeSpec fn a -> Specification fn b
mapTypeSpec BoolFn fn '[a] b
Not (SumSpec Maybe (Int, Int)
h Specification fn ()
a Specification fn ()
b) = forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a b.
Maybe (Int, Int)
-> Specification fn a -> Specification fn b -> SumSpec fn a b
SumSpec Maybe (Int, Int)
h Specification fn ()
b Specification fn ()
a

-- | We have something like ('constant' ||. HOLE) must evaluate to 'need'. Return a (Specification fn Bool) for HOLE, that makes that True.
okOr :: Bool -> Bool -> Specification fn Bool
okOr :: forall (fn :: [*] -> * -> *). Bool -> Bool -> Specification fn Bool
okOr Bool
constant Bool
need = case (Bool
constant, Bool
need) of
  (Bool
True, Bool
True) -> forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
  (Bool
True, Bool
False) ->
    forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec
      (forall (f :: * -> *) a. Applicative f => a -> f a
pure (String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Bool
constant forall a. [a] -> [a] -> [a]
++ String
"||. HOLE) must equal False. That cannot be the case."))
  (Bool
False, Bool
False) -> forall a (fn :: [*] -> * -> *). NonEmpty a -> Specification fn a
MemberSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False)
  (Bool
False, Bool
True) -> forall a (fn :: [*] -> * -> *). NonEmpty a -> Specification fn a
MemberSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True)