{-# 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 :: [*] -> * -> *). OrdSet a -> Specification fn a MemberSpec [Bool False] (Bool False, Bool True) -> forall a (fn :: [*] -> * -> *). OrdSet a -> Specification fn a MemberSpec [Bool True]