src/HOL/thy_syntax.ML
author wenzelm
Sun Nov 04 21:12:03 2001 +0100 (2001-11-04)
changeset 12050 6934c005aec4
parent 11822 122834177ec1
child 12180 91c9f661b183
permissions -rw-r--r--
tuned comment;
clasohm@923
     1
(*  Title:      HOL/thy_syntax.ML
clasohm@923
     2
    ID:         $Id$
clasohm@923
     3
    Author:     Markus Wenzel and Lawrence C Paulson and Carsten Clasohm
clasohm@923
     4
wenzelm@12050
     5
Additional sections for *old-style* theory files in HOL.
clasohm@923
     6
*)
clasohm@923
     7
wenzelm@3622
     8
local
clasohm@923
     9
clasohm@923
    10
open ThyParse;
clasohm@923
    11
clasohm@923
    12
clasohm@1475
    13
(** typedef **)
clasohm@923
    14
clasohm@1475
    15
fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) =
clasohm@923
    16
  let
clasohm@923
    17
    val name' = if_none opt_name t;
wenzelm@6642
    18
    val name = unenclose name';
clasohm@923
    19
  in
clasohm@923
    20
    (cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt],
clasohm@923
    21
      [name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse",
clasohm@923
    22
        "Abs_" ^ name ^ "_inverse"])
clasohm@923
    23
  end;
clasohm@923
    24
clasohm@1475
    25
val typedef_decl =
clasohm@923
    26
  optional ("(" $$-- name --$$ ")" >> Some) None --
clasohm@923
    27
  type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
clasohm@1475
    28
  >> mk_typedef_decl;
clasohm@923
    29
clasohm@923
    30
clasohm@923
    31
wenzelm@3980
    32
(** record **)
wenzelm@3980
    33
wenzelm@3980
    34
val record_decl =
wenzelm@4225
    35
  (type_args -- name >> (mk_pair o apfst mk_list)) --$$ "="
wenzelm@4226
    36
    -- optional (typ --$$ "+" >> (parens o cat "Some")) "None"
wenzelm@4225
    37
    -- repeat1 ((name --$$ "::" -- typ) >> mk_pair)
wenzelm@4001
    38
  >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]);
wenzelm@3980
    39
wenzelm@3980
    40
wenzelm@6477
    41
clasohm@923
    42
(** (co)inductive **)
clasohm@923
    43
wenzelm@8813
    44
(*Skipping initial blanks, find the first identifier*)  (* FIXME slightly broken! *)
wenzelm@8813
    45
fun scan_to_id s =
wenzelm@8813
    46
    s |> Symbol.explode
