Mercurial > urweb

comparison lib/top.urs @ 355:fa2d25fe75ce

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
top.urs indents and type-checks with new twiddle syntax
author Adam Chlipala <adamc@hcoop.net>
date Sun, 12 Oct 2008 11:50:21 -0400
parents b85e6ba56618
children 06fcddcd20d3
comparison
equal deleted inserted replaced
354:527529a083d9 355:fa2d25fe75ce
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 3 con fstTT = fn t :: (Type * Type) => t.1
4 con sndTT = fn t :: (Type * Type) => t.2 4 con sndTT = fn t :: (Type * Type) => t.2
5 5
6 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] =>
7 [nm = f t] ++ acc) [] 7 [nm = f t] ++ acc) []
8 8
9 con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc => [nm] ~ acc => 9 con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] =>
10 [nm = f t] ++ acc) [] 10 [nm = f t] ++ acc) []
11 11
12 con ex = fn tf :: (Type -> Type) => 12 con ex = fn tf :: (Type -> Type) =>
13 res ::: Type -> (choice :: Type -> tf choice -> res) -> res 13 res ::: Type -> (choice :: Type -> tf choice -> res) -> res
14 14
15 val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf 15 val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf
16 16
17 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type 17 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type
18 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3) 18 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3)
19 19
20 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t 20 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
21 -> xml ctx use [] 21 -> xml ctx use []
22 22
23 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type) 23 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
24 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest 24 -> (nm :: Name -> t :: Type -> rest :: {Type}
25 => tf t -> tr rest -> tr ([nm = t] ++ rest)) 25 -> fn [[nm] ~ rest] =>
26 -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r 26 tf t -> tr rest -> tr ([nm = t] ++ rest))
27 -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r
27 28
28 val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type) 29 val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type)
29 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest 30 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
30 => tf t -> tr rest -> tr ([nm = t] ++ rest)) 31 -> fn [[nm] ~ rest] =>
31 -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r 32 tf t -> tr rest -> tr ([nm = t] ++ rest))
33 -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r
32 34
33 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type) 35 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type)
34 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest 36 -> tr :: ({Type} -> Type)
35 => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 37 -> (nm :: Name -> t :: Type -> rest :: {Type}
36 -> tr [] -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r 38 -> fn [[nm] ~ rest] =>
37 39 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
40 -> tr []
41 -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r
42
38 val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) 43 val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
39 -> tr :: ({(Type * Type)} -> Type) 44 -> tr :: ({(Type * Type)} -> Type)
40 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest 45 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
41 => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 46 -> fn [[nm] ~ rest] =>
42 -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r 47 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
48 -> tr [] -> r :: {(Type * Type)}
49 -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r
43 50
44 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit} 51 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
45 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest 52 -> (nm :: Name -> t :: Type -> rest :: {Type}
46 => tf t -> xml ctx [] []) 53 -> fn [[nm] ~ rest] =>
47 -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] [] 54 tf t -> xml ctx [] [])
55 -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] []
48 56
49 val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit} 57 val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit}
50 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest 58 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
51 => tf t -> xml ctx [] []) 59 -> fn [[nm] ~ rest] =>
52 -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] [] 60 tf t -> xml ctx [] [])
61 -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] []
53 62
54 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit} 63 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
55 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest 64 -> (nm :: Name -> t :: Type -> rest :: {Type}
56 => tf1 t -> tf2 t -> xml ctx [] []) 65 -> fn [[nm] ~ rest] =>
57 -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] [] 66 tf1 t -> tf2 t -> xml ctx [] [])
67 -> r :: {Type}
68 -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] []
58 69
59 val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> ctx :: {Unit} 70 val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
60 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest 71 -> ctx :: {Unit}
61 => tf1 t -> tf2 t -> xml ctx [] []) 72 -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)}
62 -> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] [] 73 -> fn [[nm] ~ rest] =>
74 tf1 t -> tf2 t -> xml ctx [] [])
75 -> r :: {(Type * Type)}
76 -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] []
63 77
64 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} 78 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
65 -> sql_query tables exps -> tables ~ exps 79 -> sql_query tables exps
66 => ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables) 80 -> fn [tables ~ exps] =>
67 -> xml ctx [] []) 81 ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] =>
68 -> transaction (xml ctx [] []) 82 [nm = $fields] ++ acc) [] tables)
83 -> xml ctx [] [])
84 -> transaction (xml ctx [] [])
69 85
70 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type} -> sql_query tables exps 86 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
71 -> tables ~ exps 87 -> sql_query tables exps
72 => transaction 88 -> fn [tables ~ exps] =>
73 (option $(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)) 89 transaction
90 (option
91 $(exps
92 ++ fold (fn nm (fields :: {Type}) acc
93 [[nm] ~ acc] =>
94 [nm = $fields] ++ acc)
95 [] tables))