Coq lang

prover/build

@@ -18,9 +18,11 @@ proj = KProject()
 # Matching Logic Prover
 # =====================
 
-other_md_files = [ 'lang/smt-lang.md'
+other_md_files = [ 'lang/coq-lang.md'
+                 , 'lang/smt-lang.md'
                  , 'lang/kore-lang.md'
                  , 'drivers/base.md'
+                 , 'drivers/coq-driver.md'
                  , 'drivers/smt-driver.md'
                  , 'drivers/kore-driver.md'
                  , 'strategies/apply-equation.md'
@@ -53,13 +55,16 @@ def prover(alias, flags = None):
 
 prover_kore = prover('prover-kore', '--main-module DRIVER-KORE --syntax-module DRIVER-KORE-SYNTAX')
 prover_smt  = prover('prover-smt',  '--main-module DRIVER-SMT  --syntax-module DRIVER-SMT-SYNTAX' )
+prover_coq  = prover('prover-coq',  '--main-module DRIVER-COQ  --syntax-module DRIVER-COQ-SYNTAX' )
 
 # Functional tests
 # ----------------
 
 # prover_kore.tests(inputs = glob('t/*.kore'), implicit_inputs = glob('t/definitions/*.kore'), flags = '-cCOMMANDLINE=.CommandLine')
 # prover_smt .tests(inputs = glob('t/*.smt2'), flags = '-cCOMMANDLINE=.CommandLine')
 
+prover_coq .tests(inputs = glob('t/coq-tests/*.v'), flags = '-cCOMMANDLINE=.CommandLine')
+
 def log_on_success(file, message):
     return proj.rule( 'log-to-success'
                     , description = '$out: $message'

prover/drivers/coq-driver.md

@@ -0,0 +1,156 @@
+Coq Driver
+==========
+
+This file is responsible for loading definitions in the Coq format.
+
+```k
+module DRIVER-COQ-COMMON
+  imports COQ
+  imports STRATEGIES-EXPORTED-SYNTAX
+  syntax Pgm ::= CoqSentences
+endmodule
+```
+
+```k
+module DRIVER-COQ-SYNTAX
+  imports DRIVER-BASE-SYNTAX
+  imports DRIVER-COQ-COMMON
+  imports COQ-SYNTAX
+endmodule
+```
+
+```k
+module DRIVER-COQ
+  imports DRIVER-KORE
+  imports DRIVER-COQ-COMMON
+  imports KORE
+  imports PROVER-CONFIGURATION
+  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>
+
+// Add symbol (of sort Term) and equality axiom corresponding to each definition
+  rule Definition ID BINDERs : TYPE1 := TERM hasType TYPE2 . => Definition ID := TERM hasType TYPE2 .
+  rule <k> Definition ID := TERM hasType TYPE .
+        => .K
+           ...
+       </k>
+       <declarations> ( .Bag
+                     => <declaration> symbol CoqIdentToSymbol(ID)(.Sorts) : StringToSort("Term") </declaration>
+                        <declaration> axiom getFreshGlobalAxiomName() : \equals(CoqIdentToSymbol(ID), CoqTermToPattern(TERM)) </declaration>
+                      ) ...
+       </declarations>
+       <goals>
+         ( .Bag =>
+           <goal>
+             <id> !N:ClaimName </id>
+             <active> true:Bool </active>
+             <parent> .K </parent>
+             <claim> \type(CoqIdentToSymbol(ID), CoqTermToPattern(TYPE)) </claim>
+             <strategy> type-check </strategy>
+             <expected> success </expected>
+             <local-context> .Bag </local-context>
+             <trace> .K </trace>
+           </goal>
+         )
+         ...
+       </goals>
+
+
+// Translate inductive cases
+  rule <k> Inductive ID BINDERs : TERM := .CoqIndCases .
+        => .K
+           ...
+       </k>
+       <declarations> ( .Bag
+                     => <declaration> symbol CoqIdentToSymbol(ID)(.Sorts) : StringToSort("Term") </declaration>
+                      ) ...
+       </declarations>
+
+  rule <k> Inductive ID BINDERs : TERM := (IDC BINDERCs : TERMC) | CASEs .
+        => Inductive ID BINDERs : TERM := CASEs .
+           ...
+       </k>
+       <declarations> ( .Bag
+                     => <declaration> symbol CoqIdentToSymbol(IDC)(.Sorts) : StringToSort("Term") </declaration>
+                        <declaration> axiom getFreshGlobalAxiomName() : \type(CoqIdentToSymbol(IDC)(.Patterns), CoqTermToPattern(TERMC))  </declaration>
+                      ) ...
+       </declarations>
+
+// Converting Term to Pattern
+  syntax Pattern ::= CoqTermToPattern(CoqTerm) [function]
+  rule CoqTermToPattern(UN:UpperName) => CoqIdentToSymbol(UN)
+  rule CoqTermToPattern(LN:LowerName) => CoqIdentToSymbol(LN)
+  rule CoqTermToPattern(#token("Prop", "CoqSort")) => StringToSort("Term")
+  rule CoqTermToPattern(fun BINDERs => TERM) => \lambda { CoqBindersToPatterns(BINDERs) } CoqTermToPattern(TERM)
+  rule CoqTermToPattern(forall BINDERs, TERM) => \forall { CoqBindersToPatterns(BINDERs) } CoqTermToPattern(TERM)
+  rule CoqTermToPattern(match Ts with .CoqEquations end) => \bottom()
+  rule CoqTermToPattern(match Ts with (MP:CoqMultPattern => TM:CoqTerm) | EQs end) =>
+       \or( #flattenOrs(
+         \or( \exists { CoqMultPatternToBinders(MP) }
+                \and( #equals(CoqMatchItemsToPatterns(Ts), CoqMultPatternToPatterns(MP))
+                    ++Patterns
+                    CoqTermToPattern(TM)
+                    )
+            ++Patterns
+            CoqTermToPattern(match Ts with EQs end)
+            ), .Patterns))
+  rule CoqTermToPattern(TM:CoqTerm ARG) => CoqTermToPattern(TM)(CoqArgToPatterns(ARG))
+  rule CoqTermToPattern(fix ID BINDERs := TM) => \mu { # CoqNameToVariableName(ID) } CoqTermToPattern(fun BINDERs => TM)
+  rule CoqTermToPattern(@ QID:CoqQualID TM:CoqTerm) => CoqIdentToSymbol(QID)(CoqTermToPattern(TM))
+
+  syntax Patterns ::= CoqArgToPatterns(CoqArg) [function]
+  rule CoqArgToPatterns(ARG1 ARG2) => CoqArgToPatterns(ARG1) ++Patterns CoqArgToPatterns(ARG2)
+  rule CoqArgToPatterns(TM:CoqTerm) => CoqTermToPattern(TM), .Patterns
+   [owise]
+
+  syntax Patterns ::= CoqMatchItemsToPatterns(CoqMatchItems) [function]
+  syntax Pattern ::= CoqMatchItemToPattern(CoqMatchItem) [function]
+  rule CoqMatchItemsToPatterns(.CoqMatchItems) => .Patterns
+  rule CoqMatchItemsToPatterns(MI:CoqMatchItem, MIs) => CoqMatchItemToPattern(MI), .Patterns
+
+  rule CoqMatchItemToPattern(MI:CoqTerm) => CoqTermToPattern(MI)
+
+  syntax Patterns ::= #equals(Patterns, Patterns) [function]
+  rule #equals(.Patterns, .Patterns) => .Patterns
+  rule #equals((P1, Ps1), (P2, Ps2)) => \equals(P1, P2), #equals(Ps1, Ps2)
+
+  syntax Pattern ::= CoqPatternToPattern(CoqPattern) [function]
+  syntax Patterns ::= CoqPatternToPatterns(CoqPattern) [function]
+  syntax Patterns ::= CoqMultPatternToPatterns(CoqMultPattern) [function]
+  rule CoqMultPatternToPatterns(.CoqMultPattern) => .Patterns
+  rule CoqMultPatternToPatterns(MP, MPs) => CoqPatternToPattern(MP), CoqMultPatternToPatterns(MPs)
+
+  rule CoqPatternToPattern(ID:CoqQualID) => CoqIdentToSymbol(ID)
+  rule CoqPatternToPattern(ID:CoqQualID P:CoqPattern) => CoqIdentToSymbol(ID)(CoqPatternToPatterns(P))
+  rule CoqPatternToPatterns(ID:CoqQualID) => CoqIdentToSymbol(ID), .Patterns
+  rule CoqPatternToPatterns(ID:CoqQualID P:CoqPattern) => CoqIdentToSymbol(ID) ++Patterns CoqPatternToPatterns(P)
+
+// Get binders from MultPattern
+  syntax Patterns ::= CoqMultPatternToBinders(CoqMultPattern) [function]
+  syntax Patterns ::= CoqPatternToBinders(CoqMultPattern) [function]
+  rule CoqMultPatternToBinders(ID:CoqQualID) => .Patterns
+  rule CoqMultPatternToBinders(ID:CoqQualID P:CoqPattern) => CoqPatternToBinders(P)
+  rule CoqPatternToBinders(ID:CoqQualID) => CoqIdentToSymbol(ID), .Patterns
+  rule CoqPatternToBinders(ID:CoqQualID P:CoqPattern) => CoqIdentToSymbol(ID), CoqPatternToBinders(P)
+
+  syntax Patterns ::= CoqBindersToPatterns(CoqBinders) [function]
+  rule CoqBindersToPatterns(.CoqBinders) => .Patterns
+  rule CoqBindersToPatterns(BINDER BINDERs:CoqBinders) =>
+       CoqBinderToPatterns(BINDER) ++Patterns CoqBindersToPatterns(BINDERs)
+
+  syntax Patterns ::= CoqBinderToPatterns(CoqBinder) [function]
+  rule CoqBinderToPatterns(NAME:CoqName) => CoqNameToVariableName(NAME) { StringToSort("Term") }
+  rule CoqBinderToPatterns((.CoqNames : TYPE:CoqTerm)) => .Patterns
+  rule CoqBinderToPatterns(((NAME:CoqName NAMES:CoqNames) : TYPE:CoqTerm)) => CoqNameToVariableName(NAME) { StringToSort("Term") }, CoqBinderToPatterns((NAMES : TYPE))
+```
+
+```k
+endmodule
+```

prover/lang/coq-lang.md

@@ -0,0 +1,116 @@
+```k
+module COQ-SYNTAX
+  imports TOKENS-SYNTAX
+  imports COQ
+endmodule
+
+module COQ
+  imports INT-SYNTAX
+  imports BOOL-SYNTAX
+  imports STRING
+  imports KORE-HELPERS
+
+// Identifiers
+  syntax CoqIdent ::= LowerName
+                    | UpperName
+  syntax CoqQualID ::= CoqIdent
+  syntax CoqName ::= CoqIdent
+                   | Underscore
+  syntax CoqNames ::= List{CoqName, ""} [klabel(CoqNames)]
+
+// Sorts
+  syntax CoqSort ::= "SProp" [token]
+                   | "Prop"  [token]
+                   | "Set"   [token]
+                   | "Type"  [token]
+
+// Seralize to String:
+  syntax String ::= CoqNameToString(CoqName) [function, functional, hook(STRING.token2string)]
+
+// Sort conversions
+  syntax Symbol ::= CoqIdentToSymbol(CoqIdent) [function]
+  rule CoqIdentToSymbol(IDENT:UpperName) => IDENT
+  rule CoqIdentToSymbol(IDENT:LowerName) => IDENT
+
+  syntax Symbol ::= CoqQualIDToSymbol(CoqQualID) [function]
+  rule CoqQualIDToSymbol(ID:CoqIdent) => CoqIdentToSymbol(ID)
+
+  syntax VariableName ::= CoqNameToVariableName(CoqName) [function]
+  rule CoqNameToVariableName(NAME) => StringToVariableName(CoqNameToString(NAME))
+
+  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
+                   | "cofix" CoqCofixBodies
+                   | "let" CoqIdent ":=" CoqTerm "in" CoqTerm
+                   | "let" CoqIdent CoqBinders ":" CoqTerm ":=" CoqTerm "in" CoqTerm
+                   | "@" CoqQualID CoqTerm
+                   | "match" CoqMatchItems "with" CoqEquations "end"
+                   > CoqTerm CoqArg [right]
+                   | CoqQualID
+                   | CoqSort
+                   | Int
+                   | Underscore
+                   > "forall" CoqBinders "," CoqTerm
+                   > "(" CoqTerm ")" [bracket]
+
+  syntax CoqBinder ::= CoqName
+                     | "(" CoqNames ":" CoqTerm ")"
+  syntax CoqBinders ::= List{CoqBinder, ""} [klabel(CoqBinders)]
+
+  syntax CoqArg ::= CoqArg CoqArg
+                  | "(" CoqIdent ":=" CoqTerm ")"
+                  > CoqTerm
+  syntax CoqTerms ::= List{CoqTerm, ""} [klabel(CoqTerms)]
+
+  syntax CoqFixBody ::= CoqIdent CoqBinders ":=" CoqTerm
+                      | CoqIdent CoqBinders ":" CoqTerm ":=" CoqTerm
+  syntax CoqFixBodyList ::= List{CoqFixBody, "with"}
+  syntax CoqFixBodies ::= CoqFixBody
+                        | CoqFixBody CoqFixBodyList "for" CoqIdent
+
+  syntax CoqCofixBody ::= CoqIdent CoqBinders ":=" CoqTerm
+  syntax CoqCofixBodyList ::= List{CoqCofixBody, "with"}
+  syntax CoqCofixBodies ::= CoqCofixBody
+                          | CoqCofixBody CoqCofixBodyList "for" CoqIdent
+
+  syntax CoqMatchItem ::= CoqTerm
+  syntax CoqMatchItems ::= List{CoqMatchItem, ","} [klabel(CoqMatchItems)]
+
+  syntax CoqEquation ::= CoqMultPattern "=>" CoqTerm
+  syntax CoqEquations ::= List{CoqEquation, "|"} [klabel(CoqEquations)]
+
+  syntax CoqPattern ::= CoqQualID CoqPattern
+                      | "@" CoqQualID CoqPattern
+                      // | CoqPattern CoqPattern
+                      | CoqPattern "as" CoqIdent
+                      | CoqPattern "%" CoqIdent
+                      | CoqQualID
+                      | Underscore
+                      | Int
+
+  syntax CoqMultPattern ::= List{CoqPattern, ","} [klabel(CoqMultPattern)]
+  syntax CoqPatterns ::= NeList{CoqPattern, ""} [klabel(CoqPatterns)]
+
+// Vernacular
+  syntax CoqSentence ::= CoqDefinition
+                       | CoqInductive
+  //                   | CoqCoInductive
+  syntax CoqSentences ::= List{CoqSentence, ""} [klabel(CoqSentences), format(%1%n%2 %3)]
+  syntax CoqDefinition ::= "Definition" CoqIdent ":=" CoqTerm "hasType" CoqTerm "."
+                         | "Definition" CoqIdent CoqBinders ":" CoqTerm ":=" CoqTerm "hasType" CoqTerm "."
+
+  syntax CoqInductive ::= "Inductive" CoqIndBody "."
+  syntax CoqIndBody ::= CoqIdent CoqBinders ":" CoqTerm ":=" CoqIndCases
+  syntax CoqIndCase ::= CoqIdent CoqBinders ":" CoqTerm
+  syntax CoqIndCases ::= List{CoqIndCase, "|"} [klabel(CoqIndCases)]
+
+```
+
+```k
+endmodule
+```

prover/lang/kore-lang.md

@@ -9,6 +9,7 @@ module TOKENS
   syntax ColonName
   syntax PipeQID
   syntax Decimal
+  syntax Underscore
 
   // Abstract
   syntax Symbol ::= UpperName | LowerName
@@ -118,6 +119,7 @@ module TOKENS-SYNTAX
   syntax ColonName ::= r":[a-z][A-Za-z\\-0-9'\\#\\_]*" [token, autoReject]
   syntax Decimal ::= r"[0-9][0-9]*\\.[0-9][0-9]*" [token, autoreject]
                    | "2.0" [token]
+  syntax Underscore ::= "_" [token]
 endmodule
 
 module KORE
@@ -135,11 +137,13 @@ is to be used for generating fresh variables. *The second variety must be used
 only in this scenario*.
 
 ```k
-  syntax Variable ::= VariableName "{" Sort "}" [klabel(sortedVariable)]
+  syntax Variable    ::= VariableName  "{" Sort "}"  [klabel(sortedVariable)]
+  syntax SetVariable ::= "#" VariableName [klabel(setVariable)]
   syntax Pattern ::= Int
                    | Variable
+                   | SetVariable
                    | Symbol
-                   | Symbol "(" Patterns ")"                    [klabel(apply)]
+                   | Pattern "(" Patterns ")"                   [klabel(apply)]
 
                    | "\\top"    "(" ")"                         [klabel(top)]
                    | "\\bottom" "(" ")"                         [klabel(bottom)]
@@ -153,6 +157,9 @@ only in this scenario*.
                    | "\\exists" "{" Patterns "}" Pattern        [klabel(exists)]
                    | "\\forall" "{" Patterns "}" Pattern        [klabel(forall)]
 
+                   | "\\mu" "{" Patterns "}" Pattern            [klabel(mu)]
+                   | "\\nu" "{" Patterns "}" Pattern            [klabel(nu)]
+
                      /* Sugar for \iff, \mu and application */
                    | "\\iff-lfp" "(" Pattern "," Pattern ")"    [klabel(ifflfp)]
 
@@ -162,6 +169,11 @@ only in this scenario*.
                    | "heap" "(" Sort "," Sort ")" // Location, Data
                    | "\\hole" "(" ")" [klabel(Phole)]
 
+                   // for Coq translation
+                   | "\\lambda" "{" Patterns "}" Pattern        [klabel(lambda)]
+                   | "\\pi"     "{" Patterns "}" Pattern        [klabel(pi)]
+                   | "\\type" "(" Pattern "," Pattern ")"       [klabel(type)]
+
   rule \top()    => \and(.Patterns) [anywhere]
   rule \bottom() => \or(.Patterns) [anywhere]
 
@@ -207,6 +219,9 @@ module KORE-HELPERS
   syntax String ::= SortToString(Sort)     [function, functional, hook(STRING.token2string)]
   syntax String ::= SymbolToString(Symbol) [function, functional, hook(STRING.token2string)]
   syntax LowerName ::= StringToSymbol(String) [function, functional, hook(STRING.string2token)]
+  syntax UpperName ::= StringToSort(String) [function, functional, hook(STRING.string2token)]
+
+  syntax VariableName ::= StringToVariableName(String) [function, functional, hook(STRING.string2token)]
 
   syntax Symbol ::= parameterizedSymbol(Symbol, Sort) [function]
   rule parameterizedSymbol(SYMBOL, SORT) => StringToSymbol(SymbolToString(SYMBOL) +String "_" +String SortToString(SORT))

prover/lang/smt-lang.md

@@ -103,6 +103,7 @@ module SMTLIB2-HELPERS
   imports K-IO
   imports SMTLIB2
   imports PROVER-CORE-SYNTAX
+  imports KORE-HELPERS
 
   syntax SMTLIB2AttributeValue ::=  CheckSATResult
   syntax CheckSATResult ::= "error" "(" K ")"
@@ -116,7 +117,6 @@ module SMTLIB2-HELPERS
 
 // Converting between Sorts:
 
-  syntax VariableName ::= StringToVariableName(String) [function, functional, hook(STRING.string2token)]
   syntax VariableName ::= SMTLIB2SimpleSymbolToVariableName(SMTLIB2SimpleSymbol) [function]
   rule SMTLIB2SimpleSymbolToVariableName(SYMBOL) => StringToVariableName("V" +String SMTLIB2SimpleSymbolToString(SYMBOL))
 

prover/prover

@@ -18,6 +18,12 @@ KDefinition( proj
            , directory = proj.builddir('defn/prover-smt')
            , krun_flags = '--interpret'
            )
+KDefinition( proj
+           , alias = 'prover-coq'
+           , backend = 'ocaml'
+           , directory = proj.builddir('defn/prover-coq')
+           , krun_flags = '--interpret'
+           )
 KDefinition( proj
            , alias = 'test-driver'
            , backend = 'llvm'