Language.IntrinsicScoping.Variables(source)

Definitions

Name : Type

  We do not really care about the notion of names used here
  as long as it has a decidable notion of equality.
  String will do for now

Totality: total
Visibility: export

IContext : Type

  A context of De Bruijn indices is right-to-left.
  Just like in typing rules, newly bound variables are added
  at the most local end with index 0, and all other variables
  see their index shifted by 1.

Totality: total
Visibility: public export

data AtIndex : Nat -> Name -> IContext -> Type

  De Bruijn indices are right-to-left, starting from 0

Totality: total
Visibility: public export
Constructors:

Z : AtIndex 0 nm (g :< nm)

S : AtIndex n nm g -> AtIndex (S n) nm (g :< {_:9456})

record Index : Name -> IContext -> Type

  An index is the pairing of its encoding as a natural number
  and the proof it is valid

Totality: total
Visibility: public export
Constructor: 

MkIndex : (getIndex : Nat) -> (0 _ : AtIndex getIndex nm ctx) -> Index nm ctx

Projections:

.getIndex : Index nm ctx -> Nat

0 .validIndex : ({rec:0} : Index nm ctx) -> AtIndex (getIndex {rec:0}) nm ctx

Hint: 

Injective weaken

.getIndex : Index nm ctx -> Nat

Totality: total
Visibility: public export

getIndex : Index nm ctx -> Nat

Totality: total
Visibility: public export

0 .validIndex : ({rec:0} : Index nm ctx) -> AtIndex (getIndex {rec:0}) nm ctx

Totality: total
Visibility: public export

0 validIndex : ({rec:0} : Index nm ctx) -> AtIndex (getIndex {rec:0}) nm ctx

Totality: total
Visibility: public export

fresh : Index nm (ctx :< nm)

Totality: total
Visibility: public export

weaken : Index nm ctx -> Index nm (ctx :< {_:9575})

Totality: total
Visibility: public export

data View : Index nm ctx -> Type

Totality: total
Visibility: public export
Constructors:

Z : View fresh

S : (p : Index nm ctx) -> View (weaken p)

view : (p : Index nm ctx) -> View p

Totality: total
Visibility: public export

isLast : Index nm ([<x] <+> g) -> Either (nm = x) (Index nm g)

Totality: total
Visibility: export

delete : Index nm g -> IContext

Totality: total
Visibility: public export

thicken : (v : Index nm g) -> (v' : Index nm' g) -> Either (nm = nm', v = v') (Index nm' (delete v))

Totality: total
Visibility: export

irrelevantAtIndex : (p : AtIndex n nm g) -> (q : AtIndex n nm' g) -> (nm = nm', p = q)

Totality: total
Visibility: export

hetEqDec : (v : Index nm g) -> (w : Index nm' g) -> Dec (nm = nm', v = w)

Totality: total
Visibility: export

LContext : Type

  A context of De Bruijn levels is left-to-right
  Newly bound variables are added at the far end, with index (length ctx).
  This has the advantage that all other variables have an unchanged level.

Totality: total
Visibility: public export

data AtLevel : Nat -> Name -> LContext -> Type

Totality: total
Visibility: public export
Constructors:

H : n = length ctx -> AtLevel n nm (nm :: ctx)

T : AtLevel n nm ctx -> AtLevel n nm ({_:10379} :: ctx)

record Level : Name -> LContext -> Type

  A level is the pairing of its encoding as a natural number
  and the proof it is valid

Totality: total
Visibility: public export
Constructor: 

MkLevel : (getLevel : Nat) -> (0 _ : AtLevel getLevel nm ctx) -> Level nm ctx

Projections:

.getLevel : Level nm ctx -> Nat

0 .validIndex : ({rec:0} : Level nm ctx) -> AtLevel (getLevel {rec:0}) nm ctx

.getLevel : Level nm ctx -> Nat

Totality: total
Visibility: public export

getLevel : Level nm ctx -> Nat

Totality: total
Visibility: public export

0 .validIndex : ({rec:0} : Level nm ctx) -> AtLevel (getLevel {rec:0}) nm ctx

Totality: total
Visibility: public export

0 validIndex : ({rec:0} : Level nm ctx) -> AtLevel (getLevel {rec:0}) nm ctx

Totality: total
Visibility: public export

weaken : Level nm ctx -> Level nm ({_:10528} :: ctx)

Totality: total
Visibility: export

fresh : Level nm (nm :: ctx)

Totality: total
Visibility: export

data View : Level nm ctx -> Type

Totality: total
Visibility: public export
Constructors:

Z : View fresh

S : (p : Level nm ctx) -> View (weaken p)

view : (p : Level nm ctx) -> View p

Totality: total
Visibility: public export

irrelevantAtLevel : (p : AtLevel n nm ctx) -> (q : AtLevel n nm' ctx) -> (nm = nm', p = q)

Totality: total
Visibility: export

hetEqDec : (v : Level nm g) -> (w : Level nm' g) -> Dec (nm = nm', v = w)

Totality: total
Visibility: export

rev : List a -> SnocList a

Totality: total
Visibility: public export

lteIsPlus : LTE m n -> Plus (minus n m) m n

Totality: total
Visibility: export

asIndex : AtLevel n nm ls -> AtIndex (minus (length ls) (S n)) nm (rev ls)

Totality: total
Visibility: export

asIndex : Level nm ls -> Index nm (rev ls)

Totality: total
Visibility: export