1(*  Title:      HOL/Tools/Old_Datatype/old_datatype.ML
2    Author:     Stefan Berghofer, TU Muenchen
3
4Pieces left from the old datatype package.
5*)
6
7signature OLD_DATATYPE =
8sig
9  include OLD_DATATYPE_COMMON
10
11  val distinct_lemma: thm
12  type spec_cmd =
13    (binding * (string * string option) list * mixfix) * (binding * string list * mixfix) list
14  val read_specs: spec_cmd list -> theory -> spec list * Proof.context
15  val check_specs: spec list -> theory -> spec list * Proof.context
16end;
17
18structure Old_Datatype : OLD_DATATYPE =
19struct
20
21val distinct_lemma = @{lemma "f x \<noteq> f y ==> x \<noteq> y" by iprover};
22
23type spec_cmd =
24  (binding * (string * string option) list * mixfix) * (binding * string list * mixfix) list;
25
26fun parse_spec ctxt ((b, args, mx), constrs) =
27  ((b, map (apsnd (Typedecl.read_constraint ctxt)) args, mx),
28    constrs |> map (fn (c, Ts, mx') => (c, map (Syntax.parse_typ ctxt) Ts, mx')));
29
30fun check_specs ctxt (specs: Old_Datatype_Aux.spec list) =
31  let
32    fun prep_spec ((tname, args, mx), constrs) tys =
33      let
34        val (args', tys1) = chop (length args) tys;
35        val (constrs', tys3) = (constrs, tys1) |-> fold_map (fn (cname, cargs, mx') => fn tys2 =>
36          let val (cargs', tys3) = chop (length cargs) tys2;
37          in ((cname, cargs', mx'), tys3) end);
38      in (((tname, map dest_TFree args', mx), constrs'), tys3) end;
39
40    val all_tys =
41      specs |> maps (fn ((_, args, _), cs) => map TFree args @ maps #2 cs)
42      |> Syntax.check_typs ctxt;
43
44  in #1 (fold_map prep_spec specs all_tys) end;
45
46fun prep_specs parse raw_specs thy =
47  let
48    val ctxt = thy
49      |> Sign.add_types_global (map (fn ((b, args, mx), _) => (b, length args, mx)) raw_specs)
50      |> Proof_Context.init_global
51      |> fold (fn ((_, args, _), _) => fold (fn (a, _) =>
52          Variable.declare_typ (TFree (a, dummyS))) args) raw_specs;
53    val specs = check_specs ctxt (map (parse ctxt) raw_specs);
54  in (specs, ctxt) end;
55
56val read_specs = prep_specs parse_spec;
57val check_specs = prep_specs (K I);
58
59open Old_Datatype_Aux;
60
61end;
62