K-user mailing list

[Radu Mereuta <headness13 AT gmail.com>]

This is definitely a problem in kompile.

Traian, can you have a look. I think the Context to Rules filter doesn't handle HOLE inside rules.

Radu

On Sun, Sep 15, 2013 at 9:16 PM, Ömer Sinan Ağacan <omeragacan AT gmail.com> wrote:

Hi all,

I'm having a weird maude error while trying to run my K program. Does
anyone have any ideas on what's going on here?

    ➜  test git:(master) ✗ kompile test.k -v && krun test
    Including file: /home/omer/K/lua-semantics/test/test.k
    Including file: /home/omer/K/k/dist/include/autoinclude.k
    Including file: /home/omer/K/k/dist/include/k-prelude.k
    Including file: /home/omer/K/k/dist/include/builtins/builtins.k
    Including file: /home/omer/K/k/dist/include/builtins/bool.k
    Including file: /home/omer/K/k/dist/include/builtins/int.k
    Including file: /home/omer/K/k/dist/include/builtins/k-equal.k
    Including file: /home/omer/K/k/dist/include/builtins/array.k
    Including file: /home/omer/K/k/dist/include/builtins/float.k
    Including file: /home/omer/K/k/dist/include/builtins/string.k
    Including file: /home/omer/K/k/dist/include/builtins/id.k
    Including file: /home/omer/K/k/dist/include/io/tcp.k
    Including file: /home/omer/K/k/dist/include/builtins/random.k
    Including file: /home/omer/K/k/dist/include/builtins/counter.k
    Including file: /home/omer/K/k/dist/include/builtins/symbolic-k.k
    Including file: /home/omer/K/k/dist/include/modules/substitution.k
    Including file: /home/omer/K/k/dist/include/modules/pattern-matching.k
    Including file: /home/omer/K/k/dist/include/io/uris.k
    Basic Parsing                                                =   321
    Preprocess                                                   =   134
    Checks                                                       =     8
    File Gen Pgm                                                 =    21
    Generate TBLPgm                                              =    80
    File Gen Def                                                 =   158
    Generate TBLDef                                              =  4487
    Importing Files                                              =  1096
    Parsing Configs                                              =   381
    Parsing Rules                                                =  4788
    Serialize Definition to XML                                  =   411
    Generating equations for hooks                               =    29
    Check that configuration cells have unique names             =     3
    Remove brackets                                              =     5
    Add empty lists                                              =     5
    Remove syntactic casts                                       =     4
    class org.kframework.compile.checks.CheckVariables           =     5
    class org.kframework.compile.checks.CheckRewrite             =     5
    Strict Ops To Context                                        =     4
    Freeze User Freezers                                         =     1
    Contexts to Heating Rules                                    =     0
    AddSupercoolDefinition                                       =     1
    Generate Heating Conditions                                  =     1
    Add Superheat rules                                          =     0
    Desugar streams                                              =     1
    Resolve Functions                                            =     2
    Add K cell                                                   =     3
    Add cells to stream rules                                    =     0
    Add symbolic constructors                                    =     1
    Define semantic equality                                     =     5
    Transform fresh conditions into fresh variables.             =     3
    Resolve fresh variables (MOS version).                       =     5
    Add top cell for configurations                              =     1
    Resolve binder                                               =     1
    Resolve anonymous variables                                  =     4
    Resolve Blocking Input                                       =     2
    Add translation from K to Z3 SMTlib v2 string                =     5
    Add syntax and symbolic predicates                           =    17
    Resolve syntax predicates                                    =    34
    Resolve Builtins                                             =     3
    Resolve KList                                                =    14
    Syntax K to Abstract K                                       =   123
    Define KLabel2String and String2Klabel for KLabel constants  =    27
    Define isKLabelConstant predicate for KLabel constants       =     6
    Resolve Hybrid                                               =     2
    Resolve Context Abstraction                                  =     7
    Resolve Default Terms                                        =     4
    Resolve Open Cells                                           =    38
    Pushing local rewrites to top                                =     3
    Compile collections to internal K representation             =    23
    Cool the <k> cell for supercool rules                        =     1
    AddStrictStar                                                =    14
    AddDefaultComputational                                      =     3
    AddOptionalTags                                              =     7
    Generating Maude file                                        =   170
    Total                                                        = 12523
    Number of Modules                                            =     2
    Number of Sentences                                          =     3
    Number of Productions                                        =     5
    Number of Cells                                              =     0
    Krun was executed with the following arguments:
    k_definition=/home/omer/K/lua-semantics/test/test.k
    syntax_module=TEST
    main_module=TEST
    compiled_def=/home/omer/K/lua-semantics/test/test-kompiled

    Warning: Compiled definition file name (test) and the extension of
the program () aren't the same. Maybe you should use --syntax-module
or --main-module options of krun
    Warning: Maude produced warnings or errors.
    Warning: "base.maude", line 5 (mod TEST-BASE): bad token HOLE.
    Warning: "base.maude", line 5 (mod TEST-BASE): no parse for statement
    eq <_>_</_> (k, _~>_ (_`(_`) ('return, Test:K),
GeneratedFreshVar0:K), k) = <_>_</_> (k, _~>_ (_~>_ (Test:K, _`(_`)
('returnVal, HOLE)), GeneratedFreshVar0:K), k) [metadata
"filename=(/home/omer/K/lua-semantics/test/test.k)
location=(16,3,16,59) computational=()"] .
    Warning: "base.maude", line 7 (mod TEST-BASE): bad token HOLE.
    Warning: "base.maude", line 7 (mod TEST-BASE): no parse for statement
    ceq <_>_</_> (k, _~>_ (_~>_ (V:KItem, _`(_`) ('returnVal, HOLE)),
GeneratedFreshVar0:K), k) = <_>_</_> (k, _~>_ (_`(_`) ('returnVal,
V:KItem), GeneratedFreshVar0:K), k) if _`(_`) (isVal, V:KItem) =
_`(_`) (# true, .KList) [metadata
"filename=(/home/omer/K/lua-semantics/test/test.k)
location=(17,3,17,60) computational=()"] .

    ➜  test git:(master) ✗ cat test.k
    module TEST-SYNTAX

      syntax Test ::= "nilExp" | return(Test) | returnVal(Val)

      syntax Val ::= "nil"

      syntax KReuslt ::=  Val

    endmodule

    module TEST

      imports TEST-SYNTAX

      rule <k> nilExp => nil ... </k>
      rule <k> return(Test) => Test ~> returnVal(HOLE) ... </k>
      rule <k> V:Val ~> returnVal(HOLE) => returnVal(V) ... </k>

    endmodule
    ➜  test git:(master) ✗ cat test
    return(nilExp)
    ➜  test git:(master) ✗

Thanks.


---
Ömer Sinan Ağacan
http://osa1.net

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user