Duplicate rules and sentences in compiled output

Start with the supplied test.k definition and run kompile test.k, then inspect test-kompiled/compiled.txt and compare the repeated isK sentence across imported modules such as KSEQ and KSEQ-SYMBOLIC. Trace where imported sentences and sort predicates enter the compiled output; done means duplicate predicates are reduced without changing the resulting definitions.

Using the following definition:

module TEST
    imports BOOL
    imports INT

    configuration <k> $PGM:Pgm </k>

    syntax Pgm ::= Bool | Int

endmodule

module TEST-SYMBOLIC [kore, symbolic]
    imports TEST

    rule A andBool B => B andBool A [simplification]
endmodule

module TEST-LLVM [symbolic]
    imports TEST-SYMBOLIC
endmodule

I call kompile test.k, to get output test-kompiled/compiled.txt.

Then I search for a rule that looks like this (the isK sort predicate):

  rule isK(K)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(16ff77cff0ef50026a8b3f4614b87bda465701918596b7ad2280baffff56f847)]

And find that there are 50 occurrences of the same rule! This is not the only sort predicate with many duplicate occurrences.

Can we eliminate these duplicates by:

• Having the compiler do something about it? Like factor out the sort predicates into their own module that is imported where it's needed?
• Refactoring our prelude/import structure a bit so that commonly duplicated sorts like K and KItem and List are declared early so their sort predicates only occur once?
• Note that we have an instance where module KSEQ declares the isK predicate, and module KSEQ-SYMBOLIC imports KSEQ but still also redeclares this sort predicate! So maybe there is a way to minimize the number of sentences directly already by not regenerating sort predicates if they already exist in imported modules.

Example from compiled.txt (snipped):

module KSEQ
  imports KAST
  imports K-TOP-SORT
  syntax {Sort} Sort ::= "(" Sort ")" [applyPriority(1), bracket, bracketLabel((_)_KSEQ_Sort_Sort{Sort}), defaultBracket]
  syntax associativity left #KSequence [org.kframework.attributes.Location(Location(104,3,104,25)), org.kframework.attributes.Source(Source(/nix/store/hdn1n6x3lclacnv59xc8wzmgravia6jw-k-6.1.77-18ce58892d77b05f8aa5
  syntax associativity left #KSequence
  syntax K ::= K "~>" K [assoc, klabel(#KSequence), left, symbol, unit(#EmptyK)]
  syntax K ::= ".K" [klabel(#EmptyK), symbol, unparseAvoid]
  syntax K ::= ".::K" [klabel(#EmptyK), symbol, unparseAvoid]
  syntax K ::= "." [klabel(#EmptyK), symbol] 
    ... 
  rule isK(K)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(16ff77cff0ef50026a8b3f4614b87bda465701918596b7ad2280baffff56f847)] 
    ... 
endmodule


module KSEQ-SYMBOLIC
  imports ML-SYNTAX
  imports KVARIABLE-SYNTAX
  imports KSEQ
  syntax KConfigVar ::= r"(?<![A-Za-z0-9_\\$!\\?@])(\\$)([A-Z][A-Za-z0-9'_]*)" [token]
  syntax KBott ::= KConfigVar
  syntax KBott ::= #KVariable
  syntax #KVariable ::= r"(?<![A-Za-z0-9_\\$!\\?@])(\\!|\\?|@)?([A-Z][A-Za-z0-9'_]*|_|_[A-Z][A-Za-z0-9'_]*)" [prec(1), token]
  syntax #KVariable ::= #UpperId [token] 
    ... 
  rule isK(K)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(16ff77cff0ef50026a8b3f4614b87bda465701918596b7ad2280baffff56f847)] 
    ... 
endmodule