src/HOL/thy_syntax.ML
author wenzelm
Tue, 27 Apr 1999 10:51:16 +0200
changeset 6523 c84935821ba0
parent 6497 120ca2bb27e1
child 6555 17b7b88a8e3c
permissions -rw-r--r--
adapted add_inductive, add_record;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     1
(*  Title:      HOL/thy_syntax.ML
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     3
    Author:     Markus Wenzel and Lawrence C Paulson and Carsten Clasohm
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
Additional theory file sections for HOL.
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
3622
85898be702b2 use ThySyn.add_syntax;
wenzelm
parents: 3617
diff changeset
     8
local
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     9
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    10
open ThyParse;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    11
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    12
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1465
diff changeset
    13
(** typedef **)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1465
diff changeset
    15
fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) =
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    16
  let
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    17
    val name' = if_none opt_name t;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    18
    val name = strip_quotes name';
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    19
  in
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    20
    (cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt],
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    21
      [name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse",
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    22
        "Abs_" ^ name ^ "_inverse"])
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    23
  end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    24
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1465
diff changeset
    25
val typedef_decl =
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    26
  optional ("(" $$-- name --$$ ")" >> Some) None --
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    27
  type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1465
diff changeset
    28
  >> mk_typedef_decl;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    29
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    30
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    31
3980
21ef91734970 added record section;
wenzelm
parents: 3945
diff changeset
    32
(** record **)
21ef91734970 added record section;
wenzelm
parents: 3945
diff changeset
    33
21ef91734970 added record section;
wenzelm
parents: 3945
diff changeset
    34
val record_decl =
4225
3d9e551bc5a6 improved record syntax;
wenzelm
parents: 4204
diff changeset
    35
  (type_args -- name >> (mk_pair o apfst mk_list)) --$$ "="
4226
38c91213f26b fixed record parser;
wenzelm
parents: 4225
diff changeset
    36
    -- optional (typ --$$ "+" >> (parens o cat "Some")) "None"
4225
3d9e551bc5a6 improved record syntax;
wenzelm
parents: 4204
diff changeset
    37
    -- repeat1 ((name --$$ "::" -- typ) >> mk_pair)
4001
b6a3c2665c45 record: tuned output;
wenzelm
parents: 3980
diff changeset
    38
  >> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]);
3980
21ef91734970 added record section;
wenzelm
parents: 3945
diff changeset
    39
21ef91734970 added record section;
wenzelm
parents: 3945
diff changeset
    40
