unified arity parser/arguments;
authorwenzelm
Fri Feb 16 22:13:15 2007 +0100 (2007-02-16 ago)
changeset 223317df6bc8cf0b0
parent 22330 00ca68f5ce29
child 22332 3ddd31fa45fd
unified arity parser/arguments;
src/HOL/Tools/datatype_codegen.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Tools/class_package.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Feb 16 19:19:19 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Feb 16 22:13:15 2007 +0100
     1.3 @@ -25,11 +25,11 @@
     1.4    val the_codetypes_mut_specs: theory -> (string * bool) list
     1.5      -> ((string * sort) list * (string * (bool * (string * typ list) list)) list)
     1.6    val get_codetypes_arities: theory -> (string * bool) list -> sort
     1.7 -    -> (string * (((string * sort list) * sort) * term list)) list option
     1.8 +    -> (string * (arity * term list)) list option
     1.9    val prove_codetypes_arities: tactic -> (string * bool) list -> sort
    1.10 -    -> (((string * sort list) * sort) list -> (string * term list) list -> theory
    1.11 +    -> (arity list -> (string * term list) list -> theory
    1.12      -> ((bstring * Attrib.src list) * term) list * theory)
    1.13 -    -> (((string * sort list) * sort) list -> (string * term list) list -> theory -> theory)
    1.14 +    -> (arity list -> (string * term list) list -> theory -> theory)
    1.15      -> theory -> theory
    1.16  
    1.17    val setup: theory -> theory
    1.18 @@ -584,11 +584,10 @@
    1.19            (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) vs v))) tys
    1.20        in (c, tys') end;
    1.21      val css = map (fn (tyco, (_, cs)) => (tyco, (map (inst_type tyco) cs))) css_proto;
    1.22 -    fun mk_arity tyco =
    1.23 -      ((tyco, map snd vs), sort);
    1.24 +    fun mk_arity tyco = (tyco, map snd vs, sort);
    1.25      fun typ_of_sort ty =
    1.26        let
    1.27 -        val arities = map (fn (tyco, _) => ((tyco, map snd vs), sort)) css;
    1.28 +        val arities = map (fn (tyco, _) => (tyco, map snd vs, sort)) css;
    1.29        in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end;
    1.30      fun mk_cons tyco (c, tys) =
    1.31        let
    1.32 @@ -605,7 +604,7 @@
    1.33    case get_codetypes_arities thy tycos sort
    1.34     of NONE => thy
    1.35      | SOME insts => let
    1.36 -        fun proven ((tyco, asorts), sort) =
    1.37 +        fun proven (tyco, asorts, sort) =
    1.38            Sorts.of_sort (Sign.classes_of thy)
    1.39              (Type (tyco, map TFree (Name.names Name.context "'a" asorts)), sort);
    1.40          val (arities, css) = (split_list o map_filter
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Feb 16 19:19:19 2007 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Feb 16 22:13:15 2007 +0100
     2.3 @@ -113,8 +113,7 @@
     2.4  
     2.5  val aritiesP =
     2.6    OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
     2.7 -    (Scan.repeat1 (P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2)
     2.8 -      >> (Toplevel.theory o fold AxClass.axiomatize_arity));
     2.9 +    (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity));
    2.10  
    2.11  
    2.12  (* consts and syntax *)
    2.13 @@ -406,19 +405,13 @@
    2.14  
    2.15  local
    2.16  
    2.17 -val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes")
    2.18 -
    2.19  val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::);
    2.20  val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element);
    2.21  
    2.22 -val parse_arity =
    2.23 -  (P.xname --| P.$$$ "::" -- P.!!! P.arity)
    2.24 -    >> (fn (tyco, (asorts, sort)) => ((tyco, asorts), sort));
    2.25 -
    2.26  in
    2.27  
    2.28  val classP =
    2.29 -  OuterSyntax.command classK "define type class" K.thy_decl (
    2.30 +  OuterSyntax.command "class" "define type class" K.thy_decl (
    2.31      P.name --| P.$$$ "="
    2.32      -- (
    2.33        class_subP --| P.$$$ "+" -- class_bodyP
    2.34 @@ -430,17 +423,17 @@
    2.35            (ClassPackage.class_cmd bname supclasses elems #-> TheoryTarget.begin true)));
    2.36  
    2.37  val instanceP =
    2.38 -  OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
    2.39 +  OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((
    2.40        P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    2.41             >> ClassPackage.instance_class_cmd
    2.42        || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    2.43             >> ClassPackage.instance_sort_cmd (*experimental: by interpretation of locales*)
    2.44 -      || P.and_list1 parse_arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    2.45 +      || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    2.46             >> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs)
    2.47      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
    2.48  
    2.49  val print_classesP =
    2.50 -  OuterSyntax.improper_command print_classesK "print classes of this theory" K.diag
    2.51 +  OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
    2.52      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
    2.53        o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
    2.54  
     3.1 --- a/src/Pure/Isar/outer_parse.ML	Fri Feb 16 19:19:19 2007 +0100
     3.2 +++ b/src/Pure/Isar/outer_parse.ML	Fri Feb 16 22:13:15 2007 +0100
     3.3 @@ -55,7 +55,7 @@
     3.4    val path: token list -> Path.T * token list
     3.5    val parname: token list -> string * token list
     3.6    val sort: token list -> string * token list
     3.7 -  val arity: token list -> (string list * string) * token list
     3.8 +  val arity: token list -> (string * string list * string) * token list
     3.9    val type_args: token list -> string list * token list
    3.10    val typ: token list -> string * token list
    3.11    val mixfix: token list -> mixfix * token list
    3.12 @@ -202,7 +202,8 @@
    3.13  
    3.14  val sort = group "sort" xname;
    3.15  
    3.16 -val arity = Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort;
    3.17 +val arity = xname -- ($$$ "::" |-- !!!
    3.18 +  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
    3.19  
    3.20  
    3.21  (* types *)
     4.1 --- a/src/Pure/Tools/class_package.ML	Fri Feb 16 19:19:19 2007 +0100
     4.2 +++ b/src/Pure/Tools/class_package.ML	Fri Feb 16 22:13:15 2007 +0100
     4.3 @@ -13,13 +13,12 @@
     4.4      string * Proof.context
     4.5    val class_cmd: bstring -> string list -> Element.context Locale.element list -> theory ->
     4.6      string * Proof.context
     4.7 -  val instance_arity: ((bstring * sort list) * sort) list
     4.8 -    -> ((bstring * Attrib.src list) * term) list
     4.9 +  val instance_arity: arity list -> ((bstring * Attrib.src list) * term) list
    4.10      -> theory -> Proof.state
    4.11 -  val instance_arity_cmd: ((bstring * string list) * string) list
    4.12 +  val instance_arity_cmd: (bstring * string list * string) list
    4.13      -> ((bstring * Attrib.src list) * string) list
    4.14      -> theory -> Proof.state
    4.15 -  val prove_instance_arity: tactic -> ((string * sort list) * sort) list
    4.16 +  val prove_instance_arity: tactic -> arity list
    4.17      -> ((bstring * Attrib.src list) * term) list
    4.18      -> theory -> theory
    4.19    val instance_class: class * class -> theory -> Proof.state
    4.20 @@ -28,9 +27,7 @@
    4.21    val instance_sort_cmd: string * string -> theory -> Proof.state
    4.22    val prove_instance_sort: tactic -> class * sort -> theory -> theory
    4.23  
    4.24 -  val assume_arities_of_sort: theory -> ((string * sort list) * sort) list -> typ * sort -> bool
    4.25 -  val assume_arities_thy: theory -> ((string * sort list) * sort) list -> (theory -> 'a) -> 'a
    4.26 -    (*'a must not keep any reference to theory*)
    4.27 +  val assume_arities_of_sort: theory -> arity list -> typ * sort -> bool
    4.28  
    4.29    (* experimental class target *)
    4.30    val class_of_locale: theory -> string -> class option
    4.31 @@ -113,16 +110,10 @@
    4.32    let
    4.33      val pp = Sign.pp thy;
    4.34      val algebra = Sign.classes_of thy
    4.35 -      |> fold (fn ((tyco, asorts), sort) =>
    4.36 +      |> fold (fn (tyco, asorts, sort) =>
    4.37             Sorts.add_arities pp (tyco, map (fn class => (class, asorts)) sort)) arities;
    4.38    in Sorts.of_sort algebra ty_sort end;
    4.39  
    4.40 -fun assume_arities_thy thy arities f =
    4.41 -  let
    4.42 -    val thy_read = (fold (fn ((tyco, asorts), sort)
    4.43 -      => Sign.primitive_arity (tyco, asorts, sort)) arities o Theory.copy) thy
    4.44 -  in f thy_read end;
    4.45 -
    4.46  
    4.47  (* instances with implicit parameter handling *)
    4.48  
    4.49 @@ -144,9 +135,7 @@
    4.50  
    4.51  fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs theory =
    4.52    let
    4.53 -    fun prep_arity' ((tyco, asorts), sort) = prep_arity theory (tyco, asorts, sort);
    4.54 -    val arities = map prep_arity' raw_arities;
    4.55 -    val arities_pair = map (fn (tyco, asorts, sort) => ((tyco, asorts), sort)) arities;
    4.56 +    val arities = map (prep_arity theory) raw_arities;
    4.57      val _ = if null arities then error "at least one arity must be given" else ();
    4.58      val _ = case (duplicates (op =) o map #1) arities
    4.59       of [] => ()
    4.60 @@ -187,7 +176,9 @@
    4.61                | SOME norm => map_types norm t
    4.62            in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;
    4.63        in fold_map read defs cs end;
    4.64 -    val (defs, _) = assume_arities_thy theory arities_pair (read_defs raw_defs cs);
    4.65 +    val (defs, _) = read_defs raw_defs cs
    4.66 +      (fold Sign.primitive_arity arities (Theory.copy theory));
    4.67 +
    4.68      fun get_remove_contraint c thy =
    4.69        let
    4.70          val ty = Sign.the_const_constraint thy c;
    4.71 @@ -272,7 +263,7 @@
    4.72  
    4.73  val ancestry = Graph.all_succs o fst o ClassData.get;
    4.74  
    4.75 -fun param_map thy = 
    4.76 +fun param_map thy =
    4.77    let
    4.78      fun params thy class =
    4.79        let