Data.HDiff.Change.Apply

Defines the application function for a CChange

Generic Application

A CChange can be applied to any treefix by pattern matching over the deletion context and instantiating over the insertion context.

data ApplicationErr :: (kon -> *) -> [[[Atom kon]]] -> (Atom kon -> *) -> * where

Application might fail with some ApplicationErr describing the point of failure.

Constructors

UndefinedVar :: Int -> ApplicationErr ki codes phi

FailedContraction :: Int -> Holes ki codes phi ix -> Holes ki codes phi ix -> ApplicationErr ki codes phi

IncompatibleTypes :: ApplicationErr ki codes phi

IncompatibleOpqs :: ki k -> ki k -> ApplicationErr ki codes phi

IncompatibleHole :: Holes ki codes (MetaVarIK ki) ix -> phi ix -> ApplicationErr ki codes phi

IncompatibleTerms :: Holes ki codes (MetaVarIK ki) ix -> Holes ki codes phi ix -> ApplicationErr ki codes phi

Instances

Show (ApplicationErr ki codes phi)

Defined in Data.HDiff.Change.Apply

Methods

showsPrec :: Int -> ApplicationErr ki codes phi -> ShowS

show :: ApplicationErr ki codes phi -> String

showList :: [ApplicationErr ki codes phi] -> ShowS

type Subst ki codes phi = Map Int (Exists (Holes ki codes phi))

A instantiation substitution from metavariable numbers to some treefix

type Applicable ki codes phi = (TestEquality ki, TestEquality phi, HasIKProjInj ki phi)

genericApply :: (Applicable ki codes phi, EqHO phi, EqHO ki) => CChange ki codes at -> Holes ki codes phi at -> Either (ApplicationErr ki codes phi) (Holes ki codes phi at)

We try to unify pa and pq onto ea. The idea is that we instantiate the variables of pa with their corresponding expression on x, and substitute those in ea. Whereas if we reach a variable in x we ignore whatever was on ea and give that variable instead.

We are essentially applying

termApply :: forall ki codes at. (ShowHO ki, EqHO ki, TestEquality ki) => CChange ki codes at -> NA ki (Fix ki codes) at -> Either String (NA ki (Fix ki codes) at)

Specializes genericApply to work over terms of our language, ie, NAs

pmatch :: (Applicable ki codes phi, EqHO phi, EqHO ki) => Holes ki codes (MetaVarIK ki) ix -> Holes ki codes phi ix -> Except (ApplicationErr ki codes phi) (Subst ki codes phi)

pmatch pa x traverses pa and x instantiating the variables of pa. Upon sucessfully instantiating the variables, returns the substitution.

pmatch' :: (Applicable ki codes phi, EqHO phi, EqHO ki) => Subst ki codes phi -> Holes ki codes (MetaVarIK ki) ix -> Holes ki codes phi ix -> Except (ApplicationErr ki codes phi) (Subst ki codes phi)

idxDecEq :: forall ki codes phi at ix. (TestEquality ki, TestEquality phi, HasIKProjInj ki phi) => Holes ki codes phi at -> MetaVarIK ki ix -> Maybe (at :~: ix)

Given a MetaVarIK and a Holes, decide whether their indexes are equal.

substInsert :: (Applicable ki codes phi, EqHO ki, EqHO phi) => Subst ki codes phi -> MetaVarIK ki ix -> Holes ki codes phi ix -> Except (ApplicationErr ki codes phi) (Subst ki codes phi)

Attempts to insert a new binding into a substitution. If the variable is already bound, we check the existing binding for equality

transport :: Applicable ki codes phi => Holes ki codes (MetaVarIK ki) ix -> Subst ki codes phi -> Except (ApplicationErr ki codes phi) (Holes ki codes phi ix)

Instantiates the metavariables in the given term using the substitution in the state

lookupVar :: forall ki codes phi ix. Applicable ki codes phi => MetaVarIK ki ix -> Subst ki codes phi -> Except (ApplicationErr ki codes phi) (Maybe (Holes ki codes phi ix))

Looks for the value of a MetaVarIK ki ix in the substitution in our state. Returns Nothing when the variables is not found or throws IncompatibleTypes when the value registered in the substitution is of type iy with ix /= iy.