src/HOL/thy_syntax.ML
author paulson
Mon Dec 28 16:46:15 1998 +0100 (1998-12-28)
changeset 6035 c041fc54ab4c
parent 5716 a3d2a6b6693e
child 6103 36f272ea9413
permissions -rw-r--r--
replaced obsolete "trim" by "strip_quotes"
     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 = strip_quotes 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 (** (co)inductive **)
    42 
    43 fun inductive_decl coind =
    44   let
    45     fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
    46       if Syntax.is_identifier s then "op " ^ s else "_";
    47     fun mk_params (((recs, ipairs), monos), con_defs) =
    48       let val big_rec_name = space_implode "_" (map (scan_to_id o strip_quotes) recs)
    49           and srec_tms = mk_list recs
    50           and sintrs   = mk_big_list (map snd ipairs)
    51       in
    52         ";\n\n\
    53         \local\n\
    54         \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
    55         \  InductivePackage.add_inductive true " ^
    56         (if coind then "true " else "false ") ^ srec_tms ^ " " ^
    57          sintrs ^ " " ^ mk_list monos ^ " " ^ mk_list con_defs ^ " thy;\n\
    58         \in\n\
    59         \structure " ^ big_rec_name ^ " =\n\
    60         \struct\n\
    61         \  val defs = defs;\n\
    62         \  val mono = mono;\n\
    63         \  val unfold = unfold;\n\
    64         \  val intrs = intrs;\n\
    65         \  val elims = elims;\n\
    66         \  val elim = hd elims;\n\
    67         \  val " ^ (if coind then "co" else "") ^ "induct = induct;\n\
    68         \  val mk_cases = mk_cases;\n\
    69         \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = intrs;\n\
    70         \end;\n\
    71         \val thy = thy;\nend;\n\
    72         \val thy = thy\n"
    73       end
    74     val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
    75     fun optlist s = optional (s $$-- list1 name) []
    76   in
    77     repeat1 name -- ipairs -- optlist "monos" -- optlist "con_defs"
    78       >> mk_params
    79   end;
    80 
    81 
    82 (** datatype **)
    83 
    84 local
    85   (*** generate string for calling add_datatype ***)
    86   (*** and bindig theorems to ML identifiers    ***)
    87 
    88   fun mk_bind_thms_string names =
    89    (case find_first (not o Syntax.is_identifier) names of
    90       Some id => (warning (id ^ " is not a valid identifier"); "")
    91     | None =>
    92         let
    93           fun mk_dt_struct (s, (id, i)) =
    94             s ^ "structure " ^ id ^ " =\n\
    95             \struct\n\
    96             \  val distinct = nth_elem (" ^ i ^ ", distinct);\n\
    97             \  val inject = nth_elem (" ^ i ^ ", inject);\n\
    98             \  val exhaust = nth_elem (" ^ i ^ ", exhaustion);\n\
    99             \  val cases = nth_elem (" ^ i ^ ", case_thms);\n\
   100             \  val (split, split_asm) = nth_elem (" ^ i ^ ", split_thms);\n" ^
   101               (if length names = 1 then
   102                  "  val induct = induction;\n\
   103                  \  val recs = rec_thms;\n\
   104                  \  val simps = simps;\n\
   105                  \  val size = size;\n"
   106                else "") ^
   107             "end;\n";
   108 
   109           val structs = foldl mk_dt_struct
   110             ("", (names ~~ (map string_of_int (0 upto length names - 1))));
   111 
   112         in
   113           (if length names > 1 then
   114              "structure " ^ (space_implode "_" names) ^ " =\n\
   115              \struct\n\
   116              \  val induct = induction;\n\
   117              \  val recs = rec_thms;\n\
   118              \  val simps = simps;\n\
   119              \  val size = size;\nend;\n"
   120            else "") ^ structs
   121         end);
   122 
   123   fun mk_dt_string dts =
   124     let
   125       val names = map (fn ((((alt_name, _), name), _), _) =>
   126         strip_quotes (if_none alt_name name)) dts;
   127 
   128       val add_datatype_args = brackets (commas (map quote names)) ^ " " ^
   129         brackets (commas (map (fn ((((_, vs), name), mx), cs) =>
   130           parens (brackets (commas vs) ^ ", " ^ name ^ ", " ^ mx ^ ", " ^
   131             brackets (commas cs))) dts));
   132 
   133     in
   134       ";\nlocal\n\
   135       \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
   136       \  case_thms, split_thms, induction, size, simps}) =\n\
   137       \  DatatypePackage.add_datatype false " ^ add_datatype_args ^ " thy;\n\
   138       \in\n" ^ mk_bind_thms_string names ^
   139       "val thy = thy;\nend;\nval thy = thy\n"
   140     end;
   141 
   142   fun mk_rep_dt_string (((names, distinct), inject), induct) =
   143     ";\nlocal\n\
   144     \val (thy, {distinct, inject, exhaustion, rec_thms,\n\
   145     \  case_thms, split_thms, induction, size, simps}) =\n\
   146     \  DatatypePackage.rep_datatype " ^
   147     (case names of
   148         Some names => "(Some [" ^ commas_quote names ^ "]) " ^
   149           mk_list (map mk_list distinct) ^ " " ^ mk_list (map mk_list inject) ^
   150             " " ^ induct ^ " thy;\nin\n" ^ mk_bind_thms_string names
   151       | None => "None " ^ mk_list (map mk_list distinct) ^ " " ^
   152           mk_list (map mk_list inject) ^ " " ^ induct ^ " thy;\nin\n") ^
   153     "val thy = thy;\nend;\nval thy = thy\n";
   154 
   155   (*** parsers ***)
   156 
   157   val simple_typ = ident || (type_var >> strip_quotes);
   158 
   159   fun complex_typ toks =
   160     let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
   161         val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")";
   162     in
   163      (typ ^^ (repeat ident >> (cat "" o space_implode " ")) ||
   164       "(" $$-- !! (list1 typ2 >> (parens o commas)) --$$ ")" ^^ !!
   165         (repeat1 ident >> (cat "" o space_implode " "))) toks
   166     end;
   167 
   168   val opt_typs = repeat ((string >> strip_quotes) ||
   169     simple_typ || ("(" $$-- complex_typ --$$ ")"));
   170   val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) =>
   171     parens (n ^ ", " ^ brackets (commas_quote Ts) ^ ", " ^ mx));
   172   val opt_name = optional ("(" $$-- name --$$ ")" >> Some) None
   173 
   174   fun optlistlist s = optional (s $$-- enum "and" (list name)) [[]]
   175 
   176 in
   177   val datatype_decl =
   178     enum1 "and" (opt_name -- type_args -- name -- opt_infix --$$ "=" --
   179       enum1 "|" constructor) >> mk_dt_string;
   180   val rep_datatype_decl =
   181     ((optional ((repeat1 (name >> strip_quotes)) >> Some) None) --
   182       optlistlist "distinct" -- optlistlist "inject" --
   183         ("induct" $$-- name)) >> mk_rep_dt_string;
   184 end;
   185 
   186 
   187 (** primrec **)
   188 
   189 fun mk_primrec_decl (alt_name, eqns) =
   190   let
   191     val names = map (fn (s, _) => if s = "" then "_" else s) eqns
   192   in
   193     ";\nval (thy, " ^ mk_list names ^
   194     ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^
   195       mk_list (map mk_pair (map (apfst quote) eqns)) ^ " " ^ " thy;\n\
   196     \val thy = thy\n"
   197   end;
   198 
   199 (* either names and axioms or just axioms *)
   200 val primrec_decl = (optional ("(" $$-- name --$$ ")") "\"\"" --
   201   (repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl;
   202 
   203 
   204 (** rec: interface to Slind's TFL **)
   205 
   206 
   207 (*fname: name of function being defined; rel: well-founded relation*)
   208 fun mk_rec_decl ((((fname, rel), congs), ss), axms) =
   209   let val fid = strip_quotes fname
   210       val intrnl_name = fid ^ "_Intrnl"
   211   in
   212 	 (";\n\n\
   213           \val _ = writeln \"Recursive function " ^ fid ^ "\"\n\
   214           \val (thy, pats_" ^ intrnl_name ^ ") = Tfl.define thy " ^ 
   215 	                 quote fid ^ " " ^ 
   216 	                 rel ^ "\n" ^ mk_big_list axms ^ ";\n\
   217           \val thy = thy"
   218          ,
   219           "structure " ^ fid ^ " =\n\
   220           \  struct\n\
   221           \  val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\
   222           \  val {rules, induct, tcs} = \n\
   223           \    \t Tfl.simplify_defn (" ^ ss ^ ", " ^ congs ^ ")\n\
   224           \    \t\t  (thy, (" ^ quote fid ^ ", pats_" ^ intrnl_name ^ "))\n\
   225           \  end;\n\
   226           \val pats_" ^ intrnl_name ^ " = ();\n")
   227   end;
   228 
   229 val rec_decl = 
   230     (name -- string -- 
   231      optional ("congs" $$-- string >> strip_quotes) "[]" -- 
   232      optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- 
   233      repeat1 string >> mk_rec_decl) ;
   234 
   235 
   236 
   237 (** augment thy syntax **)
   238 
   239 in
   240 
   241 val _ = ThySyn.add_syntax
   242  ["intrs", "monos", "con_defs", "congs", "simpset", "|",
   243   "and", "distinct", "inject", "induct"]
   244  [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
   245   section "record" "|> RecordPackage.add_record" record_decl,
   246   section "inductive" "" (inductive_decl false),
   247   section "coinductive" "" (inductive_decl true),
   248   section "datatype" "" datatype_decl,
   249   section "rep_datatype" "" rep_datatype_decl,
   250   section "primrec" "" primrec_decl,
   251   ("recdef", rec_decl)];
   252 
   253 end;