slow-mtac

slow_mtac.v

(** * Expression trees in PHOAS *)
Require Import Coq.ZArith.ZArith.
Global Set Implicit Arguments.
Reserved Notation "'dlet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200, format "'dlet'  x .. y  :=  v  'in' '//' f").
Reserved Notation "'elet' x := v 'in' f"
         (at level 200, f at level 200, format "'elet'  x  :=  v  'in' '//' f").
Definition Let_In {A P} (v : A) (f : forall x : A, P x) : P v
  := let x := v in f x.
Notation "'dlet' x .. y := v 'in' f" := (Let_In v (fun x => .. (fun y => f) .. )).

Inductive expr {var : Type} : Type :=
| NatO : expr
| NatS : expr -> expr
| LetIn (v : expr) (f : var -> expr)
| Var (v : var)
| NatMul (x y : expr).

Bind Scope expr_scope with expr.
Delimit Scope expr_scope with expr.

Infix "*" := NatMul : expr_scope.
Notation "'elet' x := v 'in' f" := (LetIn v (fun x => f%expr)) : expr_scope.
Notation "$$ x" := (Var x) (at level 9, format "$$ x") : expr_scope.

Fixpoint denote (e : @expr nat) : nat
  := match e with
     | NatO => O
     | NatS x => S (denote x)
     | LetIn v f => dlet x := denote v in denote (f x)
     | Var v => v
     | NatMul x y => denote x * denote y
     end.

Definition Expr := forall var, @expr var.
Definition Denote (e : Expr) := denote (e _).

Require Import Mtac2.Mtac2.
Import M.notations.

Module var_context.
  Inductive var_context {var : Type} := nil | cons (n : nat) (v : var) (xs : var_context).
End var_context.

Definition find_in_ctx {var : Type} (term : nat) (ctx : @var_context.var_context var) : M (option var)
  := (mfix1 find_in_ctx (ctx : @var_context.var_context var) : M (option var) :=
        (mmatch ctx with
        | [? v xs] (var_context.cons term v xs)
          =n> M.ret (Some v)
        | [? x v xs] (var_context.cons x v xs)
          =n> find_in_ctx xs
        | _ => M.ret None
         end)) ctx.

Fixpoint string_of_pos (v : positive) : String.string
  := match v with
     | xI x => String.append (string_of_pos x) "1"
     | xO x => String.append (string_of_pos x) "0"
     | xH => "0"
     end.

Definition reify_helper {var : Type} (term : nat) (ctx : @var_context.var_context var) (var_count : positive) : M (@expr var)
  := ((mfix3 reify_helper (term : nat) (ctx : @var_context.var_context var) (var_count : positive) : M (@expr var) :=
         lvar <- find_in_ctx term ctx;
           match lvar with
           | Some v => M.ret (@Var var v)
           | None
             =>
             (mmatch term with
             | O
               =n> M.ret (@NatO var)
             | [? x] (S x)
               =n> (rx <- reify_helper x ctx var_count;
                      M.ret (@NatS var rx))
             | [? x y] (x * y)
               =n> (rx <- reify_helper x ctx var_count;
                      ry <- reify_helper y ctx var_count;
                      M.ret (@NatMul var rx ry))
             | [? v f] (@Let_In nat (fun _ => nat) v f)
               =n> (rv <- reify_helper v ctx var_count;
                      x <- M.fresh_binder_name f;
                      (*let x := String.append "reify_helper_x" (string_of_pos var_count) in*)
                      let vx := String.append "var_" x in
                      rf <- (M.nu x mNone
                                  (fun x : nat
                                   => M.nu vx mNone
                                           (fun vx : var
                                            => let fx := reduce (RedWhd [rl:RedBeta]) (f x) in
                                               rf <- reify_helper fx (var_context.cons x vx ctx) (Pos.succ var_count);
                                                 M.abs_fun vx rf)));
                      M.ret (@LetIn var rv rf))
              end)
           end) term ctx var_count).

Definition reify (var : Type) (term : nat) : M (@expr var)
  := reify_helper term var_context.nil 1.

Definition Reify (term : nat) : M Expr
  := \nu var:Type, r <- reify var term; M.abs_fun var r.


Ltac Reify' x := constr:(ltac:(mrun (@Reify x))).
Ltac Reify x := Reify' x.

Fixpoint big (a : nat) (sz : nat) : nat
  := match sz with
     | O => a
     | S sz' => dlet a' := a * a in big a' sz'
     end.

Definition big_flat_op {T} (op : T -> T -> T) (a : T) (sz : nat) : T
  := Eval cbv [Z.of_nat Pos.of_succ_nat Pos.iter_op Pos.succ] in
      match Z.of_nat sz with
      | Z0 => a
      | Zpos p => Pos.iter_op op p a
      | Zneg p => a
      end.
Definition big_flat (a : nat) (sz : nat) : nat
  := big_flat_op Nat.mul a sz.

Goal exists e, e = big 1 45.
  eexists.
  cbv [big big_flat big_flat_op].
  Time let rhs := lazymatch goal with |- _ = ?RHS => RHS end in
       let rv := Reify rhs in
       transitivity (Denote rv).