From 7433e6e5f7fdc8d2434e476ef884e1ea191e907b Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Thu, 24 Feb 2022 11:30:23 -0600 Subject: [PATCH] WIP --- prototyping/Interpreter.agda | 2 +- prototyping/Properties/Step.agda | 20 ++++++++++---------- prototyping/Properties/StrictMode.agda | 14 +++++++------- 3 files changed, 18 insertions(+), 18 deletions(-) diff --git a/prototyping/Interpreter.agda b/prototyping/Interpreter.agda index b9ff03c4..da8f15e6 100644 --- a/prototyping/Interpreter.agda +++ b/prototyping/Interpreter.agda @@ -24,7 +24,7 @@ runBlock : ∀ {a} → Block a → IO ⊤ runBlock block with run block runBlock block | return V D = putStrLn (valueToString V) runBlock block | done D = putStrLn "nil" -runBlock block | error E D = putStrLn (errToStringᴮ E) +runBlock block | error E D = putStrLn (errToStringᴮ _ E) runJSON : Value → IO ⊤ runJSON value with blockFromJSON(value) diff --git a/prototyping/Properties/Step.agda b/prototyping/Properties/Step.agda index 924c2912..9cb43f9e 100644 --- a/prototyping/Properties/Step.agda +++ b/prototyping/Properties/Step.agda @@ -32,7 +32,7 @@ stepᴱ : ∀ {a} H M → StepResultᴱ {a} H M stepᴮ : ∀ {a} H B → StepResultᴮ {a} H B stepᴱ H nil = value nil refl -stepᴱ H (var x) = error (UnboundVariable x) +stepᴱ H (var x) = error UnboundVariable stepᴱ H (addr a) = value (addr a) refl stepᴱ H (number x) = value (number x) refl stepᴱ H (M $ N) with stepᴱ H M @@ -40,17 +40,17 @@ stepᴱ H (M $ N) | step H′ M′ D = step H′ (M′ $ N) (app₁ D) stepᴱ H (_ $ N) | value v refl with stepᴱ H N stepᴱ H (_ $ N) | value v refl | step H′ N′ s = step H′ (val v $ N′) (app₂ v s) stepᴱ H (_ $ _) | value (addr a) refl | value w refl with remember (H [ a ]) -stepᴱ H (_ $ _) | value (addr a) refl | value w refl | (nothing , p) = error (app₁ (SEGV a p)) +stepᴱ H (_ $ _) | value (addr a) refl | value w refl | (nothing , p) = error (app₁ (SEGV p)) stepᴱ H (_ $ _) | value (addr a) refl | value w refl | (just(function F is B end) , p) = step H (block (fun F) is B [ w / name (arg F) ]ᴮ end) (beta function F is B end w refl p) -stepᴱ H (_ $ _) | value nil refl | value w refl = error (FunctionMismatch nil w refl refl (λ ())) -stepᴱ H (_ $ _) | value (number x) refl | value w refl = error (FunctionMismatch (number x) w refl refl (λ ())) +stepᴱ H (_ $ _) | value nil refl | value w refl = error (FunctionMismatch nil w (λ ())) +stepᴱ H (_ $ _) | value (number x) refl | value w refl = error (FunctionMismatch (number x) w (λ ())) stepᴱ H (M $ N) | value V p | error E = error (app₂ E) stepᴱ H (M $ N) | error E = error (app₁ E) stepᴱ H (block b is B end) with stepᴮ H B stepᴱ H (block b is B end) | step H′ B′ D = step H′ (block b is B′ end) (block D) stepᴱ H (block b is (return _ ∙ B′) end) | return v refl = step H (val v) (return v) stepᴱ H (block b is done end) | done refl = step H nil done -stepᴱ H (block b is B end) | error E = error (block b E) +stepᴱ H (block b is B end) | error E = error (block E) stepᴱ H (function F is C end) with alloc H (function F is C end) stepᴱ H function F is C end | ok a H′ p = step H′ (addr a) (function a p) stepᴱ H (binexp M op N) with stepᴱ H M @@ -58,10 +58,10 @@ stepᴱ H (binexp M op N) | value v refl with stepᴱ H N stepᴱ H (binexp M op N) | value v refl | step H′ N′ s = step H′ (binexp (val v) op N′) (binOp₂ s) stepᴱ H (binexp M op N) | value v refl | error E = error (bin₂ E) stepᴱ H (binexp M op N) | value (number m) refl | value (number n) refl = step H (number (evalBinOp m op n)) binOpEval -stepᴱ H (binexp M op N) | value nil refl | value w refl = error (BinopMismatch₁ op nil w refl refl λ ()) -stepᴱ H (binexp M op N) | value (addr a) refl | value w refl = error (BinopMismatch₁ op (addr a) w refl refl λ ()) -stepᴱ H (binexp M op N) | value v refl | value nil refl = error (BinopMismatch₂ op v nil refl refl (λ ())) -stepᴱ H (binexp M op N) | value v refl | value (addr a) refl = error (BinopMismatch₂ op v (addr a) refl refl (λ ())) +stepᴱ H (binexp M op N) | value nil refl | value w refl = error (BinopMismatch₁ nil w λ ()) +stepᴱ H (binexp M op N) | value (addr a) refl | value w refl = error (BinopMismatch₁ (addr a) w λ ()) +stepᴱ H (binexp M op N) | value v refl | value nil refl = error (BinopMismatch₂ v nil (λ ())) +stepᴱ H (binexp M op N) | value v refl | value (addr a) refl = error (BinopMismatch₂ v (addr a) (λ ())) stepᴱ H (binexp M op N) | step H′ M′ s = step H′ (binexp M′ op N) (binOp₁ s) stepᴱ H (binexp M op N) | error E = error (bin₁ E) @@ -70,7 +70,7 @@ stepᴮ H (function F is C end ∙ B) | ok a H′ p = step H′ (B [ addr a / na stepᴮ H (local x ← M ∙ B) with stepᴱ H M stepᴮ H (local x ← M ∙ B) | step H′ M′ D = step H′ (local x ← M′ ∙ B) (local D) stepᴮ H (local x ← _ ∙ B) | value v refl = step H (B [ v / name x ]ᴮ) (subst v) -stepᴮ H (local x ← M ∙ B) | error E = error (local x E) +stepᴮ H (local x ← M ∙ B) | error E = error (local E) stepᴮ H (return M ∙ B) with stepᴱ H M stepᴮ H (return M ∙ B) | step H′ M′ D = step H′ (return M′ ∙ B) (return D) stepᴮ H (return _ ∙ B) | value V refl = return V refl diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index bff23061..8281ecd7 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -366,18 +366,18 @@ reflect* H B (step s t) W = reflectᴴᴮ H B s (reflect* _ _ t W) runtimeWarningᴱ : ∀ H M → RuntimeErrorᴱ H M → Warningᴱ H (typeCheckᴱ H ∅ M) runtimeWarningᴮ : ∀ H B → RuntimeErrorᴮ H B → Warningᴮ H (typeCheckᴮ H ∅ B) -runtimeWarningᴱ H (var x) (UnboundVariable x) = UnboundVariable x refl -runtimeWarningᴱ H (addr a) (SEGV a p) = UnallocatedAddress a p -runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p q r) = {!!} -- app₁ (runtimeWarningᴱ H M err) +runtimeWarningᴱ H (var x) UnboundVariable = UnboundVariable x refl +runtimeWarningᴱ H (addr a) (SEGV p) = UnallocatedAddress a p +runtimeWarningᴱ H (M $ N) (FunctionMismatch v w r) = {!!} -- app₁ (runtimeWarningᴱ H M err) runtimeWarningᴱ H (M $ N) (app₁ err) = app₁ (runtimeWarningᴱ H M err) runtimeWarningᴱ H (M $ N) (app₂ err) = app₂ (runtimeWarningᴱ H N err) -runtimeWarningᴱ H (block var b ∈ T is B end) (block _ err) = block₁ b (runtimeWarningᴮ H B err) -runtimeWarningᴱ H (binexp M op N) (BinopMismatch₁ op v w p q r) = {!!} -runtimeWarningᴱ H (binexp M op N) (BinopMismatch₂ op v w p q r) = {!!} +runtimeWarningᴱ H (block var b ∈ T is B end) (block err) = block₁ b (runtimeWarningᴮ H B err) +runtimeWarningᴱ H (binexp M op N) (BinopMismatch₁ v w p) = {!!} +runtimeWarningᴱ H (binexp M op N) (BinopMismatch₂ v w p) = {!!} runtimeWarningᴱ H (binexp M op N) (bin₁ err) = {!!} runtimeWarningᴱ H (binexp M op N) (bin₂ err) = {!!} -runtimeWarningᴮ H (local var x ∈ T ← M ∙ B) (local _ err) = local₁ (runtimeWarningᴱ H M err) +runtimeWarningᴮ H (local var x ∈ T ← M ∙ B) (local err) = local₁ (runtimeWarningᴱ H M err) runtimeWarningᴮ H (return M ∙ B) (return err) = return (runtimeWarningᴱ H M err) wellTypedProgramsDontGoWrong : ∀ H′ B B′ → (∅ᴴ ⊢ B ⟶* B′ ⊣ H′) → (RuntimeErrorᴮ H′ B′) → Warningᴮ ∅ᴴ (typeCheckᴮ ∅ᴴ ∅ B)