src/HOL/thy_syntax.ML
author berghofe
Fri Jul 05 14:22:59 1996 +0200 (1996-07-05)
changeset 1845 afa622bc829d
parent 1788 ca62fab4ce92
child 2922 580647a879cf
permissions -rw-r--r--
Simplified syntax of primrec definitions.
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
clasohm@923
     5
Additional theory file sections for HOL.
clasohm@923
     6
clasohm@923
     7
TODO:
clasohm@923
     8
  move datatype / primrec stuff to pre_datatype.ML (?)
clasohm@923
     9
*)
clasohm@923
    10
clasohm@923
    11
(*the kind of distinctiveness axioms depends on number of constructors*)
clasohm@923
    12
val dtK = 5;  (* FIXME rename?, move? *)
clasohm@923
    13
clasohm@923
    14
structure ThySynData: THY_SYN_DATA =
clasohm@923
    15
struct
clasohm@923
    16
clasohm@923
    17
open ThyParse;
clasohm@923
    18
clasohm@923
    19
clasohm@1475
    20
(** typedef **)
clasohm@923
    21
clasohm@1475
    22
fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) =
clasohm@923
    23
  let
clasohm@923
    24
    val name' = if_none opt_name t;
clasohm@923
    25
    val name = strip_quotes name';
clasohm@923
    26
  in
clasohm@923
    27
    (cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt],
clasohm@923
    28
      [name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse",
clasohm@923
    29
        "Abs_" ^ name ^ "_inverse"])
clasohm@923
    30
  end;
clasohm@923
    31
clasohm@1475
    32
val typedef_decl =
clasohm@923
    33
  optional ("(" $$-- name --$$ ")" >> Some) None --
clasohm@923
    34
  type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
clasohm@1475
    35
  >> mk_typedef_decl;
clasohm@923
    36
clasohm@923
    37
clasohm@923
    38
clasohm@923
    39
(** (co)inductive **)
clasohm@923
    40
clasohm@923
    41
(*co is either "" or "Co"*)
clasohm@923
    42
fun inductive_decl co =
clasohm@923
    43
  let
clasohm@923
    44
    fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
clasohm@923
    45
      if Syntax.is_identifier s then "op " ^ s else "_";
clasohm@923
    46
    fun mk_params (((recs, ipairs), monos), con_defs) =
clasohm@923
    47
      let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
clasohm@923
    48
          and srec_tms = mk_list recs
clasohm@923
    49
          and sintrs   = mk_big_list (map snd ipairs)
clasohm@923
    50
          val stri_name = big_rec_name ^ "_Intrnl"
clasohm@923
    51
      in
clasohm@923
    52
         (";\n\n\
clasohm@923
    53
          \structure " ^ stri_name ^ " =\n\
clasohm@923
    54
          \  struct\n\
clasohm@923
    55
          \  val _ = writeln \"" ^ co ^
clasohm@923
    56
                     "Inductive definition " ^ big_rec_name ^ "\"\n\
paulson@1430
    57
          \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.termTVar) "
clasohm@923
    58
                           ^ srec_tms ^ "\n\
clasohm@923
    59
          \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
clasohm@923
    60
                           ^ sintrs ^ "\n\
paulson@1430
    61
          \  end;\n\n\
clasohm@923
    62
          \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^
clasohm@923
    63
             stri_name ^ ".rec_tms, " ^
clasohm@923
    64
             stri_name ^ ".intr_tms)"
clasohm@923
    65
         ,
clasohm@923
    66
          "structure " ^ big_rec_name ^ " =\n\
paulson@1430
    67
          \ let\n\
paulson@1430
    68
          \  val _ = writeln \"Proofs for " ^ co ^ 
paulson@1430
    69
                     "Inductive definition " ^ big_rec_name ^ "\"\n\
clasohm@923
    70
          \  structure Result = " ^ co ^ "Ind_section_Fun\n\
paulson@1430
    71
          \\t  (open " ^ stri_name ^ "\n\
paulson@1430
    72
          \\t   val thy\t\t= thy\n\
paulson@1430
    73
          \\t   val monos\t\t= " ^ monos ^ "\n\
paulson@1430
    74
          \\t   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
clasohm@1465
    75
          \ in\n\
paulson@1430
    76
          \  struct\n\
clasohm@923
    77
          \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
clasohm@923
    78
          \  open Result\n\
paulson@1430
    79
          \  end\n\
paulson@1430
    80
          \ end;\n\n\
paulson@1430
    81
          \structure " ^ stri_name ^ " = struct end;\n\n"
clasohm@923
    82
         )
