Almost working subtyping

dk_lrecords.dk

@@ -212,3 +212,87 @@ to_assoc_list : f : Typer ->
                   triple
                   (l : Label => mk_triple l (f l) (R l))
                   D.
+
+(; Association lists subtyping ;)
+
+Assoc_rm : Assoc_list ->
+           Label ->
+           Assoc_list.
+(; Assoc_rm L l
+   Remove the first triple of L whith key equal to l.
+;)
+
+[ l1 : Label,
+  l2 : Label,
+  A : cc.uT,
+  a : cc.eT A,
+  L : Assoc_list ]
+    Assoc_rm (dk_list.cons _ (mk_triple l1 A a) L) l2
+      -->
+    if_label_eq (l : Label => assoc_list
+                ) l2 l1
+                L
+                (Assoc_cons (mk_triple l1 A a) (Assoc_rm L l2)).
+
+Assoc_subtype : Assoc_list ->
+                Assoc_list ->
+                Assoc_list.
+(; when lA <: lB, Assoc_subtype lA lB ~= lB ;)
+
+[] Assoc_subtype (dk_list.nil _) (dk_list.nil _) --> Assoc_nil.
+
+[ l : Assoc_list ]
+    Assoc_subtype (dk_list.cons _ _ l) (dk_list.nil _) --> Assoc_subtype l Assoc_nil.
+
+[ lA : Assoc_list,
+  t : Triple,
+  lB : Assoc_list ]
+    Assoc_subtype lA (dk_list.cons _ t lB)
+      -->
+    Assoc_cons t (Assoc_subtype (Assoc_rm lA (fst t)) lB).
+
+
+Record_subtype : f : Typer ->
+                 DA : Domain ->
+                 DB : Domain ->
+                 RA : Record f DA ->
+                 RB : Record f DB ->
+                 Record f DB.
+
+(; [f : Typer, ;)
+(;  DA : Domain, ;)
+(;  RA : Record f DA, ;)
+(;  RB : Record f domain_nil, ;)
+(;  l : Label] ;)
+(;     Record_subtype f DA (dk_list.nil _) RA RB l ;)
+(;       --> ;)
+(;     dk_fail.fail (f l). ;)
+
+(; [f : Typer, ;)
+(;  DA : Domain, ;)
+(;  l : Label, ;)
+(;  DB : Domain, ;)
+(;  RA : Record f DA, ;)
+(;  RB : Record f (domain_cons l DB)] ;)
+(;     Record_subtype f DA (dk_list.cons _ l DB) RA RB ;)
+(;       --> ;)
+(;     (assoc_val (dk_list.cons triple (mk_triple l (f l) (RA l)) (dk_list.map label triple (l:Label => mk_triple l (f l) (RA l)) DB))). ;)
+
+[ f : Typer,
+  DA : Domain,
+  RA : Record f DA,
+  RB : Record f domain_nil]
+    Record_subtype f DA (dk_list.nil _) RA RB --> RB.
+
+[ f : Typer,
+  DA : Domain,
+  DB : Domain,
+  RA : Record f DA,
+  l : Label,
+  RB : Record f (domain_cons l DB)]
+    Record_subtype f DA (dk_list.cons _ l DB) RA RB
+      -->
+    (l2 : Label =>
+     if_label_eq f l l2
+                   (RA l)
+                   (Record_subtype f DA DB RA RB l2)).

dk_string.dk

@@ -11,3 +11,5 @@ equal : cc.eT string -> cc.eT string -> cc.eT dk_bool.bool.
 [ c1 : cc.eT dk_char.char, s1 : cc.eT string, c2 : cc.eT dk_char.char, s2 : cc.eT string]
     equal (dk_list.cons _ c1 s1) (dk_list.cons _ c2 s2)
       --> dk_bool.and (dk_char.equal c1 c2) (equal s1 s2).
+
+[ s : cc.eT string ] equal s s --> dk_bool.true.

dk_zeta_FO.dk

