dropped code datatype certificates
authorhaftmann
Fri Mar 09 08:45:53 2007 +0100 (2007-03-09)
changeset 22423c1836b14c63a
parent 22422 ee19cdb07528
child 22424 8a5412121687
dropped code datatype certificates
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
src/HOL/Code_Generator.thy
src/HOL/Library/EfficientNat.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/typecopy_package.ML
src/Pure/Tools/class_package.ML
src/Pure/Tools/codegen_data.ML
src/Pure/Tools/codegen_package.ML
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Mar 09 08:45:50 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Mar 09 08:45:53 2007 +0100
     1.3 @@ -1187,8 +1187,8 @@
     1.4    @{index_ML CodegenData.add_preproc: "string * (theory -> thm list -> thm list)
     1.5      -> theory -> theory"} \\
     1.6    @{index_ML CodegenData.del_preproc: "string -> theory -> theory"} \\
     1.7 -  @{index_ML CodegenData.add_datatype: "string * (((string * sort) list * (string * typ list) list)
     1.8 -    * thm list Susp.T) -> theory -> theory"} \\
     1.9 +  @{index_ML CodegenData.add_datatype: "string * ((string * sort) list * (string * typ list) list)
    1.10 +    -> theory -> theory"} \\
    1.11    @{index_ML CodegenData.del_datatype: "string -> theory -> theory"} \\
    1.12    @{index_ML CodegenData.get_datatype: "theory -> string
    1.13      -> ((string * sort) list * (string * typ list) list) option"} \\
    1.14 @@ -1232,14 +1232,12 @@
    1.15    \item @{ML CodegenData.del_preproc}~@{text "name"}~@{text "thy"} removes
    1.16       generic preprcoessor named @{text name} from executable content.
    1.17  
    1.18 -  \item @{ML CodegenData.add_datatype}~@{text "(name, (spec, cert))"}~@{text "thy"} adds
    1.19 +  \item @{ML CodegenData.add_datatype}~@{text "(name, spec)"}~@{text "thy"} adds
    1.20       a datatype to executable content, with type constructor
    1.21       @{text name} and specification @{text spec}; @{text spec} is
    1.22       a pair consisting of a list of type variable with sort
    1.23       constraints and a list of constructors with name
    1.24 -     and types of arguments.  The addition as datatype
    1.25 -     has to be justified giving a certificate of suspended
    1.26 -     theorems as witnesses for injectiveness and distinctness.
    1.27 +     and types of arguments.
    1.28  
    1.29    \item @{ML CodegenData.del_datatype}~@{text "name"}~@{text "thy"}
    1.30       remove a datatype from executable content, if present.
     2.1 --- a/src/HOL/Code_Generator.thy	Fri Mar 09 08:45:50 2007 +0100
     2.2 +++ b/src/HOL/Code_Generator.thy	Fri Mar 09 08:45:53 2007 +0100
     2.3 @@ -87,7 +87,9 @@
     2.4    (Haskell infixl 4 "==")
     2.5  
     2.6  
     2.7 -text {* boolean expressions *}
     2.8 +text {* type bool *}
     2.9 +
    2.10 +code_datatype True False
    2.11  
    2.12  lemma [code func]:
    2.13    shows "(False \<and> x) = False"
    2.14 @@ -152,18 +154,22 @@
    2.15    bool true false not
    2.16  
    2.17  
    2.18 -text {* itself as a code generator datatype *}
    2.19 +text {* type prop *}
    2.20 +
    2.21 +code_datatype Trueprop "prop"
    2.22 +
    2.23 +
    2.24 +text {* type itself *}
    2.25  
    2.26 -setup {*
    2.27 -  let
    2.28 -    val v = ("'a", []);
    2.29 -    val t = Logic.mk_type (TFree v);
    2.30 -    val Const (c, ty) = t;
    2.31 -    val (_, Type (dtco, _)) = strip_type ty;
    2.32 -  in
    2.33 -    CodegenData.add_datatype (dtco, (([v], [(c, [])]), CodegenData.lazy (fn () => [])))
    2.34 -  end
    2.35 -*} 
    2.36 +code_datatype "TYPE('a)"
    2.37 +
    2.38 +
    2.39 +text {* prevent unfolding of quantifier definitions *}
    2.40 +
    2.41 +lemma [code func]:
    2.42 +  "Ex = Ex"
    2.43 +  "All = All"
    2.44 +  by rule+
    2.45  
    2.46  
    2.47  text {* code generation for arbitrary as exception *}
     3.1 --- a/src/HOL/Library/EfficientNat.thy	Fri Mar 09 08:45:50 2007 +0100
     3.2 +++ b/src/HOL/Library/EfficientNat.thy	Fri Mar 09 08:45:53 2007 +0100
     3.3 @@ -159,7 +159,7 @@
     3.4    (Haskell "!((_) + 1)")
     3.5  
     3.6  setup {*
     3.7 -  CodegenData.del_datatype "nat"
     3.8 +  CodegenData.add_datatype ("nat", ([], []))
     3.9  *}
    3.10  
    3.11  types_code
     4.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Mar 09 08:45:50 2007 +0100
     4.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Mar 09 08:45:53 2007 +0100
     4.3 @@ -9,8 +9,6 @@
     4.4  sig
     4.5    val get_eq: theory -> string -> thm list
     4.6    val get_eq_datatype: theory -> string -> thm list
     4.7 -  val get_cert: theory -> bool * string -> thm list
     4.8 -  val get_cert_datatype: theory -> string -> thm list
     4.9    val dest_case_expr: theory -> term
    4.10      -> ((string * typ) list * ((term * typ) * (term * term) list)) option
    4.11    val add_datatype_case_const: string -> theory -> theory
    4.12 @@ -28,7 +26,7 @@
    4.13      -> (string * (arity * term list)) list option
    4.14    val prove_codetypes_arities: tactic -> (string * bool) list -> sort
    4.15      -> (arity list -> (string * term list) list -> theory
    4.16 -    -> ((bstring * Attrib.src list) * term) list * theory)
    4.17 +      -> ((bstring * Attrib.src list) * term) list * theory)
    4.18      -> (arity list -> (string * term list) list -> theory -> theory)
    4.19      -> theory -> theory
    4.20  
    4.21 @@ -379,35 +377,6 @@
    4.22    in map mk_dist (sym_product cos) end;
    4.23  
    4.24  local
    4.25 -  val bool_eq_implies = iffD1;
    4.26 -  val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
    4.27 -  val rew_conj = thm "HOL.atomize_conj" |> Thm.symmetric;
    4.28 -  val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
    4.29 -  val not_eq_quodlibet = thm "not_eq_quodlibet";
    4.30 -in
    4.31 -
    4.32 -fun get_cert_datatype thy dtco =
    4.33 -  let
    4.34 -    val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
    4.35 -    val inject = (#inject o DatatypePackage.the_datatype thy) dtco
    4.36 -      |> map (fn thm => bool_eq_implies OF [thm] )
    4.37 -      |> map (MetaSimplifier.rewrite_rule [rew_eq, rew_conj]);
    4.38 -    val ctxt = ProofContext.init thy;
    4.39 -    val simpset = Simplifier.context ctxt
    4.40 -      (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]);
    4.41 -    val cos = map (fn (co, tys) =>
    4.42 -        (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
    4.43 -    val tac = ALLGOALS (simp_tac simpset)
    4.44 -      THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
    4.45 -    val distinct =
    4.46 -      mk_distinct cos
    4.47 -      |> map (fn t => Goal.prove_global thy [] [] t (K tac))
    4.48 -      |> map (fn thm => not_eq_quodlibet OF [thm])
    4.49 -  in inject @ distinct end
    4.50 -
    4.51 -end;
    4.52 -
    4.53 -local
    4.54    val not_sym = thm "HOL.not_sym";
    4.55    val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
    4.56    val refl = thm "refl";
    4.57 @@ -496,9 +465,6 @@
    4.58    | get_spec thy (tyco, false) =
    4.59        TypecopyPackage.get_spec thy tyco;
    4.60  
    4.61 -fun get_cert thy (true, dtco) = get_cert_datatype thy dtco
    4.62 -  | get_cert thy (false, dtco) = [TypecopyPackage.get_cert thy dtco];
    4.63 -
    4.64  local
    4.65    fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
    4.66     of SOME _ => get_eq_datatype thy tyco
    4.67 @@ -559,20 +525,20 @@
    4.68  
    4.69  (* registering code types in code generator *)
    4.70  
    4.71 -fun codetype_hook specs =
    4.72 -  let
    4.73 -    fun add (dtco, (flag, spec)) thy =
    4.74 -      let
    4.75 -        fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco));
    4.76 -      in
    4.77 -        CodegenData.add_datatype
    4.78 -          (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy
    4.79 -      end;
    4.80 -  in fold add specs end;
    4.81 +val codetype_hook =
    4.82 +  fold (fn (dtco, (_, spec)) => CodegenData.add_datatype (dtco, spec));
    4.83  
    4.84  
    4.85  (* instrumentalizing the sort algebra *)
    4.86  
    4.87 +(*fun assume_arities_of_sort thy arities ty_sort =
    4.88 +  let
    4.89 +    val pp = Sign.pp thy;
    4.90 +    val algebra = Sign.classes_of thy
    4.91 +      |> fold (fn (tyco, asorts, sort) =>
    4.92 +           Sorts.add_arities pp (tyco, map (fn class => (class, asorts)) sort)) arities;
    4.93 +  in Sorts.of_sort algebra ty_sort end;
    4.94 +
    4.95  fun get_codetypes_arities thy tycos sort =
    4.96    let
    4.97      val algebra = Sign.classes_of thy;
    4.98 @@ -588,7 +554,7 @@
    4.99      fun typ_of_sort ty =
   4.100        let
   4.101          val arities = map (fn (tyco, _) => (tyco, map snd vs, sort)) css;
   4.102 -      in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end;
   4.103 +      in assume_arities_of_sort thy arities (ty, sort) end;
   4.104      fun mk_cons tyco (c, tys) =
   4.105        let
   4.106          val ts = Name.names Name.context "a" tys;
   4.107 @@ -598,7 +564,34 @@
   4.108      then SOME (
   4.109        map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css
   4.110      ) else NONE
   4.111 -  end;
   4.112 +  end;*)
   4.113 +
   4.114 +fun get_codetypes_arities thy tycos sort =
   4.115 +  let
   4.116 +    val pp = Sign.pp thy;
   4.117 +    val algebra = Sign.classes_of thy;
   4.118 +    val (vs_proto, css_proto) = the_codetypes_mut_specs thy tycos;
   4.119 +    val vs = map (fn (v, vsort) => (v, Sorts.inter_sort algebra (vsort, sort))) vs_proto;
   4.120 +    val css = map (fn (tyco, (_, cs)) => (tyco, cs)) css_proto;
   4.121 +    val algebra' = algebra
   4.122 +      |> fold (fn (tyco, _) =>
   4.123 +           Sorts.add_arities pp (tyco, map (fn class => (class, map snd vs)) sort)) css;
   4.124 +    fun typ_sort_inst ty = CodegenConsts.typ_sort_inst algebra' (Logic.varifyT ty, sort);
   4.125 +    val venv = Vartab.empty
   4.126 +      |> fold (fn (v, sort) => Vartab.update_new ((v, 0), sort)) vs
   4.127 +      |> fold (fn (_, cs) => fold (fn (_, tys) => fold typ_sort_inst tys) cs) css;
   4.128 +    fun inst (v, _) = (v, (the o Vartab.lookup venv) (v, 0));
   4.129 +    val vs' = map inst vs;
   4.130 +    fun mk_arity tyco = (tyco, map snd vs', sort);
   4.131 +    fun mk_cons tyco (c, tys) =
   4.132 +      let
   4.133 +        val tys' = (map o Term.map_type_tfree) (TFree o inst) tys;
   4.134 +        val ts = Name.names Name.context "a" tys';
   4.135 +        val ty = (tys' ---> Type (tyco, map TFree vs'));
   4.136 +      in list_comb (Const (c, ty), map Free ts) end;
   4.137 +  in
   4.138 +    map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css |> SOME
   4.139 +  end handle Class_Error => NONE;
   4.140  
   4.141  fun prove_codetypes_arities tac tycos sort f after_qed thy =
   4.142    case get_codetypes_arities thy tycos sort
     5.1 --- a/src/HOL/Tools/typecopy_package.ML	Fri Mar 09 08:45:50 2007 +0100
     5.2 +++ b/src/HOL/Tools/typecopy_package.ML	Fri Mar 09 08:45:53 2007 +0100
     5.3 @@ -22,7 +22,6 @@
     5.4    type hook = string * info -> theory -> theory
     5.5    val add_hook: hook -> theory -> theory
     5.6    val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
     5.7 -  val get_cert: theory -> string -> thm
     5.8    val get_eq: theory -> string -> thm
     5.9    val print: theory -> unit
    5.10    val setup: theory -> theory
    5.11 @@ -132,26 +131,16 @@
    5.12  end; (*local*)
    5.13  
    5.14  
    5.15 -(* equality function equation *)
    5.16 +(* equality function equation and datatype specification *)
    5.17  
    5.18  fun get_eq thy tyco =
    5.19    (#inject o the o get_typecopy_info thy) tyco;
    5.20  
    5.21 -
    5.22 -(* datatype specification and certificate *)
    5.23 -
    5.24  fun get_spec thy tyco =
    5.25    let
    5.26      val SOME { vs, constr, typ, ... } = get_typecopy_info thy tyco
    5.27    in (vs, [(constr, [typ])]) end;
    5.28  
    5.29 -local
    5.30 -  val bool_eq_implies = iffD1;
    5.31 -  val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
    5.32 -in fun get_cert thy tyco =
    5.33 -  MetaSimplifier.rewrite_rule [rew_eq] (bool_eq_implies OF [get_eq thy tyco])
    5.34 -end; (*local*)
    5.35 -
    5.36  
    5.37  (* hook for projection function code *)
    5.38  
     6.1 --- a/src/Pure/Tools/class_package.ML	Fri Mar 09 08:45:50 2007 +0100
     6.2 +++ b/src/Pure/Tools/class_package.ML	Fri Mar 09 08:45:53 2007 +0100
     6.3 @@ -27,8 +27,6 @@
     6.4    val instance_sort_cmd: string * string -> theory -> Proof.state
     6.5    val prove_instance_sort: tactic -> class * sort -> theory -> theory
     6.6  
     6.7 -  val assume_arities_of_sort: theory -> arity list -> typ * sort -> bool
     6.8 -
     6.9    (* experimental class target *)
    6.10    val class_of_locale: theory -> string -> class option
    6.11    val add_def_in_class: local_theory -> string
    6.12 @@ -105,17 +103,6 @@
    6.13    end;
    6.14  
    6.15  
    6.16 -(* contexts with arity assumptions *)
    6.17 -
    6.18 -fun assume_arities_of_sort thy arities ty_sort =
    6.19 -  let
    6.20 -    val pp = Sign.pp thy;
    6.21 -    val algebra = Sign.classes_of thy
    6.22 -      |> fold (fn (tyco, asorts, sort) =>
    6.23 -           Sorts.add_arities pp (tyco, map (fn class => (class, asorts)) sort)) arities;
    6.24 -  in Sorts.of_sort algebra ty_sort end;
    6.25 -
    6.26 -
    6.27  (* instances with implicit parameter handling *)
    6.28  
    6.29  local
    6.30 @@ -141,7 +128,7 @@
    6.31      val _ = case (duplicates (op =) o map #1) arities
    6.32       of [] => ()
    6.33        | dupl_tycos => error ("type constructors occur more than once in arities: "
    6.34 -        ^ (commas o map quote) dupl_tycos);
    6.35 +          ^ (commas o map quote) dupl_tycos);
    6.36      val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory
    6.37      fun get_consts_class tyco ty class =
    6.38        let
    6.39 @@ -179,7 +166,6 @@
    6.40        in fold_map read defs cs end;
    6.41      val (defs, _) = read_defs raw_defs cs
    6.42        (fold Sign.primitive_arity arities (Theory.copy theory));
    6.43 -
    6.44      fun get_remove_contraint c thy =
    6.45        let
    6.46          val ty = Sign.the_const_constraint thy c;
    6.47 @@ -334,7 +320,6 @@
    6.48  
    6.49  
    6.50  (* exporting terms and theorems to global toplevel *)
    6.51 -(*FIXME should also be used when introducing classes*)
    6.52  
    6.53  fun globalize thy classes =
    6.54    let
    6.55 @@ -380,6 +365,7 @@
    6.56    ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
    6.57      "apply some intro/elim rule")]);
    6.58  
    6.59 +
    6.60  (* tactical interfaces to locale commands *)
    6.61  
    6.62  fun prove_interpretation tac prfx_atts expr insts thy =
    6.63 @@ -431,13 +417,6 @@
    6.64  
    6.65  local
    6.66  
    6.67 -fun add_axclass (name, supsort) params axs thy =
    6.68 -  let
    6.69 -    val (c, thy') = thy
    6.70 -      |> AxClass.define_class_i (name, supsort) params axs;
    6.71 -    val {intro, axioms, ...} = AxClass.get_definition thy' c;
    6.72 -  in ((c, (intro, axioms)), thy') end;
    6.73 -
    6.74  fun certify_class thy class =
    6.75    tap (the_class_data thy) (Sign.certify_class thy class);
    6.76  
    6.77 @@ -454,27 +433,28 @@
    6.78      (*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I,
    6.79        typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*)
    6.80      val other_consts = map (prep_param thy) raw_other_consts;
    6.81 -    val elems = fold_rev (fn Locale.Elem e => cons e | _ => I)
    6.82 -      raw_elems []; (*FIXME make include possible here?*)
    6.83 +    val (elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
    6.84 +      | Locale.Expr i => apsnd (cons i)) raw_elems ([], []);
    6.85      val supclasses = map (prep_class thy) raw_supclasses;
    6.86      val supsort =
    6.87        supclasses
    6.88        |> Sign.certify_sort thy
    6.89 -      |> (fn [] => Sign.defaultS thy | S => S);    (*FIXME Why syntax defaultS?*)
    6.90 -    val supexpr = Locale.Merge
    6.91 -      (map (Locale.Locale o #locale o the_class_data thy) supclasses);
    6.92 -    val supparams = (map fst o Locale.parameters_of_expr thy) supexpr;
    6.93 +      |> (fn [] => Sign.defaultS thy | S => S); (*FIXME Why syntax defaultS?*)
    6.94 +    val suplocales = map (Locale.Locale o #locale o the_class_data thy) supclasses;
    6.95 +    val supexpr = Locale.Merge (suplocales @ includes);
    6.96 +    val supparams = (map fst o Locale.parameters_of_expr thy)
    6.97 +      (Locale.Merge suplocales);
    6.98      val supconsts = AList.make
    6.99        (the o AList.lookup (op =) (param_map thy supclasses)) (map fst supparams);
   6.100 -      (*FIXME include proper*)
   6.101      (*val elems_constrains = map
   6.102        (Element.Constrains o apsnd (Term.map_type_tfree subst_classtyvar)) supparams;*)
   6.103      fun extract_params thy name_locale =
   6.104 -      let
   6.105 +      let   
   6.106          val params = Locale.parameters_of thy name_locale;
   6.107        in
   6.108          (map (fst o fst) params, params
   6.109 -        |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, Sign.defaultS thy)))
   6.110 +        |> (map o apfst o apsnd o Term.map_type_tfree)
   6.111 +             (K (TFree (AxClass.param_tyvarname, Sign.defaultS thy)))
   6.112          |> (map o apsnd) (fork_mixfix true NONE #> fst)
   6.113          |> chop (length supconsts)
   6.114          |> snd)
   6.115 @@ -486,8 +466,8 @@
   6.116                Const ((fst o the o AList.lookup (op =) consts) c, ty)
   6.117            | subst t = t;
   6.118          fun prep_asm ((name, atts), ts) =
   6.119 -          (*FIXME: name handling?*)
   6.120 -          ((NameSpace.base name, map (Attrib.attribute thy) atts), (map o map_aterms) subst ts);
   6.121 +          ((NameSpace.base name, map (Attrib.attribute thy) atts),
   6.122 +            (map o map_aterms) subst ts);
   6.123        in
   6.124          Locale.global_asms_of thy name_locale
   6.125          |> map prep_asm
   6.126 @@ -578,17 +558,24 @@
   6.127  
   6.128  fun add_def_in_class lthy class ((c, syn), ((name, atts), (rhs, eq))) thy =
   6.129    let
   6.130 +    val prfx = (Logic.const_of_class o NameSpace.base) class;
   6.131      val rhs' = global_term thy [class] rhs;
   6.132      val (syn', _) = fork_mixfix true NONE syn;
   6.133      val ty = Term.fastype_of rhs';
   6.134 +    fun mk_name thy c =
   6.135 +      let
   6.136 +        val n1 = Sign.full_name thy c;
   6.137 +        val n2 = NameSpace.qualifier n1;
   6.138 +        val n3 = NameSpace.base n1;
   6.139 +      in NameSpace.implode [n2, prfx, n3] end;
   6.140      fun add_const (c, ty, syn) =
   6.141        Sign.add_consts_authentic [(c, ty, syn)]
   6.142 -      #> pair (Sign.full_name thy c, ty);
   6.143 +      #> pair (mk_name thy c, ty);
   6.144      fun add_def ((name, atts), prop) thy =
   6.145        thy
   6.146        |> PureThy.add_defs_i false [((name, prop), map (Attrib.attribute thy) atts)]
   6.147        |>> the_single;
   6.148 -    (*val _ = Output.info "------ DEF ------";
   6.149 +    val _ = Output.info "------ DEF ------";
   6.150      val _ = Output.info c;
   6.151      val _ = Output.info name;
   6.152      val _ = (Output.info o Sign.string_of_term thy) rhs';
   6.153 @@ -603,12 +590,14 @@
   6.154      val _ = map print_witness witness;
   6.155      val _ = (Output.info o string_of_thm) eq';
   6.156      val eq'' = Element.satisfy_thm witness eq';
   6.157 -    val _ = (Output.info o string_of_thm) eq'';*)
   6.158 +    val _ = (Output.info o string_of_thm) eq'';
   6.159    in
   6.160      thy
   6.161 -    (*|> add_const (c, ty, syn')
   6.162 +    |> Sign.add_path prfx
   6.163 +    |> add_const (c, ty, syn')
   6.164      |-> (fn c => add_def ((name, atts), Logic.mk_equals (Const c, rhs')))
   6.165 -    |-> (fn global_def_thm => tap (fn _ => (Output.info o string_of_thm) global_def_thm))*)
   6.166 +    |-> (fn global_def_thm => tap (fn _ => (Output.info o string_of_thm) global_def_thm))
   6.167 +    |> Sign.restore_naming thy
   6.168    end;
   6.169  
   6.170  end;
     7.1 --- a/src/Pure/Tools/codegen_data.ML	Fri Mar 09 08:45:50 2007 +0100
     7.2 +++ b/src/Pure/Tools/codegen_data.ML	Fri Mar 09 08:45:53 2007 +0100
     7.3 @@ -15,9 +15,8 @@
     7.4    val add_func_legacy: thm -> theory -> theory
     7.5    val del_func: thm -> theory -> theory
     7.6    val add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory
     7.7 -  val add_datatype: string * (((string * sort) list * (string * typ list) list) * thm list Susp.T)
     7.8 +  val add_datatype: string * ((string * sort) list * (string * typ list) list)
     7.9      -> theory -> theory
    7.10 -  val del_datatype: string -> theory -> theory
    7.11    val add_inline: thm -> theory -> theory
    7.12    val del_inline: thm -> theory -> theory
    7.13    val add_inline_proc: string * (theory -> cterm list -> thm list) -> theory -> theory
    7.14 @@ -28,8 +27,7 @@
    7.15    val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
    7.16    val these_funcs: theory -> CodegenConsts.const -> thm list
    7.17    val tap_typ: theory -> CodegenConsts.const -> typ option
    7.18 -  val get_datatype: theory -> string
    7.19 -    -> ((string * sort) list * (string * typ list) list) option
    7.20 +  val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
    7.21    val get_datatype_of_constr: theory -> CodegenConsts.const -> string option
    7.22  
    7.23    val preprocess_cterm: cterm -> thm
    7.24 @@ -193,7 +191,7 @@
    7.25      in (SOME consts, thms) end;
    7.26  
    7.27  val eq_string = op = : string * string -> bool;
    7.28 -fun eq_dtyp (((vs1, cs1), _), ((vs2, cs2), _)) = 
    7.29 +fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = 
    7.30    gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2)
    7.31      andalso gen_eq_set (eq_pair eq_string (eq_list (is_equal o Term.typ_ord))) (cs1, cs2);
    7.32  fun merge_dtyps (tabs as (tab1, tab2)) =
    7.33 @@ -210,7 +208,7 @@
    7.34  datatype spec = Spec of {
    7.35    funcs: sdthms Consttab.table,
    7.36    dconstrs: string Consttab.table,
    7.37 -  dtyps: (((string * sort) list * (string * typ list) list) * thm list Susp.T) Symtab.table
    7.38 +  dtyps: ((string * sort) list * (string * typ list) list) Symtab.table
    7.39  };
    7.40  
    7.41  fun mk_spec ((funcs, dconstrs), dtyps) =
    7.42 @@ -328,15 +326,17 @@
    7.43          (Pretty.block o Pretty.fbreaks) (
    7.44            Pretty.str s :: pretty_sdthms ctxt lthms
    7.45          );
    7.46 -      fun pretty_dtyp (s, cos) =
    7.47 -        (Pretty.block o Pretty.breaks) (
    7.48 -          Pretty.str s
    7.49 -          :: Pretty.str "="
    7.50 -          :: Pretty.separate "|" (map (fn (c, []) => Pretty.str c
    7.51 -               | (c, tys) =>
    7.52 -                   (Pretty.block o Pretty.breaks)
    7.53 -                      (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
    7.54 -        )
    7.55 +      fun pretty_dtyp (s, []) =
    7.56 +            Pretty.str s
    7.57 +        | pretty_dtyp (s, cos) =
    7.58 +            (Pretty.block o Pretty.breaks) (
    7.59 +              Pretty.str s
    7.60 +              :: Pretty.str "="
    7.61 +              :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
    7.62 +                   | (c, tys) =>
    7.63 +                       (Pretty.block o Pretty.breaks)
    7.64 +                          (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos)
    7.65 +            );
    7.66        val inlines = (#inlines o the_preproc) exec;
    7.67        val inline_procs = (map fst o #inline_procs o the_preproc) exec;
    7.68        val preprocs = (map fst o #preprocs o the_preproc) exec;
    7.69 @@ -346,13 +346,14 @@
    7.70          |> sort (string_ord o pairself fst);
    7.71        val dtyps = the_dtyps exec
    7.72          |> Symtab.dest
    7.73 -        |> map (fn (dtco, ((vs, cos), _)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos))
    7.74 +        |> map (fn (dtco, (vs, cos)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos))
    7.75          |> sort (string_ord o pairself fst)
    7.76      in
    7.77        (Pretty.writeln o Pretty.chunks) [
    7.78          Pretty.block (
    7.79            Pretty.str "defining equations:"
    7.80 -          :: map pretty_func funs
    7.81 +          :: Pretty.fbrk
    7.82 +          :: (Pretty.fbreaks o map pretty_func) funs
    7.83          ),
    7.84          Pretty.block (
    7.85            Pretty.str "inlining theorems:"
    7.86 @@ -431,77 +432,6 @@
    7.87          ^ CodegenConsts.string_of_const thy c ^ "\n" ^ string_of_thm thm)
    7.88    in map cert c_thms end;
    7.89  
    7.90 -fun mk_cos tyco vs cos =
    7.91 -  let
    7.92 -    val dty = Type (tyco, map TFree vs);
    7.93 -    fun mk_co (co, tys) = (Const (co, (tys ---> dty)), map I tys);
    7.94 -  in map mk_co cos end;
    7.95 -
    7.96 -fun mk_co_args (co, tys) ctxt =
    7.97 -  let
    7.98 -    val names = Name.invents ctxt "a" (length tys);
    7.99 -    val ctxt' = fold Name.declare names ctxt;
   7.100 -    val vs = map2 (fn v => fn ty => Free (fst (v, 0), I ty)) names tys;
   7.101 -  in (vs, ctxt') end;
   7.102 -
   7.103 -fun check_freeness thy cos thms =
   7.104 -  let
   7.105 -    val props = AList.make Drule.plain_prop_of thms;
   7.106 -    fun sym_product [] = []
   7.107 -      | sym_product (x::xs) = map (pair x) xs @ sym_product xs;
   7.108 -    val quodlibet =
   7.109 -      let
   7.110 -        val judg = ObjectLogic.fixed_judgment (the_context ()) "x";
   7.111 -        val [free] = fold_aterms (fn v as Free _ => cons v | _ => I) judg [];
   7.112 -        val judg' = Term.subst_free [(free, Bound 0)] judg;
   7.113 -        val prop = Type ("prop", []);
   7.114 -        val prop' = fastype_of judg';
   7.115 -      in
   7.116 -        Const ("all", (prop' --> prop) --> prop) $ Abs ("P", prop', judg')
   7.117 -      end;
   7.118 -    fun check_inj (co, []) =
   7.119 -          NONE
   7.120 -      | check_inj (co, tys) =
   7.121 -          let
   7.122 -            val ((xs, ys), _) = Name.context
   7.123 -              |> mk_co_args (co, tys)
   7.124 -              ||>> mk_co_args (co, tys);
   7.125 -            val prem = Logic.mk_equals
   7.126 -              (list_comb (co, xs), list_comb (co, ys));
   7.127 -            val concl = Logic.mk_conjunction_list
   7.128 -              (map2 (curry Logic.mk_equals) xs ys);
   7.129 -            val t = Logic.mk_implies (prem, concl);
   7.130 -          in case find_first (curry Term.could_unify t o snd) props
   7.131 -           of SOME (thm, _) => SOME thm
   7.132 -            | NONE => error ("Could not prove injectiveness statement\n"
   7.133 -               ^ Sign.string_of_term thy t
   7.134 -               ^ "\nfor constructor "
   7.135 -               ^ CodegenConsts.string_of_const_typ thy (dest_Const co)
   7.136 -               ^ "\nwith theorems\n" ^ cat_lines (map string_of_thm thms))
   7.137 -          end;
   7.138 -    fun check_dist ((co1, tys1), (co2, tys2)) =
   7.139 -          let
   7.140 -            val ((xs1, xs2), _) = Name.context
   7.141 -              |> mk_co_args (co1, tys1)
   7.142 -              ||>> mk_co_args (co2, tys2);
   7.143 -            val prem = Logic.mk_equals
   7.144 -              (list_comb (co1, xs1), list_comb (co2, xs2));
   7.145 -            val t = Logic.mk_implies (prem, quodlibet);
   7.146 -          in case find_first (curry Term.could_unify t o snd) props
   7.147 -           of SOME (thm, _) => thm
   7.148 -            | NONE => error ("Could not prove distinctness statement\n"
   7.149 -               ^ Sign.string_of_term thy t
   7.150 -               ^ "\nfor constructors "
   7.151 -               ^ CodegenConsts.string_of_const_typ thy (dest_Const co1)
   7.152 -               ^ " and "
   7.153 -               ^ CodegenConsts.string_of_const_typ thy (dest_Const co2)
   7.154 -               ^ "\nwith theorems\n" ^ cat_lines (map string_of_thm thms))
   7.155 -          end;
   7.156 -  in (map_filter check_inj cos, map check_dist (sym_product cos)) end;
   7.157 -
   7.158 -fun certify_datatype thy dtco cs thms =
   7.159 -  (op @) (check_freeness thy cs thms);
   7.160 -
   7.161  
   7.162  
   7.163  (** operational sort algebra and class discipline **)
   7.164 @@ -684,37 +614,102 @@
   7.165        (add_lthms lthms'))) thy
   7.166    end;
   7.167  
   7.168 -fun add_datatype (tyco, (vs_cos as (vs, cos), lthms)) thy =
   7.169 +local
   7.170 +
   7.171 +fun consts_of_cos thy tyco vs cos =
   7.172 +  let
   7.173 +    val dty = Type (tyco, map TFree vs);
   7.174 +    fun mk_co (co, tys) = CodegenConsts.norm_of_typ thy (co, tys ---> dty);
   7.175 +  in map mk_co cos end;
   7.176 +
   7.177 +fun co_of_const thy (c, ty) =
   7.178    let
   7.179 -    val cs = mk_cos tyco vs cos;
   7.180 -    val consts = map (CodegenConsts.norm_of_typ thy o dest_Const o fst) cs;
   7.181 -    val add =
   7.182 -      map_dtyps (Symtab.update_new (tyco,
   7.183 -        (vs_cos, certificate thy (fn thy => certify_datatype thy tyco cs) lthms)))
   7.184 -      #> map_dconstrs (fold (fn c => Consttab.update (c, tyco)) consts)
   7.185 -  in map_exec_purge (SOME consts) add thy end;
   7.186 +    fun err () = error
   7.187 +     ("Illegal type for datatype constructor: " ^ Sign.string_of_typ thy ty);
   7.188 +    val (tys, ty') = strip_type ty;
   7.189 +    val (tyco, vs) = ((apsnd o map) dest_TFree o dest_Type) ty'
   7.190 +      handle TYPE _ => err ();
   7.191 +    val sorts = if has_duplicates (eq_fst op =) vs then err ()
   7.192 +      else map snd vs;
   7.193 +    val vs_names = Name.invent_list [] "'a" (length vs);
   7.194 +    val vs_map = map fst vs ~~ vs_names;
   7.195 +    val vs' = vs_names ~~ sorts;
   7.196 +    val tys' = (map o map_type_tfree) (fn (v, sort) =>
   7.197 +      (TFree ((the o AList.lookup (op =) vs_map) v, sort))) tys
   7.198 +      handle Option => err ();
   7.199 +  in (tyco, (vs', (c, tys'))) end;
   7.200  
   7.201  fun del_datatype tyco thy =
   7.202 +  case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
   7.203 +   of SOME (vs, cos) => let
   7.204 +        val consts = consts_of_cos thy tyco vs cos;
   7.205 +        val del =
   7.206 +          map_dtyps (Symtab.delete tyco)
   7.207 +          #> map_dconstrs (fold Consttab.delete consts)
   7.208 +      in map_exec_purge (SOME consts) del thy end
   7.209 +    | NONE => thy;
   7.210 +
   7.211 +(*FIXME integrate this auxiliary properly*)
   7.212 +
   7.213 +in
   7.214 +
   7.215 +fun add_datatype (tyco, (vs_cos as (vs, cos))) thy =
   7.216    let
   7.217 -    val SOME ((vs, cos), _) = Symtab.lookup ((the_dtyps o get_exec) thy) tyco;
   7.218 -    val cs = mk_cos tyco vs cos;
   7.219 -    val consts = map (CodegenConsts.norm_of_typ thy o dest_Const o fst) cs;
   7.220 -    val del =
   7.221 -      map_dtyps (Symtab.delete tyco)
   7.222 -      #> map_dconstrs (fold Consttab.delete consts)
   7.223 -  in map_exec_purge (SOME consts) del thy end;
   7.224 +    val consts = consts_of_cos thy tyco vs cos;
   7.225 +    val add =
   7.226 +      map_dtyps (Symtab.update_new (tyco, vs_cos))
   7.227 +      #> map_dconstrs (fold (fn c => Consttab.update (c, tyco)) consts)
   7.228 +  in
   7.229 +    thy
   7.230 +    |> del_datatype tyco
   7.231 +    |> map_exec_purge (SOME consts) add
   7.232 +  end;
   7.233 +
   7.234 +fun add_datatype_consts cs thy =
   7.235 +  let
   7.236 +    val raw_cos = map (co_of_const thy) cs;
   7.237 +    val (tyco, (vs_names, sorts_cos)) = if (length o distinct (eq_fst op =)) raw_cos = 1
   7.238 +      then ((fst o hd) raw_cos, ((map fst o fst o snd o hd) raw_cos,
   7.239 +        map ((apfst o map) snd o snd) raw_cos))
   7.240 +      else error ("Term constructors not referring to the same type: "
   7.241 +        ^ commas (map (CodegenConsts.string_of_const_typ thy) cs));
   7.242 +    val sorts = foldr1 ((uncurry o map2 o curry o Sorts.inter_sort) (Sign.classes_of thy))
   7.243 +      (map fst sorts_cos);
   7.244 +    val cos = map snd sorts_cos;
   7.245 +    val vs = vs_names ~~ sorts;
   7.246 +  in
   7.247 +    thy
   7.248 +    |> add_datatype (tyco, (vs, cos))
   7.249 +  end;
   7.250 +
   7.251 +fun add_datatype_consts_cmd raw_cs thy =
   7.252 +  let
   7.253 +    val cs = map (apsnd Logic.unvarifyT o CodegenConsts.typ_of_inst thy
   7.254 +      o CodegenConsts.read_const thy) raw_cs
   7.255 +  in
   7.256 +    thy
   7.257 +    |> add_datatype_consts cs
   7.258 +  end;
   7.259 +
   7.260 +end; (*local*)
   7.261  
   7.262  fun add_inline thm thy =
   7.263 -  (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (insert Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy;
   7.264 +  (map_exec_purge NONE o map_preproc o apfst o apfst)
   7.265 +    (fold (insert Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy;
   7.266 +        (*fully applied in order to get right context for mk_rew!*)
   7.267  
   7.268  fun del_inline thm thy =
   7.269 -  (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (remove Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy ;
   7.270 +  (map_exec_purge NONE o map_preproc o apfst o apfst)
   7.271 +    (fold (remove Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy;
   7.272 +        (*fully applied in order to get right context for mk_rew!*)
   7.273  
   7.274  fun add_inline_proc (name, f) =
   7.275 -  (map_exec_purge NONE o map_preproc o apfst o apsnd) (AList.update (op =) (name, (serial (), f)));
   7.276 +  (map_exec_purge NONE o map_preproc o apfst o apsnd)
   7.277 +    (AList.update (op =) (name, (serial (), f)));
   7.278  
   7.279  fun del_inline_proc name =
   7.280 -  (map_exec_purge NONE o map_preproc o apfst o apsnd) (delete_force "inline procedure" name);
   7.281 +  (map_exec_purge NONE o map_preproc o apfst o apsnd)
   7.282 +    (delete_force "inline procedure" name);
   7.283  
   7.284  fun add_preproc (name, f) =
   7.285    (map_exec_purge NONE o map_preproc o apsnd) (AList.update (op =) (name, (serial (), f)));
   7.286 @@ -774,6 +769,25 @@
   7.287  
   7.288  end; (*local*)
   7.289  
   7.290 +fun get_datatype thy tyco =
   7.291 +  case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
   7.292 +   of SOME spec => spec
   7.293 +    | NONE => Sign.arity_number thy tyco
   7.294 +        |> Name.invents Name.context "'a"
   7.295 +        |> map (rpair [])
   7.296 +        |> rpair [];
   7.297 +
   7.298 +fun get_datatype_of_constr thy =
   7.299 +  Consttab.lookup ((the_dcontrs o get_exec) thy);
   7.300 +
   7.301 +fun get_datatype_constr thy const =
   7.302 +  case Consttab.lookup ((the_dcontrs o get_exec) thy) const
   7.303 +   of SOME tyco => let
   7.304 +        val (vs, cs) = get_datatype thy tyco;
   7.305 +        (*FIXME continue here*)
   7.306 +      in NONE end
   7.307 +    | NONE => NONE;
   7.308 +
   7.309  local
   7.310  
   7.311  fun get_funcs thy const =
   7.312 @@ -812,14 +826,6 @@
   7.313  
   7.314  end; (*local*)
   7.315  
   7.316 -fun get_datatype thy tyco =
   7.317 -  Symtab.lookup ((the_dtyps o get_exec) thy) tyco
   7.318 -  |> Option.map (fn (spec, thms) => (Susp.force thms; spec));
   7.319 -
   7.320 -fun get_datatype_of_constr thy c =
   7.321 -  Consttab.lookup ((the_dcontrs o get_exec) thy) c
   7.322 -  |> (Option.map o tap) (fn dtco => get_datatype thy dtco);
   7.323 -
   7.324  
   7.325  (** code attributes **)
   7.326  
   7.327 @@ -846,15 +852,23 @@
   7.328  and K = OuterKeyword
   7.329  
   7.330  val print_codesetupK = "print_codesetup";
   7.331 +val code_datatypeK = "code_datatype";
   7.332  
   7.333  in
   7.334  
   7.335  val print_codesetupP =
   7.336 -  OuterSyntax.improper_command print_codesetupK "print code generator setup of this theory" OuterKeyword.diag
   7.337 +  OuterSyntax.improper_command print_codesetupK "print code generator setup of this theory" K.diag
   7.338      (Scan.succeed
   7.339        (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep (CodeData.print o Toplevel.theory_of)));
   7.340  
   7.341 -val _ = OuterSyntax.add_parsers [print_codesetupP];
   7.342 +val code_datatypeP =
   7.343 +  OuterSyntax.command code_datatypeK "define set of code datatype constructors" K.thy_decl (
   7.344 +    Scan.repeat1 P.term
   7.345 +    >> (Toplevel.theory o add_datatype_consts_cmd)
   7.346 +  );
   7.347 +
   7.348 +
   7.349 +val _ = OuterSyntax.add_parsers [print_codesetupP, code_datatypeP];
   7.350  
   7.351  end; (*local*)
   7.352  
     8.1 --- a/src/Pure/Tools/codegen_package.ML	Fri Mar 09 08:45:50 2007 +0100
     8.2 +++ b/src/Pure/Tools/codegen_package.ML	Fri Mar 09 08:45:53 2007 +0100
     8.3 @@ -148,11 +148,7 @@
     8.4        let
     8.5          fun defgen_datatype trns =
     8.6            let
     8.7 -            val (vs, cos) = case CodegenData.get_datatype thy tyco
     8.8 -             of SOME x => x
     8.9 -              | NONE => (Name.invents Name.context "'a" (Sign.arity_number thy tyco)
    8.10 -                  |> map (rpair (Sign.defaultS thy)) , [])
    8.11 -              (*FIXME move to CodegenData*)
    8.12 +            val (vs, cos) = CodegenData.get_datatype thy tyco;
    8.13            in
    8.14              trns
    8.15              |> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs