- Inserted additional check for equality types in check_mode_clause that
authorberghofe
Thu Sep 23 10:20:52 2004 +0200 (2004-09-23)
changeset 15204d15f85347fcb
parent 15203 4481ada46cbb
child 15205 ecf9a884970d
- Inserted additional check for equality types in check_mode_clause that
avoids ill-typed code to be generated.
- Mode inference algorithm now outputs additional diagnostic messages.
src/HOL/Tools/inductive_codegen.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Sep 22 22:29:24 2004 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Sep 23 10:20:52 2004 +0200
     1.3 @@ -157,6 +157,15 @@
     1.4  
     1.5  (**** mode inference ****)
     1.6  
     1.7 +fun string_of_mode (iss, is) = space_implode " -> " (map
     1.8 +  (fn None => "X"
     1.9 +    | Some js => enclose "[" "]" (commas (map string_of_int js)))
    1.10 +       (iss @ [Some is]));
    1.11 +
    1.12 +fun print_modes modes = message ("Inferred modes:\n" ^
    1.13 +  space_implode "\n" (map (fn (s, ms) => s ^ ": " ^ commas (map
    1.14 +    string_of_mode ms)) modes));
    1.15 +
    1.16  val term_vs = map (fst o fst o dest_Var) o term_vars;
    1.17  val terms_vs = distinct o flat o (map term_vs);
    1.18  
    1.19 @@ -235,12 +244,12 @@
    1.20          | Some (x, _) => check_mode_prems
    1.21              (case x of Prem (us, _) => vs union terms_vs us | _ => vs)
    1.22              (filter_out (equal x) ps));
    1.23 -    val (in_ts', _) = get_args is 1 ts;
    1.24 -    val in_ts = filter (is_constrt thy) in_ts';
    1.25 +    val (in_ts, in_ts') = partition (is_constrt thy) (fst (get_args is 1 ts));
    1.26      val in_vs = terms_vs in_ts;
    1.27      val concl_vs = terms_vs ts
    1.28    in
    1.29      forall is_eqT (map snd (duplicates (flat (map term_vTs in_ts)))) andalso
    1.30 +    forall (is_eqT o fastype_of) in_ts' andalso
    1.31      (case check_mode_prems (arg_vs union in_vs) ps of
    1.32         None => false
    1.33       | Some vs => concl_vs subset vs)
    1.34 @@ -248,7 +257,12 @@
    1.35  
    1.36  fun check_modes_pred thy arg_vs preds modes (p, ms) =
    1.37    let val Some rs = assoc (preds, p)
    1.38 -  in (p, filter (fn m => forall (check_mode_clause thy arg_vs modes m) rs) ms) end
    1.39 +  in (p, filter (fn m => case find_index
    1.40 +    (not o check_mode_clause thy arg_vs modes m) rs of
    1.41 +      ~1 => true
    1.42 +    | i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^
    1.43 +      p ^ " violates mode " ^ string_of_mode m); false)) ms)
    1.44 +  end;
    1.45  
    1.46  fun fixp f x =
    1.47    let val y = f x
    1.48 @@ -492,15 +506,6 @@
    1.49    (map ((fn (Some (Modes x), _) => x | _ => ([], [])) o Graph.get_node gr)
    1.50      (Graph.all_preds gr [dep]))));
    1.51  
    1.52 -fun string_of_mode (iss, is) = space_implode " -> " (map
    1.53 -  (fn None => "X"
    1.54 -    | Some js => enclose "[" "]" (commas (map string_of_int js)))
    1.55 -       (iss @ [Some is]));
    1.56 -
    1.57 -fun print_modes modes = message ("Inferred modes:\n" ^
    1.58 -  space_implode "\n" (map (fn (s, ms) => s ^ ": " ^ commas (map
    1.59 -    string_of_mode ms)) modes));
    1.60 -
    1.61  fun print_factors factors = message ("Factors:\n" ^
    1.62    space_implode "\n" (map (fn (s, (fs, f)) => s ^ ": " ^
    1.63      space_implode " -> " (map