Skip to content

Invalid Cosette program yields invalid Coq code #76

@qaisjp

Description

@qaisjp

Input example:

/* define schema employee, 
   here employee can contain any number of attributes, 
   but it has to at least contain integer attributes 
   eid and age */
schema customer(id:int, name:text, city:text);
schema account(num:int, branch:text, custid:int, balance:int);        

-- define table uw_emp using schema s1
table accs(account);
-- define table uw_sal using schema s1
table custs(customer);

-- define query q1 over uw_emp and uw_payroll
query q1                
`select c.id, c.name
    from accs a, custs c
    where c.id=a.custid
    and balance = (select max(al.balance) from accs as al)
    group by c.id, c.name`;

-- define query q2 likewise
query q2                
`select distinct c.id, c.name
    from accs a, custs c
    where c.id=a.custid
    and balance = (select max(al.balance) from accs as al)
    `;

verify q1 q2;           -- does q1 equal to q2?

Which causes the following error output:

Invalid generated Coq code. Please file an issue.

{"size":[1],"status":"UNSAT"}
generated/jxOJRPUUIWDyf.rkt:19:47: balance: unbound identifier in module
in: balance
context...:
/root/.racket/6.8/pkgs/rosette/rosette/base/form/module.rkt:16:0
standard-module-name-resolver
/Cosette-Web/backend/Cosette/rosette/server.rkt:38:10

Problematic line: and balance = (select max(al.balance) from accs as al)

It should be: and a.balance = [..]

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions