255 lines
9.7 KiB
Coq
255 lines
9.7 KiB
Coq
Require Import Coq.Lists.List.
|
|
Require Import DawnV2.
|
|
Require Import Coq.Program.Equality.
|
|
From Ltac2 Require Import Ltac2.
|
|
|
|
Inductive step_result :=
|
|
| err
|
|
| middle (e : expr) (s : value_stack)
|
|
| final (s : value_stack).
|
|
|
|
Fixpoint eval_step (s : value_stack) (e : expr) : step_result :=
|
|
match e, s with
|
|
| e_int swap, v' :: v :: vs => final (v :: v' :: vs)
|
|
| e_int clone, v :: vs => final (v :: v :: vs)
|
|
| e_int drop, v :: vs => final vs
|
|
| e_int quote, v :: vs => final (v_quote (value_to_expr v) :: vs)
|
|
| e_int compose, (v_quote v2) :: (v_quote v1) :: vs => final (v_quote (e_comp v1 v2) :: vs)
|
|
| e_int apply, (v_quote v1) :: vs => middle v1 vs
|
|
| e_quote e', vs => final (v_quote e' :: vs)
|
|
| e_comp e1 e2, vs =>
|
|
match eval_step vs e1 with
|
|
| final vs' => middle e2 vs'
|
|
| middle e1' vs' => middle (e_comp e1' e2) vs'
|
|
| err => err
|
|
end
|
|
| _, _ => err
|
|
end.
|
|
|
|
Theorem eval_step_correct : forall (e : expr) (vs vs' : value_stack), Sem_expr vs e vs' ->
|
|
(eval_step vs e = final vs') \/
|
|
(exists (ei : expr) (vsi : value_stack),
|
|
eval_step vs e = middle ei vsi /\
|
|
Sem_expr vsi ei vs').
|
|
Proof.
|
|
intros e vs vs' Hsem.
|
|
(* Proceed by induction on the semantics. *)
|
|
induction Hsem.
|
|
- inversion H; (* The expression is just an intrnsic. *)
|
|
(* Dismiss all the straightforward "final" cases,
|
|
of which most intrinsics are. *)
|
|
try (left; reflexivity).
|
|
(* Only apply remains; We are in an intermediate / middle case. *)
|
|
right.
|
|
(* The semantics guarantee that the expression in the
|
|
quote evaluates to the final state. *)
|
|
exists e, vs0. auto.
|
|
- (* The expression is a quote. This is yet another final case. *)
|
|
left; reflexivity.
|
|
- (* The composition is never a final step, since we have to evaluate both
|
|
branches to "finish up". *)
|
|
destruct IHHsem1; right.
|
|
+ (* If the left branch finihed, only the right branch needs to be evaluted. *)
|
|
simpl. rewrite H. exists e2, vs2. auto.
|
|
+ (* Otherwise, the left branch has an intermediate evaluation, guaranteed
|
|
by induction to be consitent. *)
|
|
destruct H as [ei [vsi [Heval Hsem']]].
|
|
(* We compose the remaining part of the left branch with the right branch. *)
|
|
exists (e_comp ei e2), vsi. simpl.
|
|
(* The evaluation is trivially to a "middle" state. *)
|
|
rewrite Heval. split. auto.
|
|
eapply Sem_e_comp. apply Hsem'. apply Hsem2.
|
|
Qed.
|
|
|
|
Inductive eval_chain (vs : value_stack) (e : expr) (vs' : value_stack) : Prop :=
|
|
| chain_final (P : eval_step vs e = final vs')
|
|
| chain_middle (ei : expr) (vsi : value_stack)
|
|
(P : eval_step vs e = middle ei vsi) (rest : eval_chain vsi ei vs').
|
|
|
|
Lemma eval_chain_merge : forall (e1 e2 : expr) (vs vs' vs'' : value_stack),
|
|
eval_chain vs e1 vs' -> eval_chain vs' e2 vs'' -> eval_chain vs (e_comp e1 e2) vs''.
|
|
Proof.
|
|
intros e1 e2 vs vs' vs'' ch1 ch2.
|
|
induction ch1;
|
|
eapply chain_middle; simpl; try (rewrite P); auto.
|
|
Qed.
|
|
|
|
Lemma eval_chain_split : forall (e1 e2 : expr) (vs vs'' : value_stack),
|
|
eval_chain vs (e_comp e1 e2) vs'' -> exists vs', (eval_chain vs e1 vs') /\ (eval_chain vs' e2 vs'').
|
|
Proof.
|
|
intros e1 e2 vs vss'' ch.
|
|
ltac1:(dependent induction ch).
|
|
- simpl in P. destruct (eval_step vs e1); inversion P.
|
|
- simpl in P. destruct (eval_step vs e1) eqn:Hval; try (inversion P).
|
|
+ injection P as Hinj; subst. specialize (IHch e e2 H0) as [s'0 [ch1 ch2]].
|
|
eexists. split.
|
|
* eapply chain_middle. apply Hval. apply ch1.
|
|
* apply ch2.
|
|
+ subst. eexists. split.
|
|
* eapply chain_final. apply Hval.
|
|
* apply ch.
|
|
Qed.
|
|
|
|
Theorem val_step_sem : forall (e : expr) (vs vs' : value_stack),
|
|
Sem_expr vs e vs' -> eval_chain vs e vs'
|
|
with eval_step_int : forall (i : intrinsic) (vs vs' : value_stack),
|
|
Sem_int vs i vs' -> eval_chain vs (e_int i) vs'.
|
|
Proof.
|
|
- intros e vs vs' Hsem.
|
|
induction Hsem.
|
|
+ (* This is an intrinsic, which is handled by the second
|
|
theorem, eval_step_int. This lemma is used here. *)
|
|
auto.
|
|
+ (* A quote doesn't have a next step, and so is final. *)
|
|
apply chain_final. auto.
|
|
+ (* In composition, by induction, we know that the two sub-expressions produce
|
|
proper evaluation chains. Chains can be composed (via eval_chain_merge). *)
|
|
eapply eval_chain_merge; eauto.
|
|
- intros i vs vs' Hsem.
|
|
(* The evaluation chain depends on the specific intrinsic in use. *)
|
|
inversion Hsem; subst;
|
|
(* Most intrinsics produce a final value, and the evaluation chain is trivial. *)
|
|
try (apply chain_final; auto; fail).
|
|
(* Only apply is non-final. The first step is popping the quote from the stack,
|
|
and the rest of the steps are given by the evaluation of the code in the quote. *)
|
|
apply chain_middle with e vs0; auto.
|
|
Qed.
|
|
|
|
Ltac2 Type exn ::= [ | Not_intrinsic ].
|
|
|
|
Ltac2 rec destruct_n (n : int) (vs : constr) : unit :=
|
|
if Int.le n 0 then () else
|
|
let v := Fresh.in_goal @v in
|
|
let vs' := Fresh.in_goal @vs in
|
|
destruct $vs as [|$v $vs']; Control.enter (fun () =>
|
|
try (destruct_n (Int.sub n 1) (Control.hyp vs'))
|
|
).
|
|
|
|
Ltac2 int_arity (int : constr) : int :=
|
|
match! int with
|
|
| swap => 2
|
|
| clone => 1
|
|
| drop => 1
|
|
| quote => 1
|
|
| compose => 2
|
|
| apply => 1
|
|
| _ => Control.throw Not_intrinsic
|
|
end.
|
|
|
|
Ltac2 destruct_int_stack (int : constr) (va: constr) := destruct_n (int_arity int) va.
|
|
|
|
Ltac2 ensure_valid_stack () := Control.enter (fun () =>
|
|
match! goal with
|
|
| [h : eval_step ?a (e_int ?b) = ?c |- _] =>
|
|
let h := Control.hyp h in
|
|
destruct_int_stack b a;
|
|
try (inversion $h; fail)
|
|
| [|- _ ] => ()
|
|
end).
|
|
|
|
Theorem test : forall (vs vs': value_stack), eval_step vs (e_int swap) = final vs' ->
|
|
exists v1 v2 vs'', vs = v1 :: v2 :: vs'' /\ vs' = v2 :: v1 :: vs''.
|
|
Proof.
|
|
intros s s' Heq.
|
|
ensure_valid_stack ().
|
|
simpl in Heq. injection Heq as Hinj. subst. eauto.
|
|
Qed.
|
|
|
|
Theorem eval_step_final_sem : forall (e : expr) (vs vs' : value_stack),
|
|
eval_step vs e = final vs' -> Sem_expr vs e vs'.
|
|
Proof.
|
|
intros e vs vs' Hev. destruct e.
|
|
- destruct i; ensure_valid_stack ();
|
|
(* Get rid of trivial cases that match one-to-one. *)
|
|
simpl in Hev; try (injection Hev as Hinj; subst; solve_basic ()).
|
|
+ (* compose with one quoted value is not final, but an error. *)
|
|
destruct v. inversion Hev.
|
|
+ (* compose with two quoted values. *)
|
|
destruct v; destruct v0.
|
|
injection Hev as Hinj; subst; solve_basic ().
|
|
+ (* Apply is not final. *) destruct v. inversion Hev.
|
|
- (* Quote is always final, trivially, and the semantics match easily. *)
|
|
simpl in Hev. injection Hev as Hinj; subst. solve_basic ().
|
|
- (* Compose is never final, so we don't need to handle it here. *)
|
|
simpl in Hev. destruct (eval_step vs e1); inversion Hev.
|
|
Qed.
|
|
|
|
Theorem eval_step_middle_sem : forall (e ei: expr) (vs vsi vs' : value_stack),
|
|
eval_step vs e = middle ei vsi ->
|
|
Sem_expr vsi ei vs' ->
|
|
Sem_expr vs e vs'.
|
|
Proof.
|
|
intros e. induction e; intros ei vs vsi vs' Hev Hsem.
|
|
- destruct i; ensure_valid_stack ().
|
|
+ (* compose with one quoted value; invalid. *)
|
|
destruct v. inversion Hev.
|
|
+ (* compose with two quoted values; not a middle step. *)
|
|
destruct v; destruct v0. inversion Hev.
|
|
+ (* Apply *)
|
|
destruct v. injection Hev as Hinj; subst.
|
|
solve_basic (). auto.
|
|
- (* quoting an expression is not middle. *)
|
|
inversion Hev.
|
|
- simpl in Hev.
|
|
destruct (eval_step vs e1) eqn:Hev1.
|
|
+ (* Step led to an error, which can't happen in a chain. *)
|
|
inversion Hev.
|
|
+ (* Left expression makes a non-final step. Milk this for equalities first. *)
|
|
injection Hev as Hinj; subst.
|
|
(* The rest of the program (e_comp e e2) evaluates using our semantics,
|
|
which means that both e and e2 evaluate using our semantics. *)
|
|
inversion Hsem; subst.
|
|
(* By induction, e1 evaluates using our semantics if e does, which we just confirmed. *)
|
|
specialize (IHe1 e vs vsi vs2 Hev1 H2).
|
|
(* The composition rule can now be applied. *)
|
|
eapply Sem_e_comp; eauto.
|
|
+ (* Left expression makes a final step. Milk this for equalities first. *)
|
|
injection Hev as Hinj; subst.
|
|
(* Using eval_step_final, we know that e1 evaluates to the intermediate
|
|
state given our semantics. *)
|
|
specialize (eval_step_final_sem e1 vs vsi Hev1) as Hsem1.
|
|
(* The composition rule can now be applied. *)
|
|
eapply Sem_e_comp; eauto.
|
|
Qed.
|
|
|
|
Theorem eval_step_sem_back : forall (e : expr) (vs vs' : value_stack),
|
|
eval_chain vs e vs' -> Sem_expr vs e vs'.
|
|
Proof.
|
|
intros e vs vs' ch.
|
|
ltac1:(dependent induction ch).
|
|
- apply eval_step_final_sem. auto.
|
|
- specialize (eval_step_middle_sem e ei vs vsi vs' P IHch). auto.
|
|
Qed.
|
|
|
|
Corollary eval_step_no_sem : forall (e : expr) (vs vs' : value_stack),
|
|
~(Sem_expr vs e vs') -> ~(eval_chain vs e vs').
|
|
Proof.
|
|
intros e vs vs' Hnsem Hch.
|
|
specialize (eval_step_sem_back _ _ _ Hch). auto.
|
|
Qed.
|
|
|
|
Require Extraction.
|
|
Require Import ExtrHaskellBasic.
|
|
Extraction Language Haskell.
|
|
Set Extraction KeepSingleton.
|
|
Extraction "UccGen.hs" expr eval_step true false or.
|
|
|
|
Remark eval_swap_two_values : forall (vs vs' : value_stack),
|
|
eval_step vs (e_int swap) = final vs' -> exists v1 v2 vst, vs = v1 :: v2 :: vst /\ vs' = v2 :: v1 :: vst.
|
|
Proof.
|
|
intros vs vs' Hev.
|
|
(* Can't proceed until we know more about the stack. *)
|
|
destruct vs as [|v1 [|v2 vs]].
|
|
- (* Invalid case; empty stack. *) inversion Hev.
|
|
- (* Invalid case; stack only has one value. *) inversion Hev.
|
|
- (* Valid case: the stack has two values. *) injection Hev. eauto.
|
|
Qed.
|
|
|
|
Remark eval_swap_two_values' : forall (vs vs' : value_stack),
|
|
eval_step vs (e_int swap) = final vs' -> exists v1 v2 vst, vs = v1 :: v2 :: vst /\ vs' = v2 :: v1 :: vst.
|
|
Proof.
|
|
intros vs vs' Hev.
|
|
ensure_valid_stack ().
|
|
injection Hev. eauto.
|
|
Qed.
|