clasohm@923
    83
      end
clasohm@923
    84
    val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
clasohm@923
    85
    fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
clasohm@923
    86
  in
paulson@1788
    87
    repeat1 name -- ipairs -- optstring "monos" -- optstring "con_defs"
clasohm@923
    88
      >> mk_params
clasohm@923
    89
  end;
clasohm@923
    90
clasohm@923
    91
clasohm@923
    92
clasohm@923
    93
(** datatype **)
clasohm@923
    94
clasohm@923
    95
local
clasohm@923
    96
  (* FIXME err -> add_datatype *)
clasohm@923
    97
  fun mk_cons cs =
clasohm@923
    98
    (case duplicates (map (fst o fst) cs) of
clasohm@923
    99
      [] => map (fn ((s, ts), syn) => mk_triple (s, mk_list ts, syn)) cs
clasohm@923
   100
    | dups => error ("Duplicate constructors: " ^ commas_quote dups));
clasohm@923
   101
clasohm@923
   102
  (*generate names of distinctiveness axioms*)
clasohm@923
   103
  fun mk_distinct_rules cs tname =
clasohm@923
   104
    let
clasohm@923
   105
      val uqcs = map (fn ((s, _), _) => strip_quotes s) cs;
clasohm@923
   106
      (*combine all constructor names with all others w/o duplicates*)
clasohm@923
   107
      fun neg_one c = map (fn c2 => quote (c ^ "_not_" ^ c2));
clasohm@923
   108
      fun neg1 [] = []
clasohm@923
   109
        | neg1 (c1 :: cs) = neg_one c1 cs @ neg1 cs;
clasohm@923
   110
    in
clasohm@923
   111
      if length uqcs < dtK then neg1 uqcs
clasohm@923
   112
      else quote (tname ^ "_ord_distinct") ::
clasohm@923
   113
        map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
clasohm@923
   114
    end;
clasohm@923
   115
clasohm@923
   116
  fun mk_rules tname cons pre = " map (get_axiom thy) " ^
clasohm@923
   117
    mk_list (map (fn ((s, _), _) => quote (tname ^ pre ^ strip_quotes s)) cons);
clasohm@923
   118
clasohm@1668
   119
  (*generate string for calling add_datatype and build_record*)
clasohm@923
   120
  fun mk_params ((ts, tname), cons) =
clasohm@923
   121
   ("val (thy, " ^ tname ^ "_add_primrec) = Datatype.add_datatype\n"
clasohm@923
   122
    ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
clasohm@923
   123
    \val thy = thy",
clasohm@923
   124
    "structure " ^ tname ^ " =\n\
clasohm@923
   125
    \struct\n\
clasohm@923
   126
    \ val inject = map (get_axiom thy) " ^
clasohm@923
   127
        mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s))
clasohm@923
   128
          (filter_out (null o snd o fst) cons)) ^ ";\n\
clasohm@923
   129
    \ val distinct = " ^
clasohm@923
   130
        (if length cons < dtK then "let val distinct' = " else "") ^
clasohm@923
   131
        "map (get_axiom thy) " ^ mk_list (mk_distinct_rules cons tname) ^
clasohm@923
   132
        (if length cons < dtK then
clasohm@923
   133
          "  in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
clasohm@923
   134
          \ distinct') end"
clasohm@923
   135
         else "") ^ ";\n\
clasohm@923
   136
    \ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
clasohm@923
   137
    \ val cases =" ^ mk_rules tname cons "_case_" ^ ";\n\
clasohm@923
   138
    \ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\
clasohm@923
   139
    \ val simps = inject @ distinct @ cases @ recs;\n\
clasohm@923
   140
    \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
clasohm@1264
   141
    \end;\n\
