Require Import syntax.

Require Import List.

Fixpoint member (A : Set) (b : A) (l : list A) {struct l} : Prop :=
  match l with
  | nil => False
  | a :: m => a = b \/ member A b m
  end.


Definition VT := (vari * ty)%type.
Definition ty_env := list VT.

Definition VTT := (VT * tm)%type.
Definition OS_env := list VTT.


Definition mapsto (indx : vari) (val : ty) (l : list VT) :=
  (fix F (l0 : list VT) : Prop :=
     match l0 with
     | nil => False
     | v :: l1 => IF fst v = indx :>vari then snd v = val :>ty else F l1
     end) l.


Inductive config : Set :=
    cfg : tm -> OS_env -> config.

Definition cfgexp (c : config) := let (e, A) return tm := c in e.

Definition cfgenv (c : config) := let (e, A) return OS_env := c in A.


Definition TE_Dom (H : ty_env) :=
  (fix F (l : list VT) : list vari :=
     match l with
     | nil => nil (A:=vari)
     | v :: l0 => cons (fst v) (F l0)
     end) H.

Definition OS_Dom (A : OS_env) :=
  (fix F (l : list VTT) : list vari :=
     match l with
     | nil => nil (A:=vari)
     | v :: l0 => cons (fst (fst v)) (F l0)
     end) A.

Definition OS_Dom_ty (A : OS_env) :=
  (fix F (l : list VTT) : list VT :=
     match l with
     | nil => nil (A:=VT)
     | v :: l0 => cons (fst v) (F l0)
     end) A.