create data structure for storing (co)datatype information
authorblanchet
Mon Apr 29 17:37:00 2013 +0200 (2013-04-29)
changeset 5182338996458bc5c
parent 51819 9df935196be9
child 51824 27d073b0876c
create data structure for storing (co)datatype information
src/HOL/BNF/Tools/bnf_ctr_sugar.ML
src/HOL/BNF/Tools/bnf_def.ML
src/HOL/BNF/Tools/bnf_fp.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Apr 29 16:50:01 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Apr 29 17:37:00 2013 +0200
     1.3 @@ -18,6 +18,8 @@
     1.4       discIs: thm list,
     1.5       sel_thmss: thm list list};
     1.6  
     1.7 +  val morph_ctr_wrap_result: morphism -> ctr_wrap_result -> ctr_wrap_result
     1.8 +
     1.9    val rep_compat_prefix: string
    1.10  
    1.11    val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
    1.12 @@ -54,6 +56,18 @@
    1.13     discIs: thm list,
    1.14     sel_thmss: thm list list};
    1.15  
    1.16 +fun morph_ctr_wrap_result phi {discs, selss, exhaust, injects, distincts, case_thms, disc_thmss,
    1.17 +    discIs, sel_thmss} =
    1.18 +  {discs = map (Morphism.term phi) discs,
    1.19 +   selss = map (map (Morphism.term phi)) selss,
    1.20 +   exhaust = Morphism.thm phi exhaust,
    1.21 +   injects = map (Morphism.thm phi) injects,
    1.22 +   distincts = map (Morphism.thm phi) distincts,
    1.23 +   case_thms = map (Morphism.thm phi) case_thms,
    1.24 +   disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
    1.25 +   discIs = map (Morphism.thm phi) discIs,
    1.26 +   sel_thmss = map (map (Morphism.thm phi)) sel_thmss};
    1.27 +
    1.28  val rep_compat_prefix = "new";
    1.29  
    1.30  val isN = "is_";
     2.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Mon Apr 29 16:50:01 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Mon Apr 29 17:37:00 2013 +0200
     2.3 @@ -11,6 +11,8 @@
     2.4    type BNF
     2.5    type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
     2.6  
     2.7 +  val morph_bnf: morphism -> BNF -> BNF
     2.8 +  val eq_bnf: BNF * BNF -> bool
     2.9    val bnf_of: Proof.context -> string -> BNF option
    2.10    val register_bnf: string -> (BNF * local_theory) -> (BNF * local_theory)
    2.11  
     3.1 --- a/src/HOL/BNF/Tools/bnf_fp.ML	Mon Apr 29 16:50:01 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_fp.ML	Mon Apr 29 17:37:00 2013 +0200
     3.3 @@ -1,6 +1,7 @@
     3.4  (*  Title:      HOL/BNF/Tools/bnf_fp.ML
     3.5      Author:     Dmitriy Traytel, TU Muenchen
     3.6 -    Copyright   2012
     3.7 +    Author:     Jasmin Blanchette, TU Muenchen
     3.8 +    Copyright   2012, 2013
     3.9  
    3.10  Shared library for the datatype and codatatype constructions.
    3.11  *)
    3.12 @@ -24,6 +25,9 @@
    3.13       fold_thms: thm list,
    3.14       rec_thms: thm list}
    3.15  
    3.16 +  val morph_fp_result: morphism -> fp_result -> fp_result
    3.17 +  val eq_fp_result: fp_result * fp_result -> bool
    3.18 +
    3.19    val time: Timer.real_timer -> string -> Timer.real_timer
    3.20  
    3.21    val IITN: string
    3.22 @@ -184,6 +188,27 @@
    3.23     fold_thms: thm list,
    3.24     rec_thms: thm list};
    3.25  
    3.26 +fun morph_fp_result phi {bnfs, dtors, ctors, folds, recs, induct, strong_induct, dtor_ctors,
    3.27 +    ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, fold_thms, rec_thms} =
    3.28 +  {bnfs = map (morph_bnf phi) bnfs,
    3.29 +   dtors = map (Morphism.term phi) dtors,
    3.30 +   ctors = map (Morphism.term phi) ctors,
    3.31 +   folds = map (Morphism.term phi) folds,
    3.32 +   recs = map (Morphism.term phi) recs,
    3.33 +   induct = Morphism.thm phi induct,
    3.34 +   strong_induct = Morphism.thm phi strong_induct,
    3.35 +   dtor_ctors = map (Morphism.thm phi) dtor_ctors,
    3.36 +   ctor_dtors = map (Morphism.thm phi) ctor_dtors,
    3.37 +   ctor_injects = map (Morphism.thm phi) ctor_injects,
    3.38 +   map_thms = map (Morphism.thm phi) map_thms,
    3.39 +   set_thmss = map (map (Morphism.thm phi)) set_thmss,
    3.40 +   rel_thms = map (Morphism.thm phi) rel_thms,
    3.41 +   fold_thms = map (Morphism.thm phi) fold_thms,
    3.42 +   rec_thms = map (Morphism.thm phi) rec_thms};
    3.43 +
    3.44 +fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
    3.45 +  eq_list eq_bnf (bnfs1, bnfs2);
    3.46 +
    3.47  val timing = true;
    3.48  fun time timer msg = (if timing
    3.49    then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer))
     4.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 16:50:01 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 17:37:00 2013 +0200
     4.3 @@ -7,6 +7,13 @@
     4.4  
     4.5  signature BNF_FP_DEF_SUGAR =
     4.6  sig
     4.7 +  type fp =
     4.8 +    {fp_index: int,
     4.9 +     fp_res: BNF_FP.fp_result,
    4.10 +     ctr_wrap_res: BNF_Ctr_Sugar.ctr_wrap_result};
    4.11 +
    4.12 +  val fp_of: Proof.context -> string -> fp option
    4.13 +
    4.14    val derive_induct_fold_rec_thms_for_types: BNF_Def.BNF list -> thm -> thm list -> thm list ->
    4.15      BNF_Def.BNF list -> BNF_Def.BNF list -> typ list -> typ list -> typ list list list ->
    4.16      int list list -> int list -> term list list -> term list list -> term list list -> term list
    4.17 @@ -25,6 +32,7 @@
    4.18      * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
    4.19      * (thm list list * thm list list * Args.src list) *
    4.20      (thm list list * thm list list * Args.src list)
    4.21 +
    4.22    val datatypes: bool ->
    4.23      (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
    4.24        binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    4.25 @@ -51,6 +59,33 @@
    4.26  
    4.27  val EqN = "Eq_";
    4.28  
    4.29 +type fp =
    4.30 +  {fp_index: int,
    4.31 +   fp_res: fp_result,
    4.32 +   ctr_wrap_res: ctr_wrap_result};
    4.33 +
    4.34 +fun eq_fp ({fp_index = fp_index1, fp_res = fp_res1, ...} : fp,
    4.35 +    {fp_index = fp_index2, fp_res = fp_res2, ...} : fp) =
    4.36 +  fp_index1 = fp_index2 andalso eq_fp_result (fp_res1, fp_res2);
    4.37 +
    4.38 +fun morph_fp phi {fp_index, fp_res, ctr_wrap_res} =
    4.39 +  {fp_index = fp_index, fp_res = morph_fp_result phi fp_res,
    4.40 +   ctr_wrap_res = morph_ctr_wrap_result phi ctr_wrap_res};
    4.41 +
    4.42 +structure Data = Generic_Data
    4.43 +(
    4.44 +  type T = fp Symtab.table;
    4.45 +  val empty = Symtab.empty;
    4.46 +  val extend = I;
    4.47 +  val merge = Symtab.merge eq_fp;
    4.48 +);
    4.49 +
    4.50 +val fp_of = Symtab.lookup o Data.get o Context.Proof;
    4.51 +
    4.52 +fun register_fp key fp =
    4.53 +  Local_Theory.declaration {syntax = false, pervasive = true}
    4.54 +    (fn phi => Data.map (Symtab.update_new (key, morph_fp phi fp)));
    4.55 +
    4.56  (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)
    4.57  fun quasi_unambiguous_case_names names =
    4.58    let