# HG changeset patch # User wenzelm # Date 1005759990 -3600 # Node ID c10cea75dd56e2440e433189ef6f12454132ce9a # Parent 3f820a21dcc16e6fed8671ef52b87c5304cccaba adapted primrec/datatype to Isar; diff -r 3f820a21dcc1 -r c10cea75dd56 src/ZF/Datatype.ML --- 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); diff -r 3f820a21dcc1 -r c10cea75dd56 src/ZF/Datatype.thy --- 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 - diff -r 3f820a21dcc1 -r c10cea75dd56 src/ZF/Inductive.thy --- 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" diff -r 3f820a21dcc1 -r c10cea75dd56 src/ZF/ROOT.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; diff -r 3f820a21dcc1 -r c10cea75dd56 src/ZF/Tools/datatype_package.ML --- 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.$$$ "\\" || 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; diff -r 3f820a21dcc1 -r c10cea75dd56 src/ZF/Tools/inductive_package.ML --- 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)]; diff -r 3f820a21dcc1 -r c10cea75dd56 src/ZF/Tools/primrec_package.ML --- 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; diff -r 3f820a21dcc1 -r c10cea75dd56 src/ZF/thy_syntax.ML --- 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;