6477
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
    41
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    42
(** (co)inductive **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    43
5097
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    44
fun inductive_decl coind =
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    45
  let
6426
9a2ace82b68e intrs: names and atts;
wenzelm
parents: 6381
diff changeset
    46
    val no_atts = map (mk_pair o rpair "[]");
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    47
    fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    48
      if Syntax.is_identifier s then "op " ^ s else "_";
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    49
    fun mk_params (((recs, ipairs), monos), con_defs) =
6035
c041fc54ab4c replaced obsolete "trim" by "strip_quotes"
paulson
parents: 5716
diff changeset
    50
      let val big_rec_name = space_implode "_" (map (scan_to_id o strip_quotes) recs)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    51
          and srec_tms = mk_list recs
6426
9a2ace82b68e intrs: names and atts;
wenzelm
parents: 6381
diff changeset
    52
          and sintrs   = mk_big_list (no_atts (map (mk_pair o apfst quote) ipairs))
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    53
      in
5097
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    54
        ";\n\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    55
        \local\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    56
        \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    57
        \  InductivePackage.add_inductive true " ^
6523
c84935821ba0 adapted add_inductive, add_record;
wenzelm
parents: 6497
diff changeset
    58
        (if coind then "true " else "false ") ^ srec_tms ^ " [] " ^
6426
9a2ace82b68e intrs: names and atts;
wenzelm
parents: 6381
diff changeset
    59
         sintrs ^ " " ^ mk_list (no_atts monos) ^ " " ^ mk_list (no_atts con_defs) ^ " thy;\n\
5097
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    60
        \in\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    61
        \structure " ^ big_rec_name ^ " =\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    62
        \struct\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    63
        \  val defs = defs;\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    64
        \  val mono = mono;\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    65
        \  val unfold = unfold;\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    66
        \  val intrs = intrs;\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    67
        \  val elims = elims;\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    68
        \  val elim = hd elims;\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    69
        \  val " ^ (if coind then "co" else "") ^ "induct = induct;\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    70
        \  val mk_cases = mk_cases;\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    71
        \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = intrs;\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    72
        \end;\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    73
        \val thy = thy;\nend;\n\
6c4a7ad6ebc7 Adapted to new inductive definition package.
berghofe
parents: 4873
diff changeset
    74
        \val thy = thy\n"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    75
      end
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    76
    val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
5716
a3d2a6b6693e Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents: 5658
diff changeset
    77
    fun optlist s = optional (s $$-- list1 name) []
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    78
  in
5716
a3d2a6b6693e Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents: 5658
diff changeset
    79
    repeat1 name -- ipairs -- optlist "monos" -- optlist "con_defs"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    80
      >> mk_params
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    81
  end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    82
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    83
6477
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
    84
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    85
(** datatype **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    86
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    87
local
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
    88
  (*** generate string for calling add_datatype ***)
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
    89
  (*** and bindig theorems to ML identifiers    ***)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    90
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
    91
  fun mk_bind_thms_string names =
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
    92
   (case find_first (not o Syntax.is_identifier) names of
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
    93
      Some id => (warning (id ^ " is not a valid identifier"); "")
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
    94
    | None =>
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
    95
        let
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
    96
          fun mk_dt_struct (s, (id, i)) =
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
    97
            s ^ "structure " ^ id ^ " =\n\
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
    98
            \struct\n\
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
    99
            \  val distinct = nth_elem (" ^ i ^ ", distinct);\n\
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   100
            \  val inject = nth_elem (" ^ i ^ ", inject);\n\
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   101
            \  val exhaust = nth_elem (" ^ i ^ ", exhaustion);\n\
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   102
            \  val cases = nth_elem (" ^ i ^ ", case_thms);\n\
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   103
            \  val (split, split_asm) = nth_elem (" ^ i ^ ", split_thms);\n" ^
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   104
              (if length names = 1 then
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   105
                 "  val induct = induction;\n\
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   106
                 \  val recs = rec_thms;\n\
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   107
                 \  val simps = simps;\n\
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   108
                 \  val size = size;\n"
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   109
               else "") ^
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   110
            "end;\n";
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   111
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   112
          val structs = foldl mk_dt_struct
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   113
            ("", (names ~~ (map string_of_int (0 upto length names - 1))));
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   114
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   115
        in
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   116
          (if length names > 1 then
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   117
             "structure " ^ (space_implode "_" names) ^ " =\n\
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   118
             \struct\n\
5658
082debccf486 Changed structure of name spaces for datatypes.
berghofe
parents: 5222
diff changeset
   119
             \  val induct = induction;\n\
082debccf486 Changed structure of name spaces for datatypes.
berghofe
parents: 5222
diff changeset
   120
             \  val recs = rec_thms;\n\
082debccf486 Changed structure of name spaces for datatypes.
berghofe
parents: 5222
diff changeset
   121
             \  val simps = simps;\n\
082debccf486 Changed structure of name spaces for datatypes.
berghofe
parents: 5222
diff changeset
   122
             \  val size = size;\nend;\n"
082debccf486 Changed structure of name spaces for datatypes.
berghofe
parents: 5222
diff changeset
   123
           else "") ^ structs
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   124
        end);
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   125
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   126
  fun mk_dt_string dts =
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   127
    let
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   128
      val names = map (fn ((((alt_name, _), name), _), _) =>
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   129
        strip_quotes (if_none alt_name name)) dts;
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   130
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   131
      val add_datatype_args = brackets (commas (map quote names)) ^ " " ^
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   132
        brackets (commas (map (fn ((((_, vs), name), mx), cs) =>
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   133
          parens (brackets (commas vs) ^ ", " ^ name ^ ", " ^ mx ^ ", " ^
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   134
            brackets (commas cs))) dts));
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   135
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   136
    in
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   137
      ";\nlocal\n\
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   138
      \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   139
      \  case_thms, split_thms, induction, size, simps}) =\n\
6103
36f272ea9413 get_tthms witness theorems;
wenzelm
parents: 6035
diff changeset
   140
      \ DatatypePackage.add_datatype false " ^ add_datatype_args ^ " thy;\n\
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   141
      \in\n" ^ mk_bind_thms_string names ^
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   142
      "val thy = thy;\nend;\nval thy = thy\n"
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   143
    end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   144
6381
ed0c7b4a325d adapted rep_datatype;
wenzelm
parents: 6356
diff changeset
   145
  fun mk_thmss namess = mk_list (map (mk_list o map (mk_pair o rpair "[]")) namess);
ed0c7b4a325d adapted rep_datatype;
wenzelm
parents: 6356
diff changeset
   146
  fun mk_thm name = mk_pair (name, "[]");
6103
36f272ea9413 get_tthms witness theorems;
wenzelm
parents: 6035
diff changeset
   147
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   148
  fun mk_rep_dt_string (((names, distinct), inject), induct) =
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   149
    ";\nlocal\n\
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   150
    \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   151
    \  case_thms, split_thms, induction, size, simps}) =\n\
