Require Import Coq.Lists.List.
Require Import String.
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 -> list value -> value
| vSeq : list value -> value.

Inductive pat : Type :=
| pDiscard : pat
| pCapture : pat -> pat
| pBool : bool -> pat
| pSymbol : label -> pat
| pRecord: pat -> list pat -> pat
| pSeq : list pat -> pat.

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

Fixpoint value_dec (x y : value) : { x = y } + { x <> y }.
  repeat decide equality.
Defined.

Fixpoint pat_dec (x y : pat) : { x = y } + { x <> y }.
  repeat decide equality.
Defined.

Fixpoint qp p : value :=
  match p with
  | pDiscard => vRecord (vSymbol lDiscard) []
  | pCapture p' => vRecord (vSymbol lCapture) [qp p']
  | pBool b => vBool b
  | pSymbol s => vSymbol s
  | pRecord (pSymbol lDiscard) [] => vRecord (vQuote (vSymbol lDiscard)) []
  | pRecord (pSymbol lCapture) [p'] => vRecord (vQuote (vSymbol lCapture)) [qp p']
  | pRecord (pSymbol lQuote) [p'] => vRecord (vQuote (vSymbol lQuote)) [qp p']
  | pRecord l ps => vRecord (qp l) (map qp ps)
  | pSeq ps => vSeq (map qp 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) (map raw_uqp fs)
  | vSeq vs => pSeq (map raw_uqp vs)
  end.

Fixpoint uqp v : pat :=
  match v with
  | vRecord (vSymbol lDiscard) [] => pDiscard
  | vRecord (vSymbol lCapture) [v'] => pCapture (uqp v')
  | vRecord (vSymbol lQuote) [v'] => raw_uqp v'
  | vBool b => pBool b
  | vSymbol s => pSymbol s
  | vRecord l fs => pRecord (uqp l) (map uqp fs)
  | vSeq vs => pSeq (map uqp vs)
  end.

Fixpoint pat_ind'
         (P : pat -> Prop)
         (PDiscard : P pDiscard)
         (PCapture : forall p, P p -> P (pCapture p))
         (PBool : forall b, P (pBool b))
         (PSymbol : forall l, P (pSymbol l))
         (PRecord : forall p ps, P p -> Forall P ps -> P (pRecord p ps))
         (PSeq : forall ps, Forall P ps -> P (pSeq ps))
         p
         : P p.
Proof.
  induction p; auto; [ apply PRecord; [ apply IHp | ] | apply PSeq ];
    try solve [ induction l; [ apply Forall_nil | ];
                apply Forall_cons; [ apply pat_ind'; try assumption | ];
                apply IHl ].
Defined.

Lemma Forall_map_map_id : forall ps, Forall (fun p : pat => uqp (qp p) = p) ps ->
                                     (map uqp (map qp ps)) = ps.
Proof.
  intros; rewrite map_map; induction H; [ reflexivity | ].
  simpl; rewrite IHForall; rewrite H; reflexivity.
Qed.

Ltac solve_map_map_id := repeat f_equal; apply Forall_map_map_id; assumption.

Theorem quoting_sensible : forall p, uqp (qp p) = p.
Proof.
  induction p using pat_ind';
    try solve [ reflexivity
              | rewrite <- IHp at 2; reflexivity
              | simpl; solve_map_map_id ].

  destruct p; simpl; try rewrite <- IHp; try solve [ solve_map_map_id ].

  (* label pSymbol *)
  destruct l;
    [ destruct ps; [ reflexivity | inversion H; simpl; rewrite H2; solve_map_map_id ]
    | | | simpl; solve_map_map_id ];
    try solve [ destruct ps; [ reflexivity | ];
      destruct ps; [ inversion H; simpl; rewrite H2; reflexivity | ];
      inversion H; simpl; rewrite H2;
      inversion H3; simpl; rewrite H6;
      solve_map_map_id ].

  (* label pRecord *)
  destruct p; try solve_map_map_id;
    destruct l0; destruct l; try solve_map_map_id;
      destruct l; solve_map_map_id.
Qed.