reification

_CoqProject

-R . ReifyByPattern
-I .
comparison.v
reify.v
reify.ml4
reify.mllib

comparison.v

Require Import Coq.ZArith.ZArith.
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 "'nlet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200, format "'nlet'  x .. y  :=  v  'in' '//' f").
Reserved Notation "'zlet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200, format "'zlet'  x .. y  :=  v  'in' '//' f").
Reserved Notation "'zxlet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200, format "'zxlet'  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").
Reserved Notation "'olet' x := v 'in' f"
         (at level 200, f at level 200, format "'olet'  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.
(*Axiom Let_In : forall {A P} (v : A) (f : forall x : A, P x), P v.*)
(*Axiom plus : Z -> Z -> Z.
Infix "+" := plus : Z_scope.*)
Local Open Scope Z_scope.
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 Let_In_Z : Z -> (Z -> Z) -> Z
  := (@Let_In Z (fun _ => Z)).
Axiom Let_In_Z_ax : Z -> (Z -> Z) -> Z.
Notation "'nlet' x .. y := v 'in' f"
  := (Let_In_nat v (fun x => .. (fun y => f) .. )).
Notation "'zlet' x .. y := v 'in' f"
  := (Let_In_Z v (fun x => .. (fun y => f) .. )).
Notation "'zxlet' x .. y := v 'in' f"
  := (Let_In_Z_ax v (fun x => .. (fun y => f) .. )).

Module Import PHOAS.
  Inductive expr {var : Type} : Type :=
  | LetIn (v : expr) (f : var -> expr)
  | Var (v : var)
  | Const (v : Z)
  | Add (x y : expr).
  Bind Scope expr_scope with expr.
  Delimit Scope expr_scope with expr.
  Infix "+" := Add : expr_scope.
  Notation "'elet' x := v 'in' f" := (LetIn v (fun x => f%expr)) : expr_scope.
  Notation "' x" := (Const x) (at level 9, format "' x") : expr_scope.
  Notation "$$ x" := (Var x) (at level 9, format "$$ x") : expr_scope.
  Fixpoint denote (e : @expr Z) : Z
    := match e with
       | LetIn v f => dlet x := denote v in denote (f x)
       | Var v => v
       | Const x => x
       | Add x y => denote x + denote y
     end.

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

  Fixpoint beq_helper (e1 e2 : @expr nat) (base : nat) : bool
    := match e1, e2 with
       | LetIn v1 f1, LetIn v2 f2
         => if beq_helper v1 v2 base
            then beq_helper (f1 base) (f2 base) (S base)
            else false
       | Var v1, Var v2 => Nat.eqb v1 v2
       | Const v1, Const v2 => Z.eqb v1 v2
       | Add x1 y1, Add x2 y2
         => andb (beq_helper x1 x2 base) (beq_helper y1 y2 base)
       | LetIn _ _, _
       | Var _, _
       | Const _, _
       | Add _ _, _
         => false
       end.
  Definition beq (e1 e2 : @expr nat) : bool := beq_helper e1 e2 O.
  Definition Beq (e1 e2 : Expr) : bool := beq (e1 _) (e2 _).
End PHOAS.

Module HOAS.
  Inductive expr : Type :=
  | LetIn (v : expr) (f : Z -> expr)
  | Const (v : Z)
  | Add (x y : expr).

  Bind Scope expr_scope with expr.
  Delimit Scope expr_scope with expr.
  Infix "+" := Add : expr_scope.
  Notation "'elet' x := v 'in' f" := (LetIn v (fun x => f%expr)) : expr_scope.
  Notation "$$ x" := (Const x) (at level 9, format "$$ x") : expr_scope.

  Fixpoint denote (e : expr) : Z
    := match e with
       | LetIn v f => dlet x := denote v in denote (f x)
       | Const x => x
       | Add x y => denote x + denote y
       end.

  Fixpoint beq_helper (e1 e2 : expr) (base : Z) : bool
    := match e1, e2 with
       | LetIn v1 f1, LetIn v2 f2
         => if beq_helper v1 v2 base
            then beq_helper (f1 base) (f2 base) (Z.pred base)
            else false
       | Const v1, Const v2 => Z.eqb v1 v2
       | Add x1 y1, Add x2 y2
         => andb (beq_helper x1 x2 base) (beq_helper y1 y2 base)
       | LetIn _ _, _
       | Const _, _
       | Add _ _, _
         => false
       end.
  Definition beq (e1 e2 : expr) : bool := beq_helper e1 e2 (-1)%Z.

  Fixpoint of_phoas (e : @PHOAS.expr Z) : expr
    := match e with
       | PHOAS.LetIn v f => LetIn (of_phoas v) (fun v => of_phoas (f v))
       | Var v => Const v
       | PHOAS.Const v => Const v
       | PHOAS.Add x y => Add (of_phoas x) (of_phoas y)
       end.
  Definition of_PHOAS (e : PHOAS.Expr) : expr := of_phoas (e Z).
End HOAS.
Fixpoint big (a : Z) (sz : nat) : Z
  := 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.iter_op Pos.of_succ_nat 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 : Z) (sz : nat) : Z
  := big_flat_op Z.add a sz.

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

  Ltac check_sane ref_PHOAS ref_HOAS :=
    lazymatch goal with
    | [ |- _ = PHOAS.Denote ?e ]
      => let val := (eval vm_compute in (PHOAS.Beq e ref_PHOAS)) in
         lazymatch val with
         | true => idtac
         | false => idtac "Error: Got" e "Expected:" ref_PHOAS; unify e ref_PHOAS
         end
    | [ |- _ = HOAS.denote ?e ]
      => let val := (eval vm_compute in (HOAS.beq e ref_HOAS)) in
         lazymatch val with
         | true => idtac
         | false => idtac "Error: Got" e "Expected:" ref_HOAS; unify e ref_HOAS
         end
    | [ |- _ = ?Denote ?e ]
      => fail 0 "Unrecognized denotation function" Denote
    end.

  Ltac do_Reify_rhs_of_cps Reify_cps _ :=
    lazymatch goal with
    | [ |- _ = ?v ]
      => idtac "actual reif"; time (Reify_cps v ltac:(fun rv => idtac));
         Reify_cps v ltac:(
           fun rv
           => idtac "actual lazy"; time (let rv := eval lazy in rv in idtac);
              let rv := (eval lazy in rv) in
              idtac "lazy beta iota"; time lazy beta iota;
              idtac "trans"; time transitivity (Denote rv))
    end.
  Ltac do_Reify_rhs_of Reify _ :=
    do_Reify_rhs_of_cps ltac:(fun v tac => let rv := Reify v in tac rv) ().
  Ltac post_Reify_rhs _ :=
    [ > | lazy [Denote denote]; reflexivity ].
  Ltac Reify_rhs_of_cps Reify_cps _ :=
    do_Reify_rhs_of_cps Reify_cps (); post_Reify_rhs ().
  Ltac Reify_rhs_of Reify _ :=
    do_Reify_rhs_of Reify (); post_Reify_rhs ().
End ReifyCommon.

