-
Notifications
You must be signed in to change notification settings - Fork 0
/
O4.lean
131 lines (103 loc) · 3.5 KB
/
O4.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
-- See: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/OO.20polymorphism.3F/near/297629381
namespace O4
inductive Geo_Type
| Point2D
| Point3D
| Point4D
| Square2D
deriving DecidableEq
open Geo_Type
structure Slots_Point2D where
(x y : Float)
deriving Repr
structure Slots_Point3D extends Slots_Point2D where
z : Float
deriving Repr
structure Slots_Point4D extends Slots_Point3D where
w : Float
deriving Repr
structure Slots_Square2D extends Slots_Point2D where
width : Float
deriving Repr
universe u
def Geo_Type.Slots : Geo_Type → Type
| Point2D => Slots_Point2D
| Point3D => Slots_Point3D
| Point4D => Slots_Point4D
| Square2D => Slots_Square2D
open Geo_Type
def toRepr : (T : Geo_Type) → Repr T.Slots
| Point2D => instReprSlots_Point2D
| Point3D => instReprSlots_Point3D
| Point4D => instReprSlots_Point4D
| Square2D => instReprSlots_Square2D
/-- Get casting function to first type from second type -/
def Geo_Type.cast : (t : Geo_Type) → (t' : Geo_Type) → Option (t'.Slots → t.Slots)
| Point2D, Point2D => some id
| Point2D, Point3D => some (λ x => x.toSlots_Point2D)
| Point3D, Point3D => some id
| Point2D, Point4D => some (λ x => x.toSlots_Point2D)
| Point3D, Point4D => some (λ x => x.toSlots_Point3D)
| Point4D, Point4D => some id
| Point2D, Square2D => some (λ x => x.toSlots_Point2D)
| Square2D, Square2D => some id
| _, _ => none
/-- Whether the second type is a subtype of the first. -/
def Geo_Type.supertype (t t' : Geo_Type) : Bool := (t.cast t').isSome
theorem Geo_Type.supertype.trans (h : Geo_Type.supertype t t') (h' : Geo_Type.supertype t' t'') :
Geo_Type.supertype t t'' :=
by
cases t
all_goals
cases t'
all_goals
cases t''
all_goals
simp at h
try simp at h'
try simp
def Option.get : (x : Option α) → x.isSome → α
| some v, _ => v
| none, h => by simp [Option.isSome] at h
/-- Get the cast function from a proof that `t'` is a subtype of `t`. -/
def Geo_Type.supertype.cast (h : Geo_Type.supertype t t') : t'.Slots → t.Slots :=
Option.get (Geo_Type.cast t t') h
/-- Objects of subtype t -/
structure Obj (t : Geo_Type) where
ty : Geo_Type
sub : Geo_Type.supertype t ty
slots : ty.Slots
instance : Coe Slots_Point2D (Obj Point2D) where coe s := ⟨Point2D, rfl, s⟩
instance : Coe Slots_Point3D (Obj Point3D) where coe s := ⟨Point3D, rfl, s⟩
instance : Coe Slots_Point4D (Obj Point4D) where coe s := ⟨Point4D, rfl, s⟩
instance : Coe Slots_Square2D (Obj Square2D) where coe s := ⟨Square2D, rfl, s⟩
/-- Extract the slots from an `Obj`. -/
def Obj.get (o : Obj t) : t.Slots := Geo_Type.supertype.cast o.sub o.slots
/-- Cast up, which can be done statically. -/
def Obj.cast_up (o : Obj t) (h : Geo_Type.supertype t' t := by rfl) : Obj t' where
ty := o.ty
sub := Geo_Type.supertype.trans h o.sub
slots := o.slots
def Obj.can_cast (o : Obj t) (t' : Geo_Type) : Bool := Geo_Type.supertype t' o.ty
/-- Cast up or down using run-time information. -/
def Obj.cast (o : Obj t) (h : o.can_cast t') : Obj t' where
ty := o.ty
sub := h
slots := o.slots
/-- Example using a run-time cast. -/
def Obj.get_w (o : Obj Point2D) : Float :=
if h : o.can_cast Point4D then
(o.cast h).get.w
else
0
#eval ({x := 1, y := 2 : Slots_Point2D} : Obj Point2D).get_w
-- 0.000000
#eval Id.run do
let p := ({x := 1, y := 2, z := 3, w := 4 : Slots_Point4D} : Obj Point4D)
return p.cast_up.get_w
-- 4.000000
def s2: Slots_Point2D := {x := 1, y := 2}
#eval s2
def o2: Obj Point2D := s2
#eval o2.slots
end O4