From 85c98a21b11f4381645b1064aa88177c04746282 Mon Sep 17 00:00:00 2001 From: davidhadhazi Date: Thu, 23 Jan 2025 18:02:04 +0100 Subject: [PATCH 1/2] feat: primop_eval change --- src/Auxiliaries.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Auxiliaries.v b/src/Auxiliaries.v index 785be1d..3b0cfed 100644 --- a/src/Auxiliaries.v +++ b/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 From 13ce0dbb69192d818df5557b9ec078c3a254d003 Mon Sep 17 00:00:00 2001 From: davidhadhazi Date: Thu, 23 Jan 2025 18:13:19 +0100 Subject: [PATCH 2/2] fix: subst lemma changes --- src/FrameStack/SubstSemanticsLemmas.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/FrameStack/SubstSemanticsLemmas.v b/src/FrameStack/SubstSemanticsLemmas.v index 3defcce..432e230 100644 --- a/src/FrameStack/SubstSemanticsLemmas.v +++ b/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.