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

Safe HaskellSafe-Inferred

DDC.Type.Transform.Rename

Contents

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.

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.

pushBindSource

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.

substBoundSource

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.