Library Mtac2Tests.test_mmatch

Require Import Mtac2.Mtac2.
Import T.

Goal True.
MProof.
  (mmatch I with
  [? i] i => M.ret i : M True
  end)%MC.
Qed.

Goal True.
MProof.
  (mmatch _ with
  [? i] i => M.ret i : M True
  end)%MC.
  Unshelve.
  (mmatch (fun x=>x) I with
  [? i] (fun x=>x) i => M.ret i : M True
  end)%MC.
Qed.

Goal True.
MProof.
  (mmatch (fun x=>x) I with
  [? i] I => M.ret i : M True
  end)%MC.
  Fail (mmatch I with
  [? i] (fun x=>x) i => M.ret i : M True
  end)%MC.
  Unshelve.
  (mmatch I with
  | [? i] (fun x=>x) i => M.ret i : M True
  | [? i] i => M.ret i : M True
  end)%MC.
Qed.

Require Import List.
Import ListNotations.

Definition NotFound : Exception. exact exception. Qed.

Require Import Init.Datatypes.
Require Import Lists.List.
Import Base.M.
Import M.notations.

Definition inlist A (x : A) : forall (l : list A), M (In x l) :=
  mfix1 f (l : list A) : M (In x l) :=
  mmatch l with
  | [? l r] l ++ r =>
      M.mtry' (
        il <- f l;
        M.ret (in_or_app l r x (or_introl il)) )
      (fun e=>mmatch e with NotFound =>
        ir <- f r;
        M.ret (in_or_app l r x (or_intror ir))
      end)
  | [? s] (x :: s) => M.ret (in_eq _ _)
  | [? y s] (y :: s) => r <- f s; M.ret (in_cons y _ _ r)
  | _ => M.raise NotFound
  end.
Import ListNotations.

Example testM (
x01 x11 x21 x31 x41 x51 x61 x71 x81 x91
x02 x12 x22 x32 x42 x52 x62 x72 x82 x92
x03 x13 x23 x33 x43 x53 x63 x73 x83 x93
x04 x14 x24 x34 x44 x54 x64 x74 x84 x94
x05 x15 x25 x35 x45 x55 x65 x75 x85 x95
x06 x16 x26 x36 x46 x56 x66 x76 x86 x96
x07 x17 x27 x37 x47 x57 x67 x77 x87 x97
x08 x18 x28 x38 x48 x58 x68 x78 x88 x98
x09 x19 x29 x39 x49 x59 x69 x79 x89 x99
 : nat) : In x99 [
x01;x11;x21;x31;x41;x51;x61;x71;x81;x91;
x02;x12;x22;x32;x42;x52;x62;x72;x82;x92;
x03;x13;x23;x33;x43;x53;x63;x73;x83;x93;
x04;x14;x24;x34;x44;x54;x64;x74;x84;x94;
x05;x15;x25;x35;x45;x55;x65;x75;x85;x95;
x06;x16;x26;x36;x46;x56;x66;x76;x86;x96;
x07;x17;x27;x37;x47;x57;x67;x77;x87;x97;
x08;x18;x28;x38;x48;x58;x68;x78;x88;x98;
x09;x19;x29;x39;x49;x59;x69;x79;x89;x99
].
MProof.
  Time inlist _ _ _.
Qed.

Fail Definition test (t : nat) :=
  mmatch t with
  | 0 => ret (eq_refl 0)
  end.

Definition test_return (t : nat) : M (t = t) :=
  mmatch t as x return M (x = x) with
  | 0 => M.ret (eq_refl 0)
  end.

Definition test_return_in (t : nat) : M (t = t) :=
  mmatch 0+t as x return M (x = x) with
  | 0 => M.ret (eq_refl 0)
  end.

Definition inlist_nored A (x : A) : forall (l : list A), M (In x l) :=
  mfix1 f (l : list A) : M (In x l) :=
  mmatch l with
  | [? s] (x :: s) =n> M.ret (in_eq _ _)
  | [? y s] (y :: s) =n> r <- f s; M.ret (in_cons y _ _ r)
  | [? l r] l ++ r =n>
    mtry
      il <- f l;
      M.ret (in_or_app l r x (or_introl il))
    with NotFound =>
      ir <- f r;
      M.ret (in_or_app l r x (or_intror ir))
    end
  | _ => M.raise NotFound
  end.

