Data.HDiff.MetaVar

Exports a bunch of functionality for handling metavariables both over recursive positions only, with MetaVarI and over recursive positions and constants, MetaVarIK.

Documentation

data ForceI :: (Nat -> *) -> Atom kon -> * where

Given a functor from Nat to *, lift it to work over Atom by forcing the atom to be an I.

Constructors

ForceI

Fields

• :: IsNat i
• => { unForceI :: f i
•    } -> ForceI f (I i)

Instances

Eq (Exists (MetaVarI :: Atom kon -> Type))

Defined in Data.HDiff.MetaVar

Methods

(==) :: Exists MetaVarI -> Exists MetaVarI -> Bool

(/=) :: Exists MetaVarI -> Exists MetaVarI -> Bool

Ord (Exists (MetaVarI :: Atom kon -> Type))

Defined in Data.HDiff.MetaVar

Methods

compare :: Exists MetaVarI -> Exists MetaVarI -> Ordering

(<) :: Exists MetaVarI -> Exists MetaVarI -> Bool

(<=) :: Exists MetaVarI -> Exists MetaVarI -> Bool

(>) :: Exists MetaVarI -> Exists MetaVarI -> Bool

(>=) :: Exists MetaVarI -> Exists MetaVarI -> Bool

max :: Exists MetaVarI -> Exists MetaVarI -> Exists MetaVarI

min :: Exists MetaVarI -> Exists MetaVarI -> Exists MetaVarI

type MetaVarI = ForceI (Const Int)

A MetaVarI can only take place of a recursive position.

data Annotate (x :: *) (f :: k -> *) :: k -> * where

This is isomorphic to const x &&& f on the type level.

Constructors

Annotate :: x -> f i -> Annotate x f i

Instances

HasIKProjInj (ki :: kon -> Type) (MetaVarIK ki :: Atom kon -> Type)

Defined in Data.HDiff.MetaVar

Methods

konInj :: ki k -> MetaVarIK ki (K k)

varProj :: Proxy ki -> MetaVarIK ki x -> Maybe (IsI x)

HasIKProjInj (ki :: kon -> Type) (Holes2 ki codes :: Atom kon -> Type)

Defined in Data.HDiff.Change

Methods

konInj :: ki k -> Holes2 ki codes (K k)

varProj :: Proxy ki -> Holes2 ki codes x -> Maybe (IsI x)

TestEquality ki => TestEquality (Annotate x ki :: k -> Type)

Defined in Data.HDiff.MetaVar

Methods

testEquality :: Annotate x ki a -> Annotate x ki b -> Maybe (a :~: b)

DigestibleHO ki => DigestibleHO (MetaVarIK ki :: Atom kon -> Type)

Defined in Data.HDiff.MetaVar

Methods

digestHO :: MetaVarIK ki ki0 -> Digest

Eq (Exists (MetaVarIK ki))

Defined in Data.HDiff.MetaVar

Methods

(==) :: Exists (MetaVarIK ki) -> Exists (MetaVarIK ki) -> Bool

(/=) :: Exists (MetaVarIK ki) -> Exists (MetaVarIK ki) -> Bool

(EqHO ki, TestEquality ki) => Eq (Exists (Holes ki codes (MetaVarIK ki)))

Defined in Data.HDiff.Change.Classify

Methods

(==) :: Exists (Holes ki codes (MetaVarIK ki)) -> Exists (Holes ki codes (MetaVarIK ki)) -> Bool

(/=) :: Exists (Holes ki codes (MetaVarIK ki)) -> Exists (Holes ki codes (MetaVarIK ki)) -> Bool

Ord (Exists (MetaVarIK ki))

Defined in Data.HDiff.MetaVar

Methods

compare :: Exists (MetaVarIK ki) -> Exists (MetaVarIK ki) -> Ordering

(<) :: Exists (MetaVarIK ki) -> Exists (MetaVarIK ki) -> Bool

(<=) :: Exists (MetaVarIK ki) -> Exists (MetaVarIK ki) -> Bool

(>) :: Exists (MetaVarIK ki) -> Exists (MetaVarIK ki) -> Bool

(>=) :: Exists (MetaVarIK ki) -> Exists (MetaVarIK ki) -> Bool

max :: Exists (MetaVarIK ki) -> Exists (MetaVarIK ki) -> Exists (MetaVarIK ki)

min :: Exists (MetaVarIK ki) -> Exists (MetaVarIK ki) -> Exists (MetaVarIK ki)

(EqHO f, Eq x) => Eq (Annotate x f k2)

Defined in Data.HDiff.MetaVar

Methods

(==) :: Annotate x f k2 -> Annotate x f k2 -> Bool

(/=) :: Annotate x f k2 -> Annotate x f k2 -> Bool

(ShowHO f, Show x) => Show (Annotate x f k2)

Defined in Data.HDiff.MetaVar

Methods

showsPrec :: Int -> Annotate x f k2 -> ShowS

show :: Annotate x f k2 -> String

showList :: [Annotate x f k2] -> ShowS

type MetaVarIK ki = NA (Annotate Int ki) (Const Int)

A MetaVarIK can be over a opaque type and a recursive position

We keep the actual value of the constant around purely because sometimes we need to compare the indexes for equality. It is possible to remove that but this will require some instance like IsNat to be bubbled up all the way to generics-mrsop.

TODO: add a IsOpq instance and remove Annotate altogether. we need a method with type defOpq :: Proxy k -> ki k, we can then piggyback on testEquality for ki. The HasIKProjInj instance is part of this same hack.

metavarGet :: MetaVarIK ki at -> Int

Returns the metavariable forgetting about type information

metavarAdd :: Int -> MetaVarIK ki at -> MetaVarIK ki at

Adds a number to a metavar

Existential MetaVars

metavarIK2Int :: Exists (MetaVarIK ki) -> Int

Retrieves the int inside a existential MetaVarIK

metavarI2Int :: Exists MetaVarI -> Int

Retrieves the int inside a existential MetaVarI

metavarI2IK :: MetaVarI ix -> MetaVarIK ki ix

Injects a metavar over recursive positions into one over opaque types and recursive positions

Instances over Exists