--- a/thy_syntax.ML Mon Nov 21 17:50:34 1994 +0100
+++ b/thy_syntax.ML Wed Nov 23 10:36:03 1994 +0100
@@ -1,20 +1,23 @@
(* Title: HOL/thy_syntax.ML
ID: $Id$
- Author: Markus Wenzel and Lawrence C Paulson
+ Author: Markus Wenzel and Lawrence C Paulson and Carsten Clasohm
Additional theory file sections for HOL.
TODO:
- datatype, primrec
+ move datatype / primrec stuff to pre_datatype.ML (?)
*)
+(*the kind of distinctiveness axioms depends on number of constructors*)
+val dtK = 5; (* FIXME remove from datatype.ML, rename *)
+
structure ThySynData: THY_SYN_DATA =
struct
open ThyParse;
-(* subtype *)
+(** subtype **)
fun mk_subtype_decl (((((opt_name, vs), t), mx), rhs), wt) =
let
@@ -22,7 +25,8 @@
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"])
+ [name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse",
+ "Abs_" ^ name ^ "_inverse"])
end;
val subtype_decl =
@@ -31,62 +35,149 @@
>> mk_subtype_decl;
-(* (co)inductive *)
+
+(** (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
+ 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 *)
+
+(** datatype **)
+
+local
+ (* FIXME err -> add_datatype *)
+ fun mk_cons cs =
+ (case duplicates (map (fst o fst) cs) of
+ [] => map (fn ((s, ts), syn) => mk_triple (s, mk_list ts, syn)) cs
+ | dups => error ("Duplicate constructors: " ^ commas_quote dups));
+
+ (*generate names of distinctiveness axioms*)
+ fun mk_distinct_rules cs tname =
+ let
+ val uqcs = map (fn ((s, _), _) => strip_quotes s) cs;
+ (*combine all constructor names with all others w/o duplicates*)
+ fun neg_one c = map (fn c2 => quote (c ^ "_not_" ^ c2));
+ fun neg1 [] = []
+ | neg1 (c1 :: cs) = neg_one c1 cs @ neg1 cs;
+ in
+ if length uqcs < dtK then neg1 uqcs
+ else quote (tname ^ "_ord_distinct") ::
+ map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
+ end;
+
+ fun mk_rules tname cons pre = " map (get_axiom thy) " ^
+ mk_list (map (fn ((s, _), _) => quote (tname ^ pre ^ strip_quotes s)) cons);
-val user_keywords = ["|", "intrs", "monos", "con_defs"];
+ (*generate string for calling add_datatype*)
+ fun mk_params ((ts, tname), cons) =
+ ("val (thy, " ^ tname ^ "_add_primrec) = add_datatype\n"
+ ^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
+ \val thy = thy",
+ "structure " ^ tname ^ " =\n\
+ \struct\n\
+ \ val inject = map (get_axiom thy) " ^
+ mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s))
+ (filter_out (null o snd o fst) cons)) ^ ";\n\
+ \ val distinct = " ^
+ (if length cons < dtK then "let val distinct' = " else "") ^
+ "map (get_axiom thy) " ^ mk_list (mk_distinct_rules cons tname) ^
+ (if length cons < dtK then
+ " in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
+ \ distinct') end"
+ else "") ^ ";\n\
+ \ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
+ \ val cases =" ^ mk_rules tname cons "_case_" ^ ";\n\
+ \ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\
+ \ val simps = inject @ distinct @ cases @ recs;\n\
+ \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
+ \end;\n");
+
+ (*parsers*)
+ val tvars = type_args >> map (cat "dtVar");
+ val typ =
+ tvars -- name >> (cat "dtTyp" o mk_pair o apfst mk_list) ||
+ type_var >> cat "dtVar";
+ val opt_typs = optional ("(" $$-- list1 typ --$$ ")") [];
+ val constructor = name -- opt_typs -- opt_mixfix;
+in
+ val datatype_decl =
+ (* FIXME tvars -> type_args *)
+ tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params;
+end;
+
+
+
+(** primrec **)
+
+(* FIXME add_thms_as_axms (?) *)
+
+fun mk_primrec_decl ((fname, tname), axms) =
+ let
+ fun mk_prove (name, eqn) =
+ "val " ^ name ^ " = prove_goalw thy [get_def thy " ^ fname ^ "] " ^ eqn ^ "\n\
+ \ (fn _ => [simp_tac (HOL_ss addsimps " ^ tname ^ ".recs) 1])";
+ val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
+ in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)) end;
+
+val primrec_decl =
+ name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl;
+
+
+
+(** 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")];
+ ("coinductive", inductive_decl "Co"),
+ ("datatype", datatype_decl),
+ ("primrec", primrec_decl)];
end;
@@ -94,3 +185,4 @@
structure ThySyn = ThySynFun(ThySynData);
init_thy_reader ();
+