Example with_red : In 0 ([1;2]++[0;4]).
MProof.
  inlist _ _ _.
Defined.

Example with_nored : In 0 ([1;2]++[0;4]).
MProof.
  inlist_nored _ _ _.
Defined.

Lemma are_equal : with_nored = with_red.
Proof. reflexivity. Qed.

Definition inlist_redcons A (x : A) : forall (l : list A), M (In x l) :=
  mfix1 f (l : list A) : M (In x l) :=
  mmatch l with
  | [? s] (x :: s) => M.ret (in_eq _ _)
  | [? y s] (y :: s) => r <- f s; M.ret (in_cons y _ _ r)
  | [? l r] l ++ r =n>
    mtry
      il <- f l;
      M.ret (in_or_app l r x (or_introl il))
    with NotFound =>
      ir <- f r;
      M.ret (in_or_app l r x (or_intror ir))
    end
  | _ => M.raise NotFound
  end.

Example with_redcons : In 0 ([1;2]++[0;4]).
MProof.
  inlist_redcons _ _ _.
Defined.

Lemma are_not_equal : with_nored = with_redcons.
Proof. Fail reflexivity. Abort.


From Mtac2 Require Import Sorts.
Mtac Do ((fun (T : Type) =>
            mmatch T with [¿ s] [? (T : s)] (T : Type) =u>
              M.unify_or_fail UniMatchNoRed s S.SProp;; M.ret I
          end) (True -> True)).
Mtac Do ((fun (T : Type) =>
            mmatch T with [¿ s] [? (T : s)] (T : Type) =u>
              M.unify_or_fail UniMatchNoRed s S.SType;; M.ret I
          end) (True -> nat)).


Mtac Do (
       M.mtry'
         (
          mtry
            M.raise DoesNotMatch
          with
          | DoesNotMatch =>
            mtry
              M.raise DoesNotMatch
            with
            | DoesNotMatch => M.raise DoesNotMatch
            end
          end)
         (fun e => M.unify_or_fail UniMatchNoRed e DoesNotMatch;; M.ret tt)
     ).

Mtac Do (
       mmatch (3 + 5) with
       | branch_app_static
             (m :=MTele.mTele (fun x : nat => MTele.mTele (fun y : nat => MTele.mBase)))
             UniMatchNoRed
             plus
             (fun x y => M.unify_or_fail UniMatchNoRed (x,y) (3,5))
      end
     ).

Mtac Do (
       mmatch (3 + 5) with
       | [#] plus | x y =n> M.unify_or_fail UniMatchNoRed (x,y) (3,5)
      end
     ).

Fail Mtac Do (
       mmatch (3 + 3) with
       | [#] plus (2+1) | y =n> M.unify_or_fail UniMatchNoRed (y) (5)
      end
     ).
Mtac Do (
       mmatch (3 + 5) with
       | [#] plus (2+1) | y =u> M.unify_or_fail UniMatchNoRed (y) (5)
      end
     ).

Mtac Do (
       mmatch (forall x : nat, x = x) with
       | branch_forallP (fun X P => M.unify_or_fail UniMatchNoRed P (fun x => x = x))
      end
     ).
Mtac Do (
       mmatch (nat -> Type) with
       | branch_forallT (fun X P => M.unify_or_fail UniMatchNoRed P (fun x => Type))
      end
     ).

Mtac Do (
       mmatch (forall x : nat, x = x) with
       | [!Prop] forall _ : X, P =n> M.unify_or_fail UniMatchNoRed P (fun x => x = x)
      end
     ).
Mtac Do (
       mmatch (nat -> Type) with
       | [!Type] forall _ : X, P =n> M.unify_or_fail UniMatchNoRed P (fun x => Type)
      end
     ).