src/Pure/Isar/specification.ML
author wenzelm
Sat, 21 Jan 2006 23:02:14 +0100
changeset 18728 6790126ab5f6
parent 18670 c3f445b92aff
child 18771 63efe00371af
permissions -rw-r--r--
simplified type attribute;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/specification.ML
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
     4
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
     5
Theory specifications --- with type-inference, but no internal
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
     6
polymorphism.
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
     7
*)
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
     8
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
     9
signature SPECIFICATION =
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    10
sig
18640
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    11
  val pretty_consts: Proof.context -> (string * typ) list -> Pretty.T
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    12
  val read_specification:
18640
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    13
    (string * string option * mixfix) list *
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    14
      ((string * Attrib.src list) * string list) list -> Proof.context ->
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    15
    ((string * typ * mixfix) list *
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18670
diff changeset
    16
      ((string * attribute list) * term list) list) * Proof.context
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    17
  val cert_specification:
18640
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    18
    (string * typ option * mixfix) list *
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18670
diff changeset
    19
      ((string * attribute list) * term list) list -> Proof.context ->
18640
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    20
    ((string * typ * mixfix) list *
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18670
diff changeset
    21
      ((string * attribute list) * term list) list) * Proof.context
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    22
  val axiomatize:
18640
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    23
    (string * string option * mixfix) list *
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    24
      ((bstring * Attrib.src list) * string list) list -> theory -> thm list list * theory
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    25
  val axiomatize_i:
18640
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    26
    (string * typ option * mixfix) list *
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18670
diff changeset
    27
      ((bstring * attribute list) * term list) list -> theory ->
18640
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    28
    thm list list * theory
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    29
end;
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    30
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    31
structure Specification: SPECIFICATION =
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    32
struct
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    33
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    34
(* pretty_consts *)
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    35
18640
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    36
fun pretty_const ctxt (c, T) =
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    37
  Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
18640
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    38
    Pretty.quote (ProofContext.pretty_typ ctxt T)];
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    39
18640
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    40
fun pretty_consts ctxt decls =
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    41
  Pretty.big_list "constants" (map (pretty_const ctxt) decls);
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    42
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    43
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    44
(* prepare specification *)
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    45
18670
c3f445b92aff uniform handling of fixes;
wenzelm
parents: 18640
diff changeset
    46
fun prep_specification prep_vars prep_propp prep_att
c3f445b92aff uniform handling of fixes;
wenzelm
parents: 18640
diff changeset
    47
    (raw_vars, raw_specs) ctxt =
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    48
  let
18670
c3f445b92aff uniform handling of fixes;
wenzelm
parents: 18640
diff changeset
    49
    val thy = ProofContext.theory_of ctxt;
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    50
18670
c3f445b92aff uniform handling of fixes;
wenzelm
parents: 18640
diff changeset
    51
    val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
c3f445b92aff uniform handling of fixes;
wenzelm
parents: 18640
diff changeset
    52
    val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
c3f445b92aff uniform handling of fixes;
wenzelm
parents: 18640
diff changeset
    53
    val ((specs, vs), specs_ctxt) =
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    54
      prep_propp (params_ctxt, map (map (rpair ([], [])) o snd) raw_specs)
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    55
      |> swap |>> map (map fst)
18670
c3f445b92aff uniform handling of fixes;
wenzelm
parents: 18640
diff changeset
    56
      ||>> fold_map ProofContext.inferred_type xs;
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    57
18670
c3f445b92aff uniform handling of fixes;
wenzelm
parents: 18640
diff changeset
    58
    val params = map2 (fn (x, T) => fn (_, _, mx) => (x, T, mx)) vs vars;
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    59
    val names = map (fst o fst) raw_specs;
18670
c3f445b92aff uniform handling of fixes;
wenzelm
parents: 18640
diff changeset
    60
    val atts = map (map (prep_att thy) o snd o fst) raw_specs;
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    61
  in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end;
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    62
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    63
fun read_specification x =
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18670
diff changeset
    64
  prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.attribute x;
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    65
fun cert_specification x =
18670
c3f445b92aff uniform handling of fixes;
wenzelm
parents: 18640
diff changeset
    66
  prep_specification ProofContext.cert_vars ProofContext.cert_propp (K I) x;
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    67
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    68
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    69
(* axiomatize *)
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    70
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    71
fun gen_axiomatize prep args thy =
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    72
  let
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    73
    val ((consts, specs), ctxt) = prep args (ProofContext.init thy);
18640
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    74
    val subst = consts |> map (fn (x, T, _) => (Free (x, T), Const (Sign.full_name thy x, T)));
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    75
    val axioms = specs |> map (fn ((name, att), ts) =>
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18670
diff changeset
    76
      ((name, map (Term.subst_atomic subst) ts), att));
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    77
    val (thms, thy') =
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    78
      thy
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    79
      |> Theory.add_consts_i consts
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    80
      |> PureThy.add_axiomss_i axioms
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    81
      ||> Theory.add_finals_i false (map snd subst);
18640
61627ae3ddc3 generic attributes;
wenzelm
parents: 18620
diff changeset
    82
  in Pretty.writeln (pretty_consts ctxt (map (dest_Free o fst) subst)); (thms, thy') end;
18620
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    83
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    84
val axiomatize = gen_axiomatize read_specification;
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    85
val axiomatize_i = gen_axiomatize cert_specification;
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    86
fc8b5f275359 Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff changeset
    87
end;