Merge pull request #38 from harp-project/david-primop_eval-change

Primop eval change

src/Auxiliaries.v

@@ -513,18 +513,18 @@ match convert_primop_to_code fname with
 end.
 
 (** Simulated primary operations *)
-Definition primop_eval (fname : string) (params : list Val) (eff : SideEffectList) : option (Redex * SideEffectList) :=
+Definition primop_eval (fname : string) (params : list Val) (eff : SideEffectList) : option (Redex * (option SideEffect)) :=
 match convert_primop_to_code fname with
   | PMatchFail | PRaise =>
     match (eval_primop_error fname params) with
-    | Some exc => Some (RExc exc, eff)
+    | Some exc => Some (RExc exc, None)
     | None => None (* this is a compile-time error *)
     end
 (** These are concurrent primops: *)
   | PRecvNext | PRemoveMsg | PPeekMsg
   | PRecvWaitTimeout => None
 (***)
-  | _ => Some (RExc (undef (VLit (Atom fname))), eff)
+  | _ => Some (RExc (undef (VLit (Atom fname))), None)
 end.
 
 (** Function info of Core Erlang. We depend on this info when we argue about

src/FrameStack/SubstSemanticsLemmas.v

@@ -68,7 +68,7 @@ Proof.
     eapply closed_eval; try eassumption. eauto.
   * destruct (primop_eval f vl []) eqn: a.
     - inv Heq. destruct p. inv H0.
-      eapply (closed_primop_eval f vl [] r0 s Hall).
+      eapply (closed_primop_eval f vl [] r0 o Hall).
       assumption.
     - inv Heq.
   * inversion Hi; subst; clear Hi. destruct v; unfold badfun; try invSome.
@@ -407,7 +407,7 @@ Proof.
   1: left; destruct m, f; try destruct l; try destruct l0; try invSome; try constructor; inv H; scope_solver.
   1: symmetry in H1; eapply eval_is_result in H1; auto.
   * left. destruct (primop_eval f vl []) eqn: pe.
-    - destruct p. inv H1. apply (primop_eval_is_result f vl [] r0 s H0 pe).
+    - destruct p. inv H1. apply (primop_eval_is_result f vl [] r0 o H0 pe).
     - inv H1.
   * inv H. destruct v; try invSome; try now (left; constructor; auto).
     break_match_hyp; invSome; auto.