Mercurial > urweb

comparison lib/top.urs @ 339:075b36dbb1a4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Crud supports INSERT
author Adam Chlipala <adamc@hcoop.net>
date Sun, 14 Sep 2008 15:10:04 -0400
parents 34847732cefc
children 389399d65331
comparison
equal deleted inserted replaced
338:e976b187d73a 339:075b36dbb1a4
1 con idT = fn t :: Type => t 1 con idT = fn t :: Type => t
2 con record = fn t :: {Type} => $t 2 con record = fn t :: {Type} => $t
3 con fstTT = fn t :: (Type * Type) => t.1
4 con sndTT = fn t :: (Type * Type) => t.2
3 5
4 con mapTT = fn f :: Type -> Type => fold (fn nm t acc => [nm] ~ acc => 6 con mapTT = fn f :: Type -> Type => fold (fn nm t acc => [nm] ~ acc =>
5 [nm = f t] ++ acc) [] 7 [nm = f t] ++ acc) []
8
9 con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc => [nm] ~ acc =>
10 [nm = f t] ++ acc) []
11
12 con ex = fn tf :: (Type -> Type) =>
13 res ::: Type -> (choice :: Type -> tf choice -> res) -> res
14
15 val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf
6 16
7 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type 17 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type
8 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3) 18 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3)
9 19
10 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t 20 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
13 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type) 23 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
14 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest 24 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
15 -> tf t -> tr rest -> tr ([nm = t] ++ rest)) 25 -> tf t -> tr rest -> tr ([nm = t] ++ rest))
16 -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r 26 -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r
17 27
28 val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type)
29 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
30 -> tf t -> tr rest -> tr ([nm = t] ++ rest))
31 -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r
32
18 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type) 33 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type)
19 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest 34 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
20 -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 35 -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
21 -> tr [] -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r 36 -> tr [] -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r
37
38 val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
39 -> tr :: ({(Type * Type)} -> Type)
40 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
41 -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
42 -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r
22 43
23 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit} 44 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
24 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest 45 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
25 -> tf t -> xml ctx [] []) 46 -> tf t -> xml ctx [] [])
26 -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] [] 47 -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] []
27 48
49 val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit}
50 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
51 -> tf t -> xml ctx [] [])
52 -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] []
53
28 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit} 54 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
29 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest 55 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
30 -> tf1 t -> tf2 t -> xml ctx [] []) 56 -> tf1 t -> tf2 t -> xml ctx [] [])
31 -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] [] 57 -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] []
58
59 val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> ctx :: {Unit}
60 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
61 -> tf1 t -> tf2 t -> xml ctx [] [])
62 -> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] []
32 63
33 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} 64 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
34 -> sql_query tables exps -> tables ~ exps 65 -> sql_query tables exps -> tables ~ exps
35 -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables) 66 -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
36 -> xml ctx [] []) 67 -> xml ctx [] [])