[K-Bug] missing hook of LIST.range?

[Lslightly]

What component is the issue in?

haskell-backend

Which command

• kompile
• kast
• krun
• kprove
• kprovex
• ksearch

What K Version?

K version: v5.6.22 Build date: Mon Apr 03 19:17:44 CST 2023

Operating System

Linux

K Definitions (If Possible)

module TEST
    imports LIST
    imports INT
    syntax List ::= prefixOfList(List, Int) [function]
    rule prefixOfList(Src:List, EndIdx:Int) => range(Src, 0, size(Src) -Int EndIdx) requires size(Src) >Int EndIdx
endmodule

github does not support uploading .k file

Steps to Reproduce

1. kompile test.k --backend haskell
2. krun -cPGM='prefixOfList(ListItem(0), 0)'
3. get such error information

kore-exec: [145843] Error (ErrorException):
    Error: missing hook
    Symbol
        LblList'Coln'range{}
    declared with attribute
        hook{}("LIST.range")
    We don't recognize that hook and it was not given any rules.
    Please open a feature request at
        https://github.com/runtimeverification/haskell-backend/issues
    and include the text of this message.
    Workaround: Give rules for LblList'Coln'range{}
    CallStack (from HasCallStack):
      error, called at src/Kore/Rewrite/Function/Evaluator.hs:371:6 in kore-0.60.0.0-J3wx87sugwq89e8bV2p6uj:Kore.Rewrite.Function.Evaluator
Created bug report: kore-exec.tar.gz
[Error] krun: kore-exec ./test-kompiled/haskellDefinition.bin --module TEST 
--pattern .krun-2023-04-23-15-46-46-Q3iDbrARTI/tmp.in.3niuLFHfua --output 
.krun-2023-04-23-15-46-46-Q3iDbrARTI/result.kore
[Error] krun: Backend crashed during rewriting with exit code 1

the generated .tar.gz file kore-exec.tar.gz

Expected Results

ListItem(0) .List

[Baltoli]

@ana-pantilie can this be implemented easily in the Haskell backend?

[Baltoli]

This can be implemented easily for concrete lists.

[jberthold]

This function could be implemented using rules that define range (recursively) . Maybe that should be tried first, although we can also implement range for lists (with caveats for symbolic ones).

[jberthold]

Has been implemented in the meanwhile #4108