Library Binders


Representation of FGJ-omega binders using DeBruijn's indices


Require Import List.

Require Import Util.
Require Import MatchCompNat.

Require Syntax.
Module SetProgram(My_Program: Syntax.Program).

Import My_Program.




Function: lifts variable X with amplitude n at depth k
Definition lift_at_depth_in_typeVar (X: TypeVar) (n: nat) (k: nat): TypeVar :=
  (match_comp_nat2 X k TypeVar
    X
    (X + n)
  )
.

Function: lifts type construct t with amplitude n at depth k
Fixpoint lift_at_depth_in_type (t: TypeS) (n: nat) (k: nat) {struct t}: TypeS :=
  match t with
    
    | (Type_proj R i) => (Type_proj (lift_at_depth_in_type R n k) i)
    | (Type_class C) => (Type_class C)
    | (Type_fun Pi T) => (Type_fun (lift_at_depth_in_type Pi n k)
                                         (lift_at_depth_in_type T n (S k)))
    
    | (Type_apply K R) => (Type_apply (lift_at_depth_in_type K n k)
                                           (lift_at_depth_in_type R n k))
    
    | (Type_var X) => (Type_var (lift_at_depth_in_typeVar X n k))
    | (Type_tuple Ks) => (Type_tuple (lift_at_depth_in_type Ks n k))
    
    | (Type_param Pi T_opt) => (Type_param (lift_at_depth_in_type Pi n k)
                                           (lift_at_depth_in_type T_opt n (S k)))
    
    | (Type_section Ps) => (Type_section (lift_at_depth_in_type Ps n (S k)))
    
    | Type_none => Type_none
    | (Type_some T) => (Type_some (lift_at_depth_in_type T n k))
    
    | Type_nil => Type_nil
    | (Type_cons u us) => (Type_cons (lift_at_depth_in_type u n k)
                                          (lift_at_depth_in_type us n k))
end.

Function: lifts type syntax t with amplitude n
Definition lift_in_type (t: TypeS) (n: nat): TypeS :=
  (lift_at_depth_in_type t n 0).

Function: lifts type environment D with amplitude n at depth k
Fixpoint lift_at_depth_in_typeEnv (D: TypeEnv) (n: nat) (k: nat) {struct D}: TypeEnv :=
  match D with
    | nil => nil
    | (Pi :: D') => (lift_at_depth_in_type Pi n k) :: (lift_at_depth_in_typeEnv D' n (S k))
  end
.

Function: lifts type syntax t with amplitude n
Definition lift_in_typeEnv (D: TypeEnv) (n: nat): TypeEnv :=
  (lift_at_depth_in_typeEnv D n 0).




Function: drops variable X at depth k
Definition drop_at_depth_in_typeVar (X: TypeVar) (k: nat): TypeVar :=
  (match_comp_nat2 X k TypeVar
    X
    (pred X)
  )
.

Function: drops type construct t at depth k
Fixpoint drop_at_depth_in_type (t: TypeS) (k: nat) {struct t}: TypeS :=
  match t with
    
    | (Type_proj R i) => (Type_proj (drop_at_depth_in_type R k) i)
    | (Type_class C) => (Type_class C)
    | (Type_fun Pi T) => (Type_fun (drop_at_depth_in_type Pi k)
                                         (drop_at_depth_in_type T (S k)))
    
    | (Type_apply K R) => (Type_apply (drop_at_depth_in_type K k)
                                           (drop_at_depth_in_type R k))
    
    | (Type_var X) => (Type_var (drop_at_depth_in_typeVar X k))
    | (Type_tuple Ks) => (Type_tuple (drop_at_depth_in_type Ks k))
    
    | (Type_param Pi T_opt) => (Type_param (drop_at_depth_in_type Pi k)
                                           (drop_at_depth_in_type T_opt (S k)))
    
    | (Type_section Ps) => (Type_section (drop_at_depth_in_type Ps (S k)))
    
    | Type_none => Type_none
    | (Type_some T) => (Type_some (drop_at_depth_in_type T k))
    
    | Type_nil => Type_nil
    | (Type_cons u us) => (Type_cons (drop_at_depth_in_type u k)
                                          (drop_at_depth_in_type us k))
