summaryrefslogtreecommitdiff
path: root/lib/ur
diff options
context:
space:
mode:
Diffstat (limited to 'lib/ur')
-rw-r--r--lib/ur/basis.urs471
-rw-r--r--lib/ur/top.ur241
-rw-r--r--lib/ur/top.urs183
3 files changed, 895 insertions, 0 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
new file mode 100644
index 00000000..b4a40fde
--- /dev/null
+++ b/lib/ur/basis.urs
@@ -0,0 +1,471 @@
+type int
+type float
+type string
+type time
+
+type unit = {}
+
+datatype bool = False | True
+
+datatype option t = None | Some of t
+
+
+(** Basic type classes *)
+
+class eq
+val eq : t ::: Type -> eq t -> t -> t -> bool
+val ne : t ::: Type -> eq t -> t -> t -> bool
+val eq_int : eq int
+val eq_float : eq float
+val eq_string : eq string
+val eq_bool : eq bool
+val eq_time : eq time
+val mkEq : t ::: Type -> (t -> t -> bool) -> eq t
+
+class num
+val zero : t ::: Type -> num t -> t
+val neg : t ::: Type -> num t -> t -> t
+val plus : t ::: Type -> num t -> t -> t -> t
+val minus : t ::: Type -> num t -> t -> t -> t
+val times : t ::: Type -> num t -> t -> t -> t
+val div : t ::: Type -> num t -> t -> t -> t
+val mod : t ::: Type -> num t -> t -> t -> t
+val num_int : num int
+val num_float : num float
+
+class ord
+val lt : t ::: Type -> ord t -> t -> t -> bool
+val le : t ::: Type -> ord t -> t -> t -> bool
+val gt : t ::: Type -> ord t -> t -> t -> bool
+val ge : t ::: Type -> ord t -> t -> t -> bool
+val ord_int : ord int
+val ord_float : ord float
+val ord_string : ord string
+val ord_bool : ord bool
+val ord_time : ord time
+
+
+(** String operations *)
+
+val strcat : string -> string -> string
+
+class show
+val show : t ::: Type -> show t -> t -> string
+val show_int : show int
+val show_float : show float
+val show_string : show string
+val show_bool : show bool
+val show_time : show time
+val mkShow : t ::: Type -> (t -> string) -> show t
+
+class read
+val read : t ::: Type -> read t -> string -> option t
+val readError : t ::: Type -> read t -> string -> t
+(* [readError] calls [error] if the input is malformed. *)
+val read_int : read int
+val read_float : read float
+val read_string : read string
+val read_bool : read bool
+val read_time : read time
+
+
+(** * Monads *)
+
+class monad :: Type -> Type
+val return : m ::: (Type -> Type) -> t ::: Type
+ -> monad m
+ -> t -> m t
+val bind : m ::: (Type -> Type) -> t1 ::: Type -> t2 ::: Type
+ -> monad m
+ -> m t1 -> (t1 -> m t2)
+ -> m t2
+
+con transaction :: Type -> Type
+val transaction_monad : monad transaction
+
+con source :: Type -> Type
+val source : t ::: Type -> t -> transaction (source t)
+val set : t ::: Type -> source t -> t -> transaction unit
+val get : t ::: Type -> source t -> transaction t
+
+con signal :: Type -> Type
+val signal_monad : monad signal
+val signal : t ::: Type -> source t -> signal t
+
+
+(** HTTP operations *)
+
+val requestHeader : string -> transaction (option string)
+
+con http_cookie :: Type -> Type
+val getCookie : t ::: Type -> http_cookie t -> transaction (option t)
+val setCookie : t ::: Type -> http_cookie t -> t -> transaction unit
+
+
+(** JavaScript-y gadgets *)
+
+val alert : string -> transaction unit
+
+
+(** SQL *)
+
+con sql_table :: {Type} -> Type
+
+(*** Queries *)
+
+con sql_query :: {{Type}} -> {Type} -> Type
+con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type
+con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type
+
+con sql_subset :: {{Type}} -> {{Type}} -> Type
+val sql_subset : keep_drop :: {({Type} * {Type})}
+ -> sql_subset
+ (fold (fn nm (fields :: ({Type} * {Type}))
+ acc [[nm] ~ acc]
+ [fields.1 ~ fields.2] =>
+ [nm = fields.1 ++ fields.2]
+ ++ acc) [] keep_drop)
+ (fold (fn nm (fields :: ({Type} * {Type}))
+ acc [[nm] ~ acc] =>
+ [nm = fields.1] ++ acc)
+ [] keep_drop)
+val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables
+
+val sql_query1 : tables ::: {{Type}}
+ -> grouped ::: {{Type}}
+ -> selectedFields ::: {{Type}}
+ -> selectedExps ::: {Type}
+ -> {From : $(fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
+ [nm = sql_table fields] ++ acc)
+ [] tables),
+ Where : sql_exp tables [] [] bool,
+ GroupBy : sql_subset tables grouped,
+ Having : sql_exp grouped tables [] bool,
+ SelectFields : sql_subset grouped selectedFields,
+ SelectExps : $(fold (fn nm (t :: Type) acc [[nm] ~ acc] =>
+ [nm = sql_exp grouped tables [] t]
+ ++ acc) [] selectedExps) }
+ -> sql_query1 tables selectedFields selectedExps
+
+type sql_relop
+val sql_union : sql_relop
+val sql_intersect : sql_relop
+val sql_except : sql_relop
+val sql_relop : tables1 ::: {{Type}}
+ -> tables2 ::: {{Type}}
+ -> selectedFields ::: {{Type}}
+ -> selectedExps ::: {Type}
+ -> sql_relop
+ -> sql_query1 tables1 selectedFields selectedExps
+ -> sql_query1 tables2 selectedFields selectedExps
+ -> sql_query1 selectedFields selectedFields selectedExps
+
+type sql_direction
+val sql_asc : sql_direction
+val sql_desc : sql_direction
+
+con sql_order_by :: {{Type}} -> {Type} -> Type
+val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps
+val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type
+ -> sql_exp tables [] exps t -> sql_direction
+ -> sql_order_by tables exps
+ -> sql_order_by tables exps
+
+type sql_limit
+val sql_no_limit : sql_limit
+val sql_limit : int -> sql_limit
+
+type sql_offset
+val sql_no_offset : sql_offset
+val sql_offset : int -> sql_offset
+
+val sql_query : tables ::: {{Type}}
+ -> selectedFields ::: {{Type}}
+ -> selectedExps ::: {Type}
+ -> {Rows : sql_query1 tables selectedFields selectedExps,
+ OrderBy : sql_order_by tables selectedExps,
+ Limit : sql_limit,
+ Offset : sql_offset}
+ -> sql_query selectedFields selectedExps
+
+val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type}
+ -> fieldType ::: Type -> agg ::: {{Type}}
+ -> exps ::: {Type}
+ -> tab :: Name -> field :: Name
+ -> sql_exp
+ ([tab = [field = fieldType] ++ otherFields] ++ otherTabs)
+ agg exps fieldType
+
+val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type}
+ -> nm :: Name
+ -> sql_exp tabs agg ([nm = t] ++ rest) t
+
+class sql_injectable
+val sql_bool : sql_injectable bool
+val sql_int : sql_injectable int
+val sql_float : sql_injectable float
+val sql_string : sql_injectable string
+val sql_time : sql_injectable time
+val sql_option_bool : sql_injectable (option bool)
+val sql_option_int : sql_injectable (option int)
+val sql_option_float : sql_injectable (option float)
+val sql_option_string : sql_injectable (option string)
+val sql_option_time : sql_injectable (option time)
+val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> t ::: Type
+ -> sql_injectable t -> t -> sql_exp tables agg exps t
+
+val sql_is_null : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> t ::: Type
+ -> sql_exp tables agg exps (option t)
+ -> sql_exp tables agg exps bool
+
+class sql_arith
+val sql_int_arith : sql_arith int
+val sql_float_arith : sql_arith float
+
+con sql_unary :: Type -> Type -> Type
+val sql_not : sql_unary bool bool
+val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> arg ::: Type -> res ::: Type
+ -> sql_unary arg res -> sql_exp tables agg exps arg
+ -> sql_exp tables agg exps res
+
+val sql_neg : t ::: Type -> sql_arith t -> sql_unary t t
+
+con sql_binary :: Type -> Type -> Type -> Type
+val sql_and : sql_binary bool bool bool
+val sql_or : sql_binary bool bool bool
+val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type
+ -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1
+ -> sql_exp tables agg exps arg2
+ -> sql_exp tables agg exps res
+
+val sql_plus : t ::: Type -> sql_arith t -> sql_binary t t t
+val sql_minus : t ::: Type -> sql_arith t -> sql_binary t t t
+val sql_times : t ::: Type -> sql_arith t -> sql_binary t t t
+val sql_div : t ::: Type -> sql_arith t -> sql_binary t t t
+val sql_mod : sql_binary int int int
+
+val sql_eq : t ::: Type -> sql_binary t t bool
+val sql_ne : t ::: Type -> sql_binary t t bool
+val sql_lt : t ::: Type -> sql_binary t t bool
+val sql_le : t ::: Type -> sql_binary t t bool
+val sql_gt : t ::: Type -> sql_binary t t bool
+val sql_ge : t ::: Type -> sql_binary t t bool
+
+val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> sql_exp tables agg exps int
+
+con sql_aggregate :: Type -> Type
+val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> t ::: Type
+ -> sql_aggregate t -> sql_exp agg agg exps t
+ -> sql_exp tables agg exps t
+
+class sql_summable
+val sql_summable_int : sql_summable int
+val sql_summable_float : sql_summable float
+val sql_avg : t ::: Type -> sql_summable t -> sql_aggregate t
+val sql_sum : t ::: Type -> sql_summable t -> sql_aggregate t
+
+class sql_maxable
+val sql_maxable_int : sql_maxable int
+val sql_maxable_float : sql_maxable float
+val sql_maxable_string : sql_maxable string
+val sql_maxable_time : sql_maxable time
+val sql_max : t ::: Type -> sql_maxable t -> sql_aggregate t
+val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t
+
+con sql_nfunc :: Type -> Type
+val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> t ::: Type
+ -> sql_nfunc t -> sql_exp tables agg exps t
+val sql_current_timestamp : sql_nfunc time
+
+
+(*** Executing queries *)
+
+val query : tables ::: {{Type}} -> exps ::: {Type}
+ -> fn [tables ~ exps] =>
+ state ::: Type
+ -> sql_query tables exps
+ -> ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
+ [nm = $fields] ++ acc) [] tables)
+ -> state
+ -> transaction state)
+ -> state
+ -> transaction state
+
+
+(*** Database mutators *)
+
+type dml
+val dml : dml -> transaction unit
+
+val insert : fields ::: {Type}
+ -> sql_table fields
+ -> $(fold (fn nm (t :: Type) acc [[nm] ~ acc] =>
+ [nm = sql_exp [] [] [] t] ++ acc)
+ [] fields)
+ -> dml
+
+val update : unchanged ::: {Type} -> changed :: {Type} ->
+ fn [changed ~ unchanged] =>
+ $(fold (fn nm (t :: Type) acc [[nm] ~ acc] =>
+ [nm = sql_exp [T = changed ++ unchanged] [] [] t]
+ ++ acc)
+ [] changed)
+ -> sql_table (changed ++ unchanged)
+ -> sql_exp [T = changed ++ unchanged] [] [] bool
+ -> dml
+
+val delete : fields ::: {Type}
+ -> sql_table fields
+ -> sql_exp [T = fields] [] [] bool
+ -> dml
+
+(*** Sequences *)
+
+type sql_sequence
+val nextval : sql_sequence -> transaction int
+
+
+(** XML *)
+
+con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type
+
+
+con xml :: {Unit} -> {Type} -> {Type} -> Type
+val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
+val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type}
+ -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
+ -> useOuter ::: {Type} -> useInner ::: {Type}
+ -> bindOuter ::: {Type} -> bindInner ::: {Type}
+ -> fn [attrsGiven ~ attrsAbsent]
+ [useOuter ~ useInner]
+ [bindOuter ~ bindInner] =>
+ $attrsGiven
+ -> tag (attrsGiven ++ attrsAbsent)
+ ctxOuter ctxInner useOuter bindOuter
+ -> xml ctxInner useInner bindInner
+ -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
+val join : ctx ::: {Unit}
+ -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
+ -> fn [use1 ~ bind1] [bind1 ~ bind2] =>
+ xml ctx use1 bind1
+ -> xml ctx (use1 ++ bind1) bind2
+ -> xml ctx use1 (bind1 ++ bind2)
+val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type}
+ -> bind ::: {Type}
+ -> fn [use1 ~ use2] =>
+ xml ctx use1 bind
+ -> xml ctx (use1 ++ use2) bind
+
+con xhtml = xml [Html]
+con page = xhtml [] []
+con xbody = xml [Body] [] []
+con xtr = xml [Body, Tr] [] []
+con xform = xml [Body, Form] [] []
+
+(*** HTML details *)
+
+con html = [Html]
+con head = [Head]
+con body = [Body]
+con form = [Body, Form]
+con tabl = [Body, Table]
+con tr = [Body, Tr]
+
+val dyn : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> unit
+ -> tag [Signal = signal (xml ctx use bind)] ctx [] use bind
+
+val head : unit -> tag [] html head [] []
+val title : unit -> tag [] head [] [] []
+
+val body : unit -> tag [] html body [] []
+con bodyTag = fn (attrs :: {Type}) =>
+ ctx ::: {Unit} ->
+ fn [[Body] ~ ctx] =>
+ unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
+con bodyTagStandalone = fn (attrs :: {Type}) =>
+ ctx ::: {Unit}
+ -> fn [[Body] ~ ctx] =>
+ unit -> tag attrs ([Body] ++ ctx) [] [] []
+
+val br : bodyTagStandalone []
+
+val p : bodyTag []
+val b : bodyTag []
+val i : bodyTag []
+val tt : bodyTag []
+val font : bodyTag [Size = int, Face = string]
+
+val h1 : bodyTag []
+val h2 : bodyTag []
+val h3 : bodyTag []
+val h4 : bodyTag []
+
+val li : bodyTag []
+val ol : bodyTag []
+val ul : bodyTag []
+
+val hr : bodyTag []
+
+val a : bodyTag [Link = transaction page, Onclick = transaction unit]
+
+val form : ctx ::: {Unit} -> bind ::: {Type}
+ -> fn [[Body] ~ ctx] =>
+ xml form [] bind
+ -> xml ([Body] ++ ctx) [] []
+con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) =>
+ ctx ::: {Unit}
+ -> fn [[Form] ~ ctx] =>
+ nm :: Name -> unit
+ -> tag attrs ([Form] ++ ctx) inner [] [nm = ty]
+val textbox : formTag string [] [Value = string, Size = int, Source = source string]
+val password : formTag string [] [Value = string, Size = int]
+val textarea : formTag string [] [Rows = int, Cols = int]
+
+val checkbox : formTag bool [] [Checked = bool]
+
+con radio = [Body, Radio]
+val radio : formTag string radio []
+val radioOption : unit -> tag [Value = string] radio [] [] []
+
+con select = [Select]
+val select : formTag string select []
+val option : unit -> tag [Value = string, Selected = bool] select [] [] []
+
+val submit : ctx ::: {Unit} -> use ::: {Type}
+ -> fn [[Form] ~ ctx] =>
+ unit
+ -> tag [Value = string, Action = $use -> transaction page]
+ ([Form] ++ ctx) ([Form] ++ ctx) use []
+
+(*** AJAX-oriented widgets *)
+
+con cformTag = fn (attrs :: {Type}) =>
+ ctx ::: {Unit}
+ -> fn [[Body] ~ ctx] =>
+ unit -> tag attrs ([Body] ++ ctx) [] [] []
+
+val ctextbox : cformTag [Value = string, Size = int, Source = source string]
+val button : cformTag [Value = string, Onclick = transaction unit]
+
+(*** Tables *)
+
+val tabl : other ::: {Unit} -> fn [other ~ [Body, Table]] =>
+ unit -> tag [Border = int] ([Body] ++ other) ([Body, Table] ++ other) [] []
+val tr : other ::: {Unit} -> fn [other ~ [Body, Table, Tr]] =>
+ unit -> tag [] ([Body, Table] ++ other) ([Body, Tr] ++ other) [] []
+val th : other ::: {Unit} -> fn [other ~ [Body, Tr]] =>
+ unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] []
+val td : other ::: {Unit} -> fn [other ~ [Body, Tr]] =>
+ unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] []
+
+
+(** Aborting *)
+
+val error : t ::: Type -> xml [Body] [] [] -> t
diff --git a/lib/ur/top.ur b/lib/ur/top.ur
new file mode 100644
index 00000000..35e8519b
--- /dev/null
+++ b/lib/ur/top.ur
@@ -0,0 +1,241 @@
+fun not b = if b then False else True
+
+con idT (t :: Type) = t
+con record (t :: {Type}) = $t
+con fstTT (t :: (Type * Type)) = t.1
+con sndTT (t :: (Type * Type)) = t.2
+con fstTTT (t :: (Type * Type * Type)) = t.1
+con sndTTT (t :: (Type * Type * Type)) = t.2
+con thdTTT (t :: (Type * Type * Type)) = t.3
+
+con mapTT (f :: Type -> Type) = fold (fn nm t acc [[nm] ~ acc] =>
+ [nm = f t] ++ acc) []
+
+con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] =>
+ [nm = f] ++ acc) []
+
+con mapT2T (f :: (Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] =>
+ [nm = f t] ++ acc) []
+
+con mapT3T (f :: (Type * Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] =>
+ [nm = f t] ++ acc) []
+
+con ex = fn tf :: (Type -> Type) =>
+ res ::: Type -> (choice :: Type -> tf choice -> res) -> res
+
+fun ex (tf :: (Type -> Type)) (choice :: Type) (body : tf choice) : ex tf =
+ fn (res ::: Type) (f : choice :: Type -> tf choice -> res) =>
+ f [choice] body
+
+fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type)
+ (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x)
+
+fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (_ : show t) (v : t) =
+ cdata (show v)
+
+fun foldUR (tf :: Type) (tr :: {Unit} -> Type)
+ (f : nm :: Name -> rest :: {Unit}
+ -> fn [[nm] ~ rest] =>
+ tf -> tr rest -> tr ([nm] ++ rest))
+ (i : tr []) =
+ fold [fn r :: {Unit} => $(mapUT tf r) -> tr r]
+ (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
+ [[nm] ~ rest] r =>
+ f [nm] [rest] r.nm (acc (r -- nm)))
+ (fn _ => i)
+
+fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type)
+ (f : nm :: Name -> rest :: {Unit}
+ -> fn [[nm] ~ rest] =>
+ tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
+ (i : tr []) =
+ fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r]
+ (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc
+ [[nm] ~ rest] r1 r2 =>
+ f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+ (fn _ _ => i)
+
+fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit})
+ (f : nm :: Name -> rest :: {Unit}
+ -> fn [[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/>
+
+fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
+ (f : nm :: Name -> t :: Type -> rest :: {Type}
+ -> fn [[nm] ~ rest] =>
+ tf t -> tr rest -> tr ([nm = t] ++ rest))
+ (i : tr []) =
+ fold [fn r :: {Type} => $(mapTT tf r) -> tr r]
+ (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest)
+ [[nm] ~ rest] r =>
+ f [nm] [t] [rest] r.nm (acc (r -- nm)))
+ (fn _ => i)
+
+fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
+ (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf t -> tr rest -> tr ([nm = t] ++ rest))
+ (i : tr []) =
+ fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r]
+ (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
+ (acc : _ -> tr rest) [[nm] ~ rest] r =>
+ f [nm] [t] [rest] r.nm (acc (r -- nm)))
+ (fn _ => i)
+
+fun foldT3R (tf :: (Type * Type * Type) -> Type) (tr :: {(Type * Type * Type)} -> Type)
+ (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf t -> tr rest -> tr ([nm = t] ++ rest))
+ (i : tr []) =
+ fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf r) -> tr r]
+ (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
+ (acc : _ -> tr rest) [[nm] ~ rest] r =>
+ f [nm] [t] [rest] r.nm (acc (r -- nm)))
+ (fn _ => i)
+
+fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
+ (f : nm :: Name -> t :: Type -> rest :: {Type}
+ -> fn [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+ (i : tr []) =
+ fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r]
+ (fn (nm :: Name) (t :: Type) (rest :: {Type})
+ (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
+ f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+ (fn _ _ => i)
+
+fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type)
+ (tr :: {(Type * Type)} -> Type)
+ (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+ (i : tr []) =
+ fold [fn r :: {(Type * Type)} => $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r]
+ (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
+ (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
+ f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+ (fn _ _ => i)
+
+fun foldT3R2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type)
+ (tr :: {(Type * Type * Type)} -> Type)
+ (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+ (i : tr []) =
+ fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r]
+ (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
+ (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 =>
+ f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
+ (fn _ _ => i)
+
+fun foldTRX (tf :: Type -> Type) (ctx :: {Unit})
+ (f : nm :: Name -> t :: Type -> rest :: {Type}
+ -> fn [[nm] ~ rest] =>
+ tf t -> xml ctx [] []) =
+ foldTR [tf] [fn _ => xml ctx [] []]
+ (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] r acc =>
+ <xml>{f [nm] [t] [rest] r}{acc}</xml>)
+ <xml/>
+
+fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit})
+ (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf t -> xml ctx [] []) =
+ foldT2R [tf] [fn _ => xml ctx [] []]
+ (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
+ [[nm] ~ rest] r acc =>
+ <xml>{f [nm] [t] [rest] r}{acc}</xml>)
+ <xml/>
+
+fun foldT3RX (tf :: (Type * Type * Type) -> Type) (ctx :: {Unit})
+ (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf t -> xml ctx [] []) =
+ foldT3R [tf] [fn _ => xml ctx [] []]
+ (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
+ [[nm] ~ rest] r acc =>
+ <xml>{f [nm] [t] [rest] r}{acc}</xml>)
+ <xml/>
+
+fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
+ (f : nm :: Name -> t :: Type -> rest :: {Type}
+ -> fn [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> xml ctx [] []) =
+ foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []]
+ (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest]
+ r1 r2 acc =>
+ <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
+ <xml/>
+
+fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type)
+ (ctx :: {Unit})
+ (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> xml ctx [] []) =
+ foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []]
+ (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)})
+ [[nm] ~ rest] r1 r2 acc =>
+ <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
+ <xml/>
+
+fun foldT3RX2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type)
+ (ctx :: {Unit})
+ (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> xml ctx [] []) =
+ foldT3R2 [tf1] [tf2] [fn _ => xml ctx [] []]
+ (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)})
+ [[nm] ~ rest] r1 r2 acc =>
+ <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
+ <xml/>
+
+fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
+ (q : sql_query tables exps) [tables ~ exps]
+ (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
+ [nm = $fields] ++ acc) [] tables)
+ -> xml ctx [] []) =
+ query q
+ (fn fs acc => return <xml>{acc}{f fs}</xml>)
+ <xml/>
+
+fun queryX' (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit})
+ (q : sql_query tables exps) [tables ~ exps]
+ (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
+ [nm = $fields] ++ acc) [] tables)
+ -> transaction (xml ctx [] [])) =
+ query q
+ (fn fs acc =>
+ r <- f fs;
+ return <xml>{acc}{r}</xml>)
+ <xml/>
+
+fun oneOrNoRows (tables ::: {{Type}}) (exps ::: {Type})
+ (q : sql_query tables exps) [tables ~ exps] =
+ query q
+ (fn fs _ => return (Some fs))
+ None
+
+fun oneRow (tables ::: {{Type}}) (exps ::: {Type})
+ (q : sql_query tables exps) [tables ~ exps] =
+ o <- oneOrNoRows q;
+ return (case o of
+ None => error <xml>Query returned no rows</xml>
+ | Some r => r)
+
+fun eqNullable (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type})
+ (t ::: Type) (_ : sql_injectable (option t))
+ (e1 : sql_exp tables agg exps (option t))
+ (e2 : sql_exp tables agg exps (option t)) =
+ (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2})
+
+fun eqNullable' (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type})
+ (t ::: Type) (_ : sql_injectable (option t))
+ (e1 : sql_exp tables agg exps (option t))
+ (e2 : option t) =
+ case e2 of
+ None => (SQL {e1} IS NULL)
+ | Some _ => sql_binary sql_eq e1 (sql_inject e2)
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
new file mode 100644
index 00000000..d6315b92
--- /dev/null
+++ b/lib/ur/top.urs
@@ -0,0 +1,183 @@
+val not : bool -> bool
+
+con idT = fn t :: Type => t
+con record = fn t :: {Type} => $t
+con fstTT = fn t :: (Type * Type) => t.1
+con sndTT = fn t :: (Type * Type) => t.2
+con fstTTT = fn t :: (Type * Type * Type) => t.1
+con sndTTT = fn t :: (Type * Type * Type) => t.2
+con thdTTT = fn t :: (Type * Type * Type) => t.3
+
+con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] =>
+ [nm = f t] ++ acc) []
+
+con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] =>
+ [nm = f] ++ acc) []
+
+con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] =>
+ [nm = f t] ++ acc) []
+
+con mapT3T = fn f :: (Type * Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] =>
+ [nm = f t] ++ acc) []
+
+con ex = fn tf :: (Type -> Type) =>
+ res ::: Type -> (choice :: Type -> tf choice -> res) -> res
+
+val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf
+
+val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type
+ -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3)
+
+val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
+ -> xml ctx use []
+
+val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
+ -> (nm :: Name -> rest :: {Unit}
+ -> fn [[nm] ~ rest] =>
+ tf -> tr rest -> tr ([nm] ++ rest))
+ -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r
+
+val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
+ -> (nm :: Name -> rest :: {Unit}
+ -> fn [[nm] ~ rest] =>
+ tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
+ -> tr [] -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
+
+val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
+ -> (nm :: Name -> rest :: {Unit}
+ -> fn [[nm] ~ rest] =>
+ tf1 -> tf2 -> xml ctx [] [])
+ -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
+
+val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
+ -> (nm :: Name -> t :: Type -> rest :: {Type}
+ -> fn [[nm] ~ rest] =>
+ tf t -> tr rest -> tr ([nm = t] ++ rest))
+ -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r
+
+val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type)
+ -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf t -> tr rest -> tr ([nm = t] ++ rest))
+ -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r
+
+val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type)
+ -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf t -> tr rest -> tr ([nm = t] ++ rest))
+ -> tr [] -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> tr r
+
+val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type)
+ -> tr :: ({Type} -> Type)
+ -> (nm :: Name -> t :: Type -> rest :: {Type}
+ -> fn [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+ -> tr []
+ -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r
+
+val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
+ -> tr :: ({(Type * Type)} -> Type)
+ -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+ -> tr [] -> r :: {(Type * Type)}
+ -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r
+
+val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
+ -> tr :: ({(Type * Type * Type)} -> Type)
+ -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+ -> tr [] -> r :: {(Type * Type * Type)}
+ -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r
+
+val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
+ -> (nm :: Name -> t :: Type -> rest :: {Type}
+ -> fn [[nm] ~ rest] =>
+ tf t -> xml ctx [] [])
+ -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] []
+
+val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit}
+ -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf t -> xml ctx [] [])
+ -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] []
+
+val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit}
+ -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf t -> xml ctx [] [])
+ -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> xml ctx [] []
+
+val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
+ -> (nm :: Name -> t :: Type -> rest :: {Type}
+ -> fn [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> xml ctx [] [])
+ -> r :: {Type}
+ -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] []
+
+val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
+ -> ctx :: {Unit}
+ -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> xml ctx [] [])
+ -> r :: {(Type * Type)}
+ -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] []
+
+
+val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
+ -> ctx :: {Unit}
+ -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
+ -> fn [[nm] ~ rest] =>
+ tf1 t -> tf2 t -> xml ctx [] [])
+ -> r :: {(Type * Type * Type)}
+ -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> xml ctx [] []
+
+val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
+ -> sql_query tables exps
+ -> fn [tables ~ exps] =>
+ ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
+ [nm = $fields] ++ acc) [] tables)
+ -> xml ctx [] [])
+ -> transaction (xml ctx [] [])
+
+val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
+ -> sql_query tables exps
+ -> fn [tables ~ exps] =>
+ ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
+ [nm = $fields] ++ acc) [] tables)
+ -> transaction (xml ctx [] []))
+ -> transaction (xml ctx [] [])
+
+val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
+ -> sql_query tables exps
+ -> fn [tables ~ exps] =>
+ transaction
+ (option
+ $(exps
+ ++ fold (fn nm (fields :: {Type}) acc
+ [[nm] ~ acc] =>
+ [nm = $fields] ++ acc)
+ [] tables))
+
+val oneRow : tables ::: {{Type}} -> exps ::: {Type}
+ -> sql_query tables exps
+ -> fn [tables ~ exps] =>
+ transaction
+ $(exps
+ ++ fold (fn nm (fields :: {Type}) acc
+ [[nm] ~ acc] =>
+ [nm = $fields] ++ acc)
+ [] tables)
+
+val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> t ::: Type -> sql_injectable (option t)
+ -> sql_exp tables agg exps (option t)
+ -> sql_exp tables agg exps (option t)
+ -> sql_exp tables agg exps bool
+
+val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
+ -> t ::: Type -> sql_injectable (option t)
+ -> sql_exp tables agg exps (option t)
+ -> option t
+ -> sql_exp tables agg exps bool
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-18 21:07:29 +0000