I think I should put this change to a different pull request. It is not related to kore parser.

It is actually related to another project -- LLVM. In the original code, when I compile this set of rules, it cannot compiled:

require "builtins/list.k"
require "builtins/map.k"
/* make all values ints, use K variables for variables? */

module SMT /* defining my own for now */

  syntax K ::= getModel(Bool) [function, hook(#BOOL:checksat_)]

  syntax Bool ::= "[E]K"K"."Bool

endmodule

module TRANS2-SYNTAX
  imports MAP
  imports LIST

  syntax Node ::= Int | Id

  syntax NodeLit ::= "Start" Int | "Exit" Int | Node

  syntax Type ::= "seq" | "branch"
               
/* Can we parameterize by this? */
  syntax Instr ::= Node ":=" Node | "skip" /* put in a dummy, languages extend */
  syntax Instrs ::= List{Instr,","}

  syntax Action ::= "replace" NodeLit "with" Instrs
	| "add-edge("NodeLit"," NodeLit"," Type")"
 	| "remove-edge("NodeLit"," NodeLit"," Type")"
	| "split-edge("NodeLit"," NodeLit"," Type"," Instr")"

  syntax Pred ::= "node" Node NodeLit | "stmt" Node "("Instr")"

  syntax SideCond ::= "True" | Pred | SideCond "and" SideCond
	| "not" SideCond | "ALL" SideCond "U" SideCond
	| "EX" SideCond "U" SideCond | "ALL" SideCond "BACKTO" SideCond
	| "EX" SideCond "BACKTO" SideCond | "EX" Int "." SideCond
  | "EF" SideCond [prefer] // or [:prec 40:]

/* Note: K doesn't like "A" or "B" as operators.  Pity. */

  syntax Actions ::= List{Action,";"}

  syntax Trans ::= Actions "if" SideCond 
	| "MATCH" SideCond "IN" Trans | "APPLY-ALL" Trans 
	| Trans "THEN" Trans | Trans "[]" Trans
               

/* Concrete syntax for flowgraphs */
  syntax Nodes ::= List{Node,","}

  syntax Edge ::= "e(" Node "," Node "," Type ")"
  syntax Edges ::= List{Edge,","}

  syntax Maplet ::= Node ": " Instr
  syntax Maplets ::= List{Maplet,","}  

  syntax Graph ::= "[|Nodes:" MyList "Edges:" MyList "Start:" Node "Label:" MyMap"|]"
  syntax GraphRec ::= Int": (|Nodes:" Nodes "Edges:" Edges "Start:" Node "Label:" Maplets"|)"
  syntax TCFG ::= List{GraphRec, "||"}

  syntax Test ::= Trans "on" TCFG

endmodule

module CTL-CHECK
  imports TRANS2-SYNTAX
  imports SMT

  syntax K ::= makeStmts(MyMap, MyList, Int, Instr) [function]
    | makeNodes(MyMap, MyList, Int, NodeLit) [function]
    | makeMatch(Instr, Instr) [function]
    | satis0(MyMap, SideCond) [function]
 
  syntax BoolPlus ::= cond(K) [strict] | "andK" "(" K  "," K ")" [strict] | "orK" "(" K "," K ")" [strict] 
	| "notK" "(" K ")" [strict] | "EXK" "(" K "," K ")" [strict(2)]


//  rule <k> ((K:K andK true) => K) ...</k>
  
  /* processing atomic predicates via matching */
/*  rule <k> makeNodes(M:MyMap, (MyListItem(I), S:MyList), T, Start T2) => 
    orK(andK(andK(T ==K I, T2 ==K I),M[I] ==K N),makeNodes(M, S, T, Start T2)) ...</k>
    <name> I </name> <start> N:Node </start>*/
/*  rule makeNodes(M, (MyListItem(I), S:MyList), T, Exit T2) => 
    orK(T ==K I andK T2 ==K I andK M[I] ==K Exit, makeNodes(M, S, T, Exit T2))*/

  rule makeNodes(M:MyMap, (MyListItem(I:Int), S:MyList), T:Int, N:NodeLit) => 
    orK(andK(T ==K I, M[I] ==K N), makeNodes(M, S, T, N))
  rule makeNodes(_, .MyList, _, _) => true

  rule makeMatch(skip, skip) => true
  rule makeMatch(X := Y, Z := W) => andK(X ==K Z, Y ==K W)
  rule makeMatch(_ := _, skip) => false
  rule makeMatch(skip, _ := _) => false
  
  rule <k> makeStmts(M, (MyListItem(I), S:MyList), T, P) => orK(andK(T ==K I , makeMatch(P, Ms[M[I]])) , makeStmts(M, S, T, P)) ...</k> 
       <name> I </name> <label> Ms </label>
  rule makeStmts(_, .MyList, _, _) => true

  rule <k> satis(M, node T NL) => makeNodes(M, Ts, T, NL) ...</k> <threads> Ts </threads>
  rule <k> satis(M, stmt T (P)) => makeStmts(M, Ts, T, P) ...</k> <threads> Ts </threads>

  /* next nodes from a node */
  syntax MyList ::= next(Int, Node, MyList) [function] 
               | prev(Int, Node, MyList) [function]
               | addon(MyMap, MyList) [function] | cross(MyList) [strict]
  syntax MyList ::= nexts(MyList, MyMap, MyList) | prevs(MyList, MyMap, MyList)

  rule next(_, _, .MyList) => .MyList
  rule next(T, N:Node, (MyListItem(e(N, N2, _)), Es:MyList)) => MyListItem(T |-> N2), next(T, N, Es)

  rule nexts(.MyList, _, L) => L
  rule <k> nexts((MyListItem(T), Ts:MyList), M, L) => 
           nexts(Ts, M, (L, MyListItem(MyListItem(T |-> M[T]), next(T, M[T], Es)))) ...</k> <name> T </name> <edges> Es </edges>

  rule prev(_, _, .MyList) => .MyList
  rule prev(T, N:Node, (MyListItem(e(N2, N, _)), Es:MyList)) => MyListItem(T |-> N2), prev(T, N, Es)

  rule prevs(.MyList, _, L) => L
  rule <k> prevs((MyListItem(T), Ts:MyList), M, L) => prevs(Ts, M, (L, MyListItem(MyListItem(T |-> M[T]), prev(T, M[T], Es)))) ...</k> <name> T </name> <edges> Es </edges>

  rule addon(M, .MyList) => .MyList
  rule addon(M, (MyListItem(M2), S:MyList)) => MyListItem(update(M2, M)), addon(M, S)

  rule cross(.MyList) => .MyList
  rule cross(MyListItem(.MyList), L:MyList) => .MyList
  rule cross(MyListItem(MyListItem(M), S:MyList), L:MyList) => 
       ((addon(M, cross(L))), (cross(MyListItem(S), L)))

  /* finding enabled paths */
  syntax K ::= "backPaths" "("SideCond","SideCond","Int","MyMap")" [function]
                | "orBackPaths" "("SideCond","SideCond","Int","MyList")" [function]
                | "forPaths" "("SideCond","Int","MyMap")" [function]
                | "orForPaths" "("SideCond","Int","MyList")" [function]
                | "forRPaths" "("SideCond","SideCond","Int","MyMap")" [function]
                | "orForRPaths" "("SideCond","SideCond","Int","MyList")" [function]
		| satis(MyMap, SideCond) [function] /* memo? */ 

  rule backPaths(P0, _, 0, M) => satis(M, P0)
  rule <k> backPaths(P0, P, N:Int, M) => orK(backPaths(P0, P, N -Int 1, M) ,
           andK(satis(M, P) , orBackPaths(P0, P, N -Int 1, cross(nexts(Ts, M, .MyList))))) ...</k> 
       <threads> Ts </threads> when N >Int 0
  rule orBackPaths(_, _, _, .MyList) => true
  rule orBackPaths(P0, P, N, (MyListItem(M), R:MyList)) => orK(backPaths(P0, P, N, M),orBackPaths(P0, P, N, R))

  rule forPaths(_, 0, _) => true
  rule <k> forPaths(P, N, M) => orForPaths(P, N -Int 1, cross(nexts(Ts, M, .MyList))) ...</k> 
       <threads> Ts </threads> when N >Int 0
  rule orForPaths(_, _, .MyList) => true
  rule orForPaths(P, N, (MyListItem(M), R:MyList)) => orK(andK(satis(M, P), forPaths(P, N, M)),orForPaths(P, N, R))

  rule forRPaths(P0, _, 0, M) => satis(M, P0)
  rule <k> forRPaths(P0, P, N, M) => orK(forRPaths(P0, P, N -Int 1, M) ,andK(satis(M, P) , orForRPaths(P0, P, N -Int 1, cross(prevs(Ts, M, .MyList))))) ...</k> 
       <threads> Ts </threads> when N >Int 0
  rule orForRPaths(_, _, _, .MyList) => true
  rule orForRPaths(P0, P, N, (MyListItem(M), R:MyList)) => orK(forRPaths(P0, P, N, M), orForRPaths(P0, P, N, R))

  /* start points */
  syntax SideCond ::= allStart(MyList) [function]

  rule allStart(.MyList) => True
  rule allStart(MyListItem(T), S:MyList) => node T Start T and allStart(S)

  /* processing side conditions */
  rule satis(_, True) => true
  rule satis(M, not P) => notK (satis(M, P))
  rule satis(M, P1 and P2) => andK(satis(M, P1), satis(M, P2))
  rule satis(M, EX X. P) => EXK (X , satis(M, P))
  rule <k> satis(M, EX P1 U P2) => backPaths(P2, P1, N, M) ...</k> <size> N </size>
  rule <k> satis(M, ALL P1 U P2) => notK(forPaths(P1 and not P2, N +Int 1, M)) ...</k>
       <size> N </size>
  rule <k> satis(M, EX P1 BACKTO P2) => forRPaths(P2, P1, N, M) ...</k>
       <size> N:Int </size>
  rule <k> satis(M, ALL P1 BACKTO P2) => notK (forRPaths(allStart(Ts), P1 and not P2, N, M)) ...</k> 
       <threads> Ts </threads> <size> N:Int </size>

  rule satis0(M, P) => cond(satis(M, P))

/* language provides patterns/matching? */
endmodule  

module TRANS2
  imports CTL-CHECK

  syntax KResult ::= Graph | Bool

/* Note: stdin seems to be broken on user-defined types. */

  configuration <T color="yellow">
                  <trans color="green"> .K </trans>
		  <graphs>
                    <graph color="red" multiplicity="*"> 
                      <name> .K </name>
                      <nodes> .MyList </nodes>
                      <edges> .MyList </edges>
                      <start> .K </start>
                      <label> .MyMap </label>
                    </graph>
                  </graphs>
                  <threads> .MyList </threads>
                  <size> 0 </size>
                  <subst color="grey"> .MyMap </subst>
                  <k> $PGM:Test </k>
/*                  <in color="magenta" stream="stdin"> .List </in>
                  <out color="Orchid" stream="stdout"> .List </in>*/
                </T>

/* Don't pattern match on maps, if possible. Use lookup instead, in side conditions if necessary. */

  rule andK(B1:Bool,B2:Bool) => B1 andBool B2
  rule orK(B1:Bool,B2:Bool) => B1 orBool B2
  rule notK (B1:Bool) => notBool B1
  rule EXK (K , B1:Bool) => [E]K K . B1

  rule (EF (P:SideCond)) => EX True U P  [macro]

  syntax MyList ::= "nodes-to-set" Nodes [function] | "edges-to-set" Edges [function]

  rule nodes-to-set .Nodes => .MyList
  rule nodes-to-set(N:Node, Ns:Nodes) => MyListItem(N), nodes-to-set(Ns)
  
  rule edges-to-set .Edges => .MyList
  rule edges-to-set (E:Edge, Es:Edges) => MyListItem(E), edges-to-set Es

  syntax MyMap ::= "maplets-to-map" Maplets [function]
  rule maplets-to-map .Maplets => .MyMap
  rule maplets-to-map ((I : P:Instr), Ms:Maplets) => (maplets-to-map Ms)[I <- P]

  /* Why do I need to do this? */
  rule
    size(/* L1:MyList */ MyListItem(_), L2:MyList)
  =>
    1 +Int /* size(L1) +Int */ size(L2)
  rule size(.MyList) => 0

  rule <k> _ on (I: (|Nodes: Ns Edges: Es Start: S Label: Ms:Maplets|) || R:TCFG => R) </k>
       <graphs> B => B:Bag <graph> <name> I </name> <nodes> nodes-to-set Ns </nodes> <edges> edges-to-set Es </edges> 
                     <start> S </start> <label> maplets-to-map Ms </label> </graph> </graphs>
       <threads> _ => MyListItem(I) </threads>
       <size> 0 => size(nodes-to-set Ns) </size>
  rule <k> _ on (I: (|Nodes: Ns Edges: Es Start: S Label: Ms:Maplets|) || R:TCFG => R) </k>
       <graphs> B => B:Bag <graph> <name> I </name> <nodes> nodes-to-set Ns </nodes> <edges> edges-to-set Es </edges> 
                     <start> S </start> <label> maplets-to-map Ms </label> </graph> </graphs>
       <threads> L => L, MyListItem(I) </threads>
       <size> N:Int => N *Int size(nodes-to-set Ns) </size> when N =/=Int 0
  rule <k> T:Trans on .TCFG => T </k> <trans> _ => T </trans>

/* helper functions */

/*Why doesn't this work?  syntax K ::= "freshList" Int

  rule freshList 0 => .
  rule <k> (freshList N ~> vars(.List{K})) => (freshList (N -Int 1) ~> vars(I)) ...</k> when (fresh(I:Id)) andBool (N >Int 0)
  rule <k> (freshList N ~> vars(L)) => (freshList (N -Int 1) ~> vars(L,, I)) ...</k> when (fresh(I:Id)) andBool (N >Int 0)*/

  syntax MyList ::= remapSucc(MyList, Node, Node) [function]

  syntax Node ::= source(Edge) [function]
  syntax Edge ::= updateSource(Edge, Node) [function]

  rule source(e(N:Node, _, T)) => N
  rule updateSource(e(_, M, T), N') => e(N', M, T)

  rule remapSucc(.MyList, _, _) => .MyList
  rule remapSucc((MyListItem(I), S:MyList), N1, N2) => MyListItem(updateSource(I, N2)), remapSucc(S, N1, N2) when source(I) ==K N1
  rule remapSucc((MyListItem(I), S:MyList), N1, N2) => MyListItem(I), remapSucc(S, N1, N2) when source(I) =/=K N1

  syntax MyList ::= "removeAll" K MyList [function]
  rule removeAll _ .MyList => .MyList
  rule removeAll K (MyListItem(K), L:MyList) => removeAll K L
  rule removeAll K (MyListItem(J), L:MyList) => MyListItem(J), (removeAll K L) when J =/=K K
/* action semantics */

  /* substitution */
  syntax K ::= MyMap"("K")"

  rule S(K) => S[K] when K in keys(S)
  rule S:MyMap(N:Node) => N when notBool (N in keys(S))
  rule S:MyMap(T:Type) => T when notBool (T in keys(S))
  rule S(X := Y) => S[X] := S[Y]
  rule S:MyMap(skip) => skip
  rule <k> S(Start T) => N ...</k> <name> I </name> <start> N:Node </start> when S[T] ==K I

  rule <k> add-edge(N1:NodeLit, N2:NodeLit, T:Type) => . ...</k> <subst> S </subst>
       <edges> .MyList => MyListItem(e(S(N1), S(N2), S(T))) ...</edges>
  rule <k> remove-edge(N1:NodeLit, N2:NodeLit, T:Type) => . ...</k> <subst> S </subst>
       <edges> Es => removeAll e(S(N1), S(N2), S(T)) Es </edges>
  rule <k> split-edge(N1:NodeLit, N2:NodeLit, T:Type, P:Instr) => . ...</k> <subst> S:MyMap </subst>
       <nodes> .MyList => MyListItem(I) ...</nodes> 
       <edges> Es => (removeAll e(S(N1), S(N2), S(T)) Es), MyListItem(e(S(N1), I, S(T))), MyListItem(e(I, S(N2), seq)) </edges>
       <label>... .MyMap => I |-> (S(P)) </label> when (fresh(I:Int)) andBool e(S(N1), S(N2), S(T)) in Es
  rule <k> replace N:NodeLit with P:Instr => . ...</k> <label> Ms => Ms[S(N) <- S(P)] </label> <subst> S </subst>
  rule <k> replace N:NodeLit with P:Instr, P1:Instr, Ps:Instrs => replace I with P1, Ps ...</k> <subst> S </subst>
       <nodes> .MyList => MyListItem(I) ...</nodes> <edges> Es => remapSucc(Es, S(N), I), MyListItem(e(S(N), I, seq)) </edges> 
       <label> Ms => Ms[S(N) <- S(P)] </label> when (fresh(I:Int))
/* need remove case */

  syntax MyMap ::= "initMap" MyList [function]
  rule initMap .MyList => .MyMap
  rule <k> initMap (MyListItem(I)) => I |-> N ...</k>
       <name> I </name> <start> N:Node </start>
  rule <k> initMap (MyListItem(I), S:MyList) => (initMap S)[I <- N] ...</k>
       <name> I </name> <start> N:Node </start>

/* transformation semantics */
  syntax Trans ::= "fail"

  syntax Bool ::= makeCond(MyMap) [function]

  /* dud */ rule makeCond(M) => true

  rule <k> As:Actions if P:SideCond => makeCond(S) andThenBool satis(initMap Ts, P) ~> As ...</k> 
       <threads> Ts </threads> <subst> S </subst>
  rule <k> B:Bool => . ...</k> <subst> S => update(S, getModel(B)) </subst>
  rule <k> A:Action; As => A ~> As ...</k>
  rule <k> .Actions => . ...</k>

/*  rule <k> MATCH P IN T => fail ...</k> <threads> Ts </threads> <subst> S </subst>
    when isSat(satis(initMap Ts, P) andBool makeCond(S)) ==Bool false*/
  rule <k> MATCH P IN T => andK(satis(initMap Ts, P),makeCond(S)) ~> T ...</k> <threads> Ts </threads> 
       <subst> S </subst>
  rule <k> T1 THEN T2 => T1 ~> T2 ...</k>
  rule <k> T1 [] T2 => T1 ...</k>
  rule <k> T1 [] T2 => T2 ...</k>
  rule <k> APPLY-ALL T => T ~> APPLY-ALL T ...</k>
/* This probably needs work. */
  rule <k> (fail ~> T1:Trans ~> APPLY-ALL T2) => . ...</k>
  rule <k> (fail ~> A:Actions ~> APPLY-ALL T) => . ...</k>
  

/*  GRAPH="Nodes: [N:Id] Edges: .MyList Label: N |-> Y:Id := F:Id */

//  syntax MyList ::= "nodes-to-set" Nodes
//  rule (nodes-to-set (N:Id)) => (MyListItem(N))
//  rule nodes-to-set Ns:Nodes,Ns':Nodes => (nodes-to-set Ns) (nodes-to-set Ns')

/*  rule <k> nodes => . ...</k> <out>... . => ListItem("Input nodes: ") </out>
  rule <k> edges ...</k> <in> ListItem(Ns:Nodes) => . ...</in> 
       <graph> . => (|Nodes: (nodes-to-set Ns) Edges: edges-to-set Es Label: .Map|) </graph>*/

/* What did Kalvala et al. do in their implementation? */
/* Focus on trying to produce one satisfying valuation? */

endmodule