merged
authordesharna
Fri, 09 Jul 2021 17:59:25 +0200
changeset 74205 3aace56d282e
parent 74204 57423714c29d (current diff)
parent 74200 76dbf39a708d (diff)
child 74221 e17f76705cee
merged
--- a/Admin/jenkins/build/ci_build_benchmark.scala	Fri Jul 09 17:58:17 2021 +0200
+++ b/Admin/jenkins/build/ci_build_benchmark.scala	Fri Jul 09 17:59:25 2021 +0200
@@ -9,8 +9,8 @@
   def include = Nil
   def select = List(Path.explode("$ISABELLE_HOME/src/Benchmarks"))
 
-  def pre_hook(args: List[String]) = {}
-  def post_hook(results: Build.Results) = {}
+  def pre_hook(args: List[String]) = Result.ok
+  def post_hook(results: Build.Results) = Result.ok
 
   def selection = Sessions.Selection(session_groups = List("timing"))
 
--- a/src/Tools/ROOT	Fri Jul 09 17:58:17 2021 +0200
+++ b/src/Tools/ROOT	Fri Jul 09 17:59:25 2021 +0200
@@ -4,11 +4,6 @@
   theories
     Code_Generator
 
-session Spec_Check in Spec_Check = Pure +
-  theories
-    Spec_Check
-    Examples
-
 session SML in SML = Pure +
   theories
     Examples
--- a/src/Tools/Spec_Check/Examples.thy	Fri Jul 09 17:58:17 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-theory Examples
-imports Spec_Check
-begin
-
-section \<open>List examples\<close>
-
-ML_command \<open>
-check_property "ALL xs. rev xs = xs";
-\<close>
-
-ML_command \<open>
-check_property "ALL xs. rev (rev xs) = xs";
-\<close>
-
-
-section \<open>AList Specification\<close>
-
-ML_command \<open>
-(* map_entry applies the function to the element *)
-check_property "ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = Option.map f (AList.lookup (op =) xs k)";
-\<close>
-
-ML_command \<open>
-(* update always results in an entry *)
-check_property "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k";
-\<close>
-
-ML_command \<open>
-(* update always writes the value *)
-check_property "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v";
-\<close>
-
-ML_command \<open>
-(* default always results in an entry *)
-check_property "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k";
-\<close>
-
-ML_command \<open>
-(* delete always removes the entry *)
-check_property "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)";
-\<close>
-
-ML_command \<open>
-(* default writes the entry iff it didn't exist *)
-check_property "ALL k v xs. (AList.lookup (op =) (AList.default (op =) (k, v) xs) k = (if AList.defined (op =) xs k then AList.lookup (op =) xs k else SOME v))";
-\<close>
-
-section \<open>Examples on Types and Terms\<close>
-
-ML_command \<open>
-check_property "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t";
-\<close>
-
-ML_command \<open>
-check_property "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t";
-\<close>
-
-
-text \<open>One would think this holds:\<close>
-
-ML_command \<open>
-check_property "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)"
-\<close>
-
-text \<open>But it only holds with this precondition:\<close>
-
-ML_command \<open>
-check_property "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)"
-\<close>
-
-section \<open>Some surprises\<close>
-
-ML_command \<open>
-check_property "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)"
-\<close>
-
-
-ML_command \<open>
-val thy = \<^theory>;
-check_property "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true"
-\<close>
-
-end
--- a/src/Tools/Spec_Check/README	Fri Jul 09 17:58:17 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-This is a Quickcheck tool for Isabelle/ML.
-
-Authors
-
-  Lukas Bulwahn
-  Nicolai Schaffroth
-
-Quick Usage
-
-  - Import Spec_Check.thy in your development
-  - Look at examples in Examples.thy
-  - write specifications with the ML invocation
-      check_property "ALL x. P x"
-
-Notes
-
-Our specification-based testing tool originated from Christopher League's
-QCheck tool for SML (cf. https://github.com/league/qcheck). As Isabelle
-provides a rich and uniform ML platform (called Isabelle/ML), this
-testing tools is very different than the one for a typical ML developer.
-
-1. Isabelle/ML provides common data structures, which we can use in the
-tool's implementation for storing data and printing output.
-
-2. The implementation in Isabelle that will be checked with this tool
-commonly use Isabelle/ML's int type (which corresponds ML's IntInf.int),
-but they do not use other integer types in ML, such as ML's Int.int,
-Word.word and others.
-
-3. As Isabelle can run heavily in parallel, we avoid reference types.
-
-4. Isabelle has special naming conventions and documentation of source
-code is only minimal to avoid parroting.
-
-Next steps:
-  - Remove all references and store the neccessary random seed in the
-    Isabelle's context.
-  - Simplify some existing random generators.
-    The original ones from Christopher League are so complicated to
-    support many integer types uniformly.
-
-License
-
-  The source code originated from Christopher League's QCheck, which is
-  licensed under the 2-clause BSD license. The current source code is
-  licensed under the compatible 3-clause BSD license of Isabelle.
-
--- a/src/Tools/Spec_Check/Spec_Check.thy	Fri Jul 09 17:58:17 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-theory Spec_Check
-imports Pure
-begin
-
-ML_file \<open>random.ML\<close>
-ML_file \<open>property.ML\<close>
-ML_file \<open>base_generator.ML\<close>
-ML_file \<open>generator.ML\<close>
-ML_file \<open>gen_construction.ML\<close>
-ML_file \<open>spec_check.ML\<close>
-ML_file \<open>output_style.ML\<close>
-
-end
\ No newline at end of file
--- a/src/Tools/Spec_Check/base_generator.ML	Fri Jul 09 17:58:17 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,201 +0,0 @@
-(*  Title:      Tools/Spec_Check/base_generator.ML
-    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
-    Author:     Christopher League
-
-Basic random generators.
-*)
-
-signature BASE_GENERATOR =
-sig
-
-type rand
-type 'a gen = rand -> 'a * rand
-type ('a, 'b) co = 'a -> 'b gen -> 'b gen
-
-val new : unit -> rand
-val range : int * int -> rand -> int * rand
-type ('a, 'b) reader = 'b -> ('a * 'b) option
-
-val lift : 'a -> 'a gen
-val select : 'a vector -> 'a gen
-val choose : 'a gen vector -> 'a gen
-val choose' : (int * 'a gen) vector -> 'a gen
-val selectL : 'a list -> 'a gen
-val chooseL : 'a gen list -> 'a gen
-val chooseL' : (int * 'a gen) list -> 'a gen
-val filter : ('a -> bool) -> 'a gen -> 'a gen
-
-val zip : ('a gen * 'b gen) -> ('a * 'b) gen
-val zip3 : ('a gen * 'b gen * 'c gen) -> ('a * 'b * 'c) gen
-val zip4 : ('a gen * 'b gen * 'c gen * 'd gen) -> ('a * 'b * 'c * 'd) gen
-val map : ('a -> 'b) -> 'a gen -> 'b gen
-val map2 : ('a * 'b -> 'c) -> ('a gen * 'b gen) -> 'c gen
-val map3 : ('a * 'b * 'c -> 'd) -> ('a gen * 'b gen * 'c gen) -> 'd gen
-val map4 : ('a * 'b * 'c * 'd -> 'e) -> ('a gen * 'b gen * 'c gen * 'd gen) -> 'e gen
-
-val flip : bool gen
-val flip' : int * int -> bool gen
-
-val list : bool gen -> 'a gen -> 'a list gen
-val option : bool gen -> 'a gen -> 'a option gen
-val vector : (int * (int -> 'a) -> 'b) -> int gen * 'a gen -> 'b gen
-
-val variant : (int, 'b) co
-val arrow : ('a, 'b) co * 'b gen -> ('a -> 'b) gen
-val cobool : (bool, 'b) co
-val colist : ('a, 'b) co -> ('a list, 'b) co
-val coopt : ('a, 'b) co -> ('a option, 'b) co
-
-type stream
-val start : rand -> stream
-val limit : int -> 'a gen -> ('a, stream) reader
-
-end
-
-structure Base_Generator : BASE_GENERATOR =
-struct
-
-(* random number engine *)
-
-type rand = real
-
-val a = 16807.0
-val m = 2147483647.0
-
-fun nextrand seed =
-  let
-    val t = a * seed
-  in
-    t - m * real (floor (t / m))
-  end
-
-val new = nextrand o Time.toReal o Time.now
-
-fun range (min, max) =
-  if min > max then raise Domain (* TODO: raise its own error *)
-  else fn r => (min + (floor (real (max - min + 1) * r / m)), nextrand r)
-
-fun split r =
-  let
-    val r = r / a
-    val r0 = real (floor r)
-    val r1 = r - r0
-  in
-    (nextrand r0, nextrand r1)
-  end
-
-(* generators *)
-
-type 'a gen = rand -> 'a * rand
-type ('a, 'b) reader = 'b -> ('a * 'b) option
-
-fun lift obj r = (obj, r)
-
-local (* Isabelle does not use vectors? *)
-  fun explode ((freq, gen), acc) =
-    List.tabulate (freq, fn _ => gen) @ acc
-in
-  fun choose v r =
-    let val (i, r) = range(0, Vector.length v - 1) r
-    in Vector.sub (v, i) r end
-  fun choose' v = choose (Vector.fromList (Vector.foldr explode [] v))
-  fun select v = choose (Vector.map lift v)
-end
-
-fun chooseL l = choose (Vector.fromList l)
-fun chooseL' l = choose' (Vector.fromList l)
-fun selectL l = select (Vector.fromList l)
-
-fun zip (g1, g2) = g1 #-> (fn x1 => g2 #-> (fn x2 => pair (x1, x2)))
-
-fun zip3 (g1, g2, g3) =
-  zip (g1, zip (g2, g3)) #-> (fn (x1, (x2, x3)) => pair (x1, x2, x3))
-
-fun zip4 (g1, g2, g3, g4) =
-  zip (zip (g1, g2), zip (g3, g4)) #-> (fn ((x1, x2), (x3, x4)) => pair (x1, x2, x3, x4))
-
-fun map f g = apfst f o g
-
-fun map2 f = map f o zip
-fun map3 f = map f o zip3
-fun map4 f = map f o zip4
-
-fun filter p gen r =
-  let
-    fun loop (x, r) = if p x then (x, r) else loop (gen r)
-  in
-    loop (gen r)
-  end
-
-val flip = selectL [true, false]
-fun flip' (p, q) = chooseL' [(p, lift true), (q, lift false)]
-
-fun list flip g r =
-  case flip r of
-      (true, r) => ([], r)
-    | (false, r) =>
-      let
-        val (x,r) = g r
-        val (xs,r) = list flip g r
-      in (x::xs, r) end
-
-fun option flip g r =
-  case flip r of
-    (true, r) => (NONE, r)
-  | (false, r) => map SOME g r
-
-fun vector tabulate (int, elem) r =
-  let
-    val (n, r) = int r
-    val p = Unsynchronized.ref r
-    fun g _ =
-      let
-        val (x,r) = elem(!p)
-      in x before p := r end
-  in
-    (tabulate(n, g), !p)
-  end
-
-type stream = rand Unsynchronized.ref * int
-
-fun start r = (Unsynchronized.ref r, 0)
-
-fun limit max gen =
-  let
-    fun next (p, i) =
-      if i >= max then NONE
-      else
-        let val (x, r) = gen(!p)
-        in SOME(x, (p, i+1)) before p := r end
-  in
-    next
-  end
-
-type ('a, 'b) co = 'a -> 'b gen -> 'b gen
-
-fun variant v g r =
-  let
-    fun nth (i, r) =
-      let val (r1, r2) = split r
-      in if i = 0 then r1 else nth (i-1, r2) end
-  in
-    g (nth (v, r))
-  end
-
-fun arrow (cogen, gen) r =
-  let
-    val (r1, r2) = split r
-    fun g x = fst (cogen x gen r1)
-  in (g, r2) end
-
-fun cobool false = variant 0
-  | cobool true = variant 1
-
-fun colist _ [] = variant 0
-  | colist co (x::xs) = variant 1 o co x o colist co xs
-
-fun coopt _ NONE = variant 0
-  | coopt co (SOME x) = variant 1 o co x
-
-end
-
--- a/src/Tools/Spec_Check/gen_construction.ML	Fri Jul 09 17:58:17 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,179 +0,0 @@
-(*  Title:      Tools/Spec_Check/gen_construction.ML
-    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
-    Author:     Christopher League
-
-Constructing generators and pretty printing function for complex types.
-*)
-
-signature GEN_CONSTRUCTION =
-sig
-  val register : string * (string * string) -> theory -> theory
-  type mltype
-  val parse_pred : string -> string * mltype
-  val build_check : Proof.context -> string -> mltype * string -> string
-  (*val safe_check : string -> mltype * string -> string*)
-  val string_of_bool : bool -> string
-  val string_of_ref : ('a -> string) -> 'a Unsynchronized.ref -> string
-end;
-
-structure Gen_Construction : GEN_CONSTRUCTION =
-struct
-
-(* Parsing ML types *)
-
-datatype mltype = Var | Con of string * mltype list | Tuple of mltype list;
-
-(*Split string into tokens for parsing*)
-fun split s =
-  let
-    fun split_symbol #"(" = "( "
-      | split_symbol #")" = " )"
-      | split_symbol #"," = " ,"
-      | split_symbol #":" = " :"
-      | split_symbol c = Char.toString c
-    fun is_space c = c = #" "
-  in String.tokens is_space (String.translate split_symbol s) end;
-
-(*Accept anything that is not a recognized symbol*)
-val scan_name = Scan.one (fn s => not (String.isSubstring s "(),*->;"));
-
-(*Turn a type list into a nested Con*)
-fun make_con [] = raise Empty
-  | make_con [c] = c
-  | make_con (Con (s, _) :: cl) = Con (s, [make_con cl]);
-
-(*Parse a type*)
-fun parse_type s = (parse_fun || parse_tuple || parse_type_single) s
-
-and parse_type_arg s = (parse_tuple || parse_type_single) s
-
-and parse_type_single s = (parse_con || parse_type_basic) s
-
-and parse_type_basic s = (parse_var || $$ "(" |-- parse_type --| $$ ")") s
-
-and parse_list s =
-  ($$ "(" |-- parse_type -- Scan.repeat1 ($$ "," |-- parse_type) --| $$ ")" >> op::) s
-
-and parse_var s = (Scan.one (String.isPrefix "'") >> (fn _ => Var)) s
-
-and parse_con s = ((parse_con_nest
-  || parse_type_basic -- parse_con_nest >> (fn (b, Con (t, _) :: tl) => Con (t, [b]) :: tl)
-  || parse_list -- parse_con_nest >> (fn (l, Con (t, _) :: tl) => Con (t, l) :: tl))
-  >> (make_con o rev)) s
-
-and parse_con_nest s = Scan.unless parse_var (Scan.repeat1 (scan_name >> (fn t => Con (t, [])))) s
-
-and parse_fun s = (parse_type_arg -- $$ "->" -- parse_type >> (fn ((a, f), r) => Con (f, [a, r]))) s
-
-and parse_tuple s = (parse_type_single -- Scan.repeat1 ($$ "*" |-- parse_type_single)
-  >> (fn (t, tl) => Tuple (t :: tl))) s;
-
-(*Parse entire type + name*)
-fun parse_function s =
-  let
-    val p = $$ "val" |-- scan_name --| ($$ "=" -- $$ "fn" -- $$ ":")
-    val (name, ty) = p (split s)
-    val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
-    val (typ, _) = Scan.finite stop parse_type ty
-  in (name, typ) end;
-
-(*Create desired output*)
-fun parse_pred s =
-  let
-    val (name, Con ("->", t :: _)) = parse_function s
-  in (name, t) end;
-
-(* Construct Generators and Pretty Printers *)
-
-(*copied from smt_config.ML *)
-fun string_of_bool b = if b then "true" else "false"
-
-fun string_of_ref f r = f (!r) ^ " ref";
-
-val initial_content = Symtab.make
-  [("bool", ("Generator.flip", "Gen_Construction.string_of_bool")),
-  ("option", ("Generator.option (Generator.flip' (1, 3))", "ML_Syntax.print_option")),
-  ("list", ("Generator.list (Generator.flip' (1, 3))", "ML_Syntax.print_list")),
-  ("unit", ("gen_unit", "fn () => \"()\"")),
-  ("int", ("Generator.int", "string_of_int")),
-  ("real", ("Generator.real", "string_of_real")),
-  ("char", ("Generator.char", "fn c => \"#'\" ^ (Char.toString c) ^ \"'\"")),
-  ("string", ("Generator.string (Generator.range (0, 100), Generator.char)", "ML_Syntax.print_string")),
-  ("->", ("Generator.function_lazy", "fn (_, _) => fn _ => \"fn\"")),
-  ("typ", ("Generator.typ 10", "ML_Syntax.print_typ")),
-  ("term", ("Generator.term 10", "ML_Syntax.print_term"))]
-
-structure Data = Theory_Data
-(
-  type T = (string * string) Symtab.table
-  val empty = initial_content
-  val extend = I
-  fun merge data : T = Symtab.merge (K true) data
-)
-
-fun data_of ctxt tycon =
-  (case Symtab.lookup (Data.get (Proof_Context.theory_of ctxt)) tycon of
-    SOME data => data
-  | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon))
-
-val generator_of = fst oo data_of
-val printer_of = snd oo data_of
-
-fun register (ty, data) = Data.map (Symtab.update (ty, data))
-
-(*
-fun remove_gen ty = gen_table := AList.delete (op =) ty (!gen_table);
-*)
-
-fun combine dict [] = dict
-  | combine dict dicts = enclose "(" ")" dict ^ " " ^ enclose "(" ")" (commas dicts)
-
-fun compose_generator _ Var = "Generator.int"
-  | compose_generator ctxt (Con (s, types)) =
-      combine (generator_of ctxt s) (map (compose_generator ctxt) types)
-  | compose_generator ctxt (Tuple t) =
-      let
-        fun tuple_body t = space_implode ""
-          (map (fn (ty, n) => "val (x" ^ string_of_int n ^ ", r" ^ string_of_int n ^ ") = " ^
-          compose_generator ctxt ty ^ " r" ^ string_of_int (n - 1) ^ " ") (t ~~ (1 upto (length t))))
-        fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
-      in
-        "fn r0 => let " ^ tuple_body t ^
-        "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end"
-      end;
-
-fun compose_printer _ Var = "Int.toString"
-  | compose_printer ctxt (Con (s, types)) =
-      combine (printer_of ctxt s) (map (compose_printer ctxt) types)
-  | compose_printer ctxt (Tuple t) =
-      let
-        fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
-        fun tuple_body t = space_implode " ^ \", \" ^ "
-          (map (fn (ty, n) => "(" ^ compose_printer ctxt ty ^ ") x" ^ string_of_int n)
-          (t ~~ (1 upto (length t))))
-      in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end;
-
-(*produce compilable string*)
-fun build_check ctxt name (ty, spec) =
-  "Spec_Check.checkGen (Context.the_local_context ()) ("
-  ^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\""
-  ^ name ^ "\", Property.pred (" ^ spec ^ "));";
-
-(*produce compilable string - non-eqtype functions*)
-(*
-fun safe_check name (ty, spec) =
-  let
-    val default =
-      (case AList.lookup (op =) (!gen_table) "->" of
-        NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"")
-      | SOME entry => entry)
-  in
-   (gen_table :=
-     AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\"")) (!gen_table);
-    build_check name (ty, spec) before
-    gen_table := AList.update (op =) ("->", default) (!gen_table))
-  end;
-*)
-
-end;
-
--- a/src/Tools/Spec_Check/generator.ML	Fri Jul 09 17:58:17 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,235 +0,0 @@
-(*  Title:      Tools/Spec_Check/generator.ML
-    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
-    Author:     Christopher League
-
-Random generators for Isabelle/ML's types.
-*)
-
-signature GENERATOR = sig
-  include BASE_GENERATOR
-  (* text generators *)
-  val char : char gen
-  val charRange : char * char -> char gen
-  val charFrom : string -> char gen
-  val charByType : (char -> bool) -> char gen
-  val string : (int gen * char gen) -> string gen
-  val substring : string gen -> substring gen
-  val cochar : (char, 'b) co
-  val costring : (string, 'b) co
-  val cosubstring : (substring, 'b) co
-  (* integer generators *)
-  val int : int gen
-  val int_pos : int gen
-  val int_neg : int gen
-  val int_nonpos : int gen
-  val int_nonneg : int gen
-  val coint : (int, 'b) co
-  (* real generators *)
-  val real : real gen
-  val real_frac : real gen
-  val real_pos : real gen
-  val real_neg : real gen
-  val real_nonpos : real gen
-  val real_nonneg : real gen
-  val real_finite : real gen
-  (* function generators *)
-  val function_const : 'c * 'b gen -> ('a -> 'b) gen
-  val function_strict : int -> ''a gen * 'b gen -> (''a -> 'b) gen
-  val function_lazy : ''a gen * 'b gen -> (''a -> 'b) gen
-  val unit : unit gen
-  val ref' : 'a gen -> 'a Unsynchronized.ref gen
-  (* more generators *)
-  val term : int -> term gen
-  val typ : int -> typ gen
-
-  val stream : stream
-end
-
-structure Generator : GENERATOR =
-struct
-
-open Base_Generator
-
-val stream = start (new())
-
-type 'a gen = rand -> 'a * rand
-type ('a, 'b) co = 'a -> 'b gen -> 'b gen
-
-(* text *)
-
-type char = Char.char
-type string = String.string
-type substring = Substring.substring
-
-
-val char = map Char.chr (range (0, Char.maxOrd))
-fun charRange (lo, hi) = map Char.chr (range (Char.ord lo, Char.ord hi))
-
-fun charFrom s =
-  choose (Vector.tabulate (String.size s, fn i => lift (String.sub (s, i))))
-
-fun charByType p = filter p char
-
-val string = vector CharVector.tabulate
-
-fun substring gen r =
-  let
-    val (s, r') = gen r
-    val (i, r'') = range (0, String.size s) r'
-    val (j, r''') = range (0, String.size s - i) r''
-  in
-    (Substring.substring (s, i, j), r''')
-  end
-
-fun cochar c =
-  if Char.ord c = 0 then variant 0
-  else variant 1 o cochar (Char.chr (Char.ord c div 2))
-
-fun cosubstring s = Substring.foldr (fn (c,v) => cochar c o v) (variant 0) s
-
-fun costring s = cosubstring (Substring.full s)
-
-(* integers *)
-val digit = charRange (#"0", #"9")
-val nonzero = string (lift 1, charRange (#"1", #"9"))
-fun digits' n = string (range (0, n-1), digit)
-fun digits n = map2 op^ (nonzero, digits' n)
-
-val maxDigits = 64
-val ratio = 49
-
-fun pos_or_neg f r =
-  let
-    val (s, r') = digits maxDigits r
-  in (f (the (Int.fromString s)), r') end
-
-val int_pos = pos_or_neg I
-val int_neg = pos_or_neg Int.~
-val zero = lift 0
-
-val int_nonneg = chooseL' [(1, zero), (ratio, int_pos)]
-val int_nonpos = chooseL' [(1, zero), (ratio, int_neg)]
-val int = chooseL [int_nonneg, int_nonpos]
-
-fun coint n =
-  if n = 0 then variant 0
-  else if n < 0 then variant 1 o coint (~ n)
-  else variant 2 o coint (n div 2)
-
-(* reals *)
-val digits = string (range(1, Real.precision), charRange(#"0", #"9"))
-
-fun real_frac r =
-  let val (s, r') = digits r
-  in (the (Real.fromString s), r') end
-
-val {exp=minExp,...} = Real.toManExp Real.minPos
-val {exp=maxExp,...} = Real.toManExp Real.posInf
-
-val ratio = 99
-
-fun mk r =
-  let
-    val (a, r') = digits r
-    val (b, r'') = digits r'
-    val (e, r''') = range (minExp div 4, maxExp div 4) r''
-    val x = String.concat [a, ".", b, "E", Int.toString e]
-  in
-    (the (Real.fromString x), r''')
-  end
-
-val real_pos = chooseL' (List.map ((pair 1) o lift)
-    [Real.posInf, Real.maxFinite, Real.minPos, Real.minNormalPos] @ [(ratio, mk)])
-
-val real_neg = map Real.~ real_pos
-
-val real_zero = Real.fromInt 0
-val real_nonneg = chooseL' [(1, lift real_zero), (ratio, real_pos)]
-val real_nonpos = chooseL' [(1, lift real_zero), (ratio, real_neg)]
-
-val real = chooseL [real_nonneg, real_nonpos]
-
-val real_finite = filter Real.isFinite real
-
-(*alternate list generator - uses an integer generator to determine list length*)
-fun list' int gen = vector List.tabulate (int, gen);
-
-(* more function generators *)
-
-fun function_const (_, gen2) r =
-  let
-    val (v, r') = gen2 r
-  in (fn _ => v, r') end;
-
-fun function_strict size (gen1, gen2) r =
-  let
-    val (def, r') = gen2 r
-    val (table, r'') = list' (fn s => (size, s)) (zip (gen1, gen2)) r'
-  in (fn v1 => the_default def (AList.lookup (op =) table v1), r'') end;
-
-fun function_lazy (gen1, gen2) r =
-  let
-    val (initial1, r') = gen1 r
-    val (initial2, internal) = gen2 r'
-    val seed = Unsynchronized.ref internal
-    val table = Unsynchronized.ref [(initial1, initial2)]
-    fun new_entry k =
-      let
-        val (new_val, new_seed) = gen2 (!seed)
-        val _ =  seed := new_seed
-        val _ = table := AList.update (op =) (k, new_val) (!table)
-      in new_val end
-  in
-    (fn v1 =>
-      case AList.lookup (op =) (!table) v1 of
-        NONE => new_entry v1
-      | SOME v2 => v2, r')
-  end;
-
-(* unit *)
-
-fun unit r = ((), r);
-
-(* references *)
-
-fun ref' gen r =
-  let val (value, r') = gen r
-  in (Unsynchronized.ref value, r') end;
-
-(* types and terms *)
-
-val sort_string = selectL ["sort1", "sort2", "sort3"];
-val type_string = selectL ["TCon1", "TCon2", "TCon3"];
-val tvar_string = selectL ["a", "b", "c"];
-
-val const_string = selectL ["c1", "c2", "c3"];
-val var_string = selectL ["x", "y", "z"];
-val index = selectL [0, 1, 2, 3];
-val bound_index = selectL [0, 1, 2, 3];
-
-val sort = list (flip' (1, 2)) sort_string;
-
-fun typ n =
-  let
-    fun type' m = map Type (zip (type_string, list (flip' (1, 3)) (typ m)))
-    val tfree = map TFree (zip (tvar_string, sort))
-    val tvar = map TVar (zip (zip (tvar_string, index), sort))
-  in
-    if n = 0 then chooseL [tfree, tvar]
-    else chooseL [type' (n div 2), tfree, tvar]
-  end;
-
-fun term n =
-  let
-    val const = map Const (zip (const_string, typ 10))
-    val free = map Free (zip (var_string, typ 10))
-    val var = map Var (zip (zip (var_string, index), typ 10))
-    val bound = map Bound bound_index
-    fun abs m = map Abs (zip3 (var_string, typ 10, term m))
-    fun app m = map (op $) (zip (term m, term m))
-  in
-    if n = 0 then chooseL [const, free, var, bound]
-    else chooseL [const, free, var, bound, abs (n - 1), app (n div 2)]
-  end;
-
-end
--- a/src/Tools/Spec_Check/output_style.ML	Fri Jul 09 17:58:17 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,113 +0,0 @@
-(*  Title:      Tools/Spec_Check/output_style.ML
-    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
-    Author:     Christopher League
-
-Output styles for presenting Spec_Check's results.
-*)
-
-structure Output_Style : sig end =
-struct
-
-(* perl style *)
-
-val perl_style =
-  Spec_Check.register_style "Perl"
-    (fn ctxt => fn tag =>
-      let
-        val target = Config.get ctxt Spec_Check.gen_target
-        val namew = Config.get ctxt Spec_Check.column_width
-        val sort_examples = Config.get ctxt Spec_Check.sort_examples
-        val show_stats = Config.get ctxt Spec_Check.show_stats
-        val limit = Config.get ctxt Spec_Check.examples
-
-        val resultw = 8
-        val countw = 20
-        val allw = namew + resultw + countw + 2
-
-        val maybe_sort = if sort_examples then sort (int_ord o apply2 size) else I
-
-        fun result ({count = 0, ...}, _) _ = "dubious"
-          | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED"
-          | result ({count, tags}, badobjs) true =
-              if not (null badobjs) then "FAILED"
-              else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious"
-              else "ok"
-
-        fun ratio (0, _) = "(0/0 passed)"
-          | ratio (count, 0) = "(" ^ string_of_int count ^ " passed)"
-          | ratio (count, n) =
-              "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^  " passed)"
-
-        fun update (stats, badobjs) donep =
-          "\r" ^ StringCvt.padRight #"." namew tag ^ "." ^
-          StringCvt.padRight #" " resultw (result (stats, badobjs) donep) ^
-          StringCvt.padRight #" " countw (ratio (#count stats, length badobjs))
-
-        fun status (_, result, (stats, badobjs)) =
-          if Property.failure result then warning (update (stats, badobjs) false) else ()
-
-        fun prtag count (tag, n) first =
-          if String.isPrefix "__" tag then ("", first)
-          else
-             let
-               val ratio = round ((real n / real count) * 100.0)
-             in
-               (((if first then "" else StringCvt.padRight #" " allw "\n") ^
-                 StringCvt.padLeft #" " 3 (string_of_int ratio) ^ "% " ^ tag),
-               false)
-             end
-
-        fun prtags ({count, tags} : Property.stats) =
-          if show_stats then cat_lines (fst (fold_map (prtag count) tags true)) else ""
-
-        fun err badobjs =
-          let
-            fun iter [] _ = ()
-              | iter (e :: es) k =
-                  (warning (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^
-                    StringCvt.padRight #" " resultw (if k > 0 then "" else ":") ^ e);
-                  iter es (k + 1))
-          in
-            iter (maybe_sort (take limit (map_filter I badobjs))) 0
-          end
-
-        fun finish (stats, badobjs) =
-          if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats)
-          else (warning (update (stats, badobjs) true); err badobjs)
-      in
-        {status = status, finish = finish}
-      end)
-
-val _ = Theory.setup perl_style;
-
-
-(* CM style: meshes with CM output; highlighted in sml-mode *)
-
-val cm_style =
-  Spec_Check.register_style "CM"
-    (fn ctxt => fn tag =>
-      let
-        fun pad wd = StringCvt.padLeft #"0" wd o Int.toString
-        val gen_target = Config.get ctxt Spec_Check.gen_target
-        val _ = writeln ("[testing " ^ tag ^ "... ")
-        fun finish ({count, ...} : Property.stats, badobjs) =
-          (case (count, badobjs) of
-            (0, []) => warning ("no valid cases generated]")
-          | (n, []) => writeln (
-                if n >= gen_target then "ok]"
-                else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]")
-          | (_, es) =>
-              let
-                val wd = size (string_of_int (length es))
-                fun each (NONE, _) = ()
-                  | each (SOME e, i) = warning (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e)
-              in
-                (warning "FAILED]"; map each (es ~~ (1 upto (length es))); ())
-              end)
-      in
-        {status = K (), finish = finish}
-      end)
-
-val _ = Theory.setup cm_style;
-
-end
--- a/src/Tools/Spec_Check/property.ML	Fri Jul 09 17:58:17 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,77 +0,0 @@
-(*  Title:      Tools/Spec_Check/property.ML
-    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
-    Author:     Christopher League
-
-Conditional properties that can track argument distribution.
-*)
-
-signature PROPERTY =
-sig
-
-type 'a pred = 'a -> bool
-type 'a prop
-val pred : 'a pred -> 'a prop
-val pred2 : ('a * 'b) pred -> 'b -> 'a  prop
-val implies : 'a pred * 'a prop -> 'a prop
-val ==> : 'a pred * 'a pred -> 'a prop
-val trivial : 'a pred -> 'a prop -> 'a prop
-val classify : 'a pred -> string -> 'a prop -> 'a prop
-val classify' : ('a -> string option) -> 'a prop -> 'a prop
-
-(*Results*)
-type result = bool option
-type stats = { tags : (string * int) list, count : int }
-val test : 'a prop -> 'a * stats -> result * stats
-val stats : stats
-val success : result pred
-val failure : result pred
-
-end
-
-structure Property : PROPERTY =
-struct
-
-type result = bool option
-type stats = { tags : (string * int) list, count : int }
-type 'a pred = 'a -> bool
-type 'a prop = 'a * stats -> result * stats
-
-fun success (SOME true) = true
-  | success _ = false
-
-fun failure (SOME false) = true
-  | failure _ = false
-
-fun apply f x = (case try f x of NONE => SOME false | some => some)
-fun pred f (x,s) = (apply f x, s)
-fun pred2 f z = pred (fn x => f (x, z))
-
-fun implies (cond, p) (x,s) = if cond x then p (x, s) else (NONE, s)
-
-fun ==> (p1, p2) = implies (p1, pred p2)
-
-fun wrap trans p (x,s) =
-  let val (result,s) = p (x,s)
-  in (result, trans (x, result, s)) end
-
-fun classify' f =
-  wrap (fn (x, result, {tags, count}) =>
-    { tags =
-        if is_some result then
-          (case f x of
-            NONE => tags
-          | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags)
-        else tags,
-     count = count })
-
-fun classify p tag = classify' (fn x => if p x then SOME tag else NONE)
-
-fun trivial cond = classify cond "trivial"
-
-fun test p =
-  wrap (fn (_, result, {tags, count}) =>
-    { tags = tags, count = if is_some result then count + 1 else count }) p
-
-val stats = { tags = [], count = 0 }
-
-end
--- a/src/Tools/Spec_Check/random.ML	Fri Jul 09 17:58:17 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(*  Title:      Tools/Spec_Check/random.ML
-    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
-    Author:     Christopher League
-
-Random number engine.
-*)
-
-signature RANDOM =
-sig
-  type rand
-  val new : unit -> rand
-  val range : int * int -> rand -> int * rand
-  val split : rand -> rand * rand
-end
-
-structure Random : RANDOM  =
-struct
-
-type rand = real
-
-val a = 16807.0
-val m = 2147483647.0
-
-fun nextrand seed =
-  let
-    val t = a * seed
-  in
-    t - m * real(floor(t/m))
-  end
-
-val new = nextrand o Time.toReal o Time.now
-
-fun range (min, max) =
-  if min > max then raise Domain (* TODO: raise its own error *)
-  else fn r => (min + (floor(real(max-min+1) * r / m)), nextrand r)
-
-fun split r =
-  let
-    val r = r / a
-    val r0 = real(floor r)
-    val r1 = r - r0
-  in
-    (nextrand r0, nextrand r1)
-  end
-
-end
--- a/src/Tools/Spec_Check/spec_check.ML	Fri Jul 09 17:58:17 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,196 +0,0 @@
-(*  Title:      Tools/Spec_Check/spec_check.ML
-    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
-    Author:     Christopher League
-
-Specification-based testing of ML programs with random values.
-*)
-
-signature SPEC_CHECK =
-sig
-  val gen_target : int Config.T
-  val gen_max : int Config.T
-  val examples : int Config.T
-  val sort_examples : bool Config.T
-  val show_stats : bool Config.T
-  val column_width : int Config.T
-  val style : string Config.T
-
-  type output_style = Proof.context -> string ->
-    {status : string option * Property.result * (Property.stats  * string option list) -> unit,
-     finish: Property.stats * string option list -> unit}
-
-  val register_style : string -> output_style -> theory -> theory
-
-  val checkGen : Proof.context ->
-    'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit
-
-  val check_property : Proof.context -> string -> unit
-end;
-
-structure Spec_Check : SPEC_CHECK =
-struct
-
-(* configurations *)
-
-val gen_target = Attrib.setup_config_int \<^binding>\<open>spec_check_gen_target\<close> (K 100)
-val gen_max = Attrib.setup_config_int \<^binding>\<open>spec_check_gen_max\<close> (K 400)
-val examples = Attrib.setup_config_int \<^binding>\<open>spec_check_examples\<close> (K 5)
-
-val sort_examples = Attrib.setup_config_bool \<^binding>\<open>spec_check_sort_examples\<close> (K true)
-val show_stats = Attrib.setup_config_bool \<^binding>\<open>spec_check_show_stats\<close> (K true)
-val column_width = Attrib.setup_config_int \<^binding>\<open>spec_check_column_width\<close> (K 22)
-val style = Attrib.setup_config_string \<^binding>\<open>spec_check_style\<close> (K "Perl")
-
-type ('a, 'b) reader = 'b -> ('a * 'b) option
-type 'a rep = ('a -> string) option
-
-type output_style = Proof.context -> string ->
-  {status: string option * Property.result * (Property.stats * string option list) -> unit,
-   finish: Property.stats * string option list -> unit}
-
-fun limit ctxt gen = Generator.limit (Config.get ctxt gen_max) gen
-
-structure Style = Theory_Data
-(
-  type T = output_style Symtab.table
-  val empty = Symtab.empty
-  val extend = I
-  fun merge data : T = Symtab.merge (K true) data
-)
-
-fun get_style ctxt =
-  let val name = Config.get ctxt style in
-    (case Symtab.lookup (Style.get (Proof_Context.theory_of ctxt)) name of
-      SOME style => style ctxt
-    | NONE => error ("No style called " ^ quote name ^ " found"))
-  end
-
-fun register_style name style = Style.map (Symtab.update (name, style))
-
-
-(* testing functions *)
-
-fun cpsCheck ctxt s0 shrink (next, show) (tag, prop) =
-  let
-    val apply_show = case show of NONE => (fn _ => NONE) | SOME f => SOME o f
-
-    val {status, finish} = get_style ctxt tag
-    fun status' (obj, result, (stats, badobjs)) =
-      let
-        val badobjs' = if Property.failure result then obj :: badobjs else badobjs
-        val _ = status (apply_show obj, result, (stats, map apply_show badobjs'))
-      in badobjs' end
-
-    fun try_shrink (obj, result, stats') (stats, badobjs) =
-      let
-        fun is_failure s =
-          let val (result, stats') = Property.test prop (s, stats)
-          in if Property.failure result then SOME (s, result, stats') else NONE end
-      in
-        case get_first is_failure (shrink obj) of
-          SOME (obj, result, stats') => try_shrink (obj, result, stats') (stats, badobjs)
-        | NONE => status' (obj, result, (stats', badobjs))
-      end
-
-    fun iter (NONE, (stats, badobjs)) = finish (stats, map apply_show badobjs)
-      | iter (SOME (obj, stream), (stats, badobjs)) =
-        if #count stats >= Config.get ctxt gen_target then
-          finish (stats, map apply_show badobjs)
-        else
-          let
-            val (result, stats') = Property.test prop (obj, stats)
-            val badobjs' = if Property.failure result then
-                try_shrink (obj, result, stats') (stats, badobjs)
-              else
-                status' (obj, result, (stats', badobjs))
-          in iter (next stream, (stats', badobjs')) end
-  in
-    fn stream => iter (next stream, (s0, []))
-  end
-
-fun check' ctxt s0 = cpsCheck ctxt s0 (fn _ => [])
-fun check ctxt = check' ctxt Property.stats
-fun checks ctxt = cpsCheck ctxt Property.stats
-
-fun checkGen ctxt (gen, show) (tag, prop) =
-  check' ctxt {count = 0, tags = [("__GEN", 0)]}
-    (limit ctxt gen, show) (tag, prop) Generator.stream
-
-fun checkGenShrink ctxt shrink (gen, show) (tag, prop) =
-  cpsCheck ctxt {count=0, tags=[("__GEN", 0)]} shrink
-    (limit ctxt gen, show) (tag, prop) Generator.stream
-
-fun checkOne ctxt show (tag, prop) obj =
-  check ctxt (List.getItem, show) (tag, prop) [obj]
-
-(*call the compiler and pass resulting type string to the parser*)
-fun determine_type ctxt s =
-  let
-    val return = Unsynchronized.ref "return"
-    val context : ML_Compiler0.context =
-     {name_space = #name_space ML_Env.context,
-      print_depth = SOME 1000000,
-      here = #here ML_Env.context,
-      print = fn r => return := r,
-      error = #error ML_Env.context}
-    val _ =
-      Context.setmp_generic_context (SOME (Context.Proof ctxt))
-        (fn () =>
-          ML_Compiler0.ML context
-            {line = 0, file = "generated code", verbose = true, debug = false} s) ()
-  in
-    Gen_Construction.parse_pred (! return)
-  end;
-
-(*call the compiler and run the test*)
-fun run_test ctxt s =
-  Context.setmp_generic_context (SOME (Context.Proof ctxt))
-    (fn () =>
-      ML_Compiler0.ML ML_Env.context
-        {line = 0, file = "generated code", verbose = false, debug = false} s) ();
-
-(*split input into tokens*)
-fun input_split s =
-  let
-    fun dot c = c = #"."
-    fun space c = c = #" "
-    val (head, code) = Substring.splitl (not o dot) (Substring.full s)
-  in
-   (String.tokens space (Substring.string head),
-    Substring.string (Substring.dropl dot code))
-  end;
-
-(*create the function from the input*)
-fun make_fun s =
-  let
-    val scan_param = Scan.one (fn s => s <> ";")
-    fun parameters s = Scan.repeat1 scan_param s
-    val p = $$ "ALL" |-- parameters
-    val (split, code) = input_split s
-    val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
-    val (params, _) = Scan.finite stop p split
-  in "fn (" ^ commas params ^ ") => " ^ code end;
-
-(*read input and perform the test*)
-fun gen_check_property check ctxt s =
-  let
-    val func = make_fun s
-    val (_, ty) = determine_type ctxt func
-  in run_test ctxt (check ctxt "Check" (ty, func)) end;
-
-val check_property = gen_check_property Gen_Construction.build_check
-(*val check_property_safe = gen_check_property Gen_Construction.safe_check*)
-
-(*perform test for specification function*)
-fun gen_check_property_f check ctxt s =
-  let
-    val (name, ty) = determine_type ctxt s
-  in run_test ctxt (check ctxt name (ty, s)) end;
-
-val check_property_f = gen_check_property_f Gen_Construction.build_check
-(*val check_property_safe_f_ = gen_check_property_f Gen_Construction.safe_check*)
-
-end;
-
-fun check_property s = Spec_Check.check_property (Context.the_local_context ()) s;
-