Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add a timeout on the monotonicity check
authorblanchet
Tue, 24 Apr 2012 09:47:40 +0200
changeset 47716 dc9c8ce4aac5
parent 47715 04400144c6fc
child 47717 a0125644ccff
add a timeout on the monotonicity check
src/HOL/Tools/Nitpick/nitpick.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 24 09:47:40 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 24 09:47:40 2012 +0200
@@ -383,7 +383,9 @@
        (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
       is_number_type ctxt T orelse is_bit_type T
     fun is_type_actually_monotonic T =
-      formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
+      time_limit tac_timeout (formulas_monotonic hol_ctxt binarize T)
+                 (nondef_ts, def_ts)
+      handle TimeLimit.TimeOut => false
     fun is_type_kind_of_monotonic T =
       case triple_lookup (type_match thy) monos T of
         SOME (SOME false) => false
isabelle