separate structure Typedecl;
authorwenzelm
Sun Mar 07 12:47:02 2010 +0100 (2010-03-07)
changeset 3562606197484c6ad
parent 35625 9c818cab0dd0
child 35627 6cec06ef67a7
separate structure Typedecl;
src/HOL/Boogie/Tools/boogie_loader.ML
src/HOL/Tools/typedef.ML
src/Pure/IsaMakefile
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/typedecl.ML
src/Pure/ROOT.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Mar 07 12:19:47 2010 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Mar 07 12:47:02 2010 +0100
     1.3 @@ -88,7 +88,7 @@
     1.4            let
     1.5              val args = Name.variant_list [] (replicate arity "'")
     1.6              val (T, thy') =
     1.7 -              Object_Logic.typedecl (Binding.name isa_name, args, mk_syntax name arity) thy
     1.8 +              Typedecl.typedecl (Binding.name isa_name, args, mk_syntax name arity) thy
     1.9              val type_name = fst (Term.dest_Type T)
    1.10            in (((name, type_name), log_new name type_name), thy') end)
    1.11      end
     2.1 --- a/src/HOL/Tools/typedef.ML	Sun Mar 07 12:19:47 2010 +0100
     2.2 +++ b/src/HOL/Tools/typedef.ML	Sun Mar 07 12:47:02 2010 +0100
     2.3 @@ -130,7 +130,7 @@
     2.4            in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
     2.5  
     2.6      fun typedef_result inhabited =
     2.7 -      Object_Logic.typedecl (tname, vs, mx)
     2.8 +      Typedecl.typedecl (tname, vs, mx)
     2.9        #> snd
    2.10        #> Sign.add_consts_i
    2.11          [(Rep_name, newT --> oldT, NoSyn),
     3.1 --- a/src/Pure/IsaMakefile	Sun Mar 07 12:19:47 2010 +0100
     3.2 +++ b/src/Pure/IsaMakefile	Sun Mar 07 12:47:02 2010 +0100
     3.3 @@ -72,18 +72,19 @@
     3.4    Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML		\
     3.5    Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML			\
     3.6    Isar/spec_parse.ML Isar/spec_rules.ML Isar/specification.ML		\
     3.7 -  Isar/theory_target.ML Isar/toplevel.ML Isar/value_parse.ML		\
     3.8 -  ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML	\
     3.9 -  ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML		\
    3.10 -  ML/ml_syntax.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML		\
    3.11 -  ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML		\
    3.12 -  Proof/extraction.ML Proof/proof_rewrite_rules.ML			\
    3.13 -  Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML	\
    3.14 -  ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML			\
    3.15 -  ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML		\
    3.16 -  ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML		\
    3.17 -  ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML			\
    3.18 -  ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML	\
    3.19 +  Isar/theory_target.ML Isar/toplevel.ML Isar/typedecl.ML		\
    3.20 +  Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_compiler.ML		\
    3.21 +  ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML		\
    3.22 +  ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML		\
    3.23 +  ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML	\
    3.24 +  ML-Systems/use_context.ML Proof/extraction.ML				\
    3.25 +  Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
    3.26 +  Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML	\
    3.27 +  ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML		\
    3.28 +  ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML		\
    3.29 +  ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML		\
    3.30 +  ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML		\
    3.31 +  ProofGeneral/proof_general_emacs.ML					\
    3.32    ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML	\
    3.33    Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML			\
    3.34    Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML		\
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Mar 07 12:19:47 2010 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 07 12:47:02 2010 +0100
     4.3 @@ -105,7 +105,7 @@
     4.4  val _ =
     4.5    OuterSyntax.command "typedecl" "type declaration" K.thy_decl
     4.6      (P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) =>
     4.7 -      Toplevel.theory (Object_Logic.typedecl (a, args, mx) #> snd)));
     4.8 +      Toplevel.theory (Typedecl.typedecl (a, args, mx) #> snd)));
     4.9  
    4.10  val _ =
    4.11    OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
     5.1 --- a/src/Pure/Isar/object_logic.ML	Sun Mar 07 12:19:47 2010 +0100
     5.2 +++ b/src/Pure/Isar/object_logic.ML	Sun Mar 07 12:47:02 2010 +0100
     5.3 @@ -8,7 +8,6 @@
     5.4  sig
     5.5    val get_base_sort: theory -> sort option
     5.6    val add_base_sort: sort -> theory -> theory
     5.7 -  val typedecl: binding * string list * mixfix -> theory -> typ * theory
     5.8    val add_judgment: binding * typ * mixfix -> theory -> theory
     5.9    val add_judgment_cmd: binding * string * mixfix -> theory -> theory
    5.10    val judgment_name: theory -> string
    5.11 @@ -82,24 +81,6 @@
    5.12    else (SOME S, judgment, atomize_rulify));
    5.13  
    5.14  
    5.15 -(* typedecl *)
    5.16 -
    5.17 -fun typedecl (b, vs, mx) thy =
    5.18 -  let
    5.19 -    val base_sort = get_base_sort thy;
    5.20 -    val _ = has_duplicates (op =) vs andalso
    5.21 -      error ("Duplicate parameters in type declaration " ^ quote (Binding.str_of b));
    5.22 -    val name = Sign.full_name thy b;
    5.23 -    val n = length vs;
    5.24 -    val T = Type (name, map (fn v => TFree (v, [])) vs);
    5.25 -  in
    5.26 -    thy
    5.27 -    |> Sign.add_types [(b, n, mx)]
    5.28 -    |> (case base_sort of NONE => I | SOME S => AxClass.axiomatize_arity (name, replicate n S, S))
    5.29 -    |> pair T
    5.30 -  end;
    5.31 -
    5.32 -
    5.33  (* add judgment *)
    5.34  
    5.35  local
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/Isar/typedecl.ML	Sun Mar 07 12:47:02 2010 +0100
     6.3 @@ -0,0 +1,31 @@
     6.4 +(*  Title:      Pure/Isar/typedecl.ML
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Type declarations (within the object logic).
     6.8 +*)
     6.9 +
    6.10 +signature TYPEDECL =
    6.11 +sig
    6.12 +  val typedecl: binding * string list * mixfix -> theory -> typ * theory
    6.13 +end;
    6.14 +
    6.15 +structure Typedecl: TYPEDECL =
    6.16 +struct
    6.17 +
    6.18 +fun typedecl (b, vs, mx) thy =
    6.19 +  let
    6.20 +    val base_sort = Object_Logic.get_base_sort thy;
    6.21 +    val _ = has_duplicates (op =) vs andalso
    6.22 +      error ("Duplicate parameters in type declaration " ^ quote (Binding.str_of b));
    6.23 +    val name = Sign.full_name thy b;
    6.24 +    val n = length vs;
    6.25 +    val T = Type (name, map (fn v => TFree (v, [])) vs);
    6.26 +  in
    6.27 +    thy
    6.28 +    |> Sign.add_types [(b, n, mx)]
    6.29 +    |> (case base_sort of NONE => I | SOME S => AxClass.axiomatize_arity (name, replicate n S, S))
    6.30 +    |> pair T
    6.31 +  end;
    6.32 +
    6.33 +end;
    6.34 +
     7.1 --- a/src/Pure/ROOT.ML	Sun Mar 07 12:19:47 2010 +0100
     7.2 +++ b/src/Pure/ROOT.ML	Sun Mar 07 12:47:02 2010 +0100
     7.3 @@ -218,6 +218,7 @@
     7.4  use "Isar/spec_parse.ML";
     7.5  use "Isar/spec_rules.ML";
     7.6  use "Isar/specification.ML";
     7.7 +use "Isar/typedecl.ML";
     7.8  use "Isar/constdefs.ML";
     7.9  
    7.10  (*toplevel transactions*)