Skip to content

Commit 9ea795c

Browse files
author
Dwight Guth
authored
Add proof hint integration tests to llvm backend proof hint tests (#1063)
This PR ensures that the body of proofs used by Pi Squared to test the math proof tests will be tested as regression tests for the proof hint emitter and parser. We do this by folding all of these small examples into the existing test suite. It's a pretty large PR but mostly just adds the definition.kore versions of the k-files files, and the .kore input files taken by parsing the programs found in the pi2 repo. We then commit the verbose proof hint that these examples generate. There is a pretty simple way to regenerate the output files that I can show anyone who is interested in the future if they need to modify the results when the proof hints change.
1 parent e27ae13 commit 9ea795c

File tree

265 files changed

+209539
-0
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

265 files changed

+209539
-0
lines changed

‎test/input/add-rewrite/input.in

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),inj{SortState{}, SortKItem{}}(Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())))))

‎test/input/arith/add.in

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),inj{SortExp{}, SortKItem{}}(Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(inj{SortInt{}, SortExp{}}(\dv{SortInt{}}("1")),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(inj{SortInt{}, SortExp{}}(\dv{SortInt{}}("1")),inj{SortInt{}, SortExp{}}(\dv{SortInt{}}("2"))))))))

‎test/input/arith/well.in

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),inj{SortExp{}, SortKItem{}}(Lblwell'LParUndsCommUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp'Unds'Exp{}(Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(inj{SortInt{}, SortExp{}}(\dv{SortInt{}}("1")),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(inj{SortInt{}, SortExp{}}(\dv{SortInt{}}("1")),inj{SortInt{}, SortExp{}}(\dv{SortInt{}}("2")))),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(inj{SortInt{}, SortExp{}}(\dv{SortInt{}}("5")),inj{SortInt{}, SortExp{}}(\dv{SortInt{}}("10"))),Lbladd'LParUndsCommUndsRParUnds'ARITH-SYNTAX'Unds'Exp'Unds'Exp'Unds'Exp{}(inj{SortInt{}, SortExp{}}(\dv{SortInt{}}("3")),inj{SortInt{}, SortExp{}}(\dv{SortInt{}}("4"))))))))

‎test/input/assoc-function/left.in

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),inj{SortFoo{}, SortKItem{}}(Lbl'UndsPlus'left'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{}(Lbl'UndsPlus'left'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{}(Lbl'UndsPlus'left'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{}(Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}(),Lblb'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()),Lblc'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()),Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}())))))

‎test/input/assoc-function/next-left.in

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),Lbl'Hash'next'LParUndsRParUnds'ASSOC-FUNCTION-SYNTAX'Unds'KItem'Unds'Foo{}(Lbl'UndsPlus'left'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{}(Lbl'UndsPlus'left'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{}(Lbl'UndsPlus'left'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{}(Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}(),Lblb'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()),Lblc'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}()),Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}())))))

‎test/input/assoc-function/next-right.in

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),Lbl'Hash'next'LParUndsRParUnds'ASSOC-FUNCTION-SYNTAX'Unds'KItem'Unds'Foo{}(Lbl'UndsPlus'right'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{}(Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}(),Lbl'UndsPlus'right'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{}(Lblb'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}(),Lbl'UndsPlus'right'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{}(Lblc'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}(),Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}())))))))

‎test/input/assoc-function/right.in

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),inj{SortFoo{}, SortKItem{}}(Lbl'UndsPlus'right'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{}(Lbla'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}(),Lbl'UndsPlus'right'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{}(Lblb'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}(),Lbl'UndsPlus'right'UndsUnds'ASSOC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo'Unds'Foo{}(Lblc'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}(),Lbld'Unds'ASSOC-FUNCTION-SYNTAX'Unds'Foo{}())))))))

‎test/input/builtin-functions/abs.in

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),inj{SortInt{}, SortKItem{}}(Lblabs'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'Int'Unds'Int{}(\dv{SortInt{}}("-5"))))))

‎test/input/builtin-functions/double.in

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),inj{SortInt{}, SortKItem{}}(Lbldouble'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'Int'Unds'Int{}(\dv{SortInt{}}("5"))))))

‎test/input/builtin-functions/head-bytes.in

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),inj{SortBytes{}, SortKItem{}}(Lblhead'LParUndsRParUnds'BUILTIN-FUNCTIONS-SYNTAX'Unds'Bytes'Unds'Bytes{}(\dv{SortBytes{}}("bytes"))))))

0 commit comments

Comments
 (0)