Safe Haskell | None |
---|

- data Id
- type IdMap = IntjectionMap Id
- type IdSet = IntjectionSet Id
- newIds :: IdSet -> [Id]
- module E.Type
- isWHNF :: E -> Bool
- tIntegerzh :: E
- tBits32zh :: E
- tFunc :: E -> E -> E
- tvrSilly :: TVr' E
- tBoolzh :: E
- lFalsezh :: Lit e E
- lTruezh :: Lit e E
- ePi :: TVr -> E -> E
- eLam :: TVr -> E -> E
- discardArgs :: Int -> E -> E
- tvrName :: Monad m => TVr -> m Name
- tvrShowName :: TVr -> String
- modAbsurd :: Module
- modBox :: Module
- nameConjured :: Module -> E -> Name
- fromConjured :: Monad m => Module -> Name -> m E
- isBottom :: E -> Bool
- caseBodiesMapM :: Monad m => (E -> m E) -> E -> m E
- caseBodiesMap :: (E -> E) -> E -> E
- eToList :: Monad m => E -> m [E]
- toString :: Monad m => E -> m [Char]
- ltTuple :: [E] -> E
- ltTuple' :: [E] -> E
- p_unsafeCoerce :: Prim
- p_dependingOn :: Prim
- p_toTag :: Prim
- p_fromTag :: Prim
- fromUnboxedTuple :: Monad m => E -> m [E]
- isUnboxedTuple :: E -> Bool
- module E.FreeVars

# Documentation

Eq Id | |

Ord Id | |

Show IdSet | |

Show Id | |

Binary IdSet | |

Binary Id | |

GenName Id | |

Intjection Id | |

FromAtom Id | |

FreeVars TVr IdSet | determine free variables of a binding site |

FreeVars E IdSet | |

FreeVars ARules IdSet | |

FreeVars Rule IdSet | we delete the free variables of the heads of a rule from the rule's free variables. the reason for doing this is that the rule cannot fire if all its heads are in scope, and if it were not done then many functions seem recursive when they arn't actually. |

FreeVars Comb IdSet | |

DocLike d => PPrint d Id | |

Monad m => NameMonad Id (IdNameT m) | |

FreeVars E [Id] | |

FreeVars E (IdMap (Maybe E)) | |

FreeVars E (IdMap TVr) | |

FreeVars Rule [Id] | |

FreeVars Comb [Id] | |

Show v => Show (IdMap v) | |

Binary a => Binary (IdMap a) | |

FreeVars (Alt E) IdSet | |

FreeVars (Alt E) (IdMap TVr) |

type IdMap = IntjectionMap IdSource

type IdSet = IntjectionSet IdSource

find some temporary ids that are not members of the set, useful for generating a small number of local unique names.

module E.Type

discardArgs :: Int -> E -> ESource

throw away first n EPi terms

tvrShowName :: TVr -> StringSource

nameConjured :: Module -> E -> NameSource

fromUnboxedTuple :: Monad m => E -> m [E]Source

isUnboxedTuple :: E -> BoolSource

module E.FreeVars