Require Import Coq.Lists.List.
Require Import Coq.Strings.String.
Require Import Coq.Program.Equality.
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_ind'
         (P : value -> Prop)
         (PBool : forall b, P (vBool b))
         (PSymbol : forall l, P (vSymbol l))
         (PRecord : forall v vs, P v -> Forall P vs -> P (vRecord v vs))
         (PSeq : forall vs, Forall P vs -> P (vSeq vs))
         p
         : P p.
Proof.
  induction p; auto; [ apply PRecord; [ apply IHp | ] | apply PSeq ];
    try solve [ induction l; [ apply Forall_nil | ];
                apply Forall_cons; [ apply value_ind'; try assumption | ];
                apply IHl ].
Defined.

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.

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.

Scheme Equality for label.

Fixpoint mat p v : bool :=
  let matseq := (fix matseq ps vs : bool :=
                   match ps, vs with
                   | [], [] => true
                   | (p :: ps'), (v :: vs') => andb (mat p v) (matseq ps' vs')
                   | _, _ => false
                   end) in
  match p with
  | pDiscard => true
  | pCapture p' => mat p' v
  | pBool b => match v with vBool b' => bool_beq b b' | _ => false end
  | pSymbol s => match v with vSymbol s' => label_beq s s' | _ => false end
  | pRecord p' ps => match v with vRecord v' vs => mat p' v' && matseq ps vs | _ => false end
  | pSeq ps => match v with vSeq vs => matseq ps vs | _ => false end
  end.

Fixpoint raw_v_to_p v : pat :=
  match v with
  | vBool b => pBool b
  | vSymbol s => pSymbol s
  | vRecord l fs => pRecord (raw_v_to_p l) (map raw_v_to_p fs)
  | vSeq vs => pSeq (map raw_v_to_p vs)
  end.

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

Fixpoint p_to_v p : value :=
  match p with
  | pDiscard => vRecord (vSymbol lDiscard) []
  | pCapture p' => vRecord (vSymbol lCapture) [p_to_v p']
  | pBool b => vBool b
  | pSymbol s => vSymbol s
  | pRecord (pSymbol lDiscard) [] => vRecord (vQuote (vSymbol lDiscard)) []
  | pRecord (pSymbol lCapture) [p'] => vRecord (vQuote (vSymbol lCapture)) [p_to_v p']
  | pRecord (pSymbol lQuote) [p'] => vRecord (vQuote (vSymbol lQuote)) [p_to_v p']
  | pRecord l ps => vRecord (p_to_v l) (map p_to_v ps)
  | pSeq ps => vSeq (map p_to_v ps)
  end.