6103
36f272ea9413 get_tthms witness theorems;
wenzelm
parents: 6035
diff changeset
   152
    \ DatatypePackage.rep_datatype " ^
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   153
    (case names of
6103
36f272ea9413 get_tthms witness theorems;
wenzelm
parents: 6035
diff changeset
   154
        Some names => "(Some [" ^ commas_quote names ^ "])\n " ^
36f272ea9413 get_tthms witness theorems;
wenzelm
parents: 6035
diff changeset
   155
          mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
36f272ea9413 get_tthms witness theorems;
wenzelm
parents: 6035
diff changeset
   156
            "\n " ^ mk_thm induct ^ " thy;\nin\n" ^ mk_bind_thms_string names
36f272ea9413 get_tthms witness theorems;
wenzelm
parents: 6035
diff changeset
   157
      | None => "None\n " ^ mk_thmss distinct ^ "\n " ^ mk_thmss inject ^
36f272ea9413 get_tthms witness theorems;
wenzelm
parents: 6035
diff changeset
   158
            "\n " ^ mk_thm induct ^ " thy;\nin\n") ^
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   159
    "val thy = thy;\nend;\nval thy = thy\n";
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   160
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   161
  (*** parsers ***)
4106
wenzelm
parents: 4091
diff changeset
   162
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   163
  val simple_typ = ident || (type_var >> strip_quotes);
1316
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   164
1251
81fc4d8e3eda added nested types on right hand side of datatype definitions
clasohm
parents: 977
diff changeset
   165
  fun complex_typ toks =
1316
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   166
    let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   167
        val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")";
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   168
    in
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   169
     (typ ^^ (repeat ident >> (cat "" o space_implode " ")) ||
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   170
      "(" $$-- !! (list1 typ2 >> (parens o commas)) --$$ ")" ^^ !!
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   171
        (repeat1 ident >> (cat "" o space_implode " "))) toks
1316
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   172
    end;
ce35d42d2190 extended complex_typ
clasohm
parents: 1264
diff changeset
   173
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   174
  val opt_typs = repeat ((string >> strip_quotes) ||
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   175
    simple_typ || ("(" $$-- complex_typ --$$ ")"));
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   176
  val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) =>
5716
a3d2a6b6693e Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents: 5658
diff changeset
   177
    parens (n ^ ", " ^ brackets (commas_quote Ts) ^ ", " ^ mx));
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   178
  val opt_name = optional ("(" $$-- name --$$ ")" >> Some) None
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   179
5716
a3d2a6b6693e Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents: 5658
diff changeset
   180
  fun optlistlist s = optional (s $$-- enum "and" (list name)) [[]]
a3d2a6b6693e Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents: 5658
diff changeset
   181
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   182
in
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   183
  val datatype_decl =
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   184
    enum1 "and" (opt_name -- type_args -- name -- opt_infix --$$ "=" --
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   185
      enum1 "|" constructor) >> mk_dt_string;
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   186
  val rep_datatype_decl =
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   187
    ((optional ((repeat1 (name >> strip_quotes)) >> Some) None) --
5716
a3d2a6b6693e Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents: 5658
diff changeset
   188
      optlistlist "distinct" -- optlistlist "inject" --
a3d2a6b6693e Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents: 5658
diff changeset
   189
        ("induct" $$-- name)) >> mk_rep_dt_string;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   190
end;
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   191
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   192
6477
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   193
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   194
(** primrec **)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   195
5716
a3d2a6b6693e Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents: 5658
diff changeset
   196
fun mk_primrec_decl (alt_name, eqns) =
a3d2a6b6693e Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents: 5658
diff changeset
   197
  let
a3d2a6b6693e Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents: 5658
diff changeset
   198
    val names = map (fn (s, _) => if s = "" then "_" else s) eqns
a3d2a6b6693e Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents: 5658
diff changeset
   199
  in
6356
6c01697e082e primrec: empty attributes;
wenzelm
parents: 6103
diff changeset
   200
    ";\nval (thy, " ^ mk_list names ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^
6c01697e082e primrec: empty attributes;
wenzelm
parents: 6103
diff changeset
   201
    mk_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) eqns) ^
6c01697e082e primrec: empty attributes;
wenzelm
parents: 6103
diff changeset
   202
    " " ^ " thy;\n\
5716
a3d2a6b6693e Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents: 5658
diff changeset
   203
    \val thy = thy\n"
a3d2a6b6693e Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents: 5658
diff changeset
   204
  end;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   205
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   206
(* either names and axioms or just axioms *)
5716
a3d2a6b6693e Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents: 5658
diff changeset
   207
