context_pattern.v

From Mtac2 Require Import Specif Mtac2 MTele MFix MTeleMatch.
Close Scope tactic_scope.       (* Really need to fix this! *)
From Unicoq Require Import Unicoq.

Definition make_pattern_tele :=
  mfix go (T : Type) : forall f: T, M MTele :=
    mtmmatch T as T return forall f: T, M _ with
    | [? X P] forall x : X, P x =u>
      fun f =>
        \nu_f for f as x,
          let Px := reduce (RedOneStep [rl:RedBeta]) (P x) in
          tele <- go _ (f x);
          tele_cont <- M.abs_fun x tele;
          M.ret (mTele tele_cont)
    | _ => fun _ => M.ret mBase
    end.
Arguments make_pattern_tele [_].

Open Scope tactic_scope.
#[local] Definition match_context_type (Ti To : Type) (tele: MTele) :=
  forall
    (pattern_head : MTele_ConstT Ti tele)
    (target_head : MTele_ConstT To tele)
    (cont: ArgsOf tele -> To -> tactic),
    tactic.
Definition match_context {Ti To : Type} :
  forall (tele: MTele), match_context_type Ti To tele :=
  fix go tele : match_context_type Ti To tele :=
    match tele as tele return match_context_type Ti To tele
    with
    | mBase => fun ph th cont => (* we've handled all arguments. time to search for occurrences *)
        match_goal with
        | [[ |- context C [ ph ] ]] => cont tt th
        end
    | @mTele X F => fun ph th cont =>
        (* prepare evar for one argument *)
        x <- M.evar X;
        go (F x) (ph x) (th x) (fun args to => cont (mexistT _ x args) to)
    end
.

Goal 1 + 2 = 3.
  mrun (tele <- make_pattern_tele (Nat.add);
        M.print_term tele;;
        (* we don't know the connection between [tele] and [Nat.add] so we coerce to get [Nat.add : MTele_ConstT nat tele] *)
        na <- M.coerce Nat.add;
        nm <- M.coerce Nat.mul;
        match_context tele na nm (fun args mul => M.print_term mul;; T.idtac)).
  (* Prints [1 * 2] *)
Abort.

I can't seem to get this to compile. I'm getting a Conversion test raised an anomaly: Anomaly "Universe Var(0) undefined." when trying to evaluate the first definition. I assume that this is coming from the fact that you are looking for a universe.