[CN] Unify scopes of predicates and functions (confusing err msg for "return (Predicate(args))")

[bcpierce00]

The CN file

/*@
predicate (i32) IntQueueAux(i32 x) {
  return (x);
}

predicate (i32) IntQueue1() {
  return (IntQueueAux (0i32));
}
@*/

produces the error message:

parseError.broken.c:12:11: error: the specification function `IntQueueAux' is not declared
OOPS:   return (IntQueueAux (H.head, H.tail));

Why?

[dc-mak]

In CN, as things currently stand, predicates are separation logic predicates ("stateful") and function are pure, referring only to purely logical terms. This is stratified in practice by having functions and predicates living in separate namespaces I think. The error is saying that it can't find "IntQueueAux" in the purely logical function list of declarations, which is true. If I Haskell-ified the above it would be something like

IntQueueAux :: i32 -> Heap i32
IntQueueAux x = return x

IntQueue1 :: () -> Heap i32
IntQueue1 () = return (IntQueue 0)

whereas what you'd actually want is something like

IntQueue1 () = do 
    x <- IntQueue 0;
    return x

Or in CN terms

predicate (i32) IntQueue1() {
    take X = IntQueueAux(0i32);
    return X;
}

Perhaps this suggests that syntactically, the declaration of predicates and functions could be unified? We have some syntactic restrictions on predicates right now but a potential future syntax like this may be worth considering:

fun (i32) add_one(i32 x) {
  x + 1;
}

fun (heap<i32>) intQueueAux(i32 x) {
  return (add_one(x));
 }

fun (heap<i32>) intQueue(i32 x) {
  intQueueAux(0);
}

[bcpierce00]

Thank you!

The example may have gotten simplified too much, though. What I was trying to do by introducing IntQueue1 was get around the restriction on "if" after "take". Maybe someone that understands CN could sit with me for a few minutes before or after the CN meeting today and take a look at the actual code...

On Tue, Jun 4, 2024 at 5:16 AM Dhruv Makwana @.***> wrote:

In CN, as things currently stand, predicates are separation logic predicates ("stateful") and function are pure, referring only to purely logical terms. This is stratified in practice by having functions and predicates living in separate namespaces I think. The error is saying that it can't find "IntQueueAux" in the purely logical function list of declarations, which is true. If I Haskell-ified the above it would be something like

IntQueueAux :: i32 -> Heap i32 IntQueueAux x = return x

IntQueue1 :: () -> Heap i32 IntQueue1 () = return (IntQueue 0)

whereas what you'd actually want is something like

IntQueue1 () = do x <- IntQueue 0; return 0

Or in CN terms

predicate (i32) IntQueue1() { take X = IntQueueAux(0i32); return X; }

Perhaps this suggests that syntactically, the declaration of predicates and functions could be unified?

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/rems-project/cerberus/issues/288*issuecomment-2147024195__;Iw!!IBzWLUs!T2fQAuBTScqvWYyLLDijvQMboItqn0sZZnkRiheyV2-kn-Glqn4q6sx0mnbcwuSTsvzrsGyLtJbj6Q4TOw8VH45W7n04$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/ABVQQC66PCVBDLVXUHJKR33ZFWAXVAVCNFSM6AAAAABIXEDAZ6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCNBXGAZDIMJZGU__;!!IBzWLUs!T2fQAuBTScqvWYyLLDijvQMboItqn0sZZnkRiheyV2-kn-Glqn4q6sx0mnbcwuSTsvzrsGyLtJbj6Q4TOw8VHz-ZWjlb$ . You are receiving this because you authored the thread.Message ID: @.***>