# HG changeset patch # User huffman # Date 1267322951 28800 # Node ID f5461b02d754560bc337db607bd2e55b35d573b6 # Parent 34360a1e35372238a53fc7e50ce6820b25bfaa7d move definition of match combinators to domain_constructors.ML diff -r 34360a1e3537 -r f5461b02d754 src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Sat Feb 27 16:34:13 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Sat Feb 27 18:09:11 2010 -0800 @@ -78,19 +78,6 @@ (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep)) end; - val mat_defs = - let - fun mdef (con, _, _) = - let - val k = Bound 0 - val x = Bound 1 - fun one_con (con', _, args') = - if con'=con then k else List.foldr /\# mk_fail args' - val w = list_ccomb(%%:(dname^"_when"), map one_con cons) - val rhs = /\ "x" (/\ "k" (w ` x)) - in (mat_name con ^"_def", %%:(mat_name con) == rhs) end - in map mdef cons end; - val pat_defs = let fun pdef (con, _, args) = @@ -125,7 +112,7 @@ in (dnam, (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]), (if definitional then [when_def] else [when_def, copy_def]) @ - mat_defs @ pat_defs @ + pat_defs @ [take_def, finite_def]) end; (* let (calc_axioms) *) diff -r 34360a1e3537 -r f5461b02d754 src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Feb 27 16:34:13 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Feb 27 18:09:11 2010 -0800 @@ -26,7 +26,8 @@ dist_eqs : thm list, cases : thm list, sel_rews : thm list, - dis_rews : thm list + dis_rews : thm list, + match_rews : thm list } * theory; end; @@ -230,6 +231,13 @@ sscase_const (T, U, U) ` mk_bottom (T ->> U) ` mk_ID U; +(*** pattern match monad type ***) + +fun mk_matchT T = Type (@{type_name "maybe"}, [T]); + +fun mk_fail T = Const (@{const_name "Fixrec.fail"}, mk_matchT T); + + (*** miscellaneous constructions ***) val trT = @{typ "tr"}; @@ -892,6 +900,61 @@ end; (******************************************************************************) +(*************** definitions and theorems for match combinators ***************) +(******************************************************************************) + +fun add_match_combinators + (bindings : binding list) + (spec : (term * (bool * typ) list) list) + (lhsT : typ) + (casedist : thm) + (case_const : typ -> term) + (case_rews : thm list) + (thy : theory) = + let + + (* get a fresh type variable for the result type *) + val resultT : typ = + let + val ts : string list = map (fst o dest_TFree) (snd (dest_Type lhsT)); + val t : string = Name.variant ts "'t"; + in TFree (t, @{sort pcpo}) end; + + (* define match combinators *) + local + val x = Free ("x", lhsT); + fun k args = Free ("k", map snd args -->> mk_matchT resultT); + val fail = mk_fail resultT; + fun mat_fun i (j, (con, args)) = + let + val Ts = map snd args; + val ns = Name.variant_list ["x","k"] (Datatype_Prop.make_tnames Ts); + val vs = map Free (ns ~~ Ts); + in + if i = j then k args else big_lambdas vs fail + end; + fun mat_eqn (i, (bind, (con, args))) : binding * term * mixfix = + let + val mat_bind = Binding.prefix_name "match_" bind; + val funs = map_index (mat_fun i) spec + val body = list_ccomb (case_const (mk_matchT resultT), funs); + val rhs = big_lambda x (big_lambda (k args) (body ` x)); + in + (mat_bind, rhs, NoSyn) + end; + in + val ((match_consts, match_defs), thy) = + define_consts (map_index mat_eqn (bindings ~~ spec)) thy + end; + + in + (match_defs, thy) +(* + (match_stricts @ match_apps, thy) +*) + end; + +(******************************************************************************) (******************************* main function ********************************) (******************************************************************************) @@ -959,6 +1022,18 @@ casedist case_const cases thy end + (* define and prove theorems for match combinators *) + val (match_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 mat_spec = map2 prep_con con_consts spec; + in + add_match_combinators bindings mat_spec lhsT + casedist case_const cases thy + end + (* restore original signature path *) val thy = Sign.parent_path thy; @@ -975,7 +1050,8 @@ dist_eqs = #dist_eqs con_result, cases = cases, sel_rews = sel_thms, - dis_rews = dis_thms }; + dis_rews = dis_thms, + match_rews = match_thms }; in (result, thy) end; diff -r 34360a1e3537 -r f5461b02d754 src/HOLCF/Tools/Domain/domain_syntax.ML --- a/src/HOLCF/Tools/Domain/domain_syntax.ML Sat Feb 27 16:34:13 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Sat Feb 27 18:09:11 2010 -0800 @@ -64,8 +64,6 @@ | esc [] = [] in implode o esc o Symbol.explode end; - fun mat_name_ con = - Binding.name ("match_" ^ strip_esc (Binding.name_of con)); fun pat_name_ con = Binding.name (strip_esc (Binding.name_of con) ^ "_pat"); (* strictly speaking, these constants have one argument, @@ -75,12 +73,6 @@ let val tvar = mk_TFree (s ^ string_of_int n) in if tvar mem typevars then freetvar ("t"^s) n else tvar end; - fun mk_matT (a,bs,c) = - a ->> List.foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c; - fun mat (con,args,mx) = - (mat_name_ con, - mk_matT(dtype, map third args, freetvar "t" 1), - Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri)); fun mk_patT (a,b) = a ->> mk_maybeT b; fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n); fun pat (con,args,mx) = @@ -90,7 +82,6 @@ mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))), Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri)); in - val consts_mat = map mat cons'; val consts_pat = map pat cons'; end; @@ -159,7 +150,7 @@ if definitional then [] else [const_rep, const_abs, const_copy]; in (optional_consts @ [const_when] @ - consts_mat @ consts_pat @ + consts_pat @ [const_take, const_finite], (case_trans false :: case_trans true :: (abscon_trans false @ abscon_trans true @ Case_trans))) end; (* let *) diff -r 34360a1e3537 -r f5461b02d754 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Feb 27 16:34:13 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Feb 27 18:09:11 2010 -0800 @@ -156,7 +156,6 @@ val ax_rep_iso = ga "rep_iso" dname; val ax_when_def = ga "when_def" dname; fun get_def mk_name (con, _, _) = ga (mk_name con^"_def") dname; - val axs_mat_def = map (get_def mat_name) cons; val axs_pat_def = map (get_def pat_name) cons; val ax_copy_def = ga "copy_def" dname; end; (* local *) @@ -191,6 +190,7 @@ val when_rews = #cases result; val when_strict = hd when_rews; val dis_rews = #dis_rews result; +val axs_mat_def = #match_rews result; (* ----- theorems concerning the isomorphism -------------------------------- *)