***> first define the List data structure, for creating columns
obj LIST[X :: TRIV] is sorts List NeList .
  op nil : -> List .
  subsorts Elt < NeList < List .
  op _,_ : List List -> List [assoc id: nil] .
  op _,_ : NeList List -> NeList .
  op _,_ : NeList NeList -> NeList .
  protecting NAT .
  op |_| : List -> Nat .
  eq | nil | = 0 .
  var E : Elt .   var L : List .
  eq | E,L | = 1 + | L | .
  op tail_ : NeList -> List [prec 120] .
  var E : Elt .   var L : List .
  eq tail E,L = L .
end

***> query conditions in SQL select statement
obj QUERY-COND is
  pr QID .
  pr NAT .
  sort QueryCond String .
  subsort Id < String .
  op _ _ : String String -> String [assoc] .
  op _=_ : Id String -> QueryCond .
  op _=_ : Id Nat -> QueryCond .
  op _>_ : Id Nat -> QueryCond .
  op _ and _ : QueryCond QueryCond -> QueryCond .
  op _ or _ : QueryCond QueryCond -> QueryCond .
end

***> select statement in SQL
obj TABLE-SELECT is
  pr QUERY-COND .
  pr COLUMNS is
      (LIST *(sort List to BColumns, sort NeList to Columns))[QID].
  sorts QueryCond Query .
  op * : -> Columns .
  op SELECT _ FROM _ WHERE _ : Columns Id QueryCond -> Query .
  op contains : Columns Id -> Bool .
  op index : Columns Id -> Nat .
  var Col : Columns .
  vars I J : Id .
  eq contains(nil, I) = false .
  eq contains(I, J) = (I == J).
  eq contains((I, Col) , J) = (I == J) or contains(Col, J).
  eq index(Col, I) = 0 if not contains(Col, I).
  eq index(I, I) = 1 .
  eq index((I, Col), I) = 1 .
  eq index((J, Col), I) = index(Col, I)+1 if (J =/= I) and contains(Col, I).
end

***> database specification
bth DATABASE is
  pr TABLE-SELECT .
  sort Database ResultSet .
  op query : Database Query -> ResultSet .
  op _ U _ : ResultSet ResultSet -> ResultSet .
end

***> integrated database
bth BOOK-DATABASE is
  pr DATABASE .
  ops db db1 db2 : -> Database .
  ops transform1 transform2 : QueryCond -> QueryCond .
  op change : Columns -> Columns .
  op format : ResultSet -> ResultSet .
  ops first last : String -> Id .
  vars C E1 E2 : QueryCond .
  var Q : Query .
  var S : String .
  var N : Nat .
  vars I I1 I2 : Id .
  var Col Col1 Col2 : Columns .
  eq first(I1 I2) = I1 .
  eq last(I1 I2) = I2 .
  eq query(db, SELECT Col FROM 'book WHERE C) =
      format(query(db1, SELECT change(Col) FROM 'book WHERE transform1(C))) U
      format(query(db2, SELECT Col FROM 'book WHERE transform2(C))).

  eq transform1(E1 and E2) = transform1(E1) and transform1(E2).
  eq transform1(E1 or E2) = transform1(E1) or transform1(E2).
  eq transform1('author = S) =
       ('first-name = first(S) and 'last-name = last(S)).
  eq transform1('price > N) = ('price > N).
  eq transform1('title = S) = ('title = S).
  eq change('title) = 'title .
  eq change('title, Col) = 'title, change(Col).
  eq change('price) = 'price .
  eq change('price, Col) = 'price, change(Col).
  eq change('author) = 'first-name, 'last-name .
  eq change('author, Col) = 'first-name, 'last-name, change(Col).
  op concat-two-columns-at-as : ResultSet Nat Nat Id -> ResultSet .
  eq format(query(db1, SELECT Col FROM I WHERE C)) =
	query(db1, SELECT Col FROM I WHERE C)
        if not contains(Col, 'first-name).
  eq format(query(db1, SELECT Col FROM I WHERE C)) =
	concat-two-columns-at-as(query(db1, SELECT Col FROM I WHERE C),
			         index(Col, 'first-name),
                                 index(Col, 'last-name),
                                 'author)
        if contains(Col, 'first-name).

  eq transform2(E1 and E2) = transform2(E1) and transform2(E2).
  eq transform2(E1 or E2) = transform2(E1) or transform2(E2).
  eq transform2('author = S) = ('author = S).
  eq transform2('price > N) = ('price > N * 8).
  eq transform2('title = S) = ('title = S).
  op each-div-by-8-at-column : ResultSet Nat -> ResultSet .
  eq format(query(db2, SELECT Col FROM I WHERE C)) =
	each-div-by-8-at-column(query(db2, SELECT Col  FROM I WHERE C),
                                index(Col, 'price))
        if contains(Col, 'price).
  eq format(query(db2, SELECT Col FROM I WHERE C)) =
	query(db2, SELECT Col FROM I WHERE C) if not contains(Col, 'price).
end

red query(db,
	  SELECT 'title
            FROM 'book
	   WHERE ('author = 'Joe 'Walter)
             and ('price > 33)).

red query(db,
          SELECT 'author , 'price
            FROM 'book
           WHERE ('title = 'Modern 'Operating 'System)).