Domain package generates match functions for new datatypes, for use with the fixrec package
--- a/src/HOLCF/domain/axioms.ML Sat Jun 04 00:23:40 2005 +0200
+++ b/src/HOLCF/domain/axioms.ML Sat Jun 04 00:24:33 2005 +0200
@@ -61,6 +61,13 @@
(if con'=con then %%:"TT" else %%:"FF") args)) cons))
in map ddef cons end;
+ val mat_defs = let
+ fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) ==
+ mk_cRep_CFun(%%:(dname^"_when"),map
+ (fn (con',args) => (foldr /\#
+ (if con'=con then (%%:"return")`(mk_ctuple (map (bound_arg args) args)) else %%:"fail") args)) cons))
+ in map mdef cons end;
+
val sel_defs = let
fun sdef con n arg = (sel_of arg^"_def",%%:(sel_of arg) ==
mk_cRep_CFun(%%:(dname^"_when"),map
@@ -81,7 +88,7 @@
in (dnam,
[abs_iso_ax, rep_iso_ax, reach_ax],
[when_def, copy_def] @
- con_defs @ dis_defs @ sel_defs @
+ con_defs @ dis_defs @ mat_defs @ sel_defs @
[take_def, finite_def])
end; (* let *)
--- a/src/HOLCF/domain/library.ML Sat Jun 04 00:23:40 2005 +0200
+++ b/src/HOLCF/domain/library.ML Sat Jun 04 00:24:33 2005 +0200
@@ -56,6 +56,8 @@
| _ => con;
fun dis_name con = "is_"^ (extern_name con);
fun dis_name_ con = "is_"^ (strip_esc con);
+fun mat_name con = "match_"^ (extern_name con);
+fun mat_name_ con = "match_"^ (strip_esc con);
(* make distinct names out of the type list,
forbidding "o","n..","x..","f..","P.." as names *)
@@ -174,6 +176,12 @@
fun strict f = f`UU === UU;
fun defined t = t ~= UU;
fun cpair (S,T) = %%:"cpair"`S`T;
+fun mk_ctuple [] = %%:"UU" (* used in match_defs *)
+| mk_ctuple (t::[]) = t
+| mk_ctuple (t::ts) = cpair (t, mk_ctuple ts);
+fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *)
+| mk_ctupleT (T::[]) = T
+| mk_ctupleT (T::Ts) = mk_prodT(T, mk_ctupleT Ts);
fun lift_defined f = lift (fn x => defined (f x));
fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
--- a/src/HOLCF/domain/syntax.ML Sat Jun 04 00:23:40 2005 +0200
+++ b/src/HOLCF/domain/syntax.ML Sat Jun 04 00:24:33 2005 +0200
@@ -47,10 +47,13 @@
(* stricly speaking, these constants have one argument,
but the mixfix (without arguments) is introduced only
to generate parse rules for non-alphanumeric names*)
+ fun mat (con ,s,args) = (mat_name_ con, dtype->>mk_ssumT(oneT,mk_uT(mk_ctupleT(map third args))),
+ Mixfix(escape ("match_" ^ con), [], Syntax.max_pri));
fun sel (_ ,_,args) = map (fn(_,sel,typ)=>(sel,dtype ->> typ,NoSyn))args;
in
val consts_con = map con cons';
val consts_dis = map dis cons';
+ val consts_mat = map mat cons';
val consts_sel = List.concat(map sel cons');
end;
@@ -87,7 +90,7 @@
end;
in ([const_rep, const_abs, const_when, const_copy] @
- consts_con @ consts_dis @ consts_sel @
+ consts_con @ consts_dis @ consts_mat @ consts_sel @
[const_take, const_finite],
[case_trans])
end; (* let *)
--- a/src/HOLCF/domain/theorems.ML Sat Jun 04 00:23:40 2005 +0200
+++ b/src/HOLCF/domain/theorems.ML Sat Jun 04 00:24:33 2005 +0200
@@ -69,6 +69,7 @@
val ax_when_def = ga "when_def" dname;
val axs_con_def = map (fn (con,_) => ga (extern_name con^"_def") dname) cons;
val axs_dis_def = map (fn (con,_) => ga ( dis_name con^"_def") dname) cons;
+val axs_mat_def = map (fn (con,_) => ga ( mat_name con^"_def") dname) cons;
val axs_sel_def = List.concat(map (fn (_,args) =>
map (fn arg => ga (sel_of arg ^"_def") dname) args)
cons);
@@ -83,8 +84,8 @@
val x_name = "x";
val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso];
-val abs_strict = iso_locale RS iso_abs_strict;
-val rep_strict = iso_locale RS iso_rep_strict;
+val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
+val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
val abs_defin' = iso_locale RS iso_abs_defin';
val rep_defin' = iso_locale RS iso_rep_defin';
val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
@@ -217,6 +218,18 @@
(HOLCF_ss addsimps dis_apps) 1))]) cons;
in dis_stricts @ dis_defins @ dis_apps end;
+val mat_rews = let
+ val mat_stricts = map (fn (con,_) => pg axs_mat_def (mk_trp(
+ strict(%%:(mat_name con)))) [
+ rtac when_strict 1]) cons;
+ val mat_apps = let fun one_mat c (con,args)= pg axs_mat_def
+ (lift_defined %: (nonlazy args,
+ (mk_trp((%%:(mat_name c))`(con_app con args) ===
+ (if con=c then (%%:"return")`(mk_ctuple (map %# args)) else %%:"fail"))))) [
+ asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
+ in List.concat(map (fn (c,_) => map (one_mat c) cons) cons) end;
+in mat_stricts @ mat_apps end;
+
val con_stricts = List.concat(map (fn (con,args) => map (fn vn =>
pg con_appls
(mk_trp(con_app2 con (fn arg => if vname arg = vn
@@ -263,7 +276,7 @@
(lift_defined %: ((nonlazy args1),
(mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([
rtac rev_contrapos 1,
- eres_inst_tac[("fo",dis_name con1)] monofun_cfun_arg 1]
+ eres_inst_tac[("f",dis_name con1)] monofun_cfun_arg 1]
@map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2)
@[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]);
fun distinct (con1,args1) (con2,args2) =
@@ -304,7 +317,7 @@
val inverts = map (fn (con,args) =>
pgterm (op <<) con args (List.concat(map (fn arg => [
TRY(rtac conjI 1),
- dres_inst_tac [("fo",sel_of arg)] monofun_cfun_arg 1,
+ dres_inst_tac [("f",sel_of arg)] monofun_cfun_arg 1,
asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1]
) args))) cons';
val injects = map (fn ((con,args),inv_thm) =>
@@ -320,8 +333,7 @@
(* ----- theorems concerning one induction step ----------------------------- *)
val copy_strict = pg[ax_copy_def](mk_trp(strict(dc_copy`%"f"))) [
- asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict,
- cfst_strict,csnd_strict]) 1];
+ asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict]) 1];
val copy_apps = map (fn (con,args) => pg [ax_copy_def]
(lift_defined %: (nonlazy_rec args,
mk_trp(dc_copy`%"f"`(con_app con args) ===
@@ -333,7 +345,7 @@
simp_tac (HOLCF_ss addsimps con_appls) 1]))cons;
val copy_stricts = map (fn (con,args) => pg [] (mk_trp(dc_copy`UU`
(con_app con args) ===UU))
- (let val rews = cfst_strict::csnd_strict::copy_strict::copy_apps@con_rews
+ (let val rews = copy_strict::copy_apps@con_rews
in map (case_UU_tac rews 1) (nonlazy args) @ [
asm_simp_tac (HOLCF_ss addsimps rews) 1] end))
(List.filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
@@ -347,6 +359,7 @@
("con_rews", con_rews),
("sel_rews", sel_rews),
("dis_rews", dis_rews),
+ ("match_rews", mat_rews),
("dist_les", dist_les),
("dist_eqs", dist_eqs),
("inverts" , inverts ),
@@ -390,8 +403,7 @@
(* ----- theorems concerning finite approximation and finite induction ------ *)
local
- val iterate_Cprod_ss = simpset_of Fix.thy
- addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews;
+ val iterate_Cprod_ss = simpset_of Fix.thy;
val copy_con_rews = copy_rews @ con_rews;
val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>