Lvc.IL.Patterns

Require Import List.
Require Export Util Get Drop Var Val Exp Env Map CSet AutoIndTac MoreList.

Set Implicit Arguments.

Inductive pattern :=
  | PatternScore
  | PatternVar (x:var)
  | PatternList (Z:list var).

Fixpoint patternVars (p:pattern) : set var :=
  match p with
    | PatternScore
    | PatternVar x{{x}}
    | PatternList Zof_list Z
  end.

Definition patternMatchList
         (patternMatch: pattern val option (list var × list val)) :=
  fix patternMatchList (Z:list pattern) (vl:list val) {struct Z} : option (list var × list val) :=
  match Z, vl with
    | p::Z', v::vl
      mdo l <- patternMatch p v;
        let (varl, vall) := l in
        mdo l' <- patternMatchList Z' vl;
          let (varl', vall') := l' in
          Some ((varl++varl')%list, (vall++vall')%list)
    | nil, nilSome (nil, nil)
  | _, _None
  end.

Fixpoint patternMatch (p:pattern) (v:val) {struct p} : option (list var × list val) :=
  match p, v with
    | PatternScore, _Some (nil, nil)
    | PatternVar x, vSome (x::nil, v::nil)

    | _, _None
  end.

Definition patterneq (p q:pattern)
  := v, patternMatch p v None patternMatch q v None.

Instance patterneq_Equivalence_instance : Equivalence patterneq.
constructor; firstorder.
Defined.

Lemma patterneq_some p q v ZVL
: patterneq p q patternMatch p v = Some ZVL ZVL, patternMatch q v = Some ZVL.
Proof.
  intros. specialize (H v).
  destruct (patternMatch q v).
  - eexists; eauto.
  - exfalso. destruct H. eapply H; congruence.
Qed.