--- a/datatype.ML Wed Nov 23 10:41:42 1994 +0100
+++ b/datatype.ML Wed Nov 23 15:09:44 1994 +0100
@@ -1,108 +1,10 @@
-(* Title: HOL/Datatype
- ID: $Id$
- Author: Max Breitling, Carsten Clasohm,
- Tobias Nipkow, Norbert Voelker
+(* Title: HOL/datatype.ML
+ ID: $Id$
+ Author: Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker
Copyright 1994 TU Muenchen
*)
-(*choice between Ci_neg1 and Ci_neg2 axioms depends on number of constructors*)
-local
-
- val dtK = 5
-
-in
-
-local open ThyParse in
- val datatype_decls =
- let
- val tvar = type_var >> (fn s => "dtVar" ^ s);
-
- val type_var_list =
- tvar >> (fn s => [s]) || "(" $$-- list1 tvar --$$ ")";
-
- val typ =
- ident >> (fn s => "dtTyp([]," ^ quote s ^")")
- ||
- type_var_list -- ident >> (fn (ts, id) => "dtTyp(" ^ mk_list ts ^
- "," ^ quote id ^ ")")
- ||
- tvar;
-
- val typ_list = "(" $$-- list1 typ --$$ ")" || empty;
-
- val cons = name -- typ_list -- opt_mixfix;
-
- fun constructs ts =
- ( cons --$$ "|" -- constructs >> op::
- ||
- cons >> (fn c => [c])) ts;
-
- fun mk_cons cs =
- case findrep (map (fst o fst) cs) of
- [] => map (fn ((s,ts),syn) => parens(commas [s,mk_list ts,syn])) cs
- | c::_ => error("Constructor \"" ^ c ^ "\" occurs twice");
-
- (*remove all quotes from a string*)
- val rem_quotes = implode o filter (fn c => c <> "\"") o explode;
-
- (*generate names of distinct axioms*)
- fun rules_distinct cs tname =
- let val uqcs = map (fn ((s,_),_) => rem_quotes s) cs;
- (*combine all constructor names with all others w/o duplicates*)
- fun negOne c = map (fn c2 => quote (c ^ "_not_" ^ c2));
- fun neg1 [] = []
- | neg1 (c1 :: cs) = (negOne 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 rules tname cons pre =
- " map (get_axiom thy) " ^
- mk_list (map (fn ((s,_),_) => quote(tname ^ pre ^ rem_quotes s))
- cons)
-
- (*generate string for calling 'add_datatype'*)
- fun mk_params ((ts, tname), cons) =
- ("val (thy," ^ tname ^ "_add_primrec) = add_datatype\n" ^
- parens (commas [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_" ^ rem_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 (rules_distinct 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 =" ^ rules tname cons "_case_" ^ ";\n\
- \ val recs =" ^ 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")
- in
- (type_var_list || empty) -- ident --$$ "=" -- constructs >> mk_params
-end
-
-val primrec_decl =
- let fun mkstrings((fname,tname),axms) =
- let fun 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 prove axms))
- end
- in name -- long_id -- repeat1 (ident -- string) >> mkstrings end
-end;
-
(*used for constructor parameters*)
datatype dt_type = dtVar of string |
dtTyp of dt_type list * string |
@@ -111,7 +13,7 @@
local
val mysort = sort;
-open ThyParse
+open ThyParse;
exception Impossible;
exception RecError of string;
@@ -542,4 +444,3 @@
|> add_axioms rules,add_primrec)
end
end
-end;