@@ -158,14 +158,78 @@ ifT : A : cc.uT -> Expr d_ite (BoolT A) -> cc.eT A -> cc.eT A -> cc.eT A
 (; #ASSERT (ifT A (trueT A) t e) ~= t. ;)
 (; #ASSERT (ifT A (falseT A) t e) ~= e. ;)
 
-
 (; Sous-typage ;)
+(; cast_type : DA : Domain -> ;)
+(;             DB : Domain -> ;)
+(;             RA : Record DA -> ;)
+(;             RB : Record DB -> ;)
+(;             Record DB. ;)
+
+(; [ DA : Domain, ;)
+(;   RA : Record DA, ;)
+(;   RB : Record (dk_lrecords.domain_nil) ] ;)
+(;   cast_type DA dk_lrecords.domain_nil RA RB --> RB. ;)
+
+(; [ DA : Domain, ;)
+(;   l : Label, ;)
+(;   DB : Domain ;)
+(;   RA : Record DA, ;)
+(;   RB : Record (dk_lrecords.domain_cons l DB) ] ;)
+(;   cast_type DA (dk_lrecords.domain_cons l DB) RA RB ;)
+(;       --> ;)
+(;   dk_lrecords. ;)
+(; . ;)
+
+ocast : DA : Domain ->
+        DB : Domain ->
+        RA : Record DA ->
+        RB : Record DB ->
+        Object DA RA ->
+        Object DB (dk_lrecords.Record_subtype TTyper DA DB RA RB).
+
+[ DA : Domain,
+  RA : Record DA,
+  RB : Record dk_lrecords.domain_nil,
+  oA : Object DA RA,
+  l : Label,
+  self : Expr dk_lrecords.domain_nil RB]
+    ocast DA (dk_list.nil _) RA RB oA l self
+      -->
+    dk_fail.fail (RB l).
+
+[ DA : Domain,
+  l1 : Label,
+  DB : Domain,
+  RA : Record DA,
+  RB : Record (dk_lrecords.domain_cons l1 DB),
+  oA : Object DA RA,
+  l2 : Label,
+  self : Expr
+    (dk_lrecords.domain_cons l1 DB)
+    (dk_lrecords.Record_subtype TTyper DA (dk_lrecords.domain_cons l1 DB) RA RB)]
+    ocast DA (dk_list.cons _ l1 DB) RA RB oA l2 self
+      -->
+    dk_lrecords.if_label_eq (dk_lrecords.Record_subtype TTyper DA (dk_lrecords.domain_cons l1 DB) RA RB)
+                l1 l2
+                  (select DA RA (make DA RA oA) l1)
+                  (select
+                    DB
+                    (dk_lrecords.Record_subtype TTyper DA (dk_lrecords.domain_cons l1 DB) RA RB)
+                    (make
+                      DB
+                      (dk_lrecords.Record_subtype TTyper DA (dk_lrecords.domain_cons l1 DB) RA RB)
+                      (ocast DA DB RA RB oA))
+                    l2).
+
+
+
+
 cast : DA : Domain ->
        DB : Domain ->
        RA : Record DA ->
        RB : Record DB ->
        Expr DA RA ->
-       Expr DB RB.
+       Expr DB (dk_lrecords.Record_subtype TTyper DA DB RA RB).
 
 [ DA : Domain,
   DB : Domain,
@@ -174,7 +238,7 @@ cast : DA : Domain ->
   oA : Object DA RA]
     cast DA DB RA RB (make _ _ oA)
 -->
-    make DB RB (l : Label => self : Expr DB RB => select DB RB self l).
+    make DB RA (ocast DA DB RA RB oA).
 
 (; Exemple ;)
 l_get : Label := dk_list.cons dk_char.char dk_char.g (
@@ -196,7 +260,9 @@ l_set : Label := dk_list.cons dk_char.char dk_char.s (
                  dk_list.cons dk_char.char dk_char.t (
                  dk_list.nil dk_char.char))).
 
-d_get_set : Domain := dk_lrecords.domain_cons l_set d_get.
+d_get_set : Domain := dk_lrecords.domain_cons l_get
+                        (dk_lrecords.domain_cons l_set
+                           dk_lrecords.domain_nil).
 
 PromCell : Record d_get_set
 :=
@@ -217,7 +283,10 @@ l_contents : Label := dk_list.cons dk_char.char dk_char.c (
                       dk_list.cons dk_char.char dk_char.s (
                       dk_list.nil dk_char.char)))))))).
 
-d_gsc : Domain := dk_lrecords.domain_cons l_contents d_get_set.
+d_gsc : Domain := dk_lrecords.domain_cons l_get (
+                                          dk_lrecords.domain_cons l_set
+                                            (dk_lrecords.domain_cons l_contents
+                                            dk_lrecords.domain_nil)).
 
 PrivateCell : Record d_gsc
 :=
@@ -229,13 +298,15 @@ PrivateCell : Record d_gsc
                (AssocTT_cons (mk_coupleTT l_contents dk_nat.Nat)
                (AssocTT_nil)))))).
 
-Private_to_Rom : Expr d_gsc PrivateCell
-                  -> Expr d_get RomCell
-:= cast d_gsc d_get PrivateCell RomCell.
 Private_to_Prom : Expr d_gsc PrivateCell
                   -> Expr d_get_set PromCell
 := cast d_gsc d_get_set PrivateCell PromCell.
 
+Private_to_Rom : Expr d_gsc PrivateCell
+                  -> Expr d_get RomCell
+:= cast d_gsc d_get PrivateCell RomCell.
+
+
 myCell : Expr d_get_set PromCell
 :=
     Private_to_Prom (
@@ -251,7 +322,7 @@ myCell : Expr d_get_set PromCell
                       (self : Expr d_gsc PrivateCell => dk_fail.fail (PrivateCell l)))))).
 
 (; The following check makes Dedukti use all the RAM… ;)
-(; := select d_get RomCell ;)
-(;    (select d_get_set PromCell myCell l_set dk_nat.__3) ;)
-(;    l_get. ;)
+:= select d_get RomCell
+   (select d_get_set PromCell myCell l_set dk_nat.__3)
+   l_get.