Commit bb1810cb authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Remove old file about object

parent 086c37bc
First Order fragments
Delta_Ob:
A, B ::= types
[l_i:B_i, i in 1..n] object types (l_i distinct)
K ground type
A -> B function type
a, b ::= terms
[l_i=ç(x_i:A_i)b_i, i in 1..n] object (l_i distinct)
a.l method invocation
a.l <= ç(x:A)b method update
x variable
λ(x:A)b function
b(a) application
(Type Object) (l_i distinct)
(forall i in 1..n, E |- B_i) => E |- [l_i:B_i, i in 1..n]
(Val Object) (where A=[l_i:B_i, i in 1..n])
(forall i in 1..n, E, x_i:A |- b_i : B_i) => E |- [l_i=ç(x_i:A)b_i, i in 1..n] : A
(Val Select)
E |- a : A => j in 1..n => E |- a.l_j : B_j
(Val Update)
E |- a : A => E, x:A |- b : B_j => j in 1..n => E |- a.l_j <= ç(x:A)b : A
Delta_x
(Env Empty)
=> empty |-
(Env x)
E |- A => x notin dom(E) => E, x:A |-
(Val x)
E', x:A, E'' |- => E', x:A, E'' => x : A
Delta_K
(Type Const)
E |- => E |- K
Delta_->
(Type Arrow)
E |- A => E |- B => E |- A -> B
(Val Fun)
Examples
Bool_A := [if:A, then:A, else:A]
true_A : Bool_A := [if = ç(x:Bool_A)x.then, then = ç(x:Bool_A)x.then, else=ç(x:Bool_A)x.else]
false_A : Bool_A := [if = ç(x:Bool_A)x.else, then = ç(x:Bool_A)x.then, else=ç(x:Bool_A)x.else]
if_A b then c else d := ((b.then <= ç(x:Bool_A)c).else <= ç(x:Bool_A) d).if x fresh
CHECK if_A true_A then c else d --> c
CHECK if_A false_A then c else d --> d
Delta_<:
(Sub Refl)
E |- A => E |- A <: A
(Sub Trans)
E |- A <: B => E |- B <: C => E |- A <: C
(Val Subsumption)
E |- a : A => E |- A <: B => A |- a : B
(Type Top)
E |- => E |- Top
(Sub Top)
E |- A => E |- A <: Top
Delta_<:->
(Sub Arrow)
E |- A' <: A => E |- B -> B' => E |- A -> B <: A' -> B'
Delta_<:Ob
(Sub Object) (l_i distinct)
(forall i in 1..n, E |- B_i) => E |- [l_i:B_i, i in 1..n+m] <: [l_i:B_i, i in 1..n]
Examples
RomCell := [get:Nat]
PromCell := [get:Nat, set:Nat -> RomCell]
PrivateCell := [contents:Nat, get:Nat, set: Nat -> RomCell]
myCell : PromCell := [contents=0, get=ç(s:PrivateCell)s.contents, set=ç(s:PrivateCell)λ(n:Nat)s.contents := n]
CHECK myCell.set(3).get
trait (A := [l_i:B_i, i in 1..n]) := [l_i:A -> B_i, i in 1..m]
Class(A := [l_i:B_i, i in I])_Ins,Sub := [new:[l_i:B_i, i in Ins], l_i:A -> B_i, i in Sub]
Class(A := [l_i:B_i, i in I]) := Class(A)_I,I
class(A, a_i, i in I)_Ins := [new=ç(z:Class(A)_Ins,I)[l_i=ç(s:A)z.l_i(s), i in I], l_i=a_i, i in I]
class(A, a_i, i in I) := class(A, a_i, i_in I)_I
Examples
PrivateCellClass := [new:PrivateCell, contents:PrivateCell -> Nat, get:PrivateCell -> Nat, set:PrivateCell -> Nat -> RomCell]
= Class(PrivateCell)
privateCellClass := [new=ç(s:PrivateCellClass)[contents=ç(s:PrivateCell)z.contents, get==ç(s:PrivateCell)z.get, set=ç(s:PrivateCell)z.set], contents=λ(s:PrivateCell)0, get=λ(s:PrivateCell) s.contents, set=λ(s:PrivateCell)λ(n:Nat)s.contents:=n]
PrivateCellTrait := [contents:PrivateCell -> Nat, get:PrivateCell -> Nat, set:PrivateCell -> Nat -> RomCell]
CHECK privateCellClass : PrivateCellTrait
PrivateCellLeafClass := [new:PrivateCell]
CHECK privateCellClass : PrivateCellLeafClass
CHECK privateCellClass.new : PrivateCell
RestrictedCellClass := [new:PromCell, contents:PrivateCell -> Nat, get:PrivateCell -> Nat, set:PrivateCell -> Nat -> RomCell]
= Class(PrivateCell)_{get, set},{contents, get, set}
restrictedCellClass := [new=ç(s:RestrictedCellClass)[contents=ç(s:PrivateCell)z.contents, get==ç(s:PrivateCell)z.get, set=ç(s:PrivateCell)z.set], contents=λ(s:PrivateCell)0, get=λ(s:PrivateCell) s.contents, set=λ(s:PrivateCell)λ(n:Nat)s.contents:=n]
NoContentsCellClass := [new:PromCell, get:PrivateCell -> Nat, set:PrivateCell -> Nat -> RomCell]
CHECK restrictedCellClass : NoContentsCellClass
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment