moved inductive_codegen to place where product type is available; tuned structure name
authorhaftmann
Thu Jun 10 12:24:02 2010 +0200 (2010-06-10)
changeset 373908781d80026fc
parent 37389 09467cdfa198
child 37391 476270a6c2dc
moved inductive_codegen to place where product type is available; tuned structure name
src/HOL/Inductive.thy
src/HOL/Library/SML_Quickcheck.thy
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_set.ML
     1.1 --- a/src/HOL/Inductive.thy	Thu Jun 10 12:24:01 2010 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Thu Jun 10 12:24:02 2010 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4  uses
     1.5    ("Tools/inductive.ML")
     1.6    "Tools/dseq.ML"
     1.7 -  ("Tools/inductive_codegen.ML")
     1.8    "Tools/Datatype/datatype_aux.ML"
     1.9    "Tools/Datatype/datatype_prop.ML"
    1.10    "Tools/Datatype/datatype_case.ML"
    1.11 @@ -286,9 +285,6 @@
    1.12  use "Tools/old_primrec.ML"
    1.13  use "Tools/primrec.ML"
    1.14  
    1.15 -use "Tools/inductive_codegen.ML"
    1.16 -setup InductiveCodegen.setup
    1.17 -
    1.18  text{* Lambda-abstractions with pattern matching: *}
    1.19  
    1.20  syntax
     2.1 --- a/src/HOL/Library/SML_Quickcheck.thy	Thu Jun 10 12:24:01 2010 +0200
     2.2 +++ b/src/HOL/Library/SML_Quickcheck.thy	Thu Jun 10 12:24:02 2010 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  begin
     2.5  
     2.6  setup {*
     2.7 -  InductiveCodegen.quickcheck_setup #>
     2.8 +  Inductive_Codegen.quickcheck_setup #>
     2.9    Quickcheck.add_generator ("SML", Codegen.test_term)
    2.10  *}
    2.11  
     3.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Jun 10 12:24:01 2010 +0200
     3.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jun 10 12:24:02 2010 +0200
     3.3 @@ -14,7 +14,7 @@
     3.4    val quickcheck_setup : theory -> theory
     3.5  end;
     3.6  
     3.7 -structure InductiveCodegen : INDUCTIVE_CODEGEN =
     3.8 +structure Inductive_Codegen : INDUCTIVE_CODEGEN =
     3.9  struct
    3.10  
    3.11  open Codegen;
    3.12 @@ -41,7 +41,7 @@
    3.13  );
    3.14  
    3.15  
    3.16 -fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
    3.17 +fun warn thm = warning ("Inductive_Codegen: Not a proper clause:\n" ^
    3.18    Display.string_of_thm_without_context thm);
    3.19  
    3.20  fun add_node x g = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
    3.21 @@ -324,7 +324,7 @@
    3.22    | distinct_v t nvs = (t, nvs);
    3.23  
    3.24  fun is_exhaustive (Var _) = true
    3.25 -  | is_exhaustive (Const ("Pair", _) $ t $ u) =
    3.26 +  | is_exhaustive (Const (@{const_name Pair}, _) $ t $ u) =
    3.27        is_exhaustive t andalso is_exhaustive u
    3.28    | is_exhaustive _ = false;
    3.29  
    3.30 @@ -569,7 +569,7 @@
    3.31  and mk_ind_def thy defs gr dep names module modecs intrs nparms =
    3.32    add_edge_acyclic (hd names, dep) gr handle
    3.33      Graph.CYCLES (xs :: _) =>
    3.34 -      error ("InductiveCodegen: illegal cyclic dependencies:\n" ^ commas xs)
    3.35 +      error ("Inductive_Codegen: illegal cyclic dependencies:\n" ^ commas xs)
    3.36    | Graph.UNDEF _ =>
    3.37      let
    3.38        val _ $ u = Logic.strip_imp_concl (hd intrs);
    3.39 @@ -825,7 +825,7 @@
    3.40      val s = "structure TestTerm =\nstruct\n\n" ^
    3.41        cat_lines (map snd code) ^
    3.42        "\nopen Generated;\n\n" ^ string_of
    3.43 -        (Pretty.block [str "val () = InductiveCodegen.test_fn :=",
    3.44 +        (Pretty.block [str "val () = Inductive_Codegen.test_fn :=",
    3.45            Pretty.brk 1, str "(fn p =>", Pretty.brk 1,
    3.46            str "case Seq.pull (testf p) of", Pretty.brk 1,
    3.47            str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"],
     4.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Jun 10 12:24:01 2010 +0200
     4.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Jun 10 12:24:02 2010 +0200
     4.3 @@ -401,7 +401,7 @@
     4.4        else thm
     4.5    in map preproc end;
     4.6  
     4.7 -fun code_ind_att optmod = to_pred_att [] #> InductiveCodegen.add optmod NONE;
     4.8 +fun code_ind_att optmod = to_pred_att [] #> Inductive_Codegen.add optmod NONE;
     4.9  
    4.10  
    4.11  (**** definition of inductive sets ****)