Zulip Chat Archive

Stream: lean4

Topic: struggling with recursion


Arthur Paulino (Nov 29 2021 at 18:35):

inductive Entry
  | str (s : String)
  | int (n : Int)
  | float (f : Float)
  | null

constant NULL : Entry := Entry.null

instance : Coe Int Entry where
  coe := Entry.int

instance : Coe String Entry where
  coe := Entry.str

instance : Coe Float Entry where
  coe := Entry.float

instance : OfScientific Entry where
  ofScientific m s e := Entry.float (OfScientific.ofScientific m s e)

namespace Entry

private def toString' (e : Entry) : String :=
match e with
  | Entry.str e => s!"'{e}'"
  | Entry.int e => toString e
  | Entry.float e => toString e
  | Entry.null => "NULL"

instance : ToString Entry where
  toString e := e.toString'

end Entry

abbrev Row := List Entry

namespace Row

private def toStrings (r : Row) : List String :=
r.map Entry.toString'

private def build (r : Row) : String :=
s!"({",".intercalate (r.toStrings)})"

end Row

structure Column where
  name : String
  type : String
  deriving Inhabited

namespace Column

private def build (c : Column) : String :=
s!"{c.name} {c.type}"

end Column

abbrev TableScheme := List Column

namespace TableScheme

private def build (ts : TableScheme) : String :=
  s!"({",".intercalate (ts.map λ v => v.build)})"

end TableScheme

abbrev Col := Lean.Name

namespace Col

private def toString (c : Col) := Lean.Name.toString c

end Col

private inductive ColProp
  | EqE (c : Col) (e : Entry)
  | NeqE (c : Col) (e : Entry)
  | LeE (c : Col) (e : Entry)
  | LE (c : Col) (e : Entry)
  | GeE (c : Col) (e : Entry)
  | GE (c : Col) (e : Entry)
  | EqC (c : Col) (c' : Col)
  | NeqC (c : Col) (c' : Col)
  | LeC (c : Col) (c' : Col)
  | LC (c : Col) (c' : Col)
  | GeC (c : Col) (c' : Col)
  | GC (c : Col) (c' : Col)
  | And (cp : ColProp) (cp' : ColProp)
  | Or (cp : ColProp) (cp' : ColProp)

infix:50 " = " => ColProp.EqE
infix:50 " ≠ " => ColProp.NeqE
infix:50 " ≤ " => ColProp.LeE
infix:50 " < " => ColProp.LE
infix:50 " ≥ " => ColProp.GeE
infix:50 " > " => ColProp.GE
infix:50 " = " => ColProp.EqC
infix:50 " ≠ " => ColProp.NeqC
infix:50 " ≤ " => ColProp.LeC
infix:50 " < " => ColProp.LC
infix:50 " ≥ " => ColProp.GeC
infix:50 " > " => ColProp.GC
infix:25 " ∧ " => ColProp.And
infix:25 " ∨ " => ColProp.Or

namespace ColProp

private def toString (cp : ColProp) : String :=
match cp with
| ColProp.EqE c e => s!"{c}={e}"
| ColProp.NeqE c e => s!"{c}≠{e}"
| ColProp.LeE c e => s!"{c}≤{e}"
| ColProp.LE c e => s!"{c}<{e}"
| ColProp.GeE c e => s!"{c}≥{e}"
| ColProp.GE c e => s!"{c}>{e}"
| ColProp.EqC c c' => s!"{c}={c'}"
| ColProp.NeqC c c' => s!"{c}≠{c'}"
| ColProp.LeC c c' => s!"{c}≤{c'}"
| ColProp.LC c c' => s!"{c}<{c'}"
| ColProp.GeC c c' => s!"{c}≥{c'}"
| ColProp.GC c c' => s!"{c}>{c'}"
| ColProp.And cp cp' => s!"({toString cp}) and ({toString cp'})"
| ColProp.Or cp cp' => s!"({toString cp}) or ({toString cp'})"

private instance : ToString ColProp where
  toString cp := cp.toString

