Mercurial > urweb
comparison lib/ur/top.urs @ 719:5c099b1308ae
hello compiles with CSS
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 12 Apr 2009 11:08:00 -0400 |
parents | 4e260887d8f2 |
children | acb8537f58f0 |
comparison
equal
deleted
inserted
replaced
718:f152f215a02c | 719:5c099b1308ae |
---|---|
37 val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf | 37 val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf |
38 | 38 |
39 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type | 39 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type |
40 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3) | 40 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3) |
41 | 41 |
42 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t | 42 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> css ::: {Unit} -> show t -> t |
43 -> xml ctx use [] | 43 -> xml ctx use [] css |
44 | 44 |
45 val foldUR : tf :: Type -> tr :: ({Unit} -> Type) | 45 val foldUR : tf :: Type -> tr :: ({Unit} -> Type) |
46 -> (nm :: Name -> rest :: {Unit} | 46 -> (nm :: Name -> rest :: {Unit} |
47 -> [[nm] ~ rest] => | 47 -> [[nm] ~ rest] => |
48 tf -> tr rest -> tr ([nm] ++ rest)) | 48 tf -> tr rest -> tr ([nm] ++ rest)) |
52 -> (nm :: Name -> rest :: {Unit} | 52 -> (nm :: Name -> rest :: {Unit} |
53 -> [[nm] ~ rest] => | 53 -> [[nm] ~ rest] => |
54 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) | 54 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) |
55 -> tr [] -> r :: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> tr r | 55 -> tr [] -> r :: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> tr r |
56 | 56 |
57 val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit} | 57 val foldURX2: css ::: {Unit} -> tf1 :: Type -> tf2 :: Type -> ctx :: {Unit} |
58 -> (nm :: Name -> rest :: {Unit} | 58 -> (nm :: Name -> rest :: {Unit} |
59 -> [[nm] ~ rest] => | 59 -> [[nm] ~ rest] => |
60 tf1 -> tf2 -> xml ctx [] []) | 60 tf1 -> tf2 -> xml ctx [] [] css) |
61 -> r :: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> xml ctx [] [] | 61 -> r :: {Unit} -> folder r -> $(mapU tf1 r) -> $(mapU tf2 r) -> xml ctx [] [] css |
62 | 62 |
63 val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type) | 63 val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type) |
64 -> (nm :: Name -> t :: K -> rest :: {K} | 64 -> (nm :: Name -> t :: K -> rest :: {K} |
65 -> [[nm] ~ rest] => | 65 -> [[nm] ~ rest] => |
66 tf t -> tr rest -> tr ([nm = t] ++ rest)) | 66 tf t -> tr rest -> tr ([nm = t] ++ rest)) |
72 -> [[nm] ~ rest] => | 72 -> [[nm] ~ rest] => |
73 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) | 73 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) |
74 -> tr [] | 74 -> tr [] |
75 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r | 75 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r |
76 | 76 |
77 val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit} | 77 val foldRX : K --> css ::: {Unit} -> tf :: (K -> Type) -> ctx :: {Unit} |
78 -> (nm :: Name -> t :: K -> rest :: {K} | 78 -> (nm :: Name -> t :: K -> rest :: {K} |
79 -> [[nm] ~ rest] => | 79 -> [[nm] ~ rest] => |
80 tf t -> xml ctx [] []) | 80 tf t -> xml ctx [] [] css) |
81 -> r :: {K} -> folder r -> $(map tf r) -> xml ctx [] [] | 81 -> r :: {K} -> folder r -> $(map tf r) -> xml ctx [] [] css |
82 | 82 |
83 val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit} | 83 val foldRX2 : K --> css ::: {Unit} -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit} |
84 -> (nm :: Name -> t :: K -> rest :: {K} | 84 -> (nm :: Name -> t :: K -> rest :: {K} |
85 -> [[nm] ~ rest] => | 85 -> [[nm] ~ rest] => |
86 tf1 t -> tf2 t -> xml ctx [] []) | 86 tf1 t -> tf2 t -> xml ctx [] [] css) |
87 -> r :: {K} -> folder r | 87 -> r :: {K} -> folder r |
88 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] | 88 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] css |
89 | 89 |
90 val queryI : tables ::: {{Type}} -> exps ::: {Type} | 90 val queryI : tables ::: {{Type}} -> exps ::: {Type} |
91 -> [tables ~ exps] => | 91 -> [tables ~ exps] => |
92 sql_query tables exps | 92 sql_query tables exps |
93 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) | 93 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) |
94 -> transaction unit) | 94 -> transaction unit) |
95 -> transaction unit | 95 -> transaction unit |
96 | 96 |
97 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} | 97 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> css ::: {Unit} |
98 -> [tables ~ exps] => | 98 -> [tables ~ exps] => |
99 sql_query tables exps | 99 sql_query tables exps |
100 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) | 100 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) |
101 -> xml ctx [] []) | 101 -> xml ctx [] [] css) |
102 -> transaction (xml ctx [] []) | 102 -> transaction (xml ctx [] [] css) |
103 | 103 |
104 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} | 104 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> css ::: {Unit} |
105 -> [tables ~ exps] => | 105 -> [tables ~ exps] => |
106 sql_query tables exps | 106 sql_query tables exps |
107 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) | 107 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) |
108 -> transaction (xml ctx [] [])) | 108 -> transaction (xml ctx [] [] css)) |
109 -> transaction (xml ctx [] []) | 109 -> transaction (xml ctx [] [] css) |
110 | 110 |
111 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type} | 111 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type} |
112 -> [tables ~ exps] => | 112 -> [tables ~ exps] => |
113 sql_query tables exps | 113 sql_query tables exps |
114 -> transaction | 114 -> transaction |