Library Mtac2.ideas.StaticApply

Require Import Coq.Strings.String.
From Mtac2 Require Import Base Logic Datatypes List MFix MTeleMatch.
Import M.notations.
Import Mtac2.lib.List.ListNotations.

Definition funs_of (T : Prop) : mlist Prop -> Prop :=
  fix f l :=
  match l with
  | [m: ] => T
  | X :m: l => X -> f l
  end.

Definition args_of : mlist Prop -> Prop :=
  fix f l :=
  match l with
  | [m: ] => True
  | X :m: l => (X * f l)%type
  end.

Definition apply_args_of {T} : forall {l}, funs_of T l -> args_of l -> T :=
  fix f l :=
  match l as l return funs_of T l -> args_of l -> T with
  | [m: ] => fun t _ => t
  | X :m: l => fun F '(x, a) => f l (F x) a
  end.


Definition funs_bind {T X : Type} : forall {l},
  (X -> funs_of (M T) l) -> (M X -> funs_of (M T) l) :=
  fix f l :=
    match l return (X -> funs_of _ l) -> (M X -> funs_of _ l) with
    | [m:] => fun g mx => M.bind mx g
    | Y :m: l => fun g mx y => f _ (fun x => g x y) mx
    end.



Record Apply_Args (P T : Type) (t : T) :=
  APPLY_ARGS {
      apply_type: Type;
      apply_func: apply_type;
    }.

Definition remove_ret {V} {B} {Q : B -> Type} {A} : forall (v : V) b (m : Q b), (Q b -> M A) -> M A :=
  fun v b m cont =>
  m' <- M.remove v (M.ret m);
  oe <- M.unify m m' UniMatchNoRed;
  match oe with
  | mNone => M.failwith "Impossible branch."
  | mSome e =>
    match meq_sym e in _ =m= m'' return _ -> M A with
    | meq_refl =>
      fun cont =>
        cont m'
    end cont
  end
.

Set Printing Universes.
Set Use Unicoq.
Program Definition apply_type_of (P : Type) :
  forall {T} (t : T),
                      M (sigT (funs_of (M P))) :=
  mfix f (T : _) : T -> M (sigT (funs_of (M P))) :=
     mtmmatch_prog T as T' return T' -> M (sigT (funs_of (M P))) with
     | (M P : Type) =c> fun t => M.ret (existT (funs_of (M P)) [m:] t)
     | [? X F] (forall x : X, F x) =c>
        fun ft =>
          M.nu (FreshFrom ft) mNone (fun x_nu : X =>
          x <- M.evar X;
          let F' := reduce (RedOneStep [rl:RedBeta]) (F x) in
          let f' := reduce (RedOneStep [rl:RedBeta]) (ft x) in
          r <- f F' f';
          mif M.is_evar x then
            o <- M.unify x_nu x UniEvarconv;
            let '(existT _ rl rp) := r in
             rp' <- M.abs_fun x_nu rp;
             mtry (M.remove x_nu (
                   let r' : sigT (funs_of (M P)) := existT _ (M X :m: rl) (funs_bind rp') in
                   M.ret r'
                 )) with
          | [?s] CannotRemoveVar s =>
            let err := (String.append "A hypothesis depends on " s) in
            M.failwith err
         end
       else M.remove x_nu (M.ret r)
       )
  | _ => fun _ =>
      M.failwith "The lemma's conclusion does not unify with the goal."
  end
.







Notation "t '&s>' '[s' t1 ; .. ; tn ]" :=
  (
    let t' := t in
    let r := M.eval (apply_type_of _ t') in
    let args := M.eval ( (M.coerce (pair t1 .. (pair tn I) ..))) in
    apply_args_of (projT2 r) args
  ) (at level 41, left associativity,
     format "t &s> [s t1 ; .. ; tn ]"
    ).