blog-static/code/dawn/DawnEval.v

179 lines
6.6 KiB
Coq
Raw Normal View History

Require Import Coq.Lists.List.
Require Import Dawn.
Require Import Coq.Program.Equality.
2021-11-27 14:17:09 -08:00
From Ltac2 Require Import Ltac2.
Inductive step_result :=
| err
| middle (e : expr) (s : list expr)
| final (s : list expr).
Fixpoint eval_step (s : list expr) (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 (e_quote v :: vs)
| e_int compose, (e_quote v2) :: (e_quote v1) :: vs => final (e_quote (e_comp v1 v2) :: vs)
| e_int apply, (e_quote v1) :: vs => middle v1 vs
| e_quote e', vs => final (e_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.
Definition strip_value_list (vs : value_stack) := @map value expr (@projT1 expr IsValue) vs.
Theorem eval_step_correct : forall (e : expr) (vs vs' : value_stack), Sem_expr vs e vs' ->
(eval_step (strip_value_list vs) e = final (strip_value_list vs')) \/
(exists (ei : expr) (vsi : value_stack),
eval_step (strip_value_list vs) e = middle ei (strip_value_list 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).
(* 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 (s : list expr) (e : expr) (s' : list expr) : Prop :=
| chain_final (P : eval_step s e = final s')
| chain_middle (ei : expr) (si : list expr)
(P : eval_step s e = middle ei si) (rest : eval_chain si ei s').
Lemma eval_chain_merge : forall (e1 e2 : expr) (s s' s'' : list expr),
eval_chain s e1 s' -> eval_chain s' e2 s'' -> eval_chain s (e_comp e1 e2) s''.
Proof.
intros e1 e2 s s' s'' ch1 ch2.
induction ch1;
eapply chain_middle; simpl; try (rewrite P); auto.
Qed.
Lemma eval_chain_split : forall (e1 e2 : expr) (s s'' : list expr),
eval_chain s (e_comp e1 e2) s'' -> exists s', (eval_chain s e1 s') /\ (eval_chain s' e2 s'').
Proof.
intros e1 e2 s ss'' ch.
2021-11-27 14:17:09 -08:00
ltac1:(dependent induction ch).
- simpl in P. destruct (eval_step s e1); inversion P.
- simpl in P. destruct (eval_step s 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 (strip_value_list vs) e (strip_value_list vs')
with eval_step_int : forall (i : intrinsic) (vs vs' : value_stack),
Sem_int vs i vs' -> eval_chain (strip_value_list vs) (e_int i) (strip_value_list 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 compoition, 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 with (strip_value_list vs2); auto.
- 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 (strip_value_list vs0); auto.
Qed.
Theorem eval_step_sem_back : forall (e : expr) (vs vs' : value_stack),
2021-11-27 14:17:09 -08:00
eval_chain (strip_value_list vs) e (strip_value_list vs') -> Sem_expr vs e vs'.
Proof.
2021-11-27 14:17:09 -08:00
(* Thoughts: the issue is with the apparent nondeterminism of evalution. *)
Admitted.
2021-11-27 14:17:09 -08:00
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.
2021-11-27 14:17:09 -08:00
Ltac2 destruct_int_stack (int : constr) (va: constr) := destruct_n (int_arity int) va.
Ltac2 ensure_valid_value_stack () := Control.enter (fun () =>
match! goal with
| [h : eval_step (strip_value_list ?a) (e_int ?b) = ?c |- _] =>
let h := Control.hyp h in
destruct_int_stack b a;
try (inversion $h; fail)
| [|- _ ] => ()
end).
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 (s s': list expr), eval_step s (e_int swap) = final s' ->
exists v1 v2 s'', s = v1 :: v2 :: s'' /\ s' = v2 :: v1 :: s''.
Proof.
2021-11-27 14:17:09 -08:00
intros s s' Heq.
ensure_valid_stack ().
simpl in Heq. injection Heq as Hinj. subst. eauto.
Qed.
Require Extraction.
Require Import ExtrHaskellBasic.
Extraction Language Haskell.
2021-11-27 14:17:09 -08:00
Extraction "UccGen.hs" expr eval_step true false or.