# HG changeset patch # User huffman # Date 1235672933 28800 # Node ID 6be1be402ef0c0196062efb83195ab7073069774 # Parent e23770bc97c87cdf6eab5e03e72833512d96d92c use TheoryData to keep track of pattern match combinators diff -r e23770bc97c8 -r 6be1be402ef0 src/HOLCF/Fixrec.thy --- a/src/HOLCF/Fixrec.thy Thu Feb 26 08:48:33 2009 -0800 +++ b/src/HOLCF/Fixrec.thy Thu Feb 26 10:28:53 2009 -0800 @@ -583,6 +583,20 @@ use "Tools/fixrec_package.ML" +setup {* FixrecPackage.setup *} + +setup {* + FixrecPackage.add_matchers + [ (@{const_name up}, @{const_name match_up}), + (@{const_name sinl}, @{const_name match_sinl}), + (@{const_name sinr}, @{const_name match_sinr}), + (@{const_name spair}, @{const_name match_spair}), + (@{const_name cpair}, @{const_name match_cpair}), + (@{const_name ONE}, @{const_name match_ONE}), + (@{const_name TT}, @{const_name match_TT}), + (@{const_name FF}, @{const_name match_FF}) ] +*} + hide (open) const return bind fail run cases end diff -r e23770bc97c8 -r 6be1be402ef0 src/HOLCF/Tools/domain/domain_axioms.ML --- a/src/HOLCF/Tools/domain/domain_axioms.ML Thu Feb 26 08:48:33 2009 -0800 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML Thu Feb 26 10:28:53 2009 -0800 @@ -39,7 +39,7 @@ fun one_con (con,args) = foldr /\# (list_ccomb (%%:con, mapn (idxs (length args)) 1 args)) args; in ("copy_def", %%:(dname^"_copy") == - /\"f" (list_ccomb (%%:(dname^"_when"), map one_con cons))) end; + /\ "f" (list_ccomb (%%:(dname^"_when"), map one_con cons))) end; (* -- definitions concerning the constructors, discriminators and selectors - *) @@ -107,7 +107,7 @@ [when_def, copy_def] @ con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @ [take_def, finite_def]) -end; (* let *) +end; (* let (calc_axioms) *) fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy)); @@ -117,6 +117,14 @@ fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x); fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; +fun add_matchers (((dname,_),cons) : eq) thy = + let + val con_names = map fst cons; + val mat_names = map mat_name con_names; + fun qualify n = Sign.full_name thy (Binding.name n); + val ms = map qualify con_names ~~ map qualify mat_names; + in FixrecPackage.add_matchers ms thy end; + in (* local *) fun add_axioms (comp_dnam, eqs : eq list) thy' = let @@ -125,7 +133,7 @@ val x_name = idx_name dnames "x"; fun copy_app dname = %%:(dname^"_copy")`Bound 0; val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == - /\"f"(mk_ctuple (map copy_app dnames))); + /\ "f"(mk_ctuple (map copy_app dnames))); val bisim_def = ("bisim_def",%%:(comp_dname^"_bisim")==mk_lam("R", let fun one_con (con,args) = let @@ -164,7 +172,8 @@ in thy |> Sign.add_path comp_dnam |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) |> Sign.parent_path -end; + |> fold add_matchers eqs +end; (* let (add_axioms) *) end; (* local *) end; (* struct *) diff -r e23770bc97c8 -r 6be1be402ef0 src/HOLCF/Tools/fixrec_package.ML --- a/src/HOLCF/Tools/fixrec_package.ML Thu Feb 26 08:48:33 2009 -0800 +++ b/src/HOLCF/Tools/fixrec_package.ML Thu Feb 26 10:28:53 2009 -0800 @@ -12,6 +12,8 @@ val add_fixrec_i: bool -> ((binding * attribute list) * term) list list -> theory -> theory val add_fixpat: Attrib.binding * string list -> theory -> theory val add_fixpat_i: (binding * attribute list) * term list -> theory -> theory + val add_matchers: (string * string) list -> theory -> theory + val setup: theory -> theory end; structure FixrecPackage: FIXREC_PACKAGE = @@ -123,6 +125,17 @@ (*********** monadic notation and pattern matching compilation ***********) (*************************************************************************) +structure FixrecMatchData = TheoryDataFun ( + type T = string Symtab.table; + val empty = Symtab.empty; + val copy = I; + val extend = I; + fun merge _ tabs : T = Symtab.merge (K true) tabs; +); + +(* associate match functions with pattern constants *) +fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms); + fun add_names (Const(a,_), bs) = insert (op =) (Sign.base_name a) bs | add_names (Free(a,_) , bs) = insert (op =) a bs | add_names (f $ u , bs) = add_names (f, add_names(u, bs)) @@ -132,20 +145,20 @@ fun add_terms ts xs = foldr add_names xs ts; (* builds a monadic term for matching a constructor pattern *) -fun pre_build pat rhs vs taken = +fun pre_build match_name pat rhs vs taken = case pat of Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) => - pre_build f rhs (v::vs) taken + pre_build match_name f rhs (v::vs) taken | Const(@{const_name Rep_CFun},_)$f$x => - let val (rhs', v, taken') = pre_build x rhs [] taken; - in pre_build f rhs' (v::vs) taken' end + let val (rhs', v, taken') = pre_build match_name x rhs [] taken; + in pre_build match_name f rhs' (v::vs) taken' end | Const(c,T) => let val n = Name.variant taken "v"; fun result_type (Type(@{type_name "->"},[_,T])) (x::xs) = result_type T xs | result_type T _ = T; val v = Free(n, result_type T vs); - val m = "match_"^(extern_name(Sign.base_name c)); + val m = match_name c; val k = lambda_ctuple vs rhs; in (%%:@{const_name Fixrec.bind}`(%%:m`v)`k, v, n::taken) @@ -155,19 +168,22 @@ (* builds a monadic term for matching a function definition pattern *) (* returns (name, arity, matcher) *) -fun building pat rhs vs taken = +fun building match_name pat rhs vs taken = case pat of Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) => - building f rhs (v::vs) taken + building match_name f rhs (v::vs) taken | Const(@{const_name Rep_CFun}, _)$f$x => - let val (rhs', v, taken') = pre_build x rhs [] taken; - in building f rhs' (v::vs) taken' end + let val (rhs', v, taken') = pre_build match_name x rhs [] taken; + in building match_name f rhs' (v::vs) taken' end | Const(name,_) => (name, length vs, big_lambdas vs rhs) | _ => fixrec_err "function is not declared as constant in theory"; -fun match_eq eq = +fun match_eq match_name eq = let val (lhs,rhs) = dest_eqs eq; - in building lhs (%%:@{const_name Fixrec.return}`rhs) [] (add_terms [eq] []) end; + in + building match_name lhs (%%:@{const_name Fixrec.return}`rhs) [] + (add_terms [eq] []) + end; (* returns the sum (using +++) of the terms in ms *) (* also applies "run" to the result! *) @@ -190,9 +206,9 @@ in (x::xs, y::ys, z::zs) end; (* this is the pattern-matching compiler function *) -fun compile_pats eqs = +fun compile_pats match_name eqs = let - val ((n::names),(a::arities),mats) = unzip3 (map match_eq eqs); + val ((n::names),(a::arities),mats) = unzip3 (map (match_eq match_name) eqs); val cname = if forall (fn x => n=x) names then n else fixrec_err "all equations in block must define the same function"; val arity = if forall (fn x => a=x) arities then a @@ -235,8 +251,14 @@ fun unconcat [] _ = [] | unconcat (n::ns) xs = List.take (xs,n) :: unconcat ns (List.drop (xs,n)); + val matcher_tab = FixrecMatchData.get thy; + fun match_name c = + case Symtab.lookup matcher_tab c of SOME m => m + | NONE => fixrec_err ("unknown pattern constructor: " ^ c); + val pattern_blocks = unconcat lengths (map Logic.strip_imp_concl eqn_ts'); - val compiled_ts = map (legacy_infer_term thy o compile_pats) pattern_blocks; + val compiled_ts = + map (legacy_infer_term thy o compile_pats match_name) pattern_blocks; val (thy', cnames, fixdef_thms, unfold_thms) = add_fixdefs compiled_ts thy; in if strict then let (* only prove simp rules if strict = true *) @@ -312,4 +334,6 @@ end; (* local structure *) +val setup = FixrecMatchData.init; + end;