gistfile1.coq

Require Import List.

Section phoas.

Inductive type : Type :=
  | Tunit : type
  | Tint : option nat -> type
  | Tfunc : list type -> type -> type
.

Variable var : type -> Type.

Inductive expr' : type -> Type :=
  | Let' : forall aty bty,
           expr' aty ->
           (var aty -> expr' bty) ->
           expr' bty
  | Func' : forall argtypes restype,
            expr' restype ->
            expr' (Tfunc argtypes restype)
  | Call' : forall argtypes restype,
            expr' (Tfunc argtypes restype) ->
            expr_list' argtypes ->
            expr' restype
  | Var' : forall t, var t -> expr' t
  | Seq' : forall t, expr' Tunit -> expr' t -> expr' t
  | Prim' : forall t, prim_expr' t -> expr' t

with expr_list' : list type -> Type :=
  | Lnil' : expr_list' nil
  | Lcons' : forall t (e : expr' t) tl,
             expr_list' tl -> expr_list' (t :: tl)

with prim_expr' : type -> Type :=
  | Pint : forall (n : nat), prim_expr' (Tint None)
  | Padd : prim_expr'
             (Tfunc (Tint None :: Tint None :: nil)
             (Tint None))
.

End phoas.

Implicit Arguments Let' [var aty bty].
Implicit Arguments Func' [var argtypes restype].
Implicit Arguments Call' [var argtypes restype].
Implicit Arguments Var' [var t].
Implicit Arguments Seq' [var t].
Implicit Arguments Prim' [var t].
Implicit Arguments Lnil' [var].
Implicit Arguments Lcons' [var t tl].
Implicit Arguments Pint [var].

Definition expr t := forall var, expr' var t.
Definition expr_list t := forall var, expr_list' var t.
Definition prim_expr t := forall var, prim_expr' var t.

Definition Call
  {A R}
  (f : expr (Tfunc A R )) (a : expr_list A)
 :
  expr R
 :=
  fun _ => Call' (f _) (a _)
.


Definition Let {A B} (a : expr A) (ab : expr A -> expr B) : expr B.
unfold expr in *.
refine (fun (v : type -> Type) => @Let' v A B _ _).
exact (a v).
exact (fun _ : v A => ab a v).
Defined.
Print Let.


Definition PrimFunc
  {A R}
  (p : prim_expr (Tfunc A R))
 :
  expr (Tfunc A R)
 :=
  fun _ => Prim' (p _)
.

Definition Lcons {A B} (h : expr A) (t : expr_list B)
 : expr_list (A :: B)
 := fun _ => Lcons' (h _) (t _)
.

Definition Lnil : expr_list nil := fun _ => Lnil'.

Definition f_add_int (a b : expr (Tint None)) : expr (Tint None)
 := Call (PrimFunc Padd) (Lcons a (Lcons b Lnil))
.

Notation "x + y" := (f_add_int x y)
  (at level 50, left associativity).


Definition add_3_ints (a b c : expr (Tint None)) : expr (Tint None).
refine
  (Let (a + b) (fun ab => ab + c)).
Defined.

Definition Int (n : nat) : expr (Tint None) :=
  fun v => Prim' (Pint n).

Definition one := Int 1.
Definition two := Int 2.
Definition three := Int 3.

Section flatten.

Variable var : type -> Type.

Lemma prim_expr_conv : forall {va vb A}, prim_expr' va A -> prim_expr' vb A.
intros va vb A H.
destruct H.
(* *)
apply (Pint n).
(* *)
apply Padd.
Show Proof.
Defined.

Fixpoint flatten_expr' A (e : expr' (expr' var) A) : expr' var A
with flatten_expr_list' A (e : expr_list' (expr' var) A) : expr_list' var A
with flatten_prim_expr' A (pe : prim_expr' (expr' var) A) : prim_expr' var A
.
refine
  (match e with
   | Let' aty bty a body =>
       _ (* (flatten_expr' A a) (fun af => body _) *)
  | Func' argtypes restype body => _
  | Call' argtypes restype func args => _
  | Var' t v => _
  | Seq' t e1 e2 => _
  | Prim' t pe => _
   end
  )
.
(* *)
apply (@Let' var aty).
  exact (flatten_expr' aty a).
  exact (fun var_a => flatten_expr' _ (body ((Var' var_a)))).
(* *)
apply Func'.
  exact (flatten_expr' restype body).
(* *)
apply (Call' (argtypes := argtypes)).
  exact (flatten_expr' _ func).
  exact (flatten_expr_list' _ args).
(* *)
exact v.
(* *)
exact (Seq' (flatten_expr' _ e1) (flatten_expr' _ e2)).
(* *)
exact (Prim' (flatten_prim_expr' _ pe)).
(***)
refine
  ( (fix _self_ (L : list type) (e : expr_list' (expr' var) L) {struct e}: expr_list' var L :=
       match e with
       | Lnil' => Lnil'
       | Lcons' _ _ _ _ => Lcons' _ _
       end
    )
    A e
  ); clear e
.
(* *)
exact (flatten_expr' _ e1).
(* *)
exact (_self_ tl e2).
(***)
apply (prim_expr_conv pe).
Show Proof.
Defined.

End flatten.

Fixpoint simpl_expr' (var : type -> Type) (A : type) (e : expr' (expr' var) A) {struct e} : expr' var A :=
  (match e with
   | Let' aty bty a body => flatten_expr' var bty (body (flatten_expr' var aty a))
   | Func' argtypes restype body => flatten_expr' var _ (Func' body)
   | Call' argtypes restype func args => flatten_expr' var _ (Call' func args)
   | Var' t v => flatten_expr' var _ (Var' v)
   | Seq' t e1 e2 => flatten_expr' var _ (Seq' e1 e2)
   | Prim' t pe => flatten_expr' var _ (Prim' pe)
   end
  )
.


Definition six := add_3_ints one two three.

Definition simpl_expr A (e : expr A) : expr A :=
  fun v => simpl_expr' v A (e _).

Eval compute in six.
Eval compute in simpl_expr _ six.