Merge pull request #4 from kframework/rule-translation

Rule translation

Jenkinsfile

@@ -4,6 +4,9 @@ pipeline {
       additionalBuildArgs '--build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)'
     }
   }
+  options {
+    ansiColor('xterm')
+  }
   stages {
     stage("Init title") {
       when { changeRequest() }
@@ -17,37 +20,16 @@ pipeline {
       steps {
         ansiColor('xterm') {
           sh '''#!/bin/bash
-            (cd ext/k-light/ && mvn package -DskipTests) && ./build kink
-          '''
-        }
-      }
-    }
-    stage('t/foobar') {
-      steps {
-        ansiColor('xterm') {
-          sh '''#!/bin/bash
-            ./build t/foobar
-          '''
-        }
-      }
-    }
-    stage('t/peano') {
-      steps {
-        ansiColor('xterm') {
-          sh '''#!/bin/bash
-            ./build t/foobar
-          '''
-        }
-      }
-    }
-    stage('t/*') {
-      steps {
-        ansiColor('xterm') {
-          sh '''#!/bin/bash
-            ./build
+            (cd ext/k-light/ && mvn package -DskipTests) && ./build kink .build/kbackend-haskell
           '''
         }
       }
     }
+    stage('t/foobar') { steps {  sh '''./build t/foobar''' } }
+    stage('t/peano')  { steps {  sh '''./build t/peano'''  } }
+    stage('t/imp')    { steps {  sh '''./build t/imp'''    } }
+
+    // Catch-all for anything left out
+    stage('t/*')      { steps {  sh '''./build'''          } }
   }
 }

README.md

@@ -16,12 +16,12 @@ Running
 
 First, build K-in-K with `./build kink`. Then: 
 
-* to kompile an ekore definition, use `./kink kompile -- foo.ekore`
-* to parse a program, use `./kink kast program.foo -- foo.k`
+* to kompile an ekore definition, use `./bin/kink kompile -- foo.ekore`
+* to parse a program, use `./bin/kink kast program.foo -- foo.k`
 
 Note that the `foo.k/ekore` files are arguments to KRun, whereas `kompile` and
 `kast program.foo` are arguments to the K-in-K definition. See
-[src/command-line.md](src/command-line.md) and [./kink](./kink) for details.
+[src/command-line.md](src/command-line.md) and [./bin/kink](./bin/kink) for details.
 
 Testing
 =======

build

@@ -19,12 +19,12 @@ proj = KProject()
 
 kore_from_config = proj.rule( 'kore-from-config'
                             , description = 'kore-from-config: $in'
-                            , command = 'lib/kore-from-config "$in" "$out"'
+                            , command = 'lib/kore-from-config "$in" "$out" || (cat "$in" ; false)'
                             , ext = 'kore'
                             )
 k_from_config = proj.rule( 'k-from-config'
                          , description = 'k-from-config'
-                         , command = 'lib/k-from-config "$in" "$out"'
+                         , command = 'lib/k-from-config "$in" "$out" || (cat "$in" ; false)'
                          , ext = 'kore'
                          )
 def kore_exec(kore, ext = 'kore-exec'):
@@ -64,7 +64,7 @@ kink = proj.definition( backend   = 'ocaml'
                       )
 
 def pipeline(commandline, extension):
