Safe Haskell | None |
---|

Type checker for the Disciple Core language.

- checkExp :: (Ord n, Pretty n) => DataDefs n -> Env n -> Env n -> Exp a n -> Either (Error a n) (Exp a n, Type n, Effect n, Closure n)
- typeOfExp :: (Ord n, Pretty n) => DataDefs n -> Exp a n -> Either (Error a n) (Type n)
- type CheckM a n = CheckM (Error a n)
- checkExpM :: (Ord n, Pretty n) => DataDefs n -> Env n -> Env n -> Exp a n -> CheckM a n (Exp a n, Type n, TypeSum n, Set (TaggedClosure n))
- data TaggedClosure n
- = GBoundVal (Bound n) (TypeSum n)
- | GBoundRgnVar (Bound n)
- | GBoundRgnCon (Bound n)

# Documentation

:: (Ord n, Pretty n) | |

=> DataDefs n | Data type definitions. |

-> Env n | Kind environment. |

-> Env n | Type environment. |

-> Exp a n | Expression to check. |

-> Either (Error a n) (Exp a n, Type n, Effect n, Closure n) |

Type check an expression.

If it's good, you get a new version with types attached to all the bound variables, as well its the type, effect and closure.

If it's bad, you get a description of the error.

The returned expression has types attached to all variable occurrences,
so you can call `typeOfExp`

on any open subterm.

data TaggedClosure n Source

A closure-term tagged with the bound variable that the term is due to.

GBoundVal (Bound n) (TypeSum n) | Term due to a free value variable. |

GBoundRgnVar (Bound n) | Term due to a free region variable. |

GBoundRgnCon (Bound n) | Term due to a region handle. |

LowerT TaggedClosure | |

Eq n => Eq (TaggedClosure n) | |

(Eq (TaggedClosure n), Ord n) => Ord (TaggedClosure n) | |

Show n => Show (TaggedClosure n) | |

(Eq n, Pretty n) => Pretty (TaggedClosure n) |