Mercurial > urweb

annotate lib/ur/top.urs @ 628:12b73f3c108e

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