Mercurial > urweb

comparison lib/ur/top.urs @ 629:e68de2a5506b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Top.Fold.concat elaborates
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 13:46:08 -0500
parents 12b73f3c108e
children 6a6eb9882d57
comparison
equal deleted inserted replaced
628:12b73f3c108e 629:e68de2a5506b
1 (** Row folding *) 1 (** Row folding *)
2 2
3 con folder = K ==> fn r :: {K} => 3 con folder = K ==> fn r :: {K} =>
4 tf :: ({K} -> Type) 4 tf :: ({K} -> Type)
5 -> (nm :: Name -> v :: K -> r :: {K} -> tf r 5 -> (nm :: Name -> v :: K -> r :: {K} -> tf r
6 -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) 6 -> [[nm] ~ r] => tf ([nm = v] ++ r))
7 -> tf [] -> tf r 7 -> tf [] -> tf r
8 8
9 structure Folder : sig 9 structure Folder : sig
10 val nil : K --> folder (([]) :: {K}) 10 val nil : K --> folder (([]) :: {K})
11 val cons : K --> r ::: {K} -> nm :: Name -> v :: K 11 val cons : K --> r ::: {K} -> nm :: Name -> v :: K
12 -> fn [[nm] ~ r] => folder r -> folder ([nm = v] ++ r) 12 -> [[nm] ~ r] => folder r -> folder ([nm = v] ++ r)
13 val concat : K --> r1 ::: {K} -> r2 ::: {K} 13 val concat : K --> r1 ::: {K} -> r2 ::: {K}
14 -> fn [r1 ~ r2] => folder r1 -> folder r2 -> folder (r1 ++ r2) 14 -> [r1 ~ r2] => folder r1 -> folder r2 -> folder (r1 ++ r2)
15 end 15 end
16 16
17 17
18 val not : bool -> bool 18 val not : bool -> bool
19 19
38 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t 38 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
39 -> xml ctx use [] 39 -> xml ctx use []
40 40
41 val foldUR : tf :: Type -> tr :: ({Unit} -> Type) 41 val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
42 -> (nm :: Name -> rest :: {Unit} 42 -> (nm :: Name -> rest :: {Unit}
43 -> fn [[nm] ~ rest] => 43 -> [[nm] ~ rest] =>
44 tf -> tr rest -> tr ([nm] ++ rest)) 44 tf -> tr rest -> tr ([nm] ++ rest))
45 -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf r) -> tr r 45 -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf r) -> tr r
46 46
47 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type) 47 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
48 -> (nm :: Name -> rest :: {Unit} 48 -> (nm :: Name -> rest :: {Unit}
49 -> fn [[nm] ~ rest] => 49 -> [[nm] ~ rest] =>
50 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) 50 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
51 -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r 51 -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
52 52
53 val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit} 53 val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
54 -> (nm :: Name -> rest :: {Unit} 54 -> (nm :: Name -> rest :: {Unit}
55 -> fn [[nm] ~ rest] => 55 -> [[nm] ~ rest] =>
56 tf1 -> tf2 -> xml ctx [] []) 56 tf1 -> tf2 -> xml ctx [] [])
57 -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] [] 57 -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
58 58
59 val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type) 59 val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type)
60 -> (nm :: Name -> t :: K -> rest :: {K} 60 -> (nm :: Name -> t :: K -> rest :: {K}
61 -> fn [[nm] ~ rest] => 61 -> [[nm] ~ rest] =>
62 tf t -> tr rest -> tr ([nm = t] ++ rest)) 62 tf t -> tr rest -> tr ([nm = t] ++ rest))
63 -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r 63 -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r
64 64
65 val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) 65 val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
66 -> tr :: ({K} -> Type) 66 -> tr :: ({K} -> Type)
67 -> (nm :: Name -> t :: K -> rest :: {K} 67 -> (nm :: Name -> t :: K -> rest :: {K}
68 -> fn [[nm] ~ rest] => 68 -> [[nm] ~ rest] =>
69 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 69 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
70 -> tr [] 70 -> tr []
71 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r 71 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
72 72
73 val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit} 73 val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit}
74 -> (nm :: Name -> t :: K -> rest :: {K} 74 -> (nm :: Name -> t :: K -> rest :: {K}
75 -> fn [[nm] ~ rest] => 75 -> [[nm] ~ rest] =>
76 tf t -> xml ctx [] []) 76 tf t -> xml ctx [] [])
77 -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] [] 77 -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] []
78 78
79 val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit} 79 val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit}
80 -> (nm :: Name -> t :: K -> rest :: {K} 80 -> (nm :: Name -> t :: K -> rest :: {K}
81 -> fn [[nm] ~ rest] => 81 -> [[nm] ~ rest] =>
82 tf1 t -> tf2 t -> xml ctx [] []) 82 tf1 t -> tf2 t -> xml ctx [] [])
83 -> r ::: {K} -> folder r 83 -> r ::: {K} -> folder r
84 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] 84 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
85 85
86 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} 86 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
87 -> sql_query tables exps 87 -> sql_query tables exps
88 -> fn [tables ~ exps] => 88 -> [tables ~ exps] =>
89 ($(exps ++ map (fn fields :: {Type} => $fields) tables) 89 ($(exps ++ map (fn fields :: {Type} => $fields) tables)
90 -> xml ctx [] []) 90 -> xml ctx [] [])
91 -> transaction (xml ctx [] []) 91 -> transaction (xml ctx [] [])
92 92
93 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} 93 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
94 -> sql_query tables exps 94 -> sql_query tables exps
95 -> fn [tables ~ exps] => 95 -> [tables ~ exps] =>
96 ($(exps ++ map (fn fields :: {Type} => $fields) tables) 96 ($(exps ++ map (fn fields :: {Type} => $fields) tables)
97 -> transaction (xml ctx [] [])) 97 -> transaction (xml ctx [] []))
98 -> transaction (xml ctx [] []) 98 -> transaction (xml ctx [] [])
99 99
100 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type} 100 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
101 -> sql_query tables exps 101 -> [tables ~ exps] =>
102 -> fn [tables ~ exps] => 102 sql_query tables exps
103 transaction 103 -> transaction
104 (option 104 (option
105 $(exps 105 $(exps
106 ++ map (fn fields :: {Type} => $fields) tables)) 106 ++ map (fn fields :: {Type} => $fields) tables))
107 107
108 val oneRow : tables ::: {{Type}} -> exps ::: {Type} 108 val oneRow : tables ::: {{Type}} -> exps ::: {Type}
109 -> sql_query tables exps 109 -> [tables ~ exps] =>
110 -> fn [tables ~ exps] => 110 sql_query tables exps
111 transaction 111 -> transaction
112 $(exps 112 $(exps
113 ++ map (fn fields :: {Type} => $fields) tables) 113 ++ map (fn fields :: {Type} => $fields) tables)
114 114
115 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} 115 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
116 -> t ::: Type -> sql_injectable (option t) 116 -> t ::: Type -> sql_injectable (option t)
117 -> sql_exp tables agg exps (option t) 117 -> sql_exp tables agg exps (option t)
118 -> sql_exp tables agg exps (option t) 118 -> sql_exp tables agg exps (option t)
119 -> sql_exp tables agg exps bool 119 -> sql_exp tables agg exps bool