# HG changeset patch
# User blanchet
# Date 1504821741 -7200
# Node ID 8fc868e9e1bf25a64437d1ca9df4ff79735da81c
# Parent  0916eb2dbaca7fa9530663652e1e678d8b18fb55
better model parsing and display in Nunchaku

diff -r 0916eb2dbaca -r 8fc868e9e1bf src/HOL/Tools/Nunchaku/nunchaku.ML
--- 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 =
diff -r 0916eb2dbaca -r 8fc868e9e1bf src/HOL/Tools/Nunchaku/nunchaku_display.ML
--- 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
diff -r 0916eb2dbaca -r 8fc868e9e1bf src/HOL/Tools/Nunchaku/nunchaku_model.ML
--- 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;
 
diff -r 0916eb2dbaca -r 8fc868e9e1bf src/HOL/Tools/Nunchaku/nunchaku_problem.ML
--- 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";
diff -r 0916eb2dbaca -r 8fc868e9e1bf src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML
--- 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;