clasohm@1668
   142
    \val dummy = datatypes := Dtype.build_record (thy, " ^
clasohm@1668
   143
      mk_pair (quote tname, mk_list (map (fst o fst) cons)) ^
clasohm@1668
   144
      ", " ^ tname ^ ".induct_tac) :: (!datatypes);\n\
clasohm@1264
   145
    \val dummy = Addsimps " ^ tname ^ ".simps;\n");
clasohm@923
   146
clasohm@923
   147
  (*parsers*)
clasohm@923
   148
  val tvars = type_args >> map (cat "dtVar");
clasohm@1316
   149
clasohm@1316
   150
  val simple_typ = ident >> (cat "dtTyp" o curry mk_pair "[]" o quote) ||
clasohm@1316
   151
    type_var >> cat "dtVar";
clasohm@1316
   152
clasohm@1251
   153
  fun complex_typ toks =
clasohm@1316
   154
    let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
clasohm@1316
   155
        val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")";
clasohm@1316
   156
    in
clasohm@1316
   157
     (typ -- repeat (ident>>quote) >>
clasohm@1316
   158
        (foldl (fn (x,y) => "dtTyp " ^ mk_pair (brackets x, y))) ||
clasohm@1316
   159
      "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 (ident>>quote)) >>
clasohm@1316
   160
       (fn (fst, ids) => foldl (fn (x,y) => "dtTyp " ^
clasohm@1316
   161
                         mk_pair (brackets x, y)) (commas fst, ids))) toks
clasohm@1316
   162
    end;
clasohm@1316
   163
clasohm@977
   164
  val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));
clasohm@923
   165
  val constructor = name -- opt_typs -- opt_mixfix;
clasohm@923
   166
in
clasohm@923
   167
  val datatype_decl =
clasohm@923
   168
    tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params;
clasohm@923
   169
end;
clasohm@923
   170
clasohm@923
   171
clasohm@923
   172
clasohm@923
   173
(** primrec **)
clasohm@923
   174
berghofe@1845
   175
fun mk_primrec_decl_1 ((fname, tname), axms) =
clasohm@923
   176
  let
clasohm@1574
   177
    (*Isolate type name from the structure's identifier it may be stored in*)
clasohm@1574
   178
    val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
clasohm@1574
   179
clasohm@923
   180
    fun mk_prove (name, eqn) =
clasohm@1264
   181
      "val " ^ name ^ " = store_thm (" ^ quote name
clasohm@1574
   182
      ^ ", prove_goalw thy [get_def thy "
clasohm@1574
   183
      ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ "\n\
clasohm@1264
   184
      \  (fn _ => [Simp_tac 1]));";
clasohm@1264
   185
clasohm@923
   186
    val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
clasohm@1264
   187
  in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)
clasohm@1264
   188
      ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
clasohm@1264
   189
  end;
clasohm@923
   190
berghofe@1845
   191
fun mk_primrec_decl_2 ((fname, tname), axms) =
berghofe@1845
   192
  let
berghofe@1845
   193
    (*Isolate type name from the structure's identifier it may be stored in*)
berghofe@1845
   194
    val tname' = implode (snd (take_suffix (not_equal ".") (explode tname)));
berghofe@1845
   195
berghofe@1845
   196
    fun mk_prove eqn =
berghofe@1845
   197
      "prove_goalw thy [get_def thy "
berghofe@1845
   198
      ^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ " \
berghofe@1845
   199
      \(fn _ => [Simp_tac 1])";
berghofe@1845
   200
berghofe@1845
   201
    val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms);
berghofe@1845
   202
  in ("|> " ^ tname ^ "_add_primrec " ^ axs,
berghofe@1845
   203
      "val dummy = Addsimps " ^
berghofe@1845
   204
      brackets(space_implode ",\n" (map mk_prove axms)) ^ ";")
berghofe@1845
   205
  end;
berghofe@1845
   206
clasohm@923
   207
val primrec_decl =
berghofe@1845
   208
  (name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) ||
berghofe@1845
   209
  (name -- long_id -- repeat1 string >> mk_primrec_decl_2) ;
clasohm@923
   210
clasohm@923
   211
clasohm@923
   212
clasohm@923
   213
(** sections **)
clasohm@923
   214
clasohm@923
   215
val user_keywords = ["intrs", "monos", "con_defs", "|"];
clasohm@923
   216
clasohm@923
   217
val user_sections =
clasohm@1475
   218
 [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
clasohm@923
   219
  ("inductive", inductive_decl ""),
clasohm@923
   220
  ("coinductive", inductive_decl "Co"),
clasohm@923
   221
  ("datatype", datatype_decl),
clasohm@923
   222
  ("primrec", primrec_decl)];
clasohm@923
   223
clasohm@923
   224
clasohm@923
   225
end;
clasohm@923
   226
clasohm@923
   227
clasohm@923
   228
structure ThySyn = ThySynFun(ThySynData);
clasohm@923
   229
init_thy_reader ();
clasohm@923
   230