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