From 3be67ca4c8392da945d756e952dd804a661dd7e1 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 3 Nov 2024 16:05:04 -0800 Subject: [PATCH] Use unification-based 'eq' for numbers and symbols Signed-off-by: Danila Fedorin --- content/blog/05_spa_agda_semantics/index.md | 23 ++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) diff --git a/content/blog/05_spa_agda_semantics/index.md b/content/blog/05_spa_agda_semantics/index.md index 3ce4778..944fa17 100644 --- a/content/blog/05_spa_agda_semantics/index.md +++ b/content/blog/05_spa_agda_semantics/index.md @@ -285,6 +285,9 @@ the exact rules that were used in computing a particular value. The variables `x`, `y`, and `z` are pre-defined for your convenience. {{< bergamot_widget id="expr-widget" query="" prompt="eval(extend(extend(extend(empty, x, 17), y, 42), z, 0), TERM, ?v)" modes="Expression:Expression" >}} +hidden section "" { + Eq @ eq(?x, ?x) <-; +} section "" { EvalNum @ eval(?rho, lit(?n), ?n) <- int(?n); EvalVar @ eval(?rho, var(?x), ?v) <- inenv(?x, ?v, ?rho); @@ -295,7 +298,7 @@ section "" { } hidden section "" { EnvTake @ inenv(?x, ?v, extend(?rho, ?x, ?v)) <-; - EnvSkip @ inenv(?x, ?v_1, extend(?rho, ?y, ?v_2)) <- inenv(?x, ?v_1, ?rho), not(symeq(?x, ?y)); + EnvSkip @ inenv(?x, ?v_1, extend(?rho, ?y, ?v_2)) <- inenv(?x, ?v_1, ?rho), not(eq(?x, ?y)); } {{< /bergamot_widget >}} @@ -349,6 +352,9 @@ a Bergamot instance, this time with simple statements. Try out `noop` or some sort of variable assignment, like `x = x + 1`. {{< bergamot_widget id="basic-stmt-widget" query="" prompt="stepbasic(extend(extend(extend(empty, x, 17), y, 42), z, 0), TERM, ?env)" modes="Basic Statement:Basic Statement" >}} +hidden section "" { + Eq @ eq(?x, ?x) <-; +} hidden section "" { EvalNum @ eval(?rho, lit(?n), ?n) <- int(?n); EvalVar @ eval(?rho, var(?x), ?v) <- inenv(?x, ?v, ?rho); @@ -363,7 +369,7 @@ section "" { } hidden section "" { EnvTake @ inenv(?x, ?v, extend(?rho, ?x, ?v)) <-; - EnvSkip @ inenv(?x, ?v_1, extend(?rho, ?y, ?v_2)) <- inenv(?x, ?v_1, ?rho), not(symeq(?x, ?y)); + EnvSkip @ inenv(?x, ?v_1, extend(?rho, ?y, ?v_2)) <- inenv(?x, ?v_1, ?rho), not(eq(?x, ?y)); } {{< /bergamot_widget >}} @@ -420,6 +426,9 @@ The rule for evaluating a conditional with a "false" branch is very similar. {{< /latex >}} {{< bergamot_widget id="stmt-widget" query="" prompt="step(extend(extend(extend(empty, x, 17), y, 42), z, 0), TERM, ?env)" modes="Statement:Statement" >}} +hidden section "" { + Eq @ eq(?x, ?x) <-; +} hidden section "" { EvalNum @ eval(?rho, lit(?n), ?n) <- int(?n); EvalVar @ eval(?rho, var(?x), ?v) <- inenv(?x, ?v, ?rho); @@ -440,14 +449,14 @@ hidden section "" { StepLiftBasic @ step(?rho_1, ?s, ?rho_2) <- stepbasic(?rho_1, ?s, ?rho_2); } section "" { - StepIfTrue @ step(?rho_1, if(?e, ?s_1, ?s_2), ?rho_2) <- eval(?rho_1, ?e, ?v), not(numeq(?v, 0)), step(?rho_1, ?s_1, ?rho_2); - StepIfFalse @ step(?rho_1, if(?e, ?s_1, ?s_2), ?rho_2) <- eval(?rho_1, ?e, ?v), numeq(?v, 0), step(?rho_1, ?s_2, ?rho_2); - StepWhileTrue @ step(?rho_1, while(?e, ?s), ?rho_3) <- eval(?rho_1, ?e, ?v), not(numeq(?v, 0)), step(?rho_1, ?s, ?rho_2), step(?rho_2, while(?e, ?s), ?rho_3); - StepWhileFalse @ step(?rho_1, while(?e, ?s), ?rho_1) <- eval(?rho_1, ?e, ?v), numeq(?v, 0); + StepIfTrue @ step(?rho_1, if(?e, ?s_1, ?s_2), ?rho_2) <- eval(?rho_1, ?e, ?v), not(eq(?v, 0)), step(?rho_1, ?s_1, ?rho_2); + StepIfFalse @ step(?rho_1, if(?e, ?s_1, ?s_2), ?rho_2) <- eval(?rho_1, ?e, ?v), eq(?v, 0), step(?rho_1, ?s_2, ?rho_2); + StepWhileTrue @ step(?rho_1, while(?e, ?s), ?rho_3) <- eval(?rho_1, ?e, ?v), not(eq(?v, 0)), step(?rho_1, ?s, ?rho_2), step(?rho_2, while(?e, ?s), ?rho_3); + StepWhileFalse @ step(?rho_1, while(?e, ?s), ?rho_1) <- eval(?rho_1, ?e, ?v), eq(?v, 0); StepSeq @ step(?rho_1, seq(?s_1, ?s_2), ?rho_3) <- step(?rho_1, ?s_1, ?rho_2), step(?rho_2, ?s_2, ?rho_3); } hidden section "" { EnvTake @ inenv(?x, ?v, extend(?rho, ?x, ?v)) <-; - EnvSkip @ inenv(?x, ?v_1, extend(?rho, ?y, ?v_2)) <- inenv(?x, ?v_1, ?rho), not(symeq(?x, ?y)); + EnvSkip @ inenv(?x, ?v_1, extend(?rho, ?y, ?v_2)) <- inenv(?x, ?v_1, ?rho), not(eq(?x, ?y)); } {{< /bergamot_widget >}}