Module TypeClasses.
  Local Generalizable Variables x y rx ry f rf.
  Section with_var.
    Context {var : Type}.

    Class reify_of (term : Z) (rterm : @expr var) := {}.
    Global Instance reify_Add `{reify_of x rx, reify_of y ry}
      : reify_of (x + y) (rx + ry).
    Global Instance reify_LetIn `{reify_of x rx}
           `{forall y ry, reify_of y (Var ry) -> reify_of (f y) (rf ry)}
      : reify_of (dlet y := x in f y) (elet ry := rx in rf ry).
    Global Instance reify_Const {x}
      : reify_of x (Const x) | 100.
  End with_var.
  Hint Mode reify_of - ! - : typeclass_instances.
  Hint Opaque Nat.add Z.add Let_In : typeclass_instances.

  Ltac reify var x :=
    let c := constr:(_ : @reify_of var x _) in
    lazymatch type of c with
    | reify_of _ ?rx => rx
    end.

  Ltac Reify x :=
    let c := constr:(fun var => (_ : @reify_of var x _)) in
    lazymatch type of c with
    | forall var, reify_of _ (@?rx var) => rx
    end.

  Ltac do_Reify_rhs _ := do_Reify_rhs_of Reify ().
  Ltac post_Reify_rhs _ := ReifyCommon.post_Reify_rhs ().
  Ltac Reify_rhs _ := Reify_rhs_of Reify ().
End TypeClasses.

Module Pattern.
  Ltac Reify x :=
    let rx := lazymatch (eval pattern Z, Z.add, (@Let_In Z (fun _ => Z)), Zpos, Zneg, Z0 in x) with
              | ?rx _ _ _ _ _ _ => rx
              end in
    let rx := lazymatch rx with fun N : Set => ?rx => constr:(fun N : Type => rx) end in
    let dummy := type of rx in (* propogate universe constraints, c.f., https://github.com/coq/coq/issues/5996 *)
    let rx := constr:(fun var : Type
                      => rx (@expr var) (@Add var) (fun x' f' => @LetIn var x' (fun v => f' (@Var var v))) (fun p => @Const var (Zpos p)) (fun p => @Const var (Zneg p)) (@Const var Z0)) in
    rx.
  Ltac reify var x :=
    let rx := Reify x in
    constr:(rx var).

  Ltac do_Reify_rhs _ := do_Reify_rhs_of Reify ().
  Ltac post_Reify_rhs _ := ReifyCommon.post_Reify_rhs ().
  Ltac Reify_rhs _ := Reify_rhs_of Reify ().
End Pattern.

Module LtacReifyCommon.
  (* cf COQBUG(https://github.com/coq/coq/issues/5448), COQBUG(https://github.com/coq/coq/issues/6315) *)
  Ltac refresh n :=
    let n' := fresh n in
    let n' := fresh n in
    n'.

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

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

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

    Ltac find_in_ctx var term ctx then_tac else_tac :=
      lazymatch ctx with
      | context[var_context.cons term ?v _]
        => then_tac v
      | _
        => else_tac ()
      end.

    Module TacInTerm.
      Ltac binder_recr reify_helper var ctx f then_tac :=
        lazymatch f with
        | fun x => ?f
          => 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 : Z) (not_x : var)
                     => match f, @var_context.cons var x not_x ctx return _ 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
                                   let rf := reify_helper var fx ctx in
                                   exact rf)
                        end)
                 with
                 | fun _ => ?f => f
                 | ?f => error_cant_elim_deps f
                 end in
             then_tac rf
        | ?f => error_bad_function f
        end.
    End TacInTerm.

    Module TC.
      Class reify_helper_cls (var : Type) (term : Z) (ctx : @var_context.var_context var) := do_reify_helper : @expr var.

      Ltac binder_recr reify_helper var ctx f then_tac :=
        lazymatch f with
        | fun x => ?f
          => let not_x := refresh x in
             let rf
                 :=
                 lazymatch
                   constr:(_ : forall (x : Z) (not_x : var),
                              @reify_helper_cls var f (@var_context.cons var x not_x ctx))
                 with
                 | fun _ => ?f => f
                 | ?f => error_cant_elim_deps f
                 end in
             then_tac rf
        | ?f => error_bad_function f
        end.

      Global Hint Extern 0 (@reify_helper_cls _ _ _) => progress intros : typeclass_instances.
    End TC.
  End InductiveCtx.

  Module GallinaCtx.
    Definition var_for {var : Type} (n : Z) (v : var) := False.

    Ltac find_in_ctx var term ctx then_tac else_tac :=
      lazymatch goal with
      | [ H : var_for term ?v |- _ ]
        => then_tac v
      | _
        => else_tac ()
      end.

    Module TacInTerm.
      Ltac binder_recr reify_helper var ctx f then_tac :=
        lazymatch f with
        | fun x => ?f
          => let not_x := refresh x in
             let not_x2 := refresh not_x in
             let rf
                 :=
                 lazymatch
                   constr:(
                     fun (x : Z) (not_x : var) (_ : @var_for var x not_x)
                     => match f return _ with
                        | not_x2
                          => ltac:(let fx := (eval cbv delta [not_x2] in not_x2) in
                                   let rf := reify_helper var fx () in
                                   exact rf)
                        end)
                 with
                 | fun _ v' _ => @?f v' => f
                 | ?f => error_cant_elim_deps f
                 end in
             then_tac rf
        | ?f => error_bad_function f
        end.
    End TacInTerm.

    Module TC.
      Class reify_cls (var : Type) (term : Z) := do_reify : @expr var.

      Ltac binder_recr reify_helper var ctx f then_tac :=
        lazymatch f with
        | fun x => ?f
          => let not_x := refresh x in
             let not_x2 := refresh not_x in
             let rf
                 :=
                 lazymatch
                   constr:(_ : forall (x : Z) (not_x : var) (_ : @var_for var x not_x),
                              @reify_cls var f)
                 with
                 | fun _ v' _ => @?f v' => f
                 | ?f => error_cant_elim_deps f
                 end in
             then_tac rf
        | ?f => error_bad_function f
        end.

      Global Hint Extern 0 (@reify_cls _ _) => progress intros : typeclass_instances.
    End TC.
  End GallinaCtx.

  Ltac reify_helper_of find_in_ctx binder_recr var term ctx :=
    let reify_helper var term ctx := reify_helper_of find_in_ctx binder_recr var term ctx in
    let reify_rec term := reify_helper var term ctx in
    find_in_ctx
      var term ctx
      ltac:(fun v => constr:(@Var var v))
             ltac:(
      fun _
      =>
        lazymatch term with
        | ?x + ?y
          => let rx := reify_rec x in
             let ry := reify_rec y in
             constr:(@Add var rx ry)
        | (dlet x := ?v in @?f x)
          => let rv := reify_rec v in
             binder_recr
               reify_helper var ctx f
               ltac:(fun rf => constr:(@LetIn var rv rf))
        | ?v
          => constr:(@Const var v)
        end).

  Ltac reify_of find_in_ctx binder_recr var term
    := reify_helper_of find_in_ctx binder_recr var term (@InductiveCtx.var_context.nil var).
End LtacReifyCommon.

Module LtacTacInTermInductiveCtx.
  Import LtacReifyCommon.
  Import InductiveCtx.
  Import TacInTerm.

  Ltac reify var term := reify_of find_in_ctx binder_recr var term.
  Ltac Reify x := Reify_of reify x.
  Ltac do_Reify_rhs _ := do_Reify_rhs_of Reify ().
  Ltac post_Reify_rhs _ := ReifyCommon.post_Reify_rhs ().
  Ltac Reify_rhs _ := Reify_rhs_of Reify ().
End LtacTacInTermInductiveCtx.

Module LtacTacInTermGallinaCtx.
  Import LtacReifyCommon.
  Import GallinaCtx.
  Import TacInTerm.

  Ltac reify var term := reify_of find_in_ctx binder_recr var term.
  Ltac Reify x := Reify_of reify x.
  Ltac do_Reify_rhs _ := do_Reify_rhs_of Reify ().
  Ltac post_Reify_rhs _ := ReifyCommon.post_Reify_rhs ().
  Ltac Reify_rhs _ := Reify_rhs_of Reify ().
End LtacTacInTermGallinaCtx.

Module LtacTCInductiveCtx.
  Import LtacReifyCommon.
  Import InductiveCtx.
  Export TC.

  Ltac reify_helper var term ctx := reify_helper_of find_in_ctx binder_recr var term ctx.
  Ltac reify var term := reify_of find_in_ctx binder_recr var term.
  Ltac Reify x := Reify_of reify x.
  Ltac do_Reify_rhs _ := do_Reify_rhs_of Reify ().
  Ltac post_Reify_rhs _ := ReifyCommon.post_Reify_rhs ().
  Ltac Reify_rhs _ := Reify_rhs_of Reify ().

  Global Hint Extern 0 (@reify_helper_cls ?var ?term ?ctx)
  => (let res := reify_helper var term ctx in exact res) : typeclass_instances.
End LtacTCInductiveCtx.

Module LtacTCGallinaCtx.
  Import LtacReifyCommon.
  Import GallinaCtx.
  Export TC.

  Ltac reify_helper var term := reify_helper_of find_in_ctx binder_recr var term ().
  Ltac reify var term := reify_of find_in_ctx binder_recr var term.
  Ltac Reify x := Reify_of reify x.
  Ltac do_Reify_rhs _ := do_Reify_rhs_of Reify ().
  Ltac post_Reify_rhs _ := ReifyCommon.post_Reify_rhs ().
  Ltac Reify_rhs _ := Reify_rhs_of Reify ().

  Global Hint Extern 0 (@reify_cls ?var ?term)
  => (let res := reify_helper var term in exact res) : typeclass_instances.
End LtacTCGallinaCtx.

Module LtacPrimUncurry.
  Module Import prim.
    Set Primitive Projections.
    Record prod A B := pair { fst : A ; snd : B }.
    Add Printing Let prod.

    Notation "x * y" := (prod x y) : type_scope.
    Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.

    Arguments pair {A B} _ _.
    Arguments fst {A B} _.
    Arguments snd {A B} _.
  End prim.

  (* cf COQBUG(https://github.com/coq/coq/issues/5448), COQBUG(https://github.com/coq/coq/issues/6315) *)
  Ltac refresh n :=
    let n' := fresh n in
    let n' := fresh n in
    n'.

  Axiom bad : nat.

  Ltac reify var term :=
    let reify_rec term := reify var term in
    lazymatch term with
    | fun args : ?T => @?x args + @?y args
      => let rx := reify_rec x in
         let ry := reify_rec y in
         constr:(fun args : T => @Add var (rx args) (ry args))
    | (fun args : ?T => dlet x := @?v args in ?f)
      => let rv := reify_rec v in
         let args2 := refresh args in
         let rf := reify_rec (fun args2 : (nat * var) * T
                              => match snd args2, fst (fst args2) with
                                 | args, x => f
                                 end) in
         constr:(fun args : T => @LetIn var (rv args) (fun x => rf ((bad, x), args)))
    | (fun args : ?T => fst (fst ?args'))
      => constr:(fun args : T => @Var var (snd (fst args)))
    | (fun args : ?T => ?v)
      => constr:(fun args : T => @Const var v)
    | ?v
      => let rv := reify_rec (fun dummy : unit => v) in
         (eval cbv [fst snd] in (rv tt))
    end.

  Ltac Reify x := Reify_of reify x.
  Ltac do_Reify_rhs _ := do_Reify_rhs_of Reify ().
  Ltac post_Reify_rhs _ := ReifyCommon.post_Reify_rhs ().
  Ltac Reify_rhs _ := Reify_rhs_of Reify ().
End LtacPrimUncurry.

Require Ltac2.Ltac2.
Module Ltac2Common.
  Import Ltac2.Init.
  Import Ltac2.Notations.

  Module List.
    Ltac2 rec map f ls :=
      match ls with
      | [] => []
      | l :: ls => f l :: map f ls
      end.
  End List.
  Module Ident.
    Ltac2 rec find_error id xs :=
      match xs with
      | [] => None
      | x :: xs
        => let ((id', val)) := x in
           match Ident.equal id id' with
           | true => Some val
           | false => find_error id xs
           end
      end.
    Ltac2 find id xs :=
      match find_error id xs with
      | None => Control.zero Not_found
      | Some val => val
      end.
  End Ident.
  Module Array.
    Ltac2 rec to_list_aux (ls : 'a array) (start : int) :=
      match Int.equal (Int.compare start (Array.length ls)) -1 with
      | true => Array.get ls start :: to_list_aux ls (Int.add start 1)
      | false => []
      end.
    Ltac2 to_list (ls : 'a array) := to_list_aux ls 0.
  End Array.
  Module Constr.
    Ltac2 rec strip_casts term :=
      match Constr.Unsafe.kind term with
      | Constr.Unsafe.Cast term' _ _ => strip_casts term'
      | _ => term
      end.
    Module Unsafe.
      Ltac2 beta1 (c : constr) :=
        match Constr.Unsafe.kind c with
        | Constr.Unsafe.App f args
          => match Constr.Unsafe.kind f with
             | Constr.Unsafe.Lambda id ty f
               => Constr.Unsafe.substnl (Array.to_list args) 0 f
             | _ => c
             end
        | _ => c
        end.
      Ltac2 zeta1 (c : constr) :=
        match Constr.Unsafe.kind c with
        | Constr.Unsafe.LetIn id v ty f
          => Constr.Unsafe.substnl [v] 0 f
        | _ => c
        end.
    End Unsafe.
  End Constr.
  Module Ltac1.
    Class Ltac1Result {T} (v : T) := {}.
    Class Ltac1Results {T} (v : list T) := {}.
    Class Ltac2Result {T} (v : T) := {}.
    Ltac save_ltac1_result v :=
      match goal with
      | _ => assert (Ltac1Result v) by constructor
      end.
    Ltac clear_ltac1_results _ :=
      match goal with
      | _ => repeat match goal with
                    | [ H : Ltac1Result _ |- _ ] => clear H
                    end
      end.
    Ltac2 get_ltac1_result () :=
      (lazy_match! goal with
       | [ id : Ltac1Result ?v |- _ ]
        => Std.clear [id]; v
       end).

    Ltac save_ltac1_results v :=
      match goal with
      | _ => assert (Ltac1Result v) by constructor
      end.
    Ltac2 save_ltac2_result v :=
      Std.cut '(Ltac2Result $v);
        Control.dispatch
          [(fun ()
            => Std.intros false [Std.IntroNaming (Std.IntroFresh @res)])
           ;
           (fun () => Notations.constructor)].
    Ltac get_ltac2_result _ :=
      lazymatch goal with
      | [ res : Ltac2Result ?v |- _ ]
        => let dummy := match goal with
                        | _ => clear res
                        end in
           v
      end.
    Ltac2 from_ltac1 (save_args : constr) (tac : unit -> unit) :=
      let beta_flag :=
          {
            Std.rBeta := true; Std.rMatch := false; Std.rFix := false; Std.rCofix := false;
            Std.rZeta := false; Std.rDelta := false; Std.rConst := [];
          } in
      let c := '(ltac2:(save_ltac2_result save_args;
                          tac ();
                          let v := get_ltac1_result () in
                          Control.refine (fun () => v))) in
      Constr.Unsafe.zeta1 (Constr.Unsafe.zeta1 (Std.eval_cbv beta_flag c)).
    End Ltac1.
End Ltac2Common.

Module Ltac2.
  Import Ltac2Common.
  Import Ltac2.Init.
  Import Ltac2.Notations.

  Ltac2 rec reify_helper
        (var : constr)
        (term : constr)
        (ctx : (ident * ident) list)
    :=
      let reify_rec term := reify_helper var term ctx in
      Control.plus
        (fun ()
         => match Constr.Unsafe.kind (Constr.strip_casts term) with
            | Constr.Unsafe.Var x
              => let v := Ident.find x ctx in
                 let v := Constr.Unsafe.make (Constr.Unsafe.Var v) in
                 constr:(@Var $var $v)
            | _ => Control.zero Not_found
            end)
        (fun _
         => (lazy_match! term with
            | ?x + ?y
              => let rx := reify_rec x in
                 let ry := reify_rec y in
                 constr:(@Add $var $rx $ry)
            | (dlet x : ?t := ?v in @?f x)
              => let rv := reify_rec v in
                 (** We assume the invariant that all bound variables
                     show up as Rel nodes rather than Var nodes *)
                 match Constr.Unsafe.kind f with
                 | Constr.Unsafe.Lambda id t c
                   => let c_set := Fresh.Free.of_ids (List.map (fun (id, _, _) => id) (Control.hyps ())) in
                      let c_set := Fresh.Free.union c_set (Fresh.Free.of_constr c) in
                      let x_base := match id with
                                    | Some id => id
                                    | None => @x
                                    end in
                      let x := Fresh.fresh c_set x_base in
                      let c_set := Fresh.Free.union
                                     c_set
                                     (Fresh.Free.of_ids [x]) in
                      let not_x := Fresh.fresh c_set x_base in
                      let ctx := (x, not_x) :: ctx in
                      let c := Constr.Unsafe.substnl [Constr.Unsafe.make (Constr.Unsafe.Var x)] 0 c in
                      let ret :=
                          Constr.in_context
                            x t
                            (fun ()
                             => let rf :=
                                    Constr.in_context
                                      not_x var
                                      (fun ()
                                       => let rf := reify_helper var c ctx in
                                          Control.refine (fun () => rf)) in
                                Control.refine (fun () => rf)) in
                      (lazy_match! ret with
                      | fun _ => ?rf
                        => constr:(@LetIn $var $rv $rf)
                      | ?f
                        => let msg :=
                               Message.concat (Message.of_string "Failed to eliminate functional dependencies in ")
                                              (Message.of_constr f) in
                           Message.print msg;
                             Control.zero (Tactic_failure (Some msg))
                       end)
                 | _ => let msg :=
                               Message.concat (Message.of_string "Bad let-in function: ")
                                              (Message.of_constr f) in
                         Message.print msg;
                           Control.zero (Tactic_failure (Some msg))
                 end
            | ?v
              => constr:(@Const $var $v)
             end)).

  Ltac2 reify (var : constr) (term : constr) := reify_helper var term [].

  Ltac reify var term :=
    let dummy := Ltac1.save_ltac1_result (var, term) in
    let ret :=
        constr:(ltac2:(let args := Ltac1.get_ltac1_result () in
                       (lazy_match! args with
                       | (?var, ?term)
                         => let rv := reify var term in
                            Control.refine (fun () => rv)
                       | _ => Control.throw Not_found
                        end))) in
    let dummy := Ltac1.clear_ltac1_results () in
    ret.

  Ltac Reify x := Reify_of reify x.
  Ltac do_Reify_rhs _ := do_Reify_rhs_of Reify ().
  Ltac post_Reify_rhs _ := ReifyCommon.post_Reify_rhs ().
  Ltac Reify_rhs _ := Reify_rhs_of Reify ().
End Ltac2.

Module Ltac2Unsafe.
  Import Ltac2Common.
  Import Ltac2.Init.
  Import Ltac2.Notations.

  Ltac2 rec unsafe_reify_helper
        (mkVar : constr -> 'a)
        (mkConst : constr -> 'a)
        (zAdd : constr)
        (mkAdd : 'a -> 'a -> 'a)
        (idLetIn : constr)
        (mkLetIn : 'a -> ident option -> constr -> 'a -> 'a)
        (term : constr)
    :=
      let reify_rec term := unsafe_reify_helper mkVar mkConst zAdd mkAdd idLetIn mkLetIn term in
      let kterm := Constr.Unsafe.kind term in
      match kterm with
      | Constr.Unsafe.Rel _ => mkVar term
      | Constr.Unsafe.Var _ => mkVar term
      | Constr.Unsafe.Cast term _ _ => reify_rec term
      | Constr.Unsafe.App f args
        =>
        match Constr.equal f zAdd with
        | true
          => let x := Array.get args 0 in
             let y := Array.get args 1 in
             let rx := reify_rec x in
             let ry := reify_rec y in
             mkAdd rx ry
        | false
          =>
          match Constr.equal f idLetIn with
          | true
            => let x := Array.get args 2 (* assume the first two args are type params *) in
               let f := Array.get args 3 in
               match Constr.Unsafe.kind f with
               | Constr.Unsafe.Lambda idx ty body
                 => let rx := reify_rec x in
                    let rf := reify_rec body in
                    mkLetIn rx idx ty rf
               | _ => mkConst term
               end
          | false
            => mkConst term
          end
        end
      | _
        => mkConst term
      end.

  Ltac2 unsafe_reify (var : constr) (term : constr) :=
    let cVar := '@Var in
    let cConst := '@Const in
    let cAdd := '@Add in
    let cLetIn := '@LetIn in
    let cZAdd := '@Z.add in
    let cLet_In := '@Let_In in
    let mk1VarArgs (x : constr) :=
        let args := Array.make 2 var in
        let () := Array.set args 1 x in
        args in
    let mk2VarArgs (x : constr) (y : constr) :=
        let args := Array.make 3 var in
        let () := Array.set args 1 x in
        let () := Array.set args 2 y in
        args in
    let mkApp1 (f : constr) (x : constr) :=
        Constr.Unsafe.make (Constr.Unsafe.App f (mk1VarArgs x)) in
    let mkApp2 (f : constr) (x : constr) (y : constr) :=
        Constr.Unsafe.make (Constr.Unsafe.App f (mk2VarArgs x y)) in
    let mkVar (v : constr) := mkApp1 cVar v in
    let mkConst (v : constr) := mkApp1 cConst v in
    let mkAdd (x : constr) (y : constr) := mkApp2 cAdd x y in
    let mkcLetIn (x : constr) (y : constr) := mkApp2 cLetIn x y in
    let mkLetIn (x : constr) (idx : ident option) (ty : constr) (fbody : constr)
        := mkcLetIn x (Constr.Unsafe.make (Constr.Unsafe.Lambda idx var fbody)) in
    let ret := unsafe_reify_helper mkVar mkConst cZAdd mkAdd cLet_In mkLetIn term in
    ret.
  Ltac2 check_result (ret : constr) :=
    match Constr.Unsafe.check ret with
    | Val rterm => rterm
    | Err exn => Control.zero exn
    end.
  Ltac2 reify (var : constr) (term : constr) :=
    check_result (unsafe_reify var term).

  Ltac2 unsafe_Reify (term : constr) :=
    let fresh_set := Fresh.Free.of_constr term in
    let idvar := Fresh.fresh fresh_set @var in
    let var := Constr.Unsafe.make (Constr.Unsafe.Var idvar) in
    let rterm := unsafe_reify var term in
    let rterm := Constr.Unsafe.closenl [idvar] 1 rterm in
    Constr.Unsafe.make (Constr.Unsafe.Lambda (Some idvar) 'Type rterm).

  Ltac2 do_Reify (term : constr) :=
    check_result (unsafe_Reify term).

  Ltac2 unsafe_mkApp1 (f : constr) (x : constr) :=
    let args := Array.make 1 x in
    Constr.Unsafe.make (Constr.Unsafe.App f args).
  Ltac2 mkApp1 (f : constr) (x : constr) :=
    check_result (unsafe_mkApp1 f x).

  Ltac2 all_flags :=
    {
      Std.rBeta := true; Std.rMatch := true; Std.rFix := true; Std.rCofix := true;
      Std.rZeta := true; Std.rDelta := true; Std.rConst := [];
    }.
  Ltac2 betaiota_flags :=
    {
      Std.rBeta := true; Std.rMatch := true; Std.rFix := true; Std.rCofix := true;
      Std.rZeta := false; Std.rDelta := false; Std.rConst := [];
    }.
  Ltac2 in_goal :=
    { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences }.

  Ltac2 do_Reify_rhs_fast () :=
    let g := Control.goal () in
    match Constr.Unsafe.kind g with
    | Constr.Unsafe.App f args (* App eq [ty; lhs; rhs] *)
      => let v := Array.get args 2 in
         let rv := Control.time (Some "Actual reif") (fun _ => unsafe_Reify v) in
         let rv := Control.time (Some "Actual lazy") (fun _ => Std.eval_lazy all_flags rv) in
         Control.time (Some "lazy beta iota") (fun _ => Std.lazy betaiota_flags in_goal);
         Control.time (Some "trans") (fun _ => Std.transitivity (unsafe_mkApp1 'Denote rv))
    | _
      => Control.zero (Tactic_failure (Some (Message.concat (Message.of_string "Invalid goal in Ltac2Unsafe.do_Reify_rhs_fast: ") (Message.of_constr g))))
    end.

  Ltac2 do_Reify_rhs () :=
    lazy_match! goal with
    | [ |- _ = ?v ]
      => let rv := do_Reify v in
         let rv := Std.eval_lazy all_flags rv in
         Std.transitivity (mkApp1 'Denote rv)
    | [ |- ?g ] => Control.zero (Tactic_failure (Some (Message.concat (Message.of_string "Invalid goal in Ltac2Unsafe.do_Reify_rhs: ") (Message.of_constr g))))
    end.

  Ltac reify var term :=
    let dummy := Ltac1.save_ltac1_result (var, term) in
    let ret :=
        constr:(ltac2:(let args := Ltac1.get_ltac1_result () in
                       (lazy_match! args with
                       | (?var, ?term)
                         => let rv := reify var term in
                            Control.refine (fun () => rv)
                       | _ => Control.throw Not_found
                        end))) in
    let dummy := Ltac1.clear_ltac1_results () in
    ret.

  Ltac Reify x := Reify_of reify x.
  (*Ltac do_Reify_rhs _ := do_Reify_rhs_of Reify ().*)
  Ltac do_Reify_rhs _ := ltac2:(do_Reify_rhs_fast ()).
  Ltac post_Reify_rhs _ := ReifyCommon.post_Reify_rhs ().
  Ltac Reify_rhs _ := Reify_rhs_of Reify ().
End Ltac2Unsafe.

Module CanonicalStructuresReifyCommon.
  Ltac make_pre_Reify_rhs Z_of untag Let_In_Z :=
    let RHS := lazymatch goal with |- _ = ?RHS => RHS end in
    let RHS := lazymatch (eval pattern (@Let_In Z (fun _ => Z)) in RHS) with ?RHS _ => RHS end in
    let e := fresh "e" in
    let T := fresh in
    evar (T : Type);
    evar (e : T);
    subst T;
    cut (untag (Z_of e) = RHS Let_In_Z);
    [ subst e
    | cbv [e]; clear e ].
  Ltac do_Reify_rhs _ :=
    [ > .. | refine eq_refl ].
  Ltac make_post_Reify_rhs denote reified_Z_of :=
    [ > lazymatch goal with
        | [ |- ?untag (?Z_of ?e) = _ -> _ ]
          => let e' := (eval lazy in (reified_Z_of e)) in
             intros _;
             transitivity (denote e');
             [ | lazy [HOAS.denote PHOAS.Denote PHOAS.denote]; reflexivity ]
        end ].
End CanonicalStructuresReifyCommon.

Module CanonicalStructuresFlatHOAS.
  Import CanonicalStructuresReifyCommon.
  Import HOAS.
  (* structure for packaging a Z expr and its reification *)

  Structure tagged_Z := tag { untag :> Z }.
  Structure reified_of :=
    reify { Z_of : tagged_Z ; reified_Z_of :> expr }.
  (* tags to control the order of application *)
  Definition const_tag := tag.
  Module Export Exports.
    Canonical Structure add_tag n := const_tag n.
    Canonical Structure reify_const n
      := reify (const_tag n) (Const n).
    Canonical Structure reify_add x y
      := reify (add_tag (Z_of x + Z_of y))
               (@Add x y).
  End Exports.
  Ltac pre_Reify_rhs _ := make_pre_Reify_rhs Z_of untag Let_In_Z.
  Ltac do_Reify_rhs _ := CanonicalStructuresReifyCommon.do_Reify_rhs ().
  Ltac post_Reify_rhs _ := make_post_Reify_rhs denote reified_Z_of.
  Ltac Reify_rhs _ := pre_Reify_rhs (); do_Reify_rhs (); post_Reify_rhs ().
End CanonicalStructuresFlatHOAS.

Module CanonicalStructuresFlatPHOAS.
  Import CanonicalStructuresReifyCommon.
  Import PHOAS.
  (* structure for packaging a Z expr and its reification *)

  Structure tagged_Z := tag { untag :> Z }.
  Structure reified_of :=
    reify { Z_of : tagged_Z ; reified_Z_of :> Expr }.
  (* tags to control the order of application *)
  Definition const_tag := tag.
  Module Export Exports.
    Canonical Structure add_tag n := const_tag n.
    Canonical Structure reify_const n
      := reify (const_tag n) (fun var => @Const var n).
    Canonical Structure reify_add x y
      := reify (add_tag (Z_of x + Z_of y))
               (fun var => @Add var (reified_Z_of x var) (reified_Z_of y var)).
  End Exports.
  Ltac pre_Reify_rhs _ := make_pre_Reify_rhs Z_of untag Let_In_Z.
  Ltac do_Reify_rhs _ := CanonicalStructuresReifyCommon.do_Reify_rhs ().
  Ltac post_Reify_rhs _ := make_post_Reify_rhs Denote reified_Z_of.
  Ltac Reify_rhs _ := pre_Reify_rhs (); do_Reify_rhs (); post_Reify_rhs ().
End CanonicalStructuresFlatPHOAS.

Module CanonicalStructuresHOAS.
  Import CanonicalStructuresReifyCommon.
  Import HOAS.
  (* structure for packaging a Z expr and its reification *)

  Structure tagged_Z := tag { untag :> Z }.
  Structure reified_of :=
    reify { Z_of : tagged_Z ; reified_Z_of :> expr }.
  (* tags to control the order of application *)
  Definition const_tag := tag.
  Definition let_in_tag := const_tag.
  Module Export Exports.
    Canonical Structure add_tag n := let_in_tag n.
    Canonical Structure reify_const n
      := reify (const_tag n) (Const n).
    Canonical Structure reify_add x y
      := reify (add_tag (Z_of x + Z_of y))
               (@Add x y).
    Canonical Structure reify_let_in v f
      := reify (let_in_tag (zxlet x := untag (Z_of v) in Z_of (f x)))
               (elet x := reified_Z_of v in reified_Z_of (f x)).
  End Exports.
  Ltac pre_Reify_rhs _ := make_pre_Reify_rhs Z_of untag Let_In_Z_ax.
  Ltac do_Reify_rhs _ := CanonicalStructuresReifyCommon.do_Reify_rhs ().
  Ltac post_Reify_rhs _ := make_post_Reify_rhs denote reified_Z_of.
  Ltac Reify_rhs _ := pre_Reify_rhs (); do_Reify_rhs (); post_Reify_rhs ().
End CanonicalStructuresHOAS.

(*
Require Template.Ast.
Require Template.Template.
Module TemplateCoq.
  Import PHOAS.
  Import Template.Ast.
  Import Template.Template.
  Module Compile.
    Import Coq.Strings.String.
    Scheme Equality for string.

    Section with_var.
      Context {var : Type}.
      Axiom bad : var.
      Fixpoint compile_positive (e : term) : option positive
        := match e with
           | tApp (tConstruct (mkInd Bp 0) 0) (v :: nil)
             => option_map xI (compile_positive v)
           | tApp (tConstruct (mkInd Bp 0) 1) (v :: nil)
             => option_map xO (compile_positive v)
           | tConstruct (mkInd Bp 0) 2
             => Some xH
           | _ => None
           end.
      Definition compile_Z (e : term) : option Z
        := match e with
           | tConstruct (mkInd BZ 0) 0
             => Some Z0
           | tApp (tConstruct (mkInd BZ 0) 1) (p :: nil)
             => option_map Zpos (compile_positive p)
           | tApp (tConstruct (mkInd BZ 0) 2) (p :: nil)
             => option_map Zneg (compile_positive p)
           | _ => None
           end.
      Fixpoint compile (e : term) (ctx : list var) : @expr var
        := match e with
           | tRel idx => Var (List.nth_default bad ctx idx)
           | tCast e _ _
             => compile e ctx
           | tApp f4 (_ :: _ :: x :: tLambda _ _ f :: nil)
             => @LetIn var (compile x ctx)
                       (fun x' => compile f (x' :: ctx))
           | tApp f2 (x :: y :: nil)
             => @Add var (compile x ctx) (compile y ctx)
           | tApp _ _ as e
             => match compile_Z e with
                | Some v => @Const var v
                | None => Var bad
                end
           | _
             => Var bad
           end%list.
    End with_var.
    Definition Compile (e : term) : Expr := fun var => @compile var e nil.
  End Compile.

  Ltac reify_cps var term tac :=
    quote_term term (fun v => tac (@Compile.compile var v)).

  Ltac Reify_cps term tac :=
    quote_term term (fun v => tac (Compile.Compile v)).

  Ltac do_Reify_rhs _ := do_Reify_rhs_of_cps Reify_cps ().
  Ltac post_Reify_rhs _ := ReifyCommon.post_Reify_rhs ().
  Ltac Reify_rhs _ := Reify_rhs_of_cps Reify_cps ().
End TemplateCoq.
 *)

Require reify.
Module OCaml.
  Import PHOAS.
  Import reify.

  Ltac Reify_cps term tac :=
    quote_term_cps
      (@Var) (@Const) (@Add) (@LetIn) (@Z.add) (@Let_In)
      var Type term tac.

  Ltac reify_cps var term tac :=
    Reify_cps term ltac:(fun rt => tac (rt var)).

  Ltac do_Reify_rhs _ := do_Reify_rhs_of_cps Reify_cps ().
  Ltac post_Reify_rhs _ := ReifyCommon.post_Reify_rhs ().
  Ltac Reify_rhs _ := Reify_rhs_of_cps Reify_cps ().
End OCaml.

Ltac make_ref do_eval_cbv big ns :=
  let rv :=
      (eval cbv beta in
          (fun var : Type
           => ltac:(let v := do_eval_cbv
                               (List.map (fun n => (n, big n)) ns) in
                    let rv := Pattern.reify var v in
                    exact rv))) in
  let rv :=
      lazymatch rv with
      | (fun var => List.map (fun n => (n, @?rx n var)) ns)
        => constr:(List.map (fun n => dlet rx' := rx n in (n, rx', HOAS.of_PHOAS rx')) ns)
      end in
  let rv := (eval cbv beta in rv) in
  exact rv.

Definition big_refs (ns : list nat) : list (nat * PHOAS.Expr * HOAS.expr).
Proof. make_ref ltac:(fun v => eval lazy delta [big] in v) (big 1) ns. Defined.
Definition big_flat_refs (ns : list nat) : list (nat * PHOAS.Expr * HOAS.expr).
Proof. make_ref ltac:(fun v => eval lazy [big_flat] in v) (big_flat 1) ns. Defined.

Ltac do_test_with big do_cbv pre_reify do_reify post_reify n ref_PHOAS ref_HOAS :=
  let H := fresh in
  assert (H : exists v, v = big 1 n);
  [ eexists;
    once (do_cbv n);
    once (pre_reify n);
    once (do_reify n);
    once (post_reify n);
    check_sane ref_PHOAS ref_HOAS;
    reflexivity
  | clear H ].

Tactic Notation "do_test_with" string(name) constr(big) tactic3(do_cbv) tactic3(pre_reify) tactic3(do_reify) tactic3(post_reify) constr(n) constr(ref_PHOAS) constr(ref_HOAS) :=
  idtac "Starting test (n=" n ") for" name;
  time once (
  do_test_with
    big
    ltac:(fun n' => idtac "Doing cbv  (n=" n ") for" name "with" big ":"; time do_cbv)
    ltac:(fun n' => idtac "Doing pre  (n=" n ") for" name "with" big ":"; time pre_reify ())
    ltac:(fun n' => [ > idtac "Doing reif (n=" n ") for" name "with" big ":" | .. ]; time do_reify ())
    ltac:(fun n' => [ > idtac "Doing post (n=" n ") for" name "with" big ":" | .. ]; time post_reify ())
           n ref_PHOAS ref_HOAS;
  idtac "Aggregate time (n=" n ") for" name "with" big ":").

Ltac print_stats big n ref_PHOAS ref_HOAS :=
  once (
      idtac "Stats (n=" n "):";
      time (idtac "Doing identity cbv (n=" n ") on PHOAS with" big ":"; let dummy := (eval cbv in ref_PHOAS) in idtac);
      time (idtac "Doing identity lazy (n=" n ") on PHOAS with" big ":"; let dummy := (eval lazy in ref_PHOAS) in idtac);
      time (idtac "Doing identity vm_compute (n=" n ") on PHOAS with" big ":"; let dummy := (eval vm_compute in ref_PHOAS) in idtac);
      (*time (idtac "Doing identity native_compute (n=" n ") on PHOAS with" big ":"; let dummy := (eval native_compute in ref_PHOAS) in idtac);*)
      time (idtac "Doing refine let (n=" n ") on PHOAS with" big ":"; let p := fresh in refine (let p := ref_PHOAS in _); clear p);
      time (idtac "Doing cbv Denote (n=" n ") on PHOAS with" big ":"; let v := (eval cbv [PHOAS.Denote PHOAS.denote] in (PHOAS.Denote ref_PHOAS)) in idtac);
      time (idtac "Doing lazy Denote (n=" n ") on PHOAS with" big ":"; let v := (eval lazy [PHOAS.Denote PHOAS.denote] in (PHOAS.Denote ref_PHOAS)) in idtac);
      time (idtac "Doing identity cbv (n=" n ") on HOAS with" big ":"; let dummy := (eval cbv in ref_HOAS) in idtac);
      time (idtac "Doing identity lazy (n=" n ") on HOAS with" big ":"; let dummy := (eval lazy in ref_HOAS) in idtac);
      time (idtac "Doing identity vm_compute (n=" n ") on HOAS with" big ":"; let dummy := (eval vm_compute in ref_HOAS) in idtac);
      (*time (idtac "Doing identity native_compute (n=" n ") on HOAS with" big ":"; let dummy := (eval native_compute in ref_HOAS) in idtac);*)
      time (idtac "Doing refine let (n=" n ") on HOAS with" big ":"; let p := fresh in refine (let p := ref_HOAS in _); clear p);
      time (idtac "Doing cbv denote (n=" n ") on HOAS with" big ":"; let v := (eval cbv [HOAS.denote] in (HOAS.denote ref_HOAS)) in idtac);
      time (idtac "Doing lazy denote (n=" n ") on HOAS with" big ":"; let v := (eval lazy [HOAS.denote] in (HOAS.denote ref_HOAS)) in idtac)
    ).
Ltac foreach tac ns :=
  lazymatch ns with
  | cons ?n ?ns => once (tac n); foreach tac ns
  | nil => idtac
  end.
Ltac foreach3 tac ns :=
  lazymatch ns with
  | cons (?n, ?x, ?y) ?ns => once (tac n x y); foreach3 tac ns
  | nil => idtac
  end.
Ltac noop _ := idtac.
Open Scope nat_scope.
Import CanonicalStructuresFlatHOAS.Exports.
Import CanonicalStructuresFlatPHOAS.Exports.
Import CanonicalStructuresHOAS.Exports.
Ltac do_cbv_delta := lazy [big_flat]; lazy delta [big].
Ltac do_cbv := lazy [big_flat big big_flat_op].
Ltac do_test is_flat ns :=
  let big := lazymatch is_flat with
             | true => big_flat
             | false => big
             end in
  let ns_with_refs
      := (eval vm_compute in (if is_flat then big_flat_refs ns else big_refs ns)) in
  foreach3 ltac:(fun n refP refH => print_stats big n refP refH) ns_with_refs;
  (*foreach3 ltac:(fun n refP refH => do_test_with "pattern-no-beta" big (do_cbv_delta) (noop) (Pattern.do_Reify_rhs) (Pattern.post_Reify_rhs) n refP refH) ns_with_refs;
  foreach3 ltac:(fun n refP refH => do_test_with "pattern-beta" big (do_cbv) (noop) (Pattern.do_Reify_rhs) (Pattern.post_Reify_rhs) n refP refH) ns_with_refs;*)
  (*foreach3 ltac:(fun n refP refH => do_test_with "TemplateCoq" big (do_cbv) (noop) (TemplateCoq.do_Reify_rhs) (TemplateCoq.post_Reify_rhs) n refP refH) ns_with_refs;*)
  foreach3 ltac:(fun n refP refH => do_test_with "OCaml" big (do_cbv) (noop) (OCaml.do_Reify_rhs) (OCaml.post_Reify_rhs) n refP refH) ns_with_refs;
  foreach3 ltac:(fun n refP refH => do_test_with "Ltac2Unsafe" big (do_cbv) (noop) (Ltac2Unsafe.do_Reify_rhs) (Ltac2Unsafe.post_Reify_rhs) n refP refH) ns_with_refs(*;
  foreach3 ltac:(fun n refP refH => do_test_with "Ltac2" big (do_cbv) (noop) (Ltac2.do_Reify_rhs) (Ltac2.post_Reify_rhs) n refP refH) ns_with_refs;
  foreach3 ltac:(fun n refP refH => do_test_with "LtacTacInTermGallinaCtx" big (do_cbv) (noop) (LtacTacInTermGallinaCtx.do_Reify_rhs) (LtacTacInTermGallinaCtx.post_Reify_rhs) n refP refH) ns_with_refs;
  foreach3 ltac:(fun n refP refH => do_test_with "LtacTacInTermInductiveCtx" big (do_cbv) (noop) (LtacTacInTermInductiveCtx.do_Reify_rhs) (LtacTacInTermInductiveCtx.post_Reify_rhs) n refP refH) ns_with_refs;
  foreach3 ltac:(fun n refP refH => do_test_with "LtacTCGallinaCtx" big (do_cbv) (noop) (LtacTCGallinaCtx.do_Reify_rhs) (LtacTCGallinaCtx.post_Reify_rhs) n refP refH) ns_with_refs;
  foreach3 ltac:(fun n refP refH => do_test_with "LtacTCInductiveCtx" big (do_cbv) (noop) (LtacTCInductiveCtx.do_Reify_rhs) (LtacTCInductiveCtx.post_Reify_rhs) n refP refH) ns_with_refs;
  foreach3 ltac:(fun n refP refH => do_test_with "LtacPrimUncurry" big (do_cbv) (noop) (LtacPrimUncurry.do_Reify_rhs) (LtacPrimUncurry.post_Reify_rhs) n refP refH) ns_with_refs;
  foreach3 ltac:(fun n refP refH => do_test_with "CanonicalStructuresHOAS" big (do_cbv) (CanonicalStructuresHOAS.pre_Reify_rhs) (CanonicalStructuresHOAS.do_Reify_rhs) (CanonicalStructuresHOAS.post_Reify_rhs) n refP refH) ns_with_refs;
  lazymatch is_flat with
  | true
    =>
    foreach3 ltac:(fun n refP refH => do_test_with "CanonicalStructuresFlatHOAS" big (do_cbv) (CanonicalStructuresFlatHOAS.pre_Reify_rhs) (CanonicalStructuresFlatHOAS.do_Reify_rhs) (CanonicalStructuresFlatHOAS.post_Reify_rhs) n refP refH) ns_with_refs;
    foreach3 ltac:(fun n refP refH => do_test_with "CanonicalStructuresFlatPHOAS" big (do_cbv) (CanonicalStructuresFlatPHOAS.pre_Reify_rhs) (CanonicalStructuresFlatPHOAS.do_Reify_rhs) (CanonicalStructuresFlatPHOAS.post_Reify_rhs) n refP refH) ns_with_refs
  | false => idtac
  end;
  foreach3 ltac:(fun n refP refH => do_test_with "TypeClasses" big (do_cbv) (noop) (TypeClasses.do_Reify_rhs) (TypeClasses.post_Reify_rhs) n refP refH) ns_with_refs*).
Ltac do_one_test is_flat n := do_test is_flat (cons n nil).
Ltac do_quick_tests is_flat :=
  do_test is_flat (1::2::4::8::16::32::64::nil)%list%nat.
Ltac do_all_tests is_flat :=
  do_test is_flat (1::2::4::8::16::32::64::100::200::300::400::500::600::700::800::900::1000::nil)%list%nat.
Notation n := 800%nat.
Notation hidden := (_ = _).
Import Ltac2.Init.
Import Ltac2.Notations.
Import Ltac2Unsafe.
Goal exists v, v = big 1 7000%nat.
  eexists.
  Time lazy [big].
  let g := Control.goal () in
  match Constr.Unsafe.kind g with
  | Constr.Unsafe.App f args (* App eq [ty; lhs; rhs] *)
    => let v := Array.get args 2 in
       let rv := Control.time (Some "Actual reif") (fun _ => unsafe_Reify v) in
       () (*
         let rv := Control.time (Some "Actual lazy") (fun _ => Std.eval_lazy all_flags rv) in
         Control.time (Some "lazy beta iota") (fun _ => Std.lazy betaiota_flags in_goal);
         Control.time (Some "trans") (fun _ => Std.transitivity (unsafe_mkApp1 'Denote rv))*)
  | _
    => Control.zero (Tactic_failure (Some (Message.concat (Message.of_string "Invalid goal in Ltac2Unsafe.do_Reify_rhs_fast: ") (Message.of_constr g))))
  end.
  (*do_test false (7000::nil)%nat%list.*)

reify.ml4

(*i camlp4deps: "parsing/grammar.cma" i*)
(*i camlp4use: "pa_extend.cmp" i*)

let contrib_name = "template-coq-derivative"

open Names

let rec unsafe_reify_helper
        (mkVar : Constr.t -> 'a)
        (mkConst : Constr.t -> 'a)
        (zAdd : Constr.t)
        (mkAdd : 'a -> 'a -> 'a)
        (idLetIn : Constr.t)
        (mkLetIn : 'a -> Name.t -> Constr.t -> 'a -> 'a)
        (term : Constr.t)
    =
      let reify_rec term = unsafe_reify_helper mkVar mkConst zAdd mkAdd idLetIn mkLetIn term in
      let kterm = Constr.kind term in
      begin match kterm with
      | Term.Rel _ -> mkVar term
      | Term.Var _ -> mkVar term
      | Term.Cast (term, _, _) -> reify_rec term
      | Term.App (f, args)
        ->
        if Constr.equal f zAdd
        then let x = Array.get args 0 in
             let y = Array.get args 1 in
             let rx = reify_rec x in
             let ry = reify_rec y in
             mkAdd rx ry
        else if Constr.equal f idLetIn
        then let x = Array.get args 2 (* assume the first two args are type params *) in
             let f = Array.get args 3 in
             begin match Constr.kind f with
             | Term.Lambda (idx, ty, body)
               -> let rx = reify_rec x in
                  let rf = reify_rec body in
                  mkLetIn rx idx ty rf
             | _ -> mkConst term
             end
         else mkConst term
      | _
        -> mkConst term
      end

let unsafe_reify
        (cVar : Constr.t)
        (cConst : Constr.t)
        (cAdd : Constr.t)
        (cLetIn : Constr.t)
        (gAdd : Constr.t)
        (gLetIn : Constr.t)
        (var : Constr.t)
        (term : Constr.t) =
    let mkApp1 (f : Constr.t) (x : Constr.t) =
        Constr.mkApp (f, [| var ; x |]) in
    let mkApp2 (f : Constr.t) (x : Constr.t) (y : Constr.t) =
        Constr.mkApp (f, [| var ; x ; y |]) in
    let mkVar (v : Constr.t) = mkApp1 cVar v in
    let mkConst (v : Constr.t) = mkApp1 cConst v in
    let mkAdd (x : Constr.t) (y : Constr.t) = mkApp2 cAdd x y in
    let mkcLetIn (x : Constr.t) (y : Constr.t) = mkApp2 cLetIn x y in
    let mkLetIn (x : Constr.t) (idx : Name.t) (ty : Constr.t) (fbody : Constr.t)
        = mkcLetIn x (Constr.mkLambda (idx, var, fbody)) in
    let ret = unsafe_reify_helper mkVar mkConst gAdd mkAdd gLetIn mkLetIn term in
    ret

module Vars = (* Coq's API is stupid, so we have to copy code from the kernel to make use of things, because I can't interface with Ltac if I pass -bypass-API *)
struct
  open Vars
  let substn_vars p vars c =
  let _,subst =
    List.fold_left (fun (n,l) var -> ((n+1),(var,Constr.mkRel n)::l)) (p,[]) vars
  in replace_vars (List.rev subst) c
end

let unsafe_Reify
        (cVar : Constr.t)
        (cConst : Constr.t)
        (cAdd : Constr.t)
        (cLetIn : Constr.t)
        (gAdd : Constr.t)
        (gLetIn : Constr.t)
	(idvar : Id.t)
	(varty : Constr.t)
        (term : Constr.t) =
    let fresh_set = let rec fold accu c = match Constr.kind c with
      | Constr.Var id -> Id.Set.add id accu
      | _ -> Constr.fold fold accu c
      in
      fold Id.Set.empty term in
    (*let idvar = Namegen.next_ident_away_from idvar (fun id -> Id.Set.mem id fresh_set) in*) (* stupid API *)
    let idvar = Namegen.next_ident_away_in_goal idvar fresh_set in
    let var = Constr.mkVar idvar in
    let rterm = unsafe_reify cVar cConst cAdd cLetIn gAdd gLetIn var term in
    let rterm = Vars.substn_vars 1 [idvar] rterm in
    Constr.mkLambda (Name.Name idvar, varty, rterm)

DECLARE PLUGIN "reify"

open Ltac_plugin
open Stdarg
open Tacarg
open Names

(** Stolen from plugins/setoid_ring/newring.ml *)
open Tacexpr
open Misctypes
open Tacinterp
(* Calling a locally bound tactic *)
let ltac_lcall tac args =
  TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar(Loc.tag @@ Id.of_string tac),args)))

let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) =
  let fold arg (i, vars, lfun) =
    let id = Id.of_string ("x" ^ string_of_int i) in
    let x = Reference (ArgVar (Loc.tag id)) in
    (succ i, x :: vars, Id.Map.add id arg lfun)
  in
  let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
  let lfun = Id.Map.add (Id.of_string "F") f lfun in
  let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in
  Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args)

let to_ltac_val c = Tacinterp.Value.of_constr c

open Pp

TACTIC EXTEND quote_term_cps
    | [ "quote_term_cps" constr(cVar) constr(cConst) constr(cAdd) constr(cLetIn) constr(gAdd) constr(gLetIn) ident(idvar) constr(varty) constr(term) tactic(tac) ] ->
      [ (** quote the given term, pass the result to t **)
  Proofview.Goal.enter begin fun gl ->
          let _ (*env*) = Proofview.Goal.env gl in
          let c = unsafe_Reify (EConstr.Unsafe.to_constr cVar) (EConstr.Unsafe.to_constr cConst) (EConstr.Unsafe.to_constr cAdd) (EConstr.Unsafe.to_constr cLetIn) (EConstr.Unsafe.to_constr gAdd) (EConstr.Unsafe.to_constr gLetIn) idvar (EConstr.Unsafe.to_constr varty) (EConstr.Unsafe.to_constr term) in
          ltac_apply tac (List.map to_ltac_val [EConstr.of_constr c])
  end ]
END;;

reify.mllib

Reify

reify.v

Declare ML Module "reify".