Require Import Coq.Lists.List.
Require Import Coq.Program.Equality.
Require Import Omega.
Require Import String.
Require Import Bool.
Import ListNotations.
Open Scope list_scope.
Open Scope string_scope.

Inductive label : Type := (* efficiency hack *)
| lDiscard : label
| lCapture : label
| lQuote: label
| lStr : string -> label.

Inductive value : Type :=
| vBool : bool -> value
| vSymbol : label -> value
| vRecord: value -> values -> value
| vSeq : values -> value
with values : Type :=
     | vsNil : values
     | vsCons : value -> values -> values.

Inductive pat : Type :=
| pDiscard : pat
| pCapture : pat -> pat
| pBool : bool -> pat
| pSymbol : label -> pat
| pRecord: pat -> pats -> pat
| pSeq : pats -> pat
with pats : Type :=
     | psNil : pats
     | psCons : pat -> pats -> pats.

Definition vs1 v : values := vsCons v vsNil.
Definition ps1 p : pats := psCons p psNil.

Definition vQuote v : value := vRecord (vSymbol lQuote) (vs1 v).

Lemma value_dec : forall x y : value, { x = y } + { x <> y }
with values_dec : forall xs ys : values, { xs = ys } + { xs <> ys }.
  repeat decide equality.
  repeat decide equality.
Defined.

Lemma pat_dec : forall x y : pat, { x = y } + { x <> y }
with pats_dec : forall xs ys : pats, { xs = ys } + { xs <> ys }.
  repeat decide equality.
  repeat decide equality.
Defined.

Fixpoint qp p : value :=
  match p with
  | pDiscard => vRecord (vSymbol lDiscard) vsNil
  | pCapture p' => vRecord (vSymbol lCapture) (vs1 (qp p'))
  | pBool b => vBool b
  | pSymbol s => vSymbol s
  | pRecord (pSymbol lDiscard) psNil => vRecord (vQuote (vSymbol lDiscard)) vsNil
  | pRecord (pSymbol lCapture) (psCons p' psNil) => vRecord (vQuote (vSymbol lCapture)) (vs1 (qp p'))
  | pRecord (pSymbol lQuote) (psCons p' psNil) => vRecord (vQuote (vSymbol lQuote)) (vs1 (qp p'))
  | pRecord l ps => vRecord (qp l) (qps ps)
  | pSeq ps => vSeq (qps ps)
  end
with qps ps : values :=
       match ps with
       | psNil => vsNil
       | psCons p' ps' => vsCons (qp p') (qps ps')
       end.

Fixpoint raw_uqp v : pat :=
  match v with
  | vBool b => pBool b
  | vSymbol s => pSymbol s
  | vRecord l fs => pRecord (raw_uqp l) (raw_uqps fs)
  | vSeq vs => pSeq (raw_uqps vs)
  end
with raw_uqps vs : pats :=
       match vs with
       | vsNil => psNil
       | vsCons v vs' => psCons (raw_uqp v) (raw_uqps vs')
       end.

Fixpoint uqp v : pat :=
  match v with
  | vRecord (vSymbol lDiscard) vsNil => pDiscard
  | vRecord (vSymbol lCapture) (vsCons v' vsNil) => pCapture (uqp v')
  | vRecord (vSymbol lQuote) (vsCons v' vsNil) => raw_uqp v'
  | vBool b => pBool b
  | vSymbol s => pSymbol s
  | vRecord l fs => pRecord (uqp l) (uqps fs)
  | vSeq vs => pSeq (uqps vs)
  end
with uqps vs : pats :=
       match vs with
       | vsNil => psNil
       | vsCons v vs' => psCons (uqp v) (uqps vs')
       end.

Lemma quoting_for_record_sensible :
  forall p ps,
    p <> pSymbol lDiscard ->
    p <> pSymbol lCapture ->
    p <> pSymbol lQuote ->
    uqp (qp (pRecord p ps)) = pRecord (uqp (qp p)) (uqps (qps ps)).
Proof.
  destruct p; try reflexivity.
  destruct l; try congruence; reflexivity.
  intros; destruct p; try reflexivity.
  destruct l; try reflexivity; destruct p0; try reflexivity.
  destruct p0; try reflexivity.
  destruct p0; try reflexivity.
Qed.

Theorem quoting_sensible : forall p, uqp (qp p) = p
with quoting_list_sensible : forall ps, uqps (qps ps) = ps.
Proof.
  clear quoting_sensible.
  induction p; try reflexivity.
  remember (qp (pCapture p)) as p'; simpl in Heqp'; rewrite Heqp'; simpl; rewrite IHp; reflexivity.

  remember (pat_dec p (pSymbol lDiscard)) as HisDiscard; inversion HisDiscard.
  remember (pats_dec p0 psNil) as HisEmpty; inversion HisEmpty.
  rewrite H, H0; reflexivity.
  rewrite H; remember p0 as p0'; destruct p0'.
  congruence.
  simpl.
  rewrite Heqp0'.
  rewrite <- quoting_list_sensible with (ps := p0).
  rewrite <- Heqp0'.
  reflexivity.

  remember (pat_dec p (pSymbol lCapture)) as HisCapture; inversion HisCapture;
    [ rewrite H0; clear H0 | ].
  remember p0 as p0'; destruct p0'; [ reflexivity | ].
  rewrite Heqp0'.
  destruct p0';
    [ simpl | unfold qp];
    rewrite <- quoting_list_sensible with (ps := p0) at 2;
    rewrite <- Heqp0';
    reflexivity.

  remember (pat_dec p (pSymbol lQuote)) as HisQuote; inversion HisQuote;
    [ rewrite H1; clear H1 | ].
  remember p0 as p0'; destruct p0'; [ reflexivity | ].
  rewrite Heqp0'.
  destruct p0';
    [ simpl | unfold qp];
    rewrite <- quoting_list_sensible with (ps := p0) at 2;
    rewrite <- Heqp0';
    reflexivity.

  rewrite quoting_for_record_sensible; try assumption.
  rewrite <- IHp at 2.
  rewrite <- quoting_list_sensible with (ps := p0) at 2.
  reflexivity.

  rewrite <- quoting_list_sensible with (ps := p) at 2; reflexivity.

  clear quoting_list_sensible.
  induction ps; try reflexivity.
  simpl.
  rewrite quoting_sensible.
  f_equal.
  apply IHps.
Qed.