--- a/src/HOL/Tools/Datatype/datatype_case.ML Fri Dec 16 10:52:35 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Fri Dec 16 11:02:55 2011 +0100
@@ -130,7 +130,7 @@
names = names,
constraints = cnstrts,
group = in_group'} :: part cs not_in_group
- end
+ end;
in part constructors rows end;
fun v_to_prfx (prfx, Free v :: pats) = (v :: prfx, pats)
@@ -143,7 +143,6 @@
let
val get_info = Datatype_Data.info_of_constr_permissive (Proof_Context.theory_of ctxt);
- val name = singleton (Name.variant_list used) "a";
fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand_var_row", ~1)
| expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
if is_Free p then
@@ -153,7 +152,10 @@
let val capp = list_comb (fresh_constr ty_match ty_inst ty used' c)
in ((prfx, capp :: ps), (subst_free [(p, capp)] rhs, tag)) end
in map expnd constructors end
- else [row]
+ else [row];
+
+ val name = singleton (Name.variant_list used) "a";
+
fun mk _ [] = raise CASE_ERROR ("no rows", ~1)
| mk [] (((_, []), (tm, tag)) :: _) = ([tag], tm) (* Done *)
| mk path (rows as ((row as ((_, [Free _]), _)) :: _ :: _)) = mk path [row]
@@ -277,19 +279,22 @@
val (u', used'') = prep_pat u used';
in (t' $ u', used'') end
| prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
+
fun dest_case1 (t as Const (@{syntax_const "_case1"}, _) $ l $ r) =
let val (l', cnstrts) = strip_constraints l
in ((fst (prep_pat l' (Term.add_free_names t [])), r), cnstrts) end
| dest_case1 t = case_error "dest_case1";
+
fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
| dest_case2 t = [t];
+
val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
- val case_tm =
- make_case_untyped ctxt
- (if err then Error else Warning) []
- (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
- (flat cnstrts) t) cases;
- in case_tm end
+ in
+ make_case_untyped ctxt
+ (if err then Error else Warning) []
+ (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
+ (flat cnstrts) t) cases
+ end
| case_tr _ _ _ = case_error "case_tr";
val trfun_setup =
--- a/src/HOL/Tools/Datatype/primrec.ML Fri Dec 16 10:52:35 2011 +0100
+++ b/src/HOL/Tools/Datatype/primrec.ML Fri Dec 16 11:02:55 2011 +0100
@@ -206,11 +206,11 @@
(* find datatypes which contain all datatypes in tnames' *)
-fun find_dts (dt_info : Datatype_Aux.info Symtab.table) _ [] = []
+fun find_dts _ _ [] = []
| find_dts dt_info tnames' (tname :: tnames) =
(case Symtab.lookup dt_info tname of
NONE => primrec_error (quote tname ^ " is not a datatype")
- | SOME dt =>
+ | SOME (dt : Datatype_Aux.info) =>
if subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
(tname, dt) :: (find_dts dt_info tnames' tnames)
else find_dts dt_info tnames' tnames);
@@ -218,12 +218,12 @@
(* distill primitive definition(s) from primrec specification *)
-fun distill lthy fixes eqs =
+fun distill ctxt fixes eqs =
let
- val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
+ val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed ctxt v
orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) eqs [];
val tnames = distinct (op =) (map (#1 o snd) eqns);
- val dts = find_dts (Datatype_Data.get_all (Proof_Context.theory_of lthy)) tnames tnames;
+ val dts = find_dts (Datatype_Data.get_all (Proof_Context.theory_of ctxt)) tnames tnames;
val main_fns = map (fn (tname, {index, ...}) =>
(index, (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns)) dts;
val {descr, rec_names, rec_rewrites, ...} =
@@ -232,7 +232,7 @@
else snd (hd dts);
val (fnames, fnss) = fold_rev (process_fun descr eqns) main_fns ([], []);
val (fs, raw_defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []);
- val defs = map (make_def lthy fixes fs) raw_defs;
+ val defs = map (make_def ctxt fixes fs) raw_defs;
val names = map snd fnames;
val names_eqns = map fst eqns;
val _ =
@@ -241,17 +241,17 @@
"\nare not mutually recursive");
val rec_rewrites' = map mk_meta_eq rec_rewrites;
val prefix = space_implode "_" (map (Long_Name.base_name o #1) raw_defs);
- fun prove lthy defs =
+ fun prove ctxt defs =
let
- val frees = fold (Variable.add_free_names lthy) eqs [];
+ val frees = fold (Variable.add_free_names ctxt) eqs [];
val rewrites = rec_rewrites' @ map (snd o snd) defs;
fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
- in map (fn eq => Goal.prove lthy frees [] eq tac) eqs end;
+ in map (fn eq => Goal.prove ctxt frees [] eq tac) eqs end;
in ((prefix, (fs, defs)), prove) end
handle PrimrecError (msg, some_eqn) =>
error ("Primrec definition error:\n" ^ msg ^
(case some_eqn of
- SOME eqn => "\nin\n" ^ quote (Syntax.string_of_term lthy eqn)
+ SOME eqn => "\nin\n" ^ quote (Syntax.string_of_term ctxt eqn)
| NONE => ""));
@@ -259,7 +259,7 @@
fun add_primrec_simple fixes ts lthy =
let
- val ((prefix, (fs, defs)), prove) = distill lthy fixes ts;
+ val ((prefix, (_, defs)), prove) = distill lthy fixes ts;
in
lthy
|> fold_map Local_Theory.define defs