Mercurial > urweb

annotate lib/top.ur @ 354:527529a083d9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Basis indents and type-checks with new twiddle syntax
author Adam Chlipala <adamc@hcoop.net>
date Sun, 12 Oct 2008 11:44:43 -0400
parents b85e6ba56618
children 383c72d11db8
rev   line source
adamc@329 1 con idT = fn t :: Type => t
adamc@329 2 con record = fn t :: {Type} => $t
adamc@339 3 con fstTT = fn t :: (Type * Type) => t.1
adamc@339 4 con sndTT = fn t :: (Type * Type) => t.2
adamc@329 5
adamc@325 6 con mapTT (f :: Type -> Type) = fold (fn nm t acc => [nm] ~ acc =>
adamc@325 7 [nm = f t] ++ acc) []
adamc@325 8
adamc@339 9 con mapT2T (f :: (Type * Type) -> Type) = fold (fn nm t acc => [nm] ~ acc =>
adamc@339 10 [nm = f t] ++ acc) []
adamc@339 11
adamc@339 12 con ex = fn tf :: (Type -> Type) =>
adamc@339 13 res ::: Type -> (choice :: Type -> tf choice -> res) -> res
adamc@339 14
adamc@339 15 fun ex (tf :: (Type -> Type)) (choice :: Type) (body : tf choice) : ex tf =
adamc@339 16 fn (res ::: Type) (f : choice :: Type -> tf choice -> res) =>
adamc@339 17 f [choice] body
adamc@339 18
adamc@325 19 fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type) (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x)
adamc@325 20
adamc@325 21 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) = cdata (show sh v)
adamc@328 22
adamc@336 23 fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
adamc@336 24 (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
adamc@345 25 => tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@336 26 (i : tr []) =
adamc@336 27 fold [fn r :: {Type} => $(mapTT tf r) -> tr r]
adamc@336 28 (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest) =>
adamc@336 29 [[nm] ~ rest] =>
adamc@336 30 fn r => f [nm] [t] [rest] r.nm (acc (r -- nm)))
adamc@336 31 (fn _ => i)
adamc@336 32
adamc@339 33 fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
adamc@339 34 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
adamc@345 35 => tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@339 36 (i : tr []) =
adamc@339 37 fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r]
adamc@339 38 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> tr rest) =>
adamc@339 39 [[nm] ~ rest] =>
adamc@339 40 fn r => f [nm] [t] [rest] r.nm (acc (r -- nm)))
adamc@339 41 (fn _ => i)
adamc@339 42
adamc@330 43 fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
adamc@328 44 (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
adamc@345 45 => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@328 46 (i : tr []) =
adamc@328 47 fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r]
adamc@328 48 (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> _ -> tr rest) =>
adamc@328 49 [[nm] ~ rest] =>
adamc@328 50 fn r1 r2 => f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
adamc@328 51 (fn _ _ => i)
adamc@332 52
adamc@339 53 fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
adamc@339 54 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
adamc@345 55 => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@339 56 (i : tr []) =
adamc@339 57 fold [fn r :: {(Type * Type)} => $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r]
adamc@339 58 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> _ -> tr rest) =>
adamc@339 59 [[nm] ~ rest] =>
adamc@339 60 fn r1 r2 => f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm)))
adamc@339 61 (fn _ _ => i)
adamc@339 62
adamc@336 63 fun foldTRX (tf :: Type -> Type) (ctx :: {Unit})
adamc@336 64 (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
adamc@345 65 => tf t -> xml ctx [] []) =
adamc@336 66 foldTR [tf] [fn _ => xml ctx [] []]
adamc@336 67 (fn (nm :: Name) (t :: Type) (rest :: {Type}) =>
adamc@336 68 [[nm] ~ rest] =>
adamc@336 69 fn r acc => <xml>{f [nm] [t] [rest] r}{acc}</xml>)
adamc@336 70 <xml></xml>
adamc@336 71
adamc@339 72 fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit})
adamc@339 73 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
adamc@345 74 => tf t -> xml ctx [] []) =
adamc@339 75 foldT2R [tf] [fn _ => xml ctx [] []]
adamc@339 76 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) =>
adamc@339 77 [[nm] ~ rest] =>
adamc@339 78 fn r acc => <xml>{f [nm] [t] [rest] r}{acc}</xml>)
adamc@339 79 <xml></xml>
adamc@339 80
adamc@332 81 fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
adamc@332 82 (f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
adamc@345 83 => tf1 t -> tf2 t -> xml ctx [] []) =
adamc@332 84 foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []]
adamc@332 85 (fn (nm :: Name) (t :: Type) (rest :: {Type}) =>
adamc@332 86 [[nm] ~ rest] =>
adamc@332 87 fn r1 r2 acc => <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
adamc@332 88 <xml></xml>
adamc@334 89
adamc@339 90 fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (ctx :: {Unit})
adamc@339 91 (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
adamc@345 92 => tf1 t -> tf2 t -> xml ctx [] []) =
adamc@339 93 foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []]
adamc@339 94 (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) =>
adamc@339 95 [[nm] ~ rest] =>
adamc@339 96 fn r1 r2 acc => <xml>{f [nm] [t] [rest] r1 r2}{acc}</xml>)
adamc@339 97 <xml></xml>
adamc@339 98
adamc@334 99 fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) (q : sql_query tables exps) =
adamc@334 100 [tables ~ exps] =>
adamc@334 101 fn (f : $(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
adamc@334 102 -> xml ctx [] []) =>
adamc@334 103 query q
adamc@334 104 (fn fs acc => return <xml>{acc}{f fs}</xml>)
adamc@334 105 <xml></xml>
adamc@341 106
adamc@341 107 fun oneOrNoRows (tables ::: {{Type}}) (exps ::: {Type}) (q : sql_query tables exps) =
adamc@341 108 [tables ~ exps] =>
adamc@341 109 query q
adamc@341 110 (fn fs _ => return (Some fs))
adamc@341 111 None