epost
commented
4 years ago Some very very nice progress:
$ stack exec cql examples/Employee.cqlnow gives us:
typesides
"T" = TypesideRaw (TypesideRaw' {tsraw_tys = ["string","nat"], tsraw_syms = [("Al",([],"string")),("Akin",([],"string")),("Bob",([],"string")),("Bo",([],"string")),("Carl",([],"string")),("Cork",([],"string")),("Dan",([],"string")),("Dunn",([],"string")),("Math",([],"string")),("CS",([],"string")),("zero",([],"nat")),("succ",(["nat"],"nat")),("plus",(["nat","nat"],"nat"))], tsraw_eqs = [], tsraw_options = [], tsraw_imports = []})
schemas
"S" = TypesideVar "T"
instances
"I" = SchemaVar "S"
"J" = SchemaVar "S"
mappings
queries
transforms
other
()
-------------------
typesides
"T" = typeside
types
"nat"
"string"
functions
"Akin" : [] -> "string"
"Al" : [] -> "string"
"Bo" : [] -> "string"
"Bob" : [] -> "string"
"CS" : [] -> "string"
"Carl" : [] -> "string"
"Cork" : [] -> "string"
"Dan" : [] -> "string"
"Dunn" : [] -> "string"
"Math" : [] -> "string"
"plus" : ["nat","nat"] -> "nat"
"succ" : ["nat"] -> "nat"
"zero" : [] -> "nat"
equations
schemas
"S" = schema
entities
"Department"
"Employee"
foreign_keys
"manager" : "Employee" -> "Employee"
"secretary" : "Department" -> "Employee"
"worksIn" : "Employee" -> "Department"
atts
"age" : "Employee" -> "nat"
"first" : "Employee" -> "string"
"last" : "Employee" -> "string"
"name" : "Department" -> "string"
path_equations
observation_equations
instances
"I" = instance
presentation
generators
"a" : "Employee"
"b" : "Employee"
equations
a.first = Al
a.manager = a
a.worksIn.secretary = a
b.first = Bob
b.last = Bo
b.manager = a
b.worksIn = a.worksIn
algebra
entities
"Department" (1)
+-----------++--------------------------+-------------------+
| || "secretary" : "Employee" | "name" : "string" |
+===========++==========================+===================+
| a.worksIn || a | (a.worksIn,name) |
+-----------++--------------------------+-------------------+
"Employee" (2)
+---++------------------------+--------------------------+---------------+--------------------+-------------------+
| || "manager" : "Employee" | "worksIn" : "Department" | "age" : "nat" | "first" : "string" | "last" : "string" |
+===++========================+==========================+===============+====================+===================+
| a || a | a.worksIn | (a,age) | Al | (a,last) |
+---++------------------------+--------------------------+---------------+--------------------+-------------------+
| b || a | a.worksIn | (b,age) | Bob | Bo |
+---++------------------------+--------------------------+---------------+--------------------+-------------------+
type-algebra
nulls
"nat" (2) = [(a,"age"),(b,"age")]
"string" (2) = [(a.worksIn,"name"),(a,"last")]
"J" = instance
presentation
generators
"a" : "Employee"
"b" : "Employee"
"c" : "Department"
"d" : "Department"
equations
a.age = zero
a.first = Al
a.last = Al
a.manager = a
a.worksIn = d
b.age = y
b.manager = a
b.worksIn = c
c.name = Al
c.secretary = b
d.name = Bob
d.secretary = b
algebra
entities
"Department" (2)
+-----++--------------------------+-------------------+
| || "secretary" : "Employee" | "name" : "string" |
+=====++==========================+===================+
| "c" || "b" | Al |
+-----++--------------------------+-------------------+
| "d" || "b" | Bob |
+-----++--------------------------+-------------------+
"Employee" (2)
+-----++------------------------+--------------------------+---------------+--------------------+-------------------+
| || "manager" : "Employee" | "worksIn" : "Department" | "age" : "nat" | "first" : "string" | "last" : "string" |
+=====++========================+==========================+===============+====================+===================+
| "a" || "a" | "d" | zero | Al | Al |
+-----++------------------------+--------------------------+---------------+--------------------+-------------------+
| "b" || "a" | "c" | Left y | Right (b,first) | Right (b,last) |
+-----++------------------------+--------------------------+---------------+--------------------+-------------------+
type-algebra
nulls
"nat" (1) = [Left "y"]
"string" (2) = [Right ("b","first"),Right ("b","last")]
mappings
queries
transforms
other
Timeout = 30
Require_Consistency = True
Dont_Validate_Unsafe = False
Program_Allow_Nonconfluence_Unsafe = False
Interpret_As_Algebra = False
Program_Allow_Nontermination_Unsafe = True
Allow_Empty_Sorts_Unsafe = True
Prover = auto
fyi @marcosh @dannce