more informative error;
authorwenzelm
Mon Feb 17 17:49:29 2014 +0100 (2014-02-17)
changeset 55543f0ef75c6c0d8
parent 55537 6ec3c2c38650
child 55544 cf1baba89a27
more informative error;
src/HOL/Predicate_Compile.thy
src/HOL/Tools/Predicate_Compile/core_data.ML
     1.1 --- a/src/HOL/Predicate_Compile.thy	Mon Feb 17 14:59:09 2014 +0100
     1.2 +++ b/src/HOL/Predicate_Compile.thy	Mon Feb 17 17:49:29 2014 +0100
     1.3 @@ -81,6 +81,7 @@
     1.4    Core_Data.PredData.map (Graph.new_node 
     1.5      (@{const_name contains}, 
     1.6       Core_Data.PredData {
     1.7 +       pos = Position.thread_data (),
     1.8         intros = [(NONE, @{thm containsI})], 
     1.9         elim = SOME @{thm containsE}, 
    1.10         preprocessed = true,
     2.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Mon Feb 17 14:59:09 2014 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Mon Feb 17 17:49:29 2014 +0100
     2.3 @@ -18,6 +18,7 @@
     2.4    };
     2.5  
     2.6    datatype pred_data = PredData of {
     2.7 +    pos : Position.T,
     2.8      intros : (string option * thm) list,
     2.9      elim : thm option,
    2.10      preprocessed : bool,
    2.11 @@ -100,6 +101,7 @@
    2.12    PredfunData {definition = definition, intro = intro, elim = elim, neg_intro = neg_intro}
    2.13  
    2.14  datatype pred_data = PredData of {
    2.15 +  pos: Position.T,
    2.16    intros : (string option * thm) list,
    2.17    elim : thm option,
    2.18    preprocessed : bool,
    2.19 @@ -109,13 +111,17 @@
    2.20  };
    2.21  
    2.22  fun rep_pred_data (PredData data) = data;
    2.23 +val pos_of = #pos o rep_pred_data;
    2.24  
    2.25 -fun mk_pred_data (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))) =
    2.26 -  PredData {intros = intros, elim = elim, preprocessed = preprocessed,
    2.27 +fun mk_pred_data
    2.28 +    (pos, (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random)))) =
    2.29 +  PredData {pos = pos, intros = intros, elim = elim, preprocessed = preprocessed,
    2.30      function_names = function_names, predfun_data = predfun_data, needs_random = needs_random}
    2.31  
    2.32 -fun map_pred_data f (PredData {intros, elim, preprocessed, function_names, predfun_data, needs_random}) =
    2.33 -  mk_pred_data (f (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random))))
    2.34 +fun map_pred_data f
    2.35 +    (PredData {pos, intros, elim, preprocessed, function_names, predfun_data, needs_random}) =
    2.36 +  mk_pred_data
    2.37 +    (f (pos, (((intros, elim), preprocessed), (function_names, (predfun_data, needs_random)))))
    2.38  
    2.39  fun eq_option eq (NONE, NONE) = true
    2.40    | eq_option eq (SOME x, SOME y) = eq (x, y)
    2.41 @@ -130,7 +136,13 @@
    2.42    type T = pred_data Graph.T;
    2.43    val empty = Graph.empty;
    2.44    val extend = I;
    2.45 -  val merge = Graph.merge eq_pred_data;
    2.46 +  val merge =
    2.47 +    Graph.join (fn key => fn (x, y) =>
    2.48 +      if eq_pred_data (x, y)
    2.49 +      then raise Graph.SAME
    2.50 +      else
    2.51 +        error ("Duplicate predicate declarations for " ^ quote key ^
    2.52 +          Position.here (pos_of x) ^ Position.here (pos_of y)));
    2.53  );
    2.54  
    2.55  
    2.56 @@ -260,11 +272,13 @@
    2.57    (case try (Inductive.the_inductive ctxt) name of
    2.58      SOME (info as (_, result)) => 
    2.59        let
    2.60 +        val thy = Proof_Context.theory_of ctxt
    2.61 +
    2.62 +        val pos = Position.thread_data ()
    2.63          fun is_intro_of intro =
    2.64            let
    2.65              val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
    2.66            in (fst (dest_Const const) = name) end;
    2.67 -        val thy = Proof_Context.theory_of ctxt
    2.68          val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result))
    2.69          val index = find_index (fn s => s = name) (#names (fst info))
    2.70          val pre_elim = nth (#elims result) index
    2.71 @@ -273,13 +287,13 @@
    2.72          val nparams = length (Inductive.params_of (#raw_induct result))
    2.73          val elim = prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
    2.74        in
    2.75 -        mk_pred_data (((map (pair NONE) intros, SOME elim), true), no_compilation)
    2.76 +        mk_pred_data (pos, (((map (pair NONE) intros, SOME elim), true), no_compilation))
    2.77        end
    2.78    | NONE => error ("No such predicate: " ^ quote name))
    2.79  
    2.80  fun add_predfun_data name mode data =
    2.81    let
    2.82 -    val add = (apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))
    2.83 +    val add = (apsnd o apsnd o apsnd o apfst) (cons (mode, mk_predfun_data data))
    2.84    in PredData.map (Graph.map_node name (map_pred_data add)) end
    2.85  
    2.86  fun is_inductive_predicate ctxt name =
    2.87 @@ -305,17 +319,21 @@
    2.88        (case try (Graph.get_node gr) name of
    2.89          SOME _ =>
    2.90            Graph.map_node name (map_pred_data
    2.91 -            (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr
    2.92 +            (apsnd (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)])))))) gr
    2.93        | NONE =>
    2.94            Graph.new_node
    2.95 -            (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr)
    2.96 +            (name,
    2.97 +              mk_pred_data (Position.thread_data (),
    2.98 +                (((([(opt_case_name, thm)], NONE), false), no_compilation)))) gr)
    2.99    in PredData.map cons_intro thy end
   2.100  
   2.101  fun set_elim thm =
   2.102    let
   2.103      val (name, _) =
   2.104        dest_Const (fst (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
   2.105 -  in PredData.map (Graph.map_node name (map_pred_data (apfst (apfst (apsnd (K (SOME thm))))))) end
   2.106 +  in
   2.107 +    PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (apfst (apsnd (K (SOME thm))))))))
   2.108 +  end
   2.109  
   2.110  fun register_predicate (constname, intros, elim) thy =
   2.111    let
   2.112 @@ -324,7 +342,8 @@
   2.113      if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
   2.114        PredData.map
   2.115          (Graph.new_node (constname,
   2.116 -          mk_pred_data (((named_intros, SOME elim), false), no_compilation))) thy
   2.117 +          mk_pred_data (Position.thread_data (),
   2.118 +            (((named_intros, SOME elim), false), no_compilation)))) thy
   2.119      else thy
   2.120    end
   2.121  
   2.122 @@ -345,14 +364,14 @@
   2.123  
   2.124  fun defined_function_of compilation pred =
   2.125    let
   2.126 -    val set = (apsnd o apfst) (cons (compilation, []))
   2.127 +    val set = (apsnd o apsnd o apfst) (cons (compilation, []))
   2.128    in
   2.129      PredData.map (Graph.map_node pred (map_pred_data set))
   2.130    end
   2.131  
   2.132  fun set_function_name compilation pred mode name =
   2.133    let
   2.134 -    val set = (apsnd o apfst)
   2.135 +    val set = (apsnd o apsnd o apfst)
   2.136        (AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name)))
   2.137    in
   2.138      PredData.map (Graph.map_node pred (map_pred_data set))
   2.139 @@ -360,7 +379,7 @@
   2.140  
   2.141  fun set_needs_random name modes =
   2.142    let
   2.143 -    val set = (apsnd o apsnd o apsnd) (K modes)
   2.144 +    val set = (apsnd o apsnd o apsnd o apsnd) (K modes)
   2.145    in
   2.146      PredData.map (Graph.map_node name (map_pred_data set))
   2.147    end  
   2.148 @@ -389,7 +408,7 @@
   2.149    end
   2.150  
   2.151  fun preprocess_intros name thy =
   2.152 -  PredData.map (Graph.map_node name (map_pred_data (apfst (fn (rules, preprocessed) =>
   2.153 +  PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (fn (rules, preprocessed) =>
   2.154      if preprocessed then (rules, preprocessed)
   2.155      else
   2.156        let
   2.157 @@ -401,7 +420,7 @@
   2.158          val elim' = prove_casesrule ctxt (pred, (elim, 0)) elim_t
   2.159        in
   2.160          ((named_intros', SOME elim'), true)
   2.161 -      end))))
   2.162 +      end)))))
   2.163      thy  
   2.164  
   2.165  
   2.166 @@ -422,7 +441,7 @@
   2.167    AList.lookup eq_mode
   2.168      (Symtab.lookup_list (Alt_Compilations_Data.get (Proof_Context.theory_of ctxt)) pred_name) mode
   2.169  
   2.170 -fun force_modes_and_compilations pred_name compilations =
   2.171 +fun force_modes_and_compilations pred_name compilations thy =
   2.172    let
   2.173      (* thm refl is a dummy thm *)
   2.174      val modes = map fst compilations
   2.175 @@ -435,11 +454,14 @@
   2.176        map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations
   2.177      val alt_compilations = map (apsnd fst) compilations
   2.178    in
   2.179 +    thy |>
   2.180      PredData.map
   2.181        (Graph.new_node
   2.182          (pred_name,
   2.183 -          mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))
   2.184 -    #> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
   2.185 +          mk_pred_data
   2.186 +            (Position.thread_data (),
   2.187 +              ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random))))))
   2.188 +    |> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
   2.189    end
   2.190  
   2.191  fun functional_compilation fun_name mode compfuns T =