# HG changeset patch # User wenzelm # Date 1171660395 -3600 # Node ID 7df6bc8cf0b027fa4a35ad5c6789aed8e140d8fd # Parent 00ca68f5ce29ae8f0eab2c015f961296093fa18c unified arity parser/arguments; diff -r 00ca68f5ce29 -r 7df6bc8cf0b0 src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Fri Feb 16 19:19:19 2007 +0100 +++ b/src/HOL/Tools/datatype_codegen.ML Fri Feb 16 22:13:15 2007 +0100 @@ -25,11 +25,11 @@ val the_codetypes_mut_specs: theory -> (string * bool) list -> ((string * sort) list * (string * (bool * (string * typ list) list)) list) val get_codetypes_arities: theory -> (string * bool) list -> sort - -> (string * (((string * sort list) * sort) * term list)) list option + -> (string * (arity * term list)) list option val prove_codetypes_arities: tactic -> (string * bool) list -> sort - -> (((string * sort list) * sort) list -> (string * term list) list -> theory + -> (arity list -> (string * term list) list -> theory -> ((bstring * Attrib.src list) * term) list * theory) - -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> theory) + -> (arity list -> (string * term list) list -> theory -> theory) -> theory -> theory val setup: theory -> theory @@ -584,11 +584,10 @@ (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) vs v))) tys in (c, tys') end; val css = map (fn (tyco, (_, cs)) => (tyco, (map (inst_type tyco) cs))) css_proto; - fun mk_arity tyco = - ((tyco, map snd vs), sort); + fun mk_arity tyco = (tyco, map snd vs, sort); fun typ_of_sort ty = let - val arities = map (fn (tyco, _) => ((tyco, map snd vs), sort)) css; + val arities = map (fn (tyco, _) => (tyco, map snd vs, sort)) css; in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end; fun mk_cons tyco (c, tys) = let @@ -605,7 +604,7 @@ case get_codetypes_arities thy tycos sort of NONE => thy | SOME insts => let - fun proven ((tyco, asorts), sort) = + fun proven (tyco, asorts, sort) = Sorts.of_sort (Sign.classes_of thy) (Type (tyco, map TFree (Name.names Name.context "'a" asorts)), sort); val (arities, css) = (split_list o map_filter diff -r 00ca68f5ce29 -r 7df6bc8cf0b0 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Fri Feb 16 19:19:19 2007 +0100 +++ b/src/Pure/Isar/isar_syn.ML Fri Feb 16 22:13:15 2007 +0100 @@ -113,8 +113,7 @@ val aritiesP = OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl - (Scan.repeat1 (P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2) - >> (Toplevel.theory o fold AxClass.axiomatize_arity)); + (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity)); (* consts and syntax *) @@ -406,19 +405,13 @@ local -val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes") - val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::); val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element); -val parse_arity = - (P.xname --| P.$$$ "::" -- P.!!! P.arity) - >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort)); - in val classP = - OuterSyntax.command classK "define type class" K.thy_decl ( + OuterSyntax.command "class" "define type class" K.thy_decl ( P.name --| P.$$$ "=" -- ( class_subP --| P.$$$ "+" -- class_bodyP @@ -430,17 +423,17 @@ (ClassPackage.class_cmd bname supclasses elems #-> TheoryTarget.begin true))); val instanceP = - OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal (( + OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal (( P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) >> ClassPackage.instance_class_cmd || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) >> ClassPackage.instance_sort_cmd (*experimental: by interpretation of locales*) - || P.and_list1 parse_arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop) + || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop) >> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs) ) >> (Toplevel.print oo Toplevel.theory_to_proof)); val print_classesP = - OuterSyntax.improper_command print_classesK "print classes of this theory" K.diag + OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of))); diff -r 00ca68f5ce29 -r 7df6bc8cf0b0 src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Fri Feb 16 19:19:19 2007 +0100 +++ b/src/Pure/Isar/outer_parse.ML Fri Feb 16 22:13:15 2007 +0100 @@ -55,7 +55,7 @@ val path: token list -> Path.T * token list val parname: token list -> string * token list val sort: token list -> string * token list - val arity: token list -> (string list * string) * token list + val arity: token list -> (string * string list * string) * token list val type_args: token list -> string list * token list val typ: token list -> string * token list val mixfix: token list -> mixfix * token list @@ -202,7 +202,8 @@ val sort = group "sort" xname; -val arity = Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort; +val arity = xname -- ($$$ "::" |-- !!! + (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2; (* types *) diff -r 00ca68f5ce29 -r 7df6bc8cf0b0 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Fri Feb 16 19:19:19 2007 +0100 +++ b/src/Pure/Tools/class_package.ML Fri Feb 16 22:13:15 2007 +0100 @@ -13,13 +13,12 @@ string * Proof.context val class_cmd: bstring -> string list -> Element.context Locale.element list -> theory -> string * Proof.context - val instance_arity: ((bstring * sort list) * sort) list - -> ((bstring * Attrib.src list) * term) list + val instance_arity: arity list -> ((bstring * Attrib.src list) * term) list -> theory -> Proof.state - val instance_arity_cmd: ((bstring * string list) * string) list + val instance_arity_cmd: (bstring * string list * string) list -> ((bstring * Attrib.src list) * string) list -> theory -> Proof.state - val prove_instance_arity: tactic -> ((string * sort list) * sort) list + val prove_instance_arity: tactic -> arity list -> ((bstring * Attrib.src list) * term) list -> theory -> theory val instance_class: class * class -> theory -> Proof.state @@ -28,9 +27,7 @@ val instance_sort_cmd: string * string -> theory -> Proof.state val prove_instance_sort: tactic -> class * sort -> theory -> theory - val assume_arities_of_sort: theory -> ((string * sort list) * sort) list -> typ * sort -> bool - val assume_arities_thy: theory -> ((string * sort list) * sort) list -> (theory -> 'a) -> 'a - (*'a must not keep any reference to theory*) + val assume_arities_of_sort: theory -> arity list -> typ * sort -> bool (* experimental class target *) val class_of_locale: theory -> string -> class option @@ -113,16 +110,10 @@ let val pp = Sign.pp thy; val algebra = Sign.classes_of thy - |> fold (fn ((tyco, asorts), sort) => + |> 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 assume_arities_thy thy arities f = - let - val thy_read = (fold (fn ((tyco, asorts), sort) - => Sign.primitive_arity (tyco, asorts, sort)) arities o Theory.copy) thy - in f thy_read end; - (* instances with implicit parameter handling *) @@ -144,9 +135,7 @@ fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs theory = let - fun prep_arity' ((tyco, asorts), sort) = prep_arity theory (tyco, asorts, sort); - val arities = map prep_arity' raw_arities; - val arities_pair = map (fn (tyco, asorts, sort) => ((tyco, asorts), sort)) arities; + val arities = map (prep_arity theory) raw_arities; val _ = if null arities then error "at least one arity must be given" else (); val _ = case (duplicates (op =) o map #1) arities of [] => () @@ -187,7 +176,9 @@ | SOME norm => map_types norm t in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end; in fold_map read defs cs end; - val (defs, _) = assume_arities_thy theory arities_pair (read_defs raw_defs cs); + 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; @@ -272,7 +263,7 @@ val ancestry = Graph.all_succs o fst o ClassData.get; -fun param_map thy = +fun param_map thy = let fun params thy class = let