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.