Library Mtac2Tests.Exhaustive

Require Import Strings.String.
From Mtac2 Require Import Base List Exhaustive.
Import M.notations.

Check (mmatch 1 exhaustively_with
      | [#] S | n =n> M.print "S"
      | [#] O | =n> M.print "O"
      | _ => M.print "not in constructor normal form"
      end).

Check (mmatch 1 exhaustively_with
      | [#] O | =n> M.print "O"
      | [#] S | n =n> M.print "S"
      | _ => M.print "not in constructor normal form"
      end).

Check (mmatch 1 exhaustively_with
      | _ => M.print "always triggered first"
      | [#] O | =n> M.print "O, never triggered"
      | [#] S | n =n> M.print "S, never triggered"
      end).

Fail Check (mmatch 1 exhaustively_with
      | [#] S | n =n> M.print "S"
      | _ => M.print "not in constructor normal form"
      end).

Fail Check (mmatch 1 exhaustively_with
      | [#] O | =n> M.print "O"
      | _ => M.print "not in constructor normal form"
      end).

Fail Check (mmatch 1 exhaustively_with
      | _ => M.print "not in constructor normal form"
      | [#] O | =n> M.print "O"
      end).

Check (mmatch cons 1 nil exhaustively_with
      | [#] @nil _ | =n> M.print "nil"
      | [#] @cons _ | a l =n> M.print "cons"
      | _ => M.print "not in constructor normal form"
      end).

Fail Check (mmatch cons 1 nil exhaustively_with
      | [#] @nil _ | =n> M.print "nil"
      | [#] @cons (id nat) | a l =n> M.print "cons"
      | _ => M.print "not in constructor normal form"
      end).