K-user mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Here's a minimal valid K program that fails to compile with
java-symbolic backend

    module ERROR

      syntax S ::= "s"

      configuration
        <k> $PGM:S </k>
        <out stream="stdout"> .List </out>

    endmodule

Andrei, do we have any readings on K backends other than
org.kframework.krun.api.KRun and org.kframework.backend.Backend
interfaces? (for general questions like "what does a rewrite engine
do" or more specific ones like "how does java backend work")

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


2013/9/23 Andrei Stefanescu 
<andreistef AT gmail.com>:
> Yeah, that is correct (the description may need updating). As for the
> Exception, you have to give me more details (it is a feature that my backend
> does not support.
>
> Andrei
>
>
>
> On Mon, Sep 23, 2013 at 3:28 PM, Ömer Sinan Ağacan 
> <omeragacan AT gmail.com>
> wrote:
>>
>> Interesting. in kompile --help ml parameter is described as:
>>
>>
>>  -ml,--matching-logic            generate support for matching logic
>>                                  prover
>>
>> Is this correct?
>>
>>
>> Also, kompilation fails with null pointer exception:
>>
>>     ➜  lua-semantics git:(master) ✗ kompile -ml -v lua
>>     Including file: /home/omer/K/lua-semantics/lua.k
>>     Including file: /home/omer/K/lua-semantics/lua-configuration.k
>>     Including file: /home/omer/K/lua-semantics/lua-syntax.k
>>     Including file: /home/omer/K/lua-semantics/lua-binop.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                                                =   334
>>     Preprocess                                                   =   164
>>     Checks                                                       =    10
>>     File Gen Pgm                                                 =    37
>>     Generate TBLPgm                                              =   241
>>     File Gen Def                                                 =   209
>>     Generate TBLDef                                              =  9229
>>     Importing Files                                              =  1170
>>     Parsing Configs                                              =   519
>>     Parsing Rules                                                =  4113
>>     Serialize Definition to XML                                  =   492
>>     Check that configuration cells have unique names             =    16
>>     Remove brackets                                              =     5
>>     Add empty lists                                              =     6
>>     Remove syntactic casts                                       =     4
>>     class org.kframework.compile.checks.CheckVariables           =     6
>>     class org.kframework.compile.checks.CheckRewrite             =     7
>>     Set the sort of each variable to the inferred sort           =     8
>>     Subsort syntactic lists                                      =    33
>>     Serialize Compiled Definition to XML                         =   116
>>     Strict Ops To Context                                        =     3
>>     Freeze User Freezers                                         =     1
>>     Contexts to Heating Rules                                    =     3
>>     Generate Heating Conditions                                  =     1
>>     java.lang.NullPointerException
>>             at
>> org.kframework.compile.transformers.DesugarStreams.newListItem(DesugarStreams.java:127)
>>             at
>> org.kframework.compile.transformers.DesugarStreams.makeStreamList(DesugarStreams.java:88)
>>             at
>> org.kframework.compile.transformers.DesugarStreams.transform(DesugarStreams.java:42)
>>             at org.kframework.kil.Cell.accept(Cell.java:266)
>>             at
>> org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:365)
>>             at
>> org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:390)
>>             at org.kframework.kil.Bag.accept(Bag.java:55)
>>             at
>> org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:112)
>>             at
>> org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:161)
>>             at
>> org.kframework.kil.Configuration.accept(Configuration.java:51)
>>             at
>> org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:75)
>>             at org.kframework.kil.Module.accept(Module.java:102)
>>             at
>> org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:42)
>>             at org.kframework.kil.Definition.accept(Definition.java:121)
>>             at
>> org.kframework.compile.utils.CompilerTransformerStep.compile(CompilerTransformerStep.java:24)
>>             at
>> org.kframework.compile.utils.CompilerSteps.compile(CompilerSteps.java:37)
>>             at
>> org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:294)
>>             at
>> org.kframework.kompile.KompileFrontEnd.kompile(KompileFrontEnd.java:250)
>>             at org.kframework.main.Main.main(Main.java:69)
>>     Total                                                        = 16730
>>     Number of Modules                                            =     4
>>     Number of Sentences                                          =    20
>>     Number of Productions                                        =    86
>>     Number of Cells                                              =     9
>>     ➜  lua-semantics git:(master) ✗
>>
>> ---
>> Ömer Sinan Ağacan
>> http://osa1.net
>>
>>
>> 2013/9/23 Andrei Stefanescu 
>> <andreistef AT gmail.com>:
>> > kompile -ml
>> >
>> > Andrei
>> >
>> >
>> >
>> > On Mon, Sep 23, 2013 at 3:06 PM, Ömer Sinan Ağacan
>> > <omeragacan AT gmail.com>
>> > wrote:
>> >>
>> >> Hi all,
>> >>
>> >> How can I compile my K apps for java-symbolic backend?
>> >>
>> >> 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
>> >
>> >
>
>