diff -r 7a8fe3b95def -r 437e00414994 thy_syntax.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thy_syntax.ML	Fri Nov 04 14:15:29 1994 +0100
@@ -0,0 +1,96 @@
+(*  Title:      HOL/thy_syntax.ML
+    ID:         $Id$
+    Author:     Markus Wenzel and Lawrence C Paulson
+
+Additional theory file sections for HOL.
+
+TODO:
+  datatype, primrec
+*)
+
+structure ThySynData: THY_SYN_DATA =
+struct
+
+open ThyParse;
+
+
+(* subtype *)
+
+fun mk_subtype_decl (((((opt_name, vs), t), mx), rhs), wt) =
+  let
+    val name' = if_none opt_name t;
+    val name = strip_quotes name';
+  in
+    (cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt],
+      ["Rep_" ^ name, "Rep_" ^ name ^ "_inverse", "Abs_" ^ name ^ "_inverse"])
+  end;
+
+val subtype_decl =
+  optional ("(" $$-- name --$$ ")" >> Some) None --
+  type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
+  >> mk_subtype_decl;
+
+
+(* (co)inductive *)
+
+(*co is either "" or "Co"*)
+fun inductive_decl co =
+  let
+      fun mk_intr_name (s,_) =  (*the "op" cancels any infix status*)
+	  if Syntax.is_identifier s then "op " ^ s  else "_"
+      fun mk_params (((recs, ipairs), monos), con_defs) =
+        let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
+	    and srec_tms = mk_list recs
+            and sintrs   = mk_big_list (map snd ipairs)
+            val stri_name = big_rec_name ^ "_Intrnl"
+        in
+	   (";\n\n\
+            \structure " ^ stri_name ^ " =\n\
+            \ let open Ind_Syntax in\n\
+            \  struct\n\
+            \  val _ = writeln \"" ^ co ^ 
+	               "Inductive definition " ^ big_rec_name ^ "\"\n\
+            \  val rec_tms\t= map (readtm (sign_of thy) termTVar) "
+	                     ^ srec_tms ^ "\n\
+            \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
+	                     ^ sintrs ^ "\n\
+            \  end\n\
+            \ end;\n\n\
+            \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^ 
+	       stri_name ^ ".rec_tms, " ^
+               stri_name ^ ".intr_tms)"
+           ,
+	    "structure " ^ big_rec_name ^ " =\n\
+            \  struct\n\
+            \  structure Result = " ^ co ^ "Ind_section_Fun\n\
+            \  (open " ^ stri_name ^ "\n\
+            \   val thy\t\t= thy\n\
+            \   val monos\t\t= " ^ monos ^ "\n\
+            \   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
+            \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
+            \  open Result\n\
+            \  end\n"
+	   )
+	end
+      val ipairs  = "intrs"   $$-- repeat1 (ident -- !! string)
+      fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
+  in repeat1 string -- ipairs -- optstring "monos" -- optstring "con_defs"
+     >> mk_params
+  end;
+
+
+(* sections *)
+
+val user_keywords = ["|", "intrs", "monos", "con_defs"];
+
+val user_sections =
+ [axm_section "subtype" "|> Subtype.add_subtype" subtype_decl,
+  ("inductive", inductive_decl ""),
+  ("coinductive", inductive_decl "Co")];
+
+
+end;
+
+
+structure ThySyn = ThySynFun(ThySynData);
+init_thy_reader ();