From e44434a592770472b58f4ba052404824442ace23 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 21 Feb 2009 15:33:20 -0500 Subject: "Hello world" compiles, after replacing type-level fold with map --- lib/ur/basis.urs | 31 +++++++------------------------ lib/ur/top.ur | 30 +++++++++--------------------- lib/ur/top.urs | 52 +++++++++++++++++----------------------------------- 3 files changed, 33 insertions(+), 80 deletions(-) (limited to 'lib') diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index b4a40fde..cd2468ba 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -120,31 +120,20 @@ con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type con sql_subset :: {{Type}} -> {{Type}} -> Type val sql_subset : keep_drop :: {({Type} * {Type})} -> sql_subset - (fold (fn nm (fields :: ({Type} * {Type})) - acc [[nm] ~ acc] - [fields.1 ~ fields.2] => - [nm = fields.1 ++ fields.2] - ++ acc) [] keep_drop) - (fold (fn nm (fields :: ({Type} * {Type})) - acc [[nm] ~ acc] => - [nm = fields.1] ++ acc) - [] keep_drop) + (map (fn fields :: ({Type} * {Type}) => fields.1 ++ fields.2) keep_drop) + (map (fn fields :: ({Type} * {Type}) => fields.1) keep_drop) val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables val sql_query1 : tables ::: {{Type}} -> grouped ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type} - -> {From : $(fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = sql_table fields] ++ acc) - [] tables), + -> {From : $(map (fn fields :: {Type} => sql_table fields) tables), Where : sql_exp tables [] [] bool, GroupBy : sql_subset tables grouped, Having : sql_exp grouped tables [] bool, SelectFields : sql_subset grouped selectedFields, - SelectExps : $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => - [nm = sql_exp grouped tables [] t] - ++ acc) [] selectedExps) } + SelectExps : $(map (fn (t :: Type) => sql_exp grouped tables [] t) selectedExps) } -> sql_query1 tables selectedFields selectedExps type sql_relop @@ -291,8 +280,7 @@ val query : tables ::: {{Type}} -> exps ::: {Type} -> fn [tables ~ exps] => state ::: Type -> sql_query tables exps - -> ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = $fields] ++ acc) [] tables) + -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> state -> transaction state) -> state @@ -306,17 +294,12 @@ val dml : dml -> transaction unit val insert : fields ::: {Type} -> sql_table fields - -> $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => - [nm = sql_exp [] [] [] t] ++ acc) - [] fields) + -> $(map (fn t :: Type => sql_exp [] [] [] t) fields) -> dml val update : unchanged ::: {Type} -> changed :: {Type} -> fn [changed ~ unchanged] => - $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => - [nm = sql_exp [T = changed ++ unchanged] [] [] t] - ++ acc) - [] changed) + $(map (fn t :: Type => sql_exp [T = changed ++ unchanged] [] [] t) changed) -> sql_table (changed ++ unchanged) -> sql_exp [T = changed ++ unchanged] [] [] bool -> dml diff --git a/lib/ur/top.ur b/lib/ur/top.ur index 35e8519b..58e99f3c 100644 --- a/lib/ur/top.ur +++ b/lib/ur/top.ur @@ -8,17 +8,7 @@ con fstTTT (t :: (Type * Type * Type)) = t.1 con sndTTT (t :: (Type * Type * Type)) = t.2 con thdTTT (t :: (Type * Type * Type)) = t.3 -con mapTT (f :: Type -> Type) = fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] - -con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] => - [nm = f] ++ acc) [] - -con mapT2T (f :: (Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] - -con mapT3T (f :: (Type * Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] +con mapUT = fn f :: Type => map (fn _ :: Unit => f) con ex = fn tf :: (Type -> Type) => res ::: Type -> (choice :: Type -> tf choice -> res) -> res @@ -69,7 +59,7 @@ fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type) -> fn [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) (i : tr []) = - fold [fn r :: {Type} => $(mapTT tf r) -> tr r] + fold [fn r :: {Type} => $(map tf r) -> tr r] (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest) [[nm] ~ rest] r => f [nm] [t] [rest] r.nm (acc (r -- nm))) @@ -80,7 +70,7 @@ fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type) -> fn [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) (i : tr []) = - fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r] + fold [fn r :: {(Type * Type)} => $(map tf r) -> tr r] (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> tr rest) [[nm] ~ rest] r => f [nm] [t] [rest] r.nm (acc (r -- nm))) @@ -91,7 +81,7 @@ fun foldT3R (tf :: (Type * Type * Type) -> Type) (tr :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) (i : tr []) = - fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf r) -> tr r] + fold [fn r :: {(Type * Type * Type)} => $(map tf r) -> tr r] (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) (acc : _ -> tr rest) [[nm] ~ rest] r => f [nm] [t] [rest] r.nm (acc (r -- nm))) @@ -102,7 +92,7 @@ fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type) -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) (i : tr []) = - fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r] + fold [fn r :: {Type} => $(map tf1 r) -> $(map tf2 r) -> tr r] (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) @@ -114,7 +104,7 @@ fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) (i : tr []) = - fold [fn r :: {(Type * Type)} => $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r] + fold [fn r :: {(Type * Type)} => $(map tf1 r) -> $(map tf2 r) -> tr r] (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) @@ -126,7 +116,7 @@ fun foldT3R2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) (i : tr []) = - fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r] + fold [fn r :: {(Type * Type * Type)} => $(map tf1 r) -> $(map tf2 r) -> tr r] (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) @@ -195,8 +185,7 @@ fun foldT3RX2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) (q : sql_query tables exps) [tables ~ exps] - (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = $fields] ++ acc) [] tables) + (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> xml ctx [] []) = query q (fn fs acc => return {acc}{f fs}) @@ -204,8 +193,7 @@ fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) fun queryX' (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) (q : sql_query tables exps) [tables ~ exps] - (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = $fields] ++ acc) [] tables) + (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (xml ctx [] [])) = query q (fn fs acc => diff --git a/lib/ur/top.urs b/lib/ur/top.urs index d6315b92..49aad50c 100644 --- a/lib/ur/top.urs +++ b/lib/ur/top.urs @@ -8,17 +8,7 @@ con fstTTT = fn t :: (Type * Type * Type) => t.1 con sndTTT = fn t :: (Type * Type * Type) => t.2 con thdTTT = fn t :: (Type * Type * Type) => t.3 -con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] - -con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] => - [nm = f] ++ acc) [] - -con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] - -con mapT3T = fn f :: (Type * Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] => - [nm = f t] ++ acc) [] +con mapUT = fn f :: Type => map (fn _ :: Unit => f) con ex = fn tf :: (Type -> Type) => res ::: Type -> (choice :: Type -> tf choice -> res) -> res @@ -53,19 +43,19 @@ val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type) -> (nm :: Name -> t :: Type -> rest :: {Type} -> fn [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r + -> tr [] -> r :: {Type} -> $(map tf r) -> tr r val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type) -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> fn [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r + -> tr [] -> r :: {(Type * Type)} -> $(map tf r) -> tr r val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type) -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} -> fn [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> tr r + -> tr [] -> r :: {(Type * Type * Type)} -> $(map tf r) -> tr r val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type) @@ -73,7 +63,7 @@ val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) -> tr [] - -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r + -> r :: {Type} -> $(map tf1 r) -> $(map tf2 r) -> tr r val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type) @@ -81,7 +71,7 @@ val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) -> tr [] -> r :: {(Type * Type)} - -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r + -> $(map tf1 r) -> $(map tf2 r) -> tr r val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type) @@ -89,32 +79,32 @@ val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * T -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) -> tr [] -> r :: {(Type * Type * Type)} - -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r + -> $(map tf1 r) -> $(map tf2 r) -> tr r val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit} -> (nm :: Name -> t :: Type -> rest :: {Type} -> fn [[nm] ~ rest] => tf t -> xml ctx [] []) - -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] [] + -> r :: {Type} -> $(map tf r) -> xml ctx [] [] val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit} -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> fn [[nm] ~ rest] => tf t -> xml ctx [] []) - -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] [] + -> r :: {(Type * Type)} -> $(map tf r) -> xml ctx [] [] val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit} -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} -> fn [[nm] ~ rest] => tf t -> xml ctx [] []) - -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> xml ctx [] [] + -> r :: {(Type * Type * Type)} -> $(map tf r) -> xml ctx [] [] val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit} -> (nm :: Name -> t :: Type -> rest :: {Type} -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> xml ctx [] []) -> r :: {Type} - -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] [] + -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> ctx :: {Unit} @@ -122,7 +112,7 @@ val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> xml ctx [] []) -> r :: {(Type * Type)} - -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] [] + -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) @@ -131,21 +121,19 @@ val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> xml ctx [] []) -> r :: {(Type * Type * Type)} - -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> xml ctx [] [] + -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> sql_query tables exps -> fn [tables ~ exps] => - ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = $fields] ++ acc) [] tables) + ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> xml ctx [] []) -> transaction (xml ctx [] []) val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> sql_query tables exps -> fn [tables ~ exps] => - ($(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => - [nm = $fields] ++ acc) [] tables) + ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (xml ctx [] [])) -> transaction (xml ctx [] []) @@ -155,20 +143,14 @@ val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type} transaction (option $(exps - ++ fold (fn nm (fields :: {Type}) acc - [[nm] ~ acc] => - [nm = $fields] ++ acc) - [] tables)) + ++ map (fn fields :: {Type} => $fields) tables)) val oneRow : tables ::: {{Type}} -> exps ::: {Type} -> sql_query tables exps -> fn [tables ~ exps] => transaction $(exps - ++ fold (fn nm (fields :: {Type}) acc - [[nm] ~ acc] => - [nm = $fields] ++ acc) - [] tables) + ++ map (fn fields :: {Type} => $fields) tables) val eqNullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type -> sql_injectable (option t) -- cgit v1.2.3