{-# LANGUAGE DeriveGeneric           #-}
{-# LANGUAGE QuantifiedConstraints   #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE FlexibleContexts        #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE ConstraintKinds         #-}
{-# LANGUAGE DefaultSignatures       #-}
{-# LANGUAGE StandaloneDeriving      #-}
{-# LANGUAGE TypeOperators           #-}
{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE PolyKinds               #-}
{-# LANGUAGE GADTs                   #-}
{-# LANGUAGE KindSignatures          #-}
{-# LANGUAGE PatternSynonyms         #-}
{-# LANGUAGE RankNTypes              #-}
{-# LANGUAGE TypeFamilies            #-}
{-# LANGUAGE MultiParamTypeClasses   #-}
{-# LANGUAGE ScopedTypeVariables     #-}
{-# OPTIONS_GHC -Wno-orphans         #-}
-- |Deep representation for 'SRep'
module Generics.Simplistic.Deep
  ( -- * (Co)Free (Co)Monad and its cousins
    HolesAnn(..)
  , SFix    , pattern SFix    , pattern Prim
  , SFixAnn , pattern SFixAnn , pattern PrimAnn
  , Holes   , pattern Roll    , pattern Hole
  -- ** Constraints
  , CompoundCnstr , PrimCnstr
  -- ** Coercions
  , holesToSFix , sfixToHoles
  -- ** Maps, zips and folds
  , holesMapAnn , holesMap , holesMapM , holesMapAnnM , getAnn
  , holesJoin , holesSize, holesHolesList
  , holesRefineM , holesRefineHoles , holesRefineHolesM
  , synthesize , synthesizeM , cataM
  -- ** Anti-Unification
  , lgg
  -- ** Conversion
  , Deep(..) , GDeep(..)
  ) where

import Data.Proxy
-- import qualified Data.Set as S (Set, fromList)
import Control.Monad.Identity
import Control.DeepSeq
import GHC.Generics (from , to)
import Unsafe.Coerce

import Generics.Simplistic
import Generics.Simplistic.Util

-- Useful constraints

type PrimCnstr kappa fam b
  = (Elem b kappa , NotElem b fam)

type CompoundCnstr kappa fam a
  = (Elem a fam , NotElem a kappa , Generic a)

-- |The cofree comonad and free monad on the same type;
-- this allows us to use the same recursion operator
-- for everything.
data HolesAnn kappa fam ann h a where
  Hole' :: ann a -- ^ Annotation
        -> h a -> HolesAnn kappa fam ann h a
  Prim' :: (PrimCnstr kappa fam a)
        => ann a -- ^ Annotation
        -> a -> HolesAnn kappa fam ann h a
  Roll' :: (CompoundCnstr kappa fam a)
        => ann a -- ^ Annotation
        -> SRep (HolesAnn kappa fam ann h) (Rep a)
        -> HolesAnn kappa fam ann h a

instance (All Eq kappa , EqHO h) => EqHO (Holes kappa fam h) where
  eqHO :: Holes kappa fam h k -> Holes kappa fam h k -> Bool
eqHO x :: Holes kappa fam h k
x y :: Holes kappa fam h k
y = (Exists (Holes kappa fam h :*: Holes kappa fam h) -> Bool)
-> [Exists (Holes kappa fam h :*: Holes kappa fam h)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((forall x. (:*:) (Holes kappa fam h) (Holes kappa fam h) x -> Bool)
-> Exists (Holes kappa fam h :*: Holes kappa fam h) -> Bool
forall k (f :: k -> *) a.
(forall (x :: k). f x -> a) -> Exists f -> a
exElim ((forall x.
  (:*:) (Holes kappa fam h) (Holes kappa fam h) x -> Bool)
 -> Exists (Holes kappa fam h :*: Holes kappa fam h) -> Bool)
-> (forall x.
    (:*:) (Holes kappa fam h) (Holes kappa fam h) x -> Bool)
-> Exists (Holes kappa fam h :*: Holes kappa fam h)
-> Bool
forall a b. (a -> b) -> a -> b
$ (HolesAnn kappa fam U1 h x -> HolesAnn kappa fam U1 h x -> Bool)
-> (:*:) (Holes kappa fam h) (Holes kappa fam h) x -> Bool
forall k (f :: k -> *) (x :: k) (g :: k -> *) a.
(f x -> g x -> a) -> (:*:) f g x -> a
uncurry' HolesAnn kappa fam U1 h x -> HolesAnn kappa fam U1 h x -> Bool
forall k. Holes kappa fam h k -> Holes kappa fam h k -> Bool
go) ([Exists (Holes kappa fam h :*: Holes kappa fam h)] -> Bool)
-> [Exists (Holes kappa fam h :*: Holes kappa fam h)] -> Bool
forall a b. (a -> b) -> a -> b
$ HolesAnn kappa fam U1 (Holes kappa fam h :*: Holes kappa fam h) k
-> [Exists (Holes kappa fam h :*: Holes kappa fam h)]
forall (kappa :: [*]) (fam :: [*]) (ann :: * -> *) (f :: * -> *) a.
HolesAnn kappa fam ann f a -> [Exists f]
holesHolesList (Holes kappa fam h k
-> Holes kappa fam h k
-> HolesAnn
     kappa fam U1 (Holes kappa fam h :*: Holes kappa fam h) k
forall (kappa :: [*]) (fam :: [*]) (h :: * -> *) (i :: * -> *) a.
All Eq kappa =>
Holes kappa fam h a
-> Holes kappa fam i a
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
lgg Holes kappa fam h k
x Holes kappa fam h k
y)
    where
      go :: Holes kappa fam h a -> Holes kappa fam h a -> Bool
      go :: Holes kappa fam h a -> Holes kappa fam h a -> Bool
go (Hole h1 :: h a
h1) (Hole h2 :: h a
h2) = h a -> h a -> Bool
forall ki (f :: ki -> *) (k :: ki). EqHO f => f k -> f k -> Bool
eqHO h a
h1 h a
h2
      go _         _         = Bool
False

instance (All Eq kappa , EqHO h) => Eq (Holes kappa fam h t) where
   == :: Holes kappa fam h t -> Holes kappa fam h t -> Bool
(==) = Holes kappa fam h t -> Holes kappa fam h t -> Bool
forall ki (f :: ki -> *) (k :: ki). EqHO f => f k -> f k -> Bool
eqHO

-- |Deep representations are easily achieved by forbiding
-- the 'Hole'' constructor and providing unit annotations.
type SFix kappa fam = HolesAnn kappa fam U1 V1

pattern SFix :: () => (CompoundCnstr kappa fam a)
             => SRep (SFix kappa fam) (Rep a)
             -> SFix kappa fam a
pattern $bSFix :: SRep (SFix kappa fam) (Rep a) -> SFix kappa fam a
$mSFix :: forall r (kappa :: [*]) (fam :: [*]) a.
SFix kappa fam a
-> (CompoundCnstr kappa fam a =>
    SRep (SFix kappa fam) (Rep a) -> r)
-> (Void# -> r)
-> r
SFix x = Roll x
{-# COMPLETE SFix , Prim #-}

-- |A tree with holes has unit annotations
type Holes kappa fam = HolesAnn kappa fam U1

pattern Hole :: h a -> Holes kappa fam h a
pattern $bHole :: h a -> Holes kappa fam h a
$mHole :: forall r (h :: * -> *) a (kappa :: [*]) (fam :: [*]).
Holes kappa fam h a -> (h a -> r) -> (Void# -> r) -> r
Hole x = Hole' U1 x

pattern Prim :: () => (PrimCnstr kappa fam a)
             => a -> Holes kappa fam h a
pattern $bPrim :: a -> Holes kappa fam h a
$mPrim :: forall r (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
Holes kappa fam h a
-> (PrimCnstr kappa fam a => a -> r) -> (Void# -> r) -> r
Prim a = Prim' U1 a

pattern Roll :: () => (CompoundCnstr kappa fam a)
             => SRep (Holes kappa fam h) (Rep a)
             -> Holes kappa fam h a
pattern $bRoll :: SRep (Holes kappa fam h) (Rep a) -> Holes kappa fam h a
$mRoll :: forall r (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
Holes kappa fam h a
-> (CompoundCnstr kappa fam a =>
    SRep (Holes kappa fam h) (Rep a) -> r)
-> (Void# -> r)
-> r
Roll x = Roll' U1 x
{-# COMPLETE Hole , Prim , Roll #-}

-- |Annotated fixpoints are also easy; forbid the 'Hole''
-- constructor but add something to every 'Roll' of
-- the representation.
type SFixAnn kappa fam ann = HolesAnn kappa fam ann V1

pattern PrimAnn :: () => (PrimCnstr kappa fam a)
                => ann a -> a -> SFixAnn kappa fam ann a
pattern $bPrimAnn :: ann a -> a -> SFixAnn kappa fam ann a
$mPrimAnn :: forall r (kappa :: [*]) (fam :: [*]) a (ann :: * -> *).
SFixAnn kappa fam ann a
-> (PrimCnstr kappa fam a => ann a -> a -> r) -> (Void# -> r) -> r
PrimAnn ann a = Prim' ann a

pattern SFixAnn :: () => (CompoundCnstr kappa fam a)
                => ann a
                -> SRep (SFixAnn kappa fam ann) (Rep a)
                -> SFixAnn kappa fam ann a
pattern $bSFixAnn :: ann a
-> SRep (SFixAnn kappa fam ann) (Rep a) -> SFixAnn kappa fam ann a
$mSFixAnn :: forall r (kappa :: [*]) (fam :: [*]) a (ann :: * -> *).
SFixAnn kappa fam ann a
-> (CompoundCnstr kappa fam a =>
    ann a -> SRep (SFixAnn kappa fam ann) (Rep a) -> r)
-> (Void# -> r)
-> r
SFixAnn ann x = Roll' ann x
{-# COMPLETE SFixAnn , PrimAnn #-}

---------------
-- Coercions --
---------------

sfixToHoles :: SFix kappa fam at -> Holes kappa fam h at
sfixToHoles :: SFix kappa fam at -> Holes kappa fam h at
sfixToHoles = SFix kappa fam at -> Holes kappa fam h at
forall a b. a -> b
unsafeCoerce

holesToSFix :: Holes kappa fam V1 at -> SFix kappa fam at
holesToSFix :: Holes kappa fam V1 at -> Holes kappa fam V1 at
holesToSFix = Holes kappa fam V1 at -> Holes kappa fam V1 at
forall a. a -> a
id

------------
-- NFData --
------------

-- VCM: QUESTION: DDoes it make sense to have this here?
-- I need it in /hdiff/, and I can see how it can be useful.
-- @trupill, do you prefer to keep this or trash this?

instance (forall x . NFData (ann x) , forall x . NFData (h x))
    => NFData (HolesAnn kappa fam ann h f) where
  rnf :: HolesAnn kappa fam ann h f -> ()
rnf (Prim' ann :: ann f
ann _) = ann f -> ()
forall a. NFData a => a -> ()
rnf ann f
ann
  rnf (Hole' ann :: ann f
ann h :: h f
h) = ann f -> ()
forall a. NFData a => a -> ()
rnf ann f
ann () -> () -> ()
forall a b. a -> b -> b
`seq` h f -> ()
forall a. NFData a => a -> ()
rnf h f
h
  rnf (Roll' ann :: ann f
ann x :: SRep (HolesAnn kappa fam ann h) (Rep f)
x) = ann f -> ()
forall a. NFData a => a -> ()
rnf ann f
ann () -> () -> ()
forall a b. a -> b -> b
`seq` SRep (HolesAnn kappa fam ann h) (Rep f) -> ()
forall a. NFData a => a -> ()
rnf SRep (HolesAnn kappa fam ann h) (Rep f)
x

instance NFData (V1 x) where
  rnf :: V1 x -> ()
rnf _ = ()

instance NFData (U1 x) where
  rnf :: U1 x -> ()
rnf U1 = ()

----------------------
-- Useful Functions --
----------------------

-- |Retrieves the annotation inside a 'HolesAnn';
-- this is the counit of the comonad.
getAnn :: HolesAnn kappa fam ann h a -> ann a
getAnn :: HolesAnn kappa fam ann h a -> ann a
getAnn (Hole' ann :: ann a
ann _) = ann a
ann
getAnn (Prim' ann :: ann a
ann _) = ann a
ann
getAnn (Roll' ann :: ann a
ann _) = ann a
ann

-- TODO: swap parameters
-- |Maps over a 'HolesAnn' treating annotations and holes
-- independently.
holesMapAnnM :: (Monad m)
             => (forall x . f x   -> m (g x)) -- ^ Function to transform holes
             -> (forall x . ann x -> m (psi x)) -- ^ Function to transform annotations
             -> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam psi g a)
holesMapAnnM :: (forall x. f x -> m (g x))
-> (forall x. ann x -> m (psi x))
-> HolesAnn kappa fam ann f a
-> m (HolesAnn kappa fam psi g a)
holesMapAnnM f :: forall x. f x -> m (g x)
f g :: forall x. ann x -> m (psi x)
g (Hole' a :: ann a
a x :: f a
x)   = psi a -> g a -> HolesAnn kappa fam psi g a
forall (ann :: * -> *) a (h :: * -> *) (kappa :: [*]) (fam :: [*]).
ann a -> h a -> HolesAnn kappa fam ann h a
Hole' (psi a -> g a -> HolesAnn kappa fam psi g a)
-> m (psi a) -> m (g a -> HolesAnn kappa fam psi g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ann a -> m (psi a)
forall x. ann x -> m (psi x)
g ann a
a m (g a -> HolesAnn kappa fam psi g a)
-> m (g a) -> m (HolesAnn kappa fam psi g a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f a -> m (g a)
forall x. f x -> m (g x)
f f a
x
holesMapAnnM _ g :: forall x. ann x -> m (psi x)
g (Prim' a :: ann a
a x :: a
x)   = (psi a -> a -> HolesAnn kappa fam psi g a)
-> a -> psi a -> HolesAnn kappa fam psi g a
forall a b c. (a -> b -> c) -> b -> a -> c
flip psi a -> a -> HolesAnn kappa fam psi g a
forall (kappa :: [*]) (fam :: [*]) a (ann :: * -> *) (h :: * -> *).
PrimCnstr kappa fam a =>
ann a -> a -> HolesAnn kappa fam ann h a
Prim' a
x (psi a -> HolesAnn kappa fam psi g a)
-> m (psi a) -> m (HolesAnn kappa fam psi g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ann a -> m (psi a)
forall x. ann x -> m (psi x)
g ann a
a
holesMapAnnM f :: forall x. f x -> m (g x)
f g :: forall x. ann x -> m (psi x)
g (Roll' a :: ann a
a x :: SRep (HolesAnn kappa fam ann f) (Rep a)
x) = psi a
-> SRep (HolesAnn kappa fam psi g) (Rep a)
-> HolesAnn kappa fam psi g a
forall (kappa :: [*]) (fam :: [*]) a (ann :: * -> *) (h :: * -> *).
CompoundCnstr kappa fam a =>
ann a
-> SRep (HolesAnn kappa fam ann h) (Rep a)
-> HolesAnn kappa fam ann h a
Roll' (psi a
 -> SRep (HolesAnn kappa fam psi g) (Rep a)
 -> HolesAnn kappa fam psi g a)
-> m (psi a)
-> m (SRep (HolesAnn kappa fam psi g) (Rep a)
      -> HolesAnn kappa fam psi g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ann a -> m (psi a)
forall x. ann x -> m (psi x)
g ann a
a m (SRep (HolesAnn kappa fam psi g) (Rep a)
   -> HolesAnn kappa fam psi g a)
-> m (SRep (HolesAnn kappa fam psi g) (Rep a))
-> m (HolesAnn kappa fam psi g a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall y.
 HolesAnn kappa fam ann f y -> m (HolesAnn kappa fam psi g y))
-> SRep (HolesAnn kappa fam ann f) (Rep a)
-> m (SRep (HolesAnn kappa fam psi g) (Rep a))
forall k (m :: * -> *) (f :: * -> *) (g :: * -> *) (rep :: k -> *).
Monad m =>
(forall y. f y -> m (g y)) -> SRep f rep -> m (SRep g rep)
repMapM ((forall x. f x -> m (g x))
-> (forall x. ann x -> m (psi x))
-> HolesAnn kappa fam ann f y
-> m (HolesAnn kappa fam psi g y)
forall (m :: * -> *) (f :: * -> *) (g :: * -> *) (ann :: * -> *)
       (psi :: * -> *) (kappa :: [*]) (fam :: [*]) a.
Monad m =>
(forall x. f x -> m (g x))
-> (forall x. ann x -> m (psi x))
-> HolesAnn kappa fam ann f a
-> m (HolesAnn kappa fam psi g a)
holesMapAnnM forall x. f x -> m (g x)
f forall x. ann x -> m (psi x)
g) SRep (HolesAnn kappa fam ann f) (Rep a)
x

-- |Maps over 'HolesAnn' maintaining annotations intact.
holesMapM :: (Monad m)
          => (forall x . f x -> m (g x))
          -> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam ann g a)
holesMapM :: (forall x. f x -> m (g x))
-> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam ann g a)
holesMapM f :: forall x. f x -> m (g x)
f = (forall x. f x -> m (g x))
-> (forall x. ann x -> m (ann x))
-> HolesAnn kappa fam ann f a
-> m (HolesAnn kappa fam ann g a)
forall (m :: * -> *) (f :: * -> *) (g :: * -> *) (ann :: * -> *)
       (psi :: * -> *) (kappa :: [*]) (fam :: [*]) a.
Monad m =>
(forall x. f x -> m (g x))
-> (forall x. ann x -> m (psi x))
-> HolesAnn kappa fam ann f a
-> m (HolesAnn kappa fam psi g a)
holesMapAnnM forall x. f x -> m (g x)
f forall x. ann x -> m (ann x)
forall (m :: * -> *) a. Monad m => a -> m a
return

-- |Maps over the holes in a 'HolesAnn'
holesMap :: (forall x . f x -> g x)
         -> HolesAnn kappa fam ann f a -> HolesAnn kappa fam ann g a
holesMap :: (forall x. f x -> g x)
-> HolesAnn kappa fam ann f a -> HolesAnn kappa fam ann g a
holesMap f :: forall x. f x -> g x
f = Identity (HolesAnn kappa fam ann g a) -> HolesAnn kappa fam ann g a
forall a. Identity a -> a
runIdentity (Identity (HolesAnn kappa fam ann g a)
 -> HolesAnn kappa fam ann g a)
-> (HolesAnn kappa fam ann f a
    -> Identity (HolesAnn kappa fam ann g a))
-> HolesAnn kappa fam ann f a
-> HolesAnn kappa fam ann g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall x. f x -> Identity (g x))
-> HolesAnn kappa fam ann f a
-> Identity (HolesAnn kappa fam ann g a)
forall (m :: * -> *) (f :: * -> *) (g :: * -> *) (kappa :: [*])
       (fam :: [*]) (ann :: * -> *) a.
Monad m =>
(forall x. f x -> m (g x))
-> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam ann g a)
holesMapM (g x -> Identity (g x)
forall (m :: * -> *) a. Monad m => a -> m a
return (g x -> Identity (g x)) -> (f x -> g x) -> f x -> Identity (g x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> g x
forall x. f x -> g x
f)

-- |Maps over holes and annotations in a 'HolesAnn'
holesMapAnn :: (forall x . f   x -> g x)
            -> (forall x . ann x -> phi x)
            -> HolesAnn kappa fam ann f a -> HolesAnn kappa fam phi g a
holesMapAnn :: (forall x. f x -> g x)
-> (forall x. ann x -> phi x)
-> HolesAnn kappa fam ann f a
-> HolesAnn kappa fam phi g a
holesMapAnn f :: forall x. f x -> g x
f g :: forall x. ann x -> phi x
g = Identity (HolesAnn kappa fam phi g a) -> HolesAnn kappa fam phi g a
forall a. Identity a -> a
runIdentity (Identity (HolesAnn kappa fam phi g a)
 -> HolesAnn kappa fam phi g a)
-> (HolesAnn kappa fam ann f a
    -> Identity (HolesAnn kappa fam phi g a))
-> HolesAnn kappa fam ann f a
-> HolesAnn kappa fam phi g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall x. f x -> Identity (g x))
-> (forall x. ann x -> Identity (phi x))
-> HolesAnn kappa fam ann f a
-> Identity (HolesAnn kappa fam phi g a)
forall (m :: * -> *) (f :: * -> *) (g :: * -> *) (ann :: * -> *)
       (psi :: * -> *) (kappa :: [*]) (fam :: [*]) a.
Monad m =>
(forall x. f x -> m (g x))
-> (forall x. ann x -> m (psi x))
-> HolesAnn kappa fam ann f a
-> m (HolesAnn kappa fam psi g a)
holesMapAnnM (g x -> Identity (g x)
forall (m :: * -> *) a. Monad m => a -> m a
return (g x -> Identity (g x)) -> (f x -> g x) -> f x -> Identity (g x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> g x
forall x. f x -> g x
f) (phi x -> Identity (phi x)
forall (m :: * -> *) a. Monad m => a -> m a
return (phi x -> Identity (phi x))
-> (ann x -> phi x) -> ann x -> Identity (phi x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann x -> phi x
forall x. ann x -> phi x
g)

-- |Monadic multiplication
holesJoin :: HolesAnn kappa fam ann (HolesAnn kappa fam ann f) a
          -> HolesAnn kappa fam ann f a
holesJoin :: HolesAnn kappa fam ann (HolesAnn kappa fam ann f) a
-> HolesAnn kappa fam ann f a
holesJoin (Hole' _ x :: HolesAnn kappa fam ann f a
x) = HolesAnn kappa fam ann f a
x
holesJoin (Prim' a :: ann a
a x :: a
x) = ann a -> a -> HolesAnn kappa fam ann f a
forall (kappa :: [*]) (fam :: [*]) a (ann :: * -> *) (h :: * -> *).
PrimCnstr kappa fam a =>
ann a -> a -> HolesAnn kappa fam ann h a
Prim' ann a
a a
x
holesJoin (Roll' a :: ann a
a x :: SRep (HolesAnn kappa fam ann (HolesAnn kappa fam ann f)) (Rep a)
x) = ann a
-> SRep (HolesAnn kappa fam ann f) (Rep a)
-> HolesAnn kappa fam ann f a
forall (kappa :: [*]) (fam :: [*]) a (ann :: * -> *) (h :: * -> *).
CompoundCnstr kappa fam a =>
ann a
-> SRep (HolesAnn kappa fam ann h) (Rep a)
-> HolesAnn kappa fam ann h a
Roll' ann a
a ((forall y.
 HolesAnn kappa fam ann (HolesAnn kappa fam ann f) y
 -> HolesAnn kappa fam ann f y)
-> SRep (HolesAnn kappa fam ann (HolesAnn kappa fam ann f)) (Rep a)
-> SRep (HolesAnn kappa fam ann f) (Rep a)
forall k (f :: * -> *) (g :: * -> *) (rep :: k -> *).
(forall y. f y -> g y) -> SRep f rep -> SRep g rep
repMap forall (kappa :: [*]) (fam :: [*]) (ann :: * -> *) (f :: * -> *) a.
HolesAnn kappa fam ann (HolesAnn kappa fam ann f) a
-> HolesAnn kappa fam ann f a
forall y.
HolesAnn kappa fam ann (HolesAnn kappa fam ann f) y
-> HolesAnn kappa fam ann f y
holesJoin SRep (HolesAnn kappa fam ann (HolesAnn kappa fam ann f)) (Rep a)
x)

-- |Computes the list of holes in a 'HolesAnn'
holesHolesList :: HolesAnn kappa fam ann f a -> [Exists f]
holesHolesList :: HolesAnn kappa fam ann f a -> [Exists f]
holesHolesList (Hole' _ x :: f a
x) = [f a -> Exists f
forall k (f :: k -> *) (x :: k). f x -> Exists f
Exists f a
x]
holesHolesList (Prim' _ _) = []
holesHolesList (Roll' _ x :: SRep (HolesAnn kappa fam ann f) (Rep a)
x) = (Exists (HolesAnn kappa fam ann f) -> [Exists f])
-> [Exists (HolesAnn kappa fam ann f)] -> [Exists f]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((forall x. HolesAnn kappa fam ann f x -> [Exists f])
-> Exists (HolesAnn kappa fam ann f) -> [Exists f]
forall k (f :: k -> *) a.
(forall (x :: k). f x -> a) -> Exists f -> a
exElim forall (kappa :: [*]) (fam :: [*]) (ann :: * -> *) (f :: * -> *) a.
HolesAnn kappa fam ann f a -> [Exists f]
forall x. HolesAnn kappa fam ann f x -> [Exists f]
holesHolesList) ([Exists (HolesAnn kappa fam ann f)] -> [Exists f])
-> [Exists (HolesAnn kappa fam ann f)] -> [Exists f]
forall a b. (a -> b) -> a -> b
$ SRep (HolesAnn kappa fam ann f) (Rep a)
-> [Exists (HolesAnn kappa fam ann f)]
forall k (w :: * -> *) (rep :: k -> *). SRep w rep -> [Exists w]
repLeavesList SRep (HolesAnn kappa fam ann f) (Rep a)
x

{-
holesHolesSet :: (Ord (Exists f)) => Holes kappa fam f a -> S.Set (Exists f)
holesHolesSet = S.fromList . holesHolesList
-}

-- TODO: Implement holesMap in terms of refine; its much better!

-- |Refines holes using a monadic action
holesRefineHolesM :: (Monad m)
                  => (forall b . f b -> m (Holes kappa fam g b))
                  -> Holes kappa fam f a
                  -> m (Holes kappa fam g a)
holesRefineHolesM :: (forall b. f b -> m (Holes kappa fam g b))
-> Holes kappa fam f a -> m (Holes kappa fam g a)
holesRefineHolesM f :: forall b. f b -> m (Holes kappa fam g b)
f = (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a
 -> Holes kappa fam g a)
-> m (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
-> m (Holes kappa fam g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a
-> Holes kappa fam g a
forall (kappa :: [*]) (fam :: [*]) (ann :: * -> *) (f :: * -> *) a.
HolesAnn kappa fam ann (HolesAnn kappa fam ann f) a
-> HolesAnn kappa fam ann f a
holesJoin (m (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
 -> m (Holes kappa fam g a))
-> (Holes kappa fam f a
    -> m (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a))
-> Holes kappa fam f a
-> m (Holes kappa fam g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall b. f b -> m (Holes kappa fam g b))
-> Holes kappa fam f a
-> m (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
forall (m :: * -> *) (f :: * -> *) (g :: * -> *) (kappa :: [*])
       (fam :: [*]) (ann :: * -> *) a.
Monad m =>
(forall x. f x -> m (g x))
-> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam ann g a)
holesMapM forall b. f b -> m (Holes kappa fam g b)
f

-- |Refine holes with a simple action
holesRefineHoles :: (forall b . f b -> Holes kappa fam g b)
                 -> Holes kappa fam f a
                 -> Holes kappa fam g a
holesRefineHoles :: (forall b. f b -> Holes kappa fam g b)
-> Holes kappa fam f a -> Holes kappa fam g a
holesRefineHoles f :: forall b. f b -> Holes kappa fam g b
f = HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a
-> Holes kappa fam g a
forall (kappa :: [*]) (fam :: [*]) (ann :: * -> *) (f :: * -> *) a.
HolesAnn kappa fam ann (HolesAnn kappa fam ann f) a
-> HolesAnn kappa fam ann f a
holesJoin (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a
 -> Holes kappa fam g a)
-> (Holes kappa fam f a
    -> HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
-> Holes kappa fam f a
-> Holes kappa fam g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
-> HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a
forall a. Identity a -> a
runIdentity (Identity (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
 -> HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
-> (Holes kappa fam f a
    -> Identity (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a))
-> Holes kappa fam f a
-> HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall x. f x -> Identity (HolesAnn kappa fam U1 g x))
-> Holes kappa fam f a
-> Identity (HolesAnn kappa fam U1 (HolesAnn kappa fam U1 g) a)
forall (m :: * -> *) (f :: * -> *) (g :: * -> *) (kappa :: [*])
       (fam :: [*]) (ann :: * -> *) a.
Monad m =>
(forall x. f x -> m (g x))
-> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam ann g a)
holesMapM (Holes kappa fam g x -> Identity (Holes kappa fam g x)
forall (m :: * -> *) a. Monad m => a -> m a
return (Holes kappa fam g x -> Identity (Holes kappa fam g x))
-> (f x -> Holes kappa fam g x)
-> f x
-> Identity (Holes kappa fam g x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> Holes kappa fam g x
forall b. f b -> Holes kappa fam g b
f)

-- |Refine holes and primitives
holesRefineM :: (Monad m)
             => (forall b . f b -> m (Holes kappa fam g b))
             -> (forall b . (PrimCnstr kappa fam b)
                  => b -> m (Holes kappa fam g b))
             -> Holes kappa fam f a
             -> m (Holes kappa fam g a)
holesRefineM :: (forall b. f b -> m (Holes kappa fam g b))
-> (forall b.
    PrimCnstr kappa fam b =>
    b -> m (Holes kappa fam g b))
-> Holes kappa fam f a
-> m (Holes kappa fam g a)
holesRefineM f :: forall b. f b -> m (Holes kappa fam g b)
f _ (Hole x :: f a
x) = f a -> m (Holes kappa fam g a)
forall b. f b -> m (Holes kappa fam g b)
f f a
x
holesRefineM _ g :: forall b. PrimCnstr kappa fam b => b -> m (Holes kappa fam g b)
g (Prim x :: a
x) = a -> m (Holes kappa fam g a)
forall b. PrimCnstr kappa fam b => b -> m (Holes kappa fam g b)
g a
x
holesRefineM f :: forall b. f b -> m (Holes kappa fam g b)
f g :: forall b. PrimCnstr kappa fam b => b -> m (Holes kappa fam g b)
g (Roll x :: SRep (Holes kappa fam f) (Rep a)
x) = SRep (Holes kappa fam g) (Rep a) -> Holes kappa fam g a
forall (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
CompoundCnstr kappa fam a =>
SRep (Holes kappa fam h) (Rep a) -> Holes kappa fam h a
Roll (SRep (Holes kappa fam g) (Rep a) -> Holes kappa fam g a)
-> m (SRep (Holes kappa fam g) (Rep a)) -> m (Holes kappa fam g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall y. Holes kappa fam f y -> m (Holes kappa fam g y))
-> SRep (Holes kappa fam f) (Rep a)
-> m (SRep (Holes kappa fam g) (Rep a))
forall k (m :: * -> *) (f :: * -> *) (g :: * -> *) (rep :: k -> *).
Monad m =>
(forall y. f y -> m (g y)) -> SRep f rep -> m (SRep g rep)
repMapM ((forall b. f b -> m (Holes kappa fam g b))
-> (forall b.
    PrimCnstr kappa fam b =>
    b -> m (Holes kappa fam g b))
-> Holes kappa fam f y
-> m (Holes kappa fam g y)
forall (m :: * -> *) (f :: * -> *) (kappa :: [*]) (fam :: [*])
       (g :: * -> *) a.
Monad m =>
(forall b. f b -> m (Holes kappa fam g b))
-> (forall b.
    PrimCnstr kappa fam b =>
    b -> m (Holes kappa fam g b))
-> Holes kappa fam f a
-> m (Holes kappa fam g a)
holesRefineM forall b. f b -> m (Holes kappa fam g b)
f forall b. PrimCnstr kappa fam b => b -> m (Holes kappa fam g b)
g) SRep (Holes kappa fam f) (Rep a)
x

-- |Counts how many 'Prim's and 'Roll's are inside a 'HolesAnn'.
holesSize :: HolesAnn kappa fam ann h a -> Int
holesSize :: HolesAnn kappa fam ann h a -> Int
holesSize (Hole' _ _) = 0
holesSize (Prim' _ _) = 1
holesSize (Roll' _ x :: SRep (HolesAnn kappa fam ann h) (Rep a)
x) = 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Exists (HolesAnn kappa fam ann h) -> Int)
-> [Exists (HolesAnn kappa fam ann h)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map ((forall x. HolesAnn kappa fam ann h x -> Int)
-> Exists (HolesAnn kappa fam ann h) -> Int
forall k (f :: k -> *) a.
(forall (x :: k). f x -> a) -> Exists f -> a
exElim forall (kappa :: [*]) (fam :: [*]) (ann :: * -> *) (h :: * -> *) a.
HolesAnn kappa fam ann h a -> Int
forall x. HolesAnn kappa fam ann h x -> Int
holesSize) ([Exists (HolesAnn kappa fam ann h)] -> [Int])
-> [Exists (HolesAnn kappa fam ann h)] -> [Int]
forall a b. (a -> b) -> a -> b
$ SRep (HolesAnn kappa fam ann h) (Rep a)
-> [Exists (HolesAnn kappa fam ann h)]
forall k (w :: * -> *) (rep :: k -> *). SRep w rep -> [Exists w]
repLeavesList SRep (HolesAnn kappa fam ann h) (Rep a)
x)

-- |Catamorphism over 'HolesAnn'
cataM :: (Monad m)
      => (forall b . (CompoundCnstr kappa fam b)
            => ann b -> SRep phi (Rep b) -> m (phi b)) -- ^ How to handle recursion
      -> (forall b . (PrimCnstr kappa fam b)
            => ann b -> b -> m (phi b)) -- ^ How to handle primitivies
      -> (forall b . ann b -> h b -> m (phi b)) -- ^ How to handle holes
      -> HolesAnn kappa fam ann h a
      -> m (phi a)
cataM :: (forall b.
 CompoundCnstr kappa fam b =>
 ann b -> SRep phi (Rep b) -> m (phi b))
-> (forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b))
-> (forall b. ann b -> h b -> m (phi b))
-> HolesAnn kappa fam ann h a
-> m (phi a)
cataM f :: forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b)
f g :: forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b)
g h :: forall b. ann b -> h b -> m (phi b)
h (Roll' ann :: ann a
ann x :: SRep (HolesAnn kappa fam ann h) (Rep a)
x) = (forall y. HolesAnn kappa fam ann h y -> m (phi y))
-> SRep (HolesAnn kappa fam ann h) (Rep a) -> m (SRep phi (Rep a))
forall k (m :: * -> *) (f :: * -> *) (g :: * -> *) (rep :: k -> *).
Monad m =>
(forall y. f y -> m (g y)) -> SRep f rep -> m (SRep g rep)
repMapM ((forall b.
 CompoundCnstr kappa fam b =>
 ann b -> SRep phi (Rep b) -> m (phi b))
-> (forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b))
-> (forall b. ann b -> h b -> m (phi b))
-> HolesAnn kappa fam ann h y
-> m (phi y)
forall (m :: * -> *) (kappa :: [*]) (fam :: [*]) (ann :: * -> *)
       (phi :: * -> *) (h :: * -> *) a.
Monad m =>
(forall b.
 CompoundCnstr kappa fam b =>
 ann b -> SRep phi (Rep b) -> m (phi b))
-> (forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b))
-> (forall b. ann b -> h b -> m (phi b))
-> HolesAnn kappa fam ann h a
-> m (phi a)
cataM forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b)
f forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b)
g forall b. ann b -> h b -> m (phi b)
h) SRep (HolesAnn kappa fam ann h) (Rep a)
x m (SRep phi (Rep a))
-> (SRep phi (Rep a) -> m (phi a)) -> m (phi a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ann a -> SRep phi (Rep a) -> m (phi a)
forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b)
f ann a
ann
cataM _ g :: forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b)
g _ (Prim' ann :: ann a
ann x :: a
x) = ann a -> a -> m (phi a)
forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b)
g ann a
ann a
x
cataM _ _ h :: forall b. ann b -> h b -> m (phi b)
h (Hole' ann :: ann a
ann x :: h a
x) = ann a -> h a -> m (phi a)
forall b. ann b -> h b -> m (phi b)
h ann a
ann h a
x

-- |Synthetization of attributes
synthesizeM :: (Monad m)
            => (forall b . (CompoundCnstr kappa fam b)
                  => ann b -> SRep phi (Rep b) -> m (phi b)) -- ^ How to handle recursion
            -> (forall b . (PrimCnstr kappa fam b)
                  => ann b -> b -> m (phi b)) -- ^ How to handle primitives
           -> (forall b . ann b -> h b -> m (phi b)) -- ^ How to handle holes
            -> HolesAnn kappa fam ann h a
            -> m (HolesAnn kappa fam phi h a)
synthesizeM :: (forall b.
 CompoundCnstr kappa fam b =>
 ann b -> SRep phi (Rep b) -> m (phi b))
-> (forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b))
-> (forall b. ann b -> h b -> m (phi b))
-> HolesAnn kappa fam ann h a
-> m (HolesAnn kappa fam phi h a)
synthesizeM f :: forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b)
f g :: forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b)
g h :: forall b. ann b -> h b -> m (phi b)
h = (forall b.
 CompoundCnstr kappa fam b =>
 ann b
 -> SRep (HolesAnn kappa fam phi h) (Rep b)
 -> m (HolesAnn kappa fam phi h b))
-> (forall b.
    PrimCnstr kappa fam b =>
    ann b -> b -> m (HolesAnn kappa fam phi h b))
-> (forall b. ann b -> h b -> m (HolesAnn kappa fam phi h b))
-> HolesAnn kappa fam ann h a
-> m (HolesAnn kappa fam phi h a)
forall (m :: * -> *) (kappa :: [*]) (fam :: [*]) (ann :: * -> *)
       (phi :: * -> *) (h :: * -> *) a.
Monad m =>
(forall b.
 CompoundCnstr kappa fam b =>
 ann b -> SRep phi (Rep b) -> m (phi b))
-> (forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b))
-> (forall b. ann b -> h b -> m (phi b))
-> HolesAnn kappa fam ann h a
-> m (phi a)
cataM (\ann :: ann b
ann r :: SRep (HolesAnn kappa fam phi h) (Rep b)
r -> (phi b
 -> SRep (HolesAnn kappa fam phi h) (Rep b)
 -> HolesAnn kappa fam phi h b)
-> SRep (HolesAnn kappa fam phi h) (Rep b)
-> phi b
-> HolesAnn kappa fam phi h b
forall a b c. (a -> b -> c) -> b -> a -> c
flip phi b
-> SRep (HolesAnn kappa fam phi h) (Rep b)
-> HolesAnn kappa fam phi h b
forall (kappa :: [*]) (fam :: [*]) a (ann :: * -> *) (h :: * -> *).
CompoundCnstr kappa fam a =>
ann a
-> SRep (HolesAnn kappa fam ann h) (Rep a)
-> HolesAnn kappa fam ann h a
Roll' SRep (HolesAnn kappa fam phi h) (Rep b)
r
                                (phi b -> HolesAnn kappa fam phi h b)
-> m (phi b) -> m (HolesAnn kappa fam phi h b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ann b -> SRep phi (Rep b) -> m (phi b)
forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> m (phi b)
f ann b
ann ((forall y. HolesAnn kappa fam phi h y -> phi y)
-> SRep (HolesAnn kappa fam phi h) (Rep b) -> SRep phi (Rep b)
forall k (f :: * -> *) (g :: * -> *) (rep :: k -> *).
(forall y. f y -> g y) -> SRep f rep -> SRep g rep
repMap forall (kappa :: [*]) (fam :: [*]) (ann :: * -> *) (h :: * -> *) a.
HolesAnn kappa fam ann h a -> ann a
forall y. HolesAnn kappa fam phi h y -> phi y
getAnn SRep (HolesAnn kappa fam phi h) (Rep b)
r))
                          (\ann :: ann b
ann b :: b
b -> (phi b -> b -> HolesAnn kappa fam phi h b)
-> b -> phi b -> HolesAnn kappa fam phi h b
forall a b c. (a -> b -> c) -> b -> a -> c
flip phi b -> b -> HolesAnn kappa fam phi h b
forall (kappa :: [*]) (fam :: [*]) a (ann :: * -> *) (h :: * -> *).
PrimCnstr kappa fam a =>
ann a -> a -> HolesAnn kappa fam ann h a
Prim' b
b (phi b -> HolesAnn kappa fam phi h b)
-> m (phi b) -> m (HolesAnn kappa fam phi h b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ann b -> b -> m (phi b)
forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b)
g ann b
ann b
b)
                          (\ann :: ann b
ann r :: h b
r -> (phi b -> h b -> HolesAnn kappa fam phi h b)
-> h b -> phi b -> HolesAnn kappa fam phi h b
forall a b c. (a -> b -> c) -> b -> a -> c
flip phi b -> h b -> HolesAnn kappa fam phi h b
forall (ann :: * -> *) a (h :: * -> *) (kappa :: [*]) (fam :: [*]).
ann a -> h a -> HolesAnn kappa fam ann h a
Hole' h b
r (phi b -> HolesAnn kappa fam phi h b)
-> m (phi b) -> m (HolesAnn kappa fam phi h b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ann b -> h b -> m (phi b)
forall b. ann b -> h b -> m (phi b)
h ann b
ann h b
r)

-- |Simpler version of 'synthesizeM' working over the /Identity/ monad.
synthesize :: (forall b . (CompoundCnstr kappa fam b)
                 => ann b -> SRep phi (Rep b) -> phi b)
           -> (forall b . (PrimCnstr kappa fam b)
                 => ann b -> b -> phi b)
           -> (forall b . ann b -> h b -> phi b)
           -> HolesAnn kappa fam ann h a
           -> HolesAnn kappa fam phi h a
synthesize :: (forall b.
 CompoundCnstr kappa fam b =>
 ann b -> SRep phi (Rep b) -> phi b)
-> (forall b. PrimCnstr kappa fam b => ann b -> b -> phi b)
-> (forall b. ann b -> h b -> phi b)
-> HolesAnn kappa fam ann h a
-> HolesAnn kappa fam phi h a
synthesize f :: forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> phi b
f g :: forall b. PrimCnstr kappa fam b => ann b -> b -> phi b
g h :: forall b. ann b -> h b -> phi b
h = Identity (HolesAnn kappa fam phi h a) -> HolesAnn kappa fam phi h a
forall a. Identity a -> a
runIdentity
                 (Identity (HolesAnn kappa fam phi h a)
 -> HolesAnn kappa fam phi h a)
-> (HolesAnn kappa fam ann h a
    -> Identity (HolesAnn kappa fam phi h a))
-> HolesAnn kappa fam ann h a
-> HolesAnn kappa fam phi h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall b.
 CompoundCnstr kappa fam b =>
 ann b -> SRep phi (Rep b) -> Identity (phi b))
-> (forall b.
    PrimCnstr kappa fam b =>
    ann b -> b -> Identity (phi b))
-> (forall b. ann b -> h b -> Identity (phi b))
-> HolesAnn kappa fam ann h a
-> Identity (HolesAnn kappa fam phi h a)
forall (m :: * -> *) (kappa :: [*]) (fam :: [*]) (ann :: * -> *)
       (phi :: * -> *) (h :: * -> *) a.
Monad m =>
(forall b.
 CompoundCnstr kappa fam b =>
 ann b -> SRep phi (Rep b) -> m (phi b))
-> (forall b. PrimCnstr kappa fam b => ann b -> b -> m (phi b))
-> (forall b. ann b -> h b -> m (phi b))
-> HolesAnn kappa fam ann h a
-> m (HolesAnn kappa fam phi h a)
synthesizeM (\ann :: ann b
ann -> phi b -> Identity (phi b)
forall (m :: * -> *) a. Monad m => a -> m a
return (phi b -> Identity (phi b))
-> (SRep phi (Rep b) -> phi b)
-> SRep phi (Rep b)
-> Identity (phi b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann b -> SRep phi (Rep b) -> phi b
forall b.
CompoundCnstr kappa fam b =>
ann b -> SRep phi (Rep b) -> phi b
f ann b
ann)
                               (\ann :: ann b
ann -> phi b -> Identity (phi b)
forall (m :: * -> *) a. Monad m => a -> m a
return (phi b -> Identity (phi b))
-> (b -> phi b) -> b -> Identity (phi b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann b -> b -> phi b
forall b. PrimCnstr kappa fam b => ann b -> b -> phi b
g ann b
ann)
                               (\ann :: ann b
ann -> phi b -> Identity (phi b)
forall (m :: * -> *) a. Monad m => a -> m a
return (phi b -> Identity (phi b))
-> (h b -> phi b) -> h b -> Identity (phi b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann b -> h b -> phi b
forall b. ann b -> h b -> phi b
h ann b
ann)

-- Anti unification is so simple it doesn't
-- deserve its own module

-- |Computes the /least general generalization/ of two
-- trees.
lgg :: forall kappa fam h i a
     . (All Eq kappa)
    => Holes kappa fam h a -> Holes kappa fam i a
    -> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
lgg :: Holes kappa fam h a
-> Holes kappa fam i a
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
lgg (Prim x :: a
x) (Prim y :: a
y)
  | Proxy kappa -> a -> a -> Bool
forall x (xs :: [*]).
(All Eq xs, Elem x xs) =>
Proxy xs -> x -> x -> Bool
weq (Proxy kappa
forall k (t :: k). Proxy t
Proxy :: Proxy kappa) a
x a
y = a -> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
forall (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
PrimCnstr kappa fam a =>
a -> Holes kappa fam h a
Prim a
x
  | Bool
otherwise                      = (:*:) (Holes kappa fam h) (Holes kappa fam i) a
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
forall (h :: * -> *) a (kappa :: [*]) (fam :: [*]).
h a -> Holes kappa fam h a
Hole (a -> Holes kappa fam h a
forall (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
PrimCnstr kappa fam a =>
a -> Holes kappa fam h a
Prim a
x Holes kappa fam h a
-> Holes kappa fam i a
-> (:*:) (Holes kappa fam h) (Holes kappa fam i) a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: a -> Holes kappa fam i a
forall (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
PrimCnstr kappa fam a =>
a -> Holes kappa fam h a
Prim a
y)
lgg x :: Holes kappa fam h a
x@(Roll rx :: SRep (Holes kappa fam h) (Rep a)
rx) y :: Holes kappa fam i a
y@(Roll ry :: SRep (Holes kappa fam i) (Rep a)
ry) =
  case SRep (Holes kappa fam h) (Rep a)
-> SRep (Holes kappa fam i) (Rep a)
-> Maybe (SRep (Holes kappa fam h :*: Holes kappa fam i) (Rep a))
forall k (w :: * -> *) (f :: k -> *) (z :: * -> *).
SRep w f -> SRep z f -> Maybe (SRep (w :*: z) f)
zipSRep SRep (Holes kappa fam h) (Rep a)
rx SRep (Holes kappa fam i) (Rep a)
ry of
    Nothing -> (:*:) (Holes kappa fam h) (Holes kappa fam i) a
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
forall (h :: * -> *) a (kappa :: [*]) (fam :: [*]).
h a -> Holes kappa fam h a
Hole (Holes kappa fam h a
x Holes kappa fam h a
-> Holes kappa fam i a
-> (:*:) (Holes kappa fam h) (Holes kappa fam i) a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Holes kappa fam i a
y)
    Just r :: SRep (Holes kappa fam h :*: Holes kappa fam i) (Rep a)
r  -> SRep
  (Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i)) (Rep a)
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
forall (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
CompoundCnstr kappa fam a =>
SRep (Holes kappa fam h) (Rep a) -> Holes kappa fam h a
Roll ((forall y.
 (:*:) (Holes kappa fam h) (Holes kappa fam i) y
 -> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) y)
-> SRep (Holes kappa fam h :*: Holes kappa fam i) (Rep a)
-> SRep
     (Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i)) (Rep a)
forall k (f :: * -> *) (g :: * -> *) (rep :: k -> *).
(forall y. f y -> g y) -> SRep f rep -> SRep g rep
repMap ((HolesAnn kappa fam U1 h y
 -> HolesAnn kappa fam U1 i y
 -> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) y)
-> (:*:) (Holes kappa fam h) (Holes kappa fam i) y
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) y
forall k (f :: k -> *) (x :: k) (g :: k -> *) a.
(f x -> g x -> a) -> (:*:) f g x -> a
uncurry' HolesAnn kappa fam U1 h y
-> HolesAnn kappa fam U1 i y
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) y
forall (kappa :: [*]) (fam :: [*]) (h :: * -> *) (i :: * -> *) a.
All Eq kappa =>
Holes kappa fam h a
-> Holes kappa fam i a
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
lgg) SRep (Holes kappa fam h :*: Holes kappa fam i) (Rep a)
r)
lgg x :: Holes kappa fam h a
x y :: Holes kappa fam i a
y = (:*:) (Holes kappa fam h) (Holes kappa fam i) a
-> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a
forall (h :: * -> *) a (kappa :: [*]) (fam :: [*]).
h a -> Holes kappa fam h a
Hole (Holes kappa fam h a
x Holes kappa fam h a
-> Holes kappa fam i a
-> (:*:) (Holes kappa fam h) (Holes kappa fam i) a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Holes kappa fam i a
y)

----------------------
-- Deep translation --
----------------------

{- It is possible to have a simler GDeep; relying on
-- GShallow. I'll test performance later.

class GDeep' fam prim isPrim a where
  gdfrom'  :: Proxy isPrim -> a -> SFix fam prim a
  gdto'    :: Proxy isPrim -> SFix fam prim a -> a

instance (CompoundCnstr fam prim a , GDeep fam prim a)
     => GDeep' fam prim 'False a where
  gdfrom' _ a = gdfrom $ a
  gdto' _   x = gdto x

instance (PrimCnstr fam prim a) => GDeep' fam prim 'True a where
  gdfrom' _ a = Prim a
  gdto'   _ (Prim a) = a

class GDeep fam prim a where
  gdfrom :: a -> SFix fam prim a
  gdto   :: SFix fam prim a -> a

instance GDeep' fam prim (IsElem a prim) a => GDeep fam prim a where
  gdfrom = gdfrom' (Proxy :: Proxy (IsElem a prim))
  gdto   = gdto'   (Proxy :: Proxy (IsElem a prim))

dfrom :: forall fam prim a
       . (CompoundCnstr fam prim a)
      => a -> SFix fam prim a
dfrom = SFix
      . runIdentity
      . repMapCM (Proxy :: Proxy (GDeep fam prim))
         (\(I x) -> return $ gdfrom x)
      . fromS

-}

class (CompoundCnstr kappa fam a) => Deep kappa fam a where
  dfrom :: a -> SFix kappa fam a
  default dfrom :: (GDeep kappa fam (Rep a)) => a -> SFix kappa fam a
  dfrom = SRep (HolesAnn kappa fam U1 V1) (Rep a) -> SFix kappa fam a
forall (kappa :: [*]) (fam :: [*]) a.
CompoundCnstr kappa fam a =>
SRep (SFix kappa fam) (Rep a) -> SFix kappa fam a
SFix (SRep (HolesAnn kappa fam U1 V1) (Rep a) -> SFix kappa fam a)
-> (a -> SRep (HolesAnn kappa fam U1 V1) (Rep a))
-> a
-> SFix kappa fam a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> SRep (HolesAnn kappa fam U1 V1) (Rep a)
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
f x -> SRep (SFix kappa fam) f
gdfrom (Rep a Any -> SRep (HolesAnn kappa fam U1 V1) (Rep a))
-> (a -> Rep a Any) -> a -> SRep (HolesAnn kappa fam U1 V1) (Rep a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall a x. Generic a => a -> Rep a x
from

  dto :: SFix kappa fam a -> a
  default dto :: (GDeep kappa fam (Rep a)) => SFix kappa fam a -> a
  dto (SFix x :: SRep (HolesAnn kappa fam U1 V1) (Rep a)
x) = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
to (Rep a Any -> a)
-> (SRep (HolesAnn kappa fam U1 V1) (Rep a) -> Rep a Any)
-> SRep (HolesAnn kappa fam U1 V1) (Rep a)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SRep (HolesAnn kappa fam U1 V1) (Rep a) -> Rep a Any
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
SRep (SFix kappa fam) f -> f x
gdto (SRep (HolesAnn kappa fam U1 V1) (Rep a) -> a)
-> SRep (HolesAnn kappa fam U1 V1) (Rep a) -> a
forall a b. (a -> b) -> a -> b
$ SRep (HolesAnn kappa fam U1 V1) (Rep a)
x

class GDeep kappa fam f where
  gdfrom :: f x -> SRep (SFix kappa fam) f
  gdto   :: SRep (SFix kappa fam) f -> f x

class GDeepAtom kappa fam (isPrim :: Bool) a where
  gdfromAtom  :: Proxy isPrim -> a -> SFix kappa fam a
  gdtoAtom    :: Proxy isPrim -> SFix kappa fam a -> a

instance (CompoundCnstr kappa fam a , Deep kappa fam a)
     => GDeepAtom kappa fam 'False a where
  gdfromAtom :: Proxy 'False -> a -> SFix kappa fam a
gdfromAtom _ a :: a
a = a -> SFix kappa fam a
forall (kappa :: [*]) (fam :: [*]) a.
Deep kappa fam a =>
a -> SFix kappa fam a
dfrom (a -> SFix kappa fam a) -> a -> SFix kappa fam a
forall a b. (a -> b) -> a -> b
$ a
a
  gdtoAtom :: Proxy 'False -> SFix kappa fam a -> a
gdtoAtom _   x :: SFix kappa fam a
x = SFix kappa fam a -> a
forall (kappa :: [*]) (fam :: [*]) a.
Deep kappa fam a =>
SFix kappa fam a -> a
dto SFix kappa fam a
x

instance (PrimCnstr kappa fam a) => GDeepAtom kappa fam 'True a where
  gdfromAtom :: Proxy 'True -> a -> SFix kappa fam a
gdfromAtom _ a :: a
a = a -> SFix kappa fam a
forall (kappa :: [*]) (fam :: [*]) a (h :: * -> *).
PrimCnstr kappa fam a =>
a -> Holes kappa fam h a
Prim a
a
  gdtoAtom :: Proxy 'True -> SFix kappa fam a -> a
gdtoAtom   _ (Prim a :: a
a) = a
a

instance (GDeepAtom kappa fam (IsElem a kappa) a) => GDeep kappa fam (K1 R a) where
  gdfrom :: K1 R a x -> SRep (SFix kappa fam) (K1 R a)
gdfrom (K1 a :: a
a)   = HolesAnn kappa fam U1 V1 a -> SRep (SFix kappa fam) (K1 R a)
forall k (w :: * -> *) a i. w a -> SRep w (K1 i a)
S_K1 (Proxy (IsElem a kappa) -> a -> HolesAnn kappa fam U1 V1 a
forall (kappa :: [*]) (fam :: [*]) (isPrim :: Bool) a.
GDeepAtom kappa fam isPrim a =>
Proxy isPrim -> a -> SFix kappa fam a
gdfromAtom (Proxy (IsElem a kappa)
forall k (t :: k). Proxy t
Proxy :: Proxy (IsElem a kappa)) a
a)
  gdto :: SRep (SFix kappa fam) (K1 R a) -> K1 R a x
gdto   (S_K1 a :: SFix kappa fam a
a) = a -> K1 R a x
forall k i c (p :: k). c -> K1 i c p
K1 (Proxy (IsElem a kappa) -> SFix kappa fam a -> a
forall (kappa :: [*]) (fam :: [*]) (isPrim :: Bool) a.
GDeepAtom kappa fam isPrim a =>
Proxy isPrim -> SFix kappa fam a -> a
gdtoAtom (Proxy (IsElem a kappa)
forall k (t :: k). Proxy t
Proxy :: Proxy (IsElem a kappa)) SFix kappa fam a
a)

instance GDeep kappa fam U1 where
  gdfrom :: U1 x -> SRep (SFix kappa fam) U1
gdfrom U1  = SRep (SFix kappa fam) U1
forall k (w :: * -> *). SRep w U1
S_U1
  gdto :: SRep (SFix kappa fam) U1 -> U1 x
gdto S_U1 = U1 x
forall k (p :: k). U1 p
U1

instance (GDeep kappa fam f , GDeep kappa fam g) => GDeep kappa fam (f :*: g) where
  gdfrom :: (:*:) f g x -> SRep (SFix kappa fam) (f :*: g)
gdfrom (x :: f x
x :*: y :: g x
y) = (f x -> SRep (SFix kappa fam) f
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
f x -> SRep (SFix kappa fam) f
gdfrom f x
x) SRep (SFix kappa fam) f
-> SRep (SFix kappa fam) g -> SRep (SFix kappa fam) (f :*: g)
forall k (w :: * -> *) (f :: k -> *) (g :: k -> *).
SRep w f -> SRep w g -> SRep w (f :*: g)
:**: (g x -> SRep (SFix kappa fam) g
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
f x -> SRep (SFix kappa fam) f
gdfrom g x
y)
  gdto :: SRep (SFix kappa fam) (f :*: g) -> (:*:) f g x
gdto (x :: SRep (SFix kappa fam) f
x :**: y :: SRep (SFix kappa fam) g
y) = (SRep (SFix kappa fam) f -> f x
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
SRep (SFix kappa fam) f -> f x
gdto SRep (SFix kappa fam) f
x) f x -> g x -> (:*:) f g x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (SRep (SFix kappa fam) g -> g x
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
SRep (SFix kappa fam) f -> f x
gdto SRep (SFix kappa fam) g
y)

instance (GDeep kappa fam f , GDeep kappa fam g) => GDeep kappa fam (f :+: g) where
  gdfrom :: (:+:) f g x -> SRep (SFix kappa fam) (f :+: g)
gdfrom (L1 x :: f x
x) = SRep (SFix kappa fam) f -> SRep (SFix kappa fam) (f :+: g)
forall k (w :: * -> *) (f :: k -> *) (g :: k -> *).
SRep w f -> SRep w (f :+: g)
S_L1 (f x -> SRep (SFix kappa fam) f
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
f x -> SRep (SFix kappa fam) f
gdfrom f x
x)
  gdfrom (R1 x :: g x
x) = SRep (SFix kappa fam) g -> SRep (SFix kappa fam) (f :+: g)
forall k (w :: * -> *) (g :: k -> *) (f :: k -> *).
SRep w g -> SRep w (f :+: g)
S_R1 (g x -> SRep (SFix kappa fam) g
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
f x -> SRep (SFix kappa fam) f
gdfrom g x
x)

  gdto :: SRep (SFix kappa fam) (f :+: g) -> (:+:) f g x
gdto (S_L1 x :: SRep (SFix kappa fam) f
x) = f x -> (:+:) f g x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (SRep (SFix kappa fam) f -> f x
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
SRep (SFix kappa fam) f -> f x
gdto SRep (SFix kappa fam) f
x)
  gdto (S_R1 x :: SRep (SFix kappa fam) g
x) = g x -> (:+:) f g x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (SRep (SFix kappa fam) g -> g x
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
SRep (SFix kappa fam) f -> f x
gdto SRep (SFix kappa fam) g
x)

instance (GMeta i c , GDeep kappa fam f) => GDeep kappa fam (M1 i c f) where
  gdfrom :: M1 i c f x -> SRep (SFix kappa fam) (M1 i c f)
gdfrom (M1 x :: f x
x)   = SMeta i c
-> SRep (SFix kappa fam) f -> SRep (SFix kappa fam) (M1 i c f)
forall k i (t :: Meta) (w :: * -> *) (f :: k -> *).
SMeta i t -> SRep w f -> SRep w (M1 i t f)
S_M1 SMeta i c
forall k i (c :: k). GMeta i c => SMeta i c
smeta (f x -> SRep (SFix kappa fam) f
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
f x -> SRep (SFix kappa fam) f
gdfrom f x
x)
  gdto :: SRep (SFix kappa fam) (M1 i c f) -> M1 i c f x
gdto (S_M1 _ x :: SRep (SFix kappa fam) f
x) = f x -> M1 i c f x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (SRep (SFix kappa fam) f -> f x
forall k (kappa :: [*]) (fam :: [*]) (f :: k -> *) (x :: k).
GDeep kappa fam f =>
SRep (SFix kappa fam) f -> f x
gdto SRep (SFix kappa fam) f
x)