Mercurial > urweb

annotate lib/ur/top.urs @ 623:588b9d16b00a

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