Skip to content

Commit

Permalink
Clean up formatting of examples. #148
Browse files Browse the repository at this point in the history
  • Loading branch information
@epost
epost committed Aug 7, 2019
1 parent b7b6e91 commit 40476b6
Show file tree
Hide file tree
Showing 8 changed files with 490 additions and 499 deletions.
68 changes: 34 additions & 34 deletions examples/Congruence.cql
View file
Original file line number Diff line number Diff line change
@@ -1,38 +1,38 @@
options
prover = congruence
typeside T = literal {
types
string
nat
constants
Al Akin Bob Bo Carl Cork Dan Dunn Math CS : string
zero : nat
functions
succ : nat -> nat
plus : nat, nat -> nat
prover
options = congruence

typeside T = literal {
types
string
nat
constants
Al Akin Bob Bo Carl Cork Dan Dunn Math CS : string
zero : nat
functions
succ : nat -> nat
plus : nat, nat -> nat
}

schema S = literal : T {
entities
Employee
Department
foreign_keys
manager : Employee -> Employee
worksIn : Employee -> Department
secretary : Department -> Employee
attributes
first last : Employee -> string
age : Employee -> nat
name : Department -> string
schema S = literal : T {
entities
Employee
Department
foreign_keys
manager : Employee -> Employee
worksIn : Employee -> Department
secretary : Department -> Employee
attributes
first last : Employee -> string
age : Employee -> nat
name : Department -> string
}

instance I = literal : S {
generators
a b : Employee
equations
a.manager=a a.worksIn.secretary=a
b.manager=a b.worksIn = a.worksIn
first(a) = Al
first(b) = Bob last(b) = Bo
}
instance I = literal : S {
generators
a b : Employee
equations
a.manager=a a.worksIn.secretary=a
b.manager=a b.worksIn = a.worksIn
first(a) = Al
first(b) = Bob last(b) = Bo
}
134 changes: 66 additions & 68 deletions examples/Delta.cql
View file
Original file line number Diff line number Diff line change
@@ -1,96 +1,94 @@
typeside Ty = literal {
types
int
string
constants
// "100" "150" "200" "250" "300" : int
// "115-234" "112-988" "198-887" Smith Jones "250" "300" "100" : string
options
allow_empty_sorts_unsafe = true
types
int
string
// constants
// "100" "150" "200" "250" "300" : int
// "115-234" "112-988" "198-887" Smith Jones "250" "300" "100" : string
options
allow_empty_sorts_unsafe = true
}

schema C = literal : Ty {
entities
T1 T2
attributes
ssn first1 last1 : T1 -> string
first2 last2 : T2 -> string
salary : T2 -> int
options
allow_empty_sorts_unsafe = true
entities
T1 T2
attributes
ssn first1 last1 : T1 -> string
first2 last2 : T2 -> string
salary : T2 -> int
options
allow_empty_sorts_unsafe = true
}

schema D = literal : Ty {
entities
T
attributes
ssn0 first0 last0 : T -> string
salary0 : T -> int
options
allow_empty_sorts_unsafe = true
entities
T
attributes
ssn0 first0 last0 : T -> string
salary0 : T -> int
options
allow_empty_sorts_unsafe = true
}

mapping F = literal : C -> D {
entity
T1 -> T
attributes
ssn -> lambda x. ssn0(x)
first1 -> lambda x. first0(x)
last1 -> lambda x. x.last0

entity
T2 -> T
attributes
last2 -> lambda x. x.last0
salary -> salary0 //dot notation
first2 -> lambda x. x.first0
}

instance J = literal : D {
generators
XF667 XF891 XF221 : T
equations
// XF667.ssn0 = "115-234" XF891.ssn0 = "112-988" XF221.ssn0 = "198-887"
// XF667.first0 = Bob XF891.first0 = Sue XF221.first0 = Alice
// XF667.last0 = Smith XF891.last0 = Smith XF221.last0 = Jones
// XF667.salary0 = 250 XF891.salary0 = 300 XF221.salary0 = 100
options
allow_empty_sorts_unsafe = true
}
entity
T1 -> T
attributes
ssn -> lambda x. ssn0(x)
first1 -> lambda x. first0(x)
last1 -> lambda x. x.last0

entity
T2 -> T
attributes
last2 -> lambda x. x.last0
salary -> salary0 // dot notation
first2 -> lambda x. x.first0
}

instance J = literal : D {
generators
XF667 XF891 XF221 : T
equations
// XF667.ssn0 = "115-234" XF891.ssn0 = "112-988" XF221.ssn0 = "198-887"
// XF667.first0 = Bob XF891.first0 = Sue XF221.first0 = Alice
// XF667.last0 = Smith XF891.last0 = Smith XF221.last0 = Jones
// XF667.salary0 = 250 XF891.salary0 = 300 XF221.salary0 = 100
options
allow_empty_sorts_unsafe = true
}

instance deltaFJ = delta F J

instance J0 = literal : D {
generators
XF22 aXF66 XF89 xxx : T
equations
//aXF66.ssn0 = "115-234" XF89.ssn0 = "112-988" XF22.ssn0 = "198-887"
// aXF66.first0 = Bob XF89.first0 = Sue XF22.first0 = Alice
//aXF66.last0 = Smith XF89.last0 = Smith XF22.last0 = Jones
//aXF66.salary0 = 250 XF89.salary0 = 300 XF22.salary0 = 100
options
allow_empty_sorts_unsafe = true
generators
XF22 aXF66 XF89 xxx : T
// equations
// aXF66.ssn0 = "115-234" XF89.ssn0 = "112-988" XF22.ssn0 = "198-887"
// aXF66.first0 = Bob XF89.first0 = Sue XF22.first0 = Alice
// aXF66.last0 = Smith XF89.last0 = Smith XF22.last0 = Jones
// aXF66.salary0 = 250 XF89.salary0 = 300 XF22.salary0 = 100
options
allow_empty_sorts_unsafe = true
}

transform h = literal : J -> J0 {
generators
XF667 -> aXF66
XF891 -> XF89
XF221 -> XF22
generators
XF667 -> aXF66
XF891 -> XF89
XF221 -> XF22
}

transform h0 = delta F h

instance sigmadeltaFJ = sigma F deltaFJ {
options
program_allow_nontermination_unsafe = true
allow_empty_sorts_unsafe = true
options
program_allow_nontermination_unsafe = true
allow_empty_sorts_unsafe = true
}

transform u = counit F J {
options
program_allow_nontermination_unsafe = true
allow_empty_sorts_unsafe = true
options
program_allow_nontermination_unsafe = true
allow_empty_sorts_unsafe = true
}
123 changes: 61 additions & 62 deletions examples/Employee.cql
View file
Original file line number Diff line number Diff line change
@@ -1,67 +1,66 @@
options
//prover = completion
program_allow_nontermination_unsafe = true
allow_empty_sorts_unsafe = true
//timeout = "1"

typeside T = literal {
types
string
nat
constants
Al Akin Bob Bo Carl Cork Dan Dunn Math CS : string
zero : nat
functions
succ : nat -> nat
plus : nat, nat -> nat
equations
// zero = zero
// forall x . plus(zero, x) = x
// forall x , y . plus(succ(x),y) = succ(plus(x,y))
}
options
//prover = completion
program_allow_nontermination_unsafe = true
allow_empty_sorts_unsafe = true
//timeout = "1"

schema S = literal : T {
entities
Employee
Department
foreign_keys
manager : Employee -> Employee
worksIn : Employee -> Department
secretary : Department -> Employee
attributes
first last : Employee -> string
age : Employee -> nat
name : Department -> string
observation_equations
// forall e. e.first = Al

}
typeside T = literal {
types
string
nat
constants
Al Akin Bob Bo Carl Cork Dan Dunn Math CS : string
zero : nat
functions
succ : nat -> nat
plus : nat, nat -> nat
// equations
// zero = zero
// forall x . plus(zero, x) = x
// forall x , y . plus(succ(x),y) = succ(plus(x,y))
}

instance I = literal : S {
generators
a b : Employee
equations
a.manager=a a.worksIn.secretary=a
b.manager=a b.worksIn = a.worksIn
last(b) = Bo
schema S = literal : T {
entities
Employee
Department
foreign_keys
manager : Employee -> Employee
worksIn : Employee -> Department
secretary : Department -> Employee
attributes
first last : Employee -> string
age : Employee -> nat
name : Department -> string
// observation_equations
// forall e. e.first = Al
}

multi_equations
first -> {a Al, b Bob}

}
instance I = literal : S {
generators
a b : Employee
equations
a.manager=a a.worksIn.secretary=a
b.manager=a b.worksIn = a.worksIn
last(b) = Bo

multi_equations
first -> {a Al, b Bob}
}

instance J = literal : S {
generators
a b : Employee
c d : Department

y:nat
equations
a.manager=a a.worksIn = d c.secretary=b
b.manager=a b.worksIn = c d.secretary=b
first(a) = Al a.last = Al d.name=Bob
c.name = Al
age(a)=zero age(b) = y
options interpret_as_algebra = true
}
instance J = literal : S {
generators
a b : Employee
c d : Department
y : nat
equations
a.manager = a a.worksIn = d c.secretary = b
b.manager = a b.worksIn = c d.secretary = b
first(a) = Al
a.last = Al
d.name = Bob
c.name = Al
age(a) = zero
age(b) = y
options interpret_as_algebra = true
}
Loading

0 comments on commit 40476b6

Please sign in to comment.