struggling with recursion

Stream: lean4

[Arthur Paulino]

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]

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

[Arthur Paulino]

How come? Here it computes:

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

[Marcus Rossel]

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

[Horatiu Cheval]

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]

Totally fine at the moment. Thanks!!

[Marcus Rossel]

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]

(deleted)

[Mac]

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

[Mac]

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

[Arthur Paulino]

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]

@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]

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

[Mac]

also why are toString' functions not named just toString?

[Mac]

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]

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

[Marcus Rossel]

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]

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]

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

[Arthur Paulino]

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]

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]

@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]

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

[Marcus Rossel]

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

[Kyle Miller]

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

[Kyle Miller]

@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]

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]

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

[Arthur Paulino]

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]

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]

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]

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]

@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