comparison lib/ur/top.urs @ 910:8e540df3294d

grid1 compiles but gets stuck in JS
author Adam Chlipala <adamc@hcoop.net>
date Tue, 25 Aug 2009 13:57:56 -0400
parents 7a4b026e45dd
children 37dd42935dad
comparison
equal deleted inserted replaced
909:1d3f60e74ec7 910:8e540df3294d
82 -> [[nm] ~ rest] => 82 -> [[nm] ~ rest] =>
83 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 83 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
84 -> tr [] 84 -> tr []
85 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r 85 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
86 86
87 val foldR3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
88 -> tr :: ({K} -> Type)
89 -> (nm :: Name -> t :: K -> rest :: {K}
90 -> [[nm] ~ rest] =>
91 tf1 t -> tf2 t -> tf3 t -> tr rest -> tr ([nm = t] ++ rest))
92 -> tr []
93 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r
94
87 val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit} 95 val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit}
88 -> (nm :: Name -> t :: K -> rest :: {K} 96 -> (nm :: Name -> t :: K -> rest :: {K}
89 -> [[nm] ~ rest] => 97 -> [[nm] ~ rest] =>
90 tf t -> xml ctx [] []) 98 tf t -> xml ctx [] [])
91 -> r :: {K} -> folder r -> $(map tf r) -> xml ctx [] [] 99 -> r :: {K} -> folder r -> $(map tf r) -> xml ctx [] []
94 -> (nm :: Name -> t :: K -> rest :: {K} 102 -> (nm :: Name -> t :: K -> rest :: {K}
95 -> [[nm] ~ rest] => 103 -> [[nm] ~ rest] =>
96 tf1 t -> tf2 t -> xml ctx [] []) 104 tf1 t -> tf2 t -> xml ctx [] [])
97 -> r :: {K} -> folder r 105 -> r :: {K} -> folder r
98 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] 106 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
107
108 val foldRX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> ctx :: {Unit}
109 -> (nm :: Name -> t :: K -> rest :: {K}
110 -> [[nm] ~ rest] =>
111 tf1 t -> tf2 t -> tf3 t -> xml ctx [] [])
112 -> r :: {K} -> folder r
113 -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> xml ctx [] []
99 114
100 val queryI : tables ::: {{Type}} -> exps ::: {Type} 115 val queryI : tables ::: {{Type}} -> exps ::: {Type}
101 -> [tables ~ exps] => 116 -> [tables ~ exps] =>
102 sql_query tables exps 117 sql_query tables exps
103 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) 118 -> ($(exps ++ map (fn fields :: {Type} => $fields) tables)