# HG changeset patch # User huffman # Date 1267394721 28800 # Node ID c23b42730b9b1853d052716f1a8e50933e3efecb # Parent 94bb9f59d4e9c669c1610b113488b88af2642966 move case combinator syntax to domain_constructors.ML diff -r 94bb9f59d4e9 -r c23b42730b9b src/HOLCF/Tools/Domain/domain_constructors.ML --- 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; diff -r 94bb9f59d4e9 -r c23b42730b9b src/HOLCF/Tools/Domain/domain_syntax.ML --- 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 *)