# HG changeset patch
# User blanchet
# Date 1504821725 -7200
# Node ID ee56847876b27d316d6d60c402fc818787797977
# Parent  7706577cd10e08119d2b63c7a8d88dfb9b106f92
updated parser for Nunchaku irrelevant output

diff -r 7706577cd10e -r ee56847876b2 src/HOL/Tools/Nunchaku/nunchaku_model.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_model.ML	Fri Sep 08 00:01:52 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_model.ML	Fri Sep 08 00:02:05 2017 +0200
@@ -53,6 +53,8 @@
    const_model: tm_entry list,
    skolem_model: tm_entry list};
 
+fun base_of_id id = hd (space_explode "/" id);
+
 val nun_SAT = str_of_ident "SAT";
 
 fun str_of_ty_entry (ty, tms) =
@@ -231,9 +233,8 @@
 and parse_arg toks =
   (parse_choice_or_unique
    || parse_ident >> (fn id => NConst (id, [], dummy_ty))
-   || parse_sym nun_irrelevant
-      |-- Scan.option (parse_sym nun_lparen |-- parse_tm --| parse_sym nun_rparen) (* FIXME *)
-     >> (fn _ => NConst (nun_irrelevant, [], dummy_ty))
+   || parse_sym nun_irrelevant |-- parse_ident
+     >> (fn num => NConst (nun_irrelevant ^ num, [], dummy_ty))
    || parse_sym nun_unparsable |-- parse_ty >> (fn ty => NConst (nun_unparsable, [], ty))
    || parse_sym nun_lparen |-- parse_tm -- Scan.option (parse_sym nun_colon |-- parse_ty)
       --| parse_sym nun_rparen
@@ -242,7 +243,7 @@
    || parse_atom >> (fn (id, j) => NAtom (j, NType (id, [])))) toks;
 
 val parse_witness_name =
-  parse_ident >> (fn id => NConst (hd (space_explode "/" id), [], dummy_ty));
+  parse_ident >> (fn id => NConst (base_of_id id, [], dummy_ty));
 
 val parse_witness =
   parse_id nun__witness_of |-- parse_sym nun_lparen |-- (parse_id nun_forall || parse_id nun_exists)
diff -r 7706577cd10e -r ee56847876b2 src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML	Fri Sep 08 00:01:52 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML	Fri Sep 08 00:02:05 2017 +0200
@@ -176,13 +176,11 @@
           let val j = Int.fromString (unprefix nun_anon_fun_prefix id) |> the_default ~1 in
             Var ((anonymousN ^ nat_subscript (j + 1), 0), typ_of ty)
           end
-        else if id = nun_irrelevant then
-          (* FIXME: get bounds from Nunchaku *)
-          list_comb (Var ((irrelevantN, 0), map (typ_of o safe_ty_of) bounds ---> typ_of ty),
-            map Bound (length bounds - 1 downto 0))
+        else if String.isPrefix nun_irrelevant id then
+          Var ((irrelevantN ^ nat_subscript (Value.parse_int (unprefix nun_irrelevant id)), 0),
+            dummyT)
         else if id = nun_unparsable then
-          (* FIXME: get bounds from Nunchaku *)
-          list_comb (Var ((unparsableN, 0), typ_of ty), map Bound (length bounds - 1 downto 0))
+          Var ((unparsableN, 0), typ_of ty)
         else
           (case try str_of_nun_const id of
             SOME (args, s) =>