Use a different representation of values and prove equivalence of UCC evalutor

code/dawn/DawnEval.v

@@ -1,22 +1,22 @@
 Require Import Coq.Lists.List.
-Require Import Dawn.
+Require Import DawnV2.
 Require Import Coq.Program.Equality.
 From Ltac2 Require Import Ltac2.
 
 Inductive step_result :=
   | err
-  | middle (e : expr) (s : list expr)
-  | final (s : list expr).
+  | middle (e : expr) (s : value_stack)
+  | final (s : value_stack).
 
-Fixpoint eval_step (s : list expr) (e : expr) : step_result :=
+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 (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_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'
@@ -26,12 +26,10 @@ Fixpoint eval_step (s : list expr) (e : expr) : step_result :=
   | _, _ => 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')) \/
+  (eval_step vs e = final vs') \/
   (exists (ei : expr) (vsi : value_stack),
-    eval_step (strip_value_list vs) e = middle ei (strip_value_list vsi) /\
+    eval_step vs e = middle ei vsi /\
     Sem_expr vsi ei vs').
 Proof.
   intros e vs vs' Hsem.
@@ -39,9 +37,9 @@ Proof.
   induction Hsem.
   - inversion H; (* The expression is just an intrnsic. *)
     (* Dismiss all the straightforward "final" cases,
-       of which most intrinsics are *)
+       of which most intrinsics are. *)
     try (left; reflexivity).
-    (* We are in an intermediate / middle case. *)
+    (* 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. *)
@@ -63,26 +61,26 @@ Proof.
       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').
+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) (s s' s'' : list expr),
-  eval_chain s e1 s' -> eval_chain s' e2 s'' -> eval_chain s (e_comp e1 e2) s''.
+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 s s' s'' ch1 ch2.
+  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) (s s'' : list expr),
-  eval_chain s (e_comp e1 e2) s'' -> exists s', (eval_chain s e1 s') /\ (eval_chain s' e2 s'').
+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 s ss'' ch.
+  intros e1 e2 vs vss'' ch.
   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).
+  - 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.
@@ -93,9 +91,9 @@ Proof.
 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')
+  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 (strip_value_list vs) (e_int i) (strip_value_list vs').
+  Sem_int vs i vs' -> eval_chain vs (e_int i) vs'.
 Proof.
   - intros e vs vs' Hsem.
     induction Hsem.
@@ -106,7 +104,7 @@ Proof.
       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.
+      eapply eval_chain_merge with vs2; auto.
   - intros i vs vs' Hsem.
     (* The evaluation chain depends on the specific intrinsic in use. *)
     inversion Hsem; subst;
@@ -114,15 +112,9 @@ Proof.
     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.
+    apply chain_middle with e vs0; auto.
 Qed.
 
-Theorem eval_step_sem_back : forall (e : expr) (vs vs' : value_stack),
-  eval_chain (strip_value_list vs) e (strip_value_list vs') -> Sem_expr vs e vs'.
-Proof.
-  (* Thoughts: the issue is with the apparent nondeterminism of evalution. *)
-Admitted.
-
 Ltac2 Type exn ::= [ | Not_intrinsic ].
 
 Ltac2 rec destruct_n (n : int) (vs : constr) : unit :=
@@ -146,15 +138,6 @@ Ltac2 int_arity (int : constr) : int :=
 
 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 |- _] =>
@@ -164,15 +147,77 @@ Ltac2 ensure_valid_stack () := Control.enter (fun () =>
   | [|- _ ] => ()
   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''.
+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 *)
+      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. *)
+    simpl in Hev. injection Hev as Hinj; subst. solve_basic ().
+  - (* Compose is never final. *)
+    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. *)
+      destruct v. inversion Hev.
+    + (* compose with two quoted values. *)
+      destruct v; destruct v0. inversion Hev.
+    + (* Apply *)
+      destruct v. injection Hev as Hinj; subst.
+      solve_basic (). auto.
+  - inversion Hev.
+  - simpl in Hev.
+    destruct (eval_step vs e1) eqn:Hev1.
+    + inversion Hev.
+    + injection Hev as Hinj; subst. inversion Hsem; subst.
+      specialize (IHe1 e vs vsi vs2 Hev1 H2).
+      eapply Sem_e_comp. apply IHe1. apply H4.
+    + injection Hev as Hinj; subst.
+      specialize (eval_step_final_sem e1 vs vsi Hev1) as Hsem1.
+      eapply Sem_e_comp. apply Hsem1. apply Hsem.
+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.