Lemma Forall_map_map_id :
  forall A X xs (f : X -> A) (g : A -> X),
    Forall (fun x : X => g (f x) = x) xs ->
    (map g (map f xs)) = xs.
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 reflection_after_interpretation_sensible : forall p, v_to_p (p_to_v 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;
    apply Forall_map_map_id in H;
    destruct ps; simpl in H; inversion H; clear H; auto;
      destruct ps; simpl; repeat f_equal;
        try solve [ repeat rewrite H1; reflexivity
                  | inversion H2; repeat rewrite H0; repeat rewrite H3; reflexivity ].

  (* 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.

Theorem interpretation_after_reflection_not_sensible :
  exists v, p_to_v (v_to_p v) <> v.
Proof.
  exists (vQuote (vRecord (vSymbol lDiscard) [])).
  simpl; intro H; inversion H.
Qed.

Fixpoint escape v : value :=
  match v with
  | vBool b => vBool b
  | vSymbol s => vSymbol s
  | vRecord (vSymbol lDiscard) [] => vRecord (vQuote (vSymbol lDiscard)) []
  | vRecord (vSymbol lCapture) [v'] => vRecord (vQuote (vSymbol lCapture)) [escape v']
  | vRecord (vSymbol lQuote) [v'] => vRecord (vQuote (vSymbol lQuote)) [escape v']
  | vRecord l vs => vRecord (escape l) (map escape vs)
  | vSeq vs => vSeq (map escape vs)
  end.

Fixpoint unescape v : value :=
  match v with
  | vBool b => vBool b
  | vSymbol s => vSymbol s
  | vRecord (vSymbol lQuote) [v'] => v'
  | vRecord l vs => vRecord (unescape l) (map unescape vs)
  | vSeq vs => vSeq (map unescape vs)
  end.

Theorem unescape_after_escape_id : forall v, unescape (escape v) = v.
Proof.
  induction v using value_ind'; auto.

  destruct v; simpl; try rewrite <- IHv; try solve [ solve_map_map_id ].

  (* vRecord with a vSymbol label *)

  destruct l;
    apply Forall_map_map_id in H;
    destruct vs; simpl in H; inversion H; clear H; auto;
      destruct vs; simpl; repeat f_equal;
        try solve [ repeat rewrite H1; reflexivity
                  | inversion H2; repeat rewrite H0; repeat rewrite H3; reflexivity ].

  (* vRecord with a vRecord label *)

  destruct v; try solve_map_map_id;
    destruct l0; destruct l; try solve_map_map_id;
      destruct l; solve_map_map_id.

  (* vSeq *)

  destruct vs; inversion H; clear H;
    simpl; repeat rewrite H2; repeat rewrite H3; solve_map_map_id.
Qed.

Lemma Forall_map_map_assoc_id :
  forall A X Y ys (h : Y -> X) (f : X -> A) (g : A -> X),
    Forall (fun y : Y => g (f (h y)) = (h y)) ys ->
    map g (map f (map h ys)) = (map h ys).
Proof.
  intros; rewrite map_map; induction H; [ reflexivity | ].
  simpl; rewrite IHForall; rewrite H; reflexivity.
Qed.

Ltac solve_map_map_assoc_id := repeat f_equal; apply Forall_map_map_assoc_id; assumption.

Lemma escape_record_record_label :
  forall l inner outer,
    escape (vRecord (vRecord l inner) outer) = vRecord (escape (vRecord l inner)) (map escape outer).
Proof.
  reflexivity.
Qed.

Lemma Forall_map_map_raw :
  forall B A X xs (h : X -> A) (f : X -> B) (g : B -> A),
    Forall (fun x : X => (g (f x)) = (h x)) xs ->
    map g (map f xs) = (map h xs).
Proof.
  intros; rewrite map_map; induction H; [ reflexivity | ].
  simpl; rewrite IHForall; rewrite H; reflexivity.
Qed.

Lemma escaped_record_is_record :
  forall v l, exists l' v', escape (vRecord v l) = vRecord v' l'.
Proof.
  intros.
  exists (map escape l).
  remember v as x.
  induction x using value_ind'; try destruct l0; try destruct l; try destruct l;
    try solve [ exists v; subst; reflexivity
              | exists (vQuote (vSymbol lDiscard)); reflexivity
              | exists (vQuote (vSymbol lCapture)); reflexivity
              | exists (vQuote (vSymbol lQuote)); reflexivity
              | exists (escape (vRecord x vs)); reflexivity
              | exists (escape (vSeq vs)); reflexivity ].
Qed.

Lemma v_to_p_escaped_record_is_raw_v_to_p :
  forall v, v_to_p (escape v) = (raw_v_to_p v).
Proof.
  induction v using value_ind'; try reflexivity.

  destruct v.

  simpl; rewrite Forall_map_map_raw with (h := raw_v_to_p); auto.

  destruct l; destruct vs; simpl; inversion IHv; try reflexivity;
    (destruct vs; simpl; inversion H; rewrite H2; try reflexivity;
     inversion H3; rewrite H6;
     rewrite Forall_map_map_raw with (h := raw_v_to_p); auto).

  unfold raw_v_to_p; fold raw_v_to_p;
    (replace (pRecord (raw_v_to_p v) (map raw_v_to_p l)) with (raw_v_to_p (vRecord v l));
     [ | reflexivity ]);
    rewrite <- IHv;
    rewrite escape_record_record_label;
    (assert (exists (l' : list value) (v' : value), escape (vRecord v l) = vRecord v' l');
     [ apply escaped_record_is_record | ]);
    inversion_clear H0; inversion_clear H1;
      rewrite H0; rewrite <- Forall_map_map_raw with (f := escape) (g := v_to_p); auto.

  simpl; f_equal; [ apply IHv | ]; apply Forall_map_map_raw; assumption.

  simpl; f_equal; apply Forall_map_map_raw; assumption.
Qed.

Lemma p_to_v_of_raw_v_to_p_is_escape :
  forall v,
    p_to_v (raw_v_to_p v) = escape v.
Proof.
  induction v using value_ind'; try reflexivity.

  dependent induction v.
    (* unfold raw_v_to_p; fold raw_v_to_p; *)
    (*   unfold p_to_v; fold p_to_v. *)

  simpl; f_equal; f_equal; apply Forall_map_map_raw; assumption.

  destruct l; destruct vs; simpl; inversion IHv; try reflexivity;
    (destruct vs; simpl; inversion H; rewrite H2; try reflexivity;
     inversion H3; rewrite H6;
     rewrite Forall_map_map_raw with (h := escape); [ | assumption ]; reflexivity).

  destruct v; simpl; inversion IHv0; f_equal; f_equal;
    try solve [ apply Forall_map_map_raw; assumption ].

  simpl; inversion IHv;
    rewrite <- Forall_map_map_raw with (f := raw_v_to_p) (g := p_to_v); [ | assumption ]; reflexivity.

  inversion H; try reflexivity;
    simpl; rewrite H0;
      rewrite <- Forall_map_map_raw with (f := raw_v_to_p) (g := p_to_v); [ | assumption ]; reflexivity.
Qed.

Lemma interpretation_after_reflection_after_escape_sensible v : p_to_v (v_to_p (escape v)) = (escape v).
Proof.
  rewrite v_to_p_escaped_record_is_raw_v_to_p.
  apply p_to_v_of_raw_v_to_p_is_escape.
Qed.

Theorem unescape_interpretation_reflection_escape_sensible v : unescape (p_to_v (v_to_p (escape v))) = v.
Proof.
  rewrite interpretation_after_reflection_after_escape_sensible.
  apply unescape_after_escape_id.
Qed.

Fixpoint quotation_invariant v u : mat (v_to_p (escape v)) u = true <-> u = v.
Proof.
  destruct v;
    destruct u;
    rewrite v_to_p_escaped_record_is_raw_v_to_p;
    (split; intro Hlhs; [ | rewrite Hlhs ]);
    try solve [ simpl in * |- *; congruence ].

  apply internal_bool_dec_bl in Hlhs; congruence.
  apply internal_bool_dec_lb; reflexivity.

  apply internal_label_dec_bl in Hlhs; congruence.
  apply internal_label_dec_lb; reflexivity.

  simpl in Hlhs; symmetry in Hlhs; apply Bool.andb_true_eq in Hlhs; inversion_clear Hlhs.
  symmetry in H, H0.
  rewrite <- v_to_p_escaped_record_is_raw_v_to_p in H.
  rewrite quotation_invariant in H.
  subst u; f_equal.
  dependent induction l; dependent induction l0;
    try solve [ reflexivity
              | simpl in H0; congruence ].
  simpl in H0.
  simpl in H0; symmetry in H0; apply Bool.andb_true_eq in H0; inversion_clear H0.
  symmetry in H, H1.
  rewrite <- v_to_p_escaped_record_is_raw_v_to_p in H.
  rewrite quotation_invariant in H.
  subst a0; f_equal.
  apply IHl.
  assumption.

  simpl; apply andb_true_intro; rewrite <- v_to_p_escaped_record_is_raw_v_to_p; split.
  rewrite quotation_invariant; reflexivity.
  clear Hlhs; induction l; [ reflexivity | ].
  simpl; apply andb_true_intro; rewrite <- v_to_p_escaped_record_is_raw_v_to_p; split.
  rewrite quotation_invariant; reflexivity.
  apply IHl.

  dependent induction l; dependent induction l0;
    try solve [ reflexivity
              | simpl in Hlhs; congruence ].
  simpl in Hlhs.
  simpl in Hlhs; symmetry in Hlhs; apply Bool.andb_true_eq in Hlhs; inversion_clear Hlhs.
  symmetry in H, H0.
  rewrite <- v_to_p_escaped_record_is_raw_v_to_p in H.
  rewrite quotation_invariant in H.
  subst a0; f_equal.
  apply IHl in H0.
  congruence.

  clear Hlhs; induction l; [ reflexivity | ].
  simpl; apply andb_true_intro; rewrite <- v_to_p_escaped_record_is_raw_v_to_p; split.
  rewrite quotation_invariant; reflexivity.
  apply IHl.
Qed.