summaryrefslogtreecommitdiff
path: root/lib/ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-12-26 11:56:40 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-12-26 11:56:40 -0500
commitc4120c8ddaa5340efad5f835ce4565f2a8ae2cbf (patch)
treeb4c6e798738335ded8d209afc369885664396d08 /lib/ur
parent4300120544123e9dfb262eb8b4e3d0a0f17ff9bc (diff)
Make summary unification more conservative; infer implicit arguments after applications
Diffstat (limited to 'lib/ur')
-rw-r--r--lib/ur/monad.ur60
-rw-r--r--lib/ur/monad.urs10
-rw-r--r--lib/ur/top.ur56
-rw-r--r--lib/ur/top.urs28
4 files changed, 77 insertions, 77 deletions
diff --git a/lib/ur/monad.ur b/lib/ur/monad.ur
index efba7546..e15da523 100644
--- a/lib/ur/monad.ur
+++ b/lib/ur/monad.ur
@@ -1,10 +1,10 @@
fun exec [m ::: Type -> Type] (_ : monad m) [ts ::: {Type}] r (fd : folder ts) =
- foldR [m] [fn ts => m $ts]
- (fn [nm :: Name] [v :: Type] [rest :: {Type}] [[nm] ~ rest] action acc =>
- this <- action;
- others <- acc;
- return ({nm = this} ++ others))
- (return {}) [ts] fd r
+ @foldR [m] [fn ts => m $ts]
+ (fn [nm :: Name] [v :: Type] [rest :: {Type}] [[nm] ~ rest] action acc =>
+ this <- action;
+ others <- acc;
+ return ({nm = this} ++ others))
+ (return {}) fd r
fun ignore [m ::: Type -> Type] (_ : monad m) [t] (v : m t) = x <- v; return ()
@@ -16,40 +16,40 @@ fun foldR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: {K} -> Type]
(f : nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf t -> tr rest -> m (tr ([nm = t] ++ rest)))
- (i : tr []) [r :: {K}] (fl : folder r) =
- Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)]
- (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
- (acc : _ -> m (tr rest)) r =>
- acc' <- acc (r -- nm);
- f [nm] [t] [rest] ! r.nm acc')
- (fn _ => return i)
- [_] fl
+ (i : tr []) [r ::: {K}] (fl : folder r) =
+ @Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+ (acc : _ -> m (tr rest)) r =>
+ acc' <- acc (r -- nm);
+ f [nm] [t] [rest] ! r.nm acc')
+ (fn _ => return i)
+ fl
fun foldR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type]
(f : nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest)))
- (i : tr []) [r :: {K}] (fl : folder r) =
- Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)]
- (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
- (acc : _ -> _ -> m (tr rest)) r1 r2 =>
- acc' <- acc (r1 -- nm) (r2 -- nm);
- f [nm] [t] [rest] ! r1.nm r2.nm acc')
- (fn _ _ => return i)
- [_] fl
+ (i : tr []) [r ::: {K}] (fl : folder r) =
+ @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+ (acc : _ -> _ -> m (tr rest)) r1 r2 =>
+ acc' <- acc (r1 -- nm) (r2 -- nm);
+ f [nm] [t] [rest] ! r1.nm r2.nm acc')
+ (fn _ _ => return i)
+ fl
fun foldR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type]
(f : nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest)))
- (i : tr []) [r :: {K}] (fl : folder r) =
- Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)]
- (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
- (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 =>
- acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
- f [nm] [t] [rest] ! r1.nm r2.nm r3.nm acc')
- (fn _ _ _ => return i)
- [_] fl
+ (i : tr []) [r ::: {K}] (fl : folder r) =
+ @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+ (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 =>
+ acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
+ f [nm] [t] [rest] ! r1.nm r2.nm r3.nm acc')
+ (fn _ _ _ => return i)
+ fl
fun mapR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: K -> Type]
(f : nm :: Name -> t :: K -> tf t -> m (tr t)) =
diff --git a/lib/ur/monad.urs b/lib/ur/monad.urs
index 9ad9262d..698a4b5b 100644
--- a/lib/ur/monad.urs
+++ b/lib/ur/monad.urs
@@ -14,7 +14,7 @@ val foldR : K --> m ::: (Type -> Type) -> monad m
-> [[nm] ~ rest] =>
tf t -> tr rest -> m (tr ([nm = t] ++ rest)))
-> tr []
- -> r :: {K} -> folder r -> $(map tf r) -> m (tr r)
+ -> r ::: {K} -> folder r -> $(map tf r) -> m (tr r)
val foldR2 : K --> m ::: (Type -> Type) -> monad m
-> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
@@ -23,7 +23,7 @@ val foldR2 : K --> m ::: (Type -> Type) -> monad m
-> [[nm] ~ rest] =>
tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest)))
-> tr []
- -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r)
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r)
val foldR3 : K --> m ::: (Type -> Type) -> monad m
-> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
@@ -32,16 +32,16 @@ val foldR3 : K --> m ::: (Type -> Type) -> monad m
-> [[nm] ~ rest] =>
tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest)))
-> tr []
- -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)
val mapR : K --> m ::: (Type -> Type) -> monad m
-> tf :: (K -> Type)
-> tr :: (K -> Type)
-> (nm :: Name -> t :: K -> tf t -> m (tr t))
- -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r))
+ -> r ::: {K} -> folder r -> $(map tf r) -> m ($(map tr r))
val mapR2 : K --> m ::: (Type -> Type) -> monad m
-> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
-> tr :: (K -> Type)
-> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t))
- -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r))
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r))
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
index e4e33940..b6f6349a 100644
--- a/lib/ur/top.ur
+++ b/lib/ur/top.ur
@@ -9,7 +9,7 @@ con folder = K ==> fn r :: {K} =>
fun fold [K] [tf :: {K} -> Type]
(f : (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
tf r -> tf ([nm = v] ++ r)))
- (i : tf []) [r :: {K}] (fl : folder r) = fl [tf] f i
+ (i : tf []) [r ::: {K}] (fl : folder r) = fl [tf] f i
structure Folder = struct
fun nil [K] [tf :: {K} -> Type]
@@ -92,27 +92,27 @@ fun read_option [t ::: Type] (_ : read t) =
fun txt [t] [ctx ::: {Unit}] [use ::: {Type}] (_ : show t) (v : t) =
cdata (show v)
-fun map0 [K] [tf :: K -> Type] (f : t :: K -> tf t) [r :: {K}] (fl : folder r) =
+fun map0 [K] [tf :: K -> Type] (f : t :: K -> tf t) [r ::: {K}] (fl : folder r) =
fl [fn r :: {K} => $(map tf r)]
(fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc =>
acc ++ {nm = f [t]})
{}
-fun mp [K] [tf1 :: K -> Type] [tf2 :: K -> Type] (f : t ::: K -> tf1 t -> tf2 t) [r :: {K}] (fl : folder r) =
+fun mp [K] [tf1 :: K -> Type] [tf2 :: K -> Type] (f : t ::: K -> tf1 t -> tf2 t) [r ::: {K}] (fl : folder r) =
fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r)]
(fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r =>
acc (r -- nm) ++ {nm = f r.nm})
(fn _ => {})
fun map2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type]
- (f : t ::: K -> tf1 t -> tf2 t -> tf3 t) [r :: {K}] (fl : folder r) =
+ (f : t ::: K -> tf1 t -> tf2 t -> tf3 t) [r ::: {K}] (fl : folder r) =
fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r)]
(fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 =>
acc (r1 -- nm) (r2 -- nm) ++ {nm = f r1.nm r2.nm})
(fn _ _ => {})
fun map3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tf :: K -> Type]
- (f : t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t) [r :: {K}] (fl : folder r) =
+ (f : t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t) [r ::: {K}] (fl : folder r) =
fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)]
(fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 r3 =>
acc (r1 -- nm) (r2 -- nm) (r3 -- nm) ++ {nm = f r1.nm r2.nm r3.nm})
@@ -122,7 +122,7 @@ fun foldUR [tf :: Type] [tr :: {Unit} -> Type]
(f : nm :: Name -> rest :: {Unit}
-> [[nm] ~ rest] =>
tf -> tr rest -> tr ([nm] ++ rest))
- (i : tr []) [r :: {Unit}] (fl : folder r) =
+ (i : tr []) [r ::: {Unit}] (fl : folder r) =
fl [fn r :: {Unit} => $(mapU tf r) -> tr r]
(fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r =>
f [nm] [rest] ! r.nm (acc (r -- nm)))
@@ -132,7 +132,7 @@ fun foldUR2 [tf1 :: Type] [tf2 :: Type] [tr :: {Unit} -> Type]
(f : nm :: Name -> rest :: {Unit}
-> [[nm] ~ rest] =>
tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
- (i : tr []) [r :: {Unit}] (fl : folder r) =
+ (i : tr []) [r ::: {Unit}] (fl : folder r) =
fl [fn r :: {Unit} => $(mapU tf1 r) -> $(mapU tf2 r) -> tr r]
(fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r1 r2 =>
f [nm] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
@@ -142,16 +142,16 @@ fun foldURX2 [tf1 :: Type] [tf2 :: Type] [ctx :: {Unit}]
(f : nm :: Name -> rest :: {Unit}
-> [[nm] ~ rest] =>
tf1 -> tf2 -> xml ctx [] []) =
- foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
- (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] v1 v2 acc =>
- <xml>{f [nm] [rest] ! v1 v2}{acc}</xml>)
- <xml/>
+ @@foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []]
+ (fn [nm :: Name] [rest :: {Unit}] [[nm] ~ rest] v1 v2 acc =>
+ <xml>{f [nm] [rest] ! v1 v2}{acc}</xml>)
+ <xml/>
fun foldR [K] [tf :: K -> Type] [tr :: {K} -> Type]
(f : nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf t -> tr rest -> tr ([nm = t] ++ rest))
- (i : tr []) [r :: {K}] (fl : folder r) =
+ (i : tr []) [r ::: {K}] (fl : folder r) =
fl [fn r :: {K} => $(map tf r) -> tr r]
(fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> tr rest) r =>
f [nm] [t] [rest] ! r.nm (acc (r -- nm)))
@@ -161,7 +161,7 @@ fun foldR2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type]
(f : nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
- (i : tr []) [r :: {K}] (fl : folder r) =
+ (i : tr []) [r ::: {K}] (fl : folder r) =
fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r]
(fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
(acc : _ -> _ -> tr rest) r1 r2 =>
@@ -172,7 +172,7 @@ fun foldR3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {
(f : nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
- (i : tr []) [r :: {K}] (fl : folder r) =
+ (i : tr []) [r ::: {K}] (fl : folder r) =
fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r]
(fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
(acc : _ -> _ -> _ -> tr rest) r1 r2 r3 =>
@@ -183,30 +183,30 @@ fun foldRX [K] [tf :: K -> Type] [ctx :: {Unit}]
(f : nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf t -> xml ctx [] []) =
- foldR [tf] [fn _ => xml ctx [] []]
- (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc =>
- <xml>{f [nm] [t] [rest] ! r}{acc}</xml>)
- <xml/>
+ @@foldR [tf] [fn _ => xml ctx [] []]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc =>
+ <xml>{f [nm] [t] [rest] ! r}{acc}</xml>)
+ <xml/>
fun foldRX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}]
(f : nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf1 t -> tf2 t -> xml ctx [] []) =
- foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
- (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
- r1 r2 acc =>
- <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>)
- <xml/>
+ @@foldR2 [tf1] [tf2] [fn _ => xml ctx [] []]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+ r1 r2 acc =>
+ <xml>{f [nm] [t] [rest] ! r1 r2}{acc}</xml>)
+ <xml/>
fun foldRX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {Unit}]
(f : nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf1 t -> tf2 t -> tf3 t -> xml ctx [] []) =
- foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []]
- (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
- r1 r2 r3 acc =>
- <xml>{f [nm] [t] [rest] ! r1 r2 r3}{acc}</xml>)
- <xml/>
+ @@foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []]
+ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest]
+ r1 r2 r3 acc =>
+ <xml>{f [nm] [t] [rest] ! r1 r2 r3}{acc}</xml>)
+ <xml/>
fun queryL [tables] [exps] [tables ~ exps] (q : sql_query tables exps) =
query q
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index 11547ace..d23b3e01 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -6,7 +6,7 @@ val fold : K --> tf :: ({K} -> Type)
-> (nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] =>
tf r -> tf ([nm = v] ++ r))
-> tf []
- -> r :: {K} -> folder r -> tf r
+ -> r ::: {K} -> folder r -> tf r
structure Folder : sig
val nil : K --> folder (([]) :: {K})
@@ -47,40 +47,40 @@ val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
val map0 : K --> tf :: (K -> Type)
-> (t :: K -> tf t)
- -> r :: {K} -> folder r -> $(map tf r)
+ -> r ::: {K} -> folder r -> $(map tf r)
val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
-> (t ::: K -> tf1 t -> tf2 t)
- -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r)
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r)
val map2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf :: (K -> Type)
-> (t ::: K -> tf1 t -> tf2 t -> tf t)
- -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r)
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r)
val map3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> tf :: (K -> Type)
-> (t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t)
- -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)
val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
-> (nm :: Name -> rest :: {Unit}
-> [[nm] ~ rest] =>
tf -> tr rest -> tr ([nm] ++ rest))
- -> tr [] -> r :: {Unit} -> folder r -> $(mapU tf r) -> tr r
+ -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf r) -> tr r
val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
-> (nm :: Name -> rest :: {Unit}
-> [[nm] ~ rest] =>
tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
- -> tr [] -> r :: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> tr r
+ -> tr [] -> r ::: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> tr r
val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
-> (nm :: Name -> rest :: {Unit}
-> [[nm] ~ rest] =>
tf1 -> tf2 -> xml ctx [] [])
- -> r :: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> xml ctx [] []
+ -> r ::: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> xml ctx [] []
val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type)
-> (nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf t -> tr rest -> tr ([nm = t] ++ rest))
- -> tr [] -> r :: {K} -> folder r -> $(map tf r) -> tr r
+ -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r
val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
-> tr :: ({K} -> Type)
@@ -88,7 +88,7 @@ val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
-> [[nm] ~ rest] =>
tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
-> tr []
- -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
-> tr :: ({K} -> Type)
@@ -96,26 +96,26 @@ val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type
-> [[nm] ~ rest] =>
tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
-> tr []
- -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r
+ -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r
val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit}
-> (nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf t -> xml ctx [] [])
- -> r :: {K} -> folder r -> $(map tf r) -> xml ctx [] []
+ -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] []
val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit}
-> (nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf1 t -> tf2 t -> xml ctx [] [])
- -> r :: {K} -> folder r
+ -> r ::: {K} -> folder r
-> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
val foldRX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> ctx :: {Unit}
-> (nm :: Name -> t :: K -> rest :: {K}
-> [[nm] ~ rest] =>
tf1 t -> tf2 t -> tf3 t -> xml ctx [] [])
- -> r :: {K} -> folder r
+ -> r ::: {K} -> folder r
-> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] []
val queryL : tables ::: {{Type}} -> exps ::: {Type}