module EXP-SYNTAX syntax Boolean ::= "TRUE" | "FALSE" syntax Null ::= "NULL" // syntax Val ::= Int | Bool | Float | String | Null | Boolean syntax Vals ::= List{Val, ","} syntax Exp ::= Val | Id syntax KResult ::= #Int | #Bool | Id | #String | #Float | Null syntax Exp ::= "(" Exp ")" [bracket] > "-" Exp [strict] > Exp "*" Exp [strict, left] | Exp "/" Exp [strict, left] | Exp "DIV" Exp [strict, left] | Exp "MOD" Exp [strict, left] | Exp "%" Exp [strict, left] > Exp "+" Exp [strict, left] | Exp "-" Exp [strict, left] syntax Exp ::= "(" Exp ")" [bracket] > "!" Exp [strict] > Exp "=" Exp [strict, non-assoc] | Exp ">=" Exp [strict, non-assoc] | Exp ">" Exp [strict, non-assoc] | Exp "<=" Exp [strict, non-assoc] | Exp "<" Exp [strict, non-assoc] | Exp "!=" Exp [strict, non-assoc] | Exp "<>" Exp [strict, non-assoc] | Exp "IS" "TRUE" [strict] | Exp "IS" "FALSE" [strict] | Exp "IS" "NULL" [strict] | Exp "IS" "UNKNOWN" [strict] | Exp "IS" "NOT" "TRUE" [strict] | Exp "IS" "NOT" "FALSE" [strict] | Exp "IS" "NOT" "NULL" [strict] | Exp "IS" "NOT" "UNKNOWN" [strict] > "NOT" Exp [strict] > Exp "&&" Exp [strict(1), left] | Exp "AND" Exp [strict(1), left] > Exp "||" Exp [strict, left] | Exp "OR" Exp [strict, left] syntax Exp ::= "CONCAT" "(" Vals ")" [strict] | "ELT" "(" Int "," Strings ")" [strict] | "FIELD" "(" String "," Strings ")" [strict] | "INSERT" "(" String "," Int "," Int "," Strings ")" [strict] // INSERT(str,pos,len,newstr) | "INSTR" "(" String "," String ")" [strict] | "LENGTH" "(" String ")" [strict] | "LOCATE" "(" String "," String ")" [strict] | "LOCATE" "(" String "," String "," Int ")" [strict] // LOCATE(S1,S2,StartPosition) | "TRIM" "(" String ")" [strict] | "LTRIM" "(" String ")" [strict] | "RTRIM" "(" String ")" [strict] | "POSITION" "(" String "IN" String ")" [strict] | "REPEAT" "(" String "," Int ")" [strict] | "REPLACE" "(" String "," String "," String ")" [strict] // REPLACE(String,fromString,toString) | "LEFT" "(" String "," Int ")" [strict] | "RIGHT" "(" String "," Int ")" [strict] | "SPACE" "(" Int ")" [strict] | "SUBSTRING" "(" String "," Int ")" [strict] | "SUBSTRING" "(" String "FROM" Int ")" [strict] | "SUBSTRING" "(" String "," Int "," Int ")" [strict] | "SUBSTRING" "(" String "FROM" Int "FOR" Int ")" [strict] syntax Ints ::= List{Int,","} [strict] syntax Strings ::= List{String,","} [strict] syntax Exps ::= List{Exp,","} [strict] syntax Ids ::= List{Id,","} syntax Bool ::= in( String , Strings) syntax Int ::= getOrd(String) [strict] syntax String ::= intToChar(Int) [function] rule intToChar(I:Int) => chrChar(I) syntax Int ::= charToInt(String) [function] rule charToInt(S:String) => ordChar(S) syntax Int ::= strcmp(String,String) [function] syntax Int ::= cmpChar(String,String) [function] syntax Int ::= cmpChar(String,String) [function] syntax Int ::= convertsi(String) [function] syntax Int ::= firstLetterAt(String) [function] endmodule module EXP imports EXP-SYNTAX // rule TRUE:Boolean => 1 [anywhere] rule FALSE:Boolean => 0 [anywhere] rule true:Boolean => 1 rule false:Boolean => 0 rule ! 0 => 1 rule ! I:Int => 0 when I =Int 0 rule ! NULL => NULL rule - I:Int => 0 -Int I rule I1:Int * I2:Int => I1 *Int I2 rule I1:Int / I2:Int => I1 /Int I2 when I2 =/=K 0 rule I1:Int / I2:Int => NULL when I2 ==K 0 rule I1:Int DIV I2:Int => I1 /Int I2 when I2 =/=K 0 rule I1:Int DIV I2:Int => NULL when I2 ==K 0 rule I1:Int MOD I2:Int => I1 %Int I2 when I2 =/=K 0 rule I1:Int MOD I2:Int => NULL when I2 ==K 0 rule I1:Int % I2:Int => I1 %Int I2 when I2 =/=K 0 rule I1:Int % I2:Int => NULL when I2 ==K 0 rule I1:Int + I2:Int => I1 +Int I2 rule I1:Int - I2:Int => I1 -Int I2 rule I1:Int >= I2:Int => 1 when I1 >=Int I2 rule I1:Int >= I2:Int => 0 when I1 I2:Int => 1 when I1 >Int I2 rule I1:Int > I2:Int => 0 when I1 <=Int I2 rule I1:Int <= I2:Int => 1 when I1 <=Int I2 rule I1:Int <= I2:Int => 0 when I1 >Int I2 rule I1:Int < I2:Int => 1 when I1 0 when I1 >=Int I2 rule S:String + I:Int => convertsi(S) + I [anywhere] rule I:Int + S:String => I + convertsi(S) [anywhere] rule S:String + I:Int => convertsi(S) + I [anywhere] rule I:Int + S:String => I + convertsi(S) [anywhere] rule S1:String + S2:String => convertsi(S1) + convertsi(S2) [anywhere] rule S:String - I:Int => convertsi(S) - I [anywhere] rule I:Int - S:String => I - convertsi(S) [anywhere] rule S1:String - S2:String => convertsi(S1) - convertsi(S2) [anywhere] rule S:String * I:Int => convertsi(S) * I [anywhere] rule I:Int * S:String => I * convertsi(S) [anywhere] rule S1:String * S2:String => convertsi(S1) * convertsi(S2) [anywhere] rule S:String / I:Int => convertsi(S) / I [anywhere] rule I:Int / S:String => I / convertsi(S) [anywhere] rule S1:String / S2:String => convertsi(S1) / convertsi(S2) [anywhere] rule S:String DIV I:Int => convertsi(S) DIV I [anywhere] rule I:Int DIV S:String => I DIV convertsi(S) [anywhere] rule S1:String DIV S2:String => convertsi(S1) DIV convertsi(S2) [anywhere] rule S:String % I:Int => convertsi(S) % I [anywhere] rule I:Int % S:String => I % convertsi(S) [anywhere] rule S1:String % S2:String => convertsi(S1) % convertsi(S2) [anywhere] rule F1:Float * F2:Float => F1 *Float F2 rule I1:Int * F2:Float => Int2Float(I1) * F2 rule F1:Float * I2:Int => F1 * Int2Float(I2) rule F1:Float / F2:Float => F1 /Float F2 when F2 =/=K 0 rule F1:Float / F2:Float => NULL when F2 ==K 0 rule F1:Float DIV F2:Float => F1 /Float F2 when F2 =/=K 0 rule F1:Float DIV F2:Float => NULL when F2 ==K 0 rule I1:Int / F2:Float => Int2Float(I1) / F2 rule F1:Float / I2:Int => F1 / Int2Float(I2) rule I1:Int DIV F2:Float => Int2Float(I1) DIV F2 rule F1:Float DIV I2:Int => F1 DIV Int2Float(I2) rule F1:Float MOD F2:Float => F1 %Float F2 when F2 =/=K 0 rule F1:Float MOD F2:Float => NULL when F2 ==K 0 rule F1:Float % F2:Float => F1 %Float F2 when F2 =/=K 0 rule F1:Float % F2:Float => NULL when F2 ==K 0 rule I1:Int MOD F2:Float => Int2Float(I1) MOD F2 rule F1:Float MOD I2:Int => F1 MOD Int2Float(I2) rule I1:Int % F2:Float => Int2Float(I1) % F2 rule F1:Float % I2:Int => F1 % Int2Float(I2) rule F1:Float + F2:Float => F1 +Float F2 rule I1:Int + F2:Float => Int2Float(I1) + F2 rule F1:Float + I2:Int => F1 + Int2Float(I2) rule F1:Float - F2:Float => F1 -Float F2 rule I1:Int - F2:Float => Int2Float(I1) - F2 rule F1:Float - I2:Int => F1 - Int2Float(I2) rule F1:Float >= F2:Float => 1 when F1 >=Float F2 rule F1:Float >= F2:Float => 0 when F1 = F2:Float => Int2Float(I1) >= F2 rule F1:Float >= I2:Int => F1 >= Int2Float(I2) rule F1:Float > F2:Float => 1 when F1 >Float F2 rule F1:Float > F2:Float => 0 when F1 <=Float F2 rule I1:Int > F2:Float => Int2Float(I1) > F2 rule F1:Float > I2:Int => F1 > Int2Float(I2) rule F1:Float <= F2:Float => 1 when F1 <=Float F2 rule F1:Float <= F2:Float => 0 when F1 >Float F2 rule I1:Int <= F2:Float => Int2Float(I1) <= F2 rule F1:Float <= I2:Int => F1 <= Int2Float(I2) rule F1:Float < F2:Float => 1 when F1 0 when F1 >=Float F2 rule I1:Int < F2:Float => Int2Float(I1) < F2 rule F1:Float < I2:Int => F1 < Int2Float(I2) rule S:String = I:Int => convertsi(S) = I [anywhere] rule I:Int = S:String => I = convertsi(S) [anywhere] rule S:String < I:Int => convertsi(S) < I [anywhere] rule I:Int < S:String => I < convertsi(S) [anywhere] rule S:String <= I:Int => convertsi(S) <= I [anywhere] rule I:Int <= S:String => I <= convertsi(S) [anywhere] rule S:String > I:Int => convertsi(S) > I [anywhere] rule I:Int > S:String => I > convertsi(S) [anywhere] rule S:String >= I:Int => convertsi(S) >= I [anywhere] rule I:Int >= S:String => I >= convertsi(S) [anywhere] rule S:String != I:Int => convertsi(S) != I [anywhere] rule I:Int != S:String => I != convertsi(S) [anywhere] rule S:String <> I:Int => convertsi(S) <> I [anywhere] rule I:Int <> S:String => I <> convertsi(S) [anywhere] rule I1:Int = I2:Int => 1 when I1 =Int I2 [anywhere] rule I1:Int = I2:Int => 0 when I1 =/=Int I2 [anywhere] rule I1:Int != I2:Int => 1 when I1 =/=Int I2 [anywhere] rule I1:Int != I2:Int => 0 when I1 =Int I2 [anywhere] rule F1:Float = F2:Float => 1 when F1 ==Float F2 [anywhere] rule F1:Float = F2:Float => 0 when F1 =/=Float F2 [anywhere] rule F1:Float != F2:Float => 1 when F1 =/=Float F2 [anywhere] rule F1:Float != F2:Float => 0 when F1 ==Float F2 [anywhere] rule S1:String >= S2:String => 1 when strcmp(S1,S2) >=Int 0 [anywhere] rule S1:String >= S2:String => 0 when strcmp(S1,S2) =Int -1 [anywhere] rule S1:String > S2:String => 1 when strcmp(S1,S2) =Int 1 [anywhere] rule S1:String > S2:String => 0 when strcmp(S1,S2) <=Int 0 [anywhere] rule S1:String < S2:String => 1 when strcmp(S1,S2) =Int -1 [anywhere] rule S1:String < S2:String => 0 when strcmp(S1,S2) >=Int 0 [anywhere] rule S1:String <= S2:String => 1 when strcmp(S1,S2) <=Int 0 [anywhere] rule S1:String <= S2:String => 0 when strcmp(S1,S2) =Int 1 [anywhere] rule S1:String = S2:String => 1 when strcmp(S1,S2) =Int 0 [anywhere] rule S1:String = S2:String => 0 when strcmp(S1,S2) =/=Int 0 [anywhere] rule S1:String != S2:String => 1 when strcmp(S1,S2) =/=Int 0 [anywhere] rule S1:String != S2:String => 0 when strcmp(S1,S2) =Int 0 [anywhere] rule (N1 <> N2) => N1 != N2 [anywhere] rule NULL + _ => NULL rule _ + NULL => NULL rule NULL - _ => NULL rule _ - NULL => NULL rule NULL * _ => NULL rule _ * NULL => NULL rule NULL / _ => NULL rule _ / NULL => NULL rule NULL DIV _ => NULL rule _ DIV NULL => NULL rule NULL MOD _ => NULL rule _ MOD NULL => NULL rule NULL % _ => NULL rule _ % NULL => NULL rule NULL <= _ => NULL rule _ <= NULL => NULL rule NULL < _ => NULL rule _ < NULL => NULL rule NULL = _ => NULL rule _ = NULL => NULL rule NULL != _ => NULL rule _ != NULL => NULL rule NULL <> _ => NULL rule _ <> NULL => NULL rule NULL >= _ => NULL rule _ >= NULL => NULL rule NULL > _ => NULL rule _ > NULL => NULL rule I:Int IS TRUE => 1 when I =/=K 0 rule 0 IS TRUE => 0 rule NULL IS TRUE => 0 rule A IS TRUE => 0 when A ==Int 0 rule I:Int IS FALSE => 0 when I =/=K 0 rule 0 IS FALSE => 1 rule NULL IS FALSE => 0 rule A IS FALSE => 1 when A ==Int 0 rule I:Int IS UNKNOWN => 0 when I =/=K 0 rule 0 IS UNKNOWN => 0 rule NULL IS UNKNOWN => 1 rule A IS UNKNOWN => 1 when A ==K NULL rule I:Int IS NULL => 0 when I =/=K 0 rule 0 IS NULL => 0 rule NULL IS NULL => 1 rule A IS NULL => 0 when A ==K NULL rule I:Int IS NOT TRUE => 0 when I =/=K 0 rule 0 IS NOT TRUE => 1 rule NULL IS NOT TRUE => 1 rule A IS NOT TRUE => 0 when A ==Int 0 rule I:Int IS NOT FALSE => 1 when I =/=K 0 rule 0 IS NOT FALSE => 0 rule NULL IS NOT FALSE => 1 rule A IS NOT FALSE => 1 when A ==Int 0 rule I:Int IS NOT UNKNOWN => 1 when I =/=K 0 rule 0 IS NOT UNKNOWN => 1 rule NULL IS NOT UNKNOWN => 0 rule A IS NOT UNKNOWN => 0 when A ==K NULL rule I:Int IS NOT NULL => 1 when I =/=K 0 rule 0 IS NOT NULL => 1 rule NULL IS NOT NULL => 0 rule A IS NOT NULL => 0 when A ==K NULL rule 0 && 0 => 0 rule 0 && 1 => 0 rule 0 && NULL => 0 rule I:Int && 0 => 0 when I =/=K 0 rule I:Int && 1 => 1 when I =/=K 0 rule I:Int && NULL => NULL when I =/=K 0 rule NULL && 0 => 0 rule NULL && I:Int => NULL when I =/=K 0 rule NULL && NULL => NULL rule I1:Int && S2:String => I1 && convertsi(S2) rule S1:String && I2:Int => convertsi(S1) && I2 rule S1:String && S2:String => convertsi(S1) && convertsi(S2) rule 0 || 0 => 0 rule 0 || I:Int => 1 when I =/=K 0 rule 0 || NULL => NULL rule I:Int || 0 => 1 when I =/=K 0 rule I:Int || I => 1 when I =/=K 0 rule I:Int || NULL => 1 rule NULL || 0 => NULL rule NULL || I:Int => 1 when I =/=K 0 rule NULL || NULL => NULL rule I1:Int || S2:String => I1 || convertsi(S2) rule S1:String || I2:Int => convertsi(S1) || I2 rule S1:String || S2:String => convertsi(S1) || convertsi(S2) rule I:Int && B => B when I =/=K 0 rule 0 && B => 0 rule I:Int || B => 1 when I =/=K 0 rule 0 || B => B rule I:Int AND B => B when I =/=K 0 rule 0 AND B => 0 rule I:Int OR B => 1 when I =/=K 0 rule 0 OR B => B rule I1 AND I2 => I1 && I2 rule I1 OR I2 => I1 || I2 rule NOT 0 => 1 rule NOT I:Int => 0 when I =/=Int 0 rule NOT NULL => NULL rule B1:Bool && B2:Bool => B1 andBool B2 rule B1:Bool AND B2:Bool => B1 andBool B2 rule B1:Bool || B2:Bool => B1 orBool B2 rule B1:Bool OR B2:Bool => B1 orBool B2 rule CONCAT(.Vals) => "" rule CONCAT(S:String) => S rule CONCAT(S:String, Vs:Vals) => CONCAT(Vs) ~> S +String HOLE rule S2:String ~> S1 +String HOLE => S1 +String S2 [structural] rule NULL ~> S1 +String HOLE => NULL [structural] rule CONCAT(NULL, Vs:Vals) => NULL rule CONCAT(I:Int, Vs:Vals) => CONCAT(Int2String(I),Vs) rule CONCAT(F:Float, Vs:Vals) => CONCAT(Float2String(F),Vs) rule ELT(1, S:String , Ss:Strings) => S rule ELT(N:Int, S:String, Ss:Strings) => ELT(N -Int 1, Ss) rule FIELD(S:String, Ss:Strings) => 0 when notBool in(S,Ss) rule FIELD(S:String, .Strings) => 0 rule FIELD(S:String, S2:String, Ss:Strings) => 1 when S ==String S2 rule FIELD(S:String, S2:String, Ss:Strings) => 1 + FIELD(S,Ss) when notBool (S ==String S2) rule INSERT(S1:String, P:Int, L:Int, S2:String) => (substrString(S1, 0, P -Int 1) +String S2) +String (substrString(S1, (P -Int 1) +Int L, lengthString(S1))) rule INSTR(S1:String, S2:String) => findString(S1,S2,3) +Int 1 rule LENGTH(S:String) => lengthString(S) rule LOCATE(Sub:String, S:String) => findString(S,Sub,0) +Int 1 rule LOCATE(Sub:String, S:String, P:Int) => findString(S,Sub,P) +Int 1 rule POSITION( Sub:String IN S:String) => findString(S,Sub,0) +Int 1 rule TRIM(S:String) => trim(S) rule LTRIM(S:String) => ltrim(S) rule RTRIM(S:String) => rtrim(S) rule REPEAT(S:String,0) => "" rule REPEAT(S:String, N:Int) => REPEAT(S, (N -Int 1)) ~> S +String HOLE rule S2:String ~> S +String HOLE => S +String S2 [structural] rule REPLACE(S:String, FromS:String, ToS:String) => replaceAll(S,FromS,ToS) rule LEFT(S:String, L:Int) => substrString(S,0,L) rule RIGHT(S:String, L:Int) => substrString(S,lengthString(S) -Int L,lengthString(S)) rule SPACE(0) => "" rule SPACE(N:Int) => SPACE(N -Int 1) ~> HOLE +String " " rule S:String ~> HOLE +String S2 => S +String S2 [structural] rule SUBSTRING(S:String, StartP:Int) => substrString(S, StartP -Int 1, lengthString(S)) rule SUBSTRING(S:String FROM StartP:Int) => substrString(S, StartP -Int 1, lengthString(S)) rule SUBSTRING(S:String , StartP:Int , Len:Int) => substrString(S, StartP -Int 1, (StartP -Int 1) +Int Len) rule SUBSTRING(S:String FROM StartP:Int FOR Len:Int) => substrString(S, StartP -Int 1, (StartP -Int 1) +Int Len) rule in(S:String , .Strings ) => false [anywhere] rule in(S:String , S2:String , Ss:Strings) => true when S ==String S2 [anywhere] rule in(S:String , S2:String , Ss:Strings) => in(S, Ss) when S =/=String S2 [anywhere] rule strcmp("","") => 0 rule strcmp("",S:String) => -1 when lengthString(S) >Int 0 rule strcmp(S:String,"") => 1 when lengthString(S) >Int 0 rule strcmp(S1:String,S2:String) => strcmp(substrString(S1,1,lengthString(S1)),substrString(S2,1,lengthString(S2))) when ordChar(substrString(S1,0,1)) ==Int ordChar(substrString(S2,0,1)) rule strcmp(S1:String,S2:String) => cmpChar(substrString(S1,0,1),substrString(S2,0,1)) when ordChar(substrString(S1,0,1)) =/=Int ordChar(substrString(S2,0,1)) rule cmpChar(S1:String,S2:String) => -1 when ordChar(S1) 0 when ordChar(S1) ==Int ordChar(S2) rule cmpChar(S1:String,S2:String) => 1 when ordChar(S1) >Int ordChar(S2) rule convertsi(S:String) => 0 when notBool (#isDigit(substrString(S,0,1)) orBool (substrString(S,0,1) ==String "+" orBool substrString(S,0,1) ==String "-")) rule convertsi(S:String) => 0 when (substrString(S,0,1) ==String "+" orBool substrString(S,0,1) ==String "-") andBool (notBool #isDigit(substrString(S,1,2))) rule convertsi(S:String) => String2Int(substrString(S,1,(1 +Int firstLetterAt(substrString(S,1,lengthString(S)))))) when substrString(S,0,1) ==String "+" andBool #isDigit(substrString(S,1,2)) rule convertsi(S:String) => String2Int(substrString(S,0,(1 +Int firstLetterAt(substrString(S,1,lengthString(S)))))) when substrString(S,0,1) ==String "-" andBool #isDigit(substrString(S,1,2)) rule convertsi(S:String) => String2Int(substrString(S,0,1 +Int firstLetterAt(substrString(S,1,lengthString(S))))) when #isDigit(substrString(S,0,1)) rule firstLetterAt("") => 0 rule firstLetterAt(S:String) => (1 +Int firstLetterAt(substrString(S,1,lengthString(S)))) when #isDigit(substrString(S,0,1)) rule firstLetterAt(S:String) => 0 when notBool #isDigit(substrString(S,0,1)) endmodule module TABLE-SYNTAX imports EXP syntax DataType ::= "INT" | "BOOL" | "TEXT" | "FLOAT" // Representation syntax #TableElement ::= "e(" Vals ")" [strict] syntax TableElement ::= #TableElement syntax TableElements ::= List{TableElement,","} [strict] syntax #Record ::= "r[" TableElements "]" [strict] syntax Record ::= #Record syntax #Field ::= "f(" String "," DataType "," Bool "," Bool ")" syntax Field ::= #Field syntax Fields ::= List{Field,","} [strict] syntax #Schema ::= "s[" Fields "]" [strict] syntax Schema ::= #Schema syntax #Table ::= Id "[" Schema ":" Record "]" [strict] syntax Val ::= FieldRep syntax FieldRep ::= FieldRep1 | FieldRep2 syntax FieldRep1 ::= Id | "`" Id "`" syntax FieldRep1s ::= List{FieldRep1,","} syntax FieldRep2 ::= Id "." Id syntax Collumn ::= FieldRep syntax Collumns ::= List{FieldRep,","} syntax KResult ::= #Record | #Field | #Schema | #Table | #TableElement ////**** Main function ****///// syntax Table ::= #Table | Table "union" Table [strict] | Table "intersect" Table [strict] | Table "difference" Table [strict] | Table "cartesian" Table [strict] | Table "x" Table [strict] syntax Table ::= union(Table,Table) [strict] syntax Table ::= difference(Table,Table) [strict] syntax Table ::= intersect(Table,Table) [strict] syntax Table ::= catesian(Table,Table) [strict] syntax Record ::= union(Record,Record) [strict] syntax Record ::= difference(Record,Record) [strict] syntax Record ::= intersect(Record,Record) [strict] syntax Record ::= catesian(Record,Record) [strict] syntax Table ::= join(Table,Table) [strict] syntax Table ::= join(Table,Table,Exp) [strict(1,2)] syntax Table ::= leftJoin(Table,Table,Exp) [strict(1,2)] syntax Table ::= rightJoin(Table,Table,Exp) [strict(1,2)] syntax Table ::= select(Table,Exp) [strict(1)] syntax Record ::= leftJoin2(Schema,Schema,Record,Record,Exp) syntax Record ::= unionLeftJoin(Schema,Schema,TableElement,Record) syntax Record ::= rightJoin2(Schema,Schema,Record,Record,Exp) syntax Record ::= unionRightJoin(Schema,Schema,TableElement,Record) ////**** Auxiliary function ****///// syntax Id ::= "tmp" syntax Int ::= getIndex(Schema,String) [strict] syntax Exp ::= getValue(TableElement,Exp) [strict] syntax Record ::= filter(Schema,Record,Exp) [strict(1,2)] syntax SelectElement ::= s(Int,TableElement) [strict] syntax KResult ::= SelectElement syntax Exp ::= eval(Schema,TableElement,Exp) [strict(1,2)] syntax Field ::= getFieldFromSchema(Collumn,Schema) [strict] syntax Table ::= project(Table,Schema) [strict] syntax Record ::= project2(Record,Schema,Schema) [strict] syntax TableElement ::= project3(TableElement,Schema,Schema) [strict] syntax Val ::= getValue(Schema,TableElement,String) [strict] syntax Table ::= rename(Table,Id) [strict] syntax Table ::= changeFieldNameCorrespondToTable(Table) [strict] syntax Field ::= rename(Field,String) [strict] syntax Fields ::= concatFieldName(Schema,Id) [strict] syntax String ::= changeFieldRepIntoStringName( FieldRep ) [strict] syntax String ::= changeFieldRepIntoStringName( Id , Id ) [strict] syntax Schema ::= excludeFields(Schema,FieldRep1s) syntax Schema ::= excludeField(Schema,FieldRep1) syntax TableElement ::= addNullElementOnBottom(TableElement,Int) [strict] syntax TableElement ::= addNullElementOnTop(TableElement,Int) [strict] syntax Int ::= numberOfElementInRecord(Record) [strict] syntax TableElement ::= addElementOnBottom(TableElement,Val) [strict] syntax TableElement ::= addElementOnTop(TableElement,Val) [strict] syntax K ::= if(Int,K,K) syntax Schema ::= addElement(Field,Schema) [strict] syntax Schema ::= concat(Schema, Schema) [strict] syntax Record ::= concat(Record, Record) [strict] syntax TableElement ::= append(TableElement,TableElement) [strict] syntax TableElement ::= addTopElement(Val , TableElement) [strict] syntax Record ::= addElement(TableElement,Record) [strict] syntax Record ::= appendElementToRecord(TableElement,Record) [strict] syntax Int ::= numberOfFields(Schema) [strict] syntax Bool ::= checkUnionCompatible( Schema , Schema) [strict] syntax Bool ::= isTableElementEqual( TableElement,TableElement) [strict] syntax Bool ::= consistOf(Record,TableElement) [strict] syntax Bool ::= in( String , Ids) syntax K ::= num(Ids) endmodule module TABLE imports TABLE-SYNTAX ////**** Main function ****///// rule T1:Table cartesian T2:Table => catesian(T1, T2) [anywhere] rule T1:Table union T2:Table => union(T1,T2) [anywhere] rule T1:Table difference T2:Table => difference(T1,T2) [anywhere] rule T1:Table intersect T2:Table => intersect(T1,T2) [anywhere] // Union rule union(Id1:Id[S1:Schema : R1:Record] , Id2:Id[S2:Schema : R2:Record]) => union(R1,R2) ~> tmp[S1 : HOLE] when checkUnionCompatible(S1,S2) [structural] rule union(R,r[.TableElements]) => R [anywhere,structural] rule union(r[.TableElements],R) => R [anywhere,structural] rule union(r[T:TableElement,Ts:TableElements],R) => union(r[Ts],R) when consistOf(R,T) [anywhere] rule union(r[T1:TableElement, Ts1:TableElements],r[T2:TableElement,Ts2:TableElements]) => union(r[Ts1],r[T2,Ts2]) ~> addElement(T1,HOLE) when notBool consistOf(r[T2:TableElement,Ts2:TableElements],T1) [anywhere] // Difference rule difference(Id1:Id[S1:Schema : R1:Record] , Id2:Id[S2:Schema : R2:Record]) => difference(R1,R2) ~> tmp[S1 : HOLE ] when checkUnionCompatible(S1,S2) rule difference(r[.TableElements],R) => r[.TableElements] [structural] rule difference(r[T:TableElement,Ts:TableElements],R) => difference(r[Ts],R) when consistOf(R,T) rule difference(r[T:TableElement,Ts:TableElements],R) => difference(r[Ts],R) ~> addElement(T, HOLE ) when notBool consistOf(R,T) // Intersect rule intersect(Id1:Id[S1:Schema : R1:Record] , Id2:Id[S2:Schema : R2:Record]) => intersect(R1,R2) ~> tmp[S1: HOLE ] when checkUnionCompatible(S1,S2) rule intersect(r[.TableElements],R) => r[.TableElements] [structural] rule intersect(r[T:TableElement,Ts:TableElements],R) => intersect(r[Ts],R) when notBool consistOf(R,T) rule intersect(r[T1:TableElement, Ts1:TableElements],r[T2:TableElement,Ts2:TableElements]) => intersect(r[Ts1],r[Ts2]) ~> addElement(T1, HOLE ) when consistOf(r[T2:TableElement,Ts2:TableElements],T1) // Catesian rule catesian(r[.TableElements],_) => r[.TableElements] [structural] rule catesian(r[E1:TableElement, Es1:TableElements],r[Es2:TableElements]) => concat(appendElementToRecord(E1,r[Es2]),catesian(r[Es1],r[Es2])) rule catesian(T1:Id[S1:Schema : R1:Record],T2:Id[S2:Schema : R2:Record]) => tmp[concat(S1,S2) : catesian(R1,R2)] rule T1:Table cartesian T2:Table => catesian(changeFieldNameCorrespondToTable(T1),changeFieldNameCorrespondToTable(T2)) // Renaming rule rename(T1:Id[S:Schema : R:Record], T2:Id) => T2[S : R] [anywhere] rule rename(f(_,T,B1,B2),S2:String) => f(S2,T,B1,B2) [anywhere] rule concatFieldName(s[.Fields],T:Id) => .Fields [anywhere] rule concatFieldName(s[f(F:String,DT:DataType,B1:Bool,B2:Bool),Fs:Fields],T:Id) => rename(f(F,DT,B1,B2),(#tokenToString(T) +String ".") +String F), concatFieldName(s[Fs],T) [anywhere] // Cross join rule join(T1:Table, T2:Table) => T1 cartesian T2 rule join(T1:Table, T2:Table, E:Exp) => T1 cartesian T2 ~> select( HOLE , E) rule T:#Table ~> select(HOLE , E) => select(T,E) [structural] // left join rule leftJoin(T1:Id[ S1:Schema : R1] , T2:Id[ S2:Schema : R2:Record ], E:Exp) => tmp[ concat(S1,S2) : leftJoin2(S1,S2, R1,R2,E) ] rule leftJoin2(S1:Schema,S2:Schema, r[ .TableElements], R:Record, E:Exp) => r[ .TableElements ] rule leftJoin2(S1:Schema,S2:Schema, r[TE1:TableElement, TEs:TableElements], R:Record, E:Exp) => filter(concat(S1,S2),catesian( r[ TE1 ], R), E) ~> unionLeftJoin(S1,S2,TE1,HOLE) ~> union(HOLE,leftJoin2(S1,S2,r[TEs],R,E)) rule Result:#Record ~> unionLeftJoin(S1:Schema,S2:Schema,T:TableElement,HOLE) => unionLeftJoin(S1,S2,T,Result) [structural] rule Result:#Record ~> union(HOLE,leftJoin2(S1:Schema,S2:Schema,R1:Record,R2:Record,E:Exp)) => union(Result,leftJoin2(S1,S2,R1,R2,E)) [structural] rule unionLeftJoin(S1:Schema,S2:Schema,T:TableElement,Result:Record) => numberOfElementInRecord(Result) = 0 ~> if(HOLE, r[ addNullElementOnBottom(T,numberOfFields(S2)) ], Result) /// rightjoin rule rightJoin(T1:Id[ S1:Schema : R1] , T2:Id[ S2:Schema : R2:Record ], E:Exp) => tmp[ concat(S1,S2) : rightJoin2(S1,S2, R1,R2,E) ] rule rightJoin2(S1:Schema,S2:Schema, R:Record ,r[ .TableElements], E:Exp) => r[ .TableElements ] rule rightJoin2(S1:Schema,S2:Schema, R:Record, r[TE1:TableElement, TEs:TableElements], E:Exp) => filter(concat(S1,S2),catesian( R, r[ TE1 ]), E) ~> unionRightJoin(S1,S2,TE1,HOLE) ~> union(HOLE,rightJoin2(S1,S2,R,r[TEs],E)) rule Result:#Record ~> unionRightJoin(S1:Schema,S2:Schema,T:TableElement,HOLE) => unionRightJoin(S1,S2,T,Result) [structural] rule Result:#Record ~> union(HOLE,rightJoin2(S1:Schema,S2:Schema,R1:Record,R2:Record,E:Exp)) => union(Result,rightJoin2(S1,S2,R1,R2,E)) [structural] rule unionRightJoin(S1:Schema,S2:Schema,T:TableElement,Result:Record) => numberOfElementInRecord(Result) = 0 ~> if(HOLE, r[ addNullElementOnTop(T,numberOfFields(S2)) ], Result) ////**** Auxiliary function ****///// rule getIndex(s[ .Fields ], S2:String) => NULL [anywhere] rule getIndex(s[f(S1:String,_,_,_) , Fs:Fields] , S2:String) => 0 when S1 ==String S2 [anywhere] rule getIndex(s[f(S1:String,_,_,_) , Fs:Fields] , S2:String) => (getIndex(s[Fs],S2) + 1) when notBool S1 ==String S2 [anywhere] syntax Int ::= getIndex2(Schema,String) [strict] rule getIndex2(s[ .Fields ], S2:String) => NULL [anywhere] rule getIndex2(s[f(S1:String,_,_,_) , Fs:Fields] , S2:String) => 0 when substrString(S1,(findChar(S1,".",0) +Int 1),lengthString(S1)) ==String S2 [anywhere] rule getIndex2(s[f(S1:String,_,_,_) , Fs:Fields] , S2:String) => (getIndex2(s[Fs],S2) + 1) when substrString(S1,(findChar(S1,".",0) +Int 1),lengthString(S1)) =/=String S2 [anywhere] rule excludeFields(S:Schema, .FieldRep1s) => S [anywhere] rule excludeFields(S:Schema, F:FieldRep1,Fs:FieldRep1s) => excludeFields(excludeField(S,F),Fs) [anywhere] rule changeFieldRepIntoStringName( I1:Id . I2:Id ) => ((#tokenToString(I1) +String ".") +String #tokenToString(I2)) [anywhere] rule changeFieldRepIntoStringName( T:Id , F:Id ) => ((#tokenToString(T) +String ".") +String #tokenToString(F)) [anywhere] rule excludeField(s[.Fields] , ` I:Id `) => s[ .Fields ] [anywhere] rule excludeField(s[ f(FN:String,D:DataType,B1:Bool,B2:Bool) , Fs:Fields] , ` I:Id `) => excludeField(s[Fs], ` I `) when substrString(FN,(findChar(FN,".",0) +Int 1),lengthString(FN)) ==String #tokenToString(I) [anywhere] rule excludeField(s[ f(FN:String,D:DataType,B1:Bool,B2:Bool) , Fs:Fields] , ` I:Id `) => addElement(f(FN,D,B1,B2),excludeField(s[Fs], ` I `)) when substrString(FN,(findChar(FN,".",0) +Int 1),lengthString(FN)) =/=String #tokenToString(I) [anywhere] rule excludeField(s[.Fields] , I:Id ) => s[ .Fields ] [anywhere] rule excludeField(s[ f(FN:String,D:DataType,B1:Bool,B2:Bool) , Fs:Fields] , I:Id ) => excludeField(s[Fs], ` I `) when substrString(FN,(findChar(FN,".",0) +Int 1),lengthString(FN)) ==String #tokenToString(I) [anywhere] rule excludeField(s[ f(FN:String,D:DataType,B1:Bool,B2:Bool) , Fs:Fields] , I:Id ) => addElement(f(FN,D,B1,B2),excludeField(s[Fs], ` I `)) when substrString(FN,(findChar(FN,".",0) +Int 1),lengthString(FN)) =/=String #tokenToString(I) [anywhere] rule getValue(_, NULL) => NULL rule getValue(e(V:Val, _), 0) => V rule getValue(e(_,Vs:Vals),I:Int) => getValue(e(Vs),I -Int 1) rule getValue(s[.Fields],e(Vs:Vals),S2:String) => NULL [structural] rule getValue(s[f(S1:String,D:DataType,B1,B2),Fs:Fields],e(V:Val,Vs:Vals),S2:String) => V when S1 ==String S2 rule getValue(s[f(S1:String,D:DataType,B1,B2),Fs:Fields],e(V:Val,Vs:Vals),S2:String) => getValue(s[Fs],e(Vs),S2) when S1 =/=String S2 rule select(I:Id[ S:Schema : R:Record ] , E:Exp ) => filter(S,R,E) ~> I[ S : HOLE ] rule R:Record ~> T[ S : HOLE ] => T[ S : R ] [structural] rule r[ Ts:TableElements ] ~> s(0 , T:TableElement) => r[Ts] rule r[ Ts:TableElements ] ~> s(I:Int , T:TableElement) => r[T,Ts] when I =/=Int 0 rule r[ .TableElements ] ~> s(I:Int, T:TableElement) => r[T] when I =/=Int 0 rule r[ .TableElements ] ~> s(0, T:TableElement) => r[ .TableElements ] rule filter( S, r[ .TableElements ] , E ) => r[ .TableElements ] [structural] rule filter( S:Schema, r[ T1:TableElement , Ts:TableElements ], E:Exp ) => eval(S,T1,E) ~> s(HOLE,T1) ~> filter(S,r[Ts],E) rule I:Int ~> s(HOLE,T:TableElement) => s(I,T) rule S:SelectElement ~> R:Record => R ~> S [structural] rule project(T:Id[ S1:Schema : R:Record], S2:Schema) => T[ S2 : project2( R,S1,S2)] rule project2(r[ .TableElements], S1,S2) => r[ .TableElements] rule project2(r[ T:TableElement , Ts:TableElements], S1:Schema , S2:Schema) => addElement(project3(T,S1,S2),project2(r[Ts],S1,S2)) rule project3(T:TableElement,S:Schema,s[ .Fields]) => e(.Vals) rule project3(T:TableElement,S:Schema,s[ f(FN:String,_,_,_), Fs:Fields]) => getValue(T,getIndex(S,FN)) ~> addElementOnTop(project3(T,S,s[Fs]),HOLE) rule NULL ~> addElementOnTop(T,HOLE) => addElementOnTop(T,NULL) rule V:Val ~> addElementOnTop(T,HOLE) => addElementOnTop(T,V) rule eval(_,T,NULL) => NULL rule eval(_,T,B:Bool) => B rule eval(_,T,I:Int) => I rule eval(_,T,S:String) => S rule eval(S:Schema,T:TableElement,I:Id) => getValue(T,getIndex2(S,#tokenToString(I))) ~> eval(S,T,HOLE) rule eval(S:Schema,T:TableElement,` I:Id `) => getValue(T,getIndex2(S,#tokenToString(I))) ~> eval(S,T,HOLE) rule eval(S:Schema,T:TableElement,F:FieldRep) => getValue(T,getIndex(S,changeFieldRepIntoStringName(F))) ~> eval(S,T,HOLE) rule V:Val ~> eval(S,T,HOLE) => eval(S,T,V) [structural] rule eval(S,T, - E:Exp) => - eval(S,T,E) rule eval(S,T, E1:Exp * E2:Exp) => eval(S,T, E1) * eval(S,T,E2) rule eval(S,T, E1:Exp / E2:Exp) => eval(S,T, E1) / eval(S,T,E2) rule eval(S,T, E1:Exp DIV E2:Exp) => eval(S,T, E1) DIV eval(S,T,E2) rule eval(S,T, E1:Exp MOD E2:Exp) => eval(S,T, E1) MOD eval(S,T,E2) rule eval(S,T, E1:Exp % E2:Exp) => eval(S,T, E1) % eval(S,T,E2) rule eval(S,T, E1:Exp + E2:Exp) => eval(S,T, E1) + eval(S,T,E2) rule eval(S,T, E1:Exp - E2:Exp) => eval(S,T, E1) - eval(S,T,E2) rule eval(S,T, ! E:Exp) => ! eval(S,T,E) rule eval(S,T, E1:Exp = E2:Exp) => eval(S,T, E1) = eval(S,T,E2) rule eval(S,T, E1:Exp >= E2:Exp) => eval(S,T, E1) >= eval(S,T,E2) rule eval(S,T, E1:Exp > E2:Exp) => eval(S,T, E1) > eval(S,T,E2) rule eval(S,T, E1:Exp <= E2:Exp) => eval(S,T, E1) < eval(S,T,E2) rule eval(S,T, E1:Exp < E2:Exp) => eval(S,T, E1) < eval(S,T,E2) rule eval(S,T, E1:Exp != E2:Exp) => eval(S,T, E1) != eval(S,T,E2) rule eval(S,T, E1:Exp <> E2:Exp) => eval(S,T, E1) <> eval(S,T,E2) rule eval(S,T, E:Exp IS TRUE) => eval(S,T, E) IS TRUE rule eval(S,T, E:Exp IS FALSE) => eval(S,T, E) IS FALSE rule eval(S,T, E:Exp IS NULL) => eval(S,T, E) IS NULL rule eval(S,T, E:Exp IS UNKNOWN) => eval(S,T, E) IS UNKNOWN rule eval(S,T, E:Exp IS NOT TRUE) => eval(S,T, E) IS NOT TRUE rule eval(S,T, E:Exp IS NOT FALSE) => eval(S,T, E) IS NOT FALSE rule eval(S,T, E:Exp IS NOT NULL) => eval(S,T, E) IS NOT NULL rule eval(S,T, E:Exp IS NOT UNKNOWN) => eval(S,T, E) IS NOT UNKNOWN rule eval(S,T, NOT E:Exp ) => NOT eval(S,T, E) rule eval(S,T, E1:Exp && E2:Exp) => eval(S,T, E1) && eval(S,T,E2) rule eval(S,T, E1:Exp AND E2:Exp) => eval(S,T, E1) AND eval(S,T,E2) rule eval(S,T, E1:Exp || E2:Exp) => eval(S,T, E1) || eval(S,T,E2) rule eval(S,T, E1:Exp OR E2:Exp) => eval(S,T, E1) OR eval(S,T,E2) rule eval(S,T, CONCAT(Vs:Vals)) => CONCAT(Vs) rule eval(S,T, ELT(I:Int,Ss:Strings)) => ELT(I,Ss) rule eval(S,T, FIELD(S1:String,Ss:Strings)) => FIELD(S1,Ss) rule eval(S,T, INSERT(S1:String,I1:Int,I2:Int,Ss:Strings)) => INSERT(S1,I1,I2,Ss) rule eval(S,T, INSTR(S1:String,S2:String)) => INSTR(S1,S2) rule eval(S,T, LENGTH(S1:String)) => LENGTH(S1) rule eval(S,T, LOCATE(S1:String,S2:String)) => LOCATE(S1,S2) rule eval(S,T, LOCATE(S1:String,S2:String,I:Int)) => LOCATE(S1,S2,I) rule eval(S,T, TRIM(S1:String)) => TRIM(S1) rule eval(S,T, LTRIM(S1:String)) => LTRIM(S1) rule eval(S,T, RTRIM(S1:String)) => RTRIM(S1) rule eval(S,T, POSITION(S1:String IN S2:String)) => POSITION(S1 IN S2) rule eval(S,T, REPEAT(S1:String, I:Int)) => REPEAT(S1,I) rule eval(S,T, LEFT(S1:String, I:Int)) => LEFT(S1,I) rule eval(S,T, RIGHT(S1:String, I:Int)) => RIGHT(S1,I) rule eval(S,T, SPACE(I:Int)) => SPACE(I) rule eval(S,T, SUBSTRING(S1:String,I:Int)) => SUBSTRING(S1,I) rule eval(S,T, SUBSTRING(S1:String FROM I:Int)) => SUBSTRING(S1 FROM I) rule eval(S,T, SUBSTRING(S1:String, I1:Int, I2:Int)) => SUBSTRING(S1,I1,I2) rule eval(S,T, SUBSTRING(S1:String FROM I1:Int FOR I2:Int)) => SUBSTRING(S1 FROM I1 FOR I2) //rule getFieldFromSchema(FN:String,s[ .Fields ]) => f(FN,NULL,false,false) //rule getFieldFromSchema(FN:String,s[ f(FN2,T:DataType,B1:Bool,B2:Bool), Fs:Fields]) => f(FN2,T:DataType,B1:Bool,B2:Bool) when FN ==String FN2 rule getFieldFromSchema(I:Id,s[ f(FN2,T:DataType,B1:Bool,B2:Bool), Fs:Fields]) => f(FN2,T:DataType,B1:Bool,B2:Bool) when #tokenToString(I) ==String substrString(FN2,(findChar(FN2,".",0) +Int 1),lengthString(FN2)) [anywhere] rule getFieldFromSchema(` I:Id `,s[ f(FN2,T:DataType,B1:Bool,B2:Bool), Fs:Fields]) => f(FN2,T:DataType,B1:Bool,B2:Bool) when #tokenToString(I) ==String substrString(FN2,(findChar(FN2,".",0) +Int 1),lengthString(FN2)) [anywhere] rule getFieldFromSchema(F:FieldRep1,s[ f(FN2,T:DataType,B1:Bool,B2:Bool), Fs:Fields]) => f(FN2,T:DataType,B1:Bool,B2:Bool) when changeFieldRepIntoStringName(F) ==String FN2 [anywhere] //rule getFieldFromSchema(F:FieldRep2,s[ f(FN2,T:DataType,B1:Bool,B2:Bool), Fs:Fields]) => f(FN2,T:DataType,B1:Bool,B2:Bool) when changeFieldRepIntoStringName(F) ==String FN2 [anywhere] rule getFieldFromSchema(C:Collumn,s[ f(FN2,T:DataType,B1:Bool,B2:Bool), Fs:Fields]) => getFieldFromSchema(C,s[Fs]) [anywhere] rule changeFieldNameCorrespondToTable(T:Id[S:Schema : R:Record]) => T:Id[s[concatFieldName(S,T)] : R] when T =/=K tmp [anywhere] rule changeFieldNameCorrespondToTable(T:Id[S:Schema : R:Record]) => T:Id[S : R] when T ==K tmp [anywhere] rule addNullElementOnBottom(T:TableElement,0) => T [anywhere] rule addNullElementOnBottom(T:TableElement,I:Int) => addNullElementOnBottom(append(T,e(NULL)), I -Int 1) [anywhere] rule addNullElementOnTop(T:TableElement,0) => T [anywhere] rule addNullElementOnTop(T:TableElement,I:Int) => addNullElementOnTop(addTopElement(NULL,T), I -Int 1) [anywhere] rule numberOfElementInRecord(r[ .TableElements ]) => 0 [anywhere] rule numberOfElementInRecord(r[ T:TableElement, Ts:TableElements]) => 1 + numberOfElementInRecord(r[Ts]) [anywhere] rule addElementOnBottom(T:TableElement,V:Val) => append(T,e(V)) [anywhere] rule addElementOnTop(e( Vs:Vals ),V:Val) => e(V,Vs) [anywhere] rule if(I:Int,K1,K2) => K1 when I =/=Int 0 [anywhere] rule if(0,K1,K2) => K2 [anywhere] rule I:#Int ~> if(HOLE,K1:K,K2:K) => if(I,K1,K2) [anywhere] rule addElement(T:TableElement,r[Ts:TableElements]) => r[T,Ts] [anywhere] rule addElement(F:Field,s[Fs:Fields]) => s[F,Fs] [anywhere] rule concat(s[.Fields], S:Schema) => S [anywhere] rule concat(s[F1:Field,Fs1:Fields],s[Fs2:Fields]) => concat(s[Fs1],s[Fs2]) ~> addElement(F1, HOLE ) [anywhere] rule concat(r[.TableElements], R:Record) => R [anywhere] rule concat(r[T1:TableElement,Tb1:TableElements],r[Tb2:TableElements]) => concat(r[Tb1],r[Tb2]) ~> addElement(T1, HOLE ) [structural] [anywhere] rule S:#Schema ~> addElement(F:Field , HOLE ) => addElement( F, S) [anywhere,structural] rule R:#Record ~> tmp [S : HOLE ] => tmp [S : R] [anywhere,structural] rule R:#Record ~> addElement( T1:TableElement, HOLE ) => addElement(T1,R) [anywhere,structural] rule append(e(.Vals),e(Vs:Vals)) => e(Vs) [anywhere] rule append(e(V:Val, Vs1:Vals) ,e(Vs2:Vals)) => append(e(Vs1),e(Vs2)) ~> addTopElement(V , HOLE ) [anywhere] rule addTopElement(V:Val,e(.Vals)) => e(V) [anywhere] rule addTopElement(V:Val,e(Vs:Vals)) => e(V,Vs) [anywhere] rule T:#TableElement ~> addTopElement(V:Val , HOLE) => addTopElement( V , T) [structural] rule addElement(E:TableElement,r[Es:TableElements]) => r[E,Es] rule appendElementToRecord(E1,r[.TableElements]) => r[.TableElements] [structural] rule appendElementToRecord(E1:TableElement,r[E2:TableElement,Es:TableElements]) => addElement(append(E1,E2),appendElementToRecord(E1,r[Es])) rule numberOfFields(s[.Fields]) => 0 [anywhere,structural] rule numberOfFields(s[_, Fs:Fields]) => 1 +Int numberOfFields(s[Fs]) [anywhere] rule checkUnionCompatible(s[.Fields] , s[.Fields]) => true [anywhere,structural] rule checkUnionCompatible(s[.Fields] , s[_]) => false [anywhere,structural] rule checkUnionCompatible(s[_] , s[.Fields]) => false [anywhere,structural] rule checkUnionCompatible(s[f(S1:String,T1:DataType,_,_), Fs1:Fields],s[f(S2:String,T2:DataType,_,_), Fs2:Fields]) => checkUnionCompatible(s[Fs1],s[Fs2]) when S1 ==K S2 andBool T1 ==K T2 [anywhere] rule checkUnionCompatible(s[f(S1:String,T1:DataType,_,_), _],s[f(S2:String,T2:DataType,_,_), _]) => false when S1 =/=K S2 orBool T1 =/=K T2 [anywhere] rule isTableElementEqual(e(.Vals),e(.Vals)) => true [anywhere,structural] rule isTableElementEqual(e(V1:Val,Vs1:Vals),e(V2:Val,Vs2:Vals)) => false when V1 =/=K V2 [anywhere] rule isTableElementEqual(e(V1:Val,Vs1:Vals),e(V2:Val,Vs2:Vals)) => isTableElementEqual(e(Vs1),e(Vs2)) when V1 ==K V2 [anywhere] rule consistOf(r[.TableElements] , E2) => false [anywhere,structural] rule consistOf(r[E1:TableElement ,Ts:TableElements] , E2) => true when isTableElementEqual(E1,E2) [anywhere] rule consistOf(r[E1:TableElement ,Ts:TableElements] , E2) => consistOf(r[Ts:TableElements] , E2) when notBool isTableElementEqual(E1,E2) [anywhere] rule in( S:String , .Ids ) => false [anywhere] rule in(S:String , I1:Id , Is:Ids) => true when S ==String #tokenToString(I1) [anywhere] rule in(S:String , I1:Id , Is:Ids) => in(S, Is) when S =/=String #tokenToString(I1) [anywhere] rule num(.Ids) => 0 rule num(_, Xs:Ids) => num(Xs) +Int 1 endmodule module SQL-SYNTAX imports TABLE syntax Table ::= Stm syntax Stm ::= CreateStm | InsertStm | SelectStm | UpdateStm | DeleteStm | DropStm syntax Stms ::= Stm | Stms Stms [left,structural] syntax Table ::= doGetTableExp(TableExp) [strict] syntax Table ::= doConditionExp(Table,ConditionExp) [strict] syntax Table ::= doProjectionExp(Table,ProjectionExp) [strict] // Store syntax K ::= "store" Table // Create syntax CreateStm ::= "CREATE" "TABLE" Id "(" FieldDcls ")" ";" | "CREATE" "TABLE" Id "(" FieldDcls "," CreateOptionList ")" ";" syntax ProjectionExp ::= "*" | AsClauseOrCollumns syntax AsClauseOrCollumn ::= Collumn | AsClause syntax AsClauseOrCollumns ::= List{AsClauseOrCollumn,","} syntax AsClause ::= Collumn "AS" Collumn syntax ConditionExp ::= "WHERE" Exp syntax FieldDcl ::= Id DataType syntax FieldDcls ::= List{FieldDcl,","} syntax CreateOption ::= "PRIMARY" "KEY" "(" Ids ")" syntax CreateOptionList ::= List{CreateOption,","} syntax K ::= doCreateOption( CreateOptionList , Table) syntax Schema ::= createSchemaFromCollumns(AsClauseOrCollumns,Schema) [strict] syntax Fields ::= makeField( FieldDcls ) [strict] syntax Table ::= setPrimaryKey( Ids, Table ) [strict] syntax Schema ::= setPrimaryKey( Ids , Schema ) [strict] // Select syntax SelectStm ::= "SELECT" Exp ";" | "SELECT" ProjectionExp TableExp ";" | "SELECT" ProjectionExp TableExp ConditionExp ";" // Insert syntax InsertStm ::= "INSERT" "INTO" Id "(" Ids ")" "VALUES" "(" Vals ")" ";" // Delete syntax DeleteStm ::= "DELETE" TableExp ConditionExp ";" syntax Table ::= doDeleteRecords(Table,Exp) [strict(1)] syntax Record ::= deleteAllWhere(Schema,Record,Exp) [strict(1,2)] syntax Record ::= delete(TableElement,Record) [strict] // Drop syntax DropStm ::= "DROP" "TABLE" Ids ";" syntax K ::= dropTable(Ids) [strict] // Join syntax Table ::= getTableFromId(Id) syntax Table ::= getTableFromIds(Ids) syntax TableExp ::= "FROM" Ids [strict] | "FROM" JoinExp [strict] syntax JoinExp ::= Ids "JOIN" Ids [strict(1,2)] | Ids "JOIN" Ids JoinCondition [strict(1,2)] | Ids "INNER" "JOIN" Ids [strict(1,2)] | Ids "INNER" "JOIN" Ids JoinCondition [strict(1,2)] | Ids "CROSS" "JOIN" Ids [strict] | Ids "CROSS" "JOIN" Ids JoinCondition [strict] | Ids "LEFT" "JOIN" Ids JoinCondition [strict(1,2)] | Ids "LEFT" "OUTER" "JOIN" Ids JoinCondition [strict(1,2)] | Ids "RIGHT" "JOIN" Ids JoinCondition [strict(1,2)] | Ids "RIGHT" "OUTER" "JOIN" Ids JoinCondition [strict(1,2)] | Ids "NATURAL" "JOIN" Ids [strict(1,2)] | Ids "NATURAL" "LEFT" "JOIN" Ids [strict(1,2)] | Ids "NATURAL" "LEFT" "OUTER" "JOIN" Ids [strict(1,2)] | Ids "NATURAL" "RIGHT" "JOIN" Ids [strict(1,2)] | Ids "NATURAL" "RIGHT" "OUTER" "JOIN" Ids [strict(1,2)] syntax Table ::= joinUsing(Table,Table,Exp,FieldRep1s) [strict(1,2,4)] syntax Table ::= leftJoinUsing(Table,Table,Exp,FieldRep1s) [strict(1,2,4)] syntax Table ::= rightJoinUsing(Table,Table,Exp,FieldRep1s) [strict(1,2,4)] syntax Table ::= naturalJoin(Table,Table) [strict] syntax Table ::= naturalLeftJoin(Table,Table) [strict] syntax JoinCondition ::= OnClause | UsingClause syntax Table ::= naturalLeftJoin(Table,Table) [strict] syntax Table ::= naturalRightJoin(Table,Table) [strict] syntax OnClause ::= "ON" Exp syntax UsingClause ::= "USING" "(" Collumns ")" syntax Exp ::= changeCommonCollumnToEqualExp(Id, Id, FieldRep1s) syntax KResult ::= FieldRep | FieldEquality syntax FieldEquality ::= FieldRep "=" FieldRep syntax Ids ::= commonField(Schema,Schema) [strict] syntax Bool ::= hasCommonField(Schema,Field) [strict] // Update syntax UpdateStm ::= "UPDATE" Id "SET" AssignValues "WHERE" Exp ";" [strict(1,2)] syntax #AssignValue ::= Id "=" Val | String "=" Val syntax AssignValue ::= #AssignValue | Id "=" Exp [strict] | String "=" Exp [strict] syntax KResult ::= #AssignValue | AsClause syntax AssignValues ::= List{AssignValue,","} syntax Table ::= doUpdateValues(Table,Exp,AssignValues) [strict(1,3)] syntax Record ::= updateAllWhere(Schema, Record, Exp, AssignValues) [strict(1,2,4)] syntax TableElement ::= update(Schema, TableElement, AssignValues ) [strict] syntax TableElement ::= update2(Schema, TableElement, AssignValue ) [strict] syntax Field ::= changeFieldNameTo(Field,String) [strict] endmodule module SQL imports SQL-SYNTAX configuration $PGM:K .Map .Map .Map 0 ////**** Main function ****//// // Delete rule DELETE FROM I:Id WHERE E:Exp ; => getTableFromId(I) ~> doDeleteRecords(HOLE,E) ~> store HOLE rule T:#Table ~> doDeleteRecords(HOLE,E) => doDeleteRecords(T,E) rule doDeleteRecords(I:Id[ S:Schema : R:Record ], E:Exp) => I[ S : deleteAllWhere(S,R,E)] rule deleteAllWhere(S,r[ .TableElements ], E) => r[ .TableElements ] [structural] rule deleteAllWhere(S,r[ T:TableElement, Ts:TableElements ], E:Exp) => eval(S,T,E) ~> delete(T,deleteAllWhere(S,r[ Ts ], E)) rule true ~> delete(T,D) => D rule false ~> delete(T,D) => addElement(T,D) // Update rule UPDATE I:Id SET A:AssignValue WHERE E:Exp ; => getTableFromId(I) ~> doUpdateValues(HOLE, E, A) ~> store HOLE rule T:#Table ~> doUpdateValues(HOLE,E,A) => doUpdateValues(T,E,A) rule doUpdateValues(I:Id[ S:Schema : R:Record ],E:Exp,As:AssignValues) => I[ S : updateAllWhere(S,R,E,As)] rule updateAllWhere(S,r[ .TableElements ],E,As:AssignValues) => r[ .TableElements ] [structural] rule updateAllWhere(S,r[ T:TableElement, Ts:TableElements],E:Exp,As:AssignValues) => eval(S,T,E) ~> update(S,T,As) ~> addElement(HOLE, updateAllWhere(S,r[Ts],E,As)) [structural] rule true ~> update(S,T,As) ~> addElement(HOLE, U ) => addElement(update(S,T,As),U) [structural] rule false ~> update(S,T,As) ~> addElement(HOLE, U ) => addElement(T,U) [structural] rule update(S:Schema, T:TableElement, .AssignValues) => T rule update(S:Schema, T:TableElement, A:AssignValue , As:AssignValues) => update(S,update2(S,T,A),As) rule update2( _, e(.Vals), A ) => e(.Vals) [structural] rule update2(s[ f(FName:String,_,_,_), Fs:Fields], e(V:Val , Vs:Vals), F2Name:Id = VNew:Val) => e(VNew,Vs) when FName ==String #tokenToString(F2Name) rule update2(s[ f(FName:String,_,_,_), Fs:Fields], e(V:Val , Vs:Vals), F2Name:Id = VNew:Val) => addTopElement(V,update2(s[Fs], e(Vs), F2Name = VNew)) when FName =/=String #tokenToString(F2Name) // Drop rule DROP TABLE Ts:Ids ; => dropTable(Ts) rule dropTable( .Ids ) => . rule dropTable(I1:Id, Ids) => dropTable(Ids) ... ((I1 => NULL) |-> L:Int) ... ... (L |-> (S => NULL)) ... ... (L |-> (R => NULL)) ... // Get Table rule getTableFromId(I:Id) => I[ S : R] ... ... (I |-> L:Int) ... ... (L |-> S) ... ... (L |-> R) ... rule getTableFromIds( I:Id ) => getTableFromId(I) [structural,anywhere] rule getTableFromIds(I1:Id, Is:Ids) => join(getTableFromId(I1),getTableFromIds(Is)) [anywhere] // Store rule I:Id[ S:#Schema : R:#Record] ~> store HOLE => . ... ... I |-> L ... ... L |-> (_ => S) ... ... L |-> (_ => R) ... rule I:Id[ S:#Schema : R:#Record] ~> store HOLE => . ... ... . => I |-> L ... . => L |-> S ... . => L |-> R L:Int => L +Int 1 rule store T:Table => T ~> store HOLE [structural] // Create rule S1:Stms S2:Stms => S1 ~> S2 [structural] rule CREATE TABLE TNAME:Id ( FDcls:FieldDcls ) ; => changeFieldNameCorrespondToTable(TNAME[s[ makeField( FDcls )] : r[ .TableElements ] ]) ~> store HOLE rule CREATE TABLE Id ( FDcls:FieldDcls , Opt:CreateOptionList ) ; => changeFieldNameCorrespondToTable(doCreateOption(Opt,Id[s[ makeField( FDcls )] : r[.TableElements ]])) ~> store HOLE rule makeField(.FieldDcls) => .Fields [structural,anywhere] rule makeField(I:Id T:DataType, Dcls:FieldDcls) => f(#tokenToString(I) , T ,false,false) , makeField(Dcls) [anywhere] rule doCreateOption( .CreateOptionList , T) => T rule doCreateOption(PRIMARY KEY (KIds:Ids), Opt:CreateOptionList , T:Table) => doCreateOption(Opt, setPrimaryKey(KIds,T)) // Insert rule (INSERT INTO I:Id(Fs:Ids) VALUES (Vs:Vals) ; => .) ... ... I |-> L ... ... L |-> S ... ... (L |-> (r[ Es ] => concat(r[Es],r[e(Vs)]))) ... // Select rule SELECT E:Exp ; => E rule SELECT P:ProjectionExp T:TableExp ; => doGetTableExp(T) ~> doProjectionExp( HOLE , P ) ... rule SELECT P:ProjectionExp T:TableExp C:ConditionExp ; => doGetTableExp(T) ~> doConditionExp( HOLE , C ) ~> doProjectionExp( HOLE , P ) ... rule T:#Table ~> doConditionExp(HOLE,C) => doConditionExp( T , C) [structural] rule T:#Table ~> doProjectionExp( HOLE , P) => doProjectionExp(T,P) [structural] rule doConditionExp(T:Table , WHERE E:Exp ) => select(T,E) [anywhere] rule doProjectionExp(T:Table, * ) => T [anywhere] rule doProjectionExp(T:Id[ S:Schema : R:Record], As:AsClauseOrCollumns) => project((T[ S : R ]),createSchemaFromCollumns( As,S )) [anywhere] ////**** Auxiliary function ****//// rule changeFieldNameTo(f(FN1,D:DataType,B1:Bool,B2:Bool),FN2:String) => f(substrString(FN1,0,(findChar(FN1,".",0) +Int 1)) +String FN2,D,B1,B2) [anywhere] rule createSchemaFromCollumns( .AsClauseOrCollumns , S:Schema) => s[ .Fields ] [anywhere,structural] rule createSchemaFromCollumns(C:Collumn,Cs:AsClauseOrCollumns,S:Schema) => addElement( getFieldFromSchema(C,S) , createSchemaFromCollumns(Cs,S)) [anywhere] rule createSchemaFromCollumns(C1:Collumn AS I:Id, Cs:AsClauseOrCollumns,S:Schema) => addElement( changeFieldNameTo(getFieldFromSchema(C1,S), #tokenToString(I) ) , createSchemaFromCollumns(Cs,S)) [anywhere] rule createSchemaFromCollumns(C1:Collumn AS ` I:Id `, Cs:AsClauseOrCollumns,S:Schema) => addElement( changeFieldNameTo(getFieldFromSchema(C1,S), #tokenToString(I) ) , createSchemaFromCollumns(Cs,S)) [anywhere] rule setPrimaryKey( KIds:Ids, TName:Id[ S : R]) => TName[setPrimaryKey(KIds, S) : R] [anywhere] rule setPrimaryKey( KIds:Ids , s[.Fields]) => s[.Fields] [anywhere] rule setPrimaryKey( KIds:Ids , s[f( S:String , T:DataType , B1, B2 ) , Fs:Fields] ) => addElement( f(S,T,true,B2) , setPrimaryKey(KIds, s[Fs])) when in(S,KIds) [anywhere] rule setPrimaryKey( KIds:Ids , s[f( S:String , T:DataType , B1, B2 ) , Fs:Fields] ) => addElement( f(S,T,B1,B2) , setPrimaryKey(KIds, s[Fs])) when notBool in(S,KIds) [anywhere] //rule createSchemaFromCollumns(C1:Collumn AS ` I1:Id . I2:Id `, Cs:AsClauseOrCollumns,S:Schema) => addElement( changeFieldNameTo(getFieldFromSchema(C1,S), #tokenToString(I2) ) , createSchemaFromCollumns(Cs,S)) [anywhere] //rule createSchemaFromCollumns(C1:Collumn AS I1:Id . I2:Id , Cs:AsClauseOrCollumns,S:Schema) => addElement( changeFieldNameTo(getFieldFromSchema(C1,S), #tokenToString(I2) ) , createSchemaFromCollumns(Cs,S)) [anywhere] rule doGetTableExp(FROM Is:Ids) => getTableFromIds(Is) rule doGetTableExp(FROM Is1:Ids JOIN Is2:Ids) => join(getTableFromIds(Is1),getTableFromIds(Is2)) rule doGetTableExp(FROM Is1:Ids JOIN Is2:Ids ON E:Exp) => join(getTableFromIds(Is1),getTableFromIds(Is2),E) rule doGetTableExp(FROM Is1:Id JOIN Is2:Id USING(Fs:FieldRep1s)) => joinUsing(getTableFromIds(Is1),getTableFromIds(Is2),changeCommonCollumnToEqualExp(Is1,Is2,Fs),Fs) rule doGetTableExp(FROM Is1:Ids INNER JOIN Is2:Ids) => join(getTableFromIds(Is1),getTableFromIds(Is2)) rule doGetTableExp(FROM Is1:Ids INNER JOIN Is2:Ids ON E:Exp) => join(getTableFromIds(Is1),getTableFromIds(Is2),E) rule doGetTableExp(FROM Is1:Id INNER JOIN Is2:Id USING(Fs:FieldRep1s)) => joinUsing(getTableFromIds(Is1),getTableFromIds(Is2),changeCommonCollumnToEqualExp(Is1,Is2,Fs),Fs) rule joinUsing(T1:Id[S1:Schema : R1:Record] , T2:Id[S2:Schema : R2:Record] , E:Exp , Fs:FieldRep1s) => join(T1:Id[S1:Schema : R1:Record] , T2:Id[S2:Schema : R2:Record] , E:Exp) ~> project(HOLE,concat(S1,excludeFields(S2,Fs))) rule T:#Table ~> project(HOLE,S) => project(T,S) [structural] rule doGetTableExp(FROM Is1:Ids LEFT JOIN Is2:Ids ON E:Exp) => leftJoin( getTableFromIds(Is1), getTableFromIds(Is2),E) rule doGetTableExp(FROM Is1:Id LEFT JOIN Is2:Id USING(Fs:FieldRep1s)) => leftJoinUsing( getTableFromIds(Is1), getTableFromIds(Is2),changeCommonCollumnToEqualExp(Is1,Is2,Fs),Fs) rule doGetTableExp(FROM Is1:Ids LEFT OUTER JOIN Is2:Ids ON E:Exp) => leftJoin( getTableFromIds(Is1), getTableFromIds(Is2),E) rule doGetTableExp(FROM Is1:Id LEFT OUTER JOIN Is2:Id USING(Fs:FieldRep1s)) => leftJoinUsing( getTableFromIds(Is1), getTableFromIds(Is2),changeCommonCollumnToEqualExp(Is1,Is2,Fs),Fs) rule leftJoinUsing(T1:Id[S1:Schema : R1:Record] , T2:Id[S2:Schema : R2:Record] , E:Exp , Fs:FieldRep1s) => leftJoin(T1:Id[S1:Schema : R1:Record] , T2:Id[S2:Schema : R2:Record] , E:Exp) ~> project(HOLE,concat(S1,excludeFields(S2,Fs))) rule doGetTableExp(FROM Is1:Ids RIGHT JOIN Is2:Ids ON E:Exp) => rightJoin( getTableFromIds(Is1),getTableFromIds(Is2),E) rule doGetTableExp(FROM Is1:Id RIGHT JOIN Is2:Id USING(Fs:FieldRep1s)) => rightJoinUsing( getTableFromIds(Is1),getTableFromIds(Is2),changeCommonCollumnToEqualExp(Is1,Is2,Fs),Fs) rule doGetTableExp(FROM Is1:Ids RIGHT OUTER JOIN Is2:Ids ON E:Exp) => rightJoin( getTableFromIds(Is1),getTableFromIds(Is2),E) rule doGetTableExp(FROM Is1:Id RIGHT OUTER JOIN Is2:Id USING(Fs:FieldRep1s)) => rightJoinUsing( getTableFromIds(Is1),getTableFromIds(Is2),changeCommonCollumnToEqualExp(Is1,Is2,Fs),Fs) rule rightJoinUsing(T1:Id[S1:Schema : R1:Record] , T2:Id[S2:Schema : R2:Record] , E:Exp , Fs:FieldRep1s) => rightJoin(T1:Id[S1:Schema : R1:Record] , T2:Id[S2:Schema : R2:Record] , E:Exp) ~> project(HOLE,concat(excludeFields(S1,Fs),S2)) rule doGetTableExp(FROM Is1:Ids CROSS JOIN Is2:Ids) => catesian( getTableFromIds(Is1), getTableFromIds(Is2)) rule doGetTableExp(FROM Is1:Ids CROSS JOIN Is2:Ids ON E:Exp) => join( getTableFromIds(Is1), getTableFromIds(Is2),E) rule doGetTableExp(FROM Is1:Id CROSS JOIN Is2:Id USING(Fs:FieldRep1s)) => joinUsing( getTableFromIds(Is1), getTableFromIds(Is2), changeCommonCollumnToEqualExp(Is1,Is2,Fs),Fs) rule doGetTableExp(FROM Is1:Id NATURAL JOIN Is2:Id) => naturalJoin(getTableFromIds(Is1),getTableFromIds(Is2)) rule naturalJoin(T1:Id[ S1:Schema : R1:Record ], T2:Id[ S2:Schema : R2:Record ]) => joinUsing(T1[ S1 : R1],T2[ S2 : R2 ],changeCommonCollumnToEqualExp(T1,T2,commonField(S1,S2)),commonField(S1,S2)) rule doGetTableExp(FROM Is1:Id NATURAL LEFT JOIN Is2:Id) => naturalLeftJoin(getTableFromIds(Is1),getTableFromIds(Is2)) rule doGetTableExp(FROM Is1:Id NATURAL LEFT OUTER JOIN Is2:Id) => naturalLeftJoin(getTableFromIds(Is1),getTableFromIds(Is2)) rule naturalLeftJoin(T1:Id[ S1:Schema : R1:Record ], T2:Id[ S2:Schema : R2:Record ]) => leftJoinUsing(T1[ S1 : R1],T2[ S2 : R2 ],changeCommonCollumnToEqualExp(T1,T2,commonField(S1,S2)),commonField(S1,S2)) rule doGetTableExp(FROM Is1:Id NATURAL RIGHT JOIN Is2:Id) => naturalRightJoin(getTableFromIds(Is1),getTableFromIds(Is2)) rule doGetTableExp(FROM Is1:Id NATURAL RIGHT OUTER JOIN Is2:Id) => naturalRightJoin(getTableFromIds(Is1),getTableFromIds(Is2)) rule changeCommonCollumnToEqualExp( T1:Id, T2:Id, .FieldRep1s ) => true [anywhere] rule changeCommonCollumnToEqualExp( T1:Id, T2:Id, F1:Id , Fs:FieldRep1s ) => (((T1.F1 = T2.F1):Exp) && (changeCommonCollumnToEqualExp(T1:Id,T2:Id, Fs:FieldRep1s))) [anywhere] rule changeCommonCollumnToEqualExp( T1:Id, T2:Id , ` F1:Id ` , Fs:FieldRep1s ) => (((T1.F1 = T2.F1):Exp) && (changeCommonCollumnToEqualExp(T1:Id,T2:Id, Fs:FieldRep1s))) [anywhere] rule naturalLeftJoin(T1:Id[ S1:Schema : R1:Record ], T2:Id[ S2:Schema : R2:Record ]) => leftJoinUsing(T1[ S1 : R1],T2[ S2 : R2 ],changeCommonCollumnToEqualExp(T1,T2,commonField(S1,S2)),commonField(S1,S2)) rule doGetTableExp(FROM Is1:Id NATURAL RIGHT JOIN Is2:Id) => naturalRightJoin(getTableFromIds(Is1),getTableFromIds(Is2)) rule doGetTableExp(FROM Is1:Id NATURAL RIGHT OUTER JOIN Is2:Id) => naturalRightJoin(getTableFromIds(Is1),getTableFromIds(Is2)) rule changeCommonCollumnToEqualExp( T1:Id, T2:Id , ` F1:Id ` , Fs:FieldRep1s ) => (((T1.F1 = T2.F1):Exp) && (changeCommonCollumnToEqualExp(T1:Id,T2:Id, Fs:FieldRep1s))) [anywhere] rule commonField(s[.Fields],S2:Schema) => .Ids [anywhere] rule commonField(s[f(FN1:String,D,B1,B2), Fs:Fields],S2:Schema) => hasCommonField(S2,f(FN1:String,D,B1,B2)) ~> if(HOLE,String2Id(substrString(FN1,(findChar(FN1,".",0) +Int 1),lengthString(FN1))) , commonField(s[Fs],S2),commonField(s[Fs],S2)) [anywhere] rule hasCommonField(s[ .Fields ], _ ) => false [anywhere] rule hasCommonField(s[f(FN1:String,D,B1,B2), Fs:Fields],f(FN2:String,_,_,_)) => true when substrString(FN1,(findChar(FN1,".",0) +Int 1),lengthString(FN1)) ==String substrString(FN2,(findChar(FN2,".",0) +Int 1),lengthString(FN2)) [anywhere] rule hasCommonField(s[f(FN1:String,D,B1,B2), Fs:Fields],f(FN2:String,D2,B3,B4)) => hasCommonField(s[Fs],f(FN2,D2,B3,B4)) when substrString(FN1,(findChar(FN1,".",0) +Int 1),lengthString(FN1)) =/=String substrString(FN2,(findChar(FN2,".",0) +Int 1),lengthString(FN2)) [anywhere] syntax AList ::= List{Int,"::"} syntax TupleA ::= add(TupleA,Int) syntax TupleA ::= "[" AList "]" rule add([A:AList],I:Int) => [I :: A] syntax Bool ::= eq(TupleA,TupleA) rule eq([A1:AList],[A2:AList]) => A1 =List A2 endmodule