From b876330f60a5514949886a28e1569173323bc0ff Mon Sep 17 00:00:00 2001 From: Frederic Vogels Date: Fri, 15 Nov 2024 22:22:05 +0100 Subject: [PATCH] bool-inequality-function-notation --- .../base.template.html | 38 +++++++++++++ .../base.template.v | 16 ++++++ .../configuration.lisp | 57 +++++++++++++++++++ .../machine.template.html | 38 +++++++++++++ .../machine.template.v | 5 ++ .../model.sail | 9 +++ .../bool-inequality-function-notation/test.sh | 20 +++++++ .../translate.sh | 15 +++++ 8 files changed, 198 insertions(+) create mode 100644 tests/coq-tests/bool-inequality-function-notation/base.template.html create mode 100644 tests/coq-tests/bool-inequality-function-notation/base.template.v create mode 100644 tests/coq-tests/bool-inequality-function-notation/configuration.lisp create mode 100644 tests/coq-tests/bool-inequality-function-notation/machine.template.html create mode 100644 tests/coq-tests/bool-inequality-function-notation/machine.template.v create mode 100644 tests/coq-tests/bool-inequality-function-notation/model.sail create mode 100755 tests/coq-tests/bool-inequality-function-notation/test.sh create mode 100755 tests/coq-tests/bool-inequality-function-notation/translate.sh diff --git a/tests/coq-tests/bool-inequality-function-notation/base.template.html b/tests/coq-tests/bool-inequality-function-notation/base.template.html new file mode 100644 index 000000000..ccd9b18a8 --- /dev/null +++ b/tests/coq-tests/bool-inequality-function-notation/base.template.html @@ -0,0 +1,38 @@ + + + + + + +(*< + (generate (base-html-translation)) +>*) + + diff --git a/tests/coq-tests/bool-inequality-function-notation/base.template.v b/tests/coq-tests/bool-inequality-function-notation/base.template.v new file mode 100644 index 000000000..6756142a2 --- /dev/null +++ b/tests/coq-tests/bool-inequality-function-notation/base.template.v @@ -0,0 +1,16 @@ +(*< + (generate (base-translation)) +>*) + +(*< + (if (untranslated-definitions?) + (generate "Theorem UNTRANSLATED_DEFINITIONS : False. Qed.")) +>*) + +(* + +(*< + (generate (untranslated-definitions)) +>*) + +*) diff --git a/tests/coq-tests/bool-inequality-function-notation/configuration.lisp b/tests/coq-tests/bool-inequality-function-notation/configuration.lisp new file mode 100644 index 000000000..4513b78e9 --- /dev/null +++ b/tests/coq-tests/bool-inequality-function-notation/configuration.lisp @@ -0,0 +1,57 @@ +(use-list-notations) + +(ignore-all-overloads) +(ignore-pragmas "include_start" + "include_end" + "file_start" + "file_end" + "sail_internal") + +(ignore-function-definition-predicate (lambda (identifier) + (or + (string-ends-with? "_of_num" identifier) + (string-starts-with? "num_of_" identifier) + (string-starts-with? "undefined_" identifier) + (string-starts-with? "regval_of_" identifier) + (string-ends-with? "_of_regval" identifier) + (contains? '( + "eq_unit" + "neq_int" + "neq_bool" + "neq_bits" + "slice_mask" + "_shl_int_general" + "_shr_int_general" + "fdiv_int" + "fmod_int" + "is_none" + "is_some" + "__id" + "sail_mask" + "sail_ones" + "concat_str_bits" + "concat_str_dec") + identifier)))) + +(ignore-type-definition-predicate (lambda (identifier) + (contains? '( + "option" + "register_value" + "bits" + "regstate") + identifier))) + +(ignore-value-definition-predicate + (lambda (identifier) + (contains? '( + "default_capability" + "initial_regstate" + "initial_Capability" + ) + identifier))) + +(template "base.template.v") +(template "machine.template.v") +(template "base.template.html") +(template "machine.template.html") + diff --git a/tests/coq-tests/bool-inequality-function-notation/machine.template.html b/tests/coq-tests/bool-inequality-function-notation/machine.template.html new file mode 100644 index 000000000..6e0cd213c --- /dev/null +++ b/tests/coq-tests/bool-inequality-function-notation/machine.template.html @@ -0,0 +1,38 @@ + + + + + + +(*< + (generate (program-html-translation)) +>*) + + diff --git a/tests/coq-tests/bool-inequality-function-notation/machine.template.v b/tests/coq-tests/bool-inequality-function-notation/machine.template.v new file mode 100644 index 000000000..c2c2d87eb --- /dev/null +++ b/tests/coq-tests/bool-inequality-function-notation/machine.template.v @@ -0,0 +1,5 @@ +Require Export base. + +(*< + (generate (program-translation)) +>*) diff --git a/tests/coq-tests/bool-inequality-function-notation/model.sail b/tests/coq-tests/bool-inequality-function-notation/model.sail new file mode 100644 index 000000000..e0129a364 --- /dev/null +++ b/tests/coq-tests/bool-inequality-function-notation/model.sail @@ -0,0 +1,9 @@ +default Order dec + +$include + + +val foo : (bool, bool) -> bool +function foo(x, y) = { + x != y +} \ No newline at end of file diff --git a/tests/coq-tests/bool-inequality-function-notation/test.sh b/tests/coq-tests/bool-inequality-function-notation/test.sh new file mode 100755 index 000000000..6af8f08c8 --- /dev/null +++ b/tests/coq-tests/bool-inequality-function-notation/test.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash + +set -e + +SAIL=sail +COQ=coqc + +SAIL_SOURCES=model.sail +TESTED_FILE=microsail.v + +if [ -n "$1" ] +then + OPT="-ddump_rewrite_ast intermediate" +else + OPT= +fi + +$SAIL $OPT -katamaran -katamaran_config configuration.lisp $SAIL_SOURCES +$COQ base.v +$COQ machine.v diff --git a/tests/coq-tests/bool-inequality-function-notation/translate.sh b/tests/coq-tests/bool-inequality-function-notation/translate.sh new file mode 100755 index 000000000..71c86aee7 --- /dev/null +++ b/tests/coq-tests/bool-inequality-function-notation/translate.sh @@ -0,0 +1,15 @@ +#!/usr/bin/env bash +SAIL=sail +COQ=coqc + +SAIL_SOURCES=model.sail +TESTED_FILE=microsail.v + +if [ -n "$1" ] +then + OPT="-ddump_rewrite_ast intermediate" +else + OPT= +fi + +$SAIL $OPT -katamaran -katamaran_config configuration.lisp $SAIL_SOURCES