Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add class-based oop example from [KS22 Example 2.8] #53

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

Add class-based oop example from [KS22 Example 2.8] #53

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
810829a
Add a simple example
eyihluyc Dec 6, 2024
7c32aec
Add class-based oop example from [KS22 Example 2.8]
Anatolay Dec 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
247 changes: 247 additions & 0 deletions Minimal/Examples.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,247 @@
import Minimal.Calculus

open Term
open OptionalAttr
open Reduce

/-
## References

* [Nikolai Kudasov and Violetta Sim. 2023. Formalizing 𝜑-Calculus: A Purely Object-Oriented Calculus of Decorated Objects.][KS22]

Class-based OOP example, modelling the following snippet (Java):

class Base {
Integer g() { return h(); }
Integer h() { return 3; }
}
class Derived extends Base {
Integer f() { return 2 + this.g(); }
Integer h() { return 5; }
}
Derived d = new Derived();
-/

/-- [KS22, Example 2.8]-/
def base : Term :=
obj (Bindings.cons
"new"
(by simp)
(attached
(Bindings.cons
"g"
(by simp)
(attached
(Bindings.cons
"this"
(by simp)
void
(Bindings.cons
"φ"
(by simp)
(attached
(dot
(app
(dot
(dot
(loc 0)
"this"
)
"h"
)
"this"
(dot (loc 0) "this")
)
"φ"
)
)
Bindings.nil
)
)
)

(Binding.cons
"h"
(by simp)
(attached
(Bindings.cons
"this"
(by simp)
void
(Bindings.cons
"φ"
(by simp)
(attached (obj (Bindings.cons "3" (by simp) void Bindings.nil))) -- the base calculus does not have numbers, should be a 3
Bindings.nil
)
)
)
Bindings.nil
)
)
)
Binding.nil
)

def derived : Term :=
obj (Bindings.cons
"new"
(by simp)
(attached (obj
(Bindings.cons
"φ"
(by simp)
(attached
(dot base "new")
)

(Binding.cons
"f"
(by simp)
(attached
(Bindings.cons
"this"
(by simp)
void
(Bindings.cons
"φ"
(by simp)
(attached
(app
(dot
(obj (Bindings.cons "2" (by simp) void Bindings.nil)) -- the base calculus does not have numbers, should be a 2
"add"
)
"n"
(dot
(app
(dot
(dot
(loc 0)
"this"
)
"g"
)
"this"
(dot
(loc 0)
"this"
)
)
"φ"
)
)
)
Bindings.nil
)
)
)

(Bindings.cons
"h"
(by simp)
(attached
(Bindings.cons
"this"
(by simp)
void
(Bindings.cons
"φ"
(by simp)
(attached (obj (Bindings.cons "5" (by simp) void Bindings.nil))) -- the base calculus does not have numbers, should be a 5
Bindings.nil
)
)
)
Bindings.nil
)
)
))
)
Binding.nil
)

def d : Term := dot derived "new"

def invocation1
: d
⇝
(obj (Bindings.cons "φ" (by simp) (attached (dot base "new"))
(Binding.cons "f" (by simp) (attached
(Bindings.cons "this" (by simp) void
(Bindings.cons "φ" (by simp) (attached
(app
(dot (obj (Bindings.cons "2" (by simp) void Bindings.nil)) "add")
"n"
(dot (app (dot (dot (loc 0) "this") "g") "this" (dot (loc 0) "this")) "φ")
)
)
Bindings.nil))
)
(Bindings.cons "h" (by simp) (attached
(Bindings.cons "this" (by simp) void
(Bindings.cons "φ" (by simp) (attached (obj (Bindings.cons "5" (by simp) void Bindings.nil)))
Bindings.nil))
)
Bindings.nil))
)
)
:= by
simp [substitute]
exact dot_c _ "new" _ (by simp) (by simp [lookup])

-- def invocation
-- : dot (app (dot d "f") "this" d) "φ" -- d.f(this ↦ d).φ === Derived.new.f(this ↦ d).φ
-- ⇝* app
-- (dot (obj (Bindings.cons "2" (by simp) void Bindings.nil)) "add")
-- "n"
-- (dot (app (dot d "g") "this" d) "φ")
-- :=
-- ReflTransGen.head
-- (dot_c _ "new" _ _ _)
-- (ReflTransGen.head
-- _
-- (ReflTransGen.head
-- _
-- (ReflTransGen.head
-- _
-- (ReflTransGen.head
-- _
-- (ReflTransGen.head
-- _
-- ReflTransGen.refl
-- )))))


-- ⟦ a ↦ ⟦ ⟧ ⟧.a
def example1 : Term :=
dot
(obj
(Bindings.cons
"a"
(by simp)
(attached (obj (Bindings.nil)))
Bindings.nil))
"a"

-- ⟦ ⟧
def example1' : Term := obj Bindings.nil

-- ⟦ a ↦ ⟦ ⟧ ⟧.a ⇝ ⟦ ⟧
def test1_red1 : example1 ⇝ example1' := by
rw [example1, example1']
exact (dot_c
(obj Bindings.nil)
"a"
(Bindings.cons
"a"
(by simp)
(attached (obj (Bindings.nil)))
Bindings.nil)
(by simp)
(by simp [lookup]))

-- ⟦ a ↦ ⟦ ⟧ ⟧.a ⇝* ⟦ ⟧
def test1 : example1 ⇝* example1' := ReflTransGen.head
test1_red1
ReflTransGen.refl
Loading