-    return kink.krun().variables(
+    return kink.krun().ext(extension).variables(
                 flags = "-cCOMMANDLINE='%s' -cKINKDEPLOYEDDIR=%s"
                       % (commandline, kink.directory()))
 
@@ -127,4 +127,12 @@ peano_tests += [ lang_test('t/peano', 'PEANO', 'two-plus-two.peano') ]
 peano_tests += [ parse_test('t/peano', 'peano.k', 'two-plus-two.peano') ]
 proj.build('t/peano', 'phony', inputs = Target.to_paths(peano_tests))
 
+# Imp
+imp_tests = []
+imp_tests += [ ekore_test('t/imp-simple', 'imp-simple.ekore') ]
+imp_tests += [ ekore_test('t/imp-simple', 'expected.ekore') ]
+imp_tests += [ lang_test('t/imp-simple', 'IMP-SIMPLE', 'conjunction.imp') ]
+imp_tests += [ parse_test('t/imp-simple', 'imp-simple.k', 'conjunction.imp') ]
+proj.build('t/imp', 'phony', inputs = Target.to_paths(imp_tests))
+
 proj.main()

src/command-line.md

@@ -23,6 +23,7 @@ module COMMAND-LINE
   imports FRONTEND-MODULES-TO-KORE-MODULES
   imports FLATTEN-PRODUCTIONS
   imports OUTER-ABSTRACT
+  imports NON-FUNCTIONAL-PRODUCTIONS-TO-CONSTRUCTORS
   imports PRODUCTIONS-TO-SORT-DECLARATIONS
   imports PRODUCTIONS-TO-SYMBOL-DECLARATIONS
   imports TRANSLATE-FUNCTION-RULES
@@ -81,9 +82,10 @@ High-level pipeline steps
     => #parseToEKore
     ~> #defnToConfig
     ~> #flattenProductions
+    ~> #nonFunctionProductionsToConstructors
     ~> #productionsToSortDeclarations
     ~> #productionsToSymbolDeclarations
-    ~> #translateFunctionRules
+    ~> #translateRules
 ```
 
 ```k

src/ekore.md

@@ -120,9 +120,7 @@ module K-PRODUCTION-COMMON
   syntax KSortList ::= KSortList "," KSort [klabel(kSortList)]
                      | KSort
   syntax KProductionWAttr ::= KProduction OptionalAttributes [klabel(kProductionWAttr)]
-                            | Tag "(" KSortList ")" OptionalAttributes [klabel(kFuncProductionWAttr)]
-                            |     "(" KSortList ")" OptionalAttributes [klabel(kTupleProductionWAttr)]
-  syntax KPrioritySeq ::= KPrioritySeq ">" KNeTagSet   [klabel(kPrioritySeq)]
+  syntax KPrioritySeq ::= KPrioritySeq ">" KNeTagSet         [klabel(kPrioritySeq)]
                         | KNeTagSet
   syntax ProdBlock ::= ProdBlock "|" KProductionWAttr [klabel(prodBlock), format(%1%n%2 %3)]
                      | KProductionWAttr
@@ -132,6 +130,8 @@ module K-PRODUCTION-COMMON
   syntax KProductionItem
   syntax KProduction ::= KProductionItem
                        | KProductionItem KProduction [klabel(kProduction), unit(emptyKProduction)]
+                       | Tag "(" KSortList ")"       [klabel(kFuncProduction)]
+                       |     "(" KSortList ")"       [klabel(kTupleProduction)]
 
   syntax SyntaxDeclaration
     ::= "syntax" KSort OptionalAttributes [klabel(kSyntaxSort)]
@@ -237,7 +237,7 @@ module ATTRIBUTES-COMMON
   syntax KAttributesDeclaration ::= "[" AttrList "]" [klabel(kAttributesDeclaration)]
   syntax OptionalAttributes ::= KAttributesDeclaration
 
-  syntax TagContent ::= UpperName | LowerName | Numbers
+  syntax TagContent ::= UpperName | LowerName | Numbers | EKoreKString
   syntax TagContents
   syntax KEY ::= LowerName
 
@@ -247,7 +247,6 @@ module ATTRIBUTES-ABSTRACT
   imports ATTRIBUTES-COMMON
   syntax Attr ::= tagSimple(KEY)           [klabel(tagSimple), format(%3)]
                 | KEY "(" TagContents ")"  [klabel(tagContent)]
-                | KEY "(" EKoreKString ")" [klabel(tagString)]
   syntax AttrList ::= Attr "," AttrList    [klabel(consAttrList), format(%1 %2 %3)]
                     | ".AttrList"          [klabel(dotAttrList)]
 
@@ -263,7 +262,6 @@ module ATTRIBUTES-SYNTAX
 
   syntax Attr ::= KEY                     [klabel(tagSimple)]
                 | KEY "(" TagContents ")" [klabel(tagContent)]
-                | KEY "(" EKoreKString ")"     [klabel(tagString)]
   syntax EmptyAttrList ::= ""             [klabel(dotAttrList )]
   syntax NeAttrList    ::=  Attr "," NeAttrList [klabel(consAttrList)]
                          | Attr EmptyAttrList  [klabel(consAttrList)]

src/kink.md

@@ -145,7 +145,22 @@ module META-ACCESSORS
        <decl> symbol SNAME { .Sorts } ( _ ) : SORT [ ATTRS ]
        </decl>
        [owise]
-  syntax LowerName ::= "function" [token]
+```
+
+```k
+  syntax Bool ::= #keyInAttributes(KEY, AttrList) [function]
+  rule #keyInAttributes(_, .AttrList) => false
+  rule #keyInAttributes(KEY, (tagSimple(KEY), _)) => true
+  rule #keyInAttributes(KEY, (tagContent(KEY, _), _)) => true
+  rule #keyInAttributes(KEY, (_ , REST))
+    => #keyInAttributes(KEY, REST) [owise]
+
+  syntax TagContents ::= #getAttributeContent(KEY, AttrList) [function]
+//  rule #getAttributeContent(_, .AttrList) => undefined
+//  rule #getAttributeContent(KEY, (tagSimple(KEY)    , _)) => undefined
+  rule #getAttributeContent(KEY, (tagContent(KEY, CONTENT), _)) => CONTENT
+  rule #getAttributeContent(KEY, (_ , REST))
+    => #getAttributeContent(KEY, REST) [owise]
 ```
 
 ```k
@@ -194,9 +209,9 @@ module PARSE-PROGRAM
        <grammar> GRAMMAR </grammar>
 
   rule <k> #collectGrammar ... </k>
-       <decl> kSyntaxProduction(SORT, PROD) </decl>
-       <grammar> (.Set => SetItem(kSyntaxProduction(SORT, PROD))) REST </grammar>
-    requires notBool(kSyntaxProduction(SORT, PROD) in REST)
+       <decl> kSyntaxProduction(SORT, PROD) #as SYNTAXDECL </decl>
+       <grammar> ( .Set => SetItem(SYNTAXDECL) ) REST </grammar>
+    requires notBool(SYNTAXDECL in REST)
   rule <k> #collectGrammar => .K ... </k>
        <s> #STUCK() => .K ... </s>
 endmodule
@@ -407,6 +422,36 @@ endmodule
 Once this module is defined, we import it into the main `KINK` module and
 add it to the pipeline.
 
+Make non function productions constructors
+------------------------------------------
+
+If productions are not marked as functions, we consider them constructors.
+
+```k
+module NON-FUNCTIONAL-PRODUCTIONS-TO-CONSTRUCTORS
+  imports META-ACCESSORS
+  syntax KItem ::= "#nonFunctionProductionsToConstructors"
+  rule <k> #nonFunctionProductionsToConstructors ... </k>
+       <name> MNAME </name>
+       <declarations>
+         <decl> kSyntaxProduction(SORT, kProductionWAttr(PROD, [ ATTRS
+                                                              => (tagSimple(functional)
+                                                                 , tagSimple(constructor)
+                                                                 , tagSimple(injective)
+                                                                 , ATTRS
+                                                                 )
+                                                               ]
+                                                        ))
+         </decl>
+         ...
+       </declarations>
+    requires notBool #keyInAttributes(constructor, ATTRS)
+     andBool notBool #keyInAttributes(function, ATTRS)
+  rule <k> #nonFunctionProductionsToConstructors => .K ... </k>
+       <s> #STUCK() => .K ... </s>
+endmodule
+```
+
 Extract symbols from productions
 --------------------------------
 
@@ -422,7 +467,7 @@ module PRODUCTIONS-TO-SYMBOL-DECLARATIONS
   imports ID
   imports PARSER-UTIL
 
-  syntax MapTransform ::= "#productionsToSymbolDeclarations"
+  syntax KItem ::= "#productionsToSymbolDeclarations"
   rule <k>  #productionsToSymbolDeclarations ... </k>
        <name> MNAME </name>
        <declarations>
@@ -436,25 +481,16 @@ module PRODUCTIONS-TO-SYMBOL-DECLARATIONS
          ...
        </declarations>
     requires notBool #isSymbolDeclared(MNAME, #symbolNameFromAttrList(ATTRS))
-  rule <k>  #productionsToSymbolDeclarations => .K ... </k>
+  rule <k> #productionsToSymbolDeclarations => .K ... </k>
        <s> #STUCK() => .K ... </s>
 ```
 
 `#symbolNameFromAttrList` extracts the Name to be used for a symbol from the
 
 ```k
-  syntax LowerName ::= "klabel" [token]
   syntax SymbolName ::= #symbolNameFromAttrList(AttrList) [function]
-  rule #symbolNameFromAttrList
-           ( consAttrList
-                 ( tagContent(klabel, SNAME:TagContents)
-                 , ATTRS
-                 )
-           )
-    // TODO: We need to handle errors
-    => {parseSymbolName(tokenToString(SNAME))}:>SymbolName
-  rule #symbolNameFromAttrList(consAttrList(_, ATTRS))
-    => #symbolNameFromAttrList(ATTRS) [owise]
+  rule #symbolNameFromAttrList(ATTRS)
+    => {parseSymbolName(tokenToString(#getAttributeContent(klabel, ATTRS)))}:>SymbolName
 
   syntax Patterns ::= #removeKlabelAttr(AttrList) [function]
   rule #removeKlabelAttr(consAttrList(tagContent(klabel, _), ATTRS))
@@ -468,13 +504,10 @@ module PRODUCTIONS-TO-SYMBOL-DECLARATIONS
 
 ```k
   syntax Pattern ::= #attr2Pattern(Attr) [function]
-
   rule #attr2Pattern(tagSimple(KEY:LowerName))
     => KEY { .Sorts } ( .Patterns )
 
   syntax Patterns ::= #attrList2Patterns(AttrList) [function]
-
-  // TODO: This reverses the pattern list
   rule #attrList2Patterns(ATTR, ATTRS) => #attr2Pattern(ATTR), #attrList2Patterns(ATTRS)
   rule #attrList2Patterns(.AttrList) => .Patterns
 ```
@@ -501,27 +534,41 @@ endmodule
 Translate Function Rules
 ------------------------
 
-`#translateFunctionRules` generates new kore axioms for rewrite rules over
-function symbols. Rules whose LHS is not a kore symbol with the function
-attribute should be ignored. Since the rewrite rule carries no additional
-information over the kore axiom, it can be discarded.
+`#translateRules` generates new kore axioms for rules. When the left-hand-side
+of the rule is a function symbol, we generate an axiom that uses equalities.
+Otherwise, if it has a constructor attribute, we generate one with rewrites. We
+do not handle `requires` and `ensures` clauses yet.
 
 ```k
 module TRANSLATE-FUNCTION-RULES
   imports KINK-CONFIGURATION
   imports META-ACCESSORS
 
-  syntax KItem ::= "#translateFunctionRules"
-  rule <k> #translateFunctionRules ... </k>
+  syntax KItem ::= "#translateRules"
+  rule <k> #translateRules ... </k>
        <name> MNAME </name>
-       <decl> kRule(noAttrs(krewrite( SYMBOL { .Sorts } ( ARG_PATTERNS ) , RHS)))
+       <decl> kRule(noAttrs(krewrite( SYMBOL { .Sorts } ( ARG_PATTERNS ) #as LHS, RHS)))
            => axiom { #token("R", "UpperName") , .Sorts }
                 \equals { #getReturnSort(MNAME, SYMBOL), #token("R", "UpperName") }
-                ( SYMBOL { .Sorts } ( ARG_PATTERNS ) , RHS )
+                ( LHS , RHS )
          [ .Patterns ]
        </decl>
     requires #isFunctionSymbol(MNAME, SYMBOL)
-  rule <k> #translateFunctionRules => .K ... </k>
+
+  rule <k> #translateRules ... </k>
+       <name> MNAME </name>
+       <decl> kRule(noAttrs(krewrite( SYMBOL { .Sorts } ( ARG_PATTERNS ) #as LHS , RHS)))
+           => #fun( RETSORT
+                 => axiom { .Sorts } \rewrites { RETSORT }
+                        ( \and { RETSORT } (\top{ RETSORT }(), LHS)
+                        , \and { RETSORT } (\top{ RETSORT }(), RHS)
+                        )
+                    [ .Patterns ]
+                  ) (#getReturnSort(MNAME, SYMBOL))
+       </decl>
+    requires notBool #isFunctionSymbol(MNAME, SYMBOL)
+
+  rule <k> #translateRules => .K ... </k>
        <s> #STUCK() => .K ... </s>
 endmodule
 ```