Data.HDiff.Change.Thinning

Documentation

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

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

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)

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