--- a/src/HOL/Tools/Nunchaku/nunchaku.ML Fri Sep 08 00:02:21 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML Fri Sep 08 00:02:21 2017 +0200
@@ -201,11 +201,15 @@
str_of_nun_model ugly_nun_model);
val pat_completes = pat_completes_of_isa_problem isa_problem;
- val isa_model = isa_model_of_nun ctxt pat_completes atomss ugly_nun_model;
- val _ = print_d (fn () => "*** Isabelle model ***\n" ^
- str_of_isa_model ctxt isa_model);
+ val raw_isa_model = isa_model_of_nun ctxt pat_completes atomss ugly_nun_model;
+ val _ = print_d (fn () => "*** Raw Isabelle model ***\n" ^
+ str_of_isa_model ctxt raw_isa_model);
+
+ val cleaned_isa_model = clean_up_isa_model ctxt raw_isa_model;
+ val _ = print_d (fn () => "*** Cleaned-up Isabelle model ***\n" ^
+ str_of_isa_model ctxt cleaned_isa_model);
in
- isa_model
+ cleaned_isa_model
end;
fun isa_model_opt output =
--- a/src/HOL/Tools/Nunchaku/nunchaku_display.ML Fri Sep 08 00:02:21 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_display.ML Fri Sep 08 00:02:21 2017 +0200
@@ -33,15 +33,11 @@
| sorting_str_of_term _ = "X";
fun pretty_of_isa_model_opt _ NONE =
- pretty_indent (Pretty.str "Model unavailable (internal error)")
- | pretty_of_isa_model_opt ctxt0
- (SOME {type_model, free_model, pat_complete_model, pat_incomplete_model, skolem_model}) =
+ pretty_indent (Pretty.str "Model unavailable due to internal error")
+ | pretty_of_isa_model_opt ctxt0 (SOME {type_model, free_model, pat_complete_model,
+ pat_incomplete_model, skolem_model, auxiliary_model}) =
let
val ctxt = ctxt0 |> Config.put show_question_marks false;
-
- val pat_incomplete_model' = pat_incomplete_model
- |> filter_out (can (fn Const (@{const_name unreachable}, _) => ()) o fst);
-
fun pretty_of_typ_entry (T, atoms) =
Pretty.block (Pretty.breaks [Syntax.pretty_typ ctxt T, Pretty.str "=",
Pretty.enum "," "{" "}" (map (Syntax.pretty_term ctxt) atoms)]);
@@ -76,13 +72,12 @@
else
chunks_of_entries sorting_str_of_term pretty_of_term_entry "" free_model) @
chunks_of_entries sorting_str_of_term pretty_of_term_entry "Skolem constant" skolem_model @
- chunks_of_entries sorting_str_of_term pretty_of_term_entry "Underspecified constant"
- pat_incomplete_model' @
- (if Config.get ctxt show_consts then
- chunks_of_entries sorting_str_of_term pretty_of_term_entry "Fully specified constant"
- pat_complete_model
- else
- []) @
+ chunks_of_entries sorting_str_of_term pretty_of_term_entry
+ "Potentially underspecified constant" pat_incomplete_model @
+ chunks_of_entries sorting_str_of_term pretty_of_term_entry "Fully specified constant"
+ pat_complete_model @
+ chunks_of_entries sorting_str_of_term pretty_of_term_entry "Auxiliary variable"
+ auxiliary_model @
chunks_of_entries sorting_str_of_typ pretty_of_typ_entry "Type" type_model;
in
Pretty.chunks chunks
--- a/src/HOL/Tools/Nunchaku/nunchaku_model.ML Fri Sep 08 00:02:21 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_model.ML Fri Sep 08 00:02:21 2017 +0200
@@ -18,7 +18,8 @@
type nun_model =
{type_model: ty_entry list,
const_model: tm_entry list,
- skolem_model: tm_entry list}
+ skolem_model: tm_entry list,
+ auxiliary_model: tm_entry list}
val str_of_nun_model: nun_model -> string
@@ -51,7 +52,8 @@
type nun_model =
{type_model: ty_entry list,
const_model: tm_entry list,
- skolem_model: tm_entry list};
+ skolem_model: tm_entry list,
+ auxiliary_model: tm_entry list};
fun base_of_id id = hd (space_explode "/" id);
@@ -63,9 +65,9 @@
fun str_of_tm_entry (tm, value) =
"val " ^ str_of_tm tm ^ " := " ^ str_of_tm value ^ ".";
-fun str_of_nun_model {type_model, const_model, skolem_model} =
+fun str_of_nun_model {type_model, const_model, skolem_model, auxiliary_model} =
map str_of_ty_entry type_model @ "" :: map str_of_tm_entry const_model @ "" ::
- map str_of_tm_entry skolem_model
+ map str_of_tm_entry skolem_model @ "" :: map str_of_tm_entry auxiliary_model
|> cat_lines;
fun fold_map_ty_entry_idents f (ty, atoms) =
@@ -76,12 +78,14 @@
fold_map_tm_idents f tm
##>> fold_map_tm_idents f value;
-fun fold_map_nun_model_idents f {type_model, const_model, skolem_model} =
+fun fold_map_nun_model_idents f {type_model, const_model, skolem_model, auxiliary_model} =
fold_map (fold_map_ty_entry_idents f) type_model
##>> fold_map (fold_map_tm_entry_idents f) const_model
##>> fold_map (fold_map_tm_entry_idents f) skolem_model
- #>> (fn ((type_model, const_model), skolem_model) =>
- {type_model = type_model, const_model = const_model, skolem_model = skolem_model});
+ ##>> fold_map (fold_map_tm_entry_idents f) auxiliary_model
+ #>> (fn (((type_model, const_model), skolem_model), auxiliary_model) =>
+ {type_model = type_model, const_model = const_model, skolem_model = skolem_model,
+ auxiliary_model = auxiliary_model});
fun swap_name_pool ({nice_of_ugly, ugly_of_nice} : name_pool) =
{nice_of_ugly = ugly_of_nice, ugly_of_nice = nice_of_ugly};
@@ -114,16 +118,18 @@
in
(case Int.fromString suf of
SOME j => Atom (ident_of_str pre, j)
- | NONE => raise Fail "ill-formed atom")
+ | NONE => raise Fail ("ill-formed atom: " ^ s))
end
- | NONE => raise Fail "ill-formed atom");
+ | NONE => raise Fail ("ill-formed atom: " ^ s));
fun is_alnum_etc_char c = Char.isAlphaNum c orelse c = #"_" orelse c = #"/";
+fun is_dollar_alnum_etc_char c = c = #"$" orelse is_alnum_etc_char c;
+
val multi_ids =
[nun_arrow, nun_assign, nun_conj, nun_disj, nun_implies, nun_unparsable, nun_irrelevant];
-val nun_anon_fun_prefix_exploded = String.explode nun_anon_fun_prefix;
+val nun_dollar_anon_fun_prefix_exploded = String.explode nun_dollar_anon_fun_prefix;
val [nun_dollar_char] = String.explode nun_dollar;
fun next_token [] = (End_of_Stream, [])
@@ -131,10 +137,10 @@
if Char.isSpace c then
next_token cs
else if c = nun_dollar_char then
- let val n = find_index (not o is_alnum_etc_char) cs in
+ let val n = find_index (not o is_dollar_alnum_etc_char) cs in
(if n = ~1 then (cs, []) else chop n cs)
|>> (String.implode
- #> (if is_prefix (op =) nun_anon_fun_prefix_exploded cs then ident_of_str #> Ident
+ #> (if is_prefix (op =) nun_dollar_anon_fun_prefix_exploded cs then ident_of_str #> Ident
else atom_of_str))
end
else if is_alnum_etc_char c then
@@ -221,9 +227,13 @@
>> (fn (tm, NONE) => tm
| (lhs, SOME (Symbol id, rhs)) => napps (NConst (id, [], dummy_ty), [lhs, rhs]))) toks
and parse_conj toks =
- (parse_equals -- Scan.option (parse_sym nun_conj -- parse_conj)
+ (parse_not -- Scan.option (parse_sym nun_conj -- parse_conj)
>> (fn (tm, NONE) => tm
| (lhs, SOME (Symbol id, rhs)) => napps (NConst (id, [], dummy_ty), [lhs, rhs]))) toks
+and parse_not toks =
+ (Scan.option (parse_sym nun_not) -- parse_equals
+ >> (fn (NONE, tm) => tm
+ | (SOME _, tm) => napps (NConst (nun_not, [], dummy_ty), [tm]))) toks
and parse_equals toks =
(parse_comb -- Scan.option (parse_sym nun_equals -- parse_comb)
>> (fn (tm, NONE) => tm
@@ -250,15 +260,23 @@
|-- Scan.option (parse_sym nun_lparen) |-- parse_witness_name
--| Scan.repeat (Scan.one (curry (op <>) (Symbol nun_assign)));
+val parse_anon_fun_name =
+ Scan.one (fn Ident id => String.isPrefix nun_dollar_anon_fun_prefix id | _ => false);
+
+val parse_anon_fun =
+ parse_anon_fun_name >> (fn Ident id => NConst (id, [], dummy_ty));
+
datatype entry =
Type_Entry of ty_entry
+| Const_Entry of tm_entry
| Skolem_Entry of tm_entry
-| Const_Entry of tm_entry;
+| Auxiliary_Entry of tm_entry;
val parse_entry =
(parse_id nun_type |-- parse_ty --| parse_sym nun_assign --| parse_sym nun_lbrace --
parse_enum (parse_sym nun_comma) parse_tm --| parse_sym nun_rbrace
>> Type_Entry
+ || parse_id nun_val |-- parse_anon_fun --| parse_sym nun_assign -- parse_tm >> Auxiliary_Entry
|| parse_id nun_val |-- parse_witness --| parse_sym nun_assign -- parse_tm >> Skolem_Entry
|| parse_id nun_val |-- parse_tm --| parse_sym nun_assign -- parse_tm >> Const_Entry)
--| parse_sym nun_dot;
@@ -267,18 +285,24 @@
parse_id nun_SAT |-- parse_sym nun_colon |-- parse_sym nun_lbrace |-- Scan.repeat parse_entry
--| parse_sym nun_rbrace;
-fun add_entry entry ({type_model, const_model, skolem_model} : nun_model) =
+fun add_entry entry ({type_model, const_model, skolem_model, auxiliary_model} : nun_model) =
(case entry of
Type_Entry e =>
- {type_model = e :: type_model, const_model = const_model, skolem_model = skolem_model}
+ {type_model = e :: type_model, const_model = const_model, skolem_model = skolem_model,
+ auxiliary_model = auxiliary_model}
+ | Const_Entry e =>
+ {type_model = type_model, const_model = e :: const_model, skolem_model = skolem_model,
+ auxiliary_model = auxiliary_model}
| Skolem_Entry e =>
- {type_model = type_model, const_model = const_model, skolem_model = e :: skolem_model}
- | Const_Entry e =>
- {type_model = type_model, const_model = e :: const_model, skolem_model = skolem_model});
+ {type_model = type_model, const_model = const_model, skolem_model = e :: skolem_model,
+ auxiliary_model = auxiliary_model}
+ | Auxiliary_Entry e =>
+ {type_model = type_model, const_model = const_model, skolem_model = skolem_model,
+ auxiliary_model = e :: auxiliary_model});
fun nun_model_of_str str =
let val (entries, _) = parse_model (tokenize str) in
- {type_model = [], const_model = [], skolem_model = []}
+ {type_model = [], const_model = [], skolem_model = [], auxiliary_model = []}
|> fold_rev add_entry entries
end;
--- a/src/HOL/Tools/Nunchaku/nunchaku_problem.ML Fri Sep 08 00:02:21 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_problem.ML Fri Sep 08 00:02:21 2017 +0200
@@ -68,7 +68,6 @@
val nun_abstract: string
val nun_and: string
- val nun_anon_fun_prefix: string
val nun_arrow: string
val nun_asserting: string
val nun_assign: string
@@ -86,6 +85,7 @@
val nun_data: string
val nun_disj: string
val nun_dollar: string
+ val nun_dollar_anon_fun_prefix: string
val nun_dot: string
val nun_dummy: string
val nun_else: string
@@ -241,7 +241,6 @@
val nun_abstract = "abstract";
val nun_and = "and";
-val nun_anon_fun_prefix = "anon_fun_";
val nun_arrow = "->";
val nun_asserting = "asserting";
val nun_assign = ":=";
@@ -259,6 +258,7 @@
val nun_data = "data";
val nun_disj = "||";
val nun_dollar = "$";
+val nun_dollar_anon_fun_prefix = "$anon_fun_";
val nun_dot = ".";
val nun_dummy = "_";
val nun_else = "else";
--- a/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML Fri Sep 08 00:02:21 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML Fri Sep 08 00:02:21 2017 +0200
@@ -17,12 +17,14 @@
free_model: term_entry list,
pat_complete_model: term_entry list,
pat_incomplete_model: term_entry list,
- skolem_model: term_entry list}
+ skolem_model: term_entry list,
+ auxiliary_model: term_entry list}
val str_of_isa_model: Proof.context -> isa_model -> string
val isa_model_of_nun: Proof.context -> term list -> (typ option * string list) list ->
nun_model -> isa_model
+ val clean_up_isa_model: Proof.context -> isa_model -> isa_model
end;
structure Nunchaku_Reconstruct : NUNCHAKU_RECONSTRUCT =
@@ -41,7 +43,8 @@
free_model: term_entry list,
pat_complete_model: term_entry list,
pat_incomplete_model: term_entry list,
- skolem_model: term_entry list};
+ skolem_model: term_entry list,
+ auxiliary_model: term_entry list};
val anonymousN = "anonymous";
val irrelevantN = "irrelevant";
@@ -95,12 +98,14 @@
"val " ^ Syntax.string_of_term ctxt tm ^ " := " ^ Syntax.string_of_term ctxt value ^ ".";
fun str_of_isa_model ctxt
- {type_model, free_model, pat_complete_model, pat_incomplete_model, skolem_model} =
+ {type_model, free_model, pat_complete_model, pat_incomplete_model, skolem_model,
+ auxiliary_model} =
map (str_of_typ_entry ctxt) type_model @ "" ::
map (str_of_term_entry ctxt) free_model @ "" ::
map (str_of_term_entry ctxt) pat_complete_model @ "" ::
map (str_of_term_entry ctxt) pat_incomplete_model @ "" ::
- map (str_of_term_entry ctxt) skolem_model
+ map (str_of_term_entry ctxt) skolem_model @ "" ::
+ map (str_of_term_entry ctxt) auxiliary_model
|> cat_lines;
fun typ_of_nun ctxt =
@@ -154,10 +159,10 @@
| term_of bounds (NConst (id, tys0, ty)) =
if id = nun_conj then
HOLogic.conj
+ else if id = nun_choice then
+ Const (@{const_name Eps}, typ_of ty)
else if id = nun_disj then
HOLogic.disj
- else if id = nun_choice then
- Const (@{const_name Eps}, typ_of ty)
else if id = nun_equals then
Const (@{const_name HOL.eq}, typ_of ty)
else if id = nun_false then
@@ -166,14 +171,16 @@
Const (@{const_name If}, typ_of ty)
else if id = nun_implies then
@{term implies}
+ else if id = nun_not then
+ HOLogic.Not
else if id = nun_unique then
Const (@{const_name The}, typ_of ty)
else if id = nun_unique_unsafe then
Const (@{const_name The_unsafe}, typ_of ty)
else if id = nun_true then
@{const True}
- else if String.isPrefix nun_anon_fun_prefix id then
- let val j = Int.fromString (unprefix nun_anon_fun_prefix id) |> the_default ~1 in
+ else if String.isPrefix nun_dollar_anon_fun_prefix id then
+ let val j = Int.fromString (unprefix nun_dollar_anon_fun_prefix id) |> the_default ~1 in
Var ((anonymousN ^ nat_subscript (j + 1), 0), typ_of ty)
end
else if String.isPrefix nun_irrelevant id then
@@ -227,7 +234,8 @@
fun isa_term_entry_of_nun ctxt atomss (tm, value) =
(term_of_nun ctxt atomss tm, term_of_nun ctxt atomss value);
-fun isa_model_of_nun ctxt pat_completes atomss {type_model, const_model, skolem_model} =
+fun isa_model_of_nun ctxt pat_completes atomss
+ {type_model, const_model, skolem_model, auxiliary_model} =
let
val free_and_const_model = map (isa_term_entry_of_nun ctxt atomss) const_model;
val (free_model, (pat_complete_model, pat_incomplete_model)) =
@@ -236,7 +244,31 @@
in
{type_model = map (isa_typ_entry_of_nun ctxt atomss) type_model, free_model = free_model,
pat_complete_model = pat_complete_model, pat_incomplete_model = pat_incomplete_model,
- skolem_model = map (isa_term_entry_of_nun ctxt atomss) skolem_model}
+ skolem_model = map (isa_term_entry_of_nun ctxt atomss) skolem_model,
+ auxiliary_model = map (isa_term_entry_of_nun ctxt atomss) auxiliary_model}
+ end;
+
+fun clean_up_isa_model ctxt {type_model, free_model, pat_complete_model, pat_incomplete_model,
+ skolem_model, auxiliary_model} =
+ let
+ val pat_complete_model' = if Config.get ctxt show_consts then pat_complete_model else [];
+ val pat_incomplete_model' = pat_incomplete_model
+ |> filter_out (can (fn Const (@{const_name unreachable}, _) => ()) o fst);
+
+ val term_model = free_model @ pat_complete_model' @ pat_incomplete_model' @
+ skolem_model @ auxiliary_model;
+
+ (* Incomplete test: Can be led astray by references between the auxiliaries. *)
+ fun is_auxiliary_referenced (aux, _) =
+ exists (fn (lhs, rhs) =>
+ not (lhs aconv aux) andalso exists_subterm (curry (op aconv) aux) rhs)
+ term_model;
+
+ val auxiliary_model' = filter is_auxiliary_referenced auxiliary_model;
+ in
+ {type_model = type_model, free_model = free_model, pat_complete_model = pat_complete_model',
+ pat_incomplete_model = pat_incomplete_model', skolem_model = skolem_model,
+ auxiliary_model = auxiliary_model'}
end;
end;