Mercurial > urweb

annotate lib/ur/top.urs @ 621:8998114760c1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
"Hello world" compiles, after replacing type-level fold with map
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 15:33:20 -0500
parents 1d34d916c206
children 588b9d16b00a
rev   line source
adamc@422 1 val not : bool -> bool
adamc@422 2
adamc@329 3 con idT = fn t :: Type => t
adamc@329 4 con record = fn t :: {Type} => $t
adamc@339 5 con fstTT = fn t :: (Type * Type) => t.1
adamc@339 6 con sndTT = fn t :: (Type * Type) => t.2
adamc@445 7 con fstTTT = fn t :: (Type * Type * Type) => t.1
adamc@445 8 con sndTTT = fn t :: (Type * Type * Type) => t.2
adamc@445 9 con thdTTT = fn t :: (Type * Type * Type) => t.3
adamc@329 10
adamc@621 11 con mapUT = fn f :: Type => map (fn _ :: Unit => f)
adamc@445 12
adamc@339 13 con ex = fn tf :: (Type -> Type) =>
adamc@355 14 res ::: Type -> (choice :: Type -> tf choice -> res) -> res
adamc@339 15
adamc@339 16 val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf
adamc@339 17
adamc@325 18 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type
adamc@355 19 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3)
adamc@325 20
adamc@325 21 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
adamc@355 22 -> xml ctx use []
adamc@329 23
adamc@411 24 val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
adamc@411 25 -> (nm :: Name -> rest :: {Unit}
adamc@411 26 -> fn [[nm] ~ rest] =>
adamc@411 27 tf -> tr rest -> tr ([nm] ++ rest))
adamc@411 28 -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r
adamc@411 29
adamc@418 30 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
adamc@418 31 -> (nm :: Name -> rest :: {Unit}
adamc@418 32 -> fn [[nm] ~ rest] =>
adamc@418 33 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
adamc@418 34 -> tr [] -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
adamc@418 35
adamc@418 36 val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
adamc@418 37 -> (nm :: Name -> rest :: {Unit}
adamc@418 38 -> fn [[nm] ~ rest] =>
adamc@418 39 tf1 -> tf2 -> xml ctx [] [])
adamc@418 40 -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
adamc@418 41
adamc@336 42 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
adamc@355 43 -> (nm :: Name -> t :: Type -> rest :: {Type}
adamc@355 44 -> fn [[nm] ~ rest] =>
adamc@355 45 tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@621 46 -> tr [] -> r :: {Type} -> $(map tf r) -> tr r
adamc@336 47
adamc@339 48 val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type)
adamc@355 49 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
adamc@355 50 -> fn [[nm] ~ rest] =>
adamc@355 51 tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@621 52 -> tr [] -> r :: {(Type * Type)} -> $(map tf r) -> tr r
adamc@339 53
adamc@445 54 val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type)
adamc@445 55 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
adamc@445 56 -> fn [[nm] ~ rest] =>
adamc@445 57 tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@621 58 -> tr [] -> r :: {(Type * Type * Type)} -> $(map tf r) -> tr r
adamc@445 59
adamc@355 60 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type)
adamc@355 61 -> tr :: ({Type} -> Type)
adamc@355 62 -> (nm :: Name -> t :: Type -> rest :: {Type}
adamc@355 63 -> fn [[nm] ~ rest] =>
adamc@355 64 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@355 65 -> tr []
adamc@621 66 -> r :: {Type} -> $(map tf1 r) -> $(map tf2 r) -> tr r
adamc@355 67
adamc@339 68 val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
adamc@355 69 -> tr :: ({(Type * Type)} -> Type)
adamc@355 70 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
adamc@355 71 -> fn [[nm] ~ rest] =>
adamc@355 72 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@355 73 -> tr [] -> r :: {(Type * Type)}
adamc@621 74 -> $(map tf1 r) -> $(map tf2 r) -> tr r
adamc@339 75
adamc@445 76 val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
adamc@445 77 -> tr :: ({(Type * Type * Type)} -> Type)
adamc@445 78 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
adamc@445 79 -> fn [[nm] ~ rest] =>
adamc@445 80 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@445 81 -> tr [] -> r :: {(Type * Type * Type)}
adamc@621 82 -> $(map tf1 r) -> $(map tf2 r) -> tr r
adamc@445 83
adamc@336 84 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
adamc@355 85 -> (nm :: Name -> t :: Type -> rest :: {Type}
adamc@355 86 -> fn [[nm] ~ rest] =>
adamc@355 87 tf t -> xml ctx [] [])
adamc@621 88 -> r :: {Type} -> $(map tf r) -> xml ctx [] []
adamc@336 89
adamc@339 90 val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit}
adamc@355 91 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
adamc@355 92 -> fn [[nm] ~ rest] =>
adamc@355 93 tf t -> xml ctx [] [])
adamc@621 94 -> r :: {(Type * Type)} -> $(map tf r) -> xml ctx [] []
adamc@339 95
adamc@445 96 val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit}
adamc@445 97 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
adamc@445 98 -> fn [[nm] ~ rest] =>
adamc@445 99 tf t -> xml ctx [] [])
adamc@621 100 -> r :: {(Type * Type * Type)} -> $(map tf r) -> xml ctx [] []
adamc@445 101
adamc@332 102 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
adamc@355 103 -> (nm :: Name -> t :: Type -> rest :: {Type}
adamc@355 104 -> fn [[nm] ~ rest] =>
adamc@355 105 tf1 t -> tf2 t -> xml ctx [] [])
adamc@355 106 -> r :: {Type}
adamc@621 107 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
adamc@334 108
adamc@355 109 val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
adamc@355 110 -> ctx :: {Unit}
adamc@355 111 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
adamc@355 112 -> fn [[nm] ~ rest] =>
adamc@355 113 tf1 t -> tf2 t -> xml ctx [] [])
adamc@355 114 -> r :: {(Type * Type)}
adamc@621 115 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
adamc@339 116
adamc@445 117
adamc@445 118 val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type)
adamc@445 119 -> ctx :: {Unit}
adamc@445 120 -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)}
adamc@445 121 -> fn [[nm] ~ rest] =>
adamc@445 122 tf1 t -> tf2 t -> xml ctx [] [])
adamc@445 123 -> r :: {(Type * Type * Type)}
adamc@621 124 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
adamc@445 125
adamc@334 126 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
adamc@355 127 -> sql_query tables exps
adamc@355 128 -> fn [tables ~ exps] =>
adamc@621 129 ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@355 130 -> xml ctx [] [])
adamc@355 131 -> transaction (xml ctx [] [])
adamc@341 132
adamc@469 133 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
adamc@469 134 -> sql_query tables exps
adamc@469 135 -> fn [tables ~ exps] =>
adamc@621 136 ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@469 137 -> transaction (xml ctx [] []))
adamc@469 138 -> transaction (xml ctx [] [])
adamc@469 139
adamc@355 140 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
adamc@355 141 -> sql_query tables exps
adamc@355 142 -> fn [tables ~ exps] =>
adamc@355 143 transaction
adamc@355 144 (option
adamc@355 145 $(exps
adamc@621 146 ++ map (fn fields :: {Type} => $fields) tables))
adamc@440 147
adamc@440 148 val oneRow : tables ::: {{Type}} -> exps ::: {Type}
adamc@440 149 -> sql_query tables exps
adamc@440 150 -> fn [tables ~ exps] =>
adamc@440 151 transaction
adamc@440 152 $(exps
adamc@621 153 ++ map (fn fields :: {Type} => $fields) tables)
adamc@470 154
adamc@470 155 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@470 156 -> t ::: Type -> sql_injectable (option t)
adamc@470 157 -> sql_exp tables agg exps (option t)
adamc@470 158 -> sql_exp tables agg exps (option t)
adamc@470 159 -> sql_exp tables agg exps bool
adamc@470 160
adamc@470 161 val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@470 162 -> t ::: Type -> sql_injectable (option t)
adamc@470 163 -> sql_exp tables agg exps (option t)
adamc@470 164 -> option t
adamc@470 165 -> sql_exp tables agg exps bool