val primrec_decl = (optional ("(" $$-- name --$$ ")") "\"\"" --
a3d2a6b6693e Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents: 5658
diff changeset
   208
  (repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl;
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   209
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   210
6497
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   211
(*** recdef: interface to Slind's TFL ***)
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   212
6497
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   213
(** TFL with explicit WF relations **)
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   214
3194
36bfceef1800 TFL theory section
paulson
parents: 2930
diff changeset
   215
(*fname: name of function being defined; rel: well-founded relation*)
6497
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   216
fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
6477
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   217
  let
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   218
    val fid = strip_quotes fname;
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   219
    val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   220
    val axms_text = mk_big_list (map (fn a => mk_pair (mk_pair (quote "", a), "[]")) axms);
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   221
  in
6477
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   222
    ";\n\n\
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   223
    \local\n\
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   224
    \val (thy, result) = thy |> RecdefPackage.add_recdef " ^ quote fid ^ " " ^ rel ^ "\n" ^
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   225
    axms_text ^ "\n(Some (" ^ ss ^ "))\n" ^ congs_text ^ ";\n\
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   226
    \in\n\
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   227
    \structure " ^ fid ^ " =\n\
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   228
    \struct\n\
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   229
    \  val {rules, induct, tcs} = result;\n\
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   230
    \end;\n\
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   231
    \val thy = thy;\n\
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   232
    \end;\n\
e36581d04eee recdef adapted to RecdefPackage.add_recdef;
wenzelm
parents: 6426
diff changeset
   233
    \val thy = thy\n"
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   234
  end;
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   235
6497
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   236
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   237
(** TFL with no WF relation supplied **)
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   238
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   239
(*fname: name of function being defined; rel: well-founded relation*)
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   240
fun mk_rec_deferred_decl (((fname, congs), ss), axms) =
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   241
  let val fid = strip_quotes fname
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   242
      val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs);
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   243
  in
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   244
      ";\n\n\
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   245
       \local\n\
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   246
       \val (thy, induct_rules) = Tfl.function thy " ^ 
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   247
          quote fid ^ " " ^ 
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   248
	  " (" ^ congs_text ^ ")\n" 
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   249
	  ^ mk_big_list axms ^ ";\n\
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   250
       \in\n\
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   251
       \structure " ^ fid ^ " =\n\
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   252
       \struct\n\
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   253
       \  val induct_rules = induct_rules \n\
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   254
       \end;\n\
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   255
       \val thy = thy;\nend;\n\
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   256
       \val thy = thy\n"
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   257
  end;
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   258
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   259
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   260
(*parses either a standard or a deferred recdef; the latter has no WF
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   261
  relation given*)
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   262
val recdef_decl = 
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   263
    (name -- string -- 
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   264
     optional ("congs" $$-- list1 name) [] -- 
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   265
     optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- 
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   266
     repeat1 string >> mk_rec_decl)
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   267
    ||
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   268
    (name --$$ "??" --
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   269
     optional ("congs" $$-- list1 name) [] -- 
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   270
     optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- 
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   271
     repeat1 string >> mk_rec_deferred_decl) ;
2922
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   272
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   273
580647a879cf Using Blast_tac
paulson
parents: 1845
diff changeset
   274
3622
85898be702b2 use ThySyn.add_syntax;
wenzelm
parents: 3617
diff changeset
   275
(** augment thy syntax **)
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   276
3622
85898be702b2 use ThySyn.add_syntax;
wenzelm
parents: 3617
diff changeset
   277
in
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   278
3622
85898be702b2 use ThySyn.add_syntax;
wenzelm
parents: 3617
diff changeset
   279
val _ = ThySyn.add_syntax
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   280
 ["intrs", "monos", "con_defs", "congs", "simpset", "|",
6497
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   281
  "and", "distinct", "inject", "induct", "??"]
4873
b5999638979e TypedefPackage.add_typedef;
wenzelm
parents: 4536
diff changeset
   282
 [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
6523
c84935821ba0 adapted add_inductive, add_record;
wenzelm
parents: 6497
diff changeset
   283
  section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl,
6497
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   284
  section "inductive" 	"" (inductive_decl false),
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   285
  section "coinductive"	"" (inductive_decl true),
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   286
  section "datatype" 	"" datatype_decl,
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 5097
diff changeset
   287
  section "rep_datatype" "" rep_datatype_decl,
6497
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   288
  section "primrec" 	"" primrec_decl,
120ca2bb27e1 Now for recdefs that omit the WF relation
paulson
parents: 6477
diff changeset
   289
  section "recdef" 	"" recdef_decl];
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   290
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
   291
end;