# HG changeset patch # User huffman # Date 1267376101 28800 # Node ID 09bc6a2e22966d220959fdae633b4c57b81b4ac2 # Parent 561d8e98d9d353dda033a945ed8c21e2cca3c302 move definition and syntax of pattern combinators into domain_constructors.ML diff -r 561d8e98d9d3 -r 09bc6a2e2296 src/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOLCF/Tools/Domain/domain_axioms.ML Sat Feb 27 21:38:24 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Sun Feb 28 08:55:01 2010 -0800 @@ -78,22 +78,6 @@ (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep)) end; - val pat_defs = - let - fun pdef (con, _, args) = - let - val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; - val xs = map (bound_arg args) args; - val r = Bound (length args); - val rhs = case args of [] => mk_return HOLogic.unit - | _ => mk_ctuple_pat ps ` mk_ctuple xs; - fun one_con (con', _, args') = List.foldr /\# (if con'=con then rhs else mk_fail) args'; - in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == - list_ccomb(%%:(dname^"_when"), map one_con cons)) - end - in map pdef cons end; - - (* ----- axiom and definitions concerning induction ------------------------- *) val reach_ax = ("reach", mk_trp(proj (mk_fix (%%:(comp_dname^"_copy"))) eqs n @@ -112,7 +96,6 @@ in (dnam, (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]), (if definitional then [when_def] else [when_def, copy_def]) @ - pat_defs @ [take_def, finite_def]) end; (* let (calc_axioms) *) diff -r 561d8e98d9d3 -r 09bc6a2e2296 src/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOLCF/Tools/Domain/domain_constructors.ML Sat Feb 27 21:38:24 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_constructors.ML Sun Feb 28 08:55:01 2010 -0800 @@ -27,7 +27,8 @@ cases : thm list, sel_rews : thm list, dis_rews : thm list, - match_rews : thm list + match_rews : thm list, + pat_rews : thm list } * theory; end; @@ -94,6 +95,10 @@ let val T = fastype_of t in cabs_const (Term.domain_type T, Term.range_type T) $ t end +(* builds the expression (% v1 v2 .. vn. rhs) *) +fun lambdas [] rhs = rhs + | lambdas (v::vs) rhs = Term.lambda v (lambdas vs rhs); + (* builds the expression (LAM v. rhs) *) fun big_lambda v rhs = cabs_const (fastype_of v, fastype_of rhs) $ Term.lambda v rhs; @@ -131,9 +136,11 @@ (*** Product type ***) +val mk_prodT = HOLogic.mk_prodT + fun mk_tupleT [] = HOLogic.unitT | mk_tupleT [T] = T - | mk_tupleT (T :: Ts) = HOLogic.mk_prodT (T, mk_tupleT Ts); + | mk_tupleT (T :: Ts) = mk_prodT (T, mk_tupleT Ts); (* builds the expression (v1,v2,..,vn) *) fun mk_tuple [] = HOLogic.unit @@ -235,8 +242,14 @@ fun mk_matchT T = Type (@{type_name "maybe"}, [T]); +fun dest_matchT (Type(@{type_name "maybe"}, [T])) = T + | dest_matchT T = raise TYPE ("dest_matchT", [T], []); + fun mk_fail T = Const (@{const_name "Fixrec.fail"}, mk_matchT T); +fun return_const T = Const (@{const_name "Fixrec.return"}, T ->> mk_matchT T); +fun mk_return t = return_const (fastype_of t) ` t; + (*** miscellaneous constructions ***) @@ -997,6 +1010,109 @@ end; (******************************************************************************) +(************** definitions and theorems for pattern combinators **************) +(******************************************************************************) + +fun add_pattern_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 + + (* define pattern combinators *) + local + 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 [] = return_const HOLogic.unitT + | mk_tuple_pat ps = foldr1 mk_pair_pat ps; + + 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 ns = Name.variant_list patNs (Datatype_Prop.make_tnames Ts); + val vs = map Free (ns ~~ Ts); + val rhs = big_lambdas vs (mk_tuple_pat pats ` mk_tuple vs); + fun one_fun (j, (_, args')) = + let + val Ts = map snd args'; + val ns = Name.variant_list patNs (Datatype_Prop.make_tnames Ts); + val vs' = map Free (ns ~~ Ts); + 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 con ^ "_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; + + in + (pat_defs, thy) + end + +(******************************************************************************) (******************************* main function ********************************) (******************************************************************************) @@ -1077,6 +1193,18 @@ casedist 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 + casedist case_const cases thy + end + (* restore original signature path *) val thy = Sign.parent_path thy; @@ -1094,7 +1222,8 @@ cases = cases, sel_rews = sel_thms, dis_rews = dis_thms, - match_rews = match_thms }; + match_rews = match_thms, + pat_rews = pat_thms }; in (result, thy) end; diff -r 561d8e98d9d3 -r 09bc6a2e2296 src/HOLCF/Tools/Domain/domain_syntax.ML --- a/src/HOLCF/Tools/Domain/domain_syntax.ML Sat Feb 27 21:38:24 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Sun Feb 28 08:55:01 2010 -0800 @@ -55,36 +55,6 @@ val const_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn); end; -(* ----- constants concerning constructors, discriminators, and selectors --- *) - - local - val escape = let - fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs - else c::esc cs - | esc [] = [] - in implode o esc o Symbol.explode end; - - fun pat_name_ con = - Binding.name (strip_esc (Binding.name_of con) ^ "_pat"); - (* strictly speaking, these constants have one argument, - but the mixfix (without arguments) is introduced only - to generate parse rules for non-alphanumeric names*) - fun freetvar s n = - 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_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) = - (pat_name_ con, - (mapn pat_arg_typ 1 args) - ---> - 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_pat = map pat cons'; - end; - (* ----- constants concerning induction ------------------------------------- *) val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn); @@ -150,7 +120,6 @@ if definitional then [] else [const_rep, const_abs, const_copy]; in (optional_consts @ [const_when] @ - consts_pat @ [const_take, const_finite], (case_trans false :: case_trans true :: (abscon_trans false @ abscon_trans true @ Case_trans))) end; (* let *) diff -r 561d8e98d9d3 -r 09bc6a2e2296 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Feb 27 21:38:24 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sun Feb 28 08:55:01 2010 -0800 @@ -121,8 +121,6 @@ val ax_abs_iso = ga "abs_iso" dname; 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_pat_def = map (get_def pat_name) cons; val ax_copy_def = ga "copy_def" dname; end; (* local *) @@ -157,6 +155,7 @@ val when_strict = hd when_rews; val dis_rews = #dis_rews result; val mat_rews = #match_rews result; +val axs_pat_def = #pat_rews result; (* ----- theorems concerning the isomorphism -------------------------------- *)