# HG changeset patch # User huffman # Date 1274725789 25200 # Node ID e67760c1b851c3911c2e9fd8b01f04593f15c1f2 # Parent 00f13d3ad47473d7769ba4a2c2ab856fc31c91d0 move unused pattern match syntax stuff into HOLCF/ex diff -r 00f13d3ad474 -r e67760c1b851 src/HOLCF/Fixrec.thy --- a/src/HOLCF/Fixrec.thy Mon May 24 09:32:52 2010 -0700 +++ b/src/HOLCF/Fixrec.thy Mon May 24 11:29:49 2010 -0700 @@ -64,7 +64,6 @@ "case m of XCONST fail \ t1 | XCONST succeed\x \ t2" == "CONST match_case\t1\(\ x. t2)\m" - subsubsection {* Run operator *} definition @@ -109,334 +108,6 @@ lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)" by (cases x, simp_all) -subsubsection {* Fatbar combinator *} - -definition - fatbar :: "('a \ 'b match) \ ('a \ 'b match) \ ('a \ 'b match)" where - "fatbar = (\ a b x. a\x +++ b\x)" - -abbreviation - fatbar_syn :: "['a \ 'b match, 'a \ 'b match] \ 'a \ 'b match" (infixr "\" 60) where - "m1 \ m2 == fatbar\m1\m2" - -lemma fatbar1: "m\x = \ \ (m \ ms)\x = \" -by (simp add: fatbar_def) - -lemma fatbar2: "m\x = fail \ (m \ ms)\x = ms\x" -by (simp add: fatbar_def) - -lemma fatbar3: "m\x = succeed\y \ (m \ ms)\x = succeed\y" -by (simp add: fatbar_def) - -lemmas fatbar_simps = fatbar1 fatbar2 fatbar3 - -lemma run_fatbar1: "m\x = \ \ run\((m \ ms)\x) = \" -by (simp add: fatbar_def) - -lemma run_fatbar2: "m\x = fail \ run\((m \ ms)\x) = run\(ms\x)" -by (simp add: fatbar_def) - -lemma run_fatbar3: "m\x = succeed\y \ run\((m \ ms)\x) = y" -by (simp add: fatbar_def) - -lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3 - -subsection {* Case branch combinator *} - -definition - branch :: "('a \ 'b match) \ ('b \ 'c) \ ('a \ 'c match)" where - "branch p \ \ r x. match_case\fail\(\ y. succeed\(r\y))\(p\x)" - -lemma branch_simps: - "p\x = \ \ branch p\r\x = \" - "p\x = fail \ branch p\r\x = fail" - "p\x = succeed\y \ branch p\r\x = succeed\(r\y)" -by (simp_all add: branch_def) - -lemma branch_succeed [simp]: "branch succeed\r\x = succeed\(r\x)" -by (simp add: branch_def) - -subsubsection {* Cases operator *} - -definition - cases :: "'a match \ 'a::pcpo" where - "cases = match_case\\\ID" - -text {* rewrite rules for cases *} - -lemma cases_strict [simp]: "cases\\ = \" -by (simp add: cases_def) - -lemma cases_fail [simp]: "cases\fail = \" -by (simp add: cases_def) - -lemma cases_succeed [simp]: "cases\(succeed\x) = x" -by (simp add: cases_def) - -subsection {* Case syntax *} - -nonterminals - Case_syn Cases_syn - -syntax - "_Case_syntax":: "['a, Cases_syn] => 'b" ("(Case _ of/ _)" 10) - "_Case1" :: "['a, 'b] => Case_syn" ("(2_ =>/ _)" 10) - "" :: "Case_syn => Cases_syn" ("_") - "_Case2" :: "[Case_syn, Cases_syn] => Cases_syn" ("_/ | _") - -syntax (xsymbols) - "_Case1" :: "['a, 'b] => Case_syn" ("(2_ \/ _)" 10) - -translations - "_Case_syntax x ms" == "CONST Fixrec.cases\(ms\x)" - "_Case2 m ms" == "m \ ms" - -text {* Parsing Case expressions *} - -syntax - "_pat" :: "'a" - "_variable" :: "'a" - "_noargs" :: "'a" - -translations - "_Case1 p r" => "CONST branch (_pat p)\(_variable p r)" - "_variable (_args x y) r" => "CONST csplit\(_variable x (_variable y r))" - "_variable _noargs r" => "CONST unit_when\r" - -parse_translation {* -(* rewrite (_pat x) => (succeed) *) -(* rewrite (_variable x t) => (Abs_CFun (%x. t)) *) - [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.succeed}), - mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_CFun})]; -*} - -text {* Printing Case expressions *} - -syntax - "_match" :: "'a" - -print_translation {* - let - fun dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax unit_when},_) $ t) = - (Syntax.const @{syntax_const "_noargs"}, t) - | dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax csplit},_) $ t) = - let - val (v1, t1) = dest_LAM t; - val (v2, t2) = dest_LAM t1; - in (Syntax.const @{syntax_const "_args"} $ v1 $ v2, t2) end - | dest_LAM (Const (@{const_syntax Abs_CFun},_) $ t) = - let - val abs = - case t of Abs abs => abs - | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0); - val (x, t') = atomic_abs_tr' abs; - in (Syntax.const @{syntax_const "_variable"} $ x, t') end - | dest_LAM _ = raise Match; (* too few vars: abort translation *) - - fun Case1_tr' [Const(@{const_syntax branch},_) $ p, r] = - let val (v, t) = dest_LAM r in - Syntax.const @{syntax_const "_Case1"} $ - (Syntax.const @{syntax_const "_match"} $ p $ v) $ t - end; - - in [(@{const_syntax Rep_CFun}, Case1_tr')] end; -*} - -translations - "x" <= "_match (CONST Fixrec.succeed) (_variable x)" - - -subsection {* Pattern combinators for data constructors *} - -types ('a, 'b) pat = "'a \ 'b match" - -definition - cpair_pat :: "('a, 'c) pat \ ('b, 'd) pat \ ('a \ 'b, 'c \ 'd) pat" where - "cpair_pat p1 p2 = (\(x, y). - match_case\fail\(\ a. match_case\fail\(\ b. succeed\(a, b))\(p2\y))\(p1\x))" - -definition - spair_pat :: - "('a, 'c) pat \ ('b, 'd) pat \ ('a::pcpo \ 'b::pcpo, 'c \ 'd) pat" where - "spair_pat p1 p2 = (\(:x, y:). cpair_pat p1 p2\(x, y))" - -definition - sinl_pat :: "('a, 'c) pat \ ('a::pcpo \ 'b::pcpo, 'c) pat" where - "sinl_pat p = sscase\p\(\ x. fail)" - -definition - sinr_pat :: "('b, 'c) pat \ ('a::pcpo \ 'b::pcpo, 'c) pat" where - "sinr_pat p = sscase\(\ x. fail)\p" - -definition - up_pat :: "('a, 'b) pat \ ('a u, 'b) pat" where - "up_pat p = fup\p" - -definition - TT_pat :: "(tr, unit) pat" where - "TT_pat = (\ b. If b then succeed\() else fail fi)" - -definition - FF_pat :: "(tr, unit) pat" where - "FF_pat = (\ b. If b then fail else succeed\() fi)" - -definition - ONE_pat :: "(one, unit) pat" where - "ONE_pat = (\ ONE. succeed\())" - -text {* Parse translations (patterns) *} -translations - "_pat (XCONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)" - "_pat (XCONST spair\x\y)" => "CONST spair_pat (_pat x) (_pat y)" - "_pat (XCONST sinl\x)" => "CONST sinl_pat (_pat x)" - "_pat (XCONST sinr\x)" => "CONST sinr_pat (_pat x)" - "_pat (XCONST up\x)" => "CONST up_pat (_pat x)" - "_pat (XCONST TT)" => "CONST TT_pat" - "_pat (XCONST FF)" => "CONST FF_pat" - "_pat (XCONST ONE)" => "CONST ONE_pat" - -text {* CONST version is also needed for constructors with special syntax *} -translations - "_pat (CONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)" - "_pat (CONST spair\x\y)" => "CONST spair_pat (_pat x) (_pat y)" - -text {* Parse translations (variables) *} -translations - "_variable (XCONST Pair x y) r" => "_variable (_args x y) r" - "_variable (XCONST spair\x\y) r" => "_variable (_args x y) r" - "_variable (XCONST sinl\x) r" => "_variable x r" - "_variable (XCONST sinr\x) r" => "_variable x r" - "_variable (XCONST up\x) r" => "_variable x r" - "_variable (XCONST TT) r" => "_variable _noargs r" - "_variable (XCONST FF) r" => "_variable _noargs r" - "_variable (XCONST ONE) r" => "_variable _noargs r" - -translations - "_variable (CONST Pair x y) r" => "_variable (_args x y) r" - "_variable (CONST spair\x\y) r" => "_variable (_args x y) r" - -text {* Print translations *} -translations - "CONST Pair (_match p1 v1) (_match p2 v2)" - <= "_match (CONST cpair_pat p1 p2) (_args v1 v2)" - "CONST spair\(_match p1 v1)\(_match p2 v2)" - <= "_match (CONST spair_pat p1 p2) (_args v1 v2)" - "CONST sinl\(_match p1 v1)" <= "_match (CONST sinl_pat p1) v1" - "CONST sinr\(_match p1 v1)" <= "_match (CONST sinr_pat p1) v1" - "CONST up\(_match p1 v1)" <= "_match (CONST up_pat p1) v1" - "CONST TT" <= "_match (CONST TT_pat) _noargs" - "CONST FF" <= "_match (CONST FF_pat) _noargs" - "CONST ONE" <= "_match (CONST ONE_pat) _noargs" - -lemma cpair_pat1: - "branch p\r\x = \ \ branch (cpair_pat p q)\(csplit\r)\(x, y) = \" -apply (simp add: branch_def cpair_pat_def) -apply (cases "p\x", simp_all) -done - -lemma cpair_pat2: - "branch p\r\x = fail \ branch (cpair_pat p q)\(csplit\r)\(x, y) = fail" -apply (simp add: branch_def cpair_pat_def) -apply (cases "p\x", simp_all) -done - -lemma cpair_pat3: - "branch p\r\x = succeed\s \ - branch (cpair_pat p q)\(csplit\r)\(x, y) = branch q\s\y" -apply (simp add: branch_def cpair_pat_def) -apply (cases "p\x", simp_all) -apply (cases "q\y", simp_all) -done - -lemmas cpair_pat [simp] = - cpair_pat1 cpair_pat2 cpair_pat3 - -lemma spair_pat [simp]: - "branch (spair_pat p1 p2)\r\\ = \" - "\x \ \; y \ \\ - \ branch (spair_pat p1 p2)\r\(:x, y:) = - branch (cpair_pat p1 p2)\r\(x, y)" -by (simp_all add: branch_def spair_pat_def) - -lemma sinl_pat [simp]: - "branch (sinl_pat p)\r\\ = \" - "x \ \ \ branch (sinl_pat p)\r\(sinl\x) = branch p\r\x" - "y \ \ \ branch (sinl_pat p)\r\(sinr\y) = fail" -by (simp_all add: branch_def sinl_pat_def) - -lemma sinr_pat [simp]: - "branch (sinr_pat p)\r\\ = \" - "x \ \ \ branch (sinr_pat p)\r\(sinl\x) = fail" - "y \ \ \ branch (sinr_pat p)\r\(sinr\y) = branch p\r\y" -by (simp_all add: branch_def sinr_pat_def) - -lemma up_pat [simp]: - "branch (up_pat p)\r\\ = \" - "branch (up_pat p)\r\(up\x) = branch p\r\x" -by (simp_all add: branch_def up_pat_def) - -lemma TT_pat [simp]: - "branch TT_pat\(unit_when\r)\\ = \" - "branch TT_pat\(unit_when\r)\TT = succeed\r" - "branch TT_pat\(unit_when\r)\FF = fail" -by (simp_all add: branch_def TT_pat_def) - -lemma FF_pat [simp]: - "branch FF_pat\(unit_when\r)\\ = \" - "branch FF_pat\(unit_when\r)\TT = fail" - "branch FF_pat\(unit_when\r)\FF = succeed\r" -by (simp_all add: branch_def FF_pat_def) - -lemma ONE_pat [simp]: - "branch ONE_pat\(unit_when\r)\\ = \" - "branch ONE_pat\(unit_when\r)\ONE = succeed\r" -by (simp_all add: branch_def ONE_pat_def) - - -subsection {* Wildcards, as-patterns, and lazy patterns *} - -definition - wild_pat :: "'a \ unit match" where - "wild_pat = (\ x. succeed\())" - -definition - as_pat :: "('a \ 'b match) \ 'a \ ('a \ 'b) match" where - "as_pat p = (\ x. match_case\fail\(\ a. succeed\(x, a))\(p\x))" - -definition - lazy_pat :: "('a \ 'b::pcpo match) \ ('a \ 'b match)" where - "lazy_pat p = (\ x. succeed\(cases\(p\x)))" - -text {* Parse translations (patterns) *} -translations - "_pat _" => "CONST wild_pat" - -text {* Parse translations (variables) *} -translations - "_variable _ r" => "_variable _noargs r" - -text {* Print translations *} -translations - "_" <= "_match (CONST wild_pat) _noargs" - -lemma wild_pat [simp]: "branch wild_pat\(unit_when\r)\x = succeed\r" -by (simp add: branch_def wild_pat_def) - -lemma as_pat [simp]: - "branch (as_pat p)\(csplit\r)\x = branch p\(r\x)\x" -apply (simp add: branch_def as_pat_def) -apply (cases "p\x", simp_all) -done - -lemma lazy_pat [simp]: - "branch p\r\x = \ \ branch (lazy_pat p)\r\x = succeed\(r\\)" - "branch p\r\x = fail \ branch (lazy_pat p)\r\x = succeed\(r\\)" - "branch p\r\x = succeed\s \ branch (lazy_pat p)\r\x = succeed\s" -apply (simp_all add: branch_def lazy_pat_def) -apply (cases "p\x", simp_all)+ -done - - subsection {* Match functions for built-in types *} default_sort pcpo @@ -584,6 +255,6 @@ (@{const_name UU}, @{const_name match_UU}) ] *} -hide_const (open) succeed fail run cases +hide_const (open) succeed fail run end diff -r 00f13d3ad474 -r e67760c1b851 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Mon May 24 09:32:52 2010 -0700 +++ b/src/HOLCF/IsaMakefile Mon May 24 11:29:49 2010 -0700 @@ -115,6 +115,7 @@ ex/Hoare.thy \ ex/Letrec.thy \ ex/Loop.thy \ + ex/Pattern_Match.thy \ ex/Powerdomain_ex.thy \ ex/Stream.thy \ ex/Strict_Fun.thy \ diff -r 00f13d3ad474 -r e67760c1b851 src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Mon May 24 09:32:52 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Mon May 24 11:29:49 2010 -0700 @@ -25,8 +25,7 @@ cases : thm list, sel_rews : thm list, dis_rews : thm list, - match_rews : thm list, - pat_rews : thm list + match_rews : thm list } * theory; end; @@ -824,162 +823,6 @@ end; (******************************************************************************) -(************** definitions and theorems for pattern combinators **************) -(******************************************************************************) - -fun add_pattern_combinators - (bindings : binding list) - (spec : (term * (bool * typ) list) list) - (lhsT : typ) - (exhaust : thm) - (case_const : typ -> term) - (case_rews : thm list) - (thy : theory) = - let - - (* utility functions *) - fun mk_pair_pat (p1, p2) = - let - val T1 = fastype_of p1; - val T2 = fastype_of p2; - val (U1, V1) = apsnd dest_matchT (dest_cfunT T1); - val (U2, V2) = apsnd dest_matchT (dest_cfunT T2); - val pat_typ = [T1, T2] ---> - (mk_prodT (U1, U2) ->> mk_matchT (mk_prodT (V1, V2))); - val pat_const = Const (@{const_name cpair_pat}, pat_typ); - in - pat_const $ p1 $ p2 - end; - fun mk_tuple_pat [] = succeed_const HOLogic.unitT - | mk_tuple_pat ps = foldr1 mk_pair_pat ps; - fun branch_const (T,U,V) = - Const (@{const_name branch}, - (T ->> mk_matchT U) --> (U ->> V) ->> T ->> mk_matchT V); - - (* define pattern combinators *) - local - val tns = map (fst o dest_TFree) (snd (dest_Type lhsT)); - - fun pat_eqn (i, (bind, (con, args))) : binding * term * mixfix = - let - val pat_bind = Binding.suffix_name "_pat" bind; - val Ts = map snd args; - val Vs = - (map (K "'t") args) - |> Datatype_Prop.indexify_names - |> Name.variant_list tns - |> map (fn t => TFree (t, @{sort pcpo})); - val patNs = Datatype_Prop.indexify_names (map (K "pat") args); - val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs; - val pats = map Free (patNs ~~ patTs); - val fail = mk_fail (mk_tupleT Vs); - val (vs, nonlazy) = get_vars_avoiding patNs args; - val rhs = big_lambdas vs (mk_tuple_pat pats ` mk_tuple vs); - fun one_fun (j, (_, args')) = - let - val (vs', nonlazy) = get_vars_avoiding patNs args'; - in if i = j then rhs else big_lambdas vs' fail end; - val funs = map_index one_fun spec; - val body = list_ccomb (case_const (mk_matchT (mk_tupleT Vs)), funs); - in - (pat_bind, lambdas pats body, NoSyn) - end; - in - val ((pat_consts, pat_defs), thy) = - define_consts (map_index pat_eqn (bindings ~~ spec)) thy - end; - - (* syntax translations for pattern combinators *) - local - open Syntax - fun syntax c = Syntax.mark_const (fst (dest_Const c)); - fun app s (l, r) = Syntax.mk_appl (Constant s) [l, r]; - val capp = app @{const_syntax Rep_CFun}; - val capps = Library.foldl capp - - fun app_var x = Syntax.mk_appl (Constant "_variable") [x, Variable "rhs"]; - fun app_pat x = Syntax.mk_appl (Constant "_pat") [x]; - fun args_list [] = Constant "_noargs" - | args_list xs = foldr1 (app "_args") xs; - fun one_case_trans (pat, (con, args)) = - let - val cname = Constant (syntax con); - val pname = Constant (syntax pat); - val ns = 1 upto length args; - val xs = map (fn n => Variable ("x"^(string_of_int n))) ns; - val ps = map (fn n => Variable ("p"^(string_of_int n))) ns; - val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; - in - [ParseRule (app_pat (capps (cname, xs)), - mk_appl pname (map app_pat xs)), - ParseRule (app_var (capps (cname, xs)), - app_var (args_list xs)), - PrintRule (capps (cname, ListPair.map (app "_match") (ps,vs)), - app "_match" (mk_appl pname ps, args_list vs))] - end; - val trans_rules : Syntax.ast Syntax.trrule list = - maps one_case_trans (pat_consts ~~ spec); - in - val thy = Sign.add_trrules_i trans_rules thy; - end; - - (* prove strictness and reduction rules of pattern combinators *) - local - val tns = map (fst o dest_TFree) (snd (dest_Type lhsT)); - val rn = Name.variant tns "'r"; - val R = TFree (rn, @{sort pcpo}); - fun pat_lhs (pat, args) = - let - val Ts = map snd args; - val Vs = - (map (K "'t") args) - |> Datatype_Prop.indexify_names - |> Name.variant_list (rn::tns) - |> map (fn t => TFree (t, @{sort pcpo})); - val patNs = Datatype_Prop.indexify_names (map (K "pat") args); - val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs; - val pats = map Free (patNs ~~ patTs); - val k = Free ("rhs", mk_tupleT Vs ->> R); - val branch1 = branch_const (lhsT, mk_tupleT Vs, R); - val fun1 = (branch1 $ list_comb (pat, pats)) ` k; - val branch2 = branch_const (mk_tupleT Ts, mk_tupleT Vs, R); - val fun2 = (branch2 $ mk_tuple_pat pats) ` k; - val taken = "rhs" :: patNs; - in (fun1, fun2, taken) end; - fun pat_strict (pat, (con, args)) = - let - val (fun1, fun2, taken) = pat_lhs (pat, args); - val defs = @{thm branch_def} :: pat_defs; - val goal = mk_trp (mk_strict fun1); - val rules = @{thms match_case_simps} @ case_rews; - val tacs = [simp_tac (beta_ss addsimps rules) 1]; - in prove thy defs goal (K tacs) end; - fun pat_apps (i, (pat, (con, args))) = - let - val (fun1, fun2, taken) = pat_lhs (pat, args); - fun pat_app (j, (con', args')) = - let - val (vs, nonlazy) = get_vars_avoiding taken args'; - val con_app = list_ccomb (con', vs); - val assms = map (mk_trp o mk_defined) nonlazy; - val rhs = if i = j then fun2 ` mk_tuple vs else mk_fail R; - val concl = mk_trp (mk_eq (fun1 ` con_app, rhs)); - val goal = Logic.list_implies (assms, concl); - val defs = @{thm branch_def} :: pat_defs; - val rules = @{thms match_case_simps} @ case_rews; - val tacs = [asm_simp_tac (beta_ss addsimps rules) 1]; - in prove thy defs goal (K tacs) end; - in map_index pat_app spec end; - in - val pat_stricts = map pat_strict (pat_consts ~~ spec); - val pat_apps = flat (map_index pat_apps (pat_consts ~~ spec)); - end; - - in - (pat_stricts @ pat_apps, thy) - end - -(******************************************************************************) (******************************* main function ********************************) (******************************************************************************) @@ -1061,18 +904,6 @@ exhaust case_const cases thy end - (* define and prove theorems for pattern combinators *) - val (pat_thms : thm list, thy : theory) = - let - val bindings = map #1 spec; - fun prep_arg (lazy, sel, T) = (lazy, T); - fun prep_con c (b, args, mx) = (c, map prep_arg args); - val pat_spec = map2 prep_con con_consts spec; - in - add_pattern_combinators bindings pat_spec lhsT - exhaust case_const cases thy - end - (* restore original signature path *) val thy = Sign.parent_path thy; @@ -1090,8 +921,7 @@ cases = cases, sel_rews = sel_thms, dis_rews = dis_thms, - match_rews = match_thms, - pat_rews = pat_thms }; + match_rews = match_thms }; in (result, thy) end; diff -r 00f13d3ad474 -r e67760c1b851 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Mon May 24 09:32:52 2010 -0700 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Mon May 24 11:29:49 2010 -0700 @@ -145,7 +145,6 @@ val when_strict = hd when_rews; val dis_rews = #dis_rews result; val mat_rews = #match_rews result; -val pat_rews = #pat_rews result; (* ----- theorems concerning the isomorphism -------------------------------- *) @@ -211,7 +210,6 @@ ((qualified "con_rews" , con_rews ), [simp]), ((qualified "sel_rews" , sel_rews ), [simp]), ((qualified "dis_rews" , dis_rews ), [simp]), - ((qualified "pat_rews" , pat_rews ), [simp]), ((qualified "dist_les" , dist_les ), [simp]), ((qualified "dist_eqs" , dist_eqs ), [simp]), ((qualified "inverts" , inverts ), [simp]), @@ -220,7 +218,7 @@ ((qualified "match_rews", mat_rews ), [simp])] |> snd |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ - pat_rews @ dist_les @ dist_eqs) + dist_les @ dist_eqs) end; (* let *) (******************************************************************************) diff -r 00f13d3ad474 -r e67760c1b851 src/HOLCF/Tutorial/Domain_ex.thy --- a/src/HOLCF/Tutorial/Domain_ex.thy Mon May 24 09:32:52 2010 -0700 +++ b/src/HOLCF/Tutorial/Domain_ex.thy Mon May 24 11:29:49 2010 -0700 @@ -154,11 +154,6 @@ term is_Node thm tree.dis_rews -text {* Rules about pattern match combinators *} -term Leaf_pat -term Node_pat -thm tree.pat_rews - text {* Rules about monadic pattern match combinators *} term match_Leaf term match_Node diff -r 00f13d3ad474 -r e67760c1b851 src/HOLCF/ex/Pattern_Match.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/ex/Pattern_Match.thy Mon May 24 11:29:49 2010 -0700 @@ -0,0 +1,591 @@ +(* Title: HOLCF/ex/Pattern_Match.thy + Author: Brian Huffman +*) + +header {* An experimental pattern-matching notation *} + +theory Pattern_Match +imports HOLCF +begin + +text {* FIXME: Find a proper way to un-hide constants. *} + +abbreviation fail :: "'a match" +where "fail \ Fixrec.fail" + +abbreviation succeed :: "'a \ 'a match" +where "succeed \ Fixrec.succeed" + +abbreviation run :: "'a match \ 'a" +where "run \ Fixrec.run" + +subsection {* Fatbar combinator *} + +definition + fatbar :: "('a \ 'b match) \ ('a \ 'b match) \ ('a \ 'b match)" where + "fatbar = (\ a b x. a\x +++ b\x)" + +abbreviation + fatbar_syn :: "['a \ 'b match, 'a \ 'b match] \ 'a \ 'b match" (infixr "\" 60) where + "m1 \ m2 == fatbar\m1\m2" + +lemma fatbar1: "m\x = \ \ (m \ ms)\x = \" +by (simp add: fatbar_def) + +lemma fatbar2: "m\x = fail \ (m \ ms)\x = ms\x" +by (simp add: fatbar_def) + +lemma fatbar3: "m\x = succeed\y \ (m \ ms)\x = succeed\y" +by (simp add: fatbar_def) + +lemmas fatbar_simps = fatbar1 fatbar2 fatbar3 + +lemma run_fatbar1: "m\x = \ \ run\((m \ ms)\x) = \" +by (simp add: fatbar_def) + +lemma run_fatbar2: "m\x = fail \ run\((m \ ms)\x) = run\(ms\x)" +by (simp add: fatbar_def) + +lemma run_fatbar3: "m\x = succeed\y \ run\((m \ ms)\x) = y" +by (simp add: fatbar_def) + +lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3 + +subsection {* Case branch combinator *} + +definition + branch :: "('a \ 'b match) \ ('b \ 'c) \ ('a \ 'c match)" where + "branch p \ \ r x. match_case\fail\(\ y. succeed\(r\y))\(p\x)" + +lemma branch_simps: + "p\x = \ \ branch p\r\x = \" + "p\x = fail \ branch p\r\x = fail" + "p\x = succeed\y \ branch p\r\x = succeed\(r\y)" +by (simp_all add: branch_def) + +lemma branch_succeed [simp]: "branch succeed\r\x = succeed\(r\x)" +by (simp add: branch_def) + +subsection {* Cases operator *} + +definition + cases :: "'a match \ 'a::pcpo" where + "cases = match_case\\\ID" + +text {* rewrite rules for cases *} + +lemma cases_strict [simp]: "cases\\ = \" +by (simp add: cases_def) + +lemma cases_fail [simp]: "cases\fail = \" +by (simp add: cases_def) + +lemma cases_succeed [simp]: "cases\(succeed\x) = x" +by (simp add: cases_def) + +subsection {* Case syntax *} + +nonterminals + Case_syn Cases_syn + +syntax + "_Case_syntax":: "['a, Cases_syn] => 'b" ("(Case _ of/ _)" 10) + "_Case1" :: "['a, 'b] => Case_syn" ("(2_ =>/ _)" 10) + "" :: "Case_syn => Cases_syn" ("_") + "_Case2" :: "[Case_syn, Cases_syn] => Cases_syn" ("_/ | _") + +syntax (xsymbols) + "_Case1" :: "['a, 'b] => Case_syn" ("(2_ \/ _)" 10) + +translations + "_Case_syntax x ms" == "CONST cases\(ms\x)" + "_Case2 m ms" == "m \ ms" + +text {* Parsing Case expressions *} + +syntax + "_pat" :: "'a" + "_variable" :: "'a" + "_noargs" :: "'a" + +translations + "_Case1 p r" => "CONST branch (_pat p)\(_variable p r)" + "_variable (_args x y) r" => "CONST csplit\(_variable x (_variable y r))" + "_variable _noargs r" => "CONST unit_when\r" + +parse_translation {* +(* rewrite (_pat x) => (succeed) *) +(* rewrite (_variable x t) => (Abs_CFun (%x. t)) *) + [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.succeed}), + mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_CFun})]; +*} + +text {* Printing Case expressions *} + +syntax + "_match" :: "'a" + +print_translation {* + let + fun dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax unit_when},_) $ t) = + (Syntax.const @{syntax_const "_noargs"}, t) + | dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax csplit},_) $ t) = + let + val (v1, t1) = dest_LAM t; + val (v2, t2) = dest_LAM t1; + in (Syntax.const @{syntax_const "_args"} $ v1 $ v2, t2) end + | dest_LAM (Const (@{const_syntax Abs_CFun},_) $ t) = + let + val abs = + case t of Abs abs => abs + | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0); + val (x, t') = atomic_abs_tr' abs; + in (Syntax.const @{syntax_const "_variable"} $ x, t') end + | dest_LAM _ = raise Match; (* too few vars: abort translation *) + + fun Case1_tr' [Const(@{const_syntax branch},_) $ p, r] = + let val (v, t) = dest_LAM r in + Syntax.const @{syntax_const "_Case1"} $ + (Syntax.const @{syntax_const "_match"} $ p $ v) $ t + end; + + in [(@{const_syntax Rep_CFun}, Case1_tr')] end; +*} + +translations + "x" <= "_match (CONST succeed) (_variable x)" + + +subsection {* Pattern combinators for data constructors *} + +types ('a, 'b) pat = "'a \ 'b match" + +definition + cpair_pat :: "('a, 'c) pat \ ('b, 'd) pat \ ('a \ 'b, 'c \ 'd) pat" where + "cpair_pat p1 p2 = (\(x, y). + match_case\fail\(\ a. match_case\fail\(\ b. succeed\(a, b))\(p2\y))\(p1\x))" + +definition + spair_pat :: + "('a, 'c) pat \ ('b, 'd) pat \ ('a::pcpo \ 'b::pcpo, 'c \ 'd) pat" where + "spair_pat p1 p2 = (\(:x, y:). cpair_pat p1 p2\(x, y))" + +definition + sinl_pat :: "('a, 'c) pat \ ('a::pcpo \ 'b::pcpo, 'c) pat" where + "sinl_pat p = sscase\p\(\ x. fail)" + +definition + sinr_pat :: "('b, 'c) pat \ ('a::pcpo \ 'b::pcpo, 'c) pat" where + "sinr_pat p = sscase\(\ x. fail)\p" + +definition + up_pat :: "('a, 'b) pat \ ('a u, 'b) pat" where + "up_pat p = fup\p" + +definition + TT_pat :: "(tr, unit) pat" where + "TT_pat = (\ b. If b then succeed\() else fail fi)" + +definition + FF_pat :: "(tr, unit) pat" where + "FF_pat = (\ b. If b then fail else succeed\() fi)" + +definition + ONE_pat :: "(one, unit) pat" where + "ONE_pat = (\ ONE. succeed\())" + +text {* Parse translations (patterns) *} +translations + "_pat (XCONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)" + "_pat (XCONST spair\x\y)" => "CONST spair_pat (_pat x) (_pat y)" + "_pat (XCONST sinl\x)" => "CONST sinl_pat (_pat x)" + "_pat (XCONST sinr\x)" => "CONST sinr_pat (_pat x)" + "_pat (XCONST up\x)" => "CONST up_pat (_pat x)" + "_pat (XCONST TT)" => "CONST TT_pat" + "_pat (XCONST FF)" => "CONST FF_pat" + "_pat (XCONST ONE)" => "CONST ONE_pat" + +text {* CONST version is also needed for constructors with special syntax *} +translations + "_pat (CONST Pair x y)" => "CONST cpair_pat (_pat x) (_pat y)" + "_pat (CONST spair\x\y)" => "CONST spair_pat (_pat x) (_pat y)" + +text {* Parse translations (variables) *} +translations + "_variable (XCONST Pair x y) r" => "_variable (_args x y) r" + "_variable (XCONST spair\x\y) r" => "_variable (_args x y) r" + "_variable (XCONST sinl\x) r" => "_variable x r" + "_variable (XCONST sinr\x) r" => "_variable x r" + "_variable (XCONST up\x) r" => "_variable x r" + "_variable (XCONST TT) r" => "_variable _noargs r" + "_variable (XCONST FF) r" => "_variable _noargs r" + "_variable (XCONST ONE) r" => "_variable _noargs r" + +translations + "_variable (CONST Pair x y) r" => "_variable (_args x y) r" + "_variable (CONST spair\x\y) r" => "_variable (_args x y) r" + +text {* Print translations *} +translations + "CONST Pair (_match p1 v1) (_match p2 v2)" + <= "_match (CONST cpair_pat p1 p2) (_args v1 v2)" + "CONST spair\(_match p1 v1)\(_match p2 v2)" + <= "_match (CONST spair_pat p1 p2) (_args v1 v2)" + "CONST sinl\(_match p1 v1)" <= "_match (CONST sinl_pat p1) v1" + "CONST sinr\(_match p1 v1)" <= "_match (CONST sinr_pat p1) v1" + "CONST up\(_match p1 v1)" <= "_match (CONST up_pat p1) v1" + "CONST TT" <= "_match (CONST TT_pat) _noargs" + "CONST FF" <= "_match (CONST FF_pat) _noargs" + "CONST ONE" <= "_match (CONST ONE_pat) _noargs" + +lemma cpair_pat1: + "branch p\r\x = \ \ branch (cpair_pat p q)\(csplit\r)\(x, y) = \" +apply (simp add: branch_def cpair_pat_def) +apply (cases "p\x", simp_all) +done + +lemma cpair_pat2: + "branch p\r\x = fail \ branch (cpair_pat p q)\(csplit\r)\(x, y) = fail" +apply (simp add: branch_def cpair_pat_def) +apply (cases "p\x", simp_all) +done + +lemma cpair_pat3: + "branch p\r\x = succeed\s \ + branch (cpair_pat p q)\(csplit\r)\(x, y) = branch q\s\y" +apply (simp add: branch_def cpair_pat_def) +apply (cases "p\x", simp_all) +apply (cases "q\y", simp_all) +done + +lemmas cpair_pat [simp] = + cpair_pat1 cpair_pat2 cpair_pat3 + +lemma spair_pat [simp]: + "branch (spair_pat p1 p2)\r\\ = \" + "\x \ \; y \ \\ + \ branch (spair_pat p1 p2)\r\(:x, y:) = + branch (cpair_pat p1 p2)\r\(x, y)" +by (simp_all add: branch_def spair_pat_def) + +lemma sinl_pat [simp]: + "branch (sinl_pat p)\r\\ = \" + "x \ \ \ branch (sinl_pat p)\r\(sinl\x) = branch p\r\x" + "y \ \ \ branch (sinl_pat p)\r\(sinr\y) = fail" +by (simp_all add: branch_def sinl_pat_def) + +lemma sinr_pat [simp]: + "branch (sinr_pat p)\r\\ = \" + "x \ \ \ branch (sinr_pat p)\r\(sinl\x) = fail" + "y \ \ \ branch (sinr_pat p)\r\(sinr\y) = branch p\r\y" +by (simp_all add: branch_def sinr_pat_def) + +lemma up_pat [simp]: + "branch (up_pat p)\r\\ = \" + "branch (up_pat p)\r\(up\x) = branch p\r\x" +by (simp_all add: branch_def up_pat_def) + +lemma TT_pat [simp]: + "branch TT_pat\(unit_when\r)\\ = \" + "branch TT_pat\(unit_when\r)\TT = succeed\r" + "branch TT_pat\(unit_when\r)\FF = fail" +by (simp_all add: branch_def TT_pat_def) + +lemma FF_pat [simp]: + "branch FF_pat\(unit_when\r)\\ = \" + "branch FF_pat\(unit_when\r)\TT = fail" + "branch FF_pat\(unit_when\r)\FF = succeed\r" +by (simp_all add: branch_def FF_pat_def) + +lemma ONE_pat [simp]: + "branch ONE_pat\(unit_when\r)\\ = \" + "branch ONE_pat\(unit_when\r)\ONE = succeed\r" +by (simp_all add: branch_def ONE_pat_def) + + +subsection {* Wildcards, as-patterns, and lazy patterns *} + +definition + wild_pat :: "'a \ unit match" where + "wild_pat = (\ x. succeed\())" + +definition + as_pat :: "('a \ 'b match) \ 'a \ ('a \ 'b) match" where + "as_pat p = (\ x. match_case\fail\(\ a. succeed\(x, a))\(p\x))" + +definition + lazy_pat :: "('a \ 'b::pcpo match) \ ('a \ 'b match)" where + "lazy_pat p = (\ x. succeed\(cases\(p\x)))" + +text {* Parse translations (patterns) *} +translations + "_pat _" => "CONST wild_pat" + +text {* Parse translations (variables) *} +translations + "_variable _ r" => "_variable _noargs r" + +text {* Print translations *} +translations + "_" <= "_match (CONST wild_pat) _noargs" + +lemma wild_pat [simp]: "branch wild_pat\(unit_when\r)\x = succeed\r" +by (simp add: branch_def wild_pat_def) + +lemma as_pat [simp]: + "branch (as_pat p)\(csplit\r)\x = branch p\(r\x)\x" +apply (simp add: branch_def as_pat_def) +apply (cases "p\x", simp_all) +done + +lemma lazy_pat [simp]: + "branch p\r\x = \ \ branch (lazy_pat p)\r\x = succeed\(r\\)" + "branch p\r\x = fail \ branch (lazy_pat p)\r\x = succeed\(r\\)" + "branch p\r\x = succeed\s \ branch (lazy_pat p)\r\x = succeed\s" +apply (simp_all add: branch_def lazy_pat_def) +apply (cases "p\x", simp_all)+ +done + +subsection {* Examples *} + +term "Case t of (:up\(sinl\x), sinr\y:) \ (x, y)" + +term "\ t. Case t of up\(sinl\a) \ a | up\(sinr\b) \ b" + +term "\ t. Case t of (:up\(sinl\_), sinr\x:) \ x" + +subsection {* ML code for generating definitions *} + +ML {* +local open HOLCF_Library in + +val beta_rules = + @{thms beta_cfun cont_id cont_const cont2cont_Rep_CFun cont2cont_LAM'} @ + @{thms cont2cont_fst cont2cont_snd cont2cont_Pair}; + +val beta_ss = HOL_basic_ss addsimps (simp_thms @ beta_rules); + +fun define_consts + (specs : (binding * term * mixfix) list) + (thy : theory) + : (term list * thm list) * theory = + let + fun mk_decl (b, t, mx) = (b, fastype_of t, mx); + val decls = map mk_decl specs; + val thy = Cont_Consts.add_consts decls thy; + fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T); + val consts = map mk_const decls; + fun mk_def c (b, t, mx) = + (Binding.suffix_name "_def" b, Logic.mk_equals (c, t)); + val defs = map2 mk_def consts specs; + val (def_thms, thy) = + PureThy.add_defs false (map Thm.no_attributes defs) thy; + in + ((consts, def_thms), thy) + end; + +fun prove + (thy : theory) + (defs : thm list) + (goal : term) + (tacs : {prems: thm list, context: Proof.context} -> tactic list) + : thm = + let + fun tac {prems, context} = + rewrite_goals_tac defs THEN + EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context}) + in + Goal.prove_global thy [] [] goal tac + end; + +fun get_vars_avoiding + (taken : string list) + (args : (bool * typ) list) + : (term list * term list) = + let + val Ts = map snd args; + val ns = Name.variant_list taken (Datatype_Prop.make_tnames Ts); + val vs = map Free (ns ~~ Ts); + val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs)); + in + (vs, nonlazy) + end; + +(******************************************************************************) +(************** definitions and theorems for pattern combinators **************) +(******************************************************************************) + +fun add_pattern_combinators + (bindings : binding list) + (spec : (term * (bool * typ) list) list) + (lhsT : typ) + (exhaust : thm) + (case_const : typ -> term) + (case_rews : thm list) + (thy : theory) = + let + + (* utility functions *) + fun mk_pair_pat (p1, p2) = + let + val T1 = fastype_of p1; + val T2 = fastype_of p2; + val (U1, V1) = apsnd dest_matchT (dest_cfunT T1); + val (U2, V2) = apsnd dest_matchT (dest_cfunT T2); + val pat_typ = [T1, T2] ---> + (mk_prodT (U1, U2) ->> mk_matchT (mk_prodT (V1, V2))); + val pat_const = Const (@{const_name cpair_pat}, pat_typ); + in + pat_const $ p1 $ p2 + end; + fun mk_tuple_pat [] = succeed_const HOLogic.unitT + | mk_tuple_pat ps = foldr1 mk_pair_pat ps; + fun branch_const (T,U,V) = + Const (@{const_name branch}, + (T ->> mk_matchT U) --> (U ->> V) ->> T ->> mk_matchT V); + + (* define pattern combinators *) + local + val tns = map (fst o dest_TFree) (snd (dest_Type lhsT)); + + fun pat_eqn (i, (bind, (con, args))) : binding * term * mixfix = + let + val pat_bind = Binding.suffix_name "_pat" bind; + val Ts = map snd args; + val Vs = + (map (K "'t") args) + |> Datatype_Prop.indexify_names + |> Name.variant_list tns + |> map (fn t => TFree (t, @{sort pcpo})); + val patNs = Datatype_Prop.indexify_names (map (K "pat") args); + val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs; + val pats = map Free (patNs ~~ patTs); + val fail = mk_fail (mk_tupleT Vs); + val (vs, nonlazy) = get_vars_avoiding patNs args; + val rhs = big_lambdas vs (mk_tuple_pat pats ` mk_tuple vs); + fun one_fun (j, (_, args')) = + let + val (vs', nonlazy) = get_vars_avoiding patNs args'; + in if i = j then rhs else big_lambdas vs' fail end; + val funs = map_index one_fun spec; + val body = list_ccomb (case_const (mk_matchT (mk_tupleT Vs)), funs); + in + (pat_bind, lambdas pats body, NoSyn) + end; + in + val ((pat_consts, pat_defs), thy) = + define_consts (map_index pat_eqn (bindings ~~ spec)) thy + end; + + (* syntax translations for pattern combinators *) + local + open Syntax + fun syntax c = Syntax.mark_const (fst (dest_Const c)); + fun app s (l, r) = Syntax.mk_appl (Constant s) [l, r]; + val capp = app @{const_syntax Rep_CFun}; + val capps = Library.foldl capp + + fun app_var x = Syntax.mk_appl (Constant "_variable") [x, Variable "rhs"]; + fun app_pat x = Syntax.mk_appl (Constant "_pat") [x]; + fun args_list [] = Constant "_noargs" + | args_list xs = foldr1 (app "_args") xs; + fun one_case_trans (pat, (con, args)) = + let + val cname = Constant (syntax con); + val pname = Constant (syntax pat); + val ns = 1 upto length args; + val xs = map (fn n => Variable ("x"^(string_of_int n))) ns; + val ps = map (fn n => Variable ("p"^(string_of_int n))) ns; + val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; + in + [ParseRule (app_pat (capps (cname, xs)), + mk_appl pname (map app_pat xs)), + ParseRule (app_var (capps (cname, xs)), + app_var (args_list xs)), + PrintRule (capps (cname, ListPair.map (app "_match") (ps,vs)), + app "_match" (mk_appl pname ps, args_list vs))] + end; + val trans_rules : Syntax.ast Syntax.trrule list = + maps one_case_trans (pat_consts ~~ spec); + in + val thy = Sign.add_trrules_i trans_rules thy; + end; + + (* prove strictness and reduction rules of pattern combinators *) + local + val tns = map (fst o dest_TFree) (snd (dest_Type lhsT)); + val rn = Name.variant tns "'r"; + val R = TFree (rn, @{sort pcpo}); + fun pat_lhs (pat, args) = + let + val Ts = map snd args; + val Vs = + (map (K "'t") args) + |> Datatype_Prop.indexify_names + |> Name.variant_list (rn::tns) + |> map (fn t => TFree (t, @{sort pcpo})); + val patNs = Datatype_Prop.indexify_names (map (K "pat") args); + val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs; + val pats = map Free (patNs ~~ patTs); + val k = Free ("rhs", mk_tupleT Vs ->> R); + val branch1 = branch_const (lhsT, mk_tupleT Vs, R); + val fun1 = (branch1 $ list_comb (pat, pats)) ` k; + val branch2 = branch_const (mk_tupleT Ts, mk_tupleT Vs, R); + val fun2 = (branch2 $ mk_tuple_pat pats) ` k; + val taken = "rhs" :: patNs; + in (fun1, fun2, taken) end; + fun pat_strict (pat, (con, args)) = + let + val (fun1, fun2, taken) = pat_lhs (pat, args); + val defs = @{thm branch_def} :: pat_defs; + val goal = mk_trp (mk_strict fun1); + val rules = @{thms match_case_simps} @ case_rews; + val tacs = [simp_tac (beta_ss addsimps rules) 1]; + in prove thy defs goal (K tacs) end; + fun pat_apps (i, (pat, (con, args))) = + let + val (fun1, fun2, taken) = pat_lhs (pat, args); + fun pat_app (j, (con', args')) = + let + val (vs, nonlazy) = get_vars_avoiding taken args'; + val con_app = list_ccomb (con', vs); + val assms = map (mk_trp o mk_defined) nonlazy; + val rhs = if i = j then fun2 ` mk_tuple vs else mk_fail R; + val concl = mk_trp (mk_eq (fun1 ` con_app, rhs)); + val goal = Logic.list_implies (assms, concl); + val defs = @{thm branch_def} :: pat_defs; + val rules = @{thms match_case_simps} @ case_rews; + val tacs = [asm_simp_tac (beta_ss addsimps rules) 1]; + in prove thy defs goal (K tacs) end; + in map_index pat_app spec end; + in + val pat_stricts = map pat_strict (pat_consts ~~ spec); + val pat_apps = flat (map_index pat_apps (pat_consts ~~ spec)); + end; + + in + (pat_stricts @ pat_apps, thy) + end + +end +*} + +(* +Cut from HOLCF/Tools/domain_constructors.ML +in function add_domain_constructors: + + ( * define and prove theorems for pattern combinators * ) + val (pat_thms : thm list, thy : theory) = + let + val bindings = map #1 spec; + fun prep_arg (lazy, sel, T) = (lazy, T); + fun prep_con c (b, args, mx) = (c, map prep_arg args); + val pat_spec = map2 prep_con con_consts spec; + in + add_pattern_combinators bindings pat_spec lhsT + exhaust case_const cases thy + end + +*) + +end diff -r 00f13d3ad474 -r e67760c1b851 src/HOLCF/ex/ROOT.ML --- a/src/HOLCF/ex/ROOT.ML Mon May 24 09:32:52 2010 -0700 +++ b/src/HOLCF/ex/ROOT.ML Mon May 24 11:29:49 2010 -0700 @@ -6,4 +6,5 @@ use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare", "Loop", "Powerdomain_ex", "Domain_Proofs", "Letrec", + "Pattern_Match", "Strict_Fun"];