cleanup

kframework · Feb 5, 2020 · a514a4b · a514a4b
1 parent 0e1fb00
commit a514a4b
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 27 deletions.
diff --git a/prover/drivers/coq-driver.md b/prover/drivers/coq-driver.md
@@ -28,36 +28,32 @@ module DRIVER-COQ
   imports PROVER-CORE-SYNTAX
   imports STRATEGIES-EXPORTED-SYNTAX
 
+// Add sort "Term" to declarations
   rule <k> CS:CoqSentence CSs:CoqSentences => CS ~> CSs ... </k>
        <declarations> ( .Bag
                      => <declaration> sort StringToSort("Term") </declaration>
                       ) ...
        </declarations>
 
-  rule <k> Definition ID BINDERs : TYPE := TERM .
-        => .K
-           ...
-       </k>
-       <declarations> ( .Bag
-                     => <declaration> symbol CoqIdentToSymbol(ID)(CoqBindersToSorts(BINDERs)) : CoqTermToSort(ID) </declaration>
-                      ) ...
-       </declarations>
-
+// Add symbol (of sort Term) and equality axiom corresponding to each definition
+  rule Definition ID BINDERs : TYPE := TERM . => Definition ID := TERM .
   rule <k> Definition ID := TERM .
         => .K
            ...
        </k>
        <declarations> ( .Bag
-                     => <declaration> axiom \equals(CoqIdentToSymbol(ID), CoqTermToPattern(TERM)) </declaration>
+                     => <declaration> symbol CoqIdentToSymbol(ID)(.Sorts) : StringToSort("Term") </declaration>
+                        <declaration> axiom \equals(CoqIdentToSymbol(ID), CoqTermToPattern(TERM)) </declaration>
                       ) ...
        </declarations>       
 
+// Translate inductive cases
   rule <k> Inductive ID BINDERs : TERM := .CoqIndCases .
         => .K
            ...
        </k>
        <declarations> ( .Bag
-                     => <declaration> symbol CoqIdentToSymbol(ID)(CoqBindersToSorts(BINDERs)) : CoqTermToSort(ID) </declaration>
+                     => <declaration> symbol CoqIdentToSymbol(ID)(.Sorts) : StringToSort("Term") </declaration>
                       ) ...
        </declarations>
 
@@ -66,20 +62,12 @@ module DRIVER-COQ
            ...
        </k>
        <declarations> ( .Bag
-                     => <declaration> symbol CoqIdentToSymbol(IDC)(CoqBindersToSorts(BINDERCs)) : CoqTermToSort(ID) </declaration>
+                     => <declaration> symbol CoqIdentToSymbol(IDC)(.Sorts) : StringToSort("Term") </declaration>
                         <declaration> axiom \type(CoqIdentToSymbol(IDC)(.Patterns), CoqTermToPattern(TERMC))  </declaration>
                       ) ...
        </declarations>
 
-  syntax Sorts ::= CoqBindersToSorts(CoqBinders) [function]
-  rule CoqBindersToSorts(.CoqBinders) => .Sorts
-  rule CoqBindersToSorts(NAME:CoqName BINDERs) => StringToSort("Term"), CoqBindersToSorts(BINDERs)
-  rule CoqBindersToSorts((NAMES : TYPE) BINDERs) => CoqNamesToSorts(NAMES) ++Sorts CoqBindersToSorts(BINDERs)
-
-  syntax Sorts ::= CoqNamesToSorts(CoqNames) [function]
-  rule CoqNamesToSorts(.CoqNames) => .Sorts
-  rule CoqNamesToSorts(NAME:CoqName NAMEs) => StringToSort("Term"), CoqNamesToSorts(NAMEs)
-
+// Converting Term to Pattern
   syntax Pattern ::= CoqTermToPattern(CoqTerm) [function]
   rule CoqTermToPattern(UN:UpperName) => CoqIdentToSymbol(UN)
   rule CoqTermToPattern(LN:LowerName) => CoqIdentToSymbol(LN)
@@ -127,7 +115,7 @@ module DRIVER-COQ
   rule CoqPatternToPatterns(ID:CoqQualID) => CoqIdentToSymbol(ID), .Patterns
   rule CoqPatternToPatterns(ID:CoqQualID P:CoqPattern) => CoqIdentToSymbol(ID) ++Patterns CoqPatternToPatterns(P)
 
-  // Get binders from MultPattern
+// Get binders from MultPattern
   syntax Patterns ::= CoqMultPatternToBinders(CoqMultPattern) [function]
   syntax Patterns ::= CoqPatternToBinders(CoqMultPattern) [function]
   rule CoqMultPatternToBinders(ID:CoqQualID) => .Patterns

diff --git a/prover/lang/coq-lang.md b/prover/lang/coq-lang.md
@@ -27,11 +27,7 @@ module COQ
 // Seralize to String:
   syntax String ::= CoqNameToString(CoqName) [function, functional, hook(STRING.token2string)]
 
-// Converting between Sorts:
-  syntax Sort ::= CoqTermToSort(CoqTerm) [function]
-  rule CoqTermToSort(SORT:UpperName) => StringToSort("Term")
-  rule CoqTermToSort(SORT:LowerName) => StringToSort("Term")
-
+// Sort conversions
   syntax Symbol ::= CoqIdentToSymbol(CoqIdent) [function]
   rule CoqIdentToSymbol(IDENT:UpperName) => IDENT
   rule CoqIdentToSymbol(IDENT:LowerName) => IDENT
@@ -42,6 +38,15 @@ module COQ
   syntax VariableName ::= CoqNameToVariableName(CoqName) [function]
   rule CoqNameToVariableName(NAME) => StringToVariableName(CoqNameToString(NAME))
 
+  syntax Sorts ::= CoqBindersToSorts(CoqBinders) [function]
+  rule CoqBindersToSorts(.CoqBinders) => .Sorts
+  rule CoqBindersToSorts(NAME:CoqName BINDERs) => StringToSort("Term"), CoqBindersToSorts(BINDERs)
+  rule CoqBindersToSorts((NAMES : TYPE) BINDERs) => CoqNamesToSorts(NAMES) ++Sorts CoqBindersToSorts(BINDERs)
+
+  syntax Sorts ::= CoqNamesToSorts(CoqNames) [function]
+  rule CoqNamesToSorts(.CoqNames) => .Sorts
+  rule CoqNamesToSorts(NAME:CoqName NAMEs) => StringToSort("Term"), CoqNamesToSorts(NAMEs)
+
 // Terms
   syntax CoqTerm ::= "fun" CoqBinders "=>" CoqTerm
                    | "fix" CoqFixBodies