--- /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 ();