wenzelm@8813
    47
    |> Scan.error (Scan.finite Symbol.stopper
wenzelm@8813
    48
      (Scan.!! (fn _ => "Expected to find an identifier in " ^ s)
wenzelm@8813
    49
        (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
wenzelm@8813
    50
    |> #1;
wenzelm@8813
    51
berghofe@5097
    52
fun inductive_decl coind =
clasohm@923
    53
  let
wenzelm@6426
    54
    val no_atts = map (mk_pair o rpair "[]");
clasohm@923
    55
    fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
clasohm@923
    56
      if Syntax.is_identifier s then "op " ^ s else "_";
clasohm@923
    57
    fun mk_params (((recs, ipairs), monos), con_defs) =
wenzelm@6642
    58
      let val big_rec_name = space_implode "_" (map (scan_to_id o unenclose) recs)
clasohm@923
    59
          and srec_tms = mk_list recs
wenzelm@6426
    60
          and sintrs   = mk_big_list (no_atts (map (mk_pair o apfst quote) ipairs))
clasohm@923
    61
      in
berghofe@5097
    62
        ";\n\n\
berghofe@5097
    63
        \local\n\
berghofe@5097
    64
        \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
berghofe@5097
    65
        \  InductivePackage.add_inductive true " ^
wenzelm@11628
    66
        (if coind then "true " else "false ") ^ srec_tms ^
wenzelm@6426
    67
         sintrs ^ " " ^ mk_list (no_atts monos) ^ " " ^ mk_list (no_atts con_defs) ^ " thy;\n\
berghofe@5097
    68
        \in\n\
berghofe@5097
    69
        \structure " ^ big_rec_name ^ " =\n\
berghofe@5097
    70
        \struct\n\
berghofe@5097
    71
        \  val defs = defs;\n\
berghofe@5097
    72
        \  val mono = mono;\n\
berghofe@5097
    73
        \  val unfold = unfold;\n\
berghofe@5097
    74
        \  val intrs = intrs;\n\
berghofe@5097
    75
        \  val elims = elims;\n\
berghofe@5097
    76
        \  val elim = hd elims;\n\
berghofe@5097
    77
        \  val " ^ (if coind then "co" else "") ^ "induct = induct;\n\
berghofe@5097
    78
        \  val mk_cases = mk_cases;\n\
berghofe@5097
    79
        \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = intrs;\n\
berghofe@5097
    80
        \end;\n\
berghofe@5097
    81
        \val thy = thy;\nend;\n\
berghofe@5097
    82
        \val thy = thy\n"
clasohm@923
    83
      end
clasohm@923
    84
    val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
berghofe@5716
    85
    fun optlist s = optional (s $$-- list1 name) []
clasohm@923
    86
  in
berghofe@5716
    87
    repeat1 name -- ipairs -- optlist "monos" -- optlist "con_defs"
clasohm@923
    88
      >> mk_params
clasohm@923
    89
  end;
clasohm@923
    90
clasohm@923
    91
wenzelm@6477
    92
clasohm@923
    93
(** datatype **)
clasohm@923
    94
clasohm@923
    95
local
berghofe@5183
    96
  (*** generate string for calling add_datatype ***)
berghofe@5183
    97
  (*** and bindig theorems to ML identifiers    ***)
clasohm@923
    98
berghofe@5183
    99
  fun mk_bind_thms_string names =
berghofe@5183
   100
   (case find_first (not o Syntax.is_identifier) names of
berghofe@5183
   101
      Some id => (warning (id ^ " is not a valid identifier"); "")
berghofe@5183
   102
    | None =>
berghofe@5183
   103
        let
berghofe@5183
   104
          fun mk_dt_struct (s, (id, i)) =
berghofe@5183
   105
            s ^ "structure " ^ id ^ " =\n\
berghofe@5183
   106
            \struct\n\
berghofe@5183
   107
            \  val distinct = nth_elem (" ^ i ^ ", distinct);\n\
berghofe@5183
   108
            \  val inject = nth_elem (" ^ i ^ ", inject);\n\
berghofe@5183
   109
            \  val exhaust = nth_elem (" ^ i ^ ", exhaustion);\n\
berghofe@5183
   110
            \  val cases = nth_elem (" ^ i ^ ", case_thms);\n\
berghofe@5183
   111
            \  val (split, split_asm) = nth_elem (" ^ i ^ ", split_thms);\n" ^
berghofe@5183
   112
              (if length names = 1 then
berghofe@5183
   113
                 "  val induct = induction;\n\
berghofe@5183
   114
                 \  val recs = rec_thms;\n\
berghofe@5183
   115
                 \  val simps = simps;\n\
berghofe@5183
   116
                 \  val size = size;\n"
berghofe@5183
   117
               else "") ^
berghofe@5183
   118
            "end;\n";
berghofe@5183
   119
berghofe@5183
   120
          val structs = foldl mk_dt_struct
berghofe@5183
   121
            ("", (names ~~ (map string_of_int (0 upto length names - 1))));
berghofe@5183
   122
berghofe@5183
   123
        in
berghofe@5183
   124
          (if length names > 1 then
berghofe@5183
   125
             "structure " ^ (space_implode "_" names) ^ " =\n\
berghofe@5183
   126
             \struct\n\
berghofe@5658
   127
             \  val induct = induction;\n\
berghofe@5658
   128
             \  val recs = rec_thms;\n\
berghofe@5658
   129
             \  val simps = simps;\n\
berghofe@5658
   130
             \  val size = size;\nend;\n"
berghofe@5658
   131
           else "") ^ structs
berghofe@5183
   132
        end);
berghofe@5183
   133
berghofe@5183
   134
  fun mk_dt_string dts =
clasohm@923
   135
    let
berghofe@5183
   136
      val names = map (fn ((((alt_name, _), name), _), _) =>
wenzelm@6642
   137
        unenclose (if_none alt_name name)) dts;
berghofe@5183
   138
berghofe@5183
   139
      val add_datatype_args = brackets (commas (map quote names)) ^ " " ^
berghofe@5183
   140
        brackets (commas (map (fn ((((_, vs), name), mx), cs) =>
berghofe@5183
   141
          parens (brackets (commas vs) ^ ", " ^ name ^ ", " ^ mx ^ ", " ^
berghofe@5183
   142
            brackets (commas cs))) dts));
berghofe@5183
   143
clasohm@923
   144
    in
berghofe@5183
   145
      ";\nlocal\n\
berghofe@5183
   146
      \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
berghofe@5183
   147
      \  case_thms, split_thms, induction, size, simps}) =\n\
wenzelm@6103
   148
      \ DatatypePackage.add_datatype false " ^ add_datatype_args ^ " thy;\n\
berghofe@5183
   149
      \in\n" ^ mk_bind_thms_string names ^
berghofe@5183
   150
      "val thy = thy;\nend;\nval thy = thy\n"
clasohm@923
   151
    end;
clasohm@923
   152
wenzelm@6381
   153
  fun mk_thmss namess = mk_list (map (mk_list o map (mk_pair o rpair "[]")) namess);
wenzelm@6381
   154
  fun mk_thm name = mk_pair (name, "[]");
wenzelm@6103
   155
berghofe@5183
   156
  fun mk_rep_dt_string (((names, distinct), inject), induct) =
berghofe@5183
   157
    ";\nlocal\n\
berghofe@5183
   158
    \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
berghofe@5183
   159
    \  case_thms, split_thms, induction, size, simps}) =\n\
wenzelm@6103
   160
    \ DatatypePackage.rep_datatype " ^
berghofe@5183
   161
    (case names of
wenzelm@6103
   162
        Some names => "(Some [" ^ commas_quote names ^ "])\n " ^
wenzelm@6103
   163
          mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
wenzelm@6103
   164
            "\n " ^ mk_thm induct ^ " thy;\nin\n" ^ mk_bind_thms_string names
wenzelm@6103
   165
      | None => "None\n " ^ mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
wenzelm@6103
   166
            "\n " ^ mk_thm induct ^ " thy;\nin\n") ^
berghofe@5183
   167
    "val thy = thy;\nend;\nval thy = thy\n";
clasohm@923
   168
berghofe@5183
   169
  (*** parsers ***)
wenzelm@4106
   170
wenzelm@6642
   171
  val simple_typ = ident || (type_var >> unenclose);
clasohm@1316
   172
clasohm@1251
   173
  fun complex_typ toks =
clasohm@1316
   174
    let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
clasohm@1316
   175
        val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")";
clasohm@1316
   176
    in
berghofe@5183
   177
     (typ ^^ (repeat ident >> (cat "" o space_implode " ")) ||
berghofe@5183
   178
      "(" $$-- !! (list1 typ2 >> (parens o commas)) --$$ ")" ^^ !!
berghofe@5183
   179
        (repeat1 ident >> (cat "" o space_implode " "))) toks
clasohm@1316
   180
    end;
clasohm@1316
   181
wenzelm@6642
   182
  val opt_typs = repeat ((string >> unenclose) ||
berghofe@5183
   183
    simple_typ || ("(" $$-- complex_typ --$$ ")"));
berghofe@5183
   184
  val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) =>
berghofe@5716
   185
    parens (n ^ ", " ^ brackets (commas_quote Ts) ^ ", " ^ mx));
berghofe@5183
   186
  val opt_name = optional ("(" $$-- name --$$ ")" >> Some) None
berghofe@5183
   187
berghofe@5716
   188
  fun optlistlist s = optional (s $$-- enum "and" (list name)) [[]]
berghofe@5716
   189
clasohm@923
   190
in
clasohm@923
   191
  val datatype_decl =
berghofe@5183
   192
    enum1 "and" (opt_name -- type_args -- name -- opt_infix --$$ "=" --
berghofe@5183
   193
      enum1 "|" constructor) >> mk_dt_string;
berghofe@5183
   194
  val rep_datatype_decl =
wenzelm@6642
   195
    ((optional ((repeat1 (name >> unenclose)) >> Some) None) --
berghofe@5716
   196
      optlistlist "distinct" -- optlistlist "inject" --
berghofe@5716
   197
        ("induct" $$-- name)) >> mk_rep_dt_string;
clasohm@923
   198
end;
clasohm@923
   199
clasohm@923
   200
wenzelm@6477
   201
clasohm@923
   202
(** primrec **)
clasohm@923
   203
wenzelm@8657
   204
fun mk_patterns eqns = mk_list (map (fn (s, _) => if s = "" then "_" else s) eqns);
wenzelm@8657
   205
fun mk_eqns eqns = mk_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) eqns);
wenzelm@8657
   206
berghofe@5716
   207
fun mk_primrec_decl (alt_name, eqns) =
wenzelm@8657
   208
  ";\nval (thy, " ^ mk_patterns eqns ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " "
wenzelm@8657
   209
  ^ mk_eqns eqns ^ " " ^ " thy;\n\
wenzelm@8657
   210
  \val thy = thy\n"
clasohm@923
   211
berghofe@5183
   212
(* either names and axioms or just axioms *)
wenzelm@8657
   213
val primrec_decl = optional ("(" $$-- name --$$ ")") "\"\"" --
wenzelm@8657
   214
  repeat1 (ident -- string || (string >> pair "")) >> mk_primrec_decl;
clasohm@923
   215
paulson@2922
   216
paulson@6497
   217
