Safe Haskell	None
Language	Haskell2010

Data.HDiff.Change.Thinning

Synopsis

type ThinningErr ki codes = ApplicationErr ki codes (MetaVarIK ki)
lift' :: Monad m => m a -> StateT (Subst ki codes (MetaVarIK ki)) m a
thin :: (ShowHO ki, TestEquality ki, EqHO ki) => CChange ki codes at -> Domain ki codes at -> Either (ApplicationErr ki codes (MetaVarIK ki)) (CChange ki codes at)
tr :: (ShowHO ki, TestEquality ki, EqHO ki) => CChange ki codes at -> CChange ki codes at -> Either (ApplicationErr ki codes (Holes2 ki codes)) (CChange ki codes at)
thinUTx2 :: (ShowHO ki, TestEquality ki, EqHO ki) => Holes2 ki codes at -> Domain ki codes at -> Either (ApplicationErr ki codes (MetaVarIK ki)) (Holes2 ki codes at)
thin' :: (ShowHO ki, TestEquality ki, EqHO ki) => Holes2 ki codes at -> Holes2 ki codes at -> Either (ApplicationErr ki codes (MetaVarIK ki)) (Holes2 ki codes at)
utxThin :: (ShowHO ki, TestEquality ki, EqHO ki) => Holes ki codes (MetaVarIK ki) at -> Domain ki codes at -> StateT (Subst ki codes (MetaVarIK ki)) (Except (ThinningErr ki codes)) ()
minimize :: forall ki codes. (ShowHO ki, EqHO ki, TestEquality ki) => Subst ki codes (MetaVarIK ki) -> Except (ThinningErr ki codes) (Subst ki codes (MetaVarIK ki))
refine :: (ShowHO ki, TestEquality ki, EqHO ki) => Holes ki codes (MetaVarIK ki) ix -> Subst ki codes (MetaVarIK ki) -> Except (ThinningErr ki codes) (Holes ki codes (MetaVarIK ki) ix)

Documentation

type ThinningErr ki codes = ApplicationErr ki codes (MetaVarIK ki) Source #

lift' :: Monad m => m a -> StateT (Subst ki codes (MetaVarIK ki)) m a Source #

thin :: (ShowHO ki, TestEquality ki, EqHO ki) => CChange ki codes at -> Domain ki codes at -> Either (ApplicationErr ki codes (MetaVarIK ki)) (CChange ki codes at) Source #

tr :: (ShowHO ki, TestEquality ki, EqHO ki) => CChange ki codes at -> CChange ki codes at -> Either (ApplicationErr ki codes (Holes2 ki codes)) (CChange ki codes at) Source #

thinUTx2 :: (ShowHO ki, TestEquality ki, EqHO ki) => Holes2 ki codes at -> Domain ki codes at -> Either (ApplicationErr ki codes (MetaVarIK ki)) (Holes2 ki codes at) Source #

thin' :: (ShowHO ki, TestEquality ki, EqHO ki) => Holes2 ki codes at -> Holes2 ki codes at -> Either (ApplicationErr ki codes (MetaVarIK ki)) (Holes2 ki codes at) Source #

utxThin :: (ShowHO ki, TestEquality ki, EqHO ki) => Holes ki codes (MetaVarIK ki) at -> Domain ki codes at -> StateT (Subst ki codes (MetaVarIK ki)) (Except (ThinningErr ki codes)) () Source #

The thin' p q function is where work where we produce the map that will be applied to p in order to thin it. This function does NOT minimize this map.

minimize :: forall ki codes. (ShowHO ki, EqHO ki, TestEquality ki) => Subst ki codes (MetaVarIK ki) -> Except (ThinningErr ki codes) (Subst ki codes (MetaVarIK ki)) Source #

The minimization step performs the occurs check and removes unecessary steps. For example;

sigma = fromList
          [ (0 , bin 1 2)
          , (1 , bin 4 4) ]

Then, minimize sigma will return fromList [(0 , bin (bin 4 4) 2)]

refine :: (ShowHO ki, TestEquality ki, EqHO ki) => Holes ki codes (MetaVarIK ki) ix -> Subst ki codes (MetaVarIK ki) -> Except (ThinningErr ki codes) (Holes ki codes (MetaVarIK ki) ix) Source #

This is similar to transport, but does not throw errors on undefined variables.