Mercurial > urweb
comparison lib/top.urs @ 355:fa2d25fe75ce
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)) |