(*** recdef: interface to Slind's TFL ***)
paulson@2922
   218
paulson@6497
   219
(** TFL with explicit WF relations **)
paulson@2922
   220
paulson@3194
   221
(*fname: name of function being defined; rel: well-founded relation*)
wenzelm@8657
   222
fun mk_recdef_decl ((((fname, rel), congs), ss), eqns) =
wenzelm@9857
   223
  let val fid = unenclose fname in
wenzelm@6477
   224
    ";\n\n\
wenzelm@6477
   225
    \local\n\
nipkow@8623
   226
    \fun simpset() = Simplifier.simpset_of thy;\n\
wenzelm@9857
   227
    \val (thy, result) = thy |> RecdefPackage.add_recdef_old " ^ quote fid ^ " " ^ rel ^ "\n" ^
wenzelm@9857
   228
    mk_eqns eqns ^ "\n(" ^ ss ^ ",\n " ^ mk_list congs ^ ");\n\
wenzelm@6477
   229
    \in\n\
wenzelm@6477
   230
    \structure " ^ fid ^ " =\n\
wenzelm@6477
   231
    \struct\n\
wenzelm@8657
   232
    \  val {simps, rules = " ^ mk_patterns eqns ^ ", induct, tcs} = result;\n\
wenzelm@6477
   233
    \end;\n\
wenzelm@6477
   234
    \val thy = thy;\n\
wenzelm@6477
   235
    \end;\n\
wenzelm@6477
   236
    \val thy = thy\n"
paulson@2922
   237
  end;
paulson@2922
   238
wenzelm@6555
   239
val recdef_decl =
wenzelm@8657
   240
  name -- string --
wenzelm@9857
   241
    optional ("congs" $$-- list1 ident) [] --
wenzelm@6642
   242
    optional ("simpset" $$-- string >> unenclose) "simpset()" --
wenzelm@8657
   243
    repeat1 (ident -- string || (string >> pair "")) >> mk_recdef_decl;
wenzelm@6555
   244
paulson@6497
   245
paulson@6497
   246
(** TFL with no WF relation supplied **)
paulson@6497
   247
paulson@6497
   248
(*fname: name of function being defined; rel: well-founded relation*)
wenzelm@6555
   249
fun mk_defer_recdef_decl ((fname, congs), axms) =
wenzelm@6555
   250
  let
wenzelm@6642
   251
    val fid = unenclose fname;
wenzelm@6555
   252
    val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
wenzelm@6555
   253
    val axms_text = mk_big_list axms;
paulson@6497
   254
  in
wenzelm@6555
   255
    ";\n\n\
wenzelm@6555
   256
    \local\n\
wenzelm@6555
   257
    \val (thy, result) = thy |> RecdefPackage.defer_recdef " ^ quote fid ^ "\n" ^
wenzelm@6555
   258
    axms_text ^ "\n" ^ congs_text ^ ";\n\
wenzelm@6555
   259
    \in\n\
wenzelm@6555
   260
    \structure " ^ fid ^ " =\n\
wenzelm@6555
   261
    \struct\n\
wenzelm@6555
   262
    \  val {induct_rules} = result;\n\
wenzelm@6555
   263
    \end;\n\
wenzelm@6555
   264
    \val thy = thy;\n\
wenzelm@6555
   265
    \end;\n\
wenzelm@6555
   266
    \val thy = thy\n"
paulson@6497
   267
  end;
paulson@6497
   268
wenzelm@6555
   269
val defer_recdef_decl =
wenzelm@6555
   270
  (name --
wenzelm@6555
   271
    optional ("congs" $$-- list1 name) [] --
wenzelm@6555
   272
    repeat1 string >> mk_defer_recdef_decl);
paulson@2922
   273
paulson@2922
   274
paulson@2922
   275
wenzelm@3622
   276
(** augment thy syntax **)
clasohm@923
   277
wenzelm@3622
   278
in
clasohm@923
   279
wenzelm@3622
   280
val _ = ThySyn.add_syntax
berghofe@5183
   281
 ["intrs", "monos", "con_defs", "congs", "simpset", "|",
wenzelm@6555
   282
  "and", "distinct", "inject", "induct"]
wenzelm@11822
   283
 [axm_section "typedef" "|> TypedefPackage.add_typedef_x" typedef_decl,
wenzelm@6523
   284
  section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl,
paulson@6497
   285
  section "inductive" 	"" (inductive_decl false),
paulson@6497
   286
  section "coinductive"	"" (inductive_decl true),
paulson@6497
   287
  section "datatype" 	"" datatype_decl,
berghofe@5183
   288
  section "rep_datatype" "" rep_datatype_decl,
paulson@6497
   289
  section "primrec" 	"" primrec_decl,
wenzelm@6555
   290
  section "recdef" 	"" recdef_decl,
wenzelm@6555
   291
  section "defer_recdef" "" defer_recdef_decl];
clasohm@923
   292
clasohm@923
   293
end;