# HG changeset patch # User haftmann # Date 1173426353 -3600 # Node ID c1836b14c63abd95de565e7687d56da004e0610c # Parent ee19cdb07528f571f387c18fc9806aabc3036389 dropped code datatype certificates diff -r ee19cdb07528 -r c1836b14c63a doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Mar 09 08:45:50 2007 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Fri Mar 09 08:45:53 2007 +0100 @@ -1187,8 +1187,8 @@ @{index_ML CodegenData.add_preproc: "string * (theory -> thm list -> thm list) -> theory -> theory"} \\ @{index_ML CodegenData.del_preproc: "string -> theory -> theory"} \\ - @{index_ML CodegenData.add_datatype: "string * (((string * sort) list * (string * typ list) list) - * thm list Susp.T) -> theory -> theory"} \\ + @{index_ML CodegenData.add_datatype: "string * ((string * sort) list * (string * typ list) list) + -> theory -> theory"} \\ @{index_ML CodegenData.del_datatype: "string -> theory -> theory"} \\ @{index_ML CodegenData.get_datatype: "theory -> string -> ((string * sort) list * (string * typ list) list) option"} \\ @@ -1232,14 +1232,12 @@ \item @{ML CodegenData.del_preproc}~@{text "name"}~@{text "thy"} removes generic preprcoessor named @{text name} from executable content. - \item @{ML CodegenData.add_datatype}~@{text "(name, (spec, cert))"}~@{text "thy"} adds + \item @{ML CodegenData.add_datatype}~@{text "(name, spec)"}~@{text "thy"} adds a datatype to executable content, with type constructor @{text name} and specification @{text spec}; @{text spec} is a pair consisting of a list of type variable with sort constraints and a list of constructors with name - and types of arguments. The addition as datatype - has to be justified giving a certificate of suspended - theorems as witnesses for injectiveness and distinctness. + and types of arguments. \item @{ML CodegenData.del_datatype}~@{text "name"}~@{text "thy"} remove a datatype from executable content, if present. diff -r ee19cdb07528 -r c1836b14c63a src/HOL/Code_Generator.thy --- a/src/HOL/Code_Generator.thy Fri Mar 09 08:45:50 2007 +0100 +++ b/src/HOL/Code_Generator.thy Fri Mar 09 08:45:53 2007 +0100 @@ -87,7 +87,9 @@ (Haskell infixl 4 "==") -text {* boolean expressions *} +text {* type bool *} + +code_datatype True False lemma [code func]: shows "(False \ x) = False" @@ -152,18 +154,22 @@ bool true false not -text {* itself as a code generator datatype *} +text {* type prop *} + +code_datatype Trueprop "prop" + + +text {* type itself *} -setup {* - let - val v = ("'a", []); - val t = Logic.mk_type (TFree v); - val Const (c, ty) = t; - val (_, Type (dtco, _)) = strip_type ty; - in - CodegenData.add_datatype (dtco, (([v], [(c, [])]), CodegenData.lazy (fn () => []))) - end -*} +code_datatype "TYPE('a)" + + +text {* prevent unfolding of quantifier definitions *} + +lemma [code func]: + "Ex = Ex" + "All = All" + by rule+ text {* code generation for arbitrary as exception *} diff -r ee19cdb07528 -r c1836b14c63a src/HOL/Library/EfficientNat.thy --- a/src/HOL/Library/EfficientNat.thy Fri Mar 09 08:45:50 2007 +0100 +++ b/src/HOL/Library/EfficientNat.thy Fri Mar 09 08:45:53 2007 +0100 @@ -159,7 +159,7 @@ (Haskell "!((_) + 1)") setup {* - CodegenData.del_datatype "nat" + CodegenData.add_datatype ("nat", ([], [])) *} types_code diff -r ee19cdb07528 -r c1836b14c63a src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Fri Mar 09 08:45:50 2007 +0100 +++ b/src/HOL/Tools/datatype_codegen.ML Fri Mar 09 08:45:53 2007 +0100 @@ -9,8 +9,6 @@ sig val get_eq: theory -> string -> thm list val get_eq_datatype: theory -> string -> thm list - val get_cert: theory -> bool * string -> thm list - val get_cert_datatype: theory -> string -> thm list val dest_case_expr: theory -> term -> ((string * typ) list * ((term * typ) * (term * term) list)) option val add_datatype_case_const: string -> theory -> theory @@ -28,7 +26,7 @@ -> (string * (arity * term list)) list option val prove_codetypes_arities: tactic -> (string * bool) list -> sort -> (arity list -> (string * term list) list -> theory - -> ((bstring * Attrib.src list) * term) list * theory) + -> ((bstring * Attrib.src list) * term) list * theory) -> (arity list -> (string * term list) list -> theory -> theory) -> theory -> theory @@ -379,35 +377,6 @@ in map mk_dist (sym_product cos) end; local - val bool_eq_implies = iffD1; - val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric; - val rew_conj = thm "HOL.atomize_conj" |> Thm.symmetric; - val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI]; - val not_eq_quodlibet = thm "not_eq_quodlibet"; -in - -fun get_cert_datatype thy dtco = - let - val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco; - val inject = (#inject o DatatypePackage.the_datatype thy) dtco - |> map (fn thm => bool_eq_implies OF [thm] ) - |> map (MetaSimplifier.rewrite_rule [rew_eq, rew_conj]); - val ctxt = ProofContext.init thy; - val simpset = Simplifier.context ctxt - (MetaSimplifier.empty_ss addsimprocs [DatatypePackage.distinct_simproc]); - val cos = map (fn (co, tys) => - (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs; - val tac = ALLGOALS (simp_tac simpset) - THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]); - val distinct = - mk_distinct cos - |> map (fn t => Goal.prove_global thy [] [] t (K tac)) - |> map (fn thm => not_eq_quodlibet OF [thm]) - in inject @ distinct end - -end; - -local val not_sym = thm "HOL.not_sym"; val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI]; val refl = thm "refl"; @@ -496,9 +465,6 @@ | get_spec thy (tyco, false) = TypecopyPackage.get_spec thy tyco; -fun get_cert thy (true, dtco) = get_cert_datatype thy dtco - | get_cert thy (false, dtco) = [TypecopyPackage.get_cert thy dtco]; - local fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco of SOME _ => get_eq_datatype thy tyco @@ -559,20 +525,20 @@ (* registering code types in code generator *) -fun codetype_hook specs = - let - fun add (dtco, (flag, spec)) thy = - let - fun cert thy_ref = (fn () => get_cert (Theory.deref thy_ref) (flag, dtco)); - in - CodegenData.add_datatype - (dtco, (spec, CodegenData.lazy (cert (Theory.self_ref thy)))) thy - end; - in fold add specs end; +val codetype_hook = + fold (fn (dtco, (_, spec)) => CodegenData.add_datatype (dtco, spec)); (* instrumentalizing the sort algebra *) +(*fun assume_arities_of_sort thy arities ty_sort = + let + val pp = Sign.pp thy; + val algebra = Sign.classes_of thy + |> fold (fn (tyco, asorts, sort) => + Sorts.add_arities pp (tyco, map (fn class => (class, asorts)) sort)) arities; + in Sorts.of_sort algebra ty_sort end; + fun get_codetypes_arities thy tycos sort = let val algebra = Sign.classes_of thy; @@ -588,7 +554,7 @@ fun typ_of_sort ty = let val arities = map (fn (tyco, _) => (tyco, map snd vs, sort)) css; - in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end; + in assume_arities_of_sort thy arities (ty, sort) end; fun mk_cons tyco (c, tys) = let val ts = Name.names Name.context "a" tys; @@ -598,7 +564,34 @@ then SOME ( map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css ) else NONE - end; + end;*) + +fun get_codetypes_arities thy tycos sort = + let + val pp = Sign.pp thy; + val algebra = Sign.classes_of thy; + val (vs_proto, css_proto) = the_codetypes_mut_specs thy tycos; + val vs = map (fn (v, vsort) => (v, Sorts.inter_sort algebra (vsort, sort))) vs_proto; + val css = map (fn (tyco, (_, cs)) => (tyco, cs)) css_proto; + val algebra' = algebra + |> fold (fn (tyco, _) => + Sorts.add_arities pp (tyco, map (fn class => (class, map snd vs)) sort)) css; + fun typ_sort_inst ty = CodegenConsts.typ_sort_inst algebra' (Logic.varifyT ty, sort); + val venv = Vartab.empty + |> fold (fn (v, sort) => Vartab.update_new ((v, 0), sort)) vs + |> fold (fn (_, cs) => fold (fn (_, tys) => fold typ_sort_inst tys) cs) css; + fun inst (v, _) = (v, (the o Vartab.lookup venv) (v, 0)); + val vs' = map inst vs; + fun mk_arity tyco = (tyco, map snd vs', sort); + fun mk_cons tyco (c, tys) = + let + val tys' = (map o Term.map_type_tfree) (TFree o inst) tys; + val ts = Name.names Name.context "a" tys'; + val ty = (tys' ---> Type (tyco, map TFree vs')); + in list_comb (Const (c, ty), map Free ts) end; + in + map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css |> SOME + end handle Class_Error => NONE; fun prove_codetypes_arities tac tycos sort f after_qed thy = case get_codetypes_arities thy tycos sort diff -r ee19cdb07528 -r c1836b14c63a src/HOL/Tools/typecopy_package.ML --- a/src/HOL/Tools/typecopy_package.ML Fri Mar 09 08:45:50 2007 +0100 +++ b/src/HOL/Tools/typecopy_package.ML Fri Mar 09 08:45:53 2007 +0100 @@ -22,7 +22,6 @@ type hook = string * info -> theory -> theory val add_hook: hook -> theory -> theory val get_spec: theory -> string -> (string * sort) list * (string * typ list) list - val get_cert: theory -> string -> thm val get_eq: theory -> string -> thm val print: theory -> unit val setup: theory -> theory @@ -132,26 +131,16 @@ end; (*local*) -(* equality function equation *) +(* equality function equation and datatype specification *) fun get_eq thy tyco = (#inject o the o get_typecopy_info thy) tyco; - -(* datatype specification and certificate *) - fun get_spec thy tyco = let val SOME { vs, constr, typ, ... } = get_typecopy_info thy tyco in (vs, [(constr, [typ])]) end; -local - val bool_eq_implies = iffD1; - val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric; -in fun get_cert thy tyco = - MetaSimplifier.rewrite_rule [rew_eq] (bool_eq_implies OF [get_eq thy tyco]) -end; (*local*) - (* hook for projection function code *) diff -r ee19cdb07528 -r c1836b14c63a src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Fri Mar 09 08:45:50 2007 +0100 +++ b/src/Pure/Tools/class_package.ML Fri Mar 09 08:45:53 2007 +0100 @@ -27,8 +27,6 @@ val instance_sort_cmd: string * string -> theory -> Proof.state val prove_instance_sort: tactic -> class * sort -> theory -> theory - val assume_arities_of_sort: theory -> arity list -> typ * sort -> bool - (* experimental class target *) val class_of_locale: theory -> string -> class option val add_def_in_class: local_theory -> string @@ -105,17 +103,6 @@ end; -(* contexts with arity assumptions *) - -fun assume_arities_of_sort thy arities ty_sort = - let - val pp = Sign.pp thy; - val algebra = Sign.classes_of thy - |> fold (fn (tyco, asorts, sort) => - Sorts.add_arities pp (tyco, map (fn class => (class, asorts)) sort)) arities; - in Sorts.of_sort algebra ty_sort end; - - (* instances with implicit parameter handling *) local @@ -141,7 +128,7 @@ val _ = case (duplicates (op =) o map #1) arities of [] => () | dupl_tycos => error ("type constructors occur more than once in arities: " - ^ (commas o map quote) dupl_tycos); + ^ (commas o map quote) dupl_tycos); val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory fun get_consts_class tyco ty class = let @@ -179,7 +166,6 @@ in fold_map read defs cs end; val (defs, _) = read_defs raw_defs cs (fold Sign.primitive_arity arities (Theory.copy theory)); - fun get_remove_contraint c thy = let val ty = Sign.the_const_constraint thy c; @@ -334,7 +320,6 @@ (* exporting terms and theorems to global toplevel *) -(*FIXME should also be used when introducing classes*) fun globalize thy classes = let @@ -380,6 +365,7 @@ ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]); + (* tactical interfaces to locale commands *) fun prove_interpretation tac prfx_atts expr insts thy = @@ -431,13 +417,6 @@ local -fun add_axclass (name, supsort) params axs thy = - let - val (c, thy') = thy - |> AxClass.define_class_i (name, supsort) params axs; - val {intro, axioms, ...} = AxClass.get_definition thy' c; - in ((c, (intro, axioms)), thy') end; - fun certify_class thy class = tap (the_class_data thy) (Sign.certify_class thy class); @@ -454,27 +433,28 @@ (*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I, typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*) val other_consts = map (prep_param thy) raw_other_consts; - val elems = fold_rev (fn Locale.Elem e => cons e | _ => I) - raw_elems []; (*FIXME make include possible here?*) + val (elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e) + | Locale.Expr i => apsnd (cons i)) raw_elems ([], []); val supclasses = map (prep_class thy) raw_supclasses; val supsort = supclasses |> Sign.certify_sort thy - |> (fn [] => Sign.defaultS thy | S => S); (*FIXME Why syntax defaultS?*) - val supexpr = Locale.Merge - (map (Locale.Locale o #locale o the_class_data thy) supclasses); - val supparams = (map fst o Locale.parameters_of_expr thy) supexpr; + |> (fn [] => Sign.defaultS thy | S => S); (*FIXME Why syntax defaultS?*) + val suplocales = map (Locale.Locale o #locale o the_class_data thy) supclasses; + val supexpr = Locale.Merge (suplocales @ includes); + val supparams = (map fst o Locale.parameters_of_expr thy) + (Locale.Merge suplocales); val supconsts = AList.make (the o AList.lookup (op =) (param_map thy supclasses)) (map fst supparams); - (*FIXME include proper*) (*val elems_constrains = map (Element.Constrains o apsnd (Term.map_type_tfree subst_classtyvar)) supparams;*) fun extract_params thy name_locale = - let + let val params = Locale.parameters_of thy name_locale; in (map (fst o fst) params, params - |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, Sign.defaultS thy))) + |> (map o apfst o apsnd o Term.map_type_tfree) + (K (TFree (AxClass.param_tyvarname, Sign.defaultS thy))) |> (map o apsnd) (fork_mixfix true NONE #> fst) |> chop (length supconsts) |> snd) @@ -486,8 +466,8 @@ Const ((fst o the o AList.lookup (op =) consts) c, ty) | subst t = t; fun prep_asm ((name, atts), ts) = - (*FIXME: name handling?*) - ((NameSpace.base name, map (Attrib.attribute thy) atts), (map o map_aterms) subst ts); + ((NameSpace.base name, map (Attrib.attribute thy) atts), + (map o map_aterms) subst ts); in Locale.global_asms_of thy name_locale |> map prep_asm @@ -578,17 +558,24 @@ fun add_def_in_class lthy class ((c, syn), ((name, atts), (rhs, eq))) thy = let + val prfx = (Logic.const_of_class o NameSpace.base) class; val rhs' = global_term thy [class] rhs; val (syn', _) = fork_mixfix true NONE syn; val ty = Term.fastype_of rhs'; + fun mk_name thy c = + let + val n1 = Sign.full_name thy c; + val n2 = NameSpace.qualifier n1; + val n3 = NameSpace.base n1; + in NameSpace.implode [n2, prfx, n3] end; fun add_const (c, ty, syn) = Sign.add_consts_authentic [(c, ty, syn)] - #> pair (Sign.full_name thy c, ty); + #> pair (mk_name thy c, ty); fun add_def ((name, atts), prop) thy = thy |> PureThy.add_defs_i false [((name, prop), map (Attrib.attribute thy) atts)] |>> the_single; - (*val _ = Output.info "------ DEF ------"; + val _ = Output.info "------ DEF ------"; val _ = Output.info c; val _ = Output.info name; val _ = (Output.info o Sign.string_of_term thy) rhs'; @@ -603,12 +590,14 @@ val _ = map print_witness witness; val _ = (Output.info o string_of_thm) eq'; val eq'' = Element.satisfy_thm witness eq'; - val _ = (Output.info o string_of_thm) eq'';*) + val _ = (Output.info o string_of_thm) eq''; in thy - (*|> add_const (c, ty, syn') + |> Sign.add_path prfx + |> add_const (c, ty, syn') |-> (fn c => add_def ((name, atts), Logic.mk_equals (Const c, rhs'))) - |-> (fn global_def_thm => tap (fn _ => (Output.info o string_of_thm) global_def_thm))*) + |-> (fn global_def_thm => tap (fn _ => (Output.info o string_of_thm) global_def_thm)) + |> Sign.restore_naming thy end; end; diff -r ee19cdb07528 -r c1836b14c63a src/Pure/Tools/codegen_data.ML --- a/src/Pure/Tools/codegen_data.ML Fri Mar 09 08:45:50 2007 +0100 +++ b/src/Pure/Tools/codegen_data.ML Fri Mar 09 08:45:53 2007 +0100 @@ -15,9 +15,8 @@ val add_func_legacy: thm -> theory -> theory val del_func: thm -> theory -> theory val add_funcl: CodegenConsts.const * thm list Susp.T -> theory -> theory - val add_datatype: string * (((string * sort) list * (string * typ list) list) * thm list Susp.T) + val add_datatype: string * ((string * sort) list * (string * typ list) list) -> theory -> theory - val del_datatype: string -> theory -> theory val add_inline: thm -> theory -> theory val del_inline: thm -> theory -> theory val add_inline_proc: string * (theory -> cterm list -> thm list) -> theory -> theory @@ -28,8 +27,7 @@ val operational_algebra: theory -> (sort -> sort) * Sorts.algebra val these_funcs: theory -> CodegenConsts.const -> thm list val tap_typ: theory -> CodegenConsts.const -> typ option - val get_datatype: theory -> string - -> ((string * sort) list * (string * typ list) list) option + val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list) val get_datatype_of_constr: theory -> CodegenConsts.const -> string option val preprocess_cterm: cterm -> thm @@ -193,7 +191,7 @@ in (SOME consts, thms) end; val eq_string = op = : string * string -> bool; -fun eq_dtyp (((vs1, cs1), _), ((vs2, cs2), _)) = +fun eq_dtyp ((vs1, cs1), (vs2, cs2)) = gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2) andalso gen_eq_set (eq_pair eq_string (eq_list (is_equal o Term.typ_ord))) (cs1, cs2); fun merge_dtyps (tabs as (tab1, tab2)) = @@ -210,7 +208,7 @@ datatype spec = Spec of { funcs: sdthms Consttab.table, dconstrs: string Consttab.table, - dtyps: (((string * sort) list * (string * typ list) list) * thm list Susp.T) Symtab.table + dtyps: ((string * sort) list * (string * typ list) list) Symtab.table }; fun mk_spec ((funcs, dconstrs), dtyps) = @@ -328,15 +326,17 @@ (Pretty.block o Pretty.fbreaks) ( Pretty.str s :: pretty_sdthms ctxt lthms ); - fun pretty_dtyp (s, cos) = - (Pretty.block o Pretty.breaks) ( - Pretty.str s - :: Pretty.str "=" - :: Pretty.separate "|" (map (fn (c, []) => Pretty.str c - | (c, tys) => - (Pretty.block o Pretty.breaks) - (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos) - ) + fun pretty_dtyp (s, []) = + Pretty.str s + | pretty_dtyp (s, cos) = + (Pretty.block o Pretty.breaks) ( + Pretty.str s + :: Pretty.str "=" + :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c + | (c, tys) => + (Pretty.block o Pretty.breaks) + (Pretty.str c :: Pretty.str "of" :: map (Pretty.quote o Sign.pretty_typ thy) tys)) cos) + ); val inlines = (#inlines o the_preproc) exec; val inline_procs = (map fst o #inline_procs o the_preproc) exec; val preprocs = (map fst o #preprocs o the_preproc) exec; @@ -346,13 +346,14 @@ |> sort (string_ord o pairself fst); val dtyps = the_dtyps exec |> Symtab.dest - |> map (fn (dtco, ((vs, cos), _)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos)) + |> map (fn (dtco, (vs, cos)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos)) |> sort (string_ord o pairself fst) in (Pretty.writeln o Pretty.chunks) [ Pretty.block ( Pretty.str "defining equations:" - :: map pretty_func funs + :: Pretty.fbrk + :: (Pretty.fbreaks o map pretty_func) funs ), Pretty.block ( Pretty.str "inlining theorems:" @@ -431,77 +432,6 @@ ^ CodegenConsts.string_of_const thy c ^ "\n" ^ string_of_thm thm) in map cert c_thms end; -fun mk_cos tyco vs cos = - let - val dty = Type (tyco, map TFree vs); - fun mk_co (co, tys) = (Const (co, (tys ---> dty)), map I tys); - in map mk_co cos end; - -fun mk_co_args (co, tys) ctxt = - let - val names = Name.invents ctxt "a" (length tys); - val ctxt' = fold Name.declare names ctxt; - val vs = map2 (fn v => fn ty => Free (fst (v, 0), I ty)) names tys; - in (vs, ctxt') end; - -fun check_freeness thy cos thms = - let - val props = AList.make Drule.plain_prop_of thms; - fun sym_product [] = [] - | sym_product (x::xs) = map (pair x) xs @ sym_product xs; - val quodlibet = - let - val judg = ObjectLogic.fixed_judgment (the_context ()) "x"; - val [free] = fold_aterms (fn v as Free _ => cons v | _ => I) judg []; - val judg' = Term.subst_free [(free, Bound 0)] judg; - val prop = Type ("prop", []); - val prop' = fastype_of judg'; - in - Const ("all", (prop' --> prop) --> prop) $ Abs ("P", prop', judg') - end; - fun check_inj (co, []) = - NONE - | check_inj (co, tys) = - let - val ((xs, ys), _) = Name.context - |> mk_co_args (co, tys) - ||>> mk_co_args (co, tys); - val prem = Logic.mk_equals - (list_comb (co, xs), list_comb (co, ys)); - val concl = Logic.mk_conjunction_list - (map2 (curry Logic.mk_equals) xs ys); - val t = Logic.mk_implies (prem, concl); - in case find_first (curry Term.could_unify t o snd) props - of SOME (thm, _) => SOME thm - | NONE => error ("Could not prove injectiveness statement\n" - ^ Sign.string_of_term thy t - ^ "\nfor constructor " - ^ CodegenConsts.string_of_const_typ thy (dest_Const co) - ^ "\nwith theorems\n" ^ cat_lines (map string_of_thm thms)) - end; - fun check_dist ((co1, tys1), (co2, tys2)) = - let - val ((xs1, xs2), _) = Name.context - |> mk_co_args (co1, tys1) - ||>> mk_co_args (co2, tys2); - val prem = Logic.mk_equals - (list_comb (co1, xs1), list_comb (co2, xs2)); - val t = Logic.mk_implies (prem, quodlibet); - in case find_first (curry Term.could_unify t o snd) props - of SOME (thm, _) => thm - | NONE => error ("Could not prove distinctness statement\n" - ^ Sign.string_of_term thy t - ^ "\nfor constructors " - ^ CodegenConsts.string_of_const_typ thy (dest_Const co1) - ^ " and " - ^ CodegenConsts.string_of_const_typ thy (dest_Const co2) - ^ "\nwith theorems\n" ^ cat_lines (map string_of_thm thms)) - end; - in (map_filter check_inj cos, map check_dist (sym_product cos)) end; - -fun certify_datatype thy dtco cs thms = - (op @) (check_freeness thy cs thms); - (** operational sort algebra and class discipline **) @@ -684,37 +614,102 @@ (add_lthms lthms'))) thy end; -fun add_datatype (tyco, (vs_cos as (vs, cos), lthms)) thy = +local + +fun consts_of_cos thy tyco vs cos = + let + val dty = Type (tyco, map TFree vs); + fun mk_co (co, tys) = CodegenConsts.norm_of_typ thy (co, tys ---> dty); + in map mk_co cos end; + +fun co_of_const thy (c, ty) = let - val cs = mk_cos tyco vs cos; - val consts = map (CodegenConsts.norm_of_typ thy o dest_Const o fst) cs; - val add = - map_dtyps (Symtab.update_new (tyco, - (vs_cos, certificate thy (fn thy => certify_datatype thy tyco cs) lthms))) - #> map_dconstrs (fold (fn c => Consttab.update (c, tyco)) consts) - in map_exec_purge (SOME consts) add thy end; + fun err () = error + ("Illegal type for datatype constructor: " ^ Sign.string_of_typ thy ty); + val (tys, ty') = strip_type ty; + val (tyco, vs) = ((apsnd o map) dest_TFree o dest_Type) ty' + handle TYPE _ => err (); + val sorts = if has_duplicates (eq_fst op =) vs then err () + else map snd vs; + val vs_names = Name.invent_list [] "'a" (length vs); + val vs_map = map fst vs ~~ vs_names; + val vs' = vs_names ~~ sorts; + val tys' = (map o map_type_tfree) (fn (v, sort) => + (TFree ((the o AList.lookup (op =) vs_map) v, sort))) tys + handle Option => err (); + in (tyco, (vs', (c, tys'))) end; fun del_datatype tyco thy = + case Symtab.lookup ((the_dtyps o get_exec) thy) tyco + of SOME (vs, cos) => let + val consts = consts_of_cos thy tyco vs cos; + val del = + map_dtyps (Symtab.delete tyco) + #> map_dconstrs (fold Consttab.delete consts) + in map_exec_purge (SOME consts) del thy end + | NONE => thy; + +(*FIXME integrate this auxiliary properly*) + +in + +fun add_datatype (tyco, (vs_cos as (vs, cos))) thy = let - val SOME ((vs, cos), _) = Symtab.lookup ((the_dtyps o get_exec) thy) tyco; - val cs = mk_cos tyco vs cos; - val consts = map (CodegenConsts.norm_of_typ thy o dest_Const o fst) cs; - val del = - map_dtyps (Symtab.delete tyco) - #> map_dconstrs (fold Consttab.delete consts) - in map_exec_purge (SOME consts) del thy end; + val consts = consts_of_cos thy tyco vs cos; + val add = + map_dtyps (Symtab.update_new (tyco, vs_cos)) + #> map_dconstrs (fold (fn c => Consttab.update (c, tyco)) consts) + in + thy + |> del_datatype tyco + |> map_exec_purge (SOME consts) add + end; + +fun add_datatype_consts cs thy = + let + val raw_cos = map (co_of_const thy) cs; + val (tyco, (vs_names, sorts_cos)) = if (length o distinct (eq_fst op =)) raw_cos = 1 + then ((fst o hd) raw_cos, ((map fst o fst o snd o hd) raw_cos, + map ((apfst o map) snd o snd) raw_cos)) + else error ("Term constructors not referring to the same type: " + ^ commas (map (CodegenConsts.string_of_const_typ thy) cs)); + val sorts = foldr1 ((uncurry o map2 o curry o Sorts.inter_sort) (Sign.classes_of thy)) + (map fst sorts_cos); + val cos = map snd sorts_cos; + val vs = vs_names ~~ sorts; + in + thy + |> add_datatype (tyco, (vs, cos)) + end; + +fun add_datatype_consts_cmd raw_cs thy = + let + val cs = map (apsnd Logic.unvarifyT o CodegenConsts.typ_of_inst thy + o CodegenConsts.read_const thy) raw_cs + in + thy + |> add_datatype_consts cs + end; + +end; (*local*) fun add_inline thm thy = - (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (insert Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy; + (map_exec_purge NONE o map_preproc o apfst o apfst) + (fold (insert Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy; + (*fully applied in order to get right context for mk_rew!*) fun del_inline thm thy = - (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (remove Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy ; + (map_exec_purge NONE o map_preproc o apfst o apfst) + (fold (remove Thm.eq_thm) (CodegenFunc.mk_rew thm)) thy; + (*fully applied in order to get right context for mk_rew!*) fun add_inline_proc (name, f) = - (map_exec_purge NONE o map_preproc o apfst o apsnd) (AList.update (op =) (name, (serial (), f))); + (map_exec_purge NONE o map_preproc o apfst o apsnd) + (AList.update (op =) (name, (serial (), f))); fun del_inline_proc name = - (map_exec_purge NONE o map_preproc o apfst o apsnd) (delete_force "inline procedure" name); + (map_exec_purge NONE o map_preproc o apfst o apsnd) + (delete_force "inline procedure" name); fun add_preproc (name, f) = (map_exec_purge NONE o map_preproc o apsnd) (AList.update (op =) (name, (serial (), f))); @@ -774,6 +769,25 @@ end; (*local*) +fun get_datatype thy tyco = + case Symtab.lookup ((the_dtyps o get_exec) thy) tyco + of SOME spec => spec + | NONE => Sign.arity_number thy tyco + |> Name.invents Name.context "'a" + |> map (rpair []) + |> rpair []; + +fun get_datatype_of_constr thy = + Consttab.lookup ((the_dcontrs o get_exec) thy); + +fun get_datatype_constr thy const = + case Consttab.lookup ((the_dcontrs o get_exec) thy) const + of SOME tyco => let + val (vs, cs) = get_datatype thy tyco; + (*FIXME continue here*) + in NONE end + | NONE => NONE; + local fun get_funcs thy const = @@ -812,14 +826,6 @@ end; (*local*) -fun get_datatype thy tyco = - Symtab.lookup ((the_dtyps o get_exec) thy) tyco - |> Option.map (fn (spec, thms) => (Susp.force thms; spec)); - -fun get_datatype_of_constr thy c = - Consttab.lookup ((the_dcontrs o get_exec) thy) c - |> (Option.map o tap) (fn dtco => get_datatype thy dtco); - (** code attributes **) @@ -846,15 +852,23 @@ and K = OuterKeyword val print_codesetupK = "print_codesetup"; +val code_datatypeK = "code_datatype"; in val print_codesetupP = - OuterSyntax.improper_command print_codesetupK "print code generator setup of this theory" OuterKeyword.diag + OuterSyntax.improper_command print_codesetupK "print code generator setup of this theory" K.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep (CodeData.print o Toplevel.theory_of))); -val _ = OuterSyntax.add_parsers [print_codesetupP]; +val code_datatypeP = + OuterSyntax.command code_datatypeK "define set of code datatype constructors" K.thy_decl ( + Scan.repeat1 P.term + >> (Toplevel.theory o add_datatype_consts_cmd) + ); + + +val _ = OuterSyntax.add_parsers [print_codesetupP, code_datatypeP]; end; (*local*) diff -r ee19cdb07528 -r c1836b14c63a src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Fri Mar 09 08:45:50 2007 +0100 +++ b/src/Pure/Tools/codegen_package.ML Fri Mar 09 08:45:53 2007 +0100 @@ -148,11 +148,7 @@ let fun defgen_datatype trns = let - val (vs, cos) = case CodegenData.get_datatype thy tyco - of SOME x => x - | NONE => (Name.invents Name.context "'a" (Sign.arity_number thy tyco) - |> map (rpair (Sign.defaultS thy)) , []) - (*FIXME move to CodegenData*) + val (vs, cos) = CodegenData.get_datatype thy tyco; in trns |> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs