Mercurial > meta

changeset 6:799f43bce62b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Import some code from iwl
author Adam Chlipala <adam@chlipala.net>
date Tue, 14 Dec 2010 10:33:24 -0500
parents 943410267fad
children 32f8f5d2d9f0
files eq.ur eq.urs meta.urp sql.ur sql.urs variant.ur variant.urs
diffstat 7 files changed, 278 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/eq.ur	Tue Dec 14 10:33:24 2010 -0500
@@ -0,0 +1,76 @@
+con eq = K ==> fn (t1 :: K) (t2 :: K) => f :: (K -> Type) -> f t1 -> f t2
+
+val refl [K] [t ::: K] : eq t t = fn [f :: (K -> Type)] x => x
+
+fun sym [K] [t1 ::: K] [t2 ::: K] (e : eq t1 t2) : eq t2 t1 =
+    e [fn t => eq t t1] refl
+
+fun trans [K] [t1 ::: K] [t2 ::: K] [t3 ::: K] (e1 : eq t1 t2) (e2 : eq t2 t3) : eq t1 t3 =
+    (sym e1) [fn t => eq t t3] e2
+
+fun cast [K] [t1 ::: K] [t2 ::: K] (e : eq t1 t2) = e
+
+fun fold [K] [tf :: {K} -> Type] [r ::: {K}]
+         (f : pre :: {K} -> nm :: Name -> v :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
+          eq r (pre ++ [nm = v] ++ post) -> tf post -> tf ([nm = v] ++ post))
+    (i : tf []) (fl : folder r) : tf r =
+    @@Top.fold [fn post => pre :: {K} -> [pre ~ post] => eq r (pre ++ post) -> tf post]
+     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+                      (acc : pre :: {K} -> [pre ~ rest] => eq r (pre ++ rest) -> tf rest)
+                      [pre :: {K}] [pre ~ [nm = t] ++ rest] pf =>
+         f [pre] [nm] [t] [rest] ! ! pf (acc [[nm = t] ++ pre] ! pf))
+     (fn [pre :: {K}] [pre ~ []] _ => i) [r] fl [[]] ! refl
+
+fun foldUR [tr :: Type] [tf :: {Unit} -> Type] [r ::: {Unit}]
+    (f : pre :: {Unit} -> nm :: Name -> post :: {Unit} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
+     eq r (pre ++ [nm] ++ post) -> tr -> tf post -> tf ([nm] ++ post))
+    (i : tf []) (fl : folder r) (r : $(mapU tr r)) : tf r =
+    @@fold [fn r' => $(mapU tr r') -> tf r'] [r]
+      (fn [pre :: {Unit}] [nm :: Name] [u :: Unit] [post :: {Unit}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r =>
+          f [pre] [nm] [post] ! ! pf r.nm (acc (r -- nm)))
+      (fn _ => i) fl r
+
+fun foldR [K] [tr :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
+    (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
+     eq r (pre ++ [nm = t] ++ post) -> tr t -> tf post -> tf ([nm = t] ++ post))
+    (i : tf []) (fl : folder r) (r : $(map tr r)) : tf r =
+    @@fold [fn r' => $(map tr r') -> tf r'] [r]
+      (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r =>
+          f [pre] [nm] [t] [post] ! ! pf r.nm (acc (r -- nm)))
+      (fn _ => i) fl r
+
+fun foldR2 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
+    (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
+     eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tf post -> tf ([nm = t] ++ post))
+    (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) : tf r =
+    @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> tf r'] [r]
+      (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 =>
+          f [pre] [nm] [t] [post] ! ! pf r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+      (fn _ _ => i) fl r1 r2
+
+fun foldR3 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tr3 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
+    (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
+     eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tf post -> tf ([nm = t] ++ post))
+    (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) (r3 : $(map tr3 r)) : tf r =
+    @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> $(map tr3 r') -> tf r'] [r]
+      (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 r3 =>
+          f [pre] [nm] [t] [post] ! ! pf r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm)))
+      (fn _ _ _ => i) fl r1 r2 r3
+
+fun foldR4 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tr3 :: K -> Type] [tr4 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}]
+    (f : pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
+     eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tr4 t -> tf post -> tf ([nm = t] ++ post))
+    (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) (r3 : $(map tr3 r)) (r4 : $(map tr4 r)) : tf r =
+    @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> $(map tr3 r') -> $(map tr4 r') -> tf r'] [r]
+      (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 r3 r4 =>
+          f [pre] [nm] [t] [post] ! ! pf r1.nm r2.nm r3.nm r4.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm) (r4 -- nm)))
+      (fn _ _ _ _ => i) fl r1 r2 r3 r4
+
+fun mp [K] [tr :: K -> Type] [tf :: K -> Type] [r ::: {K}]
+       (f : nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] =>
+        eq r ([nm = t] ++ rest) -> tr t -> tf t)
+    (fl : folder r) (r : $(map tr r)) : $(map tf r) =
+  @@foldR [tr] [fn r => $(map tf r)] [r]
+      (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf r acc =>
+          {nm = f [nm] [t] [pre ++ post] ! pf r} ++ acc)
+      {} fl r
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/eq.urs	Tue Dec 14 10:33:24 2010 -0500
@@ -0,0 +1,44 @@
+(** A constructor equality predicate *)
+
+con eq :: K --> K -> K -> Type
+
+val refl : K --> t ::: K -> eq t t
+val sym : K --> t1 ::: K -> t2 ::: K -> eq t1 t2 -> eq t2 t1
+val trans : K --> t1 ::: K -> t2 ::: K -> t3 ::: K -> eq t1 t2 -> eq t2 t3 -> eq t1 t3
+
+val cast : K --> t1 ::: K -> t2 ::: K -> eq t1 t2 -> f :: (K -> Type) -> f t1 -> f t2
+
+val fold : K --> tf :: ({K} -> Type) -> r ::: {K}
+           -> (pre :: {K} -> nm :: Name -> v :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
+               eq r (pre ++ [nm = v] ++ post) -> tf post -> tf ([nm = v] ++ post))
+           -> tf [] -> folder r -> tf r
+
+val foldUR : tr :: Type -> tf :: ({Unit} -> Type) -> r ::: {Unit}
+           -> (pre :: {Unit} -> nm :: Name -> post :: {Unit} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
+               eq r (pre ++ [nm] ++ post) -> tr -> tf post -> tf ([nm] ++ post))
+           -> tf [] -> folder r -> $(mapU tr r) -> tf r
+
+val foldR : K --> tr :: (K -> Type) -> tf :: ({K} -> Type) -> r ::: {K}
+           -> (pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
+               eq r (pre ++ [nm = t] ++ post) -> tr t -> tf post -> tf ([nm = t] ++ post))
+           -> tf [] -> folder r -> $(map tr r) -> tf r
+
+val foldR2 : K --> tr1 :: (K -> Type) -> tr2 :: (K -> Type) -> tf :: ({K} -> Type) -> r ::: {K}
+             -> (pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
+                 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tf post -> tf ([nm = t] ++ post))
+             -> tf [] -> folder r -> $(map tr1 r) -> $(map tr2 r) -> tf r
+
+val foldR3 : K --> tr1 :: (K -> Type) -> tr2 :: (K -> Type) -> tr3 :: (K -> Type) -> tf :: ({K} -> Type) -> r ::: {K}
+             -> (pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
+                 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tf post -> tf ([nm = t] ++ post))
+             -> tf [] -> folder r -> $(map tr1 r) -> $(map tr2 r) -> $(map tr3 r) -> tf r
+
+val foldR4 : K --> tr1 :: (K -> Type) -> tr2 :: (K -> Type) -> tr3 :: (K -> Type) -> tr4 :: (K -> Type) -> tf :: ({K} -> Type) -> r ::: {K}
+             -> (pre :: {K} -> nm :: Name -> t :: K -> post :: {K} -> [pre ~ post] => [[nm] ~ pre ++ post] =>
+                 eq r (pre ++ [nm = t] ++ post) -> tr1 t -> tr2 t -> tr3 t -> tr4 t -> tf post -> tf ([nm = t] ++ post))
+             -> tf [] -> folder r -> $(map tr1 r) -> $(map tr2 r) -> $(map tr3 r) -> $(map tr4 r) -> tf r
+
+val mp : K --> tr :: (K -> Type) -> tf :: (K -> Type) -> r ::: {K}
+         -> (nm :: Name -> t :: K -> rest :: {K} -> [[nm] ~ rest] =>
+             eq r ([nm = t] ++ rest) -> tr t -> tf t)
+         -> folder r -> $(map tr r) -> $(map tf r)
--- a/meta.urp	Tue Dec 14 09:49:10 2010 -0500
+++ b/meta.urp	Tue Dec 14 10:33:24 2010 -0500
@@ -1,5 +1,9 @@
 $/char
 $/string
+$/option
 json
 incl
 mem
+eq
+variant
+sql
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/sql.ur	Tue Dec 14 10:33:24 2010 -0500
@@ -0,0 +1,15 @@
+fun sqexps [env] [fields] (fl : folder fields) (inj : $(map sql_injectable fields)) (r : $fields) =
+    @map2 [sql_injectable] [id] [sql_exp env [] []]
+     (fn [t] => @sql_inject)
+     fl inj r
+
+fun selector [tn :: Name] [fs] [ofs] [fs ~ ofs] (fl : folder fs) (m : $(map sql_injectable fs)) (r : $fs) =
+    @foldR2 [sql_injectable] [id]
+     [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool]
+     (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key]
+                      (inj : sql_injectable t) (v : t)
+                      (exp : rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool)
+                      [rest :: {Type}] [rest ~ [nm = t] ++ key] =>
+         (WHERE {{tn}}.{nm} = {@sql_inject inj v} AND {exp [[nm = t] ++ rest] !}))
+     (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE))
+     fl m r [_] !
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/sql.urs	Tue Dec 14 10:33:24 2010 -0500
@@ -0,0 +1,11 @@
+(** Common metaprogramming patterns for SQL syntax construction *)
+
+val sqexps : env ::: {{Type}} -> fields ::: {Type} -> folder fields -> $(map sql_injectable fields)
+             -> $fields -> $(map (sql_exp env [] []) fields)
+(* Convert a record of Ur values into a record of SQL expressions *)
+
+val selector : tn :: Name -> fs ::: {Type} -> ofs ::: {Type} -> [fs ~ ofs]
+               => folder fs -> $(map sql_injectable fs) -> $fs
+               -> sql_exp [tn = ofs ++ fs] [] [] bool
+(* Build a boolean SQL expression expressing equality of some fields of a table
+ * row with a record of Ur values *)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/variant.ur	Tue Dec 14 10:33:24 2010 -0500
@@ -0,0 +1,95 @@
+fun read [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) : t =
+    match v
+    (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> t) r)]
+     (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us] (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> _) [r'::_] [[nm = u] ++ us ~ r'] r =>
+         {nm = fn () => r.nm} ++ cs [[nm = u] ++ r'] ! r)
+     (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r)
+
+fun write [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) (x : t) : $(mapU t r) =
+    match v
+    (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> $(mapU t (r ++ r'))) r)]
+      (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us]
+          (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> $(mapU ({} -> $(mapU t (us ++ r'))) us))
+          [r'::_] [[nm = u] ++ us ~ r'] r =>
+          {nm = fn () => r -- nm ++ {nm = x}} ++ cs [[nm = u] ++ r'] ! r)
+      (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r)
+
+fun search [r] [t] (f : variant (mapU {} r) -> option t) (fl : folder r) : option t =
+    @fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t]
+    (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
+                     (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t)
+                     [r' ::_] [[nm] ++ r ~ r'] f' =>
+        case f' (make [nm] {}) of
+            None => acc [[nm] ++ r'] ! f'
+          | v => v)
+    (fn [r' ::_] [[] ~ r'] _ => None) fl [[]] ! f
+
+fun find [r] (f : variant (mapU {} r) -> bool) (fl : folder r) : option (variant (mapU {} r)) =
+    @search (fn v => if f v then Some v else None) fl
+
+fun test [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (fl : folder ([nm = t] ++ ts))
+          (v : variant ([nm = t] ++ ts)) : option t =
+    match v ({nm = Some}
+                 ++ (@map0 [fn t' => t' -> option t] (fn [t' :: Type] _ => None) fl -- nm))
+
+fun testLess [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (fl : folder ts) (v : variant ([nm = t] ++ ts)) : option t =
+    match v ({nm = Some}
+                 ++ @map0 [fn t' => t' -> option t] (fn [t' :: Type] _ => None) fl)
+
+fun eq [r] (fl : folder r) (v1 : variant (mapU {} r)) (v2 : variant (mapU {} r)) : bool =
+    match v1
+    (@fold [fn r => r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)]
+     (fn [nm ::_] [u ::_] [r ::_] [[nm] ~ r]
+         (acc : r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r))
+         [r' ::_] [[nm] ++ r ~ r'] (fl' : folder ([nm] ++ r ++ r')) v =>
+         {nm = fn () => Option.isSome (@test [nm] ! (@Folder.mp fl') v)}
+             ++ acc [[nm] ++ r'] ! fl' v)
+     (fn [r' ::_] [[] ~ r'] _ _ => {}) fl [[]] ! fl v2)
+
+fun fold [r] [t] (fl : folder r) (f : variant (mapU {} r) -> t -> t) : t -> t =
+    @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t]
+    (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
+                     (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t)
+                     [r' ::_] [[nm] ++ r ~ r'] f' acc' =>
+        f' (make [nm] {}) (acc [[nm] ++ r'] ! f' acc'))
+    (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f
+
+fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type]
+    (f : p :: K -> f p -> fr p -> t)
+    [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t =
+    match v
+    (@Top.mp [fr] [fn p => f p -> t]
+     (fn [p] (m : fr p) (v : f p) => f [p] v m)
+     fl r)
+
+fun destr2R [K] [f1 :: K -> Type] [f2 :: K -> Type] [fr :: K -> Type] [t ::: Type]
+    (f : p :: K -> f1 p -> f2 p -> fr p -> t)
+    [r ::: {K}] (fl : folder r) (v1 : variant (map f1 r)) (v2 : variant (map f2 r)) (r : $(map fr r)) : option t =
+    match v1
+    (@foldR [fr] [fn r => others :: {K} -> [others ~ r] =>
+                     folder (r ++ others)
+                     -> variant (map f2 (r ++ others))
+                     -> $(map (fn p => f1 p -> option t) r)]
+     (fn [nm ::_] [p ::_] [r ::_] [[nm] ~ r] (meta : fr p)
+         (acc : others :: {K} -> [others ~ r] =>
+          folder (r ++ others)
+          -> variant (map f2 (r ++ others))
+          -> $(map (fn p => f1 p -> option t) r))
+         [others :: {K}] [others ~ [nm = p] ++ r]
+         (fl : folder ([nm = p] ++ r ++ others))
+         (v2 : variant (map f2 ([nm = p] ++ r ++ others))) =>
+         {nm = fn x1 => match v2
+                        ({nm = fn x2 => Some (f [p] x1 x2 meta)}
+                             ++ (@map0 [fn p => f2 p -> option t] (fn [p' ::_] _ => None) fl -- nm))}
+             ++ acc [[nm = p] ++ others] ! fl v2)
+     (fn [others ::_] [others ~ []] _ _ => {})
+     fl r [[]] ! fl v2)
+
+fun testEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts]
+    (pf : Eq.eq r ([nm = t] ++ ts)) (fl : folder r) (v : variant (map f r)) : option (f t) =
+  @test [nm] ! (@Folder.mp (@Eq.cast pf [folder] fl))
+   (Eq.cast pf [fn r => variant (map f r)] v)
+
+fun makeEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts]
+    (pf : Eq.eq r ([nm = t] ++ ts)) (x : f t) : variant (map f r) =
+  Eq.cast (Eq.sym pf) [fn r => variant (map f r)] (make [nm] x)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/variant.urs	Tue Dec 14 10:33:24 2010 -0500
@@ -0,0 +1,33 @@
+(** Derived functions dealing with polymorphic variants *)
+
+val read : r ::: {Unit} -> t ::: Type -> folder r -> $(mapU t r) -> variant (mapU {} r) -> t
+val write : r ::: {Unit} -> t ::: Type -> folder r -> $(mapU t r) -> variant (mapU {} r) -> t -> $(mapU t r)
+
+val search : r ::: {Unit} -> t ::: Type -> (variant (mapU {} r) -> option t) -> folder r -> option t
+val find : r ::: {Unit} -> (variant (mapU {} r) -> bool) -> folder r -> option (variant (mapU {} r))
+
+val test : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ([nm = t] ++ ts)
+                                                                    -> variant ([nm = t] ++ ts) -> option t
+val testLess : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ts -> variant ([nm = t] ++ ts) -> option t
+
+val testEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] =>
+    Eq.eq r ([nm = t] ++ ts)
+    -> folder r
+    -> variant (map f r) -> option (f t)
+
+val eq : r ::: {Unit} -> folder r -> variant (mapU {} r) -> variant (mapU {} r) -> bool
+
+val makeEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] =>
+    Eq.eq r ([nm = t] ++ ts)
+    -> f t
+    -> variant (map f r)
+
+val fold : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t -> t) -> t -> t
+
+val destrR : K --> f :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
+             -> (p :: K -> f p -> fr p -> t)
+             -> r ::: {K} -> folder r -> variant (map f r) -> $(map fr r) -> t
+
+val destr2R : K --> f1 :: (K -> Type) -> f2 :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type
+             -> (p :: K -> f1 p -> f2 p -> fr p -> t)
+             -> r ::: {K} -> folder r -> variant (map f1 r) -> variant (map f2 r) -> $(map fr r) -> option t