end.

Function: drops type variable X
Definition drop_in_typeVar (X: TypeVar): TypeVar :=
  (drop_at_depth_in_typeVar X 0).

Function: drops type syntax t
Definition drop_in_type (t: TypeS): TypeS :=
  (drop_at_depth_in_type t 0).

Function: drops type environment D at depth k
Fixpoint drop_at_depth_in_typeEnv (D: TypeEnv) (k: nat) {struct D}: TypeEnv :=
  match D with
    | nil => nil
    | (Pi :: D') => (drop_at_depth_in_type Pi k) :: (drop_at_depth_in_typeEnv D' (S k))
  end
.

Function: drops type syntax t
Definition drop_in_typeEnv (D: TypeEnv): TypeEnv :=
  (drop_at_depth_in_typeEnv D 0).




Function: returns the free variables of a type variable X at depth k
Definition fv_at_depth_in_typeVar (X: TypeVar) (k: nat): natSet :=
  (match_comp_nat2 X k natSet
    natSet_empty
    (natSet_add (X - k) natSet_empty)
  )
.

Function: returns the free variables of a type construct t at depth k
Fixpoint fv_at_depth_in_type (t: TypeS) (k: nat) {struct t}: natSet :=
  match t with
    
    | (Type_proj R i) => (fv_at_depth_in_type R k)
    | (Type_class C) => natSet_empty
    | (Type_fun Pi T) => (natSet_union (fv_at_depth_in_type Pi k)
                                             (fv_at_depth_in_type T (S k)))
    
    | (Type_apply K R) => (natSet_union (fv_at_depth_in_type K k)
                                             (fv_at_depth_in_type R k))
    
    | (Type_var X) => (fv_at_depth_in_typeVar X k)
    | (Type_tuple Ks) => (fv_at_depth_in_type Ks k)
    
    | (Type_param Pi T_opt) => (natSet_union (fv_at_depth_in_type Pi k)
                                             (fv_at_depth_in_type T_opt (S k)))
    
    | (Type_section Ps) => (fv_at_depth_in_type Ps (S k))
    
    | Type_none => natSet_empty
    | (Type_some T) => (fv_at_depth_in_type T k)
    
    | Type_nil => natSet_empty
    | (Type_cons u us) => (natSet_union (fv_at_depth_in_type u k)
                                             (fv_at_depth_in_type us k))
end.

Function: returns the free variables of a type construct t at depth k
Definition fv_in_type (t: TypeS): natSet :=
  (fv_at_depth_in_type t 0)
.




Function: lifts variable X with amplitude n at depth k
Definition lift_at_depth_in_var (x: Var) (k: nat) (n: nat): Var :=
  (match_comp_nat2 x k Var
    x
    (x + n)
  )
.

Function: lifts term construct t with amplitude n at depth k
Fixpoint lift_at_depth_in_term (t': Term) (k: nat) (n: nat) {struct t'}: Term :=
  match t' with
    | (Term_var i) => (Term_var (lift_at_depth_in_var i k n))
    | (Term_select t f) => (Term_select (lift_at_depth_in_term t k n) f)
    | (Term_call t m R ts) => (Term_call (lift_at_depth_in_term t k n) m R
                                             (lift_at_depth_in_term ts k n))
    | (Term_new T fts) => (Term_new T (lift_at_depth_in_term fts k n))
    | Term_nil => Term_nil
    | (Term_cons t ts) => (Term_cons (lift_at_depth_in_term t k n)
                                             (lift_at_depth_in_term ts k n))
    | FieldTerm_nil => FieldTerm_nil
    | (FieldTerm_cons f t fts) => (FieldTerm_cons f (lift_at_depth_in_term t k n)
                                                    (lift_at_depth_in_term fts k n))
  end
.

Function: lifts term syntax t with amplitude n
Definition lift_in_term (t: Term) (n: nat): Term :=
  (lift_at_depth_in_term t 0 n).

End SetProgram.