--- a/src/HOLCF/Tools/Domain/domain_constructors.ML Sun Feb 28 12:59:53 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sun Feb 28 14:05:21 2010 -0800
@@ -634,6 +634,48 @@
fun case_const T = Const (case_name, caseT T);
val case_app = list_ccomb (case_const resultT, fs);
+ (* define syntax for case combinator *)
+ (* TODO: re-implement case syntax using a parse translation *)
+ local
+ open Syntax
+ open Domain_Library
+ fun syntax c = Syntax.mark_const (fst (dest_Const c));
+ fun xconst c = Long_Name.base_name (fst (dest_Const c));
+ fun c_ast authentic con =
+ Constant (if authentic then syntax con else xconst con);
+ fun expvar n = Variable ("e" ^ string_of_int n);
+ fun argvar n m _ = Variable ("a" ^ string_of_int n ^ "_" ^ string_of_int m);
+ fun argvars n args = mapn (argvar n) 1 args;
+ fun app s (l, r) = mk_appl (Constant s) [l, r];
+ val cabs = app "_cabs";
+ val capp = app @{const_syntax Rep_CFun};
+ val capps = Library.foldl capp
+ fun con1 authentic n (con,args) =
+ Library.foldl capp (c_ast authentic con, argvars n args);
+ fun case1 authentic n c =
+ app "_case1" (con1 authentic n c, expvar n);
+ fun arg1 n (con,args) = List.foldr cabs (expvar n) (argvars n args);
+ fun when1 n m = if n = m then arg1 n else K (Constant @{const_syntax UU});
+ val case_constant = Constant (syntax (case_const dummyT));
+ fun case_trans authentic =
+ ParsePrintRule
+ (app "_case_syntax"
+ (Variable "x",
+ foldr1 (app "_case2") (mapn (case1 authentic) 1 spec)),
+ capp (capps (case_constant, mapn arg1 1 spec), Variable "x"));
+ fun one_abscon_trans authentic n c =
+ ParsePrintRule
+ (cabs (con1 authentic n c, expvar n),
+ capps (case_constant, mapn (when1 n) 1 spec));
+ fun abscon_trans authentic =
+ mapn (one_abscon_trans authentic) 1 spec;
+ val trans_rules : ast Syntax.trrule list =
+ case_trans false :: case_trans true ::
+ abscon_trans false @ abscon_trans true;
+ in
+ val thy = Sign.add_trrules_i trans_rules thy;
+ end;
+
(* prove beta reduction rule for case combinator *)
val case_beta = beta_of_def thy case_def;
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML Sun Feb 28 12:59:53 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Sun Feb 28 14:05:21 2010 -0800
@@ -12,7 +12,7 @@
typ ->
(string * typ list) *
(binding * (bool * binding option * typ) list * mixfix) list ->
- (binding * typ * mixfix) list * ast Syntax.trrule list
+ (binding * typ * mixfix) list
val add_syntax:
bool ->
@@ -34,7 +34,7 @@
(dtypeprod : typ)
((dname : string, typevars : typ list),
(cons': (binding * (bool * binding option * typ) list * mixfix) list))
- : (binding * typ * mixfix) list * ast Syntax.trrule list =
+ : (binding * typ * mixfix) list =
let
(* ----- constants concerning the isomorphism ------------------------------- *)
local
@@ -60,51 +60,11 @@
val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn);
val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn);
-(* ----- case translation --------------------------------------------------- *)
-
- fun syntax b = Syntax.mark_const (Sign.full_bname thy b);
-
- local open Syntax in
- local
- fun c_ast authentic con = Constant ((authentic ? syntax) (Binding.name_of con));
- fun expvar n = Variable ("e" ^ string_of_int n);
- fun argvar n m _ = Variable ("a" ^ string_of_int n ^ "_" ^ string_of_int m);
- fun argvars n args = mapn (argvar n) 1 args;
- fun app s (l, r) = mk_appl (Constant s) [l, r];
- val cabs = app "_cabs";
- val capp = app @{const_syntax Rep_CFun};
- fun con1 authentic n (con,args,mx) =
- Library.foldl capp (c_ast authentic con, argvars n args);
- fun case1 authentic n (con,args,mx) =
- app "_case1" (con1 authentic n (con,args,mx), expvar n);
- fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args);
- fun when1 n m = if n = m then arg1 n else K (Constant @{const_syntax UU});
-
- fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
- fun app_pat x = mk_appl (Constant "_pat") [x];
- fun args_list [] = Constant "_noargs"
- | args_list xs = foldr1 (app "_args") xs;
- in
- fun case_trans authentic =
- ParsePrintRule
- (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn (case1 authentic) 1 cons')),
- capp (Library.foldl capp
- (Constant (syntax (dnam ^ "_when")), mapn arg1 1 cons'), Variable "x"));
-
- fun one_abscon_trans authentic n (con,mx,args) =
- ParsePrintRule
- (cabs (con1 authentic n (con,mx,args), expvar n),
- Library.foldl capp (Constant (syntax (dnam ^ "_when")), mapn (when1 n) 1 cons'));
- fun abscon_trans authentic = mapn (one_abscon_trans authentic) 1 cons';
-
- end;
- end;
val optional_consts =
if definitional then [] else [const_rep, const_abs, const_copy];
in (optional_consts @ [const_when] @
- [const_take, const_finite],
- (case_trans false :: case_trans true :: (abscon_trans false @ abscon_trans true)))
+ [const_take, const_finite])
end; (* let *)
(* ----- putting all the syntax stuff together ------------------------------ *)
@@ -126,15 +86,14 @@
(Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn);
val const_bisim =
(Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn);
- val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list =
+ val ctt : (binding * typ * mixfix) list list =
map (calc_syntax thy'' definitional funprod) eqs';
in thy''
|> Cont_Consts.add_consts
- (maps fst ctt @
+ (flat ctt @
(if length eqs'>1 andalso not definitional
then [const_copy] else []) @
[const_bisim])
- |> Sign.add_trrules_i (maps snd ctt)
end; (* let *)
end; (* struct *)