ddc-core-0.4.3.1: Disciplined Disciple Compiler core language and type checker.

Safe HaskellSafe
LanguageHaskell98

DDC.Type.Transform.Rename

Contents

Description

Renaming of variable binders to anonymous form to avoid capture.

Synopsis

Documentation

class Rename c where Source #

Minimal complete definition

renameWith

Methods

renameWith :: Ord n => Sub n -> c n -> c n Source #

Rewrite names in some thing to anonymous form if they conflict with any names in the Sub state. We use this to avoid variable capture during substitution.

Instances

Rename TypeSum Source # 

Methods

renameWith :: Ord n => Sub n -> TypeSum n -> TypeSum n Source #

Rename Type Source # 

Methods

renameWith :: Ord n => Sub n -> Type n -> Type n Source #

Rename Bind Source # 

Methods

renameWith :: Ord n => Sub n -> Bind n -> Bind n Source #

Substitution states

data Sub n Source #

Substitution state. Keeps track of the binders in the environment that have been rewrittten to avoid variable capture or spec binder shadowing.

Constructors

Sub 

Fields

  • subBound :: !(Bound n)

    Bound variable that we're substituting for.

  • subShadow0 :: !Bool

    We've decended past a binder that shadows the one that we're substituting for. We're no longer substituting, but still may need to anonymise variables in types. This can only happen for level-0 named binders.

  • subConflict1 :: !(Set n)

    Level-1 names that need to be rewritten to avoid capture.

  • subConflict0 :: !(Set n)

    Level-0 names that need to be rewritten to avoid capture.

  • subStack1 :: !(BindStack n)

    Rewriting stack for level-1 names.

  • subStack0 :: !(BindStack n)

    Rewriting stack for level-0 names.

Binding stacks

data BindStack n Source #

Stack of anonymous binders that we've entered under during substitution.

Constructors

BindStack 

Fields

pushBind Source #

Arguments

:: Ord n 
=> Set n

Names that need to be rewritten.

-> BindStack n

Current bind stack.

-> Bind n

Bind to push.

-> (BindStack n, Bind n)

New stack and possibly anonymised bind.

Push a bind onto a bind stack, anonymizing it if need be to avoid variable capture.

pushBinds :: Ord n => Set n -> BindStack n -> [Bind n] -> (BindStack n, [Bind n]) Source #

Push several binds onto the bind stack, anonymyzing them if need be to avoid variable capture.

substBound Source #

Arguments

:: Ord n 
=> BindStack n

Current Bind stack during substitution.

-> Bound n

Bound we're substituting for.

-> Bound n

Bound we're looking at now.

-> Either (Bound n) Int 

Compare a Bound against the one we're substituting for.

Rewriting binding occurences

bind1 :: Ord n => Sub n -> Bind n -> (Sub n, Bind n) Source #

Push a level-1 binder on the rewrite stack.

bind1s :: Ord n => Sub n -> [Bind n] -> (Sub n, [Bind n]) Source #

Push some level-1 binders on the rewrite stack.

bind0 :: Ord n => Sub n -> Bind n -> (Sub n, Bind n) Source #

Push a level-0 binder on the rewrite stack.

bind0s :: Ord n => Sub n -> [Bind n] -> (Sub n, [Bind n]) Source #

Push some level-0 binders on the rewrite stack.

Rewriting bound occurences

use1 :: Ord n => Sub n -> Bound n -> Bound n Source #

Rewrite the use of a level-1 binder if need be.

use0 :: Ord n => Sub n -> Bound n -> Bound n Source #

Rewrite the use of a level-0 binder if need be.