diff options
Diffstat (limited to 'snapshots/hol4/lem/hol-lib/lemLib.sml')
| -rw-r--r-- | snapshots/hol4/lem/hol-lib/lemLib.sml | 105 |
1 files changed, 105 insertions, 0 deletions
diff --git a/snapshots/hol4/lem/hol-lib/lemLib.sml b/snapshots/hol4/lem/hol-lib/lemLib.sml new file mode 100644 index 00000000..93d06dc2 --- /dev/null +++ b/snapshots/hol4/lem/hol-lib/lemLib.sml @@ -0,0 +1,105 @@ +(*========================================================================*) +(* Lem *) +(* *) +(* Dominic Mulligan, University of Cambridge *) +(* Francesco Zappa Nardelli, INRIA Paris-Rocquencourt *) +(* Gabriel Kerneis, University of Cambridge *) +(* Kathy Gray, University of Cambridge *) +(* Peter Boehm, University of Cambridge (while working on Lem) *) +(* Peter Sewell, University of Cambridge *) +(* Scott Owens, University of Kent *) +(* Thomas Tuerk, University of Cambridge *) +(* *) +(* The Lem sources are copyright 2010-2013 *) +(* by the UK authors above and Institut National de Recherche en *) +(* Informatique et en Automatique (INRIA). *) +(* *) +(* All files except ocaml-lib/pmap.{ml,mli} and ocaml-libpset.{ml,mli} *) +(* are distributed under the license below. The former are distributed *) +(* under the LGPLv2, as in the LICENSE file. *) +(* *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in the *) +(* documentation and/or other materials provided with the distribution. *) +(* 3. The names of the authors may not be used to endorse or promote *) +(* products derived from this software without specific prior written *) +(* permission. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) +(* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) +(* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) +(* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) +(* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) +(* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) +(* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) +(* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER *) +(* IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR *) +(* OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN *) +(* IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) +(*========================================================================*) + + +structure lemLib = +struct + +open HolKernel Parse boolLib bossLib; +open lemTheory intReduce wordsLib; + +val run_interactive = ref false +val lem_conv_eval = computeLib.EVAL_CONV +val lem_conv_simp = SIMP_CONV (srw_ss()++permLib.PERM_ss) [] + + +val lem_convs = [lem_conv_eval, lem_conv_simp]; + + +datatype test_result = + Success + | Fail + | Unknown of term + + +fun lem_run_single_test (t:term) conv = +case total conv t of + NONE => NONE + | SOME thm => + if (can EQT_ELIM thm) then SOME Success else + if (can EQF_ELIM thm) then SOME Fail else + NONE +; + +fun lem_run_test t = + case Lib.get_first (lem_run_single_test t) lem_convs of + NONE => Unknown (rhs (concl (EVAL t))) + | SOME r => r + + +fun lem_assertion s t = +let + open PPBackEnd Parse; + fun terminal_print sty s = (if !run_interactive then print_with_style sty s else + Lib.with_flag (Parse.current_backend, PPBackEnd.vt100_terminal) (print_with_style sty) s); + val _ = print "Testing "; + val _ = terminal_print [FG LightBlue] s; + val _ = print ": ``"; + val _ = print_term t; + val _ = print ("`` "); + val result = lem_run_test t; + val _ = case result of + Success => terminal_print [FG Green] "OK\n" + | Fail => (terminal_print [FG OrangeRed] "FAILED\n"; + if (not (!run_interactive)) then Process.exit Process.failure else ()) + | Unknown t => (terminal_print [FG Yellow] "evaluation failed\n") +(* print_term t; + print "\n\n"*) +in + () +end; + +end |