stlc.v

Require Import List.
Import ListNotations.

Module member.
  Inductive t {A : Type} (x : A) : list A -> Type :=
  | Here : forall {l}, t x (x :: l)
  | There : forall {y l}, t x l -> t x (y :: l)
  .
  Arguments Here {_ _ _}.
  Arguments There {_ _ _ _} _.
End member.

Module hlist.
  Inductive t {A : Type} (B : A -> Type) : list A -> Type :=
  | nil : t B []
  | cons : forall a l, B a -> t B l -> t B (a :: l)
  .
  Arguments nil {_ _}.
  Arguments cons {_ _ _ _} _ _.

  Fixpoint get {A} {B : A -> Type} {a l} (m : member.t a l) : hlist.t B l -> B a :=
    match m in member.t _ l0
          return hlist.t B l0 -> B a
    with
    | member.Here =>
      fun h => match h with
            | nil => I
            | cons b _ => b
            end
    | member.There m' =>
      fun h => match h with
            | nil => I
            | cons _ h' => fun rec => rec h'
            end (get m')
    end.
End hlist.

Module type.
  Inductive t : Type :=
  | Bool
  | Arrow : t -> t -> t
  .

  Fixpoint denote (ty : t) : Type :=
    match ty with
    | Bool => bool
    | Arrow ty1 ty2 => denote ty1 -> denote ty2
    end.
End type.

Module expr.
  Inductive t : list type.t -> type.t -> Type :=
  | Var : forall {G ty}, member.t ty G -> t G ty

  | Lambda : forall {G ty1 ty2}, t (ty1 :: G) ty2 -> t G (type.Arrow ty1 ty2)
  | App : forall {G ty1 ty2}, t G (type.Arrow ty1 ty2) -> t G ty1 -> t G ty2

  | Const : forall {G}, bool -> t G type.Bool
  | If : forall {G ty}, t G type.Bool -> t G ty -> t G ty -> t G ty
  .

  Fixpoint denote {G ty} (e : t G ty) : hlist.t type.denote G -> type.denote ty :=
    match e with
    | Var m => hlist.get m
    | Lambda e' => fun h => fun x => denote e' (hlist.cons x h)
    | App e1 e2 => fun h => denote e1 h (denote e2 h)
    | Const b => fun _ => b
    | If e1 e2 e3 => fun h => if denote e1 h then denote e2 h else denote e3 h
    end.
End expr.

(* Reification *)

(* First, reifying types: *)

Ltac type_reify' x :=
  match x with
  | ?X -> ?Y => let rX := type_reify' X in
              let rY := type_reify' Y in
              constr:(type.Arrow rX rY)
  | bool => constr:(type.Bool)
  end.

Ltac type_reify x := let r := type_reify' x in exact r.

Check ltac:(type_reify bool).
Check ltac:(type_reify (bool -> bool -> (bool -> bool) -> bool)).

(* Reifying terms is more complex because of the presence of binders and free
   variables.

   The basic idea is explained in the last section of
   http://adam.chlipala.net/cpdt/html/Cpdt.Reflection.html .

   On a first reading, it may be best to skip the following rather detailed
   explanation and just look at the code below.

   The tactic keeps track of free variables introduced during recursion under
   binders by wrapping the term being processed with a Gallina lambda of one
   argument whose type is a big product, one for each free variable. Those
   variables are marked in the term by projecting out the corresponding
   component of the argument to the outer lambda.

   For example, suppose we want to reflect `fun (x y : bool) => x`. First, we
   wrap the whole thing in an extra lambda to represent the empty free variable
   context, resulting in `fun (p : unit) (x y : bool) => x` (we will always call
   the argument to the outer lambda `p`). Then we traverse the term. At each
   step, we peel off the outer lambda which is always there and look at what's
   inside. The first thing we see is the first inner lambda.  We add the free
   variable x to our context by adding a product to the outer lambda and
   replacing all occurences of x with `snd p`, resulting in

       fun (p : unit * bool) (y : bool) => snd p

   Then we see another inner lambda, so we also add it to the context. While
   there are no occurences of y to replace with `snd p`, we do have to adjust
   all existing refrences to `p` to account for the new free variable,
   "shifting" them up by one. This is accomplished by replacing existing
   references to `p` with `fst p`, resulting in

       fun (p : (unit * bool) * bool) => snd (fst p)

   Since the most recently introduced variable in the context comes last, the
   body of the term still refers to the first free variable, ie, what we used
   to call `x`.

   At this point, we see a variable refrence. (In general, these always marked
   by `snd` being at the head of the term.) We can read off the number of
   occurences of `fst` to count backwards in the context and find the right
   variable. So `snd p` would refer to the most recently introduced variable,
   while `snd (fst p)` refers to the second motse recently introduced variable,
   and so on. Thus this recursive call to the tactic bottoms out and returns

       expr.Var (member.There member.Here)

   The next two unwindings of the recursion just wrap a couple lambdas around
   the outside to get the final answer

       expr.Lambda (expr.Lambda (expr.Var (member.There member.Here)))

*)


(* Given a free variable marking (ie, a projection out of the free variable
   context), built an element of `member.t` that reifies it. *)
Ltac build_member P :=
  let rec go P :=
      match P with
      | fun (x : _) => x => uconstr:member.Here
      | fun (x : _) => fst (@?Q x) => let r := go Q in uconstr:(member.There r)
      end
  in go P.

Ltac reify' x :=
  let x' := eval simpl in x in
  lazymatch x' with
  | fun _ => true => uconstr:(expr.Const true)
  | fun _ => false => uconstr:(expr.Const false)

  | fun (x : ?T) => if @?B x then @?X x else @?Y x =>
    let r1 := reify' B in
    let r2 := reify' X in
    let r3 := reify' Y in
    uconstr:(expr.If r1 r2 r3)

  | fun (x : ?T) (y : ?A) => @?E x y =>
    let rA := type_reify' A in
    let r := reify' (fun (p : T * A) => E (fst p) (snd p)) in
    uconstr:(expr.Lambda (ty1 := rA) r)

  | fun (x : _) => snd (@?P x) => let m := build_member P in uconstr:(expr.Var m)

  | fun (z : ?T) => ?X ?Y =>
    (* The following lines rely on a dirty, horrible hack which dynamically
       reuses the variable name z. This is apparently legal and not a bug.
       (Section 9.2 of the Coq reference manual says:

         when a metavariable of the form ?id occurs under binders, say x1, …, xn
         and the expression matches, the metavariable is instantiated by a term
         which can then be used in any context which also binds the variables
         x1, …, xn with same types. This provides with a primitive form of
         matching under context which does not require manipulating a functional
         term.)

       Here we use it to work around the fact that it is not possible to match
       on a function application with a second-order Ltac pattern. That would
       look something like `@?X x (@?Y x)`, but it doesn't work.  *)
    let r1 := reify' (fun z : T => X) in
    let r2 := reify' (fun z : T => Y) in
    uconstr:(expr.App r1 r2)
  end.

Ltac reify x := let r := reify' (fun _ : unit => x) in exact r.

Check ltac:(reify true) : expr.t [] _ .
Check ltac:(reify false) : expr.t [] _ .

(* Here is the example from the long-winded explanation above. *)
Check ltac:(reify (fun x y : bool => x)) : expr.t [] _ .

Check ltac:(reify (fun x : bool => if x then false else true)) : expr.t [] _ .

Check ltac:(reify (fun x : bool => x)) : expr.t [] _ .
Check ltac:(reify (fun (f : bool -> bool) (x : bool) => f x)) : expr.t [] _ .
Check ltac:(reify (fun (f : (bool -> bool) -> bool) => f (fun x : bool => x))) : expr.t [] _ .