Generics.Simplistic.Zipper

Provides bare-bones zipper functionality to SRep and Holes.

Documentation

data SZip ty w f where

A value of type 'SZip ty w f' corresponds to a value of type 'SRep w f' with one of its leaves of type w ty absent. This is essentially a zipper for SRep.

Constructors

Z_KH :: SZip ty w (K1 i ty)

Z_L1 :: SZip ty w f -> SZip ty w (f :+: g)

Z_R1 :: SZip ty w g -> SZip ty w (f :+: g)

Z_PairL :: SZip ty w f -> SRep w g -> SZip ty w (f :*: g)

Z_PairR :: SRep w f -> SZip ty w g -> SZip ty w (f :*: g)

Z_M1 :: SMeta i t -> SZip ty w f -> SZip ty w (M1 i t f)

Instances

(forall a. Eq (w a)) => Eq (SZip h w f)

Defined in Generics.Simplistic.Zipper

Methods

(==) :: SZip h w f -> SZip h w f -> Bool

(/=) :: SZip h w f -> SZip h w f -> Bool

(forall a. Show (w a)) => Show (SZip h w f)

Defined in Generics.Simplistic.Zipper

Methods

showsPrec :: Int -> SZip h w f -> ShowS

show :: SZip h w f -> String

showList :: [SZip h w f] -> ShowS

plug :: SZip ty phi f -> phi ty -> SRep phi f

We can transform a SZip into a SRep given we are provided with a value to plug into the identified position.

zipperMap :: (forall x. h x -> g x) -> SZip ty h f -> SZip ty g f

Maps over a SZip

inr1 :: (x :*: y) t -> (Sum z x :*: y) t

zipperRepZip :: SZip ty h f -> SRep w f -> Maybe (SRep (Sum ((:~:) ty) h :*: w) f)

Given a z :: SZip ty h f and a r :: Rep w f, if z and r are made with the same constuctor we return a representation that contains both hs and ws in its leaves, except in one leaf of type ty. This is analogous to zipSRep.

zipSZip :: SZip ty h f -> SZip ty w f -> Maybe (SZip ty (h :*: w) f)

Overlaps two zippers together; only succeeds if both zippers have the same constructor AND hole.

zipLeavesList :: SZip ty w f -> [Maybe (Exists w)]

Analogous to repLeavesList

data Zipper c f g t where

The Zipper datatype packages a SZip in a more standard presentation. A value of type Zipper c f g t represents a value of type SRep f t, where exactly one recursive leaf (of type t) carries a value of type g t, moreover, we also carry a proof that the constraint c holds.

Constructors

Zipper

Fields

• :: c
• => { zipper :: SZip t f (Rep t)
•    , sel :: g t
•    } -> Zipper c f g t

type Zipper' kappa fam ann phi t = Zipper (CompoundCnstr kappa fam t) (HolesAnn kappa fam ann phi) (HolesAnn kappa fam ann phi) t

Auxiliar type synonym for annotated fixpoints.

zippers :: forall kappa fam ann phi t. (forall a. Elem t fam => phi a -> Maybe (a :~: t)) -> HolesAnn kappa fam ann phi t -> [Zipper' kappa fam ann phi t]

Given a function that checks wheter an arbitrary position is recursive and a value of t, returns all possible zippers ove t.

zipConstructorName :: SZip h w f -> String

Retrieves the constructor name for a representation. WARNING; UNSAFE this function only works if f is the representation of a type constructed with GHC.Generics builtin mechanisms.