Mercurial > urweb

annotate lib/ur/top.urs @ 630:6a6eb9882d57

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Top.Fold.mp
author Adam Chlipala <adamc@hcoop.net>
date Tue, 24 Feb 2009 13:50:39 -0500
parents e68de2a5506b
children effa7d43aac3
rev   line source
adamc@623 1 (** Row folding *)
adamc@623 2
adamc@623 3 con folder = K ==> fn r :: {K} =>
adamc@623 4 tf :: ({K} -> Type)
adamc@623 5 -> (nm :: Name -> v :: K -> r :: {K} -> tf r
adamc@629 6 -> [[nm] ~ r] => tf ([nm = v] ++ r))
adamc@623 7 -> tf [] -> tf r
adamc@623 8
adamc@627 9 structure Folder : sig
adamc@627 10 val nil : K --> folder (([]) :: {K})
adamc@627 11 val cons : K --> r ::: {K} -> nm :: Name -> v :: K
adamc@629 12 -> [[nm] ~ r] => folder r -> folder ([nm = v] ++ r)
adamc@628 13 val concat : K --> r1 ::: {K} -> r2 ::: {K}
adamc@629 14 -> [r1 ~ r2] => folder r1 -> folder r2 -> folder (r1 ++ r2)
adamc@630 15 val mp : K1 --> K2 --> f ::: (K1 -> K2) -> r ::: {K1}
adamc@630 16 -> folder r -> folder (map f r)
adamc@627 17 end
adamc@627 18
adamc@623 19
adamc@422 20 val not : bool -> bool
adamc@422 21
adamc@329 22 con idT = fn t :: Type => t
adamc@329 23 con record = fn t :: {Type} => $t
adamc@339 24 con fstTT = fn t :: (Type * Type) => t.1
adamc@339 25 con sndTT = fn t :: (Type * Type) => t.2
adamc@445 26 con fstTTT = fn t :: (Type * Type * Type) => t.1
adamc@445 27 con sndTTT = fn t :: (Type * Type * Type) => t.2
adamc@445 28 con thdTTT = fn t :: (Type * Type * Type) => t.3
adamc@329 29
adamc@621 30 con mapUT = fn f :: Type => map (fn _ :: Unit => f)
adamc@445 31
adamc@339 32 con ex = fn tf :: (Type -> Type) =>
adamc@355 33 res ::: Type -> (choice :: Type -> tf choice -> res) -> res
adamc@339 34
adamc@339 35 val ex : tf :: (Type -> Type) -> choice :: Type -> tf choice -> ex tf
adamc@339 36
adamc@325 37 val compose : t1 ::: Type -> t2 ::: Type -> t3 ::: Type
adamc@355 38 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3)
adamc@325 39
adamc@325 40 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
adamc@355 41 -> xml ctx use []
adamc@329 42
adamc@411 43 val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
adamc@411 44 -> (nm :: Name -> rest :: {Unit}
adamc@629 45 -> [[nm] ~ rest] =>
adamc@411 46 tf -> tr rest -> tr ([nm] ++ rest))
adamc@623 47 -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf r) -> tr r
adamc@411 48
adamc@418 49 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
adamc@418 50 -> (nm :: Name -> rest :: {Unit}
adamc@629 51 -> [[nm] ~ rest] =>
adamc@418 52 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
adamc@623 53 -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
adamc@418 54
adamc@418 55 val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
adamc@418 56 -> (nm :: Name -> rest :: {Unit}
adamc@629 57 -> [[nm] ~ rest] =>
adamc@418 58 tf1 -> tf2 -> xml ctx [] [])
adamc@623 59 -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
adamc@418 60
adamc@623 61 val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type)
adamc@623 62 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@629 63 -> [[nm] ~ rest] =>
adamc@355 64 tf t -> tr rest -> tr ([nm = t] ++ rest))
adamc@623 65 -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r
adamc@336 66
adamc@623 67 val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
adamc@623 68 -> tr :: ({K} -> Type)
adamc@623 69 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@629 70 -> [[nm] ~ rest] =>
adamc@623 71 tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
adamc@623 72 -> tr []
adamc@623 73 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r
adamc@623 74
adamc@623 75 val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit}
adamc@623 76 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@629 77 -> [[nm] ~ rest] =>
adamc@623 78 tf t -> xml ctx [] [])
adamc@623 79 -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] []
adamc@623 80
adamc@623 81 val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit}
adamc@623 82 -> (nm :: Name -> t :: K -> rest :: {K}
adamc@629 83 -> [[nm] ~ rest] =>
adamc@623 84 tf1 t -> tf2 t -> xml ctx [] [])
adamc@623 85 -> r ::: {K} -> folder r
adamc@623 86 -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] []
adamc@445 87
adamc@334 88 val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
adamc@355 89 -> sql_query tables exps
adamc@629 90 -> [tables ~ exps] =>
adamc@621 91 ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@355 92 -> xml ctx [] [])
adamc@355 93 -> transaction (xml ctx [] [])
adamc@341 94
adamc@469 95 val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
adamc@469 96 -> sql_query tables exps
adamc@629 97 -> [tables ~ exps] =>
adamc@621 98 ($(exps ++ map (fn fields :: {Type} => $fields) tables)
adamc@469 99 -> transaction (xml ctx [] []))
adamc@469 100 -> transaction (xml ctx [] [])
adamc@469 101
adamc@355 102 val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 103 -> [tables ~ exps] =>
adamc@629 104 sql_query tables exps
adamc@629 105 -> transaction
adamc@629 106 (option
adamc@629 107 $(exps
adamc@629 108 ++ map (fn fields :: {Type} => $fields) tables))
adamc@440 109
adamc@440 110 val oneRow : tables ::: {{Type}} -> exps ::: {Type}
adamc@629 111 -> [tables ~ exps] =>
adamc@629 112 sql_query tables exps
adamc@629 113 -> transaction
adamc@629 114 $(exps
adamc@629 115 ++ map (fn fields :: {Type} => $fields) tables)
adamc@629 116
adamc@470 117 val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@470 118 -> t ::: Type -> sql_injectable (option t)
adamc@470 119 -> sql_exp tables agg exps (option t)
adamc@470 120 -> sql_exp tables agg exps (option t)
adamc@470 121 -> sql_exp tables agg exps bool
adamc@470 122
adamc@470 123 val eqNullable' : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type}
adamc@470 124 -> t ::: Type -> sql_injectable (option t)
adamc@470 125 -> sql_exp tables agg exps (option t)
adamc@470 126 -> option t
adamc@470 127 -> sql_exp tables agg exps bool