adam@6: fun sqexps [env] [fields] (fl : folder fields) (inj : $(map sql_injectable fields)) (r : $fields) = adam@6: @map2 [sql_injectable] [id] [sql_exp env [] []] adam@6: (fn [t] => @sql_inject) adam@6: fl inj r adam@6: adam@6: fun selector [tn :: Name] [fs] [ofs] [fs ~ ofs] (fl : folder fs) (m : $(map sql_injectable fs)) (r : $fs) = adam@6: @foldR2 [sql_injectable] [id] adam@6: [fn key => rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool] adam@6: (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key] adam@6: (inj : sql_injectable t) (v : t) adam@6: (exp : rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool) adam@6: [rest :: {Type}] [rest ~ [nm = t] ++ key] => adam@6: (WHERE {{tn}}.{nm} = {@sql_inject inj v} AND {exp [[nm = t] ++ rest] !})) adam@6: (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE)) adam@6: fl m r [_] ! adam@13: adam@13: fun joiner [tn1 :: Name] [tn2 :: Name] [fs] [ofs1] [ofs2] [[tn1] ~ [tn2]] [fs ~ ofs1] [fs ~ ofs2] adam@13: (fl : folder fs) = adam@13: @fold adam@13: [fn key => rest1 :: {Type} -> rest2 :: {Type} -> [rest1 ~ key] => [rest2 ~ key] => sql_exp [tn1 = key ++ rest1, tn2 = key ++ rest2] [] [] bool] adam@13: (fn [nm :: Name] [t :: Type] [key :: {Type}] [[nm] ~ key] adam@13: (exp : rest1 :: {Type} -> rest2 :: {Type} -> [rest1 ~ key] => [rest2 ~ key] adam@13: => sql_exp [tn1 = key ++ rest1, tn2 = key ++ rest2] [] [] bool) adam@13: [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ [nm = t] ++ key] [rest2 ~ [nm = t] ++ key] => adam@13: (WHERE {{tn1}}.{nm} = {{tn2}}.{nm} AND {exp [[nm = t] ++ rest1] [[nm = t] ++ rest2] ! !})) adam@13: (fn [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ []] [rest2 ~ []] => (WHERE TRUE)) adam@13: fl [_] [_] ! !