Generics.Simplistic.Deep

Deep representation for SRep

(Co)Free (Co)Monad and its cousins

data HolesAnn kappa fam ann h a where

The cofree comonad and free monad on the same type; this allows us to use the same recursion operator for everything.

Constructors

Hole'

Fields

• :: ann a

  Annotation

• -> h a
• -> HolesAnn kappa fam ann h a

Prim'

Fields

• :: PrimCnstr kappa fam a
• => ann a

  Annotation

• -> a
• -> HolesAnn kappa fam ann h a

Roll'

Fields

• :: CompoundCnstr kappa fam a
• => ann a

  Annotation

• -> SRep (HolesAnn kappa fam ann h) (Rep a)
• -> HolesAnn kappa fam ann h a

Instances

(All Eq kappa, EqHO h) => EqHO (Holes kappa fam h :: Type -> Type)

Defined in Generics.Simplistic.Deep

Methods

eqHO :: Holes kappa fam h k -> Holes kappa fam h k -> Bool

(All Eq kappa, EqHO h) => Eq (Holes kappa fam h t)

Defined in Generics.Simplistic.Deep

Methods

(==) :: Holes kappa fam h t -> Holes kappa fam h t -> Bool

(/=) :: Holes kappa fam h t -> Holes kappa fam h t -> Bool

(forall x. NFData (ann x), forall x. NFData (h x)) => NFData (HolesAnn kappa fam ann h f)

Defined in Generics.Simplistic.Deep

Methods

rnf :: HolesAnn kappa fam ann h f -> ()

type SFix kappa fam = HolesAnn kappa fam U1 V1

Deep representations are easily achieved by forbiding the Hole' constructor and providing unit annotations.

pattern SFix :: () => CompoundCnstr kappa fam a => SRep (SFix kappa fam) (Rep a) -> SFix kappa fam a

pattern Prim :: () => PrimCnstr kappa fam a => a -> Holes kappa fam h a

type SFixAnn kappa fam ann = HolesAnn kappa fam ann V1

Annotated fixpoints are also easy; forbid the Hole' constructor but add something to every Roll of the representation.

pattern SFixAnn :: () => CompoundCnstr kappa fam a => ann a -> SRep (SFixAnn kappa fam ann) (Rep a) -> SFixAnn kappa fam ann a

pattern PrimAnn :: () => PrimCnstr kappa fam a => ann a -> a -> SFixAnn kappa fam ann a

type Holes kappa fam = HolesAnn kappa fam U1

A tree with holes has unit annotations

pattern Roll :: () => CompoundCnstr kappa fam a => SRep (Holes kappa fam h) (Rep a) -> Holes kappa fam h a

pattern Hole :: h a -> Holes kappa fam h a

Constraints

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

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

Coercions

holesToSFix :: Holes kappa fam V1 at -> SFix kappa fam at

sfixToHoles :: SFix kappa fam at -> Holes kappa fam h at

Maps, zips and folds

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

Maps over holes and annotations in a HolesAnn

holesMap :: (forall x. f x -> g x) -> HolesAnn kappa fam ann f a -> HolesAnn kappa fam ann g a

Maps over the holes in a HolesAnn

holesMapM :: Monad m => (forall x. f x -> m (g x)) -> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam ann g a)

Maps over HolesAnn maintaining annotations intact.

holesMapAnnM

Arguments

:: 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)

Maps over a HolesAnn treating annotations and holes independently.

getAnn :: HolesAnn kappa fam ann h a -> ann a

Retrieves the annotation inside a HolesAnn; this is the counit of the comonad.

holesJoin :: HolesAnn kappa fam ann (HolesAnn kappa fam ann f) a -> HolesAnn kappa fam ann f a

Monadic multiplication

holesSize :: HolesAnn kappa fam ann h a -> Int

Counts how many Prims and Rolls are inside a HolesAnn.

holesHolesList :: HolesAnn kappa fam ann f a -> [Exists f]

Computes the list of holes in a HolesAnn

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)

Refine holes and primitives

holesRefineHoles :: (forall b. f b -> Holes kappa fam g b) -> Holes kappa fam f a -> Holes kappa fam g a

Refine holes with a simple 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)

Refines holes using a monadic action

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

Simpler version of synthesizeM working over the Identity monad.

synthesizeM

Arguments

:: 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)

Synthetization of attributes

cataM

Arguments

:: 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)

Catamorphism over HolesAnn

Anti-Unification

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

Computes the least general generalization of two trees.

Conversion

class CompoundCnstr kappa fam a => Deep kappa fam a where

Minimal complete definition

Nothing

Methods

dfrom :: a -> SFix kappa fam a

dfrom :: GDeep kappa fam (Rep a) => a -> SFix kappa fam a

dto :: SFix kappa fam a -> a

dto :: GDeep kappa fam (Rep a) => SFix kappa fam a -> a

class GDeep kappa fam f where

Methods

gdfrom :: f x -> SRep (SFix kappa fam) f

gdto :: SRep (SFix kappa fam) f -> f x

Instances

GDeep kappa fam (U1 :: k -> Type)

Defined in Generics.Simplistic.Deep

Methods

gdfrom :: U1 x -> SRep (SFix kappa fam) U1

gdto :: SRep (SFix kappa fam) U1 -> U1 x

(GDeep kappa fam f, GDeep kappa fam g) => GDeep kappa fam (f :+: g :: k -> Type)

Defined in Generics.Simplistic.Deep

Methods

gdfrom :: (f :+: g) x -> SRep (SFix kappa fam) (f :+: g)

gdto :: SRep (SFix kappa fam) (f :+: g) -> (f :+: g) x

(GDeep kappa fam f, GDeep kappa fam g) => GDeep kappa fam (f :*: g :: k -> Type)

Defined in Generics.Simplistic.Deep

Methods

gdfrom :: (f :*: g) x -> SRep (SFix kappa fam) (f :*: g)

gdto :: SRep (SFix kappa fam) (f :*: g) -> (f :*: g) x

GDeepAtom kappa fam (IsElem a kappa) a => GDeep kappa fam (K1 R a :: k -> Type)

Defined in Generics.Simplistic.Deep

Methods

gdfrom :: K1 R a x -> SRep (SFix kappa fam) (K1 R a)

gdto :: SRep (SFix kappa fam) (K1 R a) -> K1 R a x

(GMeta i c, GDeep kappa fam f) => GDeep kappa fam (M1 i c f :: k -> Type)

Defined in Generics.Simplistic.Deep

Methods

gdfrom :: M1 i c f x -> SRep (SFix kappa fam) (M1 i c f)

gdto :: SRep (SFix kappa fam) (M1 i c f) -> M1 i c f x

Orphan instances

NFData (V1 x)

Methods

rnf :: V1 x -> ()

NFData (U1 x)

Methods

rnf :: U1 x -> ()