diff options
| author | Thomas Bauereiss | 2018-02-14 19:45:07 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-02-15 20:11:21 +0000 |
| commit | 737ec26cf494affb346504c482e9b91127b68636 (patch) | |
| tree | 30bcac2487eb2294952624aa25321a0299c6e2e7 /test | |
| parent | 9883998c6de1a0421eacb4f4c352b0aa8c4a1b5c (diff) | |
Rebase state monad onto prompt monad
Generate only one Lem model based on the prompt monad (instead of two models
with different monads), and add a lifting from prompt to state monad. Add some
Isabelle lemmas about the monad lifting.
Also drop the "_embed" and "_sequential" suffixes from names of generated
files.
Diffstat (limited to 'test')
| -rwxr-xr-x | test/lem/run_tests.sh | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/test/lem/run_tests.sh b/test/lem/run_tests.sh index c53ec189..2cd97ab5 100755 --- a/test/lem/run_tests.sh +++ b/test/lem/run_tests.sh @@ -46,11 +46,13 @@ function finish_suite { printf "<testsuites>\n" >> $DIR/tests.xml +cd $DIR + for i in `ls $TESTSDIR/ | grep sail`; do - if $SAILDIR/sail -lem -lem_sequential -o out $TESTSDIR/$i &>/dev/null; + if $SAILDIR/sail -lem -o out $TESTSDIR/$i &>/dev/null; then - if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib out_embed_types_sequential.lem out_embed_sequential.lem &>/dev/null; + if lem -lib $SAILDIR/src/lem_interp -lib $SAILDIR/src/gen_lib out_types.lem out.lem &>/dev/null; then green "tested $i expecting pass" "pass" else |