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

Fix typing in dk_obj using non-linear rules

parent cea760d5
......@@ -45,7 +45,7 @@ INSTALL_DIR = /usr/local/bin
DKCHECK=dkcheck
DKDEP=dkdep
DKCHECKOPTIONS=
DKCHECKOPTIONS=-nl
DKDEPOPTIONS=-v
.dk.dko:
......
......@@ -118,68 +118,58 @@ def preselect : A : ObjType ->
D : Domain ->
o : PreObj A D ->
l : Label ->
H : dk_domain.Subset D (Ot_domain A) ->
H : domain_pos l (Ot_domain A) ->
Hd: domain_pos l D ->
Expr A ->
Expr (Ot_assoc A l (H l Hd)).
Expr (Ot_assoc A l H).
[m]
preselect _ _ (Po_cons _ _ _ _ m _) _ _ (dk_domain.Position_head _ _)
[m,H]
preselect _ _ (Po_cons _ _ _ H m _) _ H (dk_domain.Position_head _ _)
-->
m
[A,D,l,l2,o,Hsub,Htl]
[A,D,l,l2,o,H,Htl]
preselect
A
(dk_domain.cons l2 D)
(Po_cons _ _ _ _ _ o)
l
Hsub
(dk_domain.Position_tail _ _ _ Htl)
A
(dk_domain.cons l2 D)
(Po_cons _ _ _ _ _ o)
l
H
(dk_domain.Position_tail _ _ _ Htl)
-->
preselect A D o l
(l3 : Label =>
Hp : domain_pos l3 D =>
Hsub l3 (dk_domain.Position_tail l3 l2 D Hp))
Htl.
preselect A D o l H Htl.
def preupdate : A : ObjType ->
D : Domain ->
o : PreObj A D ->
l : Label ->
Hsub : dk_domain.Subset D (Ot_domain A) ->
H : domain_pos l (Ot_domain A) ->
Hp: domain_pos l D ->
(Expr A -> Expr (Ot_assoc A l (Hsub l Hp))) ->
(Expr A -> Expr (Ot_assoc A l H)) ->
PreObj A D.
[A,D,l,Hsub,o,m2]
[A,D,l,p,o,m2]
preupdate
A
(dk_domain.cons l D)
(Po_cons _ _ _ _ _ o)
l
Hsub
(dk_domain.Position_head _ _)
m2
A
(dk_domain.cons _ D)
(Po_cons _ _ _ p _ o)
l
p
(dk_domain.Position_head _ _)
m2
-->
Po_cons A D l (Hsub l (dk_domain.Position_head l D)) m2 o
Po_cons A D l p m2 o
[A,D,l,l2,H,Hsub,m1,m2,o,Hpos]
[A,D,l,l2,H,Hsub,m1,m2,o,Hpos,p]
preupdate
A
(dk_domain.cons l2 D)
(Po_cons A D l2 Hpos m1 o)
(Po_cons _ _ _ Hpos m1 o)
l
Hsub
(dk_domain.Position_tail l l2 D H)
p
(dk_domain.Position_tail _ _ _ H)
m2
-->
Po_cons A D l2 Hpos
m1
(preupdate A D o l
(l3 : Label =>
Hp : domain_pos l3 D =>
Hsub l3 (dk_domain.Position_tail l3 l2 D Hp))
H
m2).
Po_cons A D l2 Hpos m1 (preupdate A D o l p H m2).
def obj_select : A : ObjType ->
eA : Expr A ->
......@@ -194,7 +184,7 @@ def obj_select : A : ObjType ->
(Ot_domain A)
o
l
(l : Label => Hpos : domain_pos l (Ot_domain A) => Hpos)
H
H
o.
......@@ -232,7 +222,7 @@ def obj_update : A : ObjType ->
(Ot_domain A)
o
l
(l : Label => Hpos : domain_pos l (Ot_domain A) => Hpos)
H
H
m.
......
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