diff -r 16c4ea954511 -r 8aa51768ade4 thy_syntax.ML --- 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 (); +