Coq lang #38
Coq lang #38
Conversation
prover/build
Outdated
| # 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/*.v'), flags = '-cCOMMANDLINE=.CommandLine') |
There was a problem hiding this comment.
Let's move each test format to its own directory.
prover/lang/kore-lang.md
Outdated
| ```k | ||
| syntax Variable ::= VariableName "{" Sort "}" [klabel(sortedVariable)] | ||
| syntax Variable ::= VariableName "{" Sort "}" [klabel(sortedVariable)] | ||
| syntax SetVariable ::= VariableName "{{" Sort "}}" [klabel(sortedSetVariable)] |
There was a problem hiding this comment.
Should we be moving away from having the sort attached to the variable if we are moving towards AML?
Maybe we want: syntax SetVariable ::= "#" VariableName, and axiom \implies(#X, Int) as a local declaration (or part of the claim).
There was a problem hiding this comment.
Will this break any existing tests? It's definitely a change that won't affect anything for the Coq translation though
There was a problem hiding this comment.
Since we don't use set variables yet, I don't think anything would break? It should be \typeof(#X, Int) not implies.
There was a problem hiding this comment.
Whoops sorry, I thought you were talking about all variables. I'll fix this for set variables.
| </goals> | ||
| <declarations> | ||
| <declaration> | ||
| axiom \equals ( AndComm , \lambda { A { Term } , B { Term } , H { Term } , .Patterns } \or ( \exists { H0 , H1 , .Patterns } \and ( \equals ( H , conj ( H0 , H1 , .Patterns ) ) , conj ( H1 , H0 , .Patterns ) , .Patterns ) , .Patterns ) ) |
There was a problem hiding this comment.
In the current master, axioms in has always names attached: axiom ax0 : \equals[...]. Could you use getFreshGlobalAxiomName() from KORE-HELPERS to generate the names?
There was a problem hiding this comment.
Fixed, but should we remove the ability to have non-named axioms if we want to make named axioms standard?
There was a problem hiding this comment.
Maybe we should remove it. I will create an issue.
There was a problem hiding this comment.
Ad named axioms: you forgot to update the test files (*.expected).
| // Vernacular | ||
| syntax CoqSentence ::= CoqDefinition | ||
| | CoqInductive | ||
| // | CoqCoInductive |
There was a problem hiding this comment.
Any reason to keep these commented lines?
| syntax CoqDefinition ::= "Definition" CoqIdent ":=" CoqTerm "(*" "hasType" CoqTerm "*)" "." | ||
| | "Definition" CoqIdent CoqBinders ":" CoqTerm ":=" CoqTerm "(*" "hasType" CoqTerm "*)" "." | ||
| syntax CoqDefinition ::= "Definition" CoqIdent ":" CoqTerm ":=" CoqTerm "." | ||
| // | "Definition" CoqIdent CoqBinders ":" CoqTerm ":=" CoqTerm "." |
3 participants
No description provided.