--- a/src/ZF/Datatype.ML Wed Nov 14 18:46:07 2001 +0100
+++ b/src/ZF/Datatype.ML Wed Nov 14 18:46:30 2001 +0100
@@ -22,11 +22,12 @@
structure Data_Package =
- Add_datatype_def_Fun
- (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
- and Su=Standard_Sum
- and Ind_Package = Ind_Package
- and Datatype_Arg = Data_Arg);
+ Add_datatype_def_Fun
+ (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
+ and Su=Standard_Sum
+ and Ind_Package = Ind_Package
+ and Datatype_Arg = Data_Arg
+ val coind = false);
(*Typechecking rules for most codatatypes involving quniv*)
@@ -42,10 +43,12 @@
end;
structure CoData_Package =
- Add_datatype_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
- and Su=Quine_Sum
- and Ind_Package = CoInd_Package
- and Datatype_Arg = CoData_Arg);
+ Add_datatype_def_Fun
+ (structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
+ and Su=Quine_Sum
+ and Ind_Package = CoInd_Package
+ and Datatype_Arg = CoData_Arg
+ val coind = true);
--- a/src/ZF/Datatype.thy Wed Nov 14 18:46:07 2001 +0100
+++ b/src/ZF/Datatype.thy Wed Nov 14 18:46:30 2001 +0100
@@ -7,7 +7,8 @@
*)
theory Datatype = Inductive + Univ + QUniv
- files "Tools/datatype_package.ML":
+ files
+ "Tools/datatype_package.ML"
+ "Tools/numeral_syntax.ML": (*belongs to theory Bin*)
end
-
--- a/src/ZF/Inductive.thy Wed Nov 14 18:46:07 2001 +0100
+++ b/src/ZF/Inductive.thy Wed Nov 14 18:46:30 2001 +0100
@@ -8,6 +8,7 @@
theory Inductive = Fixedpt + mono
files
+ "ind_syntax.ML"
"Tools/cartprod.ML"
"Tools/ind_cases.ML"
"Tools/inductive_package.ML"
--- a/src/ZF/ROOT.ML Wed Nov 14 18:46:07 2001 +0100
+++ b/src/ZF/ROOT.ML Wed Nov 14 18:46:30 2001 +0100
@@ -21,14 +21,7 @@
use "~~/src/Provers/Arith/cancel_numerals.ML";
use "~~/src/Provers/Arith/combine_numerals.ML";
-use_thy "mono";
-use "ind_syntax.ML";
-use_thy "Datatype";
-
-use "Tools/numeral_syntax.ML";
-(*the all-in-one theory*)
with_path "Integ" use_thy "Main";
-
simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
print_depth 8;
--- a/src/ZF/Tools/datatype_package.ML Wed Nov 14 18:46:07 2001 +0100
+++ b/src/ZF/Tools/datatype_package.ML Wed Nov 14 18:46:30 2001 +0100
@@ -12,7 +12,6 @@
Products are used only to derive "streamlined" induction rules for relations
*)
-
type datatype_result =
{con_defs : thm list, (*definitions made in thy*)
case_eqns : thm list, (*equations for case operator*)
@@ -21,53 +20,40 @@
free_SEs : thm list, (*freeness destruct rules*)
mk_free : string -> thm}; (*function to make freeness theorems*)
-
signature DATATYPE_ARG =
- sig
+sig
val intrs : thm list
val elims : thm list
- end;
-
+end;
(*Functor's result signature*)
signature DATATYPE_PACKAGE =
sig
-
(*Insert definitions for the recursive sets, which
must *already* be declared as constants in parent theory!*)
- val add_datatype_i:
- term * term list * Ind_Syntax.constructor_spec list list *
- thm list * thm list * thm list
- -> theory -> theory * inductive_result * datatype_result
-
- val add_datatype:
- string * string list *
- (string * string list * mixfix) list list *
- thm list * thm list * thm list
- -> theory -> theory * inductive_result * datatype_result
-
+ val add_datatype_i: term * term list -> Ind_Syntax.constructor_spec list list ->
+ thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
+ val add_datatype_x: string * string list -> (string * string list * mixfix) list list ->
+ thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
+ val add_datatype: string * string list -> (string * string list * mixfix) list list ->
+ (xstring * Args.src list) list * (xstring * Args.src list) list *
+ (xstring * Args.src list) list -> theory -> theory * inductive_result * datatype_result
end;
-
-(*Declares functions to add fixedpoint/constructor defs to a theory.
- Recursive sets must *already* be declared as constants.*)
functor Add_datatype_def_Fun
- (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU
- and Ind_Package : INDUCTIVE_PACKAGE
- and Datatype_Arg : DATATYPE_ARG)
- : DATATYPE_PACKAGE =
+ (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU
+ and Ind_Package : INDUCTIVE_PACKAGE
+ and Datatype_Arg : DATATYPE_ARG
+ val coind : bool): DATATYPE_PACKAGE =
struct
+(*con_ty_lists specifies the constructors in the form (name, prems, mixfix) *)
-(*con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
-fun add_datatype_i (dom_sum, rec_tms, con_ty_lists,
- monos, type_intrs, type_elims) thy =
+fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy =
let
- open BasisLibrary
val dummy = (*has essential ancestors?*)
Theory.requires thy "Datatype" "(co)datatype definitions";
-
val rec_names = map (#1 o dest_Const o head_of) rec_tms
val rec_base_names = map Sign.base_name rec_names
val big_rec_base_name = space_implode "_" rec_base_names
@@ -80,9 +66,7 @@
val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists);
val dummy =
- writeln ((if (#1 (dest_Const Fp.oper) = "Fixedpt.lfp") then "Datatype"
- else "Codatatype")
- ^ " definition " ^ big_rec_name)
+ writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ big_rec_name);
val case_varname = "f"; (*name for case variables*)
@@ -238,8 +222,7 @@
(* Build the new theory *)
- val need_recursor =
- (#1 (dest_Const Fp.oper) = "Fixedpt.lfp" andalso recursor_typ <> case_typ);
+ val need_recursor = (not coind andalso recursor_typ <> case_typ);
fun add_recursor thy =
if need_recursor then
@@ -387,17 +370,11 @@
in
(*Updating theory components: simprules and datatype info*)
(thy1 |> Theory.add_path big_rec_base_name
- |> (#1 o PureThy.add_thmss [(("simps", simps),
- [Simplifier.simp_add_global])])
- |> (#1 o PureThy.add_thmss [(("", intrs),
- (*not "intrs" to avoid the warning that they
- are already stored by the inductive package*)
- [Classical.safe_intro_global])])
- |> DatatypesData.put
- (Symtab.update
- ((big_rec_name, dt_info), DatatypesData.get thy1))
- |> ConstructorsData.put
- (foldr Symtab.update (con_pairs, ConstructorsData.get thy1))
+ |> (#1 o PureThy.add_thmss
+ [(("simps", simps), [Simplifier.simp_add_global]),
+ (("", intrs), [Classical.safe_intro_global])])
+ |> DatatypesData.map (fn tab => Symtab.update ((big_rec_name, dt_info), tab))
+ |> ConstructorsData.map (fn tab => foldr Symtab.update (con_pairs, tab))
|> Theory.parent_path,
ind_result,
{con_defs = con_defs,
@@ -409,20 +386,52 @@
end;
-fun add_datatype (sdom, srec_tms, scon_ty_lists,
- monos, type_intrs, type_elims) thy =
- let val sign = sign_of thy
- val read_i = Sign.simple_read_term sign Ind_Syntax.iT
- val rec_tms = map read_i srec_tms
- val con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists
- val dom_sum =
- if sdom = "" then
- Ind_Syntax.data_domain (#1(dest_Const Fp.oper) <> "Fixedpt.lfp")
- (rec_tms, con_ty_lists)
- else read_i sdom
- in
- add_datatype_i (dom_sum, rec_tms, con_ty_lists,
- monos, type_intrs, type_elims) thy
- end
+fun add_datatype_x (sdom, srec_tms) scon_ty_lists (monos, type_intrs, type_elims) thy =
+ let
+ val sign = sign_of thy;
+ val read_i = Sign.simple_read_term sign Ind_Syntax.iT;
+ val rec_tms = map read_i srec_tms;
+ val con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists
+ val dom_sum =
+ if sdom = "" then Ind_Syntax.data_domain coind (rec_tms, con_ty_lists)
+ else read_i sdom;
+ in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy end;
+
+fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
+ let
+ val (thy', ((monos, type_intrs), type_elims)) = thy
+ |> IsarThy.apply_theorems raw_monos
+ |>>> IsarThy.apply_theorems raw_type_intrs
+ |>>> IsarThy.apply_theorems raw_type_elims;
+ in add_datatype_x (sdom, srec_tms) scon_ty_lists (monos, type_intrs, type_elims) thy' end;
+
+
+(* outer syntax *)
+
+local structure P = OuterParse and K = OuterSyntax.Keyword in
+
+fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) =
+ #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
+
+val con_decl =
+ P.name -- Scan.optional (P.$$$ "(" |-- P.list1 P.term --| P.$$$ ")") [] -- P.opt_mixfix
+ >> P.triple1;
+
+val datatype_decl =
+ (Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
+ P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
+ Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
+ Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
+ Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1 --| P.marg_comment) []
+ >> (Toplevel.theory o mk_datatype);
+
+val coind_prefix = if coind then "co" else "";
+
+val inductiveP = OuterSyntax.command (coind_prefix ^ "datatype")
+ ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl;
+
+val _ = OuterSyntax.add_parsers [inductiveP];
end;
+
+end;
--- a/src/ZF/Tools/inductive_package.ML Wed Nov 14 18:46:07 2001 +0100
+++ b/src/ZF/Tools/inductive_package.ML Wed Nov 14 18:46:30 2001 +0100
@@ -47,6 +47,7 @@
(structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU val coind: bool)
: INDUCTIVE_PACKAGE =
struct
+
open Logic Ind_Syntax;
@@ -522,28 +523,27 @@
|> standard
and mutual_induct = CP.remove_split mutual_induct_fsplit
- val induct_att =
- (case rec_names of [name] => [InductAttrib.induct_set_global name] | _ => []);
- val (thy', [induct', mutual_induct']) =
- thy |> PureThy.add_thms [(("induct", induct), induct_att),
- (("mutual_induct", mutual_induct), [])];
+ val (thy', [induct', mutual_induct']) = thy |>
+ PureThy.add_thms [(("induct", induct), [InductAttrib.induct_set_global big_rec_name]),
+ (("mutual_induct", mutual_induct), [])];
in (thy', induct', mutual_induct')
end; (*of induction_rules*)
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
val (thy2, induct, mutual_induct) =
- if #1 (dest_Const Fp.oper) = "Fixedpt.lfp" then induction_rules raw_induct thy1
+ if not coind then induction_rules raw_induct thy1
else (thy1, raw_induct, TrueI)
and defs = big_rec_def :: part_rec_defs
val (thy3, ([bnd_mono', dom_subset', elim'], [defs', intrs'])) =
thy2
+ |> IndCases.declare big_rec_name make_cases
|> PureThy.add_thms
[(("bnd_mono", bnd_mono), []),
(("dom_subset", dom_subset), []),
- (("cases", elim), [InductAttrib.cases_set_global ""])]
+ (("cases", elim), [InductAttrib.cases_set_global big_rec_name])]
|>>> (PureThy.add_thmss o map Thm.no_attributes)
[("defs", defs),
("intros", intrs)];
--- a/src/ZF/Tools/primrec_package.ML Wed Nov 14 18:46:07 2001 +0100
+++ b/src/ZF/Tools/primrec_package.ML Wed Nov 14 18:46:30 2001 +0100
@@ -9,13 +9,20 @@
signature PRIMREC_PACKAGE =
sig
- val add_primrec_i : (string * term) list -> theory -> theory * thm list
- val add_primrec : (string * string) list -> theory -> theory * thm list
+ val quiet_mode: bool ref
+ val add_primrec: ((bstring * string) * Args.src list) list -> theory -> theory * thm list
+ val add_primrec_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
end;
structure PrimrecPackage : PRIMREC_PACKAGE =
struct
+(* messages *)
+
+val quiet_mode = ref false;
+fun message s = if ! quiet_mode then () else writeln s;
+
+
exception RecError of string;
(*Remove outer Trueprop and equality sign*)
@@ -26,24 +33,25 @@
fun primrec_eq_err sign s eq =
primrec_err (s ^ "\nin equation\n" ^ Sign.string_of_term sign eq);
+
(* preprocessing of equations *)
(*rec_fn_opt records equations already noted for this function*)
-fun process_eqn thy (eq, rec_fn_opt) =
+fun process_eqn thy (eq, rec_fn_opt) =
let
- val (lhs, rhs) =
- if null (term_vars eq) then
- dest_eqn eq handle _ => raise RecError "not a proper equation"
- else raise RecError "illegal schematic variable(s)";
+ val (lhs, rhs) =
+ if null (term_vars eq) then
+ dest_eqn eq handle _ => raise RecError "not a proper equation"
+ else raise RecError "illegal schematic variable(s)";
val (recfun, args) = strip_comb lhs;
- val (fname, ftype) = dest_Const recfun handle _ =>
+ val (fname, ftype) = dest_Const recfun handle _ =>
raise RecError "function is not declared as constant in theory";
val (ls_frees, rest) = take_prefix is_Free args;
val (middle, rs_frees) = take_suffix is_Free rest;
- val (constr, cargs_frees) =
+ val (constr, cargs_frees) =
if null middle then raise RecError "constructor missing"
else strip_comb (hd middle);
val (cname, _) = dest_Const constr
@@ -52,9 +60,9 @@
handle _ =>
raise RecError "cannot determine datatype associated with function"
- val (ls, cargs, rs) = (map dest_Free ls_frees,
- map dest_Free cargs_frees,
- map dest_Free rs_frees)
+ val (ls, cargs, rs) = (map dest_Free ls_frees,
+ map dest_Free cargs_frees,
+ map dest_Free rs_frees)
handle _ => raise RecError "illegal argument in pattern";
val lfrees = ls @ rs @ cargs;
@@ -63,31 +71,31 @@
val new_eqn = (cname, (rhs, cargs, eq))
in
- if not (null (duplicates lfrees)) then
- raise RecError "repeated variable name in pattern"
+ if not (null (duplicates lfrees)) then
+ raise RecError "repeated variable name in pattern"
else if not ((map dest_Free (term_frees rhs)) subset lfrees) then
raise RecError "extra variables on rhs"
- else if length middle > 1 then
+ else if length middle > 1 then
raise RecError "more than one non-variable in pattern"
else case rec_fn_opt of
None => Some (fname, ftype, ls, rs, con_info, [new_eqn])
- | Some (fname', _, ls', rs', con_info': constructor_info, eqns) =>
- if is_some (assoc (eqns, cname)) then
- raise RecError "constructor already occurred as pattern"
- else if (ls <> ls') orelse (rs <> rs') then
- raise RecError "non-recursive arguments are inconsistent"
- else if #big_rec_name con_info <> #big_rec_name con_info' then
- raise RecError ("Mixed datatypes for function " ^ fname)
- else if fname <> fname' then
- raise RecError ("inconsistent functions for datatype " ^
- #big_rec_name con_info)
- else Some (fname, ftype, ls, rs, con_info, new_eqn::eqns)
+ | Some (fname', _, ls', rs', con_info': constructor_info, eqns) =>
+ if is_some (assoc (eqns, cname)) then
+ raise RecError "constructor already occurred as pattern"
+ else if (ls <> ls') orelse (rs <> rs') then
+ raise RecError "non-recursive arguments are inconsistent"
+ else if #big_rec_name con_info <> #big_rec_name con_info' then
+ raise RecError ("Mixed datatypes for function " ^ fname)
+ else if fname <> fname' then
+ raise RecError ("inconsistent functions for datatype " ^
+ #big_rec_name con_info)
+ else Some (fname, ftype, ls, rs, con_info, new_eqn::eqns)
end
handle RecError s => primrec_eq_err (sign_of thy) s eq;
(*Instantiates a recursor equation with constructor arguments*)
-fun inst_recursor ((_ $ constr, rhs), cargs') =
+fun inst_recursor ((_ $ constr, rhs), cargs') =
subst_atomic (#2 (strip_comb constr) ~~ map Free cargs') rhs;
@@ -111,27 +119,27 @@
(*Translate rec equations into function arguments suitable for recursor.
Missing cases are replaced by 0 and all cases are put into order.*)
fun add_case ((cname, recursor_pair), cases) =
- let val (rhs, recursor_rhs, eq) =
- case assoc (eqns, cname) of
- None => (warning ("no equation for constructor " ^ cname ^
- "\nin definition of function " ^ fname);
- (Const ("0", Ind_Syntax.iT),
- #2 recursor_pair, Const ("0", Ind_Syntax.iT)))
- | Some (rhs, cargs', eq) =>
- (rhs, inst_recursor (recursor_pair, cargs'), eq)
- val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
- val abs = foldr absterm (allowed_terms, rhs)
- in
+ let val (rhs, recursor_rhs, eq) =
+ case assoc (eqns, cname) of
+ None => (warning ("no equation for constructor " ^ cname ^
+ "\nin definition of function " ^ fname);
+ (Const ("0", Ind_Syntax.iT),
+ #2 recursor_pair, Const ("0", Ind_Syntax.iT)))
+ | Some (rhs, cargs', eq) =>
+ (rhs, inst_recursor (recursor_pair, cargs'), eq)
+ val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
+ val abs = foldr absterm (allowed_terms, rhs)
+ in
if !Ind_Syntax.trace then
- writeln ("recursor_rhs = " ^
- Sign.string_of_term (sign_of thy) recursor_rhs ^
- "\nabs = " ^ Sign.string_of_term (sign_of thy) abs)
+ writeln ("recursor_rhs = " ^
+ Sign.string_of_term (sign_of thy) recursor_rhs ^
+ "\nabs = " ^ Sign.string_of_term (sign_of thy) abs)
else();
- if Logic.occs (fconst, abs) then
- primrec_eq_err (sign_of thy)
- ("illegal recursive occurrences of " ^ fname)
- eq
- else abs :: cases
+ if Logic.occs (fconst, abs) then
+ primrec_eq_err (sign_of thy)
+ ("illegal recursive occurrences of " ^ fname)
+ eq
+ else abs :: cases
end
val recursor = head_of (#1 (hd recursor_pairs))
@@ -140,58 +148,68 @@
(*the recursive argument*)
val rec_arg = Free (variant (map #1 (ls@rs)) (Sign.base_name big_rec_name),
- Ind_Syntax.iT)
+ Ind_Syntax.iT)
val def_tm = Logic.mk_equals
- (subst_bound (rec_arg, fabs),
- list_comb (recursor,
- foldr add_case (cnames ~~ recursor_pairs, []))
- $ rec_arg)
+ (subst_bound (rec_arg, fabs),
+ list_comb (recursor,
+ foldr add_case (cnames ~~ recursor_pairs, []))
+ $ rec_arg)
in
if !Ind_Syntax.trace then
- writeln ("primrec def:\n" ^
- Sign.string_of_term (sign_of thy) def_tm)
+ writeln ("primrec def:\n" ^
+ Sign.string_of_term (sign_of thy) def_tm)
else();
(Sign.base_name fname ^ "_" ^ Sign.base_name big_rec_name ^ "_def",
def_tm)
end;
-
(* prepare functions needed for definitions *)
-(*Each equation is paired with an optional name, which is "_" (ML wildcard)
- if omitted.*)
-fun add_primrec_i recursion_eqns thy =
+fun add_primrec_i args thy =
let
- val Some (fname, ftype, ls, rs, con_info, eqns) =
- foldr (process_eqn thy) (map snd recursion_eqns, None);
- val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns)
- val (thy', [def_thm]) = thy |> Theory.add_path (Sign.base_name (#1 def))
- |> (PureThy.add_defs_i false o map Thm.no_attributes) [def]
+ val ((eqn_names, eqn_terms), eqn_atts) = apfst split_list (split_list args);
+ val Some (fname, ftype, ls, rs, con_info, eqns) =
+ foldr (process_eqn thy) (eqn_terms, None);
+ val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
+
+ val (thy1, [def_thm]) = thy
+ |> Theory.add_path (Sign.base_name (#1 def))
+ |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
+
val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
- val char_thms =
- (if !Ind_Syntax.trace then (* FIXME message / quiet_mode (!?) *)
- writeln ("Proving equations for primrec function " ^ fname)
- else ();
- map (fn (_,t) =>
- prove_goalw_cterm rewrites
- (Ind_Syntax.traceIt "next primrec equation = "
- (cterm_of (sign_of thy') t))
- (fn _ => [rtac refl 1]))
- recursion_eqns);
- val simps = char_thms;
- val thy'' = thy'
- |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
- |> (#1 o PureThy.add_thms (map (rpair [])
- (filter_out (equal "_" o fst) (map fst recursion_eqns ~~ simps))))
+ val eqn_thms =
+ (message ("Proving equations for primrec function " ^ fname);
+ map (fn t => prove_goalw_cterm rewrites
+ (Ind_Syntax.traceIt "next primrec equation = " (cterm_of (sign_of thy1) t))
+ (fn _ => [rtac refl 1])) eqn_terms);
+
+ val (thy2, eqn_thms') = thy1 |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts);
+ val thy3 = thy2
+ |> (#1 o PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add_global])])
|> Theory.parent_path;
- in
- (thy'', char_thms)
- end;
+ in (thy3, eqn_thms') end;
+
+fun add_primrec args thy =
+ add_primrec_i (map (fn ((name, s), srcs) =>
+ ((name, Sign.simple_read_term (sign_of thy) propT s), map (Attrib.global_attribute thy) srcs))
+ args) thy;
+
+
+(* outer syntax *)
-fun add_primrec eqns thy =
- add_primrec_i (map (apsnd (Sign.simple_read_term (sign_of thy) propT)) eqns) thy;
+local structure P = OuterParse and K = OuterSyntax.Keyword in
+
+val primrec_decl = Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment);
+
+val primrecP =
+ OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
+ (primrec_decl >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
+
+val _ = OuterSyntax.add_parsers [primrecP];
end;
+
+end;
--- a/src/ZF/thy_syntax.ML Wed Nov 14 18:46:07 2001 +0100
+++ b/src/ZF/thy_syntax.ML Wed Nov 14 18:46:30 2001 +0100
@@ -10,19 +10,18 @@
open ThyParse;
-(*ML identifiers for introduction rules.*)
-fun mk_intr_name suffix s =
+fun mk_bind suffix s =
if ThmDatabase.is_ml_identifier s then
- "op " ^ s ^ suffix (*the "op" cancels any infix status*)
+ "op " ^ s ^ suffix (*the "op" cancels any infix status*)
else "_"; (*bad name, don't try to bind*)
(*For lists of theorems. Either a string (an ML list expression) or else
a list of identifiers.*)
-fun optlist s =
- optional (s $$--
- (string >> unenclose
- || list1 (name>>unenclose) >> mk_list))
+fun optlist s =
+ optional (s $$--
+ (string >> unenclose
+ || list1 (name>>unenclose) >> mk_list))
"[]";
(*Skipping initial blanks, find the first identifier*) (* FIXME slightly broken! *)
@@ -33,42 +32,43 @@
(Scan.any Symbol.is_blank |-- Syntax.scan_id)))
|> #1;
-(*(Co)Inductive definitions theory section."*)
+
+(* (Co)Inductive definitions *)
+
fun inductive_decl coind =
- let
- fun mk_params ((((((recs, sdom_sum), ipairs),
+ let
+ fun mk_params ((((((recs, sdom_sum), ipairs),
monos), con_defs), type_intrs), type_elims) =
- let val big_rec_name = space_implode "_"
+ let val big_rec_name = space_implode "_"
(map (scan_to_id o unenclose) recs)
and srec_tms = mk_list recs
and sintrs =
mk_big_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) ipairs)
- and inames = mk_list (map (mk_intr_name "" o fst) ipairs)
+ and inames = mk_list (map (mk_bind "" o fst) ipairs)
in
- ";\n\n\
- \local\n\
- \val (thy, {defs, intrs, elim, mk_cases, \
- \bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\
- \ " ^
- (if coind then "Co" else "") ^
- "Ind_Package.add_inductive_x (" ^ srec_tms ^ ", " ^ sdom_sum ^ ") " ^
- sintrs ^ " (" ^ monos ^ ", " ^ con_defs ^ ", " ^
- type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
- \in\n\
- \structure " ^ big_rec_name ^ " =\n\
- \struct\n\
- \ val defs = defs\n\
- \ val bnd_mono = bnd_mono\n\
- \ val dom_subset = dom_subset\n\
- \ val intrs = intrs\n\
- \ val elim = elim\n\
- \ val " ^ (if coind then "co" else "") ^ "induct = induct\n\
- \ val mutual_induct = mutual_induct\n\
- \ val mk_cases = mk_cases\n\
- \ val " ^ inames ^ " = intrs\n\
- \end;\n\
- \val thy = thy;\nend;\n\
- \val thy = thy\n"
+ ";\n\n\
+ \local\n\
+ \val (thy, {defs, intrs, elim, mk_cases, \
+ \bnd_mono, dom_subset, induct, mutual_induct, ...}) =\n\
+ \ " ^
+ (if coind then "Co" else "") ^
+ "Ind_Package.add_inductive_x (" ^ srec_tms ^ ", " ^ sdom_sum ^ ") " ^ sintrs ^
+ " (" ^ monos ^ ", " ^ con_defs ^ ", " ^ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
+ \in\n\
+ \structure " ^ big_rec_name ^ " =\n\
+ \struct\n\
+ \ val defs = defs\n\
+ \ val bnd_mono = bnd_mono\n\
+ \ val dom_subset = dom_subset\n\
+ \ val intrs = intrs\n\
+ \ val elim = elim\n\
+ \ val " ^ (if coind then "co" else "") ^ "induct = induct\n\
+ \ val mutual_induct = mutual_induct\n\
+ \ val mk_cases = mk_cases\n\
+ \ val " ^ inames ^ " = intrs\n\
+ \end;\n\
+ \val thy = thy;\nend;\n\
+ \val thy = thy\n"
end
val domains = "domains" $$-- enum1 "+" string --$$ "<=" -- !! string
val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
@@ -78,54 +78,53 @@
end;
-(*Datatype definitions theory section. co is true for codatatypes*)
+(* Datatype definitions *)
+
fun datatype_decl coind =
let
- (*generate strings*)
fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z);
val mk_data = mk_list o map mk_const o snd
val mk_scons = mk_big_list o map mk_data
fun mk_params ((((sdom, rec_pairs), monos), type_intrs), type_elims) =
let val rec_names = map (scan_to_id o unenclose o fst) rec_pairs
- val big_rec_name = space_implode "_" rec_names
- and srec_tms = mk_list (map fst rec_pairs)
- and scons = mk_scons rec_pairs
- val con_names = flat (map (map (unenclose o #1 o #1) o snd)
- rec_pairs)
- val inames = mk_list (map (mk_intr_name "_I") con_names)
+ val big_rec_name = space_implode "_" rec_names
+ and srec_tms = mk_list (map fst rec_pairs)
+ and scons = mk_scons rec_pairs
+ val con_names = flat (map (map (unenclose o #1 o #1) o snd)
+ rec_pairs)
+ val inames = mk_list (map (mk_bind "_I") con_names)
in
- ";\n\n\
- \local\n\
- \val (thy,\n\
+ ";\n\n\
+ \local\n\
+ \val (thy,\n\
\ {defs, intrs, elim, mk_cases, \
- \bnd_mono, dom_subset, induct, mutual_induct, ...},\n\
+ \bnd_mono, dom_subset, induct, mutual_induct, ...},\n\
\ {con_defs, case_eqns, recursor_eqns, free_iffs, free_SEs, mk_free, ...}) =\n\
- \ " ^
- (if coind then "Co" else "") ^
- "Data_Package.add_datatype (" ^ sdom ^ ", " ^ srec_tms ^ ", " ^
- scons ^ ", " ^ monos ^ ", " ^
- type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
- \in\n\
- \structure " ^ big_rec_name ^ " =\n\
- \struct\n\
- \ val defs = defs\n\
- \ val bnd_mono = bnd_mono\n\
- \ val dom_subset = dom_subset\n\
- \ val intrs = intrs\n\
- \ val elim = elim\n\
- \ val " ^ (if coind then "co" else "") ^ "induct = induct\n\
- \ val mutual_induct = mutual_induct\n\
- \ val mk_cases = mk_cases\n\
- \ val con_defs = con_defs\n\
- \ val case_eqns = case_eqns\n\
- \ val recursor_eqns = recursor_eqns\n\
- \ val free_iffs = free_iffs\n\
- \ val free_SEs = free_SEs\n\
- \ val mk_free = mk_free\n\
- \ val " ^ inames ^ " = intrs;\n\
- \end;\n\
- \val thy = thy;\nend;\n\
- \val thy = thy\n"
+ \ " ^
+ (if coind then "Co" else "") ^
+ "Data_Package.add_datatype_x (" ^ sdom ^ ", " ^ srec_tms ^ ") " ^ scons ^
+ " (" ^ monos ^ ", " ^ type_intrs ^ ", " ^ type_elims ^ ") thy;\n\
+ \in\n\
+ \structure " ^ big_rec_name ^ " =\n\
+ \struct\n\
+ \ val defs = defs\n\
+ \ val bnd_mono = bnd_mono\n\
+ \ val dom_subset = dom_subset\n\
+ \ val intrs = intrs\n\
+ \ val elim = elim\n\
+ \ val " ^ (if coind then "co" else "") ^ "induct = induct\n\
+ \ val mutual_induct = mutual_induct\n\
+ \ val mk_cases = mk_cases\n\
+ \ val con_defs = con_defs\n\
+ \ val case_eqns = case_eqns\n\
+ \ val recursor_eqns = recursor_eqns\n\
+ \ val free_iffs = free_iffs\n\
+ \ val free_SEs = free_SEs\n\
+ \ val mk_free = mk_free\n\
+ \ val " ^ inames ^ " = intrs;\n\
+ \end;\n\
+ \val thy = thy;\nend;\n\
+ \val thy = thy\n"
end
val string_list = "(" $$-- list1 string --$$ ")" || ThyParse.empty;
val construct = name -- string_list -- opt_mixfix;
@@ -136,6 +135,7 @@
end;
+
(** rep_datatype **)
fun mk_rep_dt_string (((elim, induct), case_eqns), recursor_eqns) =
@@ -143,27 +143,25 @@
mk_list case_eqns ^ " " ^ mk_list recursor_eqns;
val rep_datatype_decl =
- (("elim" $$-- ident) --
+ (("elim" $$-- ident) --
("induct" $$-- ident) --
- ("case_eqns" $$-- list1 ident) --
+ ("case_eqns" $$-- list1 ident) --
optional ("recursor_eqns" $$-- list1 ident) []) >> mk_rep_dt_string;
+
(** primrec **)
fun mk_primrec_decl eqns =
- let val names = map fst eqns
- in
- ";\nval (thy, " ^ mk_list names ^
- ") = PrimrecPackage.add_primrec " ^
- mk_list (map mk_pair (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
+ let val binds = map (mk_bind "" o fst) eqns in
+ ";\nval (thy, " ^ mk_list binds ^ ") = PrimrecPackage.add_primrec " ^
+ mk_list (map (fn p => mk_pair (mk_pair p, "[]")) (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
\val thy = thy\n"
end;
(* either names and axioms or just axioms *)
-val primrec_decl =
- ((repeat1 ((ident -- string) || (string >> pair "_")))) >> mk_primrec_decl;
-
+val primrec_decl =
+ ((repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl;