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