119 lines
3.6 KiB
Coq
119 lines
3.6 KiB
Coq
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.
|