Safe Haskell	Safe-Inferred

DDC.Type.Transform.Rename

Contents

Substitution states
Binding stacks
Rewriting binding occurences
Rewriting bound occurences

Description

Renaming of variable binders to anonymous form to avoid capture.

Synopsis

Documentation

class Rename c whereSource

Methods

renameWith :: Ord n => Sub n -> c n -> c nSource

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
Rename Type
Rename Bind
Rename (Witness a)

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

stackBinds :: ![Bind n]: Holds anonymous binders that were already in the program, as well as named binders that are being rewritten to anonymous ones. In the resulting expression all these binders will be anonymous.
stackAll :: ![Bind n]: Holds all binders, independent of whether they are being rewritten or not.
stackAnons :: !Int: Number of BAnon in stackBinds.
stackNamed :: !Int: Number of BName in stackBinds.

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 nSource

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

use0 :: Ord n => Sub n -> Bound n -> Bound nSource

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