Require Import Coq.ZArith.ZArith.
Require Import Coq.Lists.List.
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 "'nllet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200, format "'nllet' 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) .. )).
Definition Let_In_nat : nat -> (nat -> nat) -> nat
  := (@Let_In nat (fun _ => nat)).
Definition key : unit. exact tt. Qed.
Definition lock {A} (v : A) : A := match key with tt => v end.
Lemma unlock {A} (v : A) : lock v = v.
Proof. unfold lock; destruct key; reflexivity. Qed.
Definition LockedLet_In_nat : nat -> (nat -> nat) -> nat
  := lock Let_In_nat.
Definition locked_nat_mul := lock Nat.mul.
Notation "'nllet' x .. y := v 'in' f"
  := (LockedLet_In_nat v (fun x => .. (fun y => f) .. )).
Definition lock_Let_In_nat : @Let_In nat (fun _ => nat) = LockedLet_In_nat
  := eq_sym (unlock _).
Definition lock_Nat_mul : Nat.mul = locked_nat_mul
  := eq_sym (unlock _).

Module Import PHOAS.
  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 _).
End PHOAS.

Ltac refresh n :=
  let n' := fresh n in
  let n' := fresh n in
  n'.

Ltac Reify_of reify x :=
  constr:(fun var : Type => ltac:(let v := reify var x in exact v)).

Ltac error_cant_elim_deps f :=
  let __ := match goal with
            | _ => idtac "Failed to eliminate functional dependencies in" f
            end in
  constr:(I : I).

Ltac error_bad_function f :=
  let __ := match goal with
            | _ => idtac "Bad let-in function" f
            end in
  constr:(I : I).

Ltac error_bad_term term :=
  let __ := match goal with
            | _ => idtac "Unrecognized term:" term
            end in
  let ret := constr:(term : I) in
  constr:(I : I).

Ltac make_pre_Reify_rhs nat_of untag do_lock_letin do_lock_natmul :=
  let RHS := lazymatch goal with |- _ = ?RHS => RHS end in
  let e := fresh "e" in
  let T := fresh in
  evar (T : Type);
  evar (e : T);
  subst T;
  cut (untag (nat_of e) = RHS);
  [ subst e
  | lazymatch do_lock_letin with
    | true => rewrite ?lock_Let_In_nat
    | false => idtac
    end;
    lazymatch do_lock_natmul with
    | true => rewrite ?lock_Nat_mul
    | false => idtac
    end;
    cbv [e]; clear e ].

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.

Module CanonicalStructuresPHOAS.

  Local Notation context := (list nat).

  Structure tagged_nat (ctx : context) := tag { untag :> nat }.

  Structure reified_of (ctx : context) :=
    reify { nat_of : tagged_nat ctx ; reified_nat_of :> forall var, list var -> (forall T, T) -> @expr var }.

  Definition var_tl_tag := tag.
  Definition var_hd_tag := var_tl_tag.
  Definition S_tag := var_hd_tag.
  Definition O_tag := S_tag.
  Definition mul_tag := O_tag.

  Module Export Exports.
    Canonical Structure letin_tag ctx n := mul_tag ctx n.

    Canonical Structure reify_O ctx
      := reify (O_tag ctx 0) (fun var _ _ => @NatO var).
    Canonical Structure reify_S ctx x
      := reify (@S_tag ctx (S (@nat_of ctx x))) (fun var vs phantom => @NatS var (x var vs phantom)).
    Canonical Structure reify_mul ctx x y
      := reify (@mul_tag ctx (@nat_of ctx x * @nat_of ctx y))
               (fun var vs phantom => @NatMul var (x var vs phantom) (y var vs phantom)).
    Canonical Structure reify_var_hd n ctx
      := reify (var_hd_tag (n :: ctx) n)
               (fun var vs phantom => @Var var (List.hd (phantom _) vs)).
    Canonical Structure reify_var_tl n ctx x
      := reify (var_tl_tag (n :: ctx) (@nat_of ctx x))
               (fun var vs phantom => reified_nat_of x (List.tl vs) phantom).
    Canonical Structure reify_letin ctx v f
      := reify (letin_tag ctx (nllet x := @nat_of ctx v in @nat_of (x :: ctx) (f x)))
               (fun var vs phantom => elet x := reified_nat_of v vs phantom in reified_nat_of (f (phantom _)) (x :: vs) phantom)%expr.
  End Exports.

  Definition ReifiedNatOf (e : reified_of nil) : (forall T, T) -> Expr
    := fun phantom var => reified_nat_of e nil phantom.

  Ltac pre_Reify_rhs _ := make_pre_Reify_rhs (@nat_of nil) (@untag nil) true false.
End CanonicalStructuresPHOAS.
Export CanonicalStructuresPHOAS.Exports.

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

  Ltac reify_helper var term ctx :=
    let reify_rec term := reify_helper var term ctx in
    lazymatch ctx with
    | context[var_context.cons term ?v _]
      => constr:(@Var var v)
    | _
      =>
      lazymatch term with
      | O => constr:(@NatO var)
      | S ?x
        => let rx := reify_rec x in
           constr:(@NatS var rx)
      | ?x * ?y
        => let rx := reify_rec x in
           let ry := reify_rec y in
           constr:(@NatMul var rx ry)
      | (dlet x := ?v in ?f)
        => let rv := reify_rec v in
           let not_x := refresh x in
           let not_x2 := refresh not_x in
           let not_x3 := refresh not_x2 in
           let rf
               :=
               lazymatch
                 constr:(
                   fun (x : nat) (not_x : var)
                   => match f, @var_context.cons var x not_x ctx return @expr var with
                      | not_x2, not_x3
                        => ltac:(let fx := (eval cbv delta [not_x2] in not_x2) in
                                 let ctx := (eval cbv delta [not_x3] in not_x3) in
                                 clear not_x2 not_x3;
                                 let rf := reify_helper var fx ctx in
                                 exact rf)
                      end)
               with
               | fun _ => ?f => f
               | ?f => error_cant_elim_deps f
               end in
           constr:(@LetIn var rv rf)
      | ?v
        => error_bad_term v
      end
    end.

  Ltac reify var x :=
    reify_helper var x (@var_context.nil var).
  Ltac Reify x := Reify_of reify x.
End LtacTacInTermExplicitCtx.


Require Mtac2.Mtac2.

Module Mtac2Mmatch.
  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.

   Definition reify_helper {var : Type} (term : nat) (ctx : @var_context.var_context var) : M (@expr var)
     := ((mfix2 reify_helper (term : nat) (ctx : @var_context.var_context var) : 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;
                          M.ret (@NatS var rx))
                 | [? x y] (x * y)
                   =n> (rx <- reify_helper x ctx;
                          ry <- reify_helper y ctx;
                          M.ret (@NatMul var rx ry))
                  | [? v f] (@Let_In nat (fun _ => nat) v f)
                    =n> (rv <- reify_helper v ctx;
                        rf <- (M.nu (FreshFrom f) mNone
                                    (fun x : nat
                                     => M.nu (FreshFrom "vx") mNone
                                             (fun vx : var
                                              => let fx := reduce (RedWhd [rl:RedBeta]) (f x) in
                                                 rf <- reify_helper fx (var_context.cons x vx ctx);
                                                   M.abs_fun vx rf)));
                          M.ret (@LetIn var rv rf))
                end
             end) term ctx).

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

  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.

End Mtac2Mmatch.

Require Mtac2.DecomposeApp.
Module MTac2.
  Import Mtac2.Mtac2 Mtac2.DecomposeApp.
  Import M.notations.

  Definition mor {A} (t1 t2 : M A) : M A :=
    M.mtry' t1 (fun _ => t2).
  Notation "a '_or_' b" := (mor a b) (at level 50).

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

  Fixpoint find_in_ctx {var : Type} (term : nat) (ctx : @var_context.var_context var) {struct ctx} : M (option var)
    := match ctx with
       | var_context.cons term' v xs =>
         mmatch term' with
         | [#] term | =n> M.ret (Some v)
         | _ => M.ret None
         end
       | _ => M.ret None
       end.
  Definition reify_helper {var : Type} (term : nat) (ctx : @var_context.var_context var) : M (@expr var)
    := ((mfix2 reify_helper (term : nat) (ctx : @var_context.var_context var) : 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)
               | [#] S | x =n>
                  rx <- reify_helper x ctx;
                  M.ret (@NatS var rx)
               | [#] Nat.mul | x y =n>
                  rx <- reify_helper x ctx;
                  ry <- reify_helper y ctx;
                  M.ret (@NatMul var rx ry)
               | [#] @Let_In nat (fun _=>nat) | v f =n>
                  rv <- reify_helper v ctx;
                  rf <- (M.nu (FreshFrom f) mNone
                              (fun x : nat
                               => M.nu Generate mNone
                                       (fun vx : var
                                        => let fx := reduce (RedWhd [rl:RedBeta]) (f x) in
                                           rf <- reify_helper fx (var_context.cons x vx ctx);
                                             M.abs_fun vx rf)));
                  M.ret (@LetIn var rv rf)
               end
             end) term ctx).

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

  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.
End MTac2.