Library Mtac2.meta.MFix

From Mtac2 Require Import Base Logic Datatypes MFixDef MTele MTeleMatch.
Import M.notations.
Import Sorts.S.

Set Universe Polymorphism.
Unset Universe Minimization ToSet.

Local Definition MFA {n} (T : MTele_Ty n) := (MTele_val (MTele_C SType SProp M T)).

Definition MTele_of' :=
  (mfix1 f (T : Prop) : M { m : MTele & { mT : MTele_Ty m & T =m= MFA mT } } :=
     mmatch T as T0 return M { m : MTele & { mT : MTele_Ty m & T =m= MFA mT } } with
     | [?X : Type] M X =u> [H]
                        M.ret (existT (fun m => {mT : MTele_Ty m & T =m= MFA mT}) (mBase)
                                      (existT (fun mT : MTele_Ty mBase => T =m= MFA mT) _ H)
                              )
     | [?(X : Type) (F : forall x:X, Prop)] (forall x:X, F x) =c> [H]
       M.nu (FreshFrom F) mNone (fun x =>
                       ''(existT _ m (existT _ mT E)) <- f (F x);
                       m' <- M.abs_fun x m;
                       mT' <- (M.coerce mT >>=
                               M.abs_fun (P:=fun x => MTele_Ty (m' x)) x);
                       
                       E' <- M.coerce (@meq_refl _ (MFA (n:=mTele m') mT'));
                       M.ret (existT _ (mTele m') (existT _ mT' E'))
                       
                       
                       
                       
                       
                       
                       
                    )
   end
  ).

Definition MTele_of : Prop -> M (sigT MTele_Ty) :=
  mfix1 f (T : Prop) : M (sigT MTele_Ty) :=
     mmatch T return M (sigT MTele_Ty) with
     | [?X : Type] M X =u> M.ret (existT _ mBase X)
     | [?(X : Type) (F : forall x:X, Prop)] (forall x:X, F x) =c>
       M.nu (FreshFrom F) mNone (fun x =>
                       ''(existT _ n T) <- f (F x);
                       n' <- M.abs_fun (P:=fun _ => MTele) x n;
                       T' <- M.abs_fun x T;
                       T' <- M.coerce T';
                       M.ret (existT _ (mTele n') T')
                    )
   end
.

Class MT_OF (T : Prop) := mt_of : sigT MTele_Ty.
Arguments mt_of _ {_}.
Hint Extern 0 (MT_OF ?t) => mrun (MTele_of t) : typeclass_instances.

Set Use Unicoq.

Structure execV {A} (f : M A) B := ExecV { value : B } .

Monomorphic Canonical Structure the_value {A} (f : M A) v := ExecV _ f (lift f v) v.

Arguments value {A} f {B} {e}.

Notation "'[run' t ]" :=
((let H := _ in let _ : value (t) = H := eq_refl in H)).

Definition exec {A} (f : M A) {v:A} : lift f v := v.

Notation "'[ex' t ']'" := (exec t) (at level 0).

Definition mfix_eq {m : MTele} {T: MTele_Ty m} {A : Prop} : forall {Eq : MFA T =m= A}, (A -> A) -> A :=
  fun eq => match eq in _ =m= R return (R -> R) -> R with
            | meq_refl => fun f => mfix' _ f
            end.

Definition mfix_lift {m : MTele} {A : Prop} {F : (A -> A) -> A}:
  lift (
     ''(existT _ m' (existT _ mT E)) <-mtry MTele_of' A
        with
    | [?E] E =>
      M.print_term E;;
      M.evar _
      end;
      M.unify m m' UniCoq;;
        match meq_sym E in _ =m= R return M ((R -> R) -> R) with
        | meq_refl => M.ret (mfix' mT)
        end) (F) := F.


Notation "'mfix' f x .. y : T := b" :=
  (
  
  
  
  
  
  
  
    ((mfix_lift
      :
        
        
        
        ((forall x, .. (forall y, T) ..)
         -> (forall x, .. (forall y, T) ..))
        -> (forall x, .. (forall y, T) ..)
     )
       (fun f => (fun x => .. (fun y => b) ..))
    )
  ) (only parsing,
      no associativity,
     at level 85,
     f ident,
     x binder,
     y binder,
     
     format "mfix f x .. y : T := b"
    ).

Definition bla := mfix f (x : nat) : True -> M True := fun i => f x i.