Usage of nested specifications

[EmilyOng]

UPDATE (18 Dec): It has been fixed in https://github.com/songyahui/AlgebraicEffect/commit/98b67cf5b2bf71b31d2625464a5c4706faf1d6de

---

Example program

let foo xs
(*@ Norm(emp, 1) @*)
= 1

let goo xs
(*@ ex t; foo(xs, t); Norm(emp, t) @*)
= foo xs

Tracing (todo); Is this supposed to be failing?

https://github.com/EmilyOng/AlgebraicEffect/blob/StagedSL/parsing/forward_rules.ml#L275

Output

DEBUG=2 dune exec parsing/hip.exe src/examples/hello.ml

1                                      
Fatal error: exception Failure("there was a res term but not a variable")
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Hiplib.replacePredicatesWithDef.helper.(fun) in file "parsing/hiplib.ml", line 999, characters 18-68
Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19
Called from Hiplib.replacePredicatesWithDef.helper in file "parsing/hiplib.ml", line 993, characters 40-507
Called from Hiplib.replacePredicatesWithDef.helper in file "parsing/hiplib.ml", line 1023, characters 17-26
Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19
Called from Hiplib.replacePredicatesWithDef in file "parsing/hiplib.ml", line 1029, characters 19-61
Called from Hiplib.transform_strs.(fun) in file "parsing/hiplib.ml", line 1061, characters 22-57
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Hiplib.transform_strs in file "parsing/hiplib.ml", line 1034, characters 4-1023
Called from Hiplib.run_string_ in file "parsing/hiplib.ml", line 1567, characters 13-33
Called from Hiplib.run_file in file "parsing/hiplib.ml", line 1610, characters 6-21
Re-raised at Hiplib.run_file in file "parsing/hiplib.ml", line 1639, characters 6-13
Called from Hiplib.main in file "parsing/hiplib.ml", line 1645, characters 2-20
Called from Dune__exe__Hip in file "parsing/hip.ml", line 28, characters 4-18

[dariusf]

Thanks! Funnily enough it works if you remove the spec for foo. I've hotfixed it, but I think the real solution is to unfold all non-recursive predicates before trying to prove entailments. For higher-order functions there is no difference, but this is needed for the normalization done on handlers in the effect paper.

Feel free to make issues on the main repo too!