--- a/src/HOL/Tools/Nitpick/kodkod.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Sat Apr 24 16:33:01 2010 +0200
@@ -321,7 +321,6 @@
(** Auxiliary functions on ML representation of Kodkod problems **)
-(* 'a fold_expr_funcs -> formula -> 'a -> 'a *)
fun fold_formula (F : 'a fold_expr_funcs) formula =
case formula of
All (ds, f) => fold (fold_decl F) ds #> fold_formula F f
@@ -354,7 +353,6 @@
| False => #formula_func F formula
| True => #formula_func F formula
| FormulaReg _ => #formula_func F formula
-(* 'a fold_expr_funcs -> rel_expr -> 'a -> 'a *)
and fold_rel_expr F rel_expr =
case rel_expr of
RelLet (bs, r) => fold (fold_expr_assign F) bs #> fold_rel_expr F r
@@ -383,7 +381,6 @@
| Rel _ => #rel_expr_func F rel_expr
| Var _ => #rel_expr_func F rel_expr
| RelReg _ => #rel_expr_func F rel_expr
-(* 'a fold_expr_funcs -> int_expr -> 'a -> 'a *)
and fold_int_expr F int_expr =
case int_expr of
Sum (ds, i) => fold (fold_decl F) ds #> fold_int_expr F i
@@ -409,7 +406,6 @@
| Signum i => fold_int_expr F i
| Num _ => #int_expr_func F int_expr
| IntReg _ => #int_expr_func F int_expr
-(* 'a fold_expr_funcs -> decl -> 'a -> 'a *)
and fold_decl F decl =
case decl of
DeclNo (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
@@ -417,7 +413,6 @@
| DeclOne (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
| DeclSome (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
| DeclSet (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
-(* 'a fold_expr_funcs -> expr_assign -> 'a -> 'a *)
and fold_expr_assign F assign =
case assign of
AssignFormulaReg (x, f) => fold_formula F (FormulaReg x) #> fold_formula F f
@@ -429,9 +424,7 @@
tuple_set_func: tuple_set -> 'a -> 'a
}
-(* 'a fold_tuple_funcs -> tuple -> 'a -> 'a *)
fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F
-(* 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a *)
fun fold_tuple_set F tuple_set =
case tuple_set of
TupleUnion (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
@@ -444,23 +437,18 @@
| TupleArea (t1, t2) => fold_tuple F t1 #> fold_tuple F t2
| TupleAtomSeq _ => #tuple_set_func F tuple_set
| TupleSetReg _ => #tuple_set_func F tuple_set
-(* 'a fold_tuple_funcs -> tuple_assign -> 'a -> 'a *)
fun fold_tuple_assign F assign =
case assign of
AssignTuple (x, t) => fold_tuple F (TupleReg x) #> fold_tuple F t
| AssignTupleSet (x, ts) =>
fold_tuple_set F (TupleSetReg x) #> fold_tuple_set F ts
-(* 'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a *)
fun fold_bound expr_F tuple_F (zs, tss) =
fold (fold_rel_expr expr_F) (map (Rel o fst) zs)
#> fold (fold_tuple_set tuple_F) tss
-(* 'a fold_tuple_funcs -> int_bound -> 'a -> 'a *)
fun fold_int_bound F (_, tss) = fold (fold_tuple_set F) tss
-(* int -> int *)
fun max_arity univ_card = floor (Math.ln 2147483647.0
/ Math.ln (Real.fromInt univ_card))
-(* rel_expr -> int *)
fun arity_of_rel_expr (RelLet (_, r)) = arity_of_rel_expr r
| arity_of_rel_expr (RelIf (_, r1, _)) = arity_of_rel_expr r1
| arity_of_rel_expr (Union (r1, _)) = arity_of_rel_expr r1
@@ -487,23 +475,18 @@
| arity_of_rel_expr (Rel (n, _)) = n
| arity_of_rel_expr (Var (n, _)) = n
| arity_of_rel_expr (RelReg (n, _)) = n
-(* rel_expr -> rel_expr -> int *)
and sum_arities_of_rel_exprs r1 r2 = arity_of_rel_expr r1 + arity_of_rel_expr r2
-(* decl -> int *)
and arity_of_decl (DeclNo ((n, _), _)) = n
| arity_of_decl (DeclLone ((n, _), _)) = n
| arity_of_decl (DeclOne ((n, _), _)) = n
| arity_of_decl (DeclSome ((n, _), _)) = n
| arity_of_decl (DeclSet ((n, _), _)) = n
-(* problem -> bool *)
fun is_problem_trivially_false ({formula = False, ...} : problem) = true
| is_problem_trivially_false _ = false
-(* string -> string list *)
val chop_solver = take 2 o space_explode ","
-(* setting list * setting list -> bool *)
fun settings_equivalent ([], []) = true
| settings_equivalent ((key1, value1) :: settings1,
(key2, value2) :: settings2) =
@@ -513,7 +496,6 @@
settings_equivalent (settings1, settings2)
| settings_equivalent _ = false
-(* problem * problem -> bool *)
fun problems_equivalent (p1 : problem, p2 : problem) =
#univ_card p1 = #univ_card p2 andalso
#formula p1 = #formula p2 andalso
@@ -525,16 +507,13 @@
(** Serialization of problem **)
-(* int -> string *)
fun base_name j =
if j < 0 then string_of_int (~j - 1) ^ "'" else string_of_int j
-(* n_ary_index -> string -> string -> string -> string *)
fun n_ary_name (1, j) prefix _ _ = prefix ^ base_name j
| n_ary_name (2, j) _ prefix _ = prefix ^ base_name j
| n_ary_name (n, j) _ _ prefix = prefix ^ string_of_int n ^ "_" ^ base_name j
-(* int -> string *)
fun atom_name j = "A" ^ base_name j
fun atom_seq_name (k, 0) = "u" ^ base_name k
| atom_seq_name (k, j0) = "u" ^ base_name k ^ "@" ^ base_name j0
@@ -542,14 +521,12 @@
fun rel_reg_name j = "$e" ^ base_name j
fun int_reg_name j = "$i" ^ base_name j
-(* n_ary_index -> string *)
fun tuple_name x = n_ary_name x "A" "P" "T"
fun rel_name x = n_ary_name x "s" "r" "m"
fun var_name x = n_ary_name x "S" "R" "M"
fun tuple_reg_name x = n_ary_name x "$A" "$P" "$T"
fun tuple_set_reg_name x = n_ary_name x "$a" "$p" "$t"
-(* string -> string *)
fun inline_comment "" = ""
| inline_comment comment =
" /* " ^ translate_string (fn "\n" => " " | "*" => "* " | s => s) comment ^
@@ -557,10 +534,8 @@
fun block_comment "" = ""
| block_comment comment = prefix_lines "// " comment ^ "\n"
-(* (n_ary_index * string) -> string *)
fun commented_rel_name (x, s) = rel_name x ^ inline_comment s
-(* tuple -> string *)
fun string_for_tuple (Tuple js) = "[" ^ commas (map atom_name js) ^ "]"
| string_for_tuple (TupleIndex x) = tuple_name x
| string_for_tuple (TupleReg x) = tuple_reg_name x
@@ -571,7 +546,6 @@
val prec_TupleProduct = 3
val prec_TupleProject = 4
-(* tuple_set -> int *)
fun precedence_ts (TupleUnion _) = prec_TupleUnion
| precedence_ts (TupleDifference _) = prec_TupleUnion
| precedence_ts (TupleIntersect _) = prec_TupleIntersect
@@ -579,10 +553,8 @@
| precedence_ts (TupleProject _) = prec_TupleProject
| precedence_ts _ = no_prec
-(* tuple_set -> string *)
fun string_for_tuple_set tuple_set =
let
- (* tuple_set -> int -> string *)
fun sub tuple_set outer_prec =
let
val prec = precedence_ts tuple_set
@@ -608,19 +580,16 @@
end
in sub tuple_set 0 end
-(* tuple_assign -> string *)
fun string_for_tuple_assign (AssignTuple (x, t)) =
tuple_reg_name x ^ " := " ^ string_for_tuple t ^ "\n"
| string_for_tuple_assign (AssignTupleSet (x, ts)) =
tuple_set_reg_name x ^ " := " ^ string_for_tuple_set ts ^ "\n"
-(* bound -> string *)
fun string_for_bound (zs, tss) =
"bounds " ^ commas (map commented_rel_name zs) ^ ": " ^
(if length tss = 1 then "" else "[") ^ commas (map string_for_tuple_set tss) ^
(if length tss = 1 then "" else "]") ^ "\n"
-(* int_bound -> string *)
fun int_string_for_bound (opt_n, tss) =
(case opt_n of
SOME n => signed_string_of_int n ^ ": "
@@ -645,7 +614,6 @@
val prec_Join = 18
val prec_BitNot = 19
-(* formula -> int *)
fun precedence_f (All _) = prec_All
| precedence_f (Exist _) = prec_All
| precedence_f (FormulaLet _) = prec_All
@@ -671,7 +639,6 @@
| precedence_f False = no_prec
| precedence_f True = no_prec
| precedence_f (FormulaReg _) = no_prec
-(* rel_expr -> int *)
and precedence_r (RelLet _) = prec_All
| precedence_r (RelIf _) = prec_All
| precedence_r (Union _) = prec_Add
@@ -697,7 +664,6 @@
| precedence_r (Rel _) = no_prec
| precedence_r (Var _) = no_prec
| precedence_r (RelReg _) = no_prec
-(* int_expr -> int *)
and precedence_i (Sum _) = prec_All
| precedence_i (IntLet _) = prec_All
| precedence_i (IntIf _) = prec_All
@@ -721,14 +687,11 @@
| precedence_i (Num _) = no_prec
| precedence_i (IntReg _) = no_prec
-(* (string -> unit) -> problem list -> unit *)
fun write_problem_file out problems =
let
- (* formula -> unit *)
fun out_outmost_f (And (f1, f2)) =
(out_outmost_f f1; out "\n && "; out_outmost_f f2)
| out_outmost_f f = out_f f prec_And
- (* formula -> int -> unit *)
and out_f formula outer_prec =
let
val prec = precedence_f formula
@@ -773,7 +736,6 @@
| FormulaReg j => out (formula_reg_name j));
(if need_parens then out ")" else ())
end
- (* rel_expr -> int -> unit *)
and out_r rel_expr outer_prec =
let
val prec = precedence_r rel_expr
@@ -813,7 +775,6 @@
| RelReg (_, j) => out (rel_reg_name j));
(if need_parens then out ")" else ())
end
- (* int_expr -> int -> unit *)
and out_i int_expr outer_prec =
let
val prec = precedence_i int_expr
@@ -848,11 +809,9 @@
| IntReg j => out (int_reg_name j));
(if need_parens then out ")" else ())
end
- (* decl list -> unit *)
and out_decls [] = ()
| out_decls [d] = out_decl d
| out_decls (d :: ds) = (out_decl d; out ", "; out_decls ds)
- (* decl -> unit *)
and out_decl (DeclNo (x, r)) =
(out (var_name x); out " : no "; out_r r 0)
| out_decl (DeclLone (x, r)) =
@@ -863,22 +822,18 @@
(out (var_name x); out " : some "; out_r r 0)
| out_decl (DeclSet (x, r)) =
(out (var_name x); out " : set "; out_r r 0)
- (* assign_expr list -> unit *)
and out_assigns [] = ()
| out_assigns [b] = out_assign b
| out_assigns (b :: bs) = (out_assign b; out ", "; out_assigns bs)
- (* assign_expr -> unit *)
and out_assign (AssignFormulaReg (j, f)) =
(out (formula_reg_name j); out " := "; out_f f 0)
| out_assign (AssignRelReg ((_, j), r)) =
(out (rel_reg_name j); out " := "; out_r r 0)
| out_assign (AssignIntReg (j, i)) =
(out (int_reg_name j); out " := "; out_i i 0)
- (* int_expr list -> unit *)
and out_columns [] = ()
| out_columns [i] = out_i i 0
| out_columns (i :: is) = (out_i i 0; out ", "; out_columns is)
- (* problem -> unit *)
and out_problem {comment, settings, univ_card, tuple_assigns, bounds,
int_bounds, expr_assigns, formula} =
(out ("\n" ^ block_comment comment ^
@@ -902,12 +857,10 @@
(** Parsing of solution **)
-(* string -> bool *)
fun is_ident_char s =
Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse
s = "_" orelse s = "'" orelse s = "$"
-(* string list -> string list *)
fun strip_blanks [] = []
| strip_blanks (" " :: ss) = strip_blanks ss
| strip_blanks [s1, " "] = [s1]
@@ -918,29 +871,20 @@
strip_blanks (s1 :: s2 :: ss)
| strip_blanks (s :: ss) = s :: strip_blanks ss
-(* (string list -> 'a * string list) -> string list -> 'a list * string list *)
fun scan_non_empty_list scan = scan ::: Scan.repeat ($$ "," |-- scan)
fun scan_list scan = scan_non_empty_list scan || Scan.succeed []
-(* string list -> int * string list *)
val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit)
>> (the o Int.fromString o space_implode "")
-(* string list -> (int * int) * string list *)
val scan_rel_name = $$ "s" |-- scan_nat >> pair 1
|| $$ "r" |-- scan_nat >> pair 2
|| ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat
-(* string list -> int * string list *)
val scan_atom = $$ "A" |-- scan_nat
-(* string list -> int list * string list *)
val scan_tuple = $$ "[" |-- scan_list scan_atom --| $$ "]"
-(* string list -> int list list * string list *)
val scan_tuple_set = $$ "[" |-- scan_list scan_tuple --| $$ "]"
-(* string list -> ((int * int) * int list list) * string list *)
val scan_assignment = (scan_rel_name --| $$ "=") -- scan_tuple_set
-(* string list -> ((int * int) * int list list) list * string list *)
val scan_instance = Scan.this_string "relations:" |--
$$ "{" |-- scan_list scan_assignment --| $$ "}"
-(* string -> raw_bound list *)
val parse_instance =
fst o Scan.finite Symbol.stopper
(Scan.error (!! (fn _ =>
@@ -953,12 +897,10 @@
val outcome_marker = "---OUTCOME---\n"
val instance_marker = "---INSTANCE---\n"
-(* string -> substring -> string *)
fun read_section_body marker =
Substring.string o fst o Substring.position "\n\n"
o Substring.triml (size marker)
-(* substring -> raw_bound list *)
fun read_next_instance s =
let val s = Substring.position instance_marker s |> snd in
if Substring.isEmpty s then
@@ -967,8 +909,6 @@
read_section_body instance_marker s |> parse_instance
end
-(* int -> substring * (int * raw_bound list) list * int list
- -> substring * (int * raw_bound list) list * int list *)
fun read_next_outcomes j (s, ps, js) =
let val (s1, s2) = Substring.position outcome_marker s in
if Substring.isEmpty s2 orelse
@@ -990,8 +930,6 @@
end
end
-(* substring * (int * raw_bound list) list * int list
- -> (int * raw_bound list) list * int list *)
fun read_next_problems (s, ps, js) =
let val s = Substring.position problem_marker s |> snd in
if Substring.isEmpty s then
@@ -1007,7 +945,6 @@
handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems",
"expected number after \"PROBLEM\"")
-(* Path.T -> bool * ((int * raw_bound list) list * int list) *)
fun read_output_file path =
(false, read_next_problems (Substring.full (File.read path), [], [])
|>> rev ||> rev)
@@ -1017,7 +954,6 @@
val created_temp_dir = Unsynchronized.ref false
-(* bool -> string * string *)
fun serial_string_and_temporary_dir_for_overlord overlord =
if overlord then
("", getenv "ISABELLE_HOME_USER")
@@ -1032,14 +968,12 @@
is partly due to the JVM and partly due to the ML "bash" function. *)
val fudge_ms = 250
-(* Time.time option -> int *)
fun milliseconds_until_deadline deadline =
case deadline of
NONE => ~1
| SOME time =>
Int.max (0, Time.toMilliseconds (Time.- (time, Time.now ())) - fudge_ms)
-(* bool -> Time.time option -> int -> int -> problem list -> outcome *)
fun uncached_solve_any_problem overlord deadline max_threads max_solutions
problems =
let
@@ -1051,7 +985,6 @@
(0 upto length problems - 1 ~~ problems)
val triv_js = filter_out (AList.defined (op =) indexed_problems)
(0 upto length problems - 1)
- (* int -> int *)
val reindex = fst o nth indexed_problems
in
if null indexed_problems then
@@ -1060,18 +993,15 @@
let
val (serial_str, temp_dir) =
serial_string_and_temporary_dir_for_overlord overlord
- (* string -> Path.T *)
fun path_for suf =
Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf)
val in_path = path_for "kki"
val in_buf = Unsynchronized.ref Buffer.empty
- (* string -> unit *)
fun out s = Unsynchronized.change in_buf (Buffer.add s)
val out_path = path_for "out"
val err_path = path_for "err"
val _ = write_problem_file out (map snd indexed_problems)
val _ = File.write_buffer in_path (!in_buf)
- (* unit -> unit *)
fun remove_temporary_files () =
if overlord then ()
else List.app (K () o try File.rm) [in_path, out_path, err_path]
@@ -1150,10 +1080,8 @@
Synchronized.var "Kodkod.cached_outcome"
(NONE : ((int * problem list) * outcome) option)
-(* bool -> Time.time option -> int -> int -> problem list -> outcome *)
fun solve_any_problem overlord deadline max_threads max_solutions problems =
let
- (* unit -> outcome *)
fun do_solve () = uncached_solve_any_problem overlord deadline max_threads
max_solutions problems
in
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Sat Apr 24 16:33:01 2010 +0200
@@ -51,8 +51,6 @@
("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],
"s SATISFIABLE", "v ", "s UNSATISFIABLE"))]
-(* string -> sink -> string -> string -> string list -> string list
- -> (string * (unit -> string list)) option *)
fun dynamic_entry_for_external name dev home exec args markers =
case getenv home of
"" => NONE
@@ -74,8 +72,6 @@
if dev = ToFile then out_file else ""] @ markers @
(if dev = ToFile then [out_file] else []) @ args
end)
-(* bool -> bool -> string * sat_solver_info
- -> (string * (unit -> string list)) option *)
fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
if incremental andalso mode = Batch then NONE else SOME (name, K ss)
| dynamic_entry_for_info incremental (name, Internal (JNI, mode, ss)) =
@@ -98,20 +94,15 @@
(name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) =
dynamic_entry_for_external name dev home exec args [m1, m2, m3]
| dynamic_entry_for_info true _ = NONE
-(* bool -> (string * (unit -> string list)) list *)
fun dynamic_list incremental =
map_filter (dynamic_entry_for_info incremental) static_list
-(* bool -> string list *)
val configured_sat_solvers = map fst o dynamic_list
-(* bool -> string *)
val smart_sat_solver_name = fst o hd o dynamic_list
-(* string -> string * string list *)
fun sat_solver_spec name =
let
val dyn_list = dynamic_list false
- (* (string * 'a) list -> string *)
fun enum_solvers solvers =
commas (distinct (op =) (map (quote o fst) solvers))
in
--- a/src/HOL/Tools/Nitpick/minipick.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML Sat Apr 24 16:33:01 2010 +0200
@@ -35,7 +35,6 @@
datatype rep = SRep | RRep
-(* Proof.context -> typ -> unit *)
fun check_type ctxt (Type (@{type_name fun}, Ts)) =
List.app (check_type ctxt) Ts
| check_type ctxt (Type (@{type_name "*"}, Ts)) =
@@ -46,7 +45,6 @@
| check_type ctxt T =
raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
-(* rep -> (typ -> int) -> typ -> int list *)
fun atom_schema_of SRep card (Type (@{type_name fun}, [T1, T2])) =
replicate_list (card T1) (atom_schema_of SRep card T2)
| atom_schema_of RRep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
@@ -56,42 +54,32 @@
| atom_schema_of _ card (Type (@{type_name "*"}, Ts)) =
maps (atom_schema_of SRep card) Ts
| atom_schema_of _ card T = [card T]
-(* rep -> (typ -> int) -> typ -> int *)
val arity_of = length ooo atom_schema_of
-(* (typ -> int) -> typ list -> int -> int *)
fun index_for_bound_var _ [_] 0 = 0
| index_for_bound_var card (_ :: Ts) 0 =
index_for_bound_var card Ts 0 + arity_of SRep card (hd Ts)
| index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1)
-(* (typ -> int) -> rep -> typ list -> int -> rel_expr list *)
fun vars_for_bound_var card R Ts j =
map (curry Var 1) (index_seq (index_for_bound_var card Ts j)
(arity_of R card (nth Ts j)))
-(* (typ -> int) -> rep -> typ list -> int -> rel_expr *)
val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var
-(* rep -> (typ -> int) -> typ list -> typ -> decl list *)
fun decls_for R card Ts T =
map2 (curry DeclOne o pair 1)
(index_seq (index_for_bound_var card (T :: Ts) 0)
(arity_of R card (nth (T :: Ts) 0)))
(map (AtomSeq o rpair 0) (atom_schema_of R card T))
-(* int list -> rel_expr *)
val atom_product = foldl1 Product o map Atom
val false_atom = Atom 0
val true_atom = Atom 1
-(* rel_expr -> formula *)
fun formula_from_atom r = RelEq (r, true_atom)
-(* formula -> rel_expr *)
fun atom_from_formula f = RelIf (f, true_atom, false_atom)
-(* Proof.context -> (typ -> int) -> styp list -> term -> formula *)
fun kodkod_formula_from_term ctxt card frees =
let
- (* typ -> rel_expr -> rel_expr *)
fun R_rep_from_S_rep (T as Type (@{type_name fun}, [T1, @{typ bool}])) r =
let
val jss = atom_schema_of SRep card T1 |> map (rpair 0)
@@ -117,13 +105,11 @@
|> foldl1 Union
end
| R_rep_from_S_rep _ r = r
- (* typ list -> typ -> rel_expr -> rel_expr *)
fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
Comprehension (decls_for SRep card Ts T,
RelEq (R_rep_from_S_rep T
(rel_expr_for_bound_var card SRep (T :: Ts) 0), r))
| S_rep_from_R_rep _ _ r = r
- (* typ list -> term -> formula *)
fun to_F Ts t =
(case t of
@{const Not} $ t1 => Not (to_F Ts t1)
@@ -154,28 +140,26 @@
| Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
| _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
handle SAME () => formula_from_atom (to_R_rep Ts t)
- (* typ list -> term -> rel_expr *)
and to_S_rep Ts t =
- case t of
- Const (@{const_name Pair}, _) $ t1 $ t2 =>
- Product (to_S_rep Ts t1, to_S_rep Ts t2)
- | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name fst}, _) $ t1 =>
- let val fst_arity = arity_of SRep card (fastype_of1 (Ts, t)) in
- Project (to_S_rep Ts t1, num_seq 0 fst_arity)
- end
- | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name snd}, _) $ t1 =>
- let
- val pair_arity = arity_of SRep card (fastype_of1 (Ts, t1))
- val snd_arity = arity_of SRep card (fastype_of1 (Ts, t))
- val fst_arity = pair_arity - snd_arity
- in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end
- | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
- | Bound j => rel_expr_for_bound_var card SRep Ts j
- | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
- (* term -> rel_expr *)
+ case t of
+ Const (@{const_name Pair}, _) $ t1 $ t2 =>
+ Product (to_S_rep Ts t1, to_S_rep Ts t2)
+ | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)
+ | Const (@{const_name fst}, _) $ t1 =>
+ let val fst_arity = arity_of SRep card (fastype_of1 (Ts, t)) in
+ Project (to_S_rep Ts t1, num_seq 0 fst_arity)
+ end
+ | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)
+ | Const (@{const_name snd}, _) $ t1 =>
+ let
+ val pair_arity = arity_of SRep card (fastype_of1 (Ts, t1))
+ val snd_arity = arity_of SRep card (fastype_of1 (Ts, t))
+ val fst_arity = pair_arity - snd_arity
+ in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end
+ | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
+ | Bound j => rel_expr_for_bound_var card SRep Ts j
+ | _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
and to_R_rep Ts t =
(case t of
@{const Not} => to_R_rep Ts (eta_expand Ts t 1)
@@ -282,7 +266,6 @@
handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
in to_F [] end
-(* (typ -> int) -> int -> styp -> bound *)
fun bound_for_free card i (s, T) =
let val js = atom_schema_of RRep card T in
([((length js, i), s)],
@@ -290,7 +273,6 @@
|> tuple_set_from_atom_schema])
end
-(* (typ -> int) -> typ list -> typ -> rel_expr -> formula *)
fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
r =
if body_type T2 = bool_T then
@@ -300,15 +282,12 @@
declarative_axiom_for_rel_expr card (T1 :: Ts) T2
(List.foldl Join r (vars_for_bound_var card SRep (T1 :: Ts) 0)))
| declarative_axiom_for_rel_expr _ _ _ r = One r
-(* (typ -> int) -> bool -> int -> styp -> formula *)
fun declarative_axiom_for_free card i (_, T) =
declarative_axiom_for_rel_expr card [] T (Rel (arity_of RRep card T, i))
-(* Proof.context -> (typ -> int) -> term -> problem *)
fun kodkod_problem_from_term ctxt raw_card t =
let
val thy = ProofContext.theory_of ctxt
- (* typ -> int *)
fun card (Type (@{type_name fun}, [T1, T2])) =
reasonable_power (card T2) (card T1)
| card (Type (@{type_name "*"}, [T1, T2])) = card T1 * card T2
@@ -328,7 +307,6 @@
bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
end
-(* theory -> problem list -> string *)
fun solve_any_kodkod_problem thy problems =
let
val {overlord, ...} = Nitpick_Isar.default_params thy []
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 24 16:33:01 2010 +0200
@@ -141,7 +141,6 @@
type rich_problem = KK.problem * problem_extension
-(* Proof.context -> string -> term list -> Pretty.T list *)
fun pretties_for_formulas _ _ [] = []
| pretties_for_formulas ctxt s ts =
[Pretty.str (s ^ plural_s_for_list ts ^ ":"),
@@ -152,10 +151,8 @@
Pretty.str (if j = 1 then "." else ";")])
(length ts downto 1) ts))]
-(* unit -> string *)
fun install_java_message () =
"Nitpick requires a Java 1.5 virtual machine called \"java\"."
-(* unit -> string *)
fun install_kodkodi_message () =
"Nitpick requires the external Java program Kodkodi. To install it, download \
\the package from Isabelle's web page and add the \"kodkodi-x.y.z\" \
@@ -167,35 +164,27 @@
val max_unsound_delay_ms = 200
val max_unsound_delay_percent = 2
-(* Time.time option -> int *)
fun unsound_delay_for_timeout NONE = max_unsound_delay_ms
| unsound_delay_for_timeout (SOME timeout) =
Int.max (0, Int.min (max_unsound_delay_ms,
Time.toMilliseconds timeout
* max_unsound_delay_percent div 100))
-(* Time.time option -> bool *)
fun passed_deadline NONE = false
| passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS
-(* ('a * bool option) list -> bool *)
fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
val syntactic_sorts =
@{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
@{sort number}
-(* typ -> bool *)
fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
subset (op =) (S, syntactic_sorts)
| has_tfree_syntactic_sort _ = false
-(* term -> bool *)
val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort)
-(* (unit -> string) -> Pretty.T *)
fun plazy f = Pretty.blk (0, pstrs (f ()))
-(* Time.time -> Proof.state -> params -> bool -> int -> int -> int
- -> (term * term) list -> term list -> term -> string * Proof.state *)
fun pick_them_nits_in_term deadline state (params : params) auto i n step
subst orig_assm_ts orig_t =
let
@@ -218,7 +207,6 @@
check_genuine, batch_size, ...} =
params
val state_ref = Unsynchronized.ref state
- (* Pretty.T -> unit *)
val pprint =
if auto then
Unsynchronized.change state_ref o Proof.goal_message o K
@@ -227,22 +215,17 @@
else
(fn s => (priority s; if debug then tracing s else ()))
o Pretty.string_of
- (* (unit -> Pretty.T) -> unit *)
fun pprint_m f = () |> not auto ? pprint o f
fun pprint_v f = () |> verbose ? pprint o f
fun pprint_d f = () |> debug ? pprint o f
- (* string -> unit *)
val print = pprint o curry Pretty.blk 0 o pstrs
val print_g = pprint o Pretty.str
- (* (unit -> string) -> unit *)
val print_m = pprint_m o K o plazy
val print_v = pprint_v o K o plazy
- (* unit -> unit *)
fun check_deadline () =
if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut
else ()
- (* unit -> 'a *)
fun do_interrupted () =
if passed_deadline deadline then raise TimeLimit.TimeOut
else raise Interrupt
@@ -307,7 +290,6 @@
val got_all_user_axioms =
got_all_mono_user_axioms andalso no_poly_user_axioms
- (* styp * (bool * bool) -> unit *)
fun print_wf (x, (gfp, wf)) =
pprint (Pretty.blk (0,
pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"")
@@ -344,7 +326,6 @@
*)
val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
- (* typ list -> string -> string *)
fun monotonicity_message Ts extra =
let val ss = map (quote o string_for_type ctxt) Ts in
"The type" ^ plural_s_for_list ss ^ " " ^
@@ -355,7 +336,6 @@
(if length ss = 1 then "is" else "are") ^ " considered monotonic") ^
". " ^ extra
end
- (* typ -> bool *)
fun is_type_fundamentally_monotonic T =
(is_datatype thy stds T andalso not (is_quot_type thy T) andalso
(not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
@@ -416,7 +396,6 @@
()
(* This detection code is an ugly hack. Fortunately, it is used only to
provide a hint to the user. *)
- (* string * (Rule_Cases.T * bool) -> bool *)
fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
not (null fixes) andalso
exists (String.isSuffix ".hyps" o fst) assumes andalso
@@ -464,7 +443,6 @@
val too_big_scopes = Unsynchronized.ref []
- (* bool -> scope -> rich_problem option *)
fun problem_for_scope unsound
(scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) =
let
@@ -480,7 +458,6 @@
(Typtab.dest ofs)
*)
val all_exact = forall (is_exact_type datatypes true) all_Ts
- (* nut list -> rep NameTable.table -> nut list * rep NameTable.table *)
val repify_consts = choose_reps_for_consts scope all_exact
val main_j0 = offset_of_type ofs bool_T
val (nat_card, nat_j0) = spec_of_type scope nat_T
@@ -604,15 +581,12 @@
val checked_problems = Unsynchronized.ref (SOME [])
val met_potential = Unsynchronized.ref 0
- (* rich_problem list -> int list -> unit *)
fun update_checked_problems problems =
List.app (Unsynchronized.change checked_problems o Option.map o cons
o nth problems)
- (* string -> unit *)
fun show_kodkod_warning "" = ()
| show_kodkod_warning s = print_m (fn () => "Kodkod warning: " ^ s ^ ".")
- (* bool -> KK.raw_bound list -> problem_extension -> bool * bool option *)
fun print_and_check_model genuine bounds
({free_names, sel_names, nonsel_names, rel_table, scope, ...}
: problem_extension) =
@@ -719,14 +693,11 @@
NONE)
|> pair genuine_means_genuine
end
- (* bool * int * int * int -> bool -> rich_problem list
- -> bool * int * int * int *)
fun solve_any_problem (found_really_genuine, max_potential, max_genuine,
donno) first_time problems =
let
val max_potential = Int.max (0, max_potential)
val max_genuine = Int.max (0, max_genuine)
- (* bool -> int * KK.raw_bound list -> bool * bool option *)
fun print_and_check genuine (j, bounds) =
print_and_check_model genuine bounds (snd (nth problems j))
val max_solutions = max_potential + max_genuine
@@ -826,8 +797,6 @@
(found_really_genuine, max_potential, max_genuine, donno + 1))
end
- (* int -> int -> scope list -> bool * int * int * int
- -> bool * int * int * int *)
fun run_batch j n scopes (found_really_genuine, max_potential, max_genuine,
donno) =
let
@@ -855,8 +824,6 @@
(length scopes downto 1) scopes))])
else
()
- (* scope * bool -> rich_problem list * bool
- -> rich_problem list * bool *)
fun add_problem_for_scope (scope, unsound) (problems, donno) =
(check_deadline ();
case problem_for_scope unsound scope of
@@ -902,13 +869,10 @@
donno) true (rev problems)
end
- (* rich_problem list -> scope -> int *)
fun scope_count (problems : rich_problem list) scope =
length (filter (curry scopes_equivalent scope o #scope o snd) problems)
- (* string -> string *)
fun excipit did_so_and_so =
let
- (* rich_problem list -> rich_problem list *)
val do_filter =
if !met_potential = max_potential then filter_out (#unsound o snd)
else I
@@ -930,7 +894,6 @@
"") ^ "."
end
- (* int -> int -> scope list -> bool * int * int * int -> KK.outcome *)
fun run_batches _ _ []
(found_really_genuine, max_potential, max_genuine, donno) =
if donno > 0 andalso max_genuine > 0 then
@@ -996,8 +959,6 @@
else
error "Nitpick was interrupted."
-(* Proof.state -> params -> bool -> int -> int -> int -> (term * term) list
- -> term list -> term -> string * Proof.state *)
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
step subst orig_assm_ts orig_t =
if getenv "KODKODI" = "" then
@@ -1016,12 +977,10 @@
else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
end
-(* string list -> term -> bool *)
fun is_fixed_equation fixes
(Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
member (op =) fixes s
| is_fixed_equation _ _ = false
-(* Proof.context -> term list * term -> (term * term) list * term list * term *)
fun extract_fixed_frees ctxt (assms, t) =
let
val fixes = Variable.fixes_of ctxt |> map snd
@@ -1030,7 +989,6 @@
|>> map Logic.dest_equals
in (subst, other_assms, subst_atomic subst t) end
-(* Proof.state -> params -> bool -> int -> int -> string * Proof.state *)
fun pick_nits_in_subgoal state params auto i step =
let
val ctxt = Proof.context_of state
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Apr 24 16:33:01 2010 +0200
@@ -293,31 +293,24 @@
(** Constant/type information and term/type manipulation **)
-(* int -> string *)
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
-(* Proof.context -> typ -> string *)
fun quot_normal_name_for_type ctxt T =
quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T)
-(* string -> string * string *)
val strip_first_name_sep =
Substring.full #> Substring.position name_sep ##> Substring.triml 1
#> pairself Substring.string
-(* string -> string *)
fun original_name s =
if String.isPrefix nitpick_prefix s then
case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2
else
s
-(* term * term -> term *)
fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
| s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t
| s_betapply p = betapply p
-(* term * term list -> term *)
val s_betapplys = Library.foldl s_betapply
-(* term * term -> term *)
fun s_conj (t1, @{const True}) = t1
| s_conj (@{const True}, t2) = t2
| s_conj (t1, t2) =
@@ -329,18 +322,15 @@
if t1 = @{const True} orelse t2 = @{const True} then @{const True}
else HOLogic.mk_disj (t1, t2)
-(* term -> term -> term list *)
fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
| strip_connective _ t = [t]
-(* term -> term list * term *)
fun strip_any_connective (t as (t0 $ _ $ _)) =
if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
(strip_connective t0 t, t0)
else
([t], @{const Not})
| strip_any_connective t = ([t], @{const Not})
-(* term -> term list *)
val conjuncts_of = strip_connective @{const "op &"}
val disjuncts_of = strip_connective @{const "op |"}
@@ -415,7 +405,6 @@
(@{const_name minus_class.minus}, 2),
(@{const_name ord_class.less_eq}, 2)]
-(* typ -> typ *)
fun unarize_type @{typ "unsigned_bit word"} = nat_T
| unarize_type @{typ "signed_bit word"} = int_T
| unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
@@ -436,44 +425,33 @@
| uniterize_type T = T
val uniterize_unarize_unbox_etc_type = uniterize_type o unarize_unbox_etc_type
-(* Proof.context -> typ -> string *)
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_unbox_etc_type
-(* string -> string -> string *)
val prefix_name = Long_Name.qualify o Long_Name.base_name
-(* string -> string *)
fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
-(* string -> term -> term *)
val prefix_abs_vars = Term.map_abs_vars o prefix_name
-(* string -> string *)
fun short_name s =
case space_explode name_sep s of
[_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
| ss => map shortest_name ss |> space_implode "_"
-(* typ -> typ *)
fun shorten_names_in_type (Type (s, Ts)) =
Type (short_name s, map shorten_names_in_type Ts)
| shorten_names_in_type T = T
-(* term -> term *)
val shorten_names_in_term =
map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t)
#> map_types shorten_names_in_type
-(* theory -> typ * typ -> bool *)
fun strict_type_match thy (T1, T2) =
(Sign.typ_match thy (T2, T1) Vartab.empty; true)
handle Type.TYPE_MATCH => false
fun type_match thy = strict_type_match thy o pairself unarize_unbox_etc_type
-(* theory -> styp * styp -> bool *)
fun const_match thy ((s1, T1), (s2, T2)) =
s1 = s2 andalso type_match thy (T1, T2)
-(* theory -> term * term -> bool *)
fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
| term_match thy (Free (s1, T1), Free (s2, T2)) =
const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
| term_match _ (t1, t2) = t1 aconv t2
-(* typ -> term -> term -> term *)
fun frac_from_term_pair T t1 t2 =
case snd (HOLogic.dest_number t1) of
0 => HOLogic.mk_number T 0
@@ -482,7 +460,6 @@
| n2 => Const (@{const_name divide}, T --> T --> T)
$ HOLogic.mk_number T n1 $ HOLogic.mk_number T n2
-(* typ -> bool *)
fun is_TFree (TFree _) = true
| is_TFree _ = false
fun is_higher_order_type (Type (@{type_name fun}, _)) = true
@@ -508,50 +485,41 @@
| is_word_type _ = false
val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type
val is_record_type = not o null o Record.dest_recTs
-(* theory -> typ -> bool *)
fun is_frac_type thy (Type (s, [])) =
not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
| is_frac_type _ _ = false
fun is_number_type thy = is_integer_like_type orf is_frac_type thy
-(* bool -> styp -> typ *)
fun iterator_type_for_const gfp (s, T) =
Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
binder_types T)
-(* typ -> styp *)
fun const_for_iterator_type (Type (s, Ts)) =
(strip_first_name_sep s |> snd, Ts ---> bool_T)
| const_for_iterator_type T =
raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
-(* int -> typ -> typ list * typ *)
fun strip_n_binders 0 T = ([], T)
| strip_n_binders n (Type (@{type_name fun}, [T1, T2])) =
strip_n_binders (n - 1) T2 |>> cons T1
| strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
strip_n_binders n (Type (@{type_name fun}, Ts))
| strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
-(* typ -> typ *)
val nth_range_type = snd oo strip_n_binders
-(* typ -> int *)
fun num_factors_in_type (Type (@{type_name "*"}, [T1, T2])) =
fold (Integer.add o num_factors_in_type) [T1, T2] 0
| num_factors_in_type _ = 1
fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
1 + num_binder_types T2
| num_binder_types _ = 0
-(* typ -> typ list *)
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
fun maybe_curried_binder_types T =
(if is_pair_type (body_type T) then binder_types else curried_binder_types) T
-(* typ -> term list -> term *)
fun mk_flat_tuple _ [t] = t
| mk_flat_tuple (Type (@{type_name "*"}, [T1, T2])) (t :: ts) =
HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
| mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
-(* int -> term -> term list *)
fun dest_n_tuple 1 t = [t]
| dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
@@ -560,7 +528,6 @@
set_def: thm option, prop_of_Rep: thm, set_name: string,
Abs_inverse: thm option, Rep_inverse: thm option}
-(* theory -> string -> typedef_info *)
fun typedef_info thy s =
if is_frac_type thy (Type (s, [])) then
SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
@@ -578,21 +545,17 @@
Rep_inverse = SOME Rep_inverse}
| _ => NONE
-(* theory -> string -> bool *)
val is_typedef = is_some oo typedef_info
val is_real_datatype = is_some oo Datatype.get_info
-(* theory -> (typ option * bool) list -> typ -> bool *)
fun is_standard_datatype thy = the oo triple_lookup (type_match thy)
(* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
e.g., by adding a field to "Datatype_Aux.info". *)
-(* theory -> (typ option * bool) list -> string -> bool *)
fun is_basic_datatype thy stds s =
member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
@{type_name int}, "Code_Numeral.code_numeral"] s orelse
(s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
-(* theory -> typ -> typ -> typ -> typ *)
fun instantiate_type thy T1 T1' T2 =
Same.commit (Envir.subst_type_same
(Sign.typ_match thy (T1, T1') Vartab.empty)) T2
@@ -601,20 +564,16 @@
fun varify_and_instantiate_type thy T1 T1' T2 =
instantiate_type thy (Logic.varifyT_global T1) T1' (Logic.varifyT_global T2)
-(* theory -> typ -> typ -> styp *)
fun repair_constr_type thy body_T' T =
varify_and_instantiate_type thy (body_type T) body_T' T
-(* string -> (string * string) list -> theory -> theory *)
fun register_frac_type frac_s ersaetze thy =
let
val {frac_types, codatatypes} = Data.get thy
val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
-(* string -> theory -> theory *)
fun unregister_frac_type frac_s = register_frac_type frac_s []
-(* typ -> string -> styp list -> theory -> theory *)
fun register_codatatype co_T case_name constr_xs thy =
let
val {frac_types, codatatypes} = Data.get thy
@@ -630,10 +589,8 @@
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
codatatypes
in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
-(* typ -> theory -> theory *)
fun unregister_codatatype co_T = register_codatatype co_T "" []
-(* theory -> typ -> bool *)
fun is_quot_type thy (Type (s, _)) =
is_some (Quotient_Info.quotdata_lookup_raw thy s)
| is_quot_type _ _ = false
@@ -670,32 +627,26 @@
end
| NONE => false)
| is_univ_typedef _ _ = false
-(* theory -> (typ option * bool) list -> typ -> bool *)
fun is_datatype thy stds (T as Type (s, _)) =
(is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
| is_datatype _ _ _ = false
-(* theory -> typ -> (string * typ) list * (string * typ) *)
fun all_record_fields thy T =
let val (recs, more) = Record.get_extT_fields thy T in
recs @ more :: all_record_fields thy (snd more)
end
handle TYPE _ => []
-(* styp -> bool *)
fun is_record_constr (s, T) =
String.isSuffix Record.extN s andalso
let val dataT = body_type T in
is_record_type dataT andalso
s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN
end
-(* theory -> typ -> int *)
val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
-(* theory -> string -> typ -> int *)
fun no_of_record_field thy s T1 =
find_index (curry (op =) s o fst)
(Record.get_extT_fields thy T1 ||> single |> op @)
-(* theory -> styp -> bool *)
fun is_record_get thy (s, Type (@{type_name fun}, [T1, _])) =
exists (curry (op =) s o fst) (all_record_fields thy T1)
| is_record_get _ _ = false
@@ -714,7 +665,6 @@
SOME {Rep_name, ...} => s = Rep_name
| NONE => false)
| is_rep_fun _ _ = false
-(* Proof.context -> styp -> bool *)
fun is_quot_abs_fun ctxt
(x as (_, Type (@{type_name fun}, [_, Type (s', _)]))) =
(try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
@@ -726,19 +676,16 @@
= SOME (Const x))
| is_quot_rep_fun _ _ = false
-(* theory -> styp -> styp *)
fun mate_of_rep_fun thy (x as (_, Type (@{type_name fun},
[T1 as Type (s', _), T2]))) =
(case typedef_info thy s' of
SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
| NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
| mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
-(* theory -> typ -> typ *)
fun rep_type_for_quot_type thy (T as Type (s, _)) =
let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in
instantiate_type thy qtyp T rtyp
end
-(* theory -> typ -> term *)
fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
let
val {qtyp, equiv_rel, ...} = Quotient_Info.quotdata_lookup thy s
@@ -747,7 +694,6 @@
| equiv_relation_for_quot_type _ T =
raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
-(* theory -> styp -> bool *)
fun is_coconstr thy (s, T) =
let
val {codatatypes, ...} = Data.get thy
@@ -770,19 +716,16 @@
fun is_stale_constr thy (x as (_, T)) =
is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
not (is_coconstr thy x)
-(* theory -> (typ option * bool) list -> styp -> bool *)
fun is_constr thy stds (x as (_, T)) =
is_constr_like thy x andalso
not (is_basic_datatype thy stds
(fst (dest_Type (unarize_type (body_type T))))) andalso
not (is_stale_constr thy x)
-(* string -> bool *)
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
val is_sel_like_and_no_discr =
String.isPrefix sel_prefix orf
(member (op =) [@{const_name fst}, @{const_name snd}])
-(* boxability -> boxability *)
fun in_fun_lhs_for InConstr = InSel
| in_fun_lhs_for _ = InFunLHS
fun in_fun_rhs_for InConstr = InConstr
@@ -790,7 +733,6 @@
| in_fun_rhs_for InFunRHS1 = InFunRHS2
| in_fun_rhs_for _ = InFunRHS1
-(* hol_context -> boxability -> typ -> bool *)
fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
case T of
Type (@{type_name fun}, _) =>
@@ -802,12 +744,10 @@
exists (is_boxing_worth_it hol_ctxt InPair)
(map (box_type hol_ctxt InPair) Ts))
| _ => false
-(* hol_context -> boxability -> string * typ list -> string *)
and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy z =
case triple_lookup (type_match thy) boxes (Type z) of
SOME (SOME box_me) => box_me
| _ => is_boxing_worth_it hol_ctxt boxy (Type z)
-(* hol_context -> boxability -> typ -> typ *)
and box_type hol_ctxt boxy T =
case T of
Type (z as (@{type_name fun}, [T1, T2])) =>
@@ -829,37 +769,29 @@
else InPair)) Ts)
| _ => T
-(* typ -> typ *)
fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
| binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
| binarize_nat_and_int_in_type (Type (s, Ts)) =
Type (s, map binarize_nat_and_int_in_type Ts)
| binarize_nat_and_int_in_type T = T
-(* term -> term *)
val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
-(* styp -> styp *)
fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
-(* typ -> int *)
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T)
-(* string -> int -> string *)
fun nth_sel_name_for_constr_name s n =
if s = @{const_name Pair} then
if n = 0 then @{const_name fst} else @{const_name snd}
else
sel_prefix_for n ^ s
-(* styp -> int -> styp *)
fun nth_sel_for_constr x ~1 = discr_for_constr x
| nth_sel_for_constr (s, T) n =
(nth_sel_name_for_constr_name s n,
body_type T --> nth (maybe_curried_binder_types T) n)
-(* hol_context -> bool -> styp -> int -> styp *)
fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize =
apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel)
oo nth_sel_for_constr
-(* string -> int *)
fun sel_no_from_name s =
if String.isPrefix discr_prefix s then
~1
@@ -870,15 +802,12 @@
else
0
-(* term -> term *)
val close_form =
let
- (* (indexname * typ) list -> (indexname * typ) list -> term -> term *)
fun close_up zs zs' =
fold (fn (z as ((s, _), T)) => fn t' =>
Term.all T $ Abs (s, T, abstract_over (Var z, t')))
(take (length zs' - length zs) zs')
- (* (indexname * typ) list -> term -> term *)
fun aux zs (@{const "==>"} $ t1 $ t2) =
let val zs' = Term.add_vars t1 zs in
close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
@@ -886,7 +815,6 @@
| aux zs t = close_up zs (Term.add_vars t zs) t
in aux [] end
-(* typ list -> term -> int -> term *)
fun eta_expand _ t 0 = t
| eta_expand Ts (Abs (s, T, t')) n =
Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
@@ -895,7 +823,6 @@
(List.take (binder_types (fastype_of1 (Ts, t)), n))
(list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
-(* term -> term *)
fun extensionalize t =
case t of
(t0 as @{const Trueprop}) $ t1 => t0 $ extensionalize t1
@@ -905,17 +832,14 @@
end
| _ => t
-(* typ -> term list -> term *)
fun distinctness_formula T =
all_distinct_unordered_pairs_of
#> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))
#> List.foldr (s_conj o swap) @{const True}
-(* typ -> term *)
fun zero_const T = Const (@{const_name zero_class.zero}, T)
fun suc_const T = Const (@{const_name Suc}, T --> T)
-(* hol_context -> typ -> styp list *)
fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
(T as Type (s, Ts)) =
(case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
@@ -952,7 +876,6 @@
else
[])
| uncached_datatype_constrs _ _ = []
-(* hol_context -> typ -> styp list *)
fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
case AList.lookup (op =) (!constr_cache) T of
SOME xs => xs
@@ -960,18 +883,14 @@
let val xs = uncached_datatype_constrs hol_ctxt T in
(Unsynchronized.change constr_cache (cons (T, xs)); xs)
end
-(* hol_context -> bool -> typ -> styp list *)
fun binarized_and_boxed_datatype_constrs hol_ctxt binarize =
map (apsnd ((binarize ? binarize_nat_and_int_in_type)
o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
-(* hol_context -> typ -> int *)
val num_datatype_constrs = length oo datatype_constrs
-(* string -> string *)
fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
| constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
| constr_name_for_sel_like s' = original_name s'
-(* hol_context -> bool -> styp -> styp *)
fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') =
let val s = constr_name_for_sel_like s' in
AList.lookup (op =)
@@ -980,7 +899,6 @@
|> the |> pair s
end
-(* hol_context -> styp -> term *)
fun discr_term_for_constr hol_ctxt (x as (s, T)) =
let val dataT = body_type T in
if s = @{const_name Suc} then
@@ -991,7 +909,6 @@
else
Abs (Name.uu, dataT, @{const True})
end
-(* hol_context -> styp -> term -> term *)
fun discriminate_value (hol_ctxt as {thy, ...}) x t =
case head_of t of
Const x' =>
@@ -1000,7 +917,6 @@
else betapply (discr_term_for_constr hol_ctxt x, t)
| _ => betapply (discr_term_for_constr hol_ctxt x, t)
-(* theory -> (typ option * bool) list -> styp -> term -> term *)
fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n =
let val (arg_Ts, dataT) = strip_type T in
if dataT = nat_T andalso is_standard_datatype thy stds nat_T then
@@ -1009,7 +925,6 @@
Const (nth_sel_for_constr x n)
else
let
- (* int -> typ -> int * term *)
fun aux m (Type (@{type_name "*"}, [T1, T2])) =
let
val (m, t1) = aux m T1
@@ -1022,7 +937,6 @@
(List.take (arg_Ts, n)) 0
in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
end
-(* theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term *)
fun select_nth_constr_arg thy stds x t n res_T =
(case strip_comb t of
(Const x', args) =>
@@ -1032,7 +946,6 @@
| _ => raise SAME())
handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
-(* theory -> (typ option * bool) list -> styp -> term list -> term *)
fun construct_value _ _ x [] = Const x
| construct_value thy stds (x as (s, _)) args =
let val args = map Envir.eta_contract args in
@@ -1049,7 +962,6 @@
| _ => list_comb (Const x, args)
end
-(* hol_context -> typ -> term -> term *)
fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
(case head_of t of
Const x => if is_constr_like thy x then t else raise SAME ()
@@ -1069,17 +981,14 @@
(index_seq 0 (length arg_Ts)) arg_Ts)
end
-(* (term -> term) -> int -> term -> term *)
fun coerce_bound_no f j t =
case t of
t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
| Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
| Bound j' => if j' = j then f t else t
| _ => t
-(* hol_context -> typ -> typ -> term -> term *)
fun coerce_bound_0_in_term hol_ctxt new_T old_T =
old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
-(* hol_context -> typ list -> typ -> typ -> term -> term *)
and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
if old_T = new_T then
t
@@ -1124,7 +1033,6 @@
raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
| _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
-(* (typ * int) list -> typ -> int *)
fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
| card_of_type assigns (Type (@{type_name "*"}, [T1, T2])) =
@@ -1138,7 +1046,6 @@
SOME k => k
| NONE => if T = @{typ bisim_iterator} then 0
else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
-(* int -> (typ * int) list -> typ -> int *)
fun bounded_card_of_type max default_card assigns
(Type (@{type_name fun}, [T1, T2])) =
let
@@ -1161,11 +1068,9 @@
card_of_type assigns T
handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
default_card)
-(* hol_context -> typ list -> int -> (typ * int) list -> typ -> int *)
fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
assigns T =
let
- (* typ list -> typ -> int *)
fun aux avoid T =
(if member (op =) avoid T then
0
@@ -1214,47 +1119,36 @@
val small_type_max_card = 5
-(* hol_context -> typ -> bool *)
fun is_finite_type hol_ctxt T =
bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0
-(* hol_context -> typ -> bool *)
fun is_small_finite_type hol_ctxt T =
let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in
n > 0 andalso n <= small_type_max_card
end
-(* term -> bool *)
fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
| is_ground_term (Const _) = true
| is_ground_term _ = false
-(* term -> word -> word *)
fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
| hashw_term (Const (s, _)) = hashw_string (s, 0w0)
| hashw_term _ = 0w0
-(* term -> int *)
val hash_term = Word.toInt o hashw_term
-(* term list -> (indexname * typ) list *)
fun special_bounds ts =
fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
-(* indexname * typ -> term -> term *)
fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
-(* theory -> string -> bool *)
fun is_funky_typedef_name thy s =
member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
@{type_name int}] s orelse
is_frac_type thy (Type (s, []))
-(* theory -> typ -> bool *)
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
| is_funky_typedef _ _ = false
-(* term -> bool *)
fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
$ Const (@{const_name TYPE}, _)) = true
| is_arity_type_axiom _ = false
-(* theory -> bool -> term -> bool *)
fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
is_typedef_axiom thy boring t2
| is_typedef_axiom thy boring
@@ -1263,7 +1157,6 @@
$ Const _ $ _)) =
boring <> is_funky_typedef_name thy s andalso is_typedef thy s
| is_typedef_axiom _ _ _ = false
-(* term -> bool *)
val is_class_axiom =
Logic.strip_horn #> swap #> op :: #> forall (can Logic.dest_of_class)
@@ -1271,7 +1164,6 @@
typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
Typedef axioms are uninteresting to Nitpick, because it can retrieve them
using "typedef_info". *)
-(* theory -> (string * term) list -> string list -> term list * term list *)
fun partition_axioms_by_definitionality thy axioms def_names =
let
val axioms = sort (fast_string_ord o pairself fst) axioms
@@ -1284,15 +1176,12 @@
(* Ideally we would check against "Complex_Main", not "Refute", but any theory
will do as long as it contains all the "axioms" and "axiomatization"
commands. *)
-(* theory -> bool *)
fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
-(* term -> bool *)
val is_trivial_definition =
the_default false o try (op aconv o Logic.dest_equals)
val is_plain_definition =
let
- (* term -> bool *)
fun do_lhs t1 =
case strip_comb t1 of
(Const _, args) =>
@@ -1304,10 +1193,8 @@
| do_eq _ = false
in do_eq end
-(* theory -> (term * term) list -> term list * term list * term list *)
fun all_axioms_of thy subst =
let
- (* theory list -> term list *)
val axioms_of_thys =
maps Thm.axioms_of
#> map (apsnd (subst_atomic subst o prop_of))
@@ -1336,7 +1223,6 @@
user_defs @ built_in_defs
in (defs, built_in_nondefs, user_nondefs) end
-(* theory -> (typ option * bool) list -> bool -> styp -> int option *)
fun arity_of_built_in_const thy stds fast_descrs (s, T) =
if s = @{const_name If} then
if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
@@ -1364,12 +1250,10 @@
else
NONE
end
-(* theory -> (typ option * bool) list -> bool -> styp -> bool *)
val is_built_in_const = is_some oooo arity_of_built_in_const
(* This function is designed to work for both real definition axioms and
simplification rules (equational specifications). *)
-(* term -> term *)
fun term_under_def t =
case t of
@{const "==>"} $ _ $ t2 => term_under_def t2
@@ -1383,8 +1267,6 @@
(* Here we crucially rely on "Refute.specialize_type" performing a preorder
traversal of the term, without which the wrong occurrence of a constant could
be matched in the face of overloading. *)
-(* theory -> (typ option * bool) list -> bool -> const_table -> styp
- -> term list *)
fun def_props_for_const thy stds fast_descrs table (x as (s, _)) =
if is_built_in_const thy stds fast_descrs x then
[]
@@ -1393,10 +1275,8 @@
|> map_filter (try (Refute.specialize_type thy x))
|> filter (curry (op =) (Const x) o term_under_def)
-(* term -> term option *)
fun normalized_rhs_of t =
let
- (* term option -> term option *)
fun aux (v as Var _) (SOME t) = SOME (lambda v t)
| aux (c as Const (@{const_name TYPE}, _)) (SOME t) = SOME (lambda c t)
| aux _ _ = NONE
@@ -1409,7 +1289,6 @@
val args = strip_comb lhs |> snd
in fold_rev aux args (SOME rhs) end
-(* theory -> const_table -> styp -> term option *)
fun def_of_const thy table (x as (s, _)) =
if is_built_in_const thy [(NONE, false)] false x orelse
original_name s <> s then
@@ -1419,16 +1298,13 @@
|> normalized_rhs_of |> Option.map (prefix_abs_vars s)
handle List.Empty => NONE
-(* term -> fixpoint_kind *)
fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
| fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
| fixpoint_kind_of_rhs (Const (@{const_name gfp}, _) $ Abs _) = Gfp
| fixpoint_kind_of_rhs _ = NoFp
-(* theory -> const_table -> term -> bool *)
fun is_mutually_inductive_pred_def thy table t =
let
- (* term -> bool *)
fun is_good_arg (Bound _) = true
| is_good_arg (Const (s, _)) =
s = @{const_name True} orelse s = @{const_name False} orelse
@@ -1442,7 +1318,6 @@
| NONE => false)
| _ => false
end
-(* theory -> const_table -> term -> term *)
fun unfold_mutually_inductive_preds thy table =
map_aterms (fn t as Const x =>
(case def_of_const thy table x of
@@ -1454,7 +1329,6 @@
| NONE => t)
| t => t)
-(* theory -> (typ option * bool) list -> (string * int) list *)
fun case_const_names thy stds =
Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
if is_basic_datatype thy stds dtype_s then
@@ -1465,7 +1339,6 @@
(Datatype.get_all thy) [] @
map (apsnd length o snd) (#codatatypes (Data.get thy))
-(* theory -> const_table -> string * typ -> fixpoint_kind *)
fun fixpoint_kind_of_const thy table x =
if is_built_in_const thy [(NONE, false)] false x then
NoFp
@@ -1473,7 +1346,6 @@
fixpoint_kind_of_rhs (the (def_of_const thy table x))
handle Option.Option => NoFp
-(* hol_context -> styp -> bool *)
fun is_real_inductive_pred ({thy, stds, fast_descrs, def_table, intro_table,
...} : hol_context) x =
fixpoint_kind_of_const thy def_table x <> NoFp andalso
@@ -1489,7 +1361,6 @@
(is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt orf
(String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
-(* term -> term *)
fun lhs_of_equation t =
case t of
Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
@@ -1500,7 +1371,6 @@
| Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
| @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
| _ => NONE
-(* theory -> term -> bool *)
fun is_constr_pattern _ (Bound _) = true
| is_constr_pattern _ (Var _) = true
| is_constr_pattern thy t =
@@ -1517,10 +1387,8 @@
(* Similar to "Refute.specialize_type" but returns all matches rather than only
the first (preorder) match. *)
-(* theory -> styp -> term -> term list *)
fun multi_specialize_type thy slack (s, T) t =
let
- (* term -> (typ * term) list -> (typ * term) list *)
fun aux (Const (s', T')) ys =
if s = s' then
ys |> (if AList.defined (op =) ys T' then
@@ -1539,22 +1407,18 @@
ys
| aux _ ys = ys
in map snd (fold_aterms aux t []) end
-(* theory -> bool -> const_table -> styp -> term list *)
fun nondef_props_for_const thy slack table (x as (s, _)) =
these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
-(* term -> term *)
fun unvarify_term (t1 $ t2) = unvarify_term t1 $ unvarify_term t2
| unvarify_term (Var ((s, 0), T)) = Free (s, T)
| unvarify_term (Abs (s, T, t')) = Abs (s, T, unvarify_term t')
| unvarify_term t = t
-(* theory -> term -> term *)
fun axiom_for_choice_spec thy =
unvarify_term
#> Object_Logic.atomize_term thy
#> Choice_Specification.close_form
#> HOLogic.mk_Trueprop
-(* hol_context -> styp -> bool *)
fun is_choice_spec_fun ({thy, def_table, nondef_table, choice_spec_table, ...}
: hol_context) x =
case nondef_props_for_const thy true choice_spec_table x of
@@ -1570,7 +1434,6 @@
ts') ts
end
-(* theory -> const_table -> term -> bool *)
fun is_choice_spec_axiom thy choice_spec_table t =
Symtab.exists (fn (_, ts) =>
exists (curry (op aconv) t o axiom_for_choice_spec thy) ts)
@@ -1578,18 +1441,15 @@
(** Constant unfolding **)
-(* theory -> (typ option * bool) list -> int * styp -> term *)
fun constr_case_body thy stds (j, (x as (_, T))) =
let val arg_Ts = binder_types T in
list_comb (Bound j, map2 (select_nth_constr_arg thy stds x (Bound 0))
(index_seq 0 (length arg_Ts)) arg_Ts)
end
-(* hol_context -> typ -> int * styp -> term -> term *)
fun add_constr_case (hol_ctxt as {thy, stds, ...}) res_T (j, x) res_t =
Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
$ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy stds (j, x)
$ res_t
-(* hol_context -> typ -> typ -> term *)
fun optimized_case_def (hol_ctxt as {thy, stds, ...}) dataT res_T =
let
val xs = datatype_constrs hol_ctxt dataT
@@ -1600,7 +1460,6 @@
|> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
|> fold_rev (curry absdummy) (func_Ts @ [dataT])
end
-(* hol_context -> string -> typ -> typ -> term -> term *)
fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t =
let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
case no_of_record_field thy s rec_T of
@@ -1617,7 +1476,6 @@
[]))
| j => select_nth_constr_arg thy stds constr_x t j res_T
end
-(* hol_context -> string -> typ -> term -> term -> term *)
fun optimized_record_update (hol_ctxt as {thy, stds, ...}) s rec_T fun_t rec_t =
let
val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
@@ -1640,12 +1498,10 @@
(* Prevents divergence in case of cyclic or infinite definition dependencies. *)
val unfold_max_depth = 255
-(* hol_context -> term -> term *)
fun unfold_defs_in_term (hol_ctxt as {thy, ctxt, stds, fast_descrs, case_names,
def_table, ground_thm_table, ersatz_table,
...}) =
let
- (* int -> typ list -> term -> term *)
fun do_term depth Ts t =
case t of
(t0 as Const (@{const_name Int.number_class.number_of},
@@ -1695,13 +1551,11 @@
| Var _ => t
| Bound _ => t
| Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
- (* int -> typ list -> styp -> term list -> int -> typ -> term * term list *)
and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
(Abs (Name.uu, body_type T,
select_nth_constr_arg thy stds x (Bound 0) n res_T), [])
| select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
(select_nth_constr_arg thy stds x (do_term depth Ts t) n res_T, ts)
- (* int -> typ list -> term -> styp -> term list -> term *)
and do_const depth Ts t (x as (s, T)) ts =
case AList.lookup (op =) ersatz_table s of
SOME s' =>
@@ -1782,39 +1636,30 @@
(** Axiom extraction/generation **)
-(* term -> string * term *)
fun pair_for_prop t =
case term_under_def t of
Const (s, _) => (s, t)
| t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
-(* (Proof.context -> term list) -> Proof.context -> (term * term) list
- -> const_table *)
fun def_table_for get ctxt subst =
ctxt |> get |> map (pair_for_prop o subst_atomic subst)
|> AList.group (op =) |> Symtab.make
-(* term -> string * term *)
fun paired_with_consts t = map (rpair t) (Term.add_const_names t [])
-(* Proof.context -> (term * term) list -> term list -> const_table *)
fun const_def_table ctxt subst ts =
def_table_for (map prop_of o Nitpick_Defs.get) ctxt subst
|> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
(map pair_for_prop ts)
-(* term list -> const_table *)
fun const_nondef_table ts =
fold (append o paired_with_consts) ts [] |> AList.group (op =) |> Symtab.make
-(* Proof.context -> (term * term) list -> const_table *)
val const_simp_table = def_table_for (map prop_of o Nitpick_Simps.get)
val const_psimp_table = def_table_for (map prop_of o Nitpick_Psimps.get)
fun const_choice_spec_table ctxt subst =
map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
|> const_nondef_table
-(* Proof.context -> (term * term) list -> const_table -> const_table *)
fun inductive_intro_table ctxt subst def_table =
def_table_for
(map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
def_table o prop_of)
o Nitpick_Intros.get) ctxt subst
-(* theory -> term list Inttab.table *)
fun ground_theorem_table thy =
fold ((fn @{const Trueprop} $ t1 =>
is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
@@ -1830,16 +1675,13 @@
(@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
(@{const_name wfrec}, @{const_name wfrec'})]
-(* theory -> (string * string) list *)
fun ersatz_table thy =
fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table
-(* const_table Unsynchronized.ref -> string -> term list -> unit *)
fun add_simps simp_table s eqs =
Unsynchronized.change simp_table
(Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
-(* theory -> styp -> term list *)
fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
let val abs_T = domain_type T in
typedef_info thy (fst (dest_Type abs_T)) |> the
@@ -1847,7 +1689,6 @@
|> pairself (Refute.specialize_type thy x o prop_of o the)
||> single |> op ::
end
-(* theory -> string * typ list -> term list *)
fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
let val abs_T = Type abs_z in
if is_univ_typedef thy abs_T then
@@ -1870,7 +1711,6 @@
end
| NONE => []
end
-(* Proof.context -> string * typ list -> term list *)
fun optimized_quot_type_axioms ctxt stds abs_z =
let
val thy = ProofContext.theory_of ctxt
@@ -1899,7 +1739,6 @@
HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
end
-(* hol_context -> typ -> term list *)
fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T =
let
val xs = datatype_constrs hol_ctxt T
@@ -1914,13 +1753,11 @@
$ (suc_const iter_T $ Bound 0) $ n_var)
val x_var = Var (("x", 0), T)
val y_var = Var (("y", 0), T)
- (* styp -> int -> typ -> term *)
fun nth_sub_bisim x n nth_T =
(if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
else HOLogic.eq_const nth_T)
$ select_nth_constr_arg thy stds x x_var n nth_T
$ select_nth_constr_arg thy stds x y_var n nth_T
- (* styp -> term *)
fun case_func (x as (_, T)) =
let
val arg_Ts = binder_types T
@@ -1942,22 +1779,18 @@
exception NO_TRIPLE of unit
-(* theory -> styp -> term -> term list * term list * term *)
fun triple_for_intro_rule thy x t =
let
val prems = Logic.strip_imp_prems t |> map (Object_Logic.atomize_term thy)
val concl = Logic.strip_imp_concl t |> Object_Logic.atomize_term thy
val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
- (* term -> bool *)
- val is_good_head = curry (op =) (Const x) o head_of
+ val is_good_head = curry (op =) (Const x) o head_of
in
if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE ()
end
-(* term -> term *)
val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
-(* indexname * typ -> term list -> term -> term -> term *)
fun wf_constraint_for rel side concl main =
let
val core = HOLogic.mk_mem (HOLogic.mk_prod (tuple_for_args main,
@@ -1971,12 +1804,9 @@
(t, vars)
end
-(* indexname * typ -> term list * term list * term -> term *)
fun wf_constraint_for_triple rel (side, main, concl) =
map (wf_constraint_for rel side concl) main |> foldr1 s_conj
-(* Proof.context -> Time.time option -> thm
- -> (Proof.context -> tactic -> tactic) -> bool *)
fun terminates_by ctxt timeout goal tac =
can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the
#> SINGLE (DETERM_TIMEOUT timeout
@@ -1992,7 +1822,6 @@
val termination_tacs = [Lexicographic_Order.lex_order_tac true,
ScnpReconstruct.sizechange_tac]
-(* hol_context -> const_table -> styp -> bool *)
fun uncached_is_well_founded_inductive_pred
({thy, ctxt, stds, debug, fast_descrs, tac_timeout, intro_table, ...}
: hol_context) (x as (_, T)) =
@@ -2037,7 +1866,6 @@
(* The type constraint below is a workaround for a Poly/ML crash. *)
-(* hol_context -> styp -> bool *)
fun is_well_founded_inductive_pred
(hol_ctxt as {thy, wfs, def_table, wf_cache, ...} : hol_context)
(x as (s, _)) =
@@ -2054,7 +1882,6 @@
Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
end
-(* typ list -> typ -> term -> term *)
fun ap_curry [_] _ t = t
| ap_curry arg_Ts tuple_T t =
let val n = length arg_Ts in
@@ -2063,7 +1890,6 @@
$ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
end
-(* int -> term -> int *)
fun num_occs_of_bound_in_term j (t1 $ t2) =
op + (pairself (num_occs_of_bound_in_term j) (t1, t2))
| num_occs_of_bound_in_term j (Abs (_, _, t')) =
@@ -2071,10 +1897,8 @@
| num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0
| num_occs_of_bound_in_term _ _ = 0
-(* term -> bool *)
val is_linear_inductive_pred_def =
let
- (* int -> term -> bool *)
fun do_disjunct j (Const (@{const_name Ex}, _) $ Abs (_, _, t2)) =
do_disjunct (j + 1) t2
| do_disjunct j t =
@@ -2082,7 +1906,6 @@
0 => true
| 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts_of t)
| _ => false
- (* term -> bool *)
fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
let val (xs, body) = strip_abs t2 in
case length xs of
@@ -2092,24 +1915,19 @@
| do_lfp_def _ = false
in do_lfp_def o strip_abs_body end
-(* int -> int list list *)
fun n_ptuple_paths 0 = []
| n_ptuple_paths 1 = []
| n_ptuple_paths n = [] :: map (cons 2) (n_ptuple_paths (n - 1))
-(* int -> typ -> typ -> term -> term *)
val ap_n_split = HOLogic.mk_psplits o n_ptuple_paths
-(* term -> term * term *)
val linear_pred_base_and_step_rhss =
let
- (* term -> term *)
fun aux (Const (@{const_name lfp}, _) $ t2) =
let
val (xs, body) = strip_abs t2
val arg_Ts = map snd (tl xs)
val tuple_T = HOLogic.mk_tupleT arg_Ts
val j = length arg_Ts
- (* int -> term -> term *)
fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) =
Const (@{const_name Ex}, T1)
$ Abs (s2, T2, repair_rec (j + 1) t2')
@@ -2139,7 +1957,6 @@
raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
in aux end
-(* hol_context -> styp -> term -> term *)
fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (s, T) def =
let
val j = maxidx_of_term def + 1
@@ -2173,7 +1990,6 @@
|> unfold_defs_in_term hol_ctxt
end
-(* hol_context -> bool -> styp -> term *)
fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
def_table, simp_table, ...})
gfp (x as (s, T)) =
@@ -2210,7 +2026,6 @@
in unrolled_const end
end
-(* hol_context -> styp -> term *)
fun raw_inductive_pred_axiom ({thy, def_table, ...} : hol_context) x =
let
val def = the (def_of_const thy def_table x)
@@ -2237,7 +2052,6 @@
else
raw_inductive_pred_axiom hol_ctxt x
-(* hol_context -> styp -> term list *)
fun raw_equational_fun_axioms (hol_ctxt as {thy, stds, fast_descrs, simp_table,
psimp_table, ...}) x =
case def_props_for_const thy stds fast_descrs (!simp_table) x of
@@ -2246,7 +2060,6 @@
| psimps => psimps)
| simps => simps
val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
-(* hol_context -> styp -> bool *)
fun is_equational_fun_surely_complete hol_ctxt x =
case raw_equational_fun_axioms hol_ctxt x of
[@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
@@ -2255,10 +2068,8 @@
(** Type preprocessing **)
-(* term list -> term list *)
fun merge_type_vars_in_terms ts =
let
- (* typ -> (sort * string) list -> (sort * string) list *)
fun add_type (TFree (s, S)) table =
(case AList.lookup (op =) table S of
SOME s' =>
@@ -2267,12 +2078,10 @@
| NONE => (S, s) :: table)
| add_type _ table = table
val table = fold (fold_types (fold_atyps add_type)) ts []
- (* typ -> typ *)
fun coalesce (TFree (_, S)) = TFree (AList.lookup (op =) table S |> the, S)
| coalesce T = T
in map (map_types (map_atyps coalesce)) ts end
-(* hol_context -> bool -> typ -> typ list -> typ list *)
fun add_ground_types hol_ctxt binarize =
let
fun aux T accum =
@@ -2293,10 +2102,8 @@
| _ => insert (op =) T accum
in aux end
-(* hol_context -> bool -> typ -> typ list *)
fun ground_types_in_type hol_ctxt binarize T =
add_ground_types hol_ctxt binarize T []
-(* hol_context -> term list -> typ list *)
fun ground_types_in_terms hol_ctxt binarize ts =
fold (fold_types (add_ground_types hol_ctxt binarize)) ts []
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Apr 24 16:33:01 2010 +0200
@@ -109,7 +109,6 @@
("trust_potential", "check_potential"),
("trust_genuine", "check_genuine")]
-(* string -> bool *)
fun is_known_raw_param s =
AList.defined (op =) default_default_params s orelse
AList.defined (op =) negated_params s orelse
@@ -118,19 +117,16 @@
["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
"mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"]
-(* string * 'a -> unit *)
fun check_raw_param (s, _) =
if is_known_raw_param s then ()
else error ("Unknown parameter: " ^ quote s ^ ".")
-(* string -> string option *)
fun unnegate_param_name name =
case AList.lookup (op =) negated_params name of
NONE => if String.isPrefix "dont_" name then SOME (unprefix "dont_" name)
else if String.isPrefix "non_" name then SOME (unprefix "non_" name)
else NONE
| some_name => some_name
-(* raw_param -> raw_param *)
fun unnegate_raw_param (name, value) =
case unnegate_param_name name of
SOME name' => (name', case value of
@@ -146,43 +142,32 @@
val extend = I
fun merge p : T = AList.merge (op =) (K true) p)
-(* raw_param -> theory -> theory *)
val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
-(* theory -> raw_param list *)
val default_raw_params = Data.get
-(* string -> bool *)
fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
-(* string list -> string *)
fun stringify_raw_param_value [] = ""
| stringify_raw_param_value [s] = s
| stringify_raw_param_value (s1 :: s2 :: ss) =
s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^
stringify_raw_param_value (s2 :: ss)
-(* int -> string -> int *)
fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))
-(* Proof.context -> bool -> raw_param list -> raw_param list -> params *)
fun extract_params ctxt auto default_params override_params =
let
val override_params = map unnegate_raw_param override_params
val raw_params = rev override_params @ rev default_params
- (* string -> string *)
val lookup =
Option.map stringify_raw_param_value o AList.lookup (op =) raw_params
val lookup_string = the_default "" o lookup
- (* bool -> bool option -> string -> bool option *)
fun general_lookup_bool option default_value name =
case lookup name of
SOME s => parse_bool_option option name s
| NONE => default_value
- (* string -> bool *)
val lookup_bool = the o general_lookup_bool false (SOME false)
- (* string -> bool option *)
val lookup_bool_option = general_lookup_bool true NONE
- (* string -> string option -> int *)
fun do_int name value =
case value of
SOME s => (case Int.fromString s of
@@ -190,14 +175,11 @@
| NONE => error ("Parameter " ^ quote name ^
" must be assigned an integer value."))
| NONE => 0
- (* string -> int *)
fun lookup_int name = do_int name (lookup name)
- (* string -> int option *)
fun lookup_int_option name =
case lookup name of
SOME "smart" => NONE
| value => SOME (do_int name value)
- (* string -> int -> string -> int list *)
fun int_range_from_string name min_int s =
let
val (k1, k2) =
@@ -211,17 +193,14 @@
handle Option.Option =>
error ("Parameter " ^ quote name ^
" must be assigned a sequence of integers.")
- (* string -> int -> string -> int list *)
fun int_seq_from_string name min_int s =
maps (int_range_from_string name min_int) (space_explode "," s)
- (* string -> int -> int list *)
fun lookup_int_seq name min_int =
case lookup name of
SOME s => (case int_seq_from_string name min_int s of
[] => [min_int]
| value => value)
| NONE => [min_int]
- (* (string -> 'a) -> int -> string -> ('a option * int list) list *)
fun lookup_ints_assigns read prefix min_int =
(NONE, lookup_int_seq prefix min_int)
:: map (fn (name, value) =>
@@ -229,7 +208,6 @@
value |> stringify_raw_param_value
|> int_seq_from_string name min_int))
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
- (* (string -> 'a) -> string -> ('a option * bool) list *)
fun lookup_bool_assigns read prefix =
(NONE, lookup_bool prefix)
:: map (fn (name, value) =>
@@ -237,7 +215,6 @@
value |> stringify_raw_param_value
|> parse_bool_option false name |> the))
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
- (* (string -> 'a) -> string -> ('a option * bool option) list *)
fun lookup_bool_option_assigns read prefix =
(NONE, lookup_bool_option prefix)
:: map (fn (name, value) =>
@@ -245,21 +222,17 @@
value |> stringify_raw_param_value
|> parse_bool_option true name))
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
- (* string -> Time.time option *)
fun lookup_time name =
case lookup name of
NONE => NONE
| SOME s => parse_time_option name s
- (* string -> term list *)
val lookup_term_list =
AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt
val read_type_polymorphic =
Syntax.read_typ ctxt #> Logic.mk_type
#> singleton (Variable.polymorphic ctxt) #> Logic.dest_type
- (* string -> term *)
val read_term_polymorphic =
Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt)
- (* string -> styp *)
val read_const_polymorphic = read_term_polymorphic #> dest_Const
val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
@@ -330,25 +303,19 @@
check_genuine = check_genuine, batch_size = batch_size, expect = expect}
end
-(* theory -> (string * string) list -> params *)
fun default_params thy =
extract_params (ProofContext.init thy) false (default_raw_params thy)
o map (apsnd single)
-(* P.token list -> string * P.token list *)
val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
-(* P.token list -> string list * P.token list *)
val parse_value =
Scan.repeat1 (P.minus >> single
|| Scan.repeat1 (Scan.unless P.minus P.name)
|| P.$$$ "," |-- P.number >> prefix "," >> single) >> flat
-(* P.token list -> raw_param * P.token list *)
val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
-(* P.token list -> raw_param list * P.token list *)
val parse_params =
Scan.optional (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]") []
-(* Proof.context -> ('a -> 'a) -> 'a -> 'a *)
fun handle_exceptions ctxt f x =
f x
handle ARG (loc, details) =>
@@ -386,7 +353,6 @@
| Refute.REFUTE (loc, details) =>
error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
-(* raw_param list -> bool -> int -> int -> Proof.state -> bool * Proof.state *)
fun pick_nits override_params auto i step state =
let
val thy = Proof.theory_of state
@@ -394,7 +360,6 @@
val _ = List.app check_raw_param override_params
val params as {blocking, debug, ...} =
extract_params ctxt auto (default_raw_params thy) override_params
- (* unit -> bool * Proof.state *)
fun go () =
(false, state)
|> (if auto then perhaps o try
@@ -407,17 +372,14 @@
else (Toplevel.thread true (fn () => (go (); ())); (false, state))
end
-(* raw_param list * int -> Toplevel.transition -> Toplevel.transition *)
fun nitpick_trans (params, i) =
Toplevel.keep (fn st =>
(pick_nits params false i (Toplevel.proof_position_of st)
(Toplevel.proof_of st); ()))
-(* raw_param -> string *)
fun string_for_raw_param (name, value) =
name ^ " = " ^ stringify_raw_param_value value
-(* raw_param list -> Toplevel.transition -> Toplevel.transition *)
fun nitpick_params_trans params =
Toplevel.theory
(fold set_default_raw_param params
@@ -430,8 +392,6 @@
params |> map string_for_raw_param
|> sort_strings |> cat_lines)))))
-(* P.token list
- -> (Toplevel.transition -> Toplevel.transition) * P.token list *)
val parse_nitpick_command =
(parse_params -- Scan.optional P.nat 1) #>> nitpick_trans
val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
@@ -443,7 +403,6 @@
"set and display the default parameters for Nitpick"
K.thy_decl parse_nitpick_params_command
-(* Proof.state -> bool * Proof.state *)
fun auto_nitpick state =
if not (!auto) then (false, state) else pick_nits [] true 1 0 state
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Sat Apr 24 16:33:01 2010 +0200
@@ -57,24 +57,19 @@
structure NfaGraph = Typ_Graph
-(* int -> KK.int_expr list *)
fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num
-(* int -> int -> int -> KK.bound list -> KK.formula -> int *)
fun univ_card nat_card int_card main_j0 bounds formula =
let
- (* KK.rel_expr -> int -> int *)
fun rel_expr_func r k =
Int.max (k, case r of
KK.Atom j => j + 1
| KK.AtomSeq (k', j0) => j0 + k'
| _ => 0)
- (* KK.tuple -> int -> int *)
fun tuple_func t k =
case t of
KK.Tuple js => fold Integer.max (map (Integer.add 1) js) k
| _ => k
- (* KK.tuple_set -> int -> int *)
fun tuple_set_func ts k =
Int.max (k, case ts of KK.TupleAtomSeq (k', j0) => j0 + k' | _ => 0)
val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func,
@@ -84,10 +79,8 @@
|> KK.fold_formula expr_F formula
in Int.max (main_j0 + fold Integer.max [2, nat_card, int_card] 0, card) end
-(* int -> KK.formula -> unit *)
fun check_bits bits formula =
let
- (* KK.int_expr -> unit -> unit *)
fun int_expr_func (KK.Num k) () =
if is_twos_complement_representable bits k then
()
@@ -100,7 +93,6 @@
int_expr_func = int_expr_func}
in KK.fold_formula expr_F formula () end
-(* int -> int -> unit *)
fun check_arity univ_card n =
if n > KK.max_arity univ_card then
raise TOO_LARGE ("Nitpick_Kodkod.check_arity",
@@ -109,7 +101,6 @@
else
()
-(* bool -> int -> int list -> KK.tuple *)
fun kk_tuple debug univ_card js =
if debug then
KK.Tuple js
@@ -117,19 +108,13 @@
KK.TupleIndex (length js,
fold (fn j => fn accum => accum * univ_card + j) js 0)
-(* (int * int) list -> KK.tuple_set *)
val tuple_set_from_atom_schema = foldl1 KK.TupleProduct o map KK.TupleAtomSeq
-(* rep -> KK.tuple_set *)
val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep
-(* int -> KK.tuple_set *)
val single_atom = KK.TupleSet o single o KK.Tuple o single
-(* int -> KK.int_bound list *)
fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))]
-(* int -> int -> KK.int_bound list *)
fun pow_of_two_int_bounds bits j0 =
let
- (* int -> int -> int -> KK.int_bound list *)
fun aux 0 _ _ = []
| aux 1 pow_of_two j = [(SOME (~ pow_of_two), [single_atom j])]
| aux iter pow_of_two j =
@@ -137,10 +122,8 @@
aux (iter - 1) (2 * pow_of_two) (j + 1)
in aux (bits + 1) 1 j0 end
-(* KK.formula -> KK.n_ary_index list *)
fun built_in_rels_in_formula formula =
let
- (* KK.rel_expr -> KK.n_ary_index list -> KK.n_ary_index list *)
fun rel_expr_func (KK.Rel (x as (n, j))) =
if x = unsigned_bit_word_sel_rel orelse x = signed_bit_word_sel_rel then
I
@@ -155,7 +138,6 @@
val max_table_size = 65536
-(* int -> unit *)
fun check_table_size k =
if k > max_table_size then
raise TOO_LARGE ("Nitpick_Kodkod.check_table_size",
@@ -163,7 +145,6 @@
else
()
-(* bool -> int -> int * int -> (int -> int) -> KK.tuple list *)
fun tabulate_func1 debug univ_card (k, j0) f =
(check_table_size k;
map_filter (fn j1 => let val j2 = f j1 in
@@ -172,7 +153,6 @@
else
NONE
end) (index_seq 0 k))
-(* bool -> int -> int * int -> int -> (int * int -> int) -> KK.tuple list *)
fun tabulate_op2 debug univ_card (k, j0) res_j0 f =
(check_table_size (k * k);
map_filter (fn j => let
@@ -186,8 +166,6 @@
else
NONE
end) (index_seq 0 (k * k)))
-(* bool -> int -> int * int -> int -> (int * int -> int * int)
- -> KK.tuple list *)
fun tabulate_op2_2 debug univ_card (k, j0) res_j0 f =
(check_table_size (k * k);
map_filter (fn j => let
@@ -202,33 +180,27 @@
else
NONE
end) (index_seq 0 (k * k)))
-(* bool -> int -> int * int -> (int * int -> int) -> KK.tuple list *)
fun tabulate_nat_op2 debug univ_card (k, j0) f =
tabulate_op2 debug univ_card (k, j0) j0 (atom_for_nat (k, 0) o f)
fun tabulate_int_op2 debug univ_card (k, j0) f =
tabulate_op2 debug univ_card (k, j0) j0
(atom_for_int (k, 0) o f o pairself (int_for_atom (k, 0)))
-(* bool -> int -> int * int -> (int * int -> int * int) -> KK.tuple list *)
fun tabulate_int_op2_2 debug univ_card (k, j0) f =
tabulate_op2_2 debug univ_card (k, j0) j0
(pairself (atom_for_int (k, 0)) o f
o pairself (int_for_atom (k, 0)))
-(* int * int -> int *)
fun isa_div (m, n) = m div n handle General.Div => 0
fun isa_mod (m, n) = m mod n handle General.Div => m
fun isa_gcd (m, 0) = m
| isa_gcd (m, n) = isa_gcd (n, isa_mod (m, n))
fun isa_lcm (m, n) = isa_div (m * n, isa_gcd (m, n))
val isa_zgcd = isa_gcd o pairself abs
-(* int * int -> int * int *)
fun isa_norm_frac (m, n) =
if n < 0 then isa_norm_frac (~m, ~n)
else if m = 0 orelse n = 0 then (0, 1)
else let val p = isa_zgcd (m, n) in (isa_div (m, p), isa_div (n, p)) end
-(* bool -> int -> int -> int -> int -> int * int
- -> string * bool * KK.tuple list *)
fun tabulate_built_in_rel debug univ_card nat_card int_card j0 (x as (n, _)) =
(check_arity univ_card n;
if x = not3_rel then
@@ -269,25 +241,21 @@
else
raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation"))
-(* bool -> int -> int -> int -> int -> int * int -> KK.rel_expr -> KK.bound *)
fun bound_for_built_in_rel debug univ_card nat_card int_card j0 x =
let
val (nick, ts) = tabulate_built_in_rel debug univ_card nat_card int_card
j0 x
in ([(x, nick)], [KK.TupleSet ts]) end
-(* bool -> int -> int -> int -> int -> KK.formula -> KK.bound list *)
fun bounds_for_built_in_rels_in_formula debug univ_card nat_card int_card j0 =
map (bound_for_built_in_rel debug univ_card nat_card int_card j0)
o built_in_rels_in_formula
-(* Proof.context -> bool -> string -> typ -> rep -> string *)
fun bound_comment ctxt debug nick T R =
short_name nick ^
(if debug then " :: " ^ unyxml (Syntax.string_of_typ ctxt T) else "") ^
" : " ^ string_for_rep R
-(* Proof.context -> bool -> nut -> KK.bound *)
fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =
([(x, bound_comment ctxt debug nick T R)],
if nick = @{const_name bisim_iterator_max} then
@@ -299,7 +267,6 @@
| bound_for_plain_rel _ _ u =
raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
-(* Proof.context -> bool -> dtype_spec list -> nut -> KK.bound *)
fun bound_for_sel_rel ctxt debug dtypes
(FreeRel (x, T as Type (@{type_name fun}, [T1, T2]),
R as Func (Atom (_, j0), R2), nick)) =
@@ -331,12 +298,9 @@
| bound_for_sel_rel _ _ _ u =
raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u])
-(* KK.bound list -> KK.bound list *)
fun merge_bounds bs =
let
- (* KK.bound -> int *)
fun arity (zs, _) = fst (fst (hd zs))
- (* KK.bound list -> KK.bound -> KK.bound list -> KK.bound list *)
fun add_bound ds b [] = List.revAppend (ds, [b])
| add_bound ds b (c :: cs) =
if arity b = arity c andalso snd b = snd c then
@@ -345,40 +309,33 @@
add_bound (c :: ds) b cs
in fold (add_bound []) bs [] end
-(* int -> int -> KK.rel_expr list *)
fun unary_var_seq j0 n = map (curry KK.Var 1) (index_seq j0 n)
-(* int list -> KK.rel_expr *)
val singleton_from_combination = foldl1 KK.Product o map KK.Atom
-(* rep -> KK.rel_expr list *)
fun all_singletons_for_rep R =
if is_lone_rep R then
all_combinations_for_rep R |> map singleton_from_combination
else
raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R])
-(* KK.rel_expr -> KK.rel_expr list *)
fun unpack_products (KK.Product (r1, r2)) =
unpack_products r1 @ unpack_products r2
| unpack_products r = [r]
fun unpack_joins (KK.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2
| unpack_joins r = [r]
-(* rep -> KK.rel_expr *)
val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep
fun full_rel_for_rep R =
case atom_schema_of_rep R of
[] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R])
| schema => foldl1 KK.Product (map KK.AtomSeq schema)
-(* int -> int list -> KK.decl list *)
fun decls_for_atom_schema j0 schema =
map2 (fn j => fn x => KK.DeclOne ((1, j), KK.AtomSeq x))
(index_seq j0 (length schema)) schema
(* The type constraint below is a workaround for a Poly/ML bug. *)
-(* kodkod_constrs -> rep -> KK.rel_expr -> KK.formula *)
fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs)
R r =
let val body_R = body_rep R in
@@ -420,14 +377,11 @@
d_n_ary_function kk R r
| kk_n_ary_function kk R r = d_n_ary_function kk R r
-(* kodkod_constrs -> KK.rel_expr list -> KK.formula *)
fun kk_disjoint_sets _ [] = KK.True
| kk_disjoint_sets (kk as {kk_and, kk_no, kk_intersect, ...} : kodkod_constrs)
(r :: rs) =
fold (kk_and o kk_no o kk_intersect r) rs (kk_disjoint_sets kk rs)
-(* int -> kodkod_constrs -> (KK.rel_expr -> KK.rel_expr) -> KK.rel_expr
- -> KK.rel_expr *)
fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r =
if inline_rel_expr r then
f r
@@ -435,36 +389,25 @@
let val x = (KK.arity_of_rel_expr r, j) in
kk_rel_let [KK.AssignRelReg (x, r)] (f (KK.RelReg x))
end
-(* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr) -> KK.rel_expr
- -> KK.rel_expr *)
val single_rel_rel_let = basic_rel_rel_let 0
-(* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr) -> KK.rel_expr
- -> KK.rel_expr -> KK.rel_expr *)
fun double_rel_rel_let kk f r1 r2 =
single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1
-(* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr)
- -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr *)
fun triple_rel_rel_let kk f r1 r2 r3 =
double_rel_rel_let kk
(fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2
-(* kodkod_constrs -> int -> KK.formula -> KK.rel_expr *)
fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f =
kk_rel_if f (KK.Atom (j0 + 1)) (KK.Atom j0)
-(* kodkod_constrs -> rep -> KK.formula -> KK.rel_expr *)
fun rel_expr_from_formula kk R f =
case unopt_rep R of
Atom (2, j0) => atom_from_formula kk j0 f
| _ => raise REP ("Nitpick_Kodkod.rel_expr_from_formula", [R])
-(* kodkod_cotrs -> int -> int -> KK.rel_expr -> KK.rel_expr list *)
fun unpack_vect_in_chunks ({kk_project_seq, ...} : kodkod_constrs) chunk_arity
num_chunks r =
List.tabulate (num_chunks, fn j => kk_project_seq r (j * chunk_arity)
chunk_arity)
-(* kodkod_constrs -> bool -> rep -> rep -> KK.rel_expr -> KK.rel_expr
- -> KK.rel_expr *)
fun kk_n_fold_join
(kk as {kk_intersect, kk_product, kk_join, kk_project_seq, ...}) one R1
res_R r1 r2 =
@@ -484,8 +427,6 @@
arity1 (arity_of_rep res_R)
end
-(* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr list
- -> KK.rel_expr list -> KK.rel_expr *)
fun kk_case_switch (kk as {kk_union, kk_product, ...}) R1 R2 r rs1 rs2 =
if rs1 = rs2 then r
else kk_n_fold_join kk true R1 R2 r (fold1 kk_union (map2 kk_product rs1 rs2))
@@ -493,7 +434,6 @@
val lone_rep_fallback_max_card = 4096
val some_j0 = 0
-(* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)
fun lone_rep_fallback kk new_R old_R r =
if old_R = new_R then
r
@@ -510,7 +450,6 @@
else
raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R])
end
-(* kodkod_constrs -> int * int -> rep -> KK.rel_expr -> KK.rel_expr *)
and atom_from_rel_expr kk x old_R r =
case old_R of
Func (R1, R2) =>
@@ -523,7 +462,6 @@
end
| Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R])
| _ => lone_rep_fallback kk (Atom x) old_R r
-(* kodkod_constrs -> rep list -> rep -> KK.rel_expr -> KK.rel_expr *)
and struct_from_rel_expr kk Rs old_R r =
case old_R of
Atom _ => lone_rep_fallback kk (Struct Rs) old_R r
@@ -547,7 +485,6 @@
lone_rep_fallback kk (Struct Rs) old_R r
end
| _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R])
-(* kodkod_constrs -> int -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)
and vect_from_rel_expr kk k R old_R r =
case old_R of
Atom _ => lone_rep_fallback kk (Vect (k, R)) old_R r
@@ -570,7 +507,6 @@
(kk_n_fold_join kk true R1 R2 arg_r r))
(all_singletons_for_rep R1))
| _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R])
-(* kodkod_constrs -> rep -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)
and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r =
let
val dom_card = card_of_rep R1
@@ -599,7 +535,6 @@
let
val args_rs = all_singletons_for_rep R1
val vals_rs = unpack_vect_in_chunks kk 1 k r
- (* KK.rel_expr -> KK.rel_expr -> KK.rel_expr *)
fun empty_or_singleton_set_for arg_r val_r =
#kk_join kk val_r (#kk_product kk (KK.Atom (j0 + 1)) arg_r)
in
@@ -682,7 +617,6 @@
end
| _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr",
[old_R, Func (R1, R2)])
-(* kodkod_constrs -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)
and rel_expr_from_rel_expr kk new_R old_R r =
let
val unopt_old_R = unopt_rep old_R
@@ -702,25 +636,20 @@
[old_R, new_R]))
unopt_old_R r
end
-(* kodkod_constrs -> rep -> rep -> rep -> KK.rel_expr -> KK.rel_expr *)
and rel_expr_to_func kk R1 R2 = rel_expr_from_rel_expr kk (Func (R1, R2))
-(* kodkod_constrs -> typ -> KK.rel_expr -> KK.rel_expr *)
fun bit_set_from_atom ({kk_join, ...} : kodkod_constrs) T r =
kk_join r (KK.Rel (if T = @{typ "unsigned_bit word"} then
unsigned_bit_word_sel_rel
else
signed_bit_word_sel_rel))
-(* kodkod_constrs -> typ -> KK.rel_expr -> KK.int_expr *)
val int_expr_from_atom = KK.SetSum ooo bit_set_from_atom
-(* kodkod_constrs -> typ -> rep -> KK.int_expr -> KK.rel_expr *)
fun atom_from_int_expr (kk as {kk_rel_eq, kk_comprehension, ...}
: kodkod_constrs) T R i =
kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R))
(kk_rel_eq (bit_set_from_atom kk T (KK.Var (1, ~1)))
(KK.Bits i))
-(* kodkod_constrs -> nut -> KK.formula *)
fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) =
kk_n_ary_function kk (R |> nick = @{const_name List.set} ? unopt_rep)
(KK.Rel x)
@@ -732,17 +661,13 @@
| declarative_axiom_for_plain_rel _ u =
raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u])
-(* nut NameTable.table -> styp -> KK.rel_expr * rep * int *)
fun const_triple rel_table (x as (s, T)) =
case the_name rel_table (ConstName (s, T, Any)) of
FreeRel ((n, j), _, R, _) => (KK.Rel (n, j), R, n)
| _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x])
-(* nut NameTable.table -> styp -> KK.rel_expr *)
fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
-(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
- -> dtype_spec list -> styp -> int -> nfa_transition list *)
fun nfa_transitions_for_sel hol_ctxt binarize
({kk_project, ...} : kodkod_constrs) rel_table
(dtypes : dtype_spec list) constr_x n =
@@ -757,14 +682,10 @@
else SOME (kk_project r (map KK.Num [0, j]), T))
(index_seq 1 (arity - 1) ~~ tl type_schema)
end
-(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
- -> dtype_spec list -> styp -> nfa_transition list *)
fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes
(x as (_, T)) =
maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
(index_seq 0 (num_sels_for_constr_type T))
-(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
- -> dtype_spec list -> dtype_spec -> nfa_entry option *)
fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
| nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE
| nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
@@ -775,12 +696,10 @@
val empty_rel = KK.Product (KK.None, KK.None)
-(* nfa_table -> typ -> typ -> KK.rel_expr list *)
fun direct_path_rel_exprs nfa start_T final_T =
case AList.lookup (op =) nfa final_T of
SOME trans => map fst (filter (curry (op =) start_T o snd) trans)
| NONE => []
-(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> KK.rel_expr *)
and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T
final_T =
fold kk_union (direct_path_rel_exprs nfa start_T final_T)
@@ -788,14 +707,11 @@
| any_path_rel_expr (kk as {kk_union, ...}) nfa (T :: Ts) start_T final_T =
kk_union (any_path_rel_expr kk nfa Ts start_T final_T)
(knot_path_rel_expr kk nfa Ts start_T T final_T)
-(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> typ
- -> KK.rel_expr *)
and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts
start_T knot_T final_T =
kk_join (kk_join (any_path_rel_expr kk nfa Ts knot_T final_T)
(kk_reflexive_closure (loop_path_rel_expr kk nfa Ts knot_T)))
(any_path_rel_expr kk nfa Ts start_T knot_T)
-(* kodkod_constrs -> nfa_table -> typ list -> typ -> KK.rel_expr *)
and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T =
fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel
| loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (T :: Ts)
@@ -806,12 +722,9 @@
kk_union (loop_path_rel_expr kk nfa Ts start_T)
(knot_path_rel_expr kk nfa Ts start_T T start_T)
-(* nfa_table -> unit NfaGraph.T *)
fun graph_for_nfa nfa =
let
- (* typ -> unit NfaGraph.T -> unit NfaGraph.T *)
fun new_node T = perhaps (try (NfaGraph.new_node (T, ())))
- (* nfa_table -> unit NfaGraph.T -> unit NfaGraph.T *)
fun add_nfa [] = I
| add_nfa ((_, []) :: nfa) = add_nfa nfa
| add_nfa ((T, ((_, T') :: transitions)) :: nfa) =
@@ -819,25 +732,19 @@
new_node T' o new_node T
in add_nfa nfa NfaGraph.empty end
-(* nfa_table -> nfa_table list *)
fun strongly_connected_sub_nfas nfa =
nfa |> graph_for_nfa |> NfaGraph.strong_conn
|> map (fn keys => filter (member (op =) keys o fst) nfa)
-(* kodkod_constrs -> nfa_table -> typ -> KK.formula *)
fun acyclicity_axiom_for_datatype kk nfa start_T =
#kk_no kk (#kk_intersect kk
(loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden)
-(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
- -> dtype_spec list -> KK.formula list *)
fun acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes =
map_filter (nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes)
dtypes
|> strongly_connected_sub_nfas
|> maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa)
-(* hol_context -> bool -> int -> kodkod_constrs -> nut NameTable.table
- -> KK.rel_expr -> constr_spec -> int -> KK.formula *)
fun sel_axiom_for_sel hol_ctxt binarize j0
(kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec)
@@ -857,8 +764,6 @@
(kk_n_ary_function kk R2 r') (kk_no r'))
end
end
-(* hol_context -> bool -> int -> int -> kodkod_constrs -> nut NameTable.table
- -> constr_spec -> KK.formula list *)
fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table
(constr as {const, delta, epsilon, explicit_max, ...}) =
let
@@ -885,19 +790,14 @@
(index_seq 0 (num_sels_for_constr_type (snd const)))
end
end
-(* hol_context -> bool -> int -> int -> kodkod_constrs -> nut NameTable.table
- -> dtype_spec -> KK.formula list *)
fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table
({constrs, ...} : dtype_spec) =
maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs
-(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table -> constr_spec
- -> KK.formula list *)
fun uniqueness_axiom_for_constr hol_ctxt binarize
({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
: kodkod_constrs) rel_table ({const, ...} : constr_spec) =
let
- (* KK.rel_expr -> KK.formula *)
fun conjunct_for_sel r =
kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
val num_sels = num_sels_for_constr_type (snd const)
@@ -915,16 +815,11 @@
(fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
(kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
end
-(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table -> dtype_spec
- -> KK.formula list *)
fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table
({constrs, ...} : dtype_spec) =
map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs
-(* constr_spec -> int *)
fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
-(* int -> kodkod_constrs -> nut NameTable.table -> dtype_spec
- -> KK.formula list *)
fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
rel_table
({card, constrs, ...} : dtype_spec) =
@@ -936,8 +831,6 @@
kk_disjoint_sets kk rs]
end
-(* hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
- -> nut NameTable.table -> dtype_spec -> KK.formula list *)
fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = []
| other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table
(dtype as {typ, ...}) =
@@ -947,15 +840,12 @@
partition_axioms_for_datatype j0 kk rel_table dtype
end
-(* hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
- -> nut NameTable.table -> dtype_spec list -> KK.formula list *)
fun declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk rel_table
dtypes =
acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes @
maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
dtypes
-(* int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
fun kodkod_formula_from_nut ofs
(kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
@@ -970,17 +860,13 @@
val false_atom = KK.Atom bool_j0
val true_atom = KK.Atom (bool_j0 + 1)
- (* polarity -> int -> KK.rel_expr -> KK.formula *)
fun formula_from_opt_atom polar j0 r =
case polar of
Neg => kk_not (kk_rel_eq r (KK.Atom j0))
| _ => kk_rel_eq r (KK.Atom (j0 + 1))
- (* int -> KK.rel_expr -> KK.formula *)
val formula_from_atom = formula_from_opt_atom Pos
- (* KK.formula -> KK.formula -> KK.formula *)
fun kk_notimplies f1 f2 = kk_and f1 (kk_not f2)
- (* KK.rel_expr -> KK.rel_expr -> KK.rel_expr *)
val kk_or3 =
double_rel_rel_let kk
(fn r1 => fn r2 =>
@@ -993,21 +879,15 @@
(kk_intersect r1 r2))
fun kk_notimplies3 r1 r2 = kk_and3 r1 (kk_not3 r2)
- (* int -> KK.rel_expr -> KK.formula list *)
val unpack_formulas =
map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1
- (* (KK.formula -> KK.formula -> KK.formula) -> int -> KK.rel_expr
- -> KK.rel_expr -> KK.rel_expr *)
fun kk_vect_set_op connective k r1 r2 =
fold1 kk_product (map2 (atom_from_formula kk bool_j0 oo connective)
(unpack_formulas k r1) (unpack_formulas k r2))
- (* (KK.formula -> KK.formula -> KK.formula) -> int -> KK.rel_expr
- -> KK.rel_expr -> KK.formula *)
fun kk_vect_set_bool_op connective k r1 r2 =
fold1 kk_and (map2 connective (unpack_formulas k r1)
(unpack_formulas k r2))
- (* nut -> KK.formula *)
fun to_f u =
case rep_of u of
Formula polar =>
@@ -1060,7 +940,6 @@
else
let
(* FIXME: merge with similar code below *)
- (* bool -> nut -> KK.rel_expr *)
fun set_to_r widen u =
if widen then
kk_difference (full_rel_for_rep dom_R)
@@ -1078,7 +957,6 @@
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
| min_R =>
let
- (* nut -> nut list *)
fun args (Op2 (Apply, _, _, u1, u2)) = u2 :: args u1
| args (Tuple (_, _, us)) = us
| args _ = []
@@ -1177,14 +1055,12 @@
| _ => raise NUT ("Nitpick_Kodkod.to_f", [u]))
| Atom (2, j0) => formula_from_atom j0 (to_r u)
| _ => raise NUT ("Nitpick_Kodkod.to_f", [u])
- (* polarity -> nut -> KK.formula *)
and to_f_with_polarity polar u =
case rep_of u of
Formula _ => to_f u
| Atom (2, j0) => formula_from_atom j0 (to_r u)
| Opt (Atom (2, j0)) => formula_from_opt_atom polar j0 (to_r u)
| _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u])
- (* nut -> KK.rel_expr *)
and to_r u =
case u of
Cst (False, _, Atom _) => false_atom
@@ -1523,7 +1399,6 @@
| Opt (Atom (2, _)) =>
let
(* FIXME: merge with similar code above *)
- (* rep -> rep -> nut -> KK.rel_expr *)
fun must R1 R2 u =
kk_join (to_rep (Func (Struct [R1, R2], body_R)) u) true_atom
fun may R1 R2 u =
@@ -1558,9 +1433,7 @@
(to_rep (Func (b_R, Formula Neut)) u2)
| Opt (Atom (2, _)) =>
let
- (* KK.rel_expr -> rep -> nut -> KK.rel_expr *)
fun do_nut r R u = kk_join (to_rep (Func (R, body_R)) u) r
- (* KK.rel_expr -> KK.rel_expr *)
fun do_term r =
kk_product (kk_product (do_nut r a_R u1) (do_nut r b_R u2)) r
in kk_union (do_term true_atom) (do_term false_atom) end
@@ -1572,7 +1445,6 @@
(Func (R11, R12), Func (R21, Formula Neut)) =>
if R21 = R11 andalso is_lone_rep R12 then
let
- (* KK.rel_expr -> KK.rel_expr *)
fun big_join r = kk_n_fold_join kk false R21 R12 r (to_r u1)
val core_r = big_join (to_r u2)
val core_R = Func (R12, Formula Neut)
@@ -1666,39 +1538,32 @@
| FreeRel (x, _, _, _) => KK.Rel x
| RelReg (j, _, R) => KK.RelReg (arity_of_rep R, j)
| u => raise NUT ("Nitpick_Kodkod.to_r", [u])
- (* nut -> KK.decl *)
and to_decl (BoundRel (x, _, R, _)) =
KK.DeclOne (x, KK.AtomSeq (the_single (atom_schema_of_rep R)))
| to_decl u = raise NUT ("Nitpick_Kodkod.to_decl", [u])
- (* nut -> KK.expr_assign *)
and to_expr_assign (FormulaReg (j, _, _)) u =
KK.AssignFormulaReg (j, to_f u)
| to_expr_assign (RelReg (j, _, R)) u =
KK.AssignRelReg ((arity_of_rep R, j), to_r u)
| to_expr_assign u1 _ = raise NUT ("Nitpick_Kodkod.to_expr_assign", [u1])
- (* int * int -> nut -> KK.rel_expr *)
and to_atom (x as (k, j0)) u =
case rep_of u of
Formula _ => atom_from_formula kk j0 (to_f u)
| Unit => if k = 1 then KK.Atom j0
else raise NUT ("Nitpick_Kodkod.to_atom", [u])
| R => atom_from_rel_expr kk x R (to_r u)
- (* rep list -> nut -> KK.rel_expr *)
and to_struct Rs u =
case rep_of u of
Unit => full_rel_for_rep (Struct Rs)
| R' => struct_from_rel_expr kk Rs R' (to_r u)
- (* int -> rep -> nut -> KK.rel_expr *)
and to_vect k R u =
case rep_of u of
Unit => full_rel_for_rep (Vect (k, R))
| R' => vect_from_rel_expr kk k R R' (to_r u)
- (* rep -> rep -> nut -> KK.rel_expr *)
and to_func R1 R2 u =
case rep_of u of
Unit => full_rel_for_rep (Func (R1, R2))
| R' => rel_expr_to_func kk R1 R2 R' (to_r u)
- (* rep -> nut -> KK.rel_expr *)
and to_opt R u =
let val old_R = rep_of u in
if is_opt_rep old_R then
@@ -1706,16 +1571,13 @@
else
to_rep R u
end
- (* rep -> nut -> KK.rel_expr *)
and to_rep (Atom x) u = to_atom x u
| to_rep (Struct Rs) u = to_struct Rs u
| to_rep (Vect (k, R)) u = to_vect k R u
| to_rep (Func (R1, R2)) u = to_func R1 R2 u
| to_rep (Opt R) u = to_opt R u
| to_rep R _ = raise REP ("Nitpick_Kodkod.to_rep", [R])
- (* nut -> KK.rel_expr *)
and to_integer u = to_opt (one_rep ofs (type_of u) (rep_of u)) u
- (* nut list -> rep -> KK.rel_expr -> KK.rel_expr *)
and to_guard guard_us R r =
let
val unpacked_rs = unpack_joins r
@@ -1733,16 +1595,13 @@
if null guard_fs then r
else kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r
end
- (* rep -> rep -> KK.rel_expr -> int -> KK.rel_expr *)
and to_project new_R old_R r j0 =
rel_expr_from_rel_expr kk new_R old_R
(kk_project_seq r j0 (arity_of_rep old_R))
- (* rep list -> nut list -> KK.rel_expr *)
and to_product Rs us =
case map (uncurry to_opt) (filter (not_equal Unit o fst) (Rs ~~ us)) of
[] => raise REP ("Nitpick_Kodkod.to_product", Rs)
| rs => fold1 kk_product rs
- (* int -> typ -> rep -> nut -> KK.rel_expr *)
and to_nth_pair_sel n res_T res_R u =
case u of
Tuple (_, _, us) => to_rep res_R (nth us n)
@@ -1770,9 +1629,6 @@
(to_rep res_R (Cst (Unity, res_T, Unit)))
| _ => to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0
end
- (* (KK.formula -> KK.formula -> KK.formula)
- -> (KK.rel_expr -> KK.rel_expr -> KK.formula) -> nut -> nut
- -> KK.formula *)
and to_set_bool_op connective set_oper u1 u2 =
let
val min_R = min_rep (rep_of u1) (rep_of u2)
@@ -1788,12 +1644,6 @@
(kk_join r2 true_atom)
| _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
end
- (* (KK.formula -> KK.formula -> KK.formula)
- -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr)
- -> (KK.rel_expr -> KK.rel_expr -> KK.formula)
- -> (KK.rel_expr -> KK.rel_expr -> KK.formula)
- -> (KK.rel_expr -> KK.rel_expr -> KK.formula) -> bool -> rep -> nut
- -> nut -> KK.rel_expr *)
and to_set_op connective connective3 set_oper true_set_oper false_set_oper
neg_second R u1 u2 =
let
@@ -1825,11 +1675,9 @@
r1 r2
| _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R]))
end
- (* typ -> rep -> (KK.int_expr -> KK.int_expr) -> KK.rel_expr *)
and to_bit_word_unary_op T R oper =
let
val Ts = strip_type T ||> single |> op @
- (* int -> KK.int_expr *)
fun int_arg j = int_expr_from_atom kk (nth Ts j) (KK.Var (1, j))
in
kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))
@@ -1837,12 +1685,9 @@
(map (fn j => KK.AssignIntReg (j, int_arg j)) (0 upto 1),
KK.IntEq (KK.IntReg 1, oper (KK.IntReg 0))))
end
- (* typ -> rep -> (KK.int_expr -> KK.int_expr -> KK.int_expr -> bool) option
- -> (KK.int_expr -> KK.int_expr -> KK.int_expr) option -> KK.rel_expr *)
and to_bit_word_binary_op T R opt_guard opt_oper =
let
val Ts = strip_type T ||> single |> op @
- (* int -> KK.int_expr *)
fun int_arg j = int_expr_from_atom kk (nth Ts j) (KK.Var (1, j))
in
kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))
@@ -1859,7 +1704,6 @@
[KK.IntEq (KK.IntReg 2,
oper (KK.IntReg 0) (KK.IntReg 1))]))))
end
- (* rep -> rep -> KK.rel_expr -> nut -> KK.rel_expr *)
and to_apply (R as Formula _) func_u arg_u =
raise REP ("Nitpick_Kodkod.to_apply", [R])
| to_apply res_R func_u arg_u =
@@ -1896,7 +1740,6 @@
(kk_n_fold_join kk true R1 R2 (to_opt R1 arg_u) (to_r func_u))
|> body_rep R2 = Formula Neut ? to_guard [arg_u] res_R
| _ => raise NUT ("Nitpick_Kodkod.to_apply", [func_u])
- (* int -> rep -> rep -> KK.rel_expr -> nut *)
and to_apply_vect k R' res_R func_r arg_u =
let
val arg_R = one_rep ofs (type_of arg_u) (unopt_rep (rep_of arg_u))
@@ -1906,10 +1749,8 @@
kk_case_switch kk arg_R res_R (to_opt arg_R arg_u)
(all_singletons_for_rep arg_R) vect_rs
end
- (* bool -> nut -> KK.formula *)
and to_could_be_unrep neg u =
if neg andalso is_opt_rep (rep_of u) then kk_no (to_r u) else KK.False
- (* nut -> KK.rel_expr -> KK.rel_expr *)
and to_compare_with_unrep u r =
if is_opt_rep (rep_of u) then
kk_rel_if (kk_some (to_r u)) r (empty_rel_for_rep (rep_of u))
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Apr 24 16:33:01 2010 +0200
@@ -16,7 +16,6 @@
show_skolems: bool,
show_datatypes: bool,
show_consts: bool}
-
type term_postprocessor =
Proof.context -> string -> (typ -> term list) -> typ -> term -> term
@@ -82,10 +81,8 @@
type atom_pool = ((string * int) * int list) list
-(* Proof.context -> ((string * string) * (string * string)) * Proof.context *)
fun add_wacky_syntax ctxt =
let
- (* term -> string *)
val name_of = fst o dest_Const
val thy = ProofContext.theory_of ctxt |> Context.reject_draft
val (maybe_t, thy) =
@@ -107,7 +104,6 @@
(** Term reconstruction **)
-(* atom_pool Unsynchronized.ref -> string -> int -> int -> string *)
fun nth_atom_suffix pool s j k =
(case AList.lookup (op =) (!pool) (s, k) of
SOME js =>
@@ -119,7 +115,6 @@
|> nat_subscript
|> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
? prefix "\<^isub>,"
-(* atom_pool Unsynchronized.ref -> string -> typ -> int -> int -> string *)
fun nth_atom_name pool prefix (Type (s, _)) j k =
let val s' = shortest_name s in
prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
@@ -129,18 +124,15 @@
prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix pool s j k
| nth_atom_name _ _ T _ _ =
raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
-(* atom_pool Unsynchronized.ref -> bool -> typ -> int -> int -> term *)
fun nth_atom pool for_auto T j k =
if for_auto then
Free (nth_atom_name pool (hd (space_explode "." nitpick_prefix)) T j k, T)
else
Const (nth_atom_name pool "" T j k, T)
-(* term -> real *)
fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) =
real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
| extract_real_number t = real (snd (HOLogic.dest_number t))
-(* term * term -> order *)
fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2)
| nice_term_ord tp = Real.compare (pairself extract_real_number tp)
handle TERM ("dest_number", _) =>
@@ -151,16 +143,12 @@
| ord => ord)
| _ => Term_Ord.fast_term_ord tp
-(* typ -> term_postprocessor -> theory -> theory *)
fun register_term_postprocessor T p = Data.map (cons (T, p))
-(* typ -> theory -> theory *)
fun unregister_term_postprocessor T = Data.map (AList.delete (op =) T)
-(* nut NameTable.table -> KK.raw_bound list -> nut -> int list list *)
fun tuple_list_for_name rel_table bounds name =
the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
-(* term -> term *)
fun unarize_unbox_etc_term (Const (@{const_name FinFun}, _) $ t1) =
unarize_unbox_etc_term t1
| unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
@@ -185,7 +173,6 @@
| unarize_unbox_etc_term (Abs (s, T, t')) =
Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t')
-(* typ -> typ -> (typ * typ) * (typ * typ) *)
fun factor_out_types (T1 as Type (@{type_name "*"}, [T11, T12]))
(T2 as Type (@{type_name "*"}, [T21, T22])) =
let val (n1, n2) = pairself num_factors_in_type (T11, T21) in
@@ -210,25 +197,20 @@
((T1, NONE), (T21, SOME T22))
| factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
-(* bool -> typ -> typ -> (term * term) list -> term *)
fun make_plain_fun maybe_opt T1 T2 =
let
- (* typ -> typ -> (term * term) list -> term *)
fun aux T1 T2 [] =
Const (if maybe_opt then opt_flag else non_opt_flag, T1 --> T2)
| aux T1 T2 ((t1, t2) :: tps) =
Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
$ aux T1 T2 tps $ t1 $ t2
in aux T1 T2 o rev end
-(* term -> bool *)
fun is_plain_fun (Const (s, _)) = (s = opt_flag orelse s = non_opt_flag)
| is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
is_plain_fun t0
| is_plain_fun _ = false
-(* term -> bool * (term list * term list) *)
val dest_plain_fun =
let
- (* term -> bool * (term list * term list) *)
fun aux (Abs (_, _, Const (s, _))) = (s <> irrelevant, ([], []))
| aux (Const (s, _)) = (s <> non_opt_flag, ([], []))
| aux (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
@@ -238,7 +220,6 @@
| aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
in apsnd (pairself rev) o aux end
-(* typ -> typ -> typ -> term -> term * term *)
fun break_in_two T T1 T2 t =
let
val ps = HOLogic.flat_tupleT_paths T
@@ -246,7 +227,6 @@
val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2)
val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
-(* typ -> term -> term -> term *)
fun pair_up (Type (@{type_name "*"}, [T1', T2']))
(t1 as Const (@{const_name Pair},
Type (@{type_name fun},
@@ -255,13 +235,10 @@
if T1 = T1' then HOLogic.mk_prod (t1, t2)
else HOLogic.mk_prod (t11, pair_up T2' t12 t2)
| pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2)
-(* typ -> term -> term list * term list -> (term * term) list*)
fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3
-(* typ -> typ -> typ -> term -> term *)
fun typecast_fun (Type (@{type_name fun}, [T1', T2'])) T1 T2 t =
let
- (* typ -> typ -> typ -> typ -> term -> term *)
fun do_curry T1 T1a T1b T2 t =
let
val (maybe_opt, tsp) = dest_plain_fun t
@@ -271,7 +248,6 @@
|> AList.coalesce (op =)
|> map (apsnd (make_plain_fun maybe_opt T1b T2))
in make_plain_fun maybe_opt T1a (T1b --> T2) tps end
- (* typ -> typ -> term -> term *)
and do_uncurry T1 T2 t =
let
val (maybe_opt, tsp) = dest_plain_fun t
@@ -280,7 +256,6 @@
|> maps (fn (t1, t2) =>
multi_pair_up T1 t1 (snd (dest_plain_fun t2)))
in make_plain_fun maybe_opt T1 T2 tps end
- (* typ -> typ -> typ -> typ -> term -> term *)
and do_arrow T1' T2' _ _ (Const (s, _)) = Const (s, T1' --> T2')
| do_arrow T1' T2' T1 T2
(Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
@@ -297,7 +272,6 @@
| ((T1a', SOME T1b'), (_, NONE)) =>
t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
| _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])
- (* typ -> typ -> term -> term *)
and do_term (Type (@{type_name fun}, [T1', T2']))
(Type (@{type_name fun}, [T1, T2])) t =
do_fun T1' T2' T1 T2 t
@@ -313,33 +287,25 @@
| typecast_fun T' _ _ _ =
raise TYPE ("Nitpick_Model.typecast_fun", [T'], [])
-(* term -> string *)
fun truth_const_sort_key @{const True} = "0"
| truth_const_sort_key @{const False} = "2"
| truth_const_sort_key _ = "1"
-(* typ -> term list -> term *)
fun mk_tuple (Type (@{type_name "*"}, [T1, T2])) ts =
HOLogic.mk_prod (mk_tuple T1 ts,
mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1))))
| mk_tuple _ (t :: _) = t
| mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
-(* theory -> typ * typ -> bool *)
fun varified_type_match thy (candid_T, pat_T) =
strict_type_match thy (candid_T, Logic.varifyT_global pat_T)
-(* atom_pool -> (string * string) * (string * string) -> scope -> nut list
- -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
- -> term list *)
fun all_values_of_type pool wacky_names (scope as {card_assigns, ...} : scope)
sel_names rel_table bounds card T =
let
val card = if card = 0 then card_of_type card_assigns T else card
- (* nat -> term *)
fun nth_value_of_type n =
let
- (* bool -> term *)
fun term unfold =
reconstruct_term unfold pool wacky_names scope sel_names rel_table
bounds T T (Atom (card, 0)) [[n]]
@@ -353,15 +319,11 @@
| t => t
end
in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
-(* bool -> atom_pool -> (string * string) * (string * string) -> scope
- -> nut list -> nut list -> nut list -> nut NameTable.table
- -> KK.raw_bound list -> typ -> typ -> rep -> int list list -> term *)
and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _))
(scope as {hol_ctxt as {ctxt, thy, stds, ...}, binarize, card_assigns,
bits, datatypes, ofs, ...}) sel_names rel_table bounds =
let
val for_auto = (maybe_name = "")
- (* int list list -> int *)
fun value_of_bits jss =
let
val j0 = offset_of_type ofs @{typ unsigned_bit}
@@ -370,10 +332,8 @@
fold (fn j => Integer.add (reasonable_power 2 j |> j = bits ? op ~))
js 0
end
- (* typ -> term list *)
val all_values =
all_values_of_type pool wacky_names scope sel_names rel_table bounds 0
- (* typ -> term -> term *)
fun postprocess_term (Type (@{type_name fun}, _)) = I
| postprocess_term T =
if null (Data.get thy) then
@@ -381,7 +341,6 @@
else case AList.lookup (varified_type_match thy) (Data.get thy) T of
SOME postproc => postproc ctxt maybe_name all_values T
| NONE => I
- (* typ list -> term -> term *)
fun postprocess_subterms Ts (t1 $ t2) =
let val t = postprocess_subterms Ts t1 $ postprocess_subterms Ts t2 in
postprocess_term (fastype_of1 (Ts, t)) t
@@ -389,13 +348,11 @@
| postprocess_subterms Ts (Abs (s, T, t')) =
Abs (s, T, postprocess_subterms (T :: Ts) t')
| postprocess_subterms Ts t = postprocess_term (fastype_of1 (Ts, t)) t
- (* bool -> typ -> typ -> (term * term) list -> term *)
fun make_set maybe_opt T1 T2 tps =
let
val empty_const = Const (@{const_abbrev Set.empty}, T1 --> T2)
val insert_const = Const (@{const_name insert},
T1 --> (T1 --> T2) --> T1 --> T2)
- (* (term * term) list -> term *)
fun aux [] =
if maybe_opt andalso not (is_complete_type datatypes false T1) then
insert_const $ Const (unrep, T1) $ empty_const
@@ -416,12 +373,10 @@
else
aux tps
end
- (* bool -> typ -> typ -> typ -> (term * term) list -> term *)
fun make_map maybe_opt T1 T2 T2' =
let
val update_const = Const (@{const_name fun_upd},
(T1 --> T2) --> T1 --> T2 --> T1 --> T2)
- (* (term * term) list -> term *)
fun aux' [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
| aux' ((t1, t2) :: tps) =
(case t2 of
@@ -434,7 +389,6 @@
else
aux' tps
in aux end
- (* typ list -> term -> term *)
fun polish_funs Ts t =
(case fastype_of1 (Ts, t) of
Type (@{type_name fun}, [T1, T2]) =>
@@ -475,7 +429,6 @@
else
t
| t => t
- (* bool -> typ -> typ -> typ -> term list -> term list -> term *)
fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
|> make_plain_fun maybe_opt T1 T2
@@ -483,7 +436,6 @@
|> typecast_fun (uniterize_unarize_unbox_etc_type T')
(uniterize_unarize_unbox_etc_type T1)
(uniterize_unarize_unbox_etc_type T2)
- (* (typ * int) list -> typ -> typ -> int -> term *)
fun term_for_atom seen (T as Type (@{type_name fun}, [T1, T2])) T' j _ =
let
val k1 = card_of_type card_assigns T1
@@ -524,10 +476,8 @@
| SOME {deep = false, ...} => nth_atom pool for_auto T j k
| SOME {co, standard, constrs, ...} =>
let
- (* styp -> int list *)
fun tuples_for_const (s, T) =
tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
- (* unit -> term *)
fun cyclic_atom () =
nth_atom pool for_auto (Type (cyclic_type_name, [])) j k
fun cyclic_var () = Var ((nth_atom_name pool "" T j k, 0), T)
@@ -616,14 +566,11 @@
t
end
end
- (* (typ * int) list -> int -> rep -> typ -> typ -> typ -> int list
- -> term *)
and term_for_vect seen k R T1 T2 T' js =
make_fun true T1 T2 T'
(map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
(map (term_for_rep true seen T2 T2 R o single)
(batch_list (arity_of_rep R) js))
- (* bool -> (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
and term_for_rep _ seen T T' Unit [[]] = term_for_atom seen T T' 0 1
| term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
@@ -675,14 +622,12 @@
(** Constant postprocessing **)
-(* int -> typ -> typ list *)
fun dest_n_tuple_type 1 T = [T]
| dest_n_tuple_type n (Type (_, [T1, T2])) =
T1 :: dest_n_tuple_type (n - 1) T2
| dest_n_tuple_type _ T =
raise TYPE ("Nitpick_Model.dest_n_tuple_type", [T], [])
-(* theory -> const_table -> styp -> int list *)
fun const_format thy def_table (x as (s, T)) =
if String.isPrefix unrolled_prefix s then
const_format thy def_table (original_name s, range_type T)
@@ -702,7 +647,6 @@
else
[num_binder_types T]
| NONE => [num_binder_types T]
-(* int list -> int list -> int list *)
fun intersect_formats _ [] = []
| intersect_formats [] _ = []
| intersect_formats ks1 ks2 =
@@ -712,7 +656,6 @@
[Int.min (k1, k2)]
end
-(* theory -> const_table -> (term option * int list) list -> term -> int list *)
fun lookup_format thy def_table formats t =
case AList.lookup (fn (SOME x, SOME y) =>
(term_match thy) (x, y) | _ => false)
@@ -725,7 +668,6 @@
| _ => format
end
-(* int list -> int list -> typ -> typ *)
fun format_type default_format format T =
let
val T = uniterize_unarize_unbox_etc_type T
@@ -743,28 +685,22 @@
|> map (HOLogic.mk_tupleT o rev)
in List.foldl (op -->) body_T batched end
end
-(* theory -> const_table -> (term option * int list) list -> term -> typ *)
fun format_term_type thy def_table formats t =
format_type (the (AList.lookup (op =) formats NONE))
(lookup_format thy def_table formats t) (fastype_of t)
-(* int list -> int -> int list -> int list *)
fun repair_special_format js m format =
m - 1 downto 0 |> chunk_list_unevenly (rev format)
|> map (rev o filter_out (member (op =) js))
|> filter_out null |> map length |> rev
-(* hol_context -> string * string -> (term option * int list) list
- -> styp -> term * typ *)
fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
: hol_context) (base_name, step_name) formats =
let
val default_format = the (AList.lookup (op =) formats NONE)
- (* styp -> term * typ *)
fun do_const (x as (s, T)) =
(if String.isPrefix special_prefix s then
let
- (* term -> term *)
val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
val (x' as (_, T'), js, ts) =
AList.find (op =) (!special_funs) (s, unarize_unbox_etc_type T)
@@ -773,7 +709,6 @@
val Ts = List.take (binder_types T', max_j + 1)
val missing_js = filter_out (member (op =) js) (0 upto max_j)
val missing_Ts = filter_indices missing_js Ts
- (* int -> indexname *)
fun nth_missing_var n =
((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n)
val missing_vars = map nth_missing_var (0 upto length missing_js - 1)
@@ -865,7 +800,6 @@
|>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
in do_const end
-(* styp -> string *)
fun assign_operator_for_const (s, T) =
if String.isPrefix ubfp_prefix s then
if is_fun_type T then "\<subseteq>" else "\<le>"
@@ -878,8 +812,6 @@
(** Model reconstruction **)
-(* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
- -> nut -> term *)
fun term_for_name pool scope sel_names rel_table bounds name =
let val T = type_of name in
tuple_list_for_name rel_table bounds name
@@ -887,13 +819,11 @@
rel_table bounds T T (rep_of name)
end
-(* term -> term *)
fun unfold_outer_the_binders (t as Const (@{const_name The}, _)
$ Abs (s, T, Const (@{const_name "op ="}, _)
$ Bound 0 $ t')) =
betapply (Abs (s, T, t'), t) |> unfold_outer_the_binders
| unfold_outer_the_binders t = t
-(* typ list -> int -> term * term -> bool *)
fun bisimilar_values _ 0 _ = true
| bisimilar_values coTs max_depth (t1, t2) =
let val T = fastype_of t1 in
@@ -910,9 +840,6 @@
t1 = t2
end
-(* params -> scope -> (term option * int list) list -> styp list -> nut list
- -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
- -> Pretty.T * bool *)
fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
debug, binary_ints, destroy_constrs, specialize,
@@ -945,13 +872,10 @@
val scope = {hol_ctxt = hol_ctxt, binarize = binarize,
card_assigns = card_assigns, bits = bits,
bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
- (* bool -> typ -> typ -> rep -> int list list -> term *)
fun term_for_rep unfold =
reconstruct_term unfold pool wacky_names scope sel_names rel_table bounds
- (* nat -> typ -> nat -> term *)
fun nth_value_of_type card T n =
let
- (* bool -> term *)
fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]]
in
case aux false of
@@ -962,10 +886,8 @@
t
| t => t
end
- (* nat -> typ -> term list *)
val all_values =
all_values_of_type pool wacky_names scope sel_names rel_table bounds
- (* dtype_spec list -> dtype_spec -> bool *)
fun is_codatatype_wellformed (cos : dtype_spec list)
({typ, card, ...} : dtype_spec) =
let
@@ -975,7 +897,6 @@
forall (not o bisimilar_values (map #typ cos) max_depth)
(all_distinct_unordered_pairs_of ts)
end
- (* string -> Pretty.T *)
fun pretty_for_assign name =
let
val (oper, (t1, T'), T) =
@@ -999,7 +920,6 @@
[setmp_show_all_types (Syntax.pretty_term ctxt) t1,
Pretty.str oper, Syntax.pretty_term ctxt t2])
end
- (* dtype_spec -> Pretty.T *)
fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
Pretty.block (Pretty.breaks
(Syntax.pretty_typ ctxt (uniterize_unarize_unbox_etc_type typ) ::
@@ -1013,7 +933,6 @@
(map (Syntax.pretty_term ctxt) (all_values card typ) @
(if fun_from_pair complete false then []
else [Pretty.str unrep]))]))
- (* typ -> dtype_spec list *)
fun integer_datatype T =
[{typ = T, card = card_of_type card_assigns T, co = false,
standard = true, complete = (false, false), concrete = (true, true),
@@ -1036,7 +955,6 @@
(map pretty_for_datatype codatatypes)]
else
[]
- (* bool -> string -> nut list -> Pretty.T list *)
fun block_of_names show title names =
if show andalso not (null names) then
Pretty.str (title ^ plural_s_for_list names ^ ":")
@@ -1075,17 +993,13 @@
forall (is_codatatype_wellformed codatatypes) codatatypes)
end
-(* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
- -> KK.raw_bound list -> term -> bool option *)
fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...},
card_assigns, ...})
auto_timeout free_names sel_names rel_table bounds prop =
let
val pool = Unsynchronized.ref []
- (* typ * int -> term *)
fun free_type_assm (T, k) =
let
- (* int -> term *)
fun atom j = nth_atom pool true T j k
fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j
val eqs = map equation_for_atom (index_seq 0 k)
@@ -1094,14 +1008,12 @@
$ Abs ("x", T, foldl1 HOLogic.mk_disj eqs)
val distinct_assm = distinctness_formula T (map atom (index_seq 0 k))
in s_conj (compreh_assm, distinct_assm) end
- (* nut -> term *)
fun free_name_assm name =
HOLogic.mk_eq (Free (nickname_of name, type_of name),
term_for_name pool scope sel_names rel_table bounds name)
val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
val model_assms = map free_name_assm free_names
val assm = foldr1 s_conj (freeT_assms @ model_assms)
- (* bool -> bool *)
fun try_out negate =
let
val concl = (negate ? curry (op $) @{const Not})
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Sat Apr 24 16:33:01 2010 +0200
@@ -54,55 +54,42 @@
exception MTYPE of string * mtyp list * typ list
exception MTERM of string * mterm list
-(* string -> unit *)
fun print_g (_ : string) = ()
(* val print_g = tracing *)
-(* var -> string *)
val string_for_var = signed_string_of_int
-(* string -> var list -> string *)
fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>"
| string_for_vars sep xs = space_implode sep (map string_for_var xs)
fun subscript_string_for_vars sep xs =
if null xs then "" else "\<^bsub>" ^ string_for_vars sep xs ^ "\<^esub>"
-(* sign -> string *)
fun string_for_sign Plus = "+"
| string_for_sign Minus = "-"
-(* sign -> sign -> sign *)
fun xor sn1 sn2 = if sn1 = sn2 then Plus else Minus
-(* sign -> sign *)
val negate = xor Minus
-(* sign_atom -> string *)
fun string_for_sign_atom (S sn) = string_for_sign sn
| string_for_sign_atom (V x) = string_for_var x
-(* literal -> string *)
fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn
val bool_M = MType (@{type_name bool}, [])
val dummy_M = MType (nitpick_prefix ^ "dummy", [])
-(* mtyp -> bool *)
fun is_MRec (MRec _) = true
| is_MRec _ = false
-(* mtyp -> mtyp * sign_atom * mtyp *)
fun dest_MFun (MFun z) = z
| dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M], [])
val no_prec = 100
-(* mtyp -> int *)
fun precedence_of_mtype (MFun _) = 1
| precedence_of_mtype (MPair _) = 2
| precedence_of_mtype _ = no_prec
-(* mtyp -> string *)
val string_for_mtype =
let
- (* int -> mtyp -> string *)
fun aux outer_prec M =
let
val prec = precedence_of_mtype M
@@ -126,22 +113,17 @@
end
in aux 0 end
-(* mtyp -> mtyp list *)
fun flatten_mtype (MPair (M1, M2)) = maps flatten_mtype [M1, M2]
| flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms
| flatten_mtype M = [M]
-(* mterm -> bool *)
fun precedence_of_mterm (MRaw _) = no_prec
| precedence_of_mterm (MAbs _) = 1
| precedence_of_mterm (MApp _) = 2
-(* Proof.context -> mterm -> string *)
fun string_for_mterm ctxt =
let
- (* mtype -> string *)
fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>"
- (* int -> mterm -> string *)
fun aux outer_prec m =
let
val prec = precedence_of_mterm m
@@ -158,7 +140,6 @@
end
in aux 0 end
-(* mterm -> mtyp *)
fun mtype_of_mterm (MRaw (_, M)) = M
| mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m)
| mtype_of_mterm (MApp (m1, _)) =
@@ -166,29 +147,24 @@
MFun (_, _, M12) => M12
| M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1], [])
-(* mterm -> mterm * mterm list *)
fun strip_mcomb (MApp (m1, m2)) = strip_mcomb m1 ||> (fn ms => append ms [m2])
| strip_mcomb m = (m, [])
-(* hol_context -> bool -> bool -> typ -> mdata *)
fun initial_mdata hol_ctxt binarize no_harmless alpha_T =
({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
no_harmless = no_harmless, max_fresh = Unsynchronized.ref 0,
datatype_mcache = Unsynchronized.ref [],
constr_mcache = Unsynchronized.ref []} : mdata)
-(* typ -> typ -> bool *)
fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
T = alpha_T orelse (not (is_fp_iterator_type T) andalso
exists (could_exist_alpha_subtype alpha_T) Ts)
| could_exist_alpha_subtype alpha_T T = (T = alpha_T)
-(* theory -> typ -> typ -> bool *)
fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
could_exist_alpha_subtype alpha_T T
| could_exist_alpha_sub_mtype thy alpha_T T =
(T = alpha_T orelse is_datatype thy [(NONE, true)] T)
-(* mtyp -> bool *)
fun exists_alpha_sub_mtype MAlpha = true
| exists_alpha_sub_mtype (MFun (M1, _, M2)) =
exists exists_alpha_sub_mtype [M1, M2]
@@ -197,7 +173,6 @@
| exists_alpha_sub_mtype (MType (_, Ms)) = exists exists_alpha_sub_mtype Ms
| exists_alpha_sub_mtype (MRec _) = true
-(* mtyp -> bool *)
fun exists_alpha_sub_mtype_fresh MAlpha = true
| exists_alpha_sub_mtype_fresh (MFun (_, V _, _)) = true
| exists_alpha_sub_mtype_fresh (MFun (_, _, M2)) =
@@ -208,11 +183,9 @@
exists exists_alpha_sub_mtype_fresh Ms
| exists_alpha_sub_mtype_fresh (MRec _) = true
-(* string * typ list -> mtyp list -> mtyp *)
fun constr_mtype_for_binders z Ms =
fold_rev (fn M => curry3 MFun M (S Minus)) Ms (MRec z)
-(* ((string * typ list) * mtyp) list -> mtyp list -> mtyp -> mtyp *)
fun repair_mtype _ _ MAlpha = MAlpha
| repair_mtype cache seen (MFun (M1, a, M2)) =
MFun (repair_mtype cache seen M1, a, repair_mtype cache seen M2)
@@ -226,30 +199,24 @@
| M => if member (op =) seen M then MType (s, [])
else repair_mtype cache (M :: seen) M
-(* ((string * typ list) * mtyp) list Unsynchronized.ref -> unit *)
fun repair_datatype_mcache cache =
let
- (* (string * typ list) * mtyp -> unit *)
fun repair_one (z, M) =
Unsynchronized.change cache
(AList.update (op =) (z, repair_mtype (!cache) [] M))
in List.app repair_one (rev (!cache)) end
-(* (typ * mtyp) list -> (styp * mtyp) list Unsynchronized.ref -> unit *)
fun repair_constr_mcache dtype_cache constr_mcache =
let
- (* styp * mtyp -> unit *)
fun repair_one (x, M) =
Unsynchronized.change constr_mcache
(AList.update (op =) (x, repair_mtype dtype_cache [] M))
in List.app repair_one (!constr_mcache) end
-(* typ -> bool *)
fun is_fin_fun_supported_type @{typ prop} = true
| is_fin_fun_supported_type @{typ bool} = true
| is_fin_fun_supported_type (Type (@{type_name option}, _)) = true
| is_fin_fun_supported_type _ = false
-(* typ -> typ -> term -> term option *)
fun fin_fun_body _ _ (t as @{term False}) = SOME t
| fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
| fin_fun_body dom_T ran_T
@@ -265,7 +232,6 @@
$ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
| fin_fun_body _ _ _ = NONE
-(* mdata -> bool -> typ -> typ -> mtyp * sign_atom * mtyp *)
fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus
T1 T2 =
let
@@ -277,12 +243,10 @@
else
S Minus
in (M1, a, M2) end
-(* mdata -> bool -> typ -> mtyp *)
and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
datatype_mcache, constr_mcache, ...})
all_minus =
let
- (* typ -> mtyp *)
fun do_type T =
if T = alpha_T then
MAlpha
@@ -329,21 +293,17 @@
| _ => MType (Refute.string_of_typ T, [])
in do_type end
-(* mtyp -> mtyp list *)
fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
| prodM_factors M = [M]
-(* mtyp -> mtyp list * mtyp *)
fun curried_strip_mtype (MFun (M1, _, M2)) =
curried_strip_mtype M2 |>> append (prodM_factors M1)
| curried_strip_mtype M = ([], M)
-(* string -> mtyp -> mtyp *)
fun sel_mtype_from_constr_mtype s M =
let val (arg_Ms, dataM) = curried_strip_mtype M in
MFun (dataM, S Minus,
case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
end
-(* mdata -> styp -> mtyp *)
fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_mcache,
...}) (x as (_, T)) =
if could_exist_alpha_sub_mtype thy alpha_T T then
@@ -362,14 +322,11 @@
x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
|> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
-(* literal list -> sign_atom -> sign_atom *)
fun resolve_sign_atom lits (V x) =
x |> AList.lookup (op =) lits |> Option.map S |> the_default (V x)
| resolve_sign_atom _ a = a
-(* literal list -> mtyp -> mtyp *)
fun resolve_mtype lits =
let
- (* mtyp -> mtyp *)
fun aux MAlpha = MAlpha
| aux (MFun (M1, a, M2)) = MFun (aux M1, resolve_sign_atom lits a, aux M2)
| aux (MPair Mp) = MPair (pairself aux Mp)
@@ -384,24 +341,19 @@
type constraint_set = literal list * comp list * sign_expr list
-(* comp_op -> string *)
fun string_for_comp_op Eq = "="
| string_for_comp_op Leq = "\<le>"
-(* sign_expr -> string *)
fun string_for_sign_expr [] = "\<bot>"
| string_for_sign_expr lits =
space_implode " \<or> " (map string_for_literal lits)
-(* literal -> literal list option -> literal list option *)
fun do_literal _ NONE = NONE
| do_literal (x, sn) (SOME lits) =
case AList.lookup (op =) lits x of
SOME sn' => if sn = sn' then SOME lits else NONE
| NONE => SOME ((x, sn) :: lits)
-(* comp_op -> var list -> sign_atom -> sign_atom -> literal list * comp list
- -> (literal list * comp list) option *)
fun do_sign_atom_comp Eq [] a1 a2 (accum as (lits, comps)) =
(case (a1, a2) of
(S sn1, S sn2) => if sn1 = sn2 then SOME accum else NONE
@@ -419,8 +371,6 @@
| do_sign_atom_comp cmp xs a1 a2 (lits, comps) =
SOME (lits, insert (op =) (a1, a2, cmp, xs) comps)
-(* comp -> var list -> mtyp -> mtyp -> (literal list * comp list) option
- -> (literal list * comp list) option *)
fun do_mtype_comp _ _ _ _ NONE = NONE
| do_mtype_comp _ _ MAlpha MAlpha accum = accum
| do_mtype_comp Eq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
@@ -450,7 +400,6 @@
raise MTYPE ("Nitpick_Mono.do_mtype_comp (" ^ string_for_comp_op cmp ^ ")",
[M1, M2], [])
-(* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *)
fun add_mtype_comp cmp M1 M2 ((lits, comps, sexps) : constraint_set) =
(print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^
" " ^ string_for_mtype M2);
@@ -458,12 +407,9 @@
NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ())
| SOME (lits, comps) => (lits, comps, sexps))
-(* mtyp -> mtyp -> constraint_set -> constraint_set *)
val add_mtypes_equal = add_mtype_comp Eq
val add_is_sub_mtype = add_mtype_comp Leq
-(* sign -> sign_expr -> mtyp -> (literal list * sign_expr list) option
- -> (literal list * sign_expr list) option *)
fun do_notin_mtype_fv _ _ _ NONE = NONE
| do_notin_mtype_fv Minus _ MAlpha accum = accum
| do_notin_mtype_fv Plus [] MAlpha _ = NONE
@@ -499,7 +445,6 @@
| do_notin_mtype_fv _ _ M _ =
raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
-(* sign -> mtyp -> constraint_set -> constraint_set *)
fun add_notin_mtype_fv sn M ((lits, comps, sexps) : constraint_set) =
(print_g ("*** Add " ^ string_for_mtype M ^ " is " ^
(case sn of Minus => "concrete" | Plus => "complete") ^ ".");
@@ -507,31 +452,23 @@
NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ())
| SOME (lits, sexps) => (lits, comps, sexps))
-(* mtyp -> constraint_set -> constraint_set *)
val add_mtype_is_concrete = add_notin_mtype_fv Minus
val add_mtype_is_complete = add_notin_mtype_fv Plus
val bool_from_minus = true
-(* sign -> bool *)
fun bool_from_sign Plus = not bool_from_minus
| bool_from_sign Minus = bool_from_minus
-(* bool -> sign *)
fun sign_from_bool b = if b = bool_from_minus then Minus else Plus
-(* literal -> PropLogic.prop_formula *)
fun prop_for_literal (x, sn) =
(not (bool_from_sign sn) ? PropLogic.Not) (PropLogic.BoolVar x)
-(* sign_atom -> PropLogic.prop_formula *)
fun prop_for_sign_atom_eq (S sn', sn) =
if sn = sn' then PropLogic.True else PropLogic.False
| prop_for_sign_atom_eq (V x, sn) = prop_for_literal (x, sn)
-(* sign_expr -> PropLogic.prop_formula *)
fun prop_for_sign_expr xs = PropLogic.exists (map prop_for_literal xs)
-(* var list -> sign -> PropLogic.prop_formula *)
fun prop_for_exists_eq xs sn =
PropLogic.exists (map (fn x => prop_for_literal (x, sn)) xs)
-(* comp -> PropLogic.prop_formula *)
fun prop_for_comp (a1, a2, Eq, []) =
PropLogic.SAnd (prop_for_comp (a1, a2, Leq, []),
prop_for_comp (a2, a1, Leq, []))
@@ -541,7 +478,6 @@
| prop_for_comp (a1, a2, cmp, xs) =
PropLogic.SOr (prop_for_exists_eq xs Minus, prop_for_comp (a1, a2, cmp, []))
-(* var -> (int -> bool option) -> literal list -> literal list *)
fun literals_from_assignments max_var assigns lits =
fold (fn x => fn accum =>
if AList.defined (op =) lits x then
@@ -550,18 +486,15 @@
SOME b => (x, sign_from_bool b) :: accum
| NONE => accum) (max_var downto 1) lits
-(* comp -> string *)
fun string_for_comp (a1, a2, cmp, xs) =
string_for_sign_atom a1 ^ " " ^ string_for_comp_op cmp ^
subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_sign_atom a2
-(* literal list -> comp list -> sign_expr list -> unit *)
fun print_problem lits comps sexps =
print_g ("*** Problem:\n" ^ cat_lines (map string_for_literal lits @
map string_for_comp comps @
map string_for_sign_expr sexps))
-(* literal list -> unit *)
fun print_solution lits =
let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in
print_g ("*** Solution:\n" ^
@@ -569,10 +502,8 @@
"-: " ^ commas (map (string_for_var o fst) neg))
end
-(* var -> constraint_set -> literal list option *)
fun solve max_var (lits, comps, sexps) =
let
- (* (int -> bool option) -> literal list option *)
fun do_assigns assigns =
SOME (literals_from_assignments max_var assigns lits
|> tap print_solution)
@@ -607,27 +538,21 @@
val initial_gamma = {bound_Ts = [], bound_Ms = [], frees = [], consts = []}
-(* typ -> mtyp -> mtype_context -> mtype_context *)
fun push_bound T M {bound_Ts, bound_Ms, frees, consts} =
{bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms, frees = frees,
consts = consts}
-(* mtype_context -> mtype_context *)
fun pop_bound {bound_Ts, bound_Ms, frees, consts} =
{bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms, frees = frees,
consts = consts}
handle List.Empty => initial_gamma (* FIXME: needed? *)
-(* mdata -> term -> accumulator -> mterm * accumulator *)
fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
def_table, ...},
alpha_T, max_fresh, ...}) =
let
- (* typ -> mtyp *)
val mtype_for = fresh_mtype_for_type mdata false
- (* mtyp -> mtyp *)
fun plus_set_mtype_for_dom M =
MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
- (* typ -> accumulator -> mterm * accumulator *)
fun do_all T (gamma, cset) =
let
val abs_M = mtype_for (domain_type (domain_type T))
@@ -656,7 +581,6 @@
let
val set_T = domain_type T
val set_M = mtype_for set_T
- (* typ -> mtyp *)
fun custom_mtype_for (T as Type (@{type_name fun}, [T1, T2])) =
if T = set_T then set_M
else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2)
@@ -664,20 +588,16 @@
in
(custom_mtype_for T, (gamma, cset |> add_mtype_is_concrete set_M))
end
- (* typ -> accumulator -> mtyp * accumulator *)
fun do_pair_constr T accum =
case mtype_for (nth_range_type 2 T) of
M as MPair (a_M, b_M) =>
(MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum)
| M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M], [])
- (* int -> typ -> accumulator -> mtyp * accumulator *)
fun do_nth_pair_sel n T =
case mtype_for (domain_type T) of
M as MPair (a_M, b_M) =>
pair (MFun (M, S Minus, if n = 0 then a_M else b_M))
| M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
- (* term -> string -> typ -> term -> term -> term -> accumulator
- -> mterm * accumulator *)
fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
let
val abs_M = mtype_for abs_T
@@ -697,7 +617,6 @@
MApp (bound_m, MRaw (Bound 0, M1))),
body_m))), accum)
end
- (* term -> accumulator -> mterm * accumulator *)
and do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
cset)) =
(case t of
@@ -747,7 +666,6 @@
| @{const_name converse} =>
let
val x = Unsynchronized.inc max_fresh
- (* typ -> mtyp *)
fun mtype_for_set T =
MFun (mtype_for (domain_type T), V x, bool_M)
val ab_set_M = domain_type T |> mtype_for_set
@@ -757,7 +675,6 @@
| @{const_name rel_comp} =>
let
val x = Unsynchronized.inc max_fresh
- (* typ -> mtyp *)
fun mtype_for_set T =
MFun (mtype_for (domain_type T), V x, bool_M)
val bc_set_M = domain_type T |> mtype_for_set
@@ -783,7 +700,6 @@
| @{const_name Sigma} =>
let
val x = Unsynchronized.inc max_fresh
- (* typ -> mtyp *)
fun mtype_for_set T =
MFun (mtype_for (domain_type T), V x, bool_M)
val a_set_T = domain_type T
@@ -891,14 +807,12 @@
string_for_mterm ctxt m))
in do_term end
-(* int -> mtyp -> accumulator -> accumulator *)
fun force_minus_funs 0 _ = I
| force_minus_funs n (M as MFun (M1, _, M2)) =
add_mtypes_equal M (MFun (M1, S Minus, M2))
#> force_minus_funs (n - 1) M2
| force_minus_funs _ M =
raise MTYPE ("Nitpick_Mono.force_minus_funs", [M], [])
-(* mdata -> bool -> styp -> term -> term -> mterm * accumulator *)
fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum =
let
val (m1, accum) = consider_term mdata t1 accum
@@ -918,17 +832,12 @@
accum)
end
-(* mdata -> sign -> term -> accumulator -> mterm * accumulator *)
fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) =
let
- (* typ -> mtyp *)
val mtype_for = fresh_mtype_for_type mdata false
- (* term -> accumulator -> mterm * accumulator *)
val do_term = consider_term mdata
- (* sign -> term -> accumulator -> mterm * accumulator *)
fun do_formula sn t accum =
let
- (* styp -> string -> typ -> term -> mterm * accumulator *)
fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
let
val abs_M = mtype_for abs_T
@@ -944,7 +853,6 @@
MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
accum |>> pop_bound)
end
- (* styp -> term -> term -> mterm * accumulator *)
fun do_equals x t1 t2 =
case sn of
Plus => do_term t accum
@@ -1005,7 +913,6 @@
[@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
val bounteous_consts = [@{const_name bisim}]
-(* mdata -> term -> bool *)
fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false
| is_harmless_axiom {hol_ctxt = {thy, stds, fast_descrs, ...}, ...} t =
Term.add_consts t []
@@ -1013,12 +920,10 @@
|> (forall (member (op =) harmless_consts o original_name o fst) orf
exists (member (op =) bounteous_consts o fst))
-(* mdata -> term -> accumulator -> mterm * accumulator *)
fun consider_nondefinitional_axiom mdata t =
if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
else consider_general_formula mdata Plus t
-(* mdata -> term -> accumulator -> mterm * accumulator *)
fun consider_definitional_axiom (mdata as {hol_ctxt = {thy, ...}, ...}) t =
if not (is_constr_pattern_formula thy t) then
consider_nondefinitional_axiom mdata t
@@ -1026,11 +931,8 @@
pair (MRaw (t, dummy_M))
else
let
- (* typ -> mtyp *)
val mtype_for = fresh_mtype_for_type mdata false
- (* term -> accumulator -> mterm * accumulator *)
val do_term = consider_term mdata
- (* term -> string -> typ -> term -> accumulator -> mterm * accumulator *)
fun do_all quant_t abs_s abs_T body_t accum =
let
val abs_M = mtype_for abs_T
@@ -1043,7 +945,6 @@
MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
accum |>> pop_bound)
end
- (* term -> term -> term -> accumulator -> mterm * accumulator *)
and do_conjunction t0 t1 t2 accum =
let
val (m1, accum) = do_formula t1 accum
@@ -1058,7 +959,6 @@
in
(MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
end
- (* term -> accumulator -> accumulator *)
and do_formula t accum =
case t of
(t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
@@ -1083,22 +983,17 @@
\do_formula", [t])
in do_formula t end
-(* Proof.context -> literal list -> term -> mtyp -> string *)
fun string_for_mtype_of_term ctxt lits t M =
Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype lits M)
-(* theory -> literal list -> mtype_context -> unit *)
fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
|> cat_lines |> print_g
-(* ('a -> 'b -> 'c * 'd) -> 'a -> 'c list * 'b -> 'c list * 'd *)
fun amass f t (ms, accum) =
let val (m, accum) = f t accum in (m :: ms, accum) end
-(* string -> bool -> hol_context -> bool -> typ -> term list * term list
- -> (literal list * (mterm list * mterm list) * (styp * mtyp) list) option *)
fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
(nondef_ts, def_ts) =
let
@@ -1127,15 +1022,11 @@
| MTERM (loc, ms) =>
raise BAD (loc, commas (map (string_for_mterm ctxt) ms))
-(* hol_context -> bool -> typ -> term list * term list -> bool *)
val formulas_monotonic = is_some oooo infer "Monotonicity" false
-(* typ -> typ -> styp *)
fun fin_fun_constr T1 T2 =
(@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
-(* hol_context -> bool -> (typ option * bool option) list -> typ
- -> term list * term list -> term list * term list *)
fun finitize_funs (hol_ctxt as {thy, stds, fast_descrs, constr_cache, ...})
binarize finitizes alpha_T tsp =
case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
@@ -1144,12 +1035,10 @@
tsp
else
let
- (* typ -> sign_atom -> bool *)
fun should_finitize T a =
case triple_lookup (type_match thy) finitizes T of
SOME (SOME false) => false
| _ => resolve_sign_atom lits a = S Plus
- (* typ -> mtyp -> typ *)
fun type_from_mtype T M =
case (M, T) of
(MAlpha, _) => T
@@ -1161,12 +1050,10 @@
| (MType _, _) => T
| _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
[M], [T])
- (* styp -> styp *)
fun finitize_constr (x as (s, T)) =
(s, case AList.lookup (op =) constr_mtypes x of
SOME M => type_from_mtype T M
| NONE => T)
- (* typ list -> mterm -> term *)
fun term_from_mterm Ts m =
case m of
MRaw (t, M) =>
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Sat Apr 24 16:33:01 2010 +0200
@@ -205,7 +205,6 @@
exception NUT of string * nut list
-(* cst -> string *)
fun string_for_cst Unity = "Unity"
| string_for_cst False = "False"
| string_for_cst True = "True"
@@ -225,7 +224,6 @@
| string_for_cst NatToInt = "NatToInt"
| string_for_cst IntToNat = "IntToNat"
-(* op1 -> string *)
fun string_for_op1 Not = "Not"
| string_for_op1 Finite = "Finite"
| string_for_op1 Converse = "Converse"
@@ -237,7 +235,6 @@
| string_for_op1 Second = "Second"
| string_for_op1 Cast = "Cast"
-(* op2 -> string *)
fun string_for_op2 All = "All"
| string_for_op2 Exist = "Exist"
| string_for_op2 Or = "Or"
@@ -258,14 +255,11 @@
| string_for_op2 Apply = "Apply"
| string_for_op2 Lambda = "Lambda"
-(* op3 -> string *)
fun string_for_op3 Let = "Let"
| string_for_op3 If = "If"
-(* int -> Proof.context -> nut -> string *)
fun basic_string_for_nut indent ctxt u =
let
- (* nut -> string *)
val sub = basic_string_for_nut (indent + 1) ctxt
in
(if indent = 0 then "" else "\n" ^ implode (replicate (2 * indent) " ")) ^
@@ -313,17 +307,14 @@
Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R) ^
")"
end
-(* Proof.context -> nut -> string *)
val string_for_nut = basic_string_for_nut 0
-(* nut -> bool *)
fun inline_nut (Op1 _) = false
| inline_nut (Op2 _) = false
| inline_nut (Op3 _) = false
| inline_nut (Tuple (_, _, us)) = forall inline_nut us
| inline_nut _ = true
-(* nut -> typ *)
fun type_of (Cst (_, T, _)) = T
| type_of (Op1 (_, T, _, _)) = T
| type_of (Op2 (_, T, _, _, _)) = T
@@ -338,7 +329,6 @@
| type_of (RelReg (_, T, _)) = T
| type_of (FormulaReg (_, T, _)) = T
-(* nut -> rep *)
fun rep_of (Cst (_, _, R)) = R
| rep_of (Op1 (_, _, R, _)) = R
| rep_of (Op2 (_, _, R, _, _)) = R
@@ -353,7 +343,6 @@
| rep_of (RelReg (_, _, R)) = R
| rep_of (FormulaReg (_, _, R)) = R
-(* nut -> string *)
fun nickname_of (BoundName (_, _, _, nick)) = nick
| nickname_of (FreeName (s, _, _)) = s
| nickname_of (ConstName (s, _, _)) = s
@@ -361,7 +350,6 @@
| nickname_of (FreeRel (_, _, _, nick)) = nick
| nickname_of u = raise NUT ("Nitpick_Nut.nickname_of", [u])
-(* nut -> bool *)
fun is_skolem_name u =
space_explode name_sep (nickname_of u)
|> exists (String.isPrefix skolem_prefix)
@@ -369,11 +357,9 @@
fun is_eval_name u =
String.isPrefix eval_prefix (nickname_of u)
handle NUT ("Nitpick_Nut.nickname_of", _) => false
-(* cst -> nut -> bool *)
fun is_Cst cst (Cst (cst', _, _)) = (cst = cst')
| is_Cst _ _ = false
-(* (nut -> 'a -> 'a) -> nut -> 'a -> 'a *)
fun fold_nut f u =
case u of
Op1 (_, _, _, u1) => fold_nut f u1
@@ -382,7 +368,6 @@
| Tuple (_, _, us) => fold (fold_nut f) us
| Construct (us', _, _, us) => fold (fold_nut f) us #> fold (fold_nut f) us'
| _ => f u
-(* (nut -> nut) -> nut -> nut *)
fun map_nut f u =
case u of
Op1 (oper, T, R, u1) => Op1 (oper, T, R, map_nut f u1)
@@ -394,7 +379,6 @@
Construct (map (map_nut f) us', T, R, map (map_nut f) us)
| _ => f u
-(* nut * nut -> order *)
fun name_ord (BoundName (j1, _, _, _), BoundName (j2, _, _, _)) =
int_ord (j1, j2)
| name_ord (BoundName _, _) = LESS
@@ -411,24 +395,19 @@
| ord => ord)
| name_ord (u1, u2) = raise NUT ("Nitpick_Nut.name_ord", [u1, u2])
-(* nut -> nut -> int *)
fun num_occs_in_nut needle_u stack_u =
fold_nut (fn u => if u = needle_u then Integer.add 1 else I) stack_u 0
-(* nut -> nut -> bool *)
val is_subterm_of = not_equal 0 oo num_occs_in_nut
-(* nut -> nut -> nut -> nut *)
fun substitute_in_nut needle_u needle_u' =
map_nut (fn u => if u = needle_u then needle_u' else u)
-(* nut -> nut list * nut list -> nut list * nut list *)
val add_free_and_const_names =
fold_nut (fn u => case u of
FreeName _ => apfst (insert (op =) u)
| ConstName _ => apsnd (insert (op =) u)
| _ => I)
-(* nut -> rep -> nut *)
fun modify_name_rep (BoundName (j, T, _, nick)) R = BoundName (j, T, R, nick)
| modify_name_rep (FreeName (s, T, _)) R = FreeName (s, T, R)
| modify_name_rep (ConstName (s, T, _)) R = ConstName (s, T, R)
@@ -436,18 +415,15 @@
structure NameTable = Table(type key = nut val ord = name_ord)
-(* 'a NameTable.table -> nut -> 'a *)
fun the_name table name =
case NameTable.lookup table name of
SOME u => u
| NONE => raise NUT ("Nitpick_Nut.the_name", [name])
-(* nut NameTable.table -> nut -> KK.n_ary_index *)
fun the_rel table name =
case the_name table name of
FreeRel (x, _, _, _) => x
| u => raise NUT ("Nitpick_Nut.the_rel", [u])
-(* typ * term -> typ * term *)
fun mk_fst (_, Const (@{const_name Pair}, T) $ t1 $ _) = (domain_type T, t1)
| mk_fst (T, t) =
let val res_T = fst (HOLogic.dest_prodT T) in
@@ -459,23 +435,17 @@
let val res_T = snd (HOLogic.dest_prodT T) in
(res_T, Const (@{const_name snd}, T --> res_T) $ t)
end
-(* typ * term -> (typ * term) list *)
fun factorize (z as (Type (@{type_name "*"}, _), _)) =
maps factorize [mk_fst z, mk_snd z]
| factorize z = [z]
-(* hol_context -> op2 -> term -> nut *)
fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, ...}) eq =
let
- (* string list -> typ list -> term -> nut *)
fun aux eq ss Ts t =
let
- (* term -> nut *)
val sub = aux Eq ss Ts
val sub' = aux eq ss Ts
- (* string -> typ -> term -> nut *)
fun sub_abs s T = aux eq (s :: ss) (T :: Ts)
- (* typ -> term -> term -> nut *)
fun sub_equals T t1 t2 =
let
val (binder_Ts, body_T) = strip_type (domain_type T)
@@ -498,7 +468,6 @@
else
Op2 (eq, bool_T, Any, aux Eq ss Ts t1, aux Eq ss Ts t2)
end
- (* op2 -> string -> typ -> term -> nut *)
fun do_quantifier quant s T t1 =
let
val bound_u = BoundName (length Ts, T, Any, s)
@@ -509,21 +478,18 @@
else
body_u
end
- (* term -> term list -> nut *)
fun do_apply t0 ts =
let
val (ts', t2) = split_last ts
val t1 = list_comb (t0, ts')
val T1 = fastype_of1 (Ts, t1)
in Op2 (Apply, range_type T1, Any, sub t1, sub t2) end
- (* op2 -> string -> styp -> term -> nut *)
fun do_description_operator oper undef_s (x as (_, T)) t1 =
if fast_descrs then
Op2 (oper, range_type T, Any, sub t1,
sub (Const (undef_s, range_type T)))
else
do_apply (Const x) [t1]
- (* styp -> term list -> nut *)
fun do_construct (x as (_, T)) ts =
case num_binder_types T - length ts of
0 => Construct (map ((fn (s', T') => ConstName (s', T', Any))
@@ -716,21 +682,16 @@
end
in aux eq [] [] end
-(* scope -> typ -> rep *)
fun rep_for_abs_fun scope T =
let val (R1, R2) = best_non_opt_symmetric_reps_for_fun_type scope T in
Func (R1, (card_of_rep R1 <> card_of_rep R2 ? Opt) R2)
end
-(* scope -> nut -> nut list * rep NameTable.table
- -> nut list * rep NameTable.table *)
fun choose_rep_for_free_var scope v (vs, table) =
let
val R = best_non_opt_set_rep_for_type scope (type_of v)
val v = modify_name_rep v R
in (v :: vs, NameTable.update (v, R) table) end
-(* scope -> bool -> nut -> nut list * rep NameTable.table
- -> nut list * rep NameTable.table *)
fun choose_rep_for_const (scope as {hol_ctxt = {thy, ...}, ...}) all_exact v
(vs, table) =
let
@@ -756,16 +717,11 @@
val v = modify_name_rep v R
in (v :: vs, NameTable.update (v, R) table) end
-(* scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table *)
fun choose_reps_for_free_vars scope vs table =
fold (choose_rep_for_free_var scope) vs ([], table)
-(* scope -> bool -> nut list -> rep NameTable.table
- -> nut list * rep NameTable.table *)
fun choose_reps_for_consts scope all_exact vs table =
fold (choose_rep_for_const scope all_exact) vs ([], table)
-(* scope -> styp -> int -> nut list * rep NameTable.table
- -> nut list * rep NameTable.table *)
fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, binarize, ...})
(x as (_, T)) n (vs, table) =
let
@@ -778,21 +734,15 @@
best_opt_set_rep_for_type scope T' |> unopt_rep
val v = ConstName (s', T', R')
in (v :: vs, NameTable.update (v, R') table) end
-(* scope -> styp -> nut list * rep NameTable.table
- -> nut list * rep NameTable.table *)
fun choose_rep_for_sels_for_constr scope (x as (_, T)) =
fold_rev (choose_rep_for_nth_sel_for_constr scope x)
(~1 upto num_sels_for_constr_type T - 1)
-(* scope -> dtype_spec -> nut list * rep NameTable.table
- -> nut list * rep NameTable.table *)
fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : dtype_spec) = I
| choose_rep_for_sels_of_datatype scope {constrs, ...} =
fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
-(* scope -> rep NameTable.table -> nut list * rep NameTable.table *)
fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []
-(* scope -> nut -> rep NameTable.table -> rep NameTable.table *)
fun choose_rep_for_bound_var scope v table =
let val R = best_one_rep_for_type scope (type_of v) in
NameTable.update (v, R) table
@@ -802,7 +752,6 @@
three-valued logic, it would evaluate to a unrepresentable value ("Unrep")
according to the HOL semantics. For example, "Suc n" is constructive if "n"
is representable or "Unrep", because unknown implies "Unrep". *)
-(* nut -> bool *)
fun is_constructive u =
is_Cst Unrep u orelse
(not (is_fun_type (type_of u)) andalso not (is_opt_rep (rep_of u))) orelse
@@ -817,14 +766,11 @@
| Construct (_, _, _, us) => forall is_constructive us
| _ => false
-(* nut -> nut *)
fun optimize_unit u =
if rep_of u = Unit then Cst (Unity, type_of u, Unit) else u
-(* typ -> rep -> nut *)
fun unknown_boolean T R =
Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
T, R)
-(* nut -> bool *)
fun is_fully_representable_set u =
not (is_opt_rep (rep_of u)) andalso
case u of
@@ -835,7 +781,6 @@
forall is_fully_representable_set [u1, u2]
| _ => false
-(* op1 -> typ -> rep -> nut -> nut *)
fun s_op1 oper T R u1 =
((if oper = Not then
if is_Cst True u1 then Cst (False, T, R)
@@ -845,7 +790,6 @@
raise SAME ())
handle SAME () => Op1 (oper, T, R, u1))
|> optimize_unit
-(* op2 -> typ -> rep -> nut -> nut -> nut *)
fun s_op2 oper T R u1 u2 =
((case oper of
Or =>
@@ -886,7 +830,6 @@
| _ => raise SAME ())
handle SAME () => Op2 (oper, T, R, u1, u2))
|> optimize_unit
-(* op3 -> typ -> rep -> nut -> nut -> nut -> nut *)
fun s_op3 oper T R u1 u2 u3 =
((case oper of
Let =>
@@ -897,12 +840,10 @@
| _ => raise SAME ())
handle SAME () => Op3 (oper, T, R, u1, u2, u3))
|> optimize_unit
-(* typ -> rep -> nut list -> nut *)
fun s_tuple T R us =
(if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us))
|> optimize_unit
-(* theory -> nut -> nut *)
fun optimize_nut u =
case u of
Op1 (oper, T, R, u1) => s_op1 oper T R (optimize_nut u1)
@@ -914,35 +855,26 @@
| Construct (us', T, R, us) => Construct (us', T, R, map optimize_nut us)
| _ => optimize_unit u
-(* (nut -> 'a) -> nut -> 'a list *)
fun untuple f (Tuple (_, _, us)) = maps (untuple f) us
| untuple f u = if rep_of u = Unit then [] else [f u]
-(* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
fun choose_reps_in_nut (scope as {card_assigns, bits, datatypes, ofs, ...})
unsound table def =
let
val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
- (* polarity -> bool -> rep *)
fun bool_rep polar opt =
if polar = Neut andalso opt then Opt bool_atom_R else Formula polar
- (* nut -> nut -> nut *)
fun triad u1 u2 = s_op2 Triad (type_of u1) (Opt bool_atom_R) u1 u2
- (* (polarity -> nut) -> nut *)
fun triad_fn f = triad (f Pos) (f Neg)
- (* rep NameTable.table -> bool -> polarity -> nut -> nut -> nut *)
fun unrepify_nut_in_nut table def polar needle_u =
let val needle_T = type_of needle_u in
substitute_in_nut needle_u (Cst (if is_fun_type needle_T then Unknown
else Unrep, needle_T, Any))
#> aux table def polar
end
- (* rep NameTable.table -> bool -> polarity -> nut -> nut *)
and aux table def polar u =
let
- (* bool -> polarity -> nut -> nut *)
val gsub = aux table
- (* nut -> nut *)
val sub = gsub false Neut
in
case u of
@@ -1050,15 +982,12 @@
let
val u1' = sub u1
val u2' = sub u2
- (* unit -> nut *)
fun non_opt_case () = s_op2 Eq T (Formula polar) u1' u2'
- (* unit -> nut *)
fun opt_opt_case () =
if polar = Neut then
triad_fn (fn polar => s_op2 Eq T (Formula polar) u1' u2')
else
non_opt_case ()
- (* nut -> nut *)
fun hybrid_case u =
(* hackish optimization *)
if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2'
@@ -1275,35 +1204,27 @@
|> optimize_unit
in aux table def Pos end
-(* int -> KK.n_ary_index list -> KK.n_ary_index list
- -> int * KK.n_ary_index list *)
fun fresh_n_ary_index n [] ys = (0, (n, 1) :: ys)
| fresh_n_ary_index n ((m, j) :: xs) ys =
if m = n then (j, ys @ ((m, j + 1) :: xs))
else fresh_n_ary_index n xs ((m, j) :: ys)
-(* int -> name_pool -> int * name_pool *)
fun fresh_rel n {rels, vars, formula_reg, rel_reg} =
let val (j, rels') = fresh_n_ary_index n rels [] in
(j, {rels = rels', vars = vars, formula_reg = formula_reg,
rel_reg = rel_reg})
end
-(* int -> name_pool -> int * name_pool *)
fun fresh_var n {rels, vars, formula_reg, rel_reg} =
let val (j, vars') = fresh_n_ary_index n vars [] in
(j, {rels = rels, vars = vars', formula_reg = formula_reg,
rel_reg = rel_reg})
end
-(* int -> name_pool -> int * name_pool *)
fun fresh_formula_reg {rels, vars, formula_reg, rel_reg} =
(formula_reg, {rels = rels, vars = vars, formula_reg = formula_reg + 1,
rel_reg = rel_reg})
-(* int -> name_pool -> int * name_pool *)
fun fresh_rel_reg {rels, vars, formula_reg, rel_reg} =
(rel_reg, {rels = rels, vars = vars, formula_reg = formula_reg,
rel_reg = rel_reg + 1})
-(* nut -> nut list * name_pool * nut NameTable.table
- -> nut list * name_pool * nut NameTable.table *)
fun rename_plain_var v (ws, pool, table) =
let
val is_formula = (rep_of v = Formula Neut)
@@ -1313,7 +1234,6 @@
val w = constr (j, type_of v, rep_of v)
in (w :: ws, pool, NameTable.update (v, w) table) end
-(* typ -> rep -> nut list -> nut *)
fun shape_tuple (T as Type (@{type_name "*"}, [T1, T2])) (R as Struct [R1, R2])
us =
let val arity1 = arity_of_rep R1 in
@@ -1327,8 +1247,6 @@
| shape_tuple T Unit [] = Cst (Unity, T, Unit)
| shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)
-(* bool -> nut -> nut list * name_pool * nut NameTable.table
- -> nut list * name_pool * nut NameTable.table *)
fun rename_n_ary_var rename_free v (ws, pool, table) =
let
val T = type_of v
@@ -1370,15 +1288,12 @@
in (w :: ws, pool, NameTable.update (v, w) table) end
end
-(* nut list -> name_pool -> nut NameTable.table
- -> nut list * name_pool * nut NameTable.table *)
fun rename_free_vars vs pool table =
let
val vs = filter (not_equal Unit o rep_of) vs
val (vs, pool, table) = fold (rename_n_ary_var true) vs ([], pool, table)
in (rev vs, pool, table) end
-(* name_pool -> nut NameTable.table -> nut -> nut *)
fun rename_vars_in_nut pool table u =
case u of
Cst _ => u
--- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Sat Apr 24 16:33:01 2010 +0200
@@ -125,40 +125,31 @@
val lcm_rel = (3, 11)
val norm_frac_rel = (4, 0)
-(* int -> bool -> rel_expr *)
fun atom_for_bool j0 = Atom o Integer.add j0 o int_from_bool
-(* bool -> formula *)
fun formula_for_bool b = if b then True else False
-(* int * int -> int -> int *)
fun atom_for_nat (k, j0) n = if n < 0 orelse n >= k then ~1 else n + j0
-(* int -> int *)
fun min_int_for_card k = ~k div 2 + 1
fun max_int_for_card k = k div 2
-(* int * int -> int -> int *)
fun int_for_atom (k, j0) j =
let val j = j - j0 in if j <= max_int_for_card k then j else j - k end
fun atom_for_int (k, j0) n =
if n < min_int_for_card k orelse n > max_int_for_card k then ~1
else if n < 0 then n + k + j0
else n + j0
-(* int -> int -> bool *)
fun is_twos_complement_representable bits n =
let val max = reasonable_power 2 bits in n >= ~ max andalso n < max end
-(* rel_expr -> bool *)
fun is_none_product (Product (r1, r2)) =
is_none_product r1 orelse is_none_product r2
| is_none_product None = true
| is_none_product _ = false
-(* rel_expr -> bool *)
fun is_one_rel_expr (Atom _) = true
| is_one_rel_expr (AtomSeq (1, _)) = true
| is_one_rel_expr (Var _) = true
| is_one_rel_expr _ = false
-(* rel_expr -> bool *)
fun inline_rel_expr (Product (r1, r2)) =
inline_rel_expr r1 andalso inline_rel_expr r2
| inline_rel_expr Iden = true
@@ -172,7 +163,6 @@
| inline_rel_expr (RelReg _) = true
| inline_rel_expr _ = false
-(* rel_expr -> rel_expr -> bool option *)
fun rel_expr_equal None (Atom _) = SOME false
| rel_expr_equal None (AtomSeq (k, _)) = SOME (k = 0)
| rel_expr_equal (Atom _) None = SOME false
@@ -183,7 +173,6 @@
| rel_expr_equal (AtomSeq x1) (AtomSeq x2) = SOME (x1 = x2)
| rel_expr_equal r1 r2 = if r1 = r2 then SOME true else NONE
-(* rel_expr -> rel_expr -> bool option *)
fun rel_expr_intersects (Atom j1) (Atom j2) = SOME (j1 = j2)
| rel_expr_intersects (Atom j) (AtomSeq (k, j0)) = SOME (j < j0 + k)
| rel_expr_intersects (AtomSeq (k, j0)) (Atom j) = SOME (j < j0 + k)
@@ -192,30 +181,23 @@
| rel_expr_intersects r1 r2 =
if is_none_product r1 orelse is_none_product r2 then SOME false else NONE
-(* int -> rel_expr *)
fun empty_n_ary_rel 0 = raise ARG ("Nitpick_Peephole.empty_n_ary_rel", "0")
| empty_n_ary_rel n = funpow (n - 1) (curry Product None) None
-(* decl -> rel_expr *)
fun decl_one_set (DeclOne (_, r)) = r
| decl_one_set _ =
raise ARG ("Nitpick_Peephole.decl_one_set", "not \"DeclOne\"")
-(* int_expr -> bool *)
fun is_Num (Num _) = true
| is_Num _ = false
-(* int_expr -> int *)
fun dest_Num (Num k) = k
| dest_Num _ = raise ARG ("Nitpick_Peephole.dest_Num", "not \"Num\"")
-(* int -> int -> int_expr list *)
fun num_seq j0 n = map Num (index_seq j0 n)
-(* rel_expr -> rel_expr -> bool *)
fun occurs_in_union r (Union (r1, r2)) =
occurs_in_union r r1 orelse occurs_in_union r r2
| occurs_in_union r r' = (r = r')
-(* rel_expr -> rel_expr -> rel_expr *)
fun s_and True f2 = f2
| s_and False _ = False
| s_and f1 True = f1
@@ -258,18 +240,13 @@
(* We assume throughout that Kodkod variables have a "one" constraint. This is
always the case if Kodkod's skolemization is disabled. *)
-(* bool -> int -> int -> int -> kodkod_constrs *)
fun kodkod_constrs optim nat_card int_card main_j0 =
let
- (* bool -> int *)
val from_bool = atom_for_bool main_j0
- (* int -> rel_expr *)
fun from_nat n = Atom (n + main_j0)
- (* int -> int *)
fun to_nat j = j - main_j0
val to_int = int_for_atom (int_card, main_j0)
- (* decl list -> formula -> formula *)
fun s_all _ True = True
| s_all _ False = False
| s_all [] f = f
@@ -281,12 +258,10 @@
| s_exist ds (Exist (ds', f)) = Exist (ds @ ds', f)
| s_exist ds f = Exist (ds, f)
- (* expr_assign list -> formula -> formula *)
fun s_formula_let _ True = True
| s_formula_let _ False = False
| s_formula_let assigns f = FormulaLet (assigns, f)
- (* formula -> formula *)
fun s_not True = False
| s_not False = True
| s_not (All (ds, f)) = Exist (ds, s_not f)
@@ -299,7 +274,6 @@
| s_not (Some r) = No r
| s_not f = Not f
- (* formula -> formula -> formula *)
fun s_or True _ = True
| s_or False f2 = f2
| s_or _ True = True
@@ -316,7 +290,6 @@
| s_implies f1 False = s_not f1
| s_implies f1 f2 = if f1 = f2 then True else Implies (f1, f2)
- (* formula -> formula -> formula -> formula *)
fun s_formula_if True f2 _ = f2
| s_formula_if False _ f3 = f3
| s_formula_if f1 True f3 = s_or f1 f3
@@ -325,7 +298,6 @@
| s_formula_if f1 f2 False = s_and f1 f2
| s_formula_if f f1 f2 = FormulaIf (f, f1, f2)
- (* rel_expr -> int_expr list -> rel_expr *)
fun s_project r is =
(case r of
Project (r1, is') =>
@@ -340,7 +312,6 @@
else Project (r, is)
end
- (* (rel_expr -> formula) -> rel_expr -> formula *)
fun s_xone xone r =
if is_one_rel_expr r then
True
@@ -348,7 +319,6 @@
1 => xone r
| arity => foldl1 And (map (xone o s_project r o single o Num)
(index_seq 0 arity))
- (* rel_expr -> formula *)
fun s_no None = True
| s_no (Product (r1, r2)) = s_or (s_no r1) (s_no r2)
| s_no (Intersect (Closure (Rel x), Iden)) = Acyclic x
@@ -362,13 +332,11 @@
| s_some (Product (r1, r2)) = s_and (s_some r1) (s_some r2)
| s_some r = if is_one_rel_expr r then True else Some r
- (* rel_expr -> rel_expr *)
fun s_not3 (Atom j) = Atom (if j = main_j0 then j + 1 else j - 1)
| s_not3 (r as Join (r1, r2)) =
if r2 = Rel not3_rel then r1 else Join (r, Rel not3_rel)
| s_not3 r = Join (r, Rel not3_rel)
- (* rel_expr -> rel_expr -> formula *)
fun s_rel_eq r1 r2 =
(case (r1, r2) of
(Join (r11, Rel x), _) =>
@@ -427,12 +395,10 @@
else if forall is_one_rel_expr [r1, r2] then s_rel_eq r1 r2
else Subset (r1, r2)
- (* expr_assign list -> rel_expr -> rel_expr *)
fun s_rel_let [b as AssignRelReg (x', r')] (r as RelReg x) =
if x = x' then r' else RelLet ([b], r)
| s_rel_let bs r = RelLet (bs, r)
- (* formula -> rel_expr -> rel_expr -> rel_expr *)
fun s_rel_if f r1 r2 =
(case (f, r1, r2) of
(True, _, _) => r1
@@ -443,7 +409,6 @@
| _ => raise SAME ())
handle SAME () => if r1 = r2 then r1 else RelIf (f, r1, r2)
- (* rel_expr -> rel_expr -> rel_expr *)
fun s_union r1 (Union (r21, r22)) = s_union (s_union r1 r21) r22
| s_union r1 r2 =
if is_none_product r1 then r2
@@ -561,14 +526,12 @@
handle SAME () => List.foldr Join r22 [r1, r21])
| s_join r1 r2 = Join (r1, r2)
- (* rel_expr -> rel_expr *)
fun s_closure Iden = Iden
| s_closure r = if is_none_product r then r else Closure r
fun s_reflexive_closure Iden = Iden
| s_reflexive_closure r =
if is_none_product r then Iden else ReflexiveClosure r
- (* decl list -> formula -> rel_expr *)
fun s_comprehension ds False = empty_n_ary_rel (length ds)
| s_comprehension ds True = fold1 s_product (map decl_one_set ds)
| s_comprehension [d as DeclOne ((1, j1), r)]
@@ -579,10 +542,8 @@
Comprehension ([d], f)
| s_comprehension ds f = Comprehension (ds, f)
- (* rel_expr -> int -> int -> rel_expr *)
fun s_project_seq r =
let
- (* int -> rel_expr -> int -> int -> rel_expr *)
fun aux arity r j0 n =
if j0 = 0 andalso arity = n then
r
@@ -595,7 +556,6 @@
val arity1 = arity - arity2
val n1 = Int.min (nat_minus arity1 j0, n)
val n2 = n - n1
- (* unit -> rel_expr *)
fun one () = aux arity1 r1 j0 n1
fun two () = aux arity2 r2 (nat_minus j0 arity1) n2
in
@@ -607,17 +567,13 @@
| _ => s_project r (num_seq j0 n)
in aux (arity_of_rel_expr r) r end
- (* rel_expr -> rel_expr -> rel_expr *)
fun s_nat_less (Atom j1) (Atom j2) = from_bool (j1 < j2)
| s_nat_less r1 r2 = fold s_join [r1, r2] (Rel nat_less_rel)
fun s_int_less (Atom j1) (Atom j2) = from_bool (to_int j1 < to_int j2)
| s_int_less r1 r2 = fold s_join [r1, r2] (Rel int_less_rel)
- (* rel_expr -> int -> int -> rel_expr *)
fun d_project_seq r j0 n = Project (r, num_seq j0 n)
- (* rel_expr -> rel_expr *)
fun d_not3 r = Join (r, Rel not3_rel)
- (* rel_expr -> rel_expr -> rel_expr *)
fun d_nat_less r1 r2 = List.foldl Join (Rel nat_less_rel) [r1, r2]
fun d_int_less r1 r2 = List.foldl Join (Rel int_less_rel) [r1, r2]
in
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Apr 24 16:33:01 2010 +0200
@@ -21,7 +21,6 @@
open Nitpick_HOL
open Nitpick_Mono
-(* polarity -> string -> bool *)
fun is_positive_existential polar quant_s =
(polar = Pos andalso quant_s = @{const_name Ex}) orelse
(polar = Neg andalso quant_s <> @{const_name Ex})
@@ -33,10 +32,8 @@
binary coding. *)
val binary_int_threshold = 3
-(* bool -> term -> bool *)
val may_use_binary_ints =
let
- (* bool -> term -> bool *)
fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) =
aux def t1 andalso aux false t2
| aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
@@ -52,10 +49,8 @@
| aux def (Abs (_, _, t')) = aux def t'
| aux _ _ = true
in aux end
-(* term -> bool *)
val should_use_binary_ints =
let
- (* term -> bool *)
fun aux (t1 $ t2) = aux t1 orelse aux t2
| aux (Const (s, T)) =
((s = @{const_name times} orelse s = @{const_name div}) andalso
@@ -70,10 +65,8 @@
(** Uncurrying **)
-(* theory -> term -> int Termtab.tab -> int Termtab.tab *)
fun add_to_uncurry_table thy t =
let
- (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
fun aux (t1 $ t2) args table =
let val table = aux t2 [] table in aux t1 (t2 :: args) table end
| aux (Abs (_, _, t')) _ table = aux t' [] table
@@ -87,14 +80,11 @@
| aux _ _ table = table
in aux t [] end
-(* int -> int -> string *)
fun uncurry_prefix_for k j =
uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
-(* int Termtab.tab term -> term *)
fun uncurry_term table t =
let
- (* term -> term list -> term *)
fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
| aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
| aux (t as Const (s, T)) args =
@@ -131,17 +121,14 @@
(** Boxing **)
-(* hol_context -> bool -> term -> term *)
fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
orig_t =
let
- (* typ -> typ *)
fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
Type (@{type_name fun}, map box_relational_operator_type Ts)
| box_relational_operator_type (Type (@{type_name "*"}, Ts)) =
Type (@{type_name "*"}, map (box_type hol_ctxt InPair) Ts)
| box_relational_operator_type T = T
- (* indexname * typ -> typ * term -> typ option list -> typ option list *)
fun add_boxed_types_for_var (z as (_, T)) (T', t') =
case t' of
Var z' => z' = z ? insert (op =) T'
@@ -152,7 +139,6 @@
| _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\
\add_boxed_types_for_var", [T'], []))
| _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
- (* typ list -> typ list -> term -> indexname * typ -> typ *)
fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
case t of
@{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
@@ -170,8 +156,6 @@
else
T
| _ => T
- (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
- -> term -> term *)
and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
let
val abs_T' =
@@ -185,7 +169,6 @@
$ Abs (abs_s, abs_T',
t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
end
- (* typ list -> typ list -> string -> typ -> term -> term -> term *)
and do_equals new_Ts old_Ts s0 T0 t1 t2 =
let
val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
@@ -195,12 +178,10 @@
list_comb (Const (s0, T --> T --> body_type T0),
map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])
end
- (* string -> typ -> term *)
and do_description_operator s T =
let val T1 = box_type hol_ctxt InFunLHS (range_type T) in
Const (s, (T1 --> bool_T) --> T1)
end
- (* typ list -> typ list -> polarity -> term -> term *)
and do_term new_Ts old_Ts polar t =
case t of
Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
@@ -302,21 +283,16 @@
val val_var_prefix = nitpick_prefix ^ "v"
-(* typ list -> int -> int -> int -> term -> term *)
fun fresh_value_var Ts k n j t =
Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
-(* typ list -> term -> bool *)
fun has_heavy_bounds_or_vars Ts t =
let
- (* typ list -> bool *)
fun aux [] = false
| aux [T] = is_fun_type T orelse is_pair_type T
| aux _ = true
in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
-(* hol_context -> typ list -> bool -> int -> int -> term -> term list
- -> term list -> term * term list *)
fun pull_out_constr_comb ({thy, stds, ...} : hol_context) Ts relax k level t
args seen =
let val t_comb = list_comb (t, args) in
@@ -336,18 +312,15 @@
| _ => (t_comb, seen)
end
-(* (term -> term) -> typ list -> int -> term list -> term list *)
fun equations_for_pulled_out_constrs mk_eq Ts k seen =
let val n = length seen in
map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
(index_seq 0 n) seen
end
-(* hol_context -> bool -> term -> term *)
fun pull_out_universal_constrs hol_ctxt def t =
let
val k = maxidx_of_term t + 1
- (* typ list -> bool -> term -> term list -> term list -> term * term list *)
fun do_term Ts def t args seen =
case t of
(t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
@@ -367,8 +340,6 @@
do_term Ts def t1 (t2 :: args) seen
end
| _ => pull_out_constr_comb hol_ctxt Ts def k 0 t args seen
- (* typ list -> bool -> bool -> term -> term -> term -> term list
- -> term * term list *)
and do_eq_or_imp Ts eq def t0 t1 t2 seen =
let
val (t2, seen) = if eq andalso def then (t2, seen)
@@ -381,22 +352,18 @@
seen, concl)
end
-(* term -> term -> term *)
fun mk_exists v t =
HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
-(* hol_context -> term -> term *)
fun pull_out_existential_constrs hol_ctxt t =
let
val k = maxidx_of_term t + 1
- (* typ list -> int -> term -> term list -> term list -> term * term list *)
fun aux Ts num_exists t args seen =
case t of
(t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
let
val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
val n = length seen'
- (* unit -> term list *)
fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
in
(equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
@@ -421,7 +388,6 @@
val let_var_prefix = nitpick_prefix ^ "l"
val let_inline_threshold = 32
-(* int -> typ -> term -> (term -> term) -> term *)
fun hol_let n abs_T body_T f t =
if n * size_of_term t <= let_inline_threshold then
f t
@@ -431,14 +397,11 @@
$ t $ abs_var z (incr_boundvars 1 (f (Var z)))
end
-(* hol_context -> bool -> term -> term *)
fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =
let
- (* styp -> int *)
val num_occs_of_var =
fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
| _ => I) t (K 0)
- (* bool -> term -> term *)
fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
aux_eq careful true t0 t1 t2
| aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
@@ -450,7 +413,6 @@
| aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
| aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
| aux _ t = t
- (* bool -> bool -> term -> term -> term -> term *)
and aux_eq careful pass1 t0 t1 t2 =
((if careful then
raise SAME ()
@@ -485,7 +447,6 @@
|> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
else t0 $ aux false t2 $ aux false t1
- (* styp -> term -> int -> typ -> term -> term *)
and sel_eq x t n nth_T nth_t =
HOLogic.eq_const nth_T $ nth_t
$ select_nth_constr_arg thy stds x t n nth_T
@@ -494,7 +455,6 @@
(** Destruction of universal and existential equalities **)
-(* term -> term *)
fun curry_assms (@{const "==>"} $ (@{const Trueprop}
$ (@{const "op &"} $ t1 $ t2)) $ t3) =
curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
@@ -502,15 +462,12 @@
@{const "==>"} $ curry_assms t1 $ curry_assms t2
| curry_assms t = t
-(* term -> term *)
val destroy_universal_equalities =
let
- (* term list -> (indexname * typ) list -> term -> term *)
fun aux prems zs t =
case t of
@{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
| _ => Logic.list_implies (rev prems, t)
- (* term list -> (indexname * typ) list -> term -> term -> term *)
and aux_implies prems zs t1 t2 =
case t1 of
Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
@@ -519,8 +476,6 @@
| @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
aux_eq prems zs z t' t1 t2
| _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
- (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
- -> term -> term *)
and aux_eq prems zs z t' t1 t2 =
if not (member (op =) zs z) andalso
not (exists_subterm (curry (op =) (Var z)) t') then
@@ -529,15 +484,11 @@
aux (t1 :: prems) (Term.add_vars t1 zs) t2
in aux [] [] end
-(* theory -> (typ option * bool) list -> int -> term list -> term list
- -> (term * term list) option *)
fun find_bound_assign thy stds j =
let
- (* term list -> term list -> (term * term list) option *)
fun do_term _ [] = NONE
| do_term seen (t :: ts) =
let
- (* bool -> term -> term -> (term * term list) option *)
fun do_eq pass1 t1 t2 =
(if loose_bvar1 (t2, j) then
if pass1 then do_eq false t2 t1 else raise SAME ()
@@ -559,10 +510,8 @@
end
in do_term end
-(* int -> term -> term -> term *)
fun subst_one_bound j arg t =
let
- (* term * int -> term *)
fun aux (Bound i, lev) =
if i < lev then raise SAME ()
else if i = lev then incr_boundvars (lev - j) arg
@@ -574,10 +523,8 @@
| aux _ = raise SAME ()
in aux (t, j) handle SAME () => t end
-(* hol_context -> term -> term *)
fun destroy_existential_equalities ({thy, stds, ...} : hol_context) =
let
- (* string list -> typ list -> term list -> term *)
fun kill [] [] ts = foldr1 s_conj ts
| kill (s :: ss) (T :: Ts) ts =
(case find_bound_assign thy stds (length ss) [] ts of
@@ -589,7 +536,6 @@
Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
$ Abs (s, T, kill ss Ts ts))
| kill _ _ _ = raise UnequalLengths
- (* string list -> typ list -> term -> term *)
fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) =
gather (ss @ [s1]) (Ts @ [T1]) t1
| gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
@@ -600,20 +546,15 @@
(** Skolemization **)
-(* int -> int -> string *)
fun skolem_prefix_for k j =
skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
-(* hol_context -> int -> term -> term *)
fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...})
skolem_depth =
let
- (* int list -> int list *)
val incrs = map (Integer.add 1)
- (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
fun aux ss Ts js depth polar t =
let
- (* string -> typ -> string -> typ -> term -> term *)
fun do_quantifier quant_s quant_T abs_s abs_T t =
if not (loose_bvar1 (t, 0)) then
aux ss Ts js depth polar (incr_boundvars ~1 t)
@@ -679,7 +620,6 @@
else
(ubfp_prefix, @{const "op &"},
@{const_name semilattice_inf_class.inf})
- (* unit -> term *)
fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
|> aux ss Ts js depth polar
fun neg () = Const (pref ^ s, T)
@@ -693,7 +633,6 @@
val ((trunk_arg_Ts, rump_arg_T), body_T) =
T |> strip_type |>> split_last
val set_T = rump_arg_T --> body_T
- (* (unit -> term) -> term *)
fun app f =
list_comb (f (),
map Bound (length trunk_arg_Ts - 1 downto 0))
@@ -717,21 +656,18 @@
(** Function specialization **)
-(* term -> term list *)
fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
| params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
| params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
snd (strip_comb t1)
| params_in_equation _ = []
-(* styp -> styp -> int list -> term list -> term list -> term -> term *)
fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
let
val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
+ 1
val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
val fixed_params = filter_indices fixed_js (params_in_equation t)
- (* term list -> term -> term *)
fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
| aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
| aux args t =
@@ -743,10 +679,8 @@
end
in aux [] t end
-(* hol_context -> styp -> (int * term option) list *)
fun static_args_in_term ({ersatz_table, ...} : hol_context) x t =
let
- (* term -> term list -> term list -> term list list *)
fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
| fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
| fun_calls t args =
@@ -756,7 +690,6 @@
SOME s'' => x = (s'', T')
| NONE => false)
| _ => false) ? cons args
- (* term list list -> term list list -> term list -> term list list *)
fun call_sets [] [] vs = [vs]
| call_sets [] uss vs = vs :: call_sets uss [] []
| call_sets ([] :: _) _ _ = []
@@ -773,12 +706,10 @@
| [t as Free _] => cons (j, SOME t)
| _ => I) indexed_sets []
end
-(* hol_context -> styp -> term list -> (int * term option) list *)
fun static_args_in_terms hol_ctxt x =
map (static_args_in_term hol_ctxt x)
#> fold1 (OrdList.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
-(* (int * term option) list -> (int * term) list -> int list *)
fun overlapping_indices [] _ = []
| overlapping_indices _ [] = []
| overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
@@ -786,7 +717,6 @@
else if j1 > j2 then overlapping_indices ps1 ps2'
else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
-(* typ list -> term -> bool *)
fun is_eligible_arg Ts t =
let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
null bad_Ts orelse
@@ -794,7 +724,6 @@
forall (not o is_higher_order_type) bad_Ts)
end
-(* int -> string *)
fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
(* If a constant's definition is picked up deeper than this threshold, we
@@ -803,7 +732,6 @@
val bound_var_prefix = "b"
-(* hol_context -> int -> term -> term *)
fun specialize_consts_in_term (hol_ctxt as {specialize, simp_table,
special_funs, ...}) depth t =
if not specialize orelse depth > special_max_depth then
@@ -812,7 +740,6 @@
let
val blacklist = if depth = 0 then []
else case term_under_def t of Const x => [x] | _ => []
- (* term list -> typ list -> term -> term *)
fun aux args Ts (Const (x as (s, T))) =
((if not (member (op =) blacklist x) andalso not (null args) andalso
not (String.isPrefix special_prefix s) andalso
@@ -836,7 +763,6 @@
val extra_args = map Var vars @ map Bound bound_js @ live_args
val extra_Ts = map snd vars @ filter_indices bound_js Ts
val k = maxidx_of_term t + 1
- (* int -> term *)
fun var_for_bound_no j =
Var ((bound_var_prefix ^
nat_subscript (find_index (curry (op =) j) bound_js
@@ -880,7 +806,6 @@
val cong_var_prefix = "c"
-(* typ -> special_triple -> special_triple -> term *)
fun special_congruence_axiom T (js1, ts1, x1) (js2, ts2, x2) =
let
val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
@@ -905,7 +830,6 @@
|> close_form (* TODO: needed? *)
end
-(* hol_context -> styp list -> term list *)
fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs =
let
val groups =
@@ -914,14 +838,10 @@
|> AList.group (op =)
|> filter_out (is_equational_fun_surely_complete hol_ctxt o fst)
|> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
- (* special_triple -> int *)
fun generality (js, _, _) = ~(length js)
- (* special_triple -> special_triple -> bool *)
fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
x1 <> x2 andalso OrdList.subset (prod_ord int_ord Term_Ord.term_ord)
(j2 ~~ t2, j1 ~~ t1)
- (* typ -> special_triple list -> special_triple list -> special_triple list
- -> term list -> term list *)
fun do_pass_1 _ [] [_] [_] = I
| do_pass_1 T skipped _ [] = do_pass_2 T skipped
| do_pass_1 T skipped all (z :: zs) =
@@ -930,7 +850,6 @@
[] => do_pass_1 T (z :: skipped) all zs
| (z' :: _) => cons (special_congruence_axiom T z z')
#> do_pass_1 T skipped all zs
- (* typ -> special_triple list -> term list -> term list *)
and do_pass_2 _ [] = I
| do_pass_2 T (z :: zs) =
fold (cons o special_congruence_axiom T z) zs #> do_pass_2 T zs
@@ -938,32 +857,23 @@
(** Axiom selection **)
-(* 'a Symtab.table -> 'a list *)
fun all_table_entries table = Symtab.fold (append o snd) table []
-(* const_table -> string -> const_table *)
fun extra_table table s = Symtab.make [(s, all_table_entries table)]
-(* int -> term -> term *)
fun eval_axiom_for_term j t =
Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
-(* term -> bool *)
val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
(* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
val axioms_max_depth = 255
-(* hol_context -> term -> term list * term list * bool * bool *)
fun axioms_for_term
(hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
fast_descrs, evals, def_table, nondef_table,
choice_spec_table, user_nondefs, ...}) t =
let
type accumulator = styp list * (term list * term list)
- (* (term list * term list -> term list)
- -> ((term list -> term list) -> term list * term list
- -> term list * term list)
- -> int -> term -> accumulator -> accumulator *)
fun add_axiom get app depth t (accum as (xs, axs)) =
let
val t = t |> unfold_defs_in_term hol_ctxt
@@ -977,7 +887,6 @@
else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
end
end
- (* int -> term -> accumulator -> accumulator *)
and add_def_axiom depth = add_axiom fst apfst depth
and add_nondef_axiom depth = add_axiom snd apsnd depth
and add_maybe_def_axiom depth t =
@@ -986,7 +895,6 @@
and add_eq_axiom depth t =
(if is_constr_pattern_formula thy t then add_def_axiom
else add_nondef_axiom) depth t
- (* int -> term -> accumulator -> accumulator *)
and add_axioms_for_term depth t (accum as (xs, axs)) =
case t of
t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
@@ -1058,7 +966,6 @@
| Bound _ => accum
| Abs (_, T, t) => accum |> add_axioms_for_term depth t
|> add_axioms_for_type depth T
- (* int -> typ -> accumulator -> accumulator *)
and add_axioms_for_type depth T =
case T of
Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts
@@ -1080,7 +987,6 @@
(codatatype_bisim_axioms hol_ctxt T)
else
I)
- (* int -> typ -> sort -> accumulator -> accumulator *)
and add_axioms_for_sort depth T S =
let
val supers = Sign.complete_sort thy S
@@ -1112,15 +1018,12 @@
(** Simplification of constructor/selector terms **)
-(* theory -> term -> term *)
fun simplify_constrs_and_sels thy t =
let
- (* term -> int -> term *)
fun is_nth_sel_on t' n (Const (s, _) $ t) =
(t = t' andalso is_sel_like_and_no_discr s andalso
sel_no_from_name s = n)
| is_nth_sel_on _ _ _ = false
- (* term -> term list -> term *)
fun do_term (Const (@{const_name Rep_Frac}, _)
$ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
| do_term (Const (@{const_name Abs_Frac}, _)
@@ -1160,7 +1063,6 @@
(** Quantifier massaging: Distributing quantifiers **)
-(* term -> term *)
fun distribute_quantifiers t =
case t of
(t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
@@ -1199,7 +1101,6 @@
(** Quantifier massaging: Pushing quantifiers inward **)
-(* int -> int -> (int -> int) -> term -> term *)
fun renumber_bounds j n f t =
case t of
t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
@@ -1214,10 +1115,8 @@
paper). *)
val quantifier_cluster_threshold = 7
-(* term -> term *)
val push_quantifiers_inward =
let
- (* string -> string list -> typ list -> term -> term *)
fun aux quant_s ss Ts t =
(case t of
Const (s0, _) $ Abs (s1, T1, t1 as _ $ _) =>
@@ -1237,7 +1136,6 @@
else
let
val typical_card = 4
- (* ('a -> ''b list) -> 'a list -> ''b list *)
fun big_union proj ps =
fold (fold (insert (op =)) o proj) ps []
val (ts, connective) = strip_any_connective t
@@ -1245,11 +1143,8 @@
map (bounded_card_of_type 65536 typical_card []) Ts
val t_costs = map size_of_term ts
val num_Ts = length Ts
- (* int -> int *)
val flip = curry (op -) (num_Ts - 1)
val t_boundss = map (map flip o loose_bnos) ts
- (* (int list * int) list -> int list
- -> (int list * int) list *)
fun merge costly_boundss [] = costly_boundss
| merge costly_boundss (j :: js) =
let
@@ -1261,9 +1156,7 @@
val yeas_cost = Integer.sum (map snd yeas)
* nth T_costs j
in merge ((yeas_bounds, yeas_cost) :: nays) js end
- (* (int list * int) list -> int list -> int *)
val cost = Integer.sum o map snd oo merge
- (* (int list * int) list -> int list -> int list *)
fun heuristically_best_permutation _ [] = []
| heuristically_best_permutation costly_boundss js =
let
@@ -1287,14 +1180,12 @@
(index_seq 0 num_Ts)
val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
ts
- (* (term * int list) list -> term *)
fun mk_connection [] =
raise ARG ("Nitpick_Preproc.push_quantifiers_inward.aux.\
\mk_connection", "")
| mk_connection ts_cum_bounds =
ts_cum_bounds |> map fst
|> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
- (* (term * int list) list -> int list -> term *)
fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
| build ts_cum_bounds (j :: js) =
let
@@ -1321,9 +1212,6 @@
(** Inference of finite functions **)
-(* hol_context -> bool -> (typ option * bool option) list
- -> (typ option * bool option) list -> term list * term list
- -> term list * term list *)
fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos
(nondef_ts, def_ts) =
let
@@ -1338,9 +1226,6 @@
(** Preprocessor entry point **)
-(* hol_context -> (typ option * bool option) list
- -> (typ option * bool option) list -> term
- -> term list * term list * bool * bool * bool *)
fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
boxes, skolemize, uncurry, ...})
finitizes monos t =
@@ -1365,7 +1250,6 @@
val table =
Termtab.empty
|> uncurry ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts)
- (* bool -> term -> term *)
fun do_rest def =
binarize ? binarize_nat_and_int_in_term
#> uncurry ? uncurry_term table
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Sat Apr 24 16:33:01 2010 +0200
@@ -77,18 +77,15 @@
exception REP of string * rep list
-(* polarity -> string *)
fun string_for_polarity Pos = "+"
| string_for_polarity Neg = "-"
| string_for_polarity Neut = "="
-(* rep -> string *)
fun atomic_string_for_rep rep =
let val s = string_for_rep rep in
if String.isPrefix "[" s orelse not (is_substring_of " " s) then s
else "(" ^ s ^ ")"
end
-(* rep -> string *)
and string_for_rep Any = "X"
| string_for_rep (Formula polar) = "F" ^ string_for_polarity polar
| string_for_rep Unit = "U"
@@ -101,7 +98,6 @@
atomic_string_for_rep R1 ^ " => " ^ string_for_rep R2
| string_for_rep (Opt R) = atomic_string_for_rep R ^ "?"
-(* rep -> bool *)
fun is_Func (Func _) = true
| is_Func _ = false
fun is_Opt (Opt _) = true
@@ -110,7 +106,6 @@
| is_opt_rep (Opt _) = true
| is_opt_rep _ = false
-(* rep -> int *)
fun card_of_rep Any = raise REP ("Nitpick_Rep.card_of_rep", [Any])
| card_of_rep (Formula _) = 2
| card_of_rep Unit = 1
@@ -140,7 +135,6 @@
Int.max (min_univ_card_of_rep R1, min_univ_card_of_rep R2)
| min_univ_card_of_rep (Opt R) = min_univ_card_of_rep R
-(* rep -> bool *)
fun is_one_rep Unit = true
| is_one_rep (Atom _) = true
| is_one_rep (Struct _) = true
@@ -149,10 +143,8 @@
fun is_lone_rep (Opt R) = is_one_rep R
| is_lone_rep R = is_one_rep R
-(* rep -> rep * rep *)
fun dest_Func (Func z) = z
| dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R])
-(* int Typtab.table -> typ -> (unit -> int) -> rep -> rep *)
fun lazy_range_rep _ _ _ Unit = Unit
| lazy_range_rep _ _ _ (Vect (_, R)) = R
| lazy_range_rep _ _ _ (Func (_, R2)) = R2
@@ -164,19 +156,15 @@
Atom (ran_card (), offset_of_type ofs T2)
| lazy_range_rep _ _ _ R = raise REP ("Nitpick_Rep.lazy_range_rep", [R])
-(* rep -> rep list *)
fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2
| binder_reps _ = []
-(* rep -> rep *)
fun body_rep (Func (_, R2)) = body_rep R2
| body_rep R = R
-(* rep -> rep *)
fun flip_rep_polarity (Formula polar) = Formula (flip_polarity polar)
| flip_rep_polarity (Func (R1, R2)) = Func (R1, flip_rep_polarity R2)
| flip_rep_polarity R = R
-(* int Typtab.table -> rep -> rep *)
fun one_rep _ _ Any = raise REP ("Nitpick_Rep.one_rep", [Any])
| one_rep _ _ (Atom x) = Atom x
| one_rep _ _ (Struct Rs) = Struct Rs
@@ -189,12 +177,10 @@
fun opt_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
Func (R1, opt_rep ofs T2 R2)
| opt_rep ofs T R = Opt (optable_rep ofs T R)
-(* rep -> rep *)
fun unopt_rep (Func (R1, R2)) = Func (R1, unopt_rep R2)
| unopt_rep (Opt R) = R
| unopt_rep R = R
-(* polarity -> polarity -> polarity *)
fun min_polarity polar1 polar2 =
if polar1 = polar2 then
polar1
@@ -208,7 +194,6 @@
(* It's important that Func is before Vect, because if the range is Opt we
could lose information by converting a Func to a Vect. *)
-(* rep -> rep -> rep *)
fun min_rep (Opt R1) (Opt R2) = Opt (min_rep R1 R2)
| min_rep (Opt R) _ = Opt R
| min_rep _ (Opt R) = Opt R
@@ -237,7 +222,6 @@
else if k1 > k2 then Vect (k2, R2)
else Vect (k1, min_rep R1 R2)
| min_rep R1 R2 = raise REP ("Nitpick_Rep.min_rep", [R1, R2])
-(* rep list -> rep list -> rep list *)
and min_reps [] _ = []
| min_reps _ [] = []
| min_reps (R1 :: Rs1) (R2 :: Rs2) =
@@ -245,7 +229,6 @@
else if min_rep R1 R2 = R1 then R1 :: Rs1
else R2 :: Rs2
-(* int -> rep -> int *)
fun card_of_domain_from_rep ran_card R =
case R of
Unit => 1
@@ -255,14 +238,12 @@
| Opt R => card_of_domain_from_rep ran_card R
| _ => raise REP ("Nitpick_Rep.card_of_domain_from_rep", [R])
-(* int Typtab.table -> typ -> rep -> rep *)
fun rep_to_binary_rel_rep ofs T R =
let
val k = exact_root 2 (card_of_domain_from_rep 2 R)
val j0 = offset_of_type ofs (fst (HOLogic.dest_prodT (domain_type T)))
in Func (Struct [Atom (k, j0), Atom (k, j0)], Formula Neut) end
-(* scope -> typ -> rep *)
fun best_one_rep_for_type (scope as {card_assigns, ...} : scope)
(Type (@{type_name fun}, [T1, T2])) =
(case best_one_rep_for_type scope T2 of
@@ -283,7 +264,6 @@
(* Datatypes are never represented by Unit, because it would confuse
"nfa_transitions_for_ctor". *)
-(* scope -> typ -> rep *)
fun best_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2)
| best_opt_set_rep_for_type (scope as {ofs, ...}) T =
@@ -308,7 +288,6 @@
| best_non_opt_symmetric_reps_for_fun_type _ T =
raise TYPE ("Nitpick_Rep.best_non_opt_symmetric_reps_for_fun_type", [T], [])
-(* rep -> (int * int) list *)
fun atom_schema_of_rep Any = raise REP ("Nitpick_Rep.atom_schema_of_rep", [Any])
| atom_schema_of_rep (Formula _) = []
| atom_schema_of_rep Unit = []
@@ -318,10 +297,8 @@
| atom_schema_of_rep (Func (R1, R2)) =
atom_schema_of_rep R1 @ atom_schema_of_rep R2
| atom_schema_of_rep (Opt R) = atom_schema_of_rep R
-(* rep list -> (int * int) list *)
and atom_schema_of_reps Rs = maps atom_schema_of_rep Rs
-(* typ -> rep -> typ list *)
fun type_schema_of_rep _ (Formula _) = []
| type_schema_of_rep _ Unit = []
| type_schema_of_rep T (Atom _) = [T]
@@ -333,12 +310,9 @@
type_schema_of_rep T1 R1 @ type_schema_of_rep T2 R2
| type_schema_of_rep T (Opt R) = type_schema_of_rep T R
| type_schema_of_rep _ R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R])
-(* typ list -> rep list -> typ list *)
and type_schema_of_reps Ts Rs = flat (map2 type_schema_of_rep Ts Rs)
-(* rep -> int list list *)
val all_combinations_for_rep = all_combinations o atom_schema_of_rep
-(* rep list -> int list list *)
val all_combinations_for_reps = all_combinations o atom_schema_of_reps
end;
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Sat Apr 24 16:33:01 2010 +0200
@@ -93,11 +93,9 @@
type row = row_kind * int list
type block = row list
-(* dtype_spec list -> typ -> dtype_spec option *)
fun datatype_spec (dtypes : dtype_spec list) T =
List.find (curry (op =) T o #typ) dtypes
-(* dtype_spec list -> styp -> constr_spec *)
fun constr_spec [] x = raise TERM ("Nitpick_Scope.constr_spec", [Const x])
| constr_spec ({constrs, ...} :: dtypes : dtype_spec list) (x as (s, T)) =
case List.find (curry (op =) (s, body_type T) o (apsnd body_type o #const))
@@ -105,7 +103,6 @@
SOME c => c
| NONE => constr_spec dtypes x
-(* dtype_spec list -> bool -> typ -> bool *)
fun is_complete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
| is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) =
@@ -128,19 +125,15 @@
and is_exact_type dtypes facto =
is_complete_type dtypes facto andf is_concrete_type dtypes facto
-(* int Typtab.table -> typ -> int *)
fun offset_of_type ofs T =
case Typtab.lookup ofs T of
SOME j0 => j0
| NONE => Typtab.lookup ofs dummyT |> the_default 0
-(* scope -> typ -> int * int *)
fun spec_of_type ({card_assigns, ofs, ...} : scope) T =
(card_of_type card_assigns T
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
-(* (string -> string) -> scope
- -> string list * string list * string list * string list * string list *)
fun quintuple_for_scope quote
({hol_ctxt = {thy, ctxt, stds, ...}, card_assigns, bits, bisim_depth,
datatypes, ...} : scope) =
@@ -180,7 +173,6 @@
maxes (), iters (), miscs ())) ()
end
-(* scope -> bool -> Pretty.T list *)
fun pretties_for_scope scope verbose =
let
val (primary_cards, secondary_cards, maxes, iters, bisim_depths) =
@@ -198,7 +190,6 @@
else serial_commas "and" ss |> map Pretty.str |> Pretty.breaks
end
-(* scope -> string *)
fun multiline_string_for_scope scope =
let
val (primary_cards, secondary_cards, maxes, iters, bisim_depths) =
@@ -213,47 +204,35 @@
| lines => space_implode "\n" lines
end
-(* scope * scope -> bool *)
fun scopes_equivalent (s1 : scope, s2 : scope) =
#datatypes s1 = #datatypes s2 andalso #card_assigns s1 = #card_assigns s2
fun scope_less_eq (s1 : scope) (s2 : scope) =
(s1, s2) |> pairself (map snd o #card_assigns) |> op ~~ |> forall (op <=)
-(* row -> int *)
fun rank_of_row (_, ks) = length ks
-(* block -> int *)
fun rank_of_block block = fold Integer.max (map rank_of_row block) 1
-(* int -> typ * int list -> typ * int list *)
fun project_row column (y, ks) = (y, [nth ks (Int.min (column, length ks - 1))])
-(* int -> block -> block *)
fun project_block (column, block) = map (project_row column) block
-(* (''a * ''a -> bool) -> (''a option * int list) list -> ''a -> int list *)
fun lookup_ints_assign eq assigns key =
case triple_lookup eq assigns key of
SOME ks => ks
| NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "")
-(* theory -> (typ option * int list) list -> typ -> int list *)
fun lookup_type_ints_assign thy assigns T =
map (Integer.max 1) (lookup_ints_assign (type_match thy) assigns T)
handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], [])
-(* theory -> (styp option * int list) list -> styp -> int list *)
fun lookup_const_ints_assign thy assigns x =
lookup_ints_assign (const_match thy) assigns x
handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
raise TERM ("Nitpick_Scope.lookup_const_ints_assign", [Const x])
-(* theory -> (styp option * int list) list -> styp -> row option *)
fun row_for_constr thy maxes_assigns constr =
SOME (Max constr, lookup_const_ints_assign thy maxes_assigns constr)
handle TERM ("lookup_const_ints_assign", _) => NONE
val max_bits = 31 (* Kodkod limit *)
-(* hol_context -> bool -> (typ option * int list) list
- -> (styp option * int list) list -> (styp option * int list) list -> int list
- -> int list -> typ -> block *)
fun block_for_type (hol_ctxt as {thy, ...}) binarize cards_assigns maxes_assigns
iters_assigns bitss bisim_depths T =
if T = @{typ unsigned_bit} then
@@ -276,13 +255,9 @@
[_] => []
| constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
-(* hol_context -> bool -> (typ option * int list) list
- -> (styp option * int list) list -> (styp option * int list) list -> int list
- -> int list -> typ list -> typ list -> block list *)
fun blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
bitss bisim_depths mono_Ts nonmono_Ts =
let
- (* typ -> block *)
val block_for = block_for_type hol_ctxt binarize cards_assigns maxes_assigns
iters_assigns bitss bisim_depths
val mono_block = maps block_for mono_Ts
@@ -291,10 +266,8 @@
val sync_threshold = 5
-(* int list -> int list list *)
fun all_combinations_ordered_smartly ks =
let
- (* int list -> int *)
fun cost_with_monos [] = 0
| cost_with_monos (k :: ks) =
if k < sync_threshold andalso forall (curry (op =) k) ks then
@@ -315,16 +288,13 @@
|> sort (int_ord o pairself fst) |> map snd
end
-(* typ -> bool *)
fun is_self_recursive_constr_type T =
exists (exists_subtype (curry (op =) (body_type T))) (binder_types T)
-(* (styp * int) list -> styp -> int *)
fun constr_max maxes x = the_default ~1 (AList.lookup (op =) maxes x)
type scope_desc = (typ * int) list * (styp * int) list
-(* hol_context -> bool -> scope_desc -> typ * int -> bool *)
fun is_surely_inconsistent_card_assign hol_ctxt binarize
(card_assigns, max_assigns) (T, k) =
case binarized_and_boxed_datatype_constrs hol_ctxt binarize T of
@@ -335,22 +305,17 @@
map (Integer.prod o map (bounded_card_of_type k ~1 card_assigns)
o binder_types o snd) xs
val maxes = map (constr_max max_assigns) xs
- (* int -> int -> int *)
fun effective_max card ~1 = card
| effective_max card max = Int.min (card, max)
val max = map2 effective_max dom_cards maxes |> Integer.sum
in max < k end
-(* hol_context -> bool -> (typ * int) list -> (typ * int) list
- -> (styp * int) list -> bool *)
fun is_surely_inconsistent_scope_description hol_ctxt binarize seen rest
max_assigns =
exists (is_surely_inconsistent_card_assign hol_ctxt binarize
(seen @ rest, max_assigns)) seen
-(* hol_context -> bool -> scope_desc -> (typ * int) list option *)
fun repair_card_assigns hol_ctxt binarize (card_assigns, max_assigns) =
let
- (* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
fun aux seen [] = SOME seen
| aux _ ((_, 0) :: _) = NONE
| aux seen ((T, k) :: rest) =
@@ -364,7 +329,6 @@
handle SAME () => aux seen ((T, k - 1) :: rest)
in aux [] (rev card_assigns) end
-(* theory -> (typ * int) list -> typ * int -> typ * int *)
fun repair_iterator_assign thy assigns (T as Type (_, Ts), k) =
(T, if T = @{typ bisim_iterator} then
let
@@ -378,15 +342,12 @@
k)
| repair_iterator_assign _ _ assign = assign
-(* row -> scope_desc -> scope_desc *)
fun add_row_to_scope_descriptor (kind, ks) (card_assigns, max_assigns) =
case kind of
Card T => ((T, the_single ks) :: card_assigns, max_assigns)
| Max x => (card_assigns, (x, the_single ks) :: max_assigns)
-(* block -> scope_desc *)
fun scope_descriptor_from_block block =
fold_rev add_row_to_scope_descriptor block ([], [])
-(* hol_context -> bool -> block list -> int list -> scope_desc option *)
fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) binarize blocks
columns =
let
@@ -400,11 +361,8 @@
end
handle Option.Option => NONE
-(* (typ * int) list -> dtype_spec list -> int Typtab.table *)
fun offset_table_for_card_assigns assigns dtypes =
let
- (* int -> (int * int) list -> (typ * int) list -> int Typtab.table
- -> int Typtab.table *)
fun aux next _ [] = Typtab.update_new (dummyT, next)
| aux next reusable ((T, k) :: assigns) =
if k = 1 orelse is_iterator_type T orelse is_integer_type T
@@ -420,18 +378,14 @@
#> aux (next + k) ((k, next) :: reusable) assigns
in aux 0 [] assigns Typtab.empty end
-(* int -> (typ * int) list -> typ -> int *)
fun domain_card max card_assigns =
Integer.prod o map (bounded_card_of_type max max card_assigns) o binder_types
-(* scope_desc -> bool -> int -> (int -> int) -> int -> int -> bool * styp
- -> constr_spec list -> constr_spec list *)
fun add_constr_spec (card_assigns, max_assigns) co card sum_dom_cards
num_self_recs num_non_self_recs (self_rec, x as (_, T))
constrs =
let
val max = constr_max max_assigns x
- (* unit -> int *)
fun next_delta () = if null constrs then 0 else #epsilon (hd constrs)
val {delta, epsilon, exclusive, total} =
if max = 0 then
@@ -467,7 +421,6 @@
explicit_max = max, total = total} :: constrs
end
-(* hol_context -> bool -> typ list -> (typ * int) list -> typ -> bool *)
fun has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T =
let val card = card_of_type card_assigns T in
card = bounded_exact_card_of_type hol_ctxt
@@ -475,8 +428,6 @@
card_assigns T
end
-(* hol_context -> bool -> typ list -> typ list -> scope_desc -> typ * int
- -> dtype_spec *)
fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, stds, ...}) binarize
deep_dataTs finitizable_dataTs (desc as (card_assigns, _)) (T, card) =
let
@@ -487,7 +438,6 @@
val self_recs = map (is_self_recursive_constr_type o snd) xs
val (num_self_recs, num_non_self_recs) =
List.partition I self_recs |> pairself length
- (* bool -> bool *)
fun is_complete facto =
has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T
fun is_concrete facto =
@@ -497,7 +447,6 @@
card_assigns)
val complete = pair_from_fun is_complete
val concrete = pair_from_fun is_concrete
- (* int -> int *)
fun sum_dom_cards max =
map (domain_card max card_assigns o snd) xs |> Integer.sum
val constrs =
@@ -509,7 +458,6 @@
concrete = concrete, deep = deep, constrs = constrs}
end
-(* hol_context -> bool -> int -> typ list -> typ list -> scope_desc -> scope *)
fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize sym_break
deep_dataTs finitizable_dataTs
(desc as (card_assigns, _)) =
@@ -530,8 +478,6 @@
else offset_table_for_card_assigns card_assigns datatypes}
end
-(* theory -> typ list -> (typ option * int list) list
- -> (typ option * int list) list *)
fun repair_cards_assigns_wrt_boxing_etc _ _ [] = []
| repair_cards_assigns_wrt_boxing_etc thy Ts ((SOME T, ks) :: cards_assigns) =
(if is_fun_type T orelse is_pair_type T then
@@ -545,9 +491,6 @@
val max_scopes = 4096
val distinct_threshold = 512
-(* hol_context -> bool -> int -> (typ option * int list) list
- -> (styp option * int list) list -> (styp option * int list) list -> int list
- -> typ list -> typ list -> typ list ->typ list -> int * scope list *)
fun all_scopes (hol_ctxt as {thy, ...}) binarize sym_break cards_assigns
maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
deep_dataTs finitizable_dataTs =
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Sat Apr 24 16:33:01 2010 +0200
@@ -292,7 +292,6 @@
*)
]
-(* Proof.context -> string * nut -> Kodkod.problem *)
fun problem_for_nut ctxt (name, u) =
let
val debug = false
@@ -319,7 +318,6 @@
formula = formula}
end
-(* unit -> unit *)
fun run_all_tests () =
case Kodkod.solve_any_problem false NONE 0 1
(map (problem_for_nut @{context}) tests) of
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Apr 24 16:33:01 2010 +0200
@@ -85,24 +85,18 @@
val nitpick_prefix = "Nitpick."
-(* ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd *)
fun curry3 f = fn x => fn y => fn z => f (x, y, z)
fun pairf f g x = (f x, g x)
-(* (bool -> 'a) -> 'a * 'a *)
fun pair_from_fun f = (f false, f true)
-(* 'a * 'a -> bool -> 'a *)
fun fun_from_pair (f, t) b = if b then t else f
-(* bool -> int *)
fun int_from_bool b = if b then 1 else 0
-(* int -> int -> int *)
fun nat_minus i j = if i > j then i - j else 0
val max_exponent = 16384
-(* int -> int -> int *)
fun reasonable_power _ 0 = 1
| reasonable_power a 1 = a
| reasonable_power 0 _ = 0
@@ -119,7 +113,6 @@
c * c * reasonable_power a (b mod 2)
end
-(* int -> int -> int *)
fun exact_log m n =
let
val r = Math.ln (Real.fromInt n) / Math.ln (Real.fromInt m) |> Real.round
@@ -131,7 +124,6 @@
commas (map signed_string_of_int [m, n]))
end
-(* int -> int -> int *)
fun exact_root m n =
let val r = Math.pow (Real.fromInt n, 1.0 / (Real.fromInt m)) |> Real.round in
if reasonable_power r m = n then
@@ -141,22 +133,16 @@
commas (map signed_string_of_int [m, n]))
end
-(* ('a -> 'a -> 'a) -> 'a list -> 'a *)
fun fold1 f = foldl1 (uncurry f)
-(* int -> 'a list -> 'a list *)
fun replicate_list 0 _ = []
| replicate_list n xs = xs @ replicate_list (n - 1) xs
-(* int list -> int list *)
fun offset_list ns = rev (tl (fold (fn x => fn xs => (x + hd xs) :: xs) ns [0]))
-(* int -> int -> int list *)
fun index_seq j0 n = if j0 < 0 then j0 downto j0 - n + 1 else j0 upto j0 + n - 1
-(* int list -> 'a list -> 'a list *)
fun filter_indices js xs =
let
- (* int -> int list -> 'a list -> 'a list *)
fun aux _ [] _ = []
| aux i (j :: js) (x :: xs) =
if i = j then x :: aux (i + 1) js xs else aux (i + 1) (j :: js) xs
@@ -165,7 +151,6 @@
in aux 0 js xs end
fun filter_out_indices js xs =
let
- (* int -> int list -> 'a list -> 'a list *)
fun aux _ [] xs = xs
| aux i (j :: js) (x :: xs) =
if i = j then aux (i + 1) js xs else x :: aux (i + 1) (j :: js) xs
@@ -173,86 +158,66 @@
"indices unordered or out of range")
in aux 0 js xs end
-(* 'a list -> 'a list list -> 'a list list *)
fun cartesian_product [] _ = []
| cartesian_product (x :: xs) yss =
map (cons x) yss @ cartesian_product xs yss
-(* 'a list list -> 'a list list *)
fun n_fold_cartesian_product xss = fold_rev cartesian_product xss [[]]
-(* ''a list -> (''a * ''a) list *)
fun all_distinct_unordered_pairs_of [] = []
| all_distinct_unordered_pairs_of (x :: xs) =
map (pair x) xs @ all_distinct_unordered_pairs_of xs
-(* (int * int) list -> int -> int list *)
val nth_combination =
let
- (* (int * int) list -> int -> int list * int *)
fun aux [] n = ([], n)
| aux ((k, j0) :: xs) n =
let val (js, n) = aux xs n in ((n mod k) + j0 :: js, n div k) end
in fst oo aux end
-(* (int * int) list -> int list list *)
val all_combinations = n_fold_cartesian_product o map (uncurry index_seq o swap)
-(* 'a list -> 'a list list *)
fun all_permutations [] = [[]]
| all_permutations xs =
maps (fn j => map (cons (nth xs j)) (all_permutations (nth_drop j xs)))
(index_seq 0 (length xs))
-(* int -> 'a list -> 'a list list *)
fun batch_list _ [] = []
| batch_list k xs =
if length xs <= k then [xs]
else List.take (xs, k) :: batch_list k (List.drop (xs, k))
-(* int list -> 'a list -> 'a list list *)
fun chunk_list_unevenly _ [] = []
| chunk_list_unevenly [] ys = map single ys
| chunk_list_unevenly (k :: ks) ys =
let val (ys1, ys2) = chop k ys in ys1 :: chunk_list_unevenly ks ys2 end
-(* ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list *)
fun map3 _ [] [] [] = []
| map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
| map3 _ _ _ _ = raise UnequalLengths
-(* ('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option *)
fun double_lookup eq ps key =
case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps
(SOME key) of
SOME z => SOME z
| NONE => ps |> find_first (is_none o fst) |> Option.map snd
-(* (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option *)
fun triple_lookup _ [(NONE, z)] _ = SOME z
| triple_lookup eq ps key =
case AList.lookup (op =) ps (SOME key) of
SOME z => SOME z
| NONE => double_lookup eq ps key
-(* string -> string -> bool *)
fun is_substring_of needle stack =
not (Substring.isEmpty (snd (Substring.position needle
(Substring.full stack))))
-(* int -> string *)
val plural_s = Sledgehammer_Util.plural_s
-(* 'a list -> string *)
fun plural_s_for_list xs = plural_s (length xs)
-(* string -> string list -> string list *)
val serial_commas = Sledgehammer_Util.serial_commas
-(* unit -> string *)
val timestamp = Sledgehammer_Util.timestamp
-(* bool -> string -> string -> bool option *)
val parse_bool_option = Sledgehammer_Util.parse_bool_option
-(* string -> string -> Time.time option *)
val parse_time_option = Sledgehammer_Util.parse_time_option
-(* polarity -> polarity *)
fun flip_polarity Pos = Neg
| flip_polarity Neg = Pos
| flip_polarity Neut = Neut
@@ -262,42 +227,32 @@
val nat_T = @{typ nat}
val int_T = @{typ int}
-(* string -> string *)
val subscript = implode o map (prefix "\<^isub>") o explode
-(* int -> string *)
fun nat_subscript n =
(* cheap trick to ensure proper alphanumeric ordering for one- and two-digit
numbers *)
if n <= 9 then "\<^bsub>" ^ signed_string_of_int n ^ "\<^esub>"
else subscript (string_of_int n)
-(* Time.time option -> ('a -> 'b) -> 'a -> 'b *)
fun time_limit NONE = I
| time_limit (SOME delay) = TimeLimit.timeLimit delay
-(* Time.time option -> tactic -> tactic *)
fun DETERM_TIMEOUT delay tac st =
Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
-(* ('a -> 'b) -> 'a -> 'b *)
fun setmp_show_all_types f =
setmp_CRITICAL show_all_types
(! show_types orelse ! show_sorts orelse ! show_all_types) f
val indent_size = 2
-(* string -> Pretty.T list *)
val pstrs = Pretty.breaks o map Pretty.str o space_explode " "
-(* XML.tree -> string *)
fun plain_string_from_xml_tree t =
Buffer.empty |> XML.add_content t |> Buffer.content
-(* string -> string *)
val unyxml = plain_string_from_xml_tree o YXML.parse
-(* string -> bool *)
val is_long_identifier = forall Syntax.is_identifier o space_explode "."
-(* string -> string *)
fun maybe_quote y =
let val s = unyxml y in
y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
@@ -308,11 +263,8 @@
(* This hash function is recommended in Compilers: Principles, Techniques, and
Tools, by Aho, Sethi and Ullman. The hashpjw function, which they
particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
-(* word * word -> word *)
fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
-(* Char.char * word -> word *)
fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
-(* string * word -> word *)
fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s
end;