separated typedecl module, providing typedecl command with interpretation
authorhaftmann
Fri Nov 23 21:09:30 2007 +0100 (2007-11-23)
changeset 25458ba8f5e4fa336
parent 25457 ba2bcae7aafd
child 25459 d1dce7d0731c
separated typedecl module, providing typedecl command with interpretation
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/typedef_package.ML
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/sign.ML
src/Pure/typedecl.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Nov 23 17:37:56 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Nov 23 21:09:30 2007 +0100
     1.3 @@ -557,7 +557,7 @@
     1.4      val thy2' = thy
     1.5  
     1.6        (** new types **)
     1.7 -      |> fold2 (fn (name, mx) => fn tvs => TypedefPackage.add_typedecls [(name, tvs, mx)])
     1.8 +      |> fold2 (fn (name, mx) => fn tvs => Typedecl.add (name, tvs, mx) #> snd)
     1.9             types_syntax tyvars
    1.10        |> add_path flat_names (space_implode "_" new_type_names)
    1.11  
     2.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Nov 23 17:37:56 2007 +0100
     2.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri Nov 23 21:09:30 2007 +0100
     2.3 @@ -9,7 +9,6 @@
     2.4  signature TYPEDEF_PACKAGE =
     2.5  sig
     2.6    val quiet_mode: bool ref
     2.7 -  val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
     2.8    type info =
     2.9     {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
    2.10      type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
    2.11 @@ -45,20 +44,6 @@
    2.12  
    2.13  
    2.14  
    2.15 -(** type declarations **)
    2.16 -
    2.17 -fun HOL_arity (raw_name, args, mx) thy =
    2.18 -  thy |> AxClass.axiomatize_arity
    2.19 -    (Sign.full_name thy (Syntax.type_name raw_name mx),
    2.20 -      replicate (length args) HOLogic.typeS, HOLogic.typeS);
    2.21 -
    2.22 -fun add_typedecls decls thy =
    2.23 -  if can (Theory.assert_super HOL.thy) thy then
    2.24 -    thy |> Sign.add_typedecls decls |> fold HOL_arity decls
    2.25 -  else thy |> Sign.add_typedecls decls;
    2.26 -
    2.27 -
    2.28 -
    2.29  (** type definitions **)
    2.30  
    2.31  (* messages *)
    2.32 @@ -150,7 +135,8 @@
    2.33        else (NONE, thy);
    2.34  
    2.35      fun typedef_result nonempty =
    2.36 -      add_typedecls [(t, vs, mx)]
    2.37 +      Typedecl.add (t, vs, mx)
    2.38 +      #> snd
    2.39        #> Sign.add_consts_i
    2.40         ((if def then [(name, setT', NoSyn)] else []) @
    2.41          [(Rep_name, newT --> oldT, NoSyn),
    2.42 @@ -275,12 +261,6 @@
    2.43  
    2.44  val _ = OuterSyntax.keywords ["morphisms"];
    2.45  
    2.46 -val _ =
    2.47 -  OuterSyntax.command "typedecl" "type declaration (HOL)" K.thy_decl
    2.48 -    (P.type_args -- P.name -- P.opt_infix >> (fn ((vs, t), mx) =>
    2.49 -      Toplevel.theory (add_typedecls [(t, vs, mx)])));
    2.50 -
    2.51 -
    2.52  val typedef_decl =
    2.53    Scan.optional (P.$$$ "(" |--
    2.54        ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
     3.1 --- a/src/Pure/IsaMakefile	Fri Nov 23 17:37:56 2007 +0100
     3.2 +++ b/src/Pure/IsaMakefile	Fri Nov 23 21:09:30 2007 +0100
     3.3 @@ -73,7 +73,7 @@
     3.4    morphism.ML name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML		\
     3.5    proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML	\
     3.6    sorts.ML subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML theory.ML	\
     3.7 -  thm.ML type.ML type_infer.ML unify.ML variable.ML
     3.8 +  thm.ML type.ML typedecl.ML type_infer.ML unify.ML variable.ML
     3.9  	@./mk
    3.10  
    3.11  
     4.1 --- a/src/Pure/ROOT.ML	Fri Nov 23 17:37:56 2007 +0100
     4.2 +++ b/src/Pure/ROOT.ML	Fri Nov 23 21:09:30 2007 +0100
     4.3 @@ -74,6 +74,7 @@
     4.4  use "conjunction.ML";
     4.5  use "assumption.ML";
     4.6  use "goal.ML";
     4.7 +use "typedecl.ML";
     4.8  use "axclass.ML";
     4.9  
    4.10  (*proof term operations*)
     5.1 --- a/src/Pure/sign.ML	Fri Nov 23 17:37:56 2007 +0100
     5.2 +++ b/src/Pure/sign.ML	Fri Nov 23 21:09:30 2007 +0100
     5.3 @@ -11,7 +11,6 @@
     5.4    val add_defsort: string -> theory -> theory
     5.5    val add_defsort_i: sort -> theory -> theory
     5.6    val add_types: (bstring * int * mixfix) list -> theory -> theory
     5.7 -  val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
     5.8    val add_nonterminals: bstring list -> theory -> theory
     5.9    val add_tyabbrs: (bstring * string list * string * mixfix) list -> theory -> theory
    5.10    val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> theory -> theory
    5.11 @@ -591,13 +590,6 @@
    5.12      val tsig' = Type.add_types naming decls tsig;
    5.13    in (naming, syn', tsig', consts) end);
    5.14  
    5.15 -fun add_typedecls decls thy =
    5.16 -  let
    5.17 -    fun type_of (a, vs: string list, mx) =
    5.18 -      if not (has_duplicates (op =) vs) then (a, length vs, mx)
    5.19 -      else error ("Duplicate parameters in type declaration: " ^ quote a);
    5.20 -  in add_types (map type_of decls) thy end;
    5.21 -
    5.22  
    5.23  (* add nonterminals *)
    5.24  
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/typedecl.ML	Fri Nov 23 21:09:30 2007 +0100
     6.3 @@ -0,0 +1,35 @@
     6.4 +(*  Title:      Pure/typedecl.ML
     6.5 +    ID:         $Id$
     6.6 +    Author:     Florian Haftmann, TU Muenchen
     6.7 +
     6.8 +Primitive type declarations.
     6.9 +*)
    6.10 +
    6.11 +signature TYPEDECL =
    6.12 +sig
    6.13 +  val add: bstring * string list * mixfix -> theory -> typ * theory
    6.14 +  val interpretation: (string -> theory -> theory) -> theory -> theory
    6.15 +end
    6.16 +
    6.17 +structure Typedecl: TYPEDECL =
    6.18 +struct
    6.19 +
    6.20 +structure TypedeclInterpretation = InterpretationFun(type T = string val eq = op =);
    6.21 +val interpretation = TypedeclInterpretation.interpretation;
    6.22 +
    6.23 +val _ = Context.add_setup TypedeclInterpretation.init;
    6.24 +
    6.25 +fun add (a, vs : string list, mx) thy =
    6.26 +  let
    6.27 +    val no_typargs = if not (has_duplicates (op =) vs) then length vs
    6.28 +      else error ("Duplicate parameters in type declaration: " ^ quote a);
    6.29 +    val a' = Sign.full_name thy a;
    6.30 +    val T = Type (a', map (fn v => TFree (v, [])) vs);
    6.31 +  in
    6.32 +    thy
    6.33 +    |> Sign.add_types [(a, no_typargs, mx)]
    6.34 +    |> TypedeclInterpretation.data a'
    6.35 +    |> pair T
    6.36 +  end;
    6.37 +
    6.38 +end;