DirectReflection.v

Require Import Coq.Lists.List.

Set Implicit Arguments.

Inductive type : Set :=
| TNat : type
| TArrow : type -> type -> type.

Definition ctx := list type.

Inductive var : ctx -> type -> Set :=
| VarZ : forall t Gamma, var (t :: Gamma) t
| VarS : forall s t Gamma, var Gamma t -> var (s :: Gamma) t.

Inductive tm (Gamma : ctx) : type -> Set :=
| Lit : nat -> tm Gamma TNat
| Add : tm Gamma TNat -> tm Gamma TNat -> tm Gamma TNat
| Var : forall t, var Gamma t -> tm Gamma t
| Lam : forall s t, tm (s :: Gamma) t -> tm Gamma (TArrow s t)
| App : forall s t, tm Gamma (TArrow s t) -> tm Gamma s -> tm Gamma t.

Class Bridge (A : Type) :=
  { ty : type ;
    reflect : forall {Gamma}, A -> tm Gamma ty ;
    reify : forall {Gamma}, tm Gamma ty -> option A ;
  }.

Instance nat_Bridge : Bridge nat :=
  { ty := TNat ;
    reflect {Gamma} n := Lit Gamma n ;
    reify {Gamma} e :=
      match e with
      | Lit _ n => Some n
      | _ => None
      end ;
  }.