end ColProp


mutual
  inductive Query
    | mk (name : String) (steps : List QueryStep)
  private inductive QueryStep
    | select (l : List Col)
    | filter (cp : ColProp)
    | join (q : Query) (on : ColProp) (how : String)
    deriving Inhabited
end

def table (n : String) : Query := n, []⟩

namespace Query

private def name : Query  String
| mk name _ => name

private def steps : Query  List QueryStep
| mk _ steps => steps

end Query

def select (l : List Col) (q : Query) : Query :=
q.name, q.steps.concat (QueryStep.select l)⟩

def filter (cp : ColProp) (q : Query)  : Query :=
q.name, q.steps.concat (QueryStep.filter cp)⟩

def join (q' : Query) (on : ColProp) (how : String) (q : Query) : Query :=
q.name, q.steps.concat (QueryStep.join q' on how)⟩

private def transform (q : Query) (f : Query  Query) : Query := f q

infixl:50 "↠" => transform

private structure SQL where
  Select : List String
  From : String
  Where : String
  As : String

namespace SQL

private def init (t : String) (as : String) : SQL :=
⟨[], t, "true", as

private def toString (b : SQL) : String :=
let select := if b.Select = [] then "*" else ",".intercalate b.Select
if b.As = "" then
  s!"select {select} from {b.From} where {b.Where}"
else
  s!"(select {select} from {b.From} where {b.Where}) as {b.As}"

end SQL

private def applyStep (sql : SQL) (step : QueryStep) : SQL :=
match step with
| QueryStep.select l =>
  let newList := l.map Col.toString
  if sql.Select = [] then
    newList, sql.From, sql.Where, sql.As
  else
    sql.Select.filter (λ s => newList.contains s), sql.From, sql.Where, sql.As
| QueryStep.filter cp => sql.Select, sql.From, s!"{sql.Where} and ({cp})", sql.As
| QueryStep.join q on how =>
  let newSQL : SQL := q.steps.foldl applyStep (SQL.init q.name q.name)
  let newFrom : String := s!"{sql.From} {how} join {newSQL.toString} on {on}"
  sql.Select, newFrom, sql.Where, sql.As
termination_by sorry

Sorry for the long MWE! My difficulty is on the definition of the last function: applyStep. The problem arises when I try to use newFrom in the output of the function. It says:

(kernel) unknown constant '_private.0.applyStep'

Marcus Rossel (Nov 29 2021 at 18:47):

I already get errors on private def toString, because it's noncomputable.

Arthur Paulino (Nov 29 2021 at 18:51):

How come? Here it computes:

#eval SQL.toString ⟨["c1", "c2"], "table1", "c1>1", ""
-- "select c1,c2 from table1 where c1>1"

Marcus Rossel (Nov 29 2021 at 18:52):

Ah sorry, I had some other code in the same file.

Horatiu Cheval (Nov 29 2021 at 18:54):

Note that declaring the function as partial or unsafe removes the error.
You might not like this fix if you intend to also prove things about your functions

Arthur Paulino (Nov 29 2021 at 18:57):

Totally fine at the moment. Thanks!!

Marcus Rossel (Nov 29 2021 at 18:57):

Hmm, so I thought it might be the sorry. But adding axiom hf : False and termination_by False.elim hf has the same issue.

Marcus Rossel (Nov 29 2021 at 18:58):

(deleted)

Mac (Nov 29 2021 at 19:00):

@Arthur Paulino why are so many of the definitions/constants private?

Mac (Nov 29 2021 at 19:01):

A lot of these functions seem like they should not be (for example, the various toString functions).

Arthur Paulino (Nov 29 2021 at 19:01):

Mac said:

Arthur Paulino why are so many of the definitions/constants private?

For constant, I'm just copying what I've seen in other implementations that rely on FFI. I don't understand why just yet. For private, I'm trying to hide implementation details from the API user

Mac (Nov 29 2021 at 19:06):

@Arthur Paulino that is not really what private is for. Lean makes it very hard to interact with things marked private, which, in Lean, you generally want to do (e.g., for proofs). Things should really only be marked private if they are part of an already opaque definition (e.g., a partia or unsafe def) and simply serve as some form of auxiliary utility function.

Mac (Nov 29 2021 at 19:06):

Nothing in your MWE looks like something that should be marked private.

Mac (Nov 29 2021 at 19:07):

also why are toString' functions not named just toString?

Mac (Nov 29 2021 at 19:08):

I am guessing because the toString in the body then clashes with the name, in which case they should be marked protected, not renamed.

Arthur Paulino (Nov 29 2021 at 19:09):

Is there a way to hide things from the API user? Or this is not a thing in Lean?

Marcus Rossel (Nov 29 2021 at 19:11):

Here's a reduced MWE:

mutual

inductive Query
  | mk (steps : List QueryStep)

inductive QueryStep
  | join (q : Query)

end

def Query.steps : Query  List QueryStep
  | mk steps => steps

def applyStep (sql : Unit) : QueryStep  Unit
  | QueryStep.join q => q.steps.foldl applyStep Unit.unit
termination_by sorry

Mac (Nov 29 2021 at 19:16):

Arthur Paulino said:

Is there a way to hide things from the API user? Or this is not a thing in Lean?

In Lean, 99% of the time you don't want to hide things from the API user. Or, more accurately, the APO user doesn't want things hidden from them (as it inhibits their ability to reason about the code).

Mac (Nov 29 2021 at 19:17):

Also note that you are overriding standard syntax with your ColProp operations, which is a very bad idea.

Arthur Paulino (Nov 29 2021 at 19:20):

Mac said:

Also note that you are overriding standard syntax with your ColProp operations, which is a very bad idea.

This was the solution I found to make it easy for the user to type in things like `age > 20

Marcus Rossel (Nov 29 2021 at 19:21):

Arthur Paulino said:

Mac said:

Also note that you are overriding standard syntax with your ColProp operations, which is a very bad idea.

This was the solution I found to make it easy for the user to type in things like `age > 20

I believe you can also do this by conforming to certain instances like LE, LT, etc.
They will then "provide" the notation for you.

Mac (Nov 29 2021 at 19:22):

@Marcus Rossel usually that is true, but in this case that will not work because these functions do not match the type classes types.

Arthur Paulino (Nov 29 2021 at 19:23):

I'm open to ideas. I'm green in Lean and I'm kind of finding my own ways to do things

Marcus Rossel (Nov 29 2021 at 19:23):

Oh, I see. I'm guessing there is no HLE or HLT? :sweat_smile:

Kyle Miller (Nov 29 2021 at 19:24):

@Marcus Rossel The problem is that they're Prop-valued, and Arthur wants an abstract syntax tree basically.

Kyle Miller (Nov 29 2021 at 19:24):

@Mac Would this be a place where Arthur could create a new type of syntax for query expressions? That way > in a query is different from the usual > in an unambiguous way.

Mac (Nov 29 2021 at 19:24):

It would be nice if there were general classes for Eq, Lt, and Le (and I have proposed such things before), but unfortunately they currently don't exist.

Mac (Nov 29 2021 at 19:25):

@Kyle Miller yeah, that would probably be the best way to go about this.

Arthur Paulino (Nov 29 2021 at 19:27):

With the things I've defined it's possible to do

#eval (table "person" 
select [`name, `age] 
filter (`age > 20)).build
-- "select * from (select name,age from person where true and (age>20)) as person"

If it's possible to achieve something like this with better practices, I'm in!

Arthur Paulino (Nov 29 2021 at 19:28):

I'm building a SQL query from those "spark-like" transformations, which I find a lot better to explore data than pure SQL

Arthur Paulino (Nov 29 2021 at 19:37):

Kyle Miller said:

Mac Would this be a place where Arthur could create a new type of syntax for query expressions? That way > in a query is different from the usual > in an unambiguous way.

That's exactly what I intended to do, but I don't know how exactly

Arthur Paulino (Nov 29 2021 at 19:42):

Is there an example of it? I just need to tweak and fix my recursion and then I can come back to this and fix this syntax overriding issue

Mac (Nov 29 2021 at 19:52):

@Arthur Paulino here is a quick example of how such a DSL my look:

open Lean

declare_syntax_cat entry

syntax "#" noWs "{" term "}" : entry

syntax num : entry
syntax "-" noWs num : entry
syntax str : entry
syntax "NULL" : entry

macro "entry% " stx:entry : term =>
  match stx with
  | `(entry| #{$v}) => `(coe $v)
  | `(entry| $v:numLit) => `(Entry.int $v)
  | `(entry| -$v:numLit) => `(Entry.int (-$v))
  | `(entry| $v:strLit) => `(Entry.str $v)
  | `(entry| NULL) => `(Entry.null)
  | _ => Macro.throwErrorAt stx "ill-formed entry"

declare_syntax_cat colProp

syntax:50 ident " = " entry : colProp
syntax:50 ident " ≠ " entry : colProp
syntax:50 ident " ≤ " entry : colProp
syntax:50 ident " < " entry : colProp
syntax:50 ident " ≥ " entry : colProp
syntax:50 ident " > " entry : colProp
syntax:50 ident " = " ident : colProp
syntax:50 ident " ≠ " ident : colProp
syntax:50 ident " ≤ " ident : colProp
syntax:50 ident " < " ident : colProp
syntax:50 ident " ≥ " ident : colProp
syntax:50 ident " > " ident : colProp
syntax:25 colProp:26 " ∧ " colProp:26 : colProp
syntax:25 colProp:26 " ∨ " colProp:26 : colProp
syntax:max "(" colProp ")" : colProp

syntax "colProp% " colProp : term

macro_rules
| `(colProp% $stx) =>
  match stx with
  | `(colProp| $x:ident = $y:entry) => `(ColProp.EqE $(quote x.getId) (entry% $y))
  | `(colProp| $x:ident  $y:entry) => `(ColProp.NeE $(quote x.getId) (entry% $y))
  | `(colProp| $x:ident  $y:entry) => `(ColProp.LeE $(quote x.getId) (entry% $y))
  | `(colProp| $x:ident < $y:entry) => `(ColProp.LE  $(quote x.getId) (entry% $y))
  | `(colProp| $x:ident  $y:entry) => `(ColProp.GeE $(quote x.getId) (entry% $y))
  | `(colProp| $x:ident > $y:entry) => `(ColProp.GE  $(quote x.getId) (entry% $y))
  | `(colProp| $x:ident = $y:ident) => `(ColProp.EqC $(quote x.getId) $(quote y.getId))
  | `(colProp| $x:ident  $y:ident) => `(ColProp.NeC $(quote x.getId) $(quote y.getId))
  | `(colProp| $x:ident  $y:ident) => `(ColProp.LeC $(quote x.getId) $(quote y.getId))
  | `(colProp| $x:ident < $y:ident) => `(ColProp.LC  $(quote x.getId) $(quote y.getId))
  | `(colProp| $x:ident  $y:ident) => `(ColProp.GeC $(quote x.getId) $(quote y.getId))
  | `(colProp| $x:ident > $y:ident) => `(ColProp.GC  $(quote x.getId) $(quote y.getId))
  | `(colProp| $x  $y) => `(ColProp.And (colProp% $x) (colProp% $y))
  | `(colProp| $x  $y) => `(ColProp.Or  (colProp% $x) (colProp% $y))
  | `(colProp| ($x)) => `(colProp% $x)
  | _ => Macro.throwErrorAt stx "ill-formed column proposition"

#check colProp% (a = 2  b = c)  d = #{42 + 21}
/-
ColProp.Or (ColProp.And (ColProp.EqE `a (Entry.int 2)) (ColProp.EqC `b `c))
  (ColProp.EqE `d (Entry.int (42 + 21))) : ColProp
-/

EDIT: Added parenthetical syntax


Last updated: Dec 20 2023 at 11:08 UTC