print_translation‹ let fun dest_LAM _ (Const (🍋‹Rep_cfun›,_) $ Const (🍋‹unit_when›,_) $ t) =
(Syntax.const 🍋‹_noargs›, t)
| dest_LAM ctxt (Const (🍋‹Rep_cfun›,_) $ Const (🍋‹csplit›,_) $ t) = let
val (v1, t1) = dest_LAM ctxt t;
val (v2, t2) = dest_LAM ctxt t1; in (Syntax.const 🍋‹_args› $ v1 $ v2, t2) end
| dest_LAM ctxt (Const (🍋‹Abs_cfun›,_) $ t) = let
val abs = case t of Abs abs => abs
| _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
val (x, t') = Syntax_Trans.atomic_abs_tr' ctxt abs; in (Syntax.const 🍋‹_variable› $ x, t') end
| dest_LAM _ _ = raise Match; (* too few vars: abort translation *)
fun Case1_tr' ctxt [Const(\<^const_syntax>\branch\,_) $ p, r] = let val (v, t) = dest_LAM ctxt r in Syntax.const 🍋‹_Case1› $
(Syntax.const 🍋‹_match› $ p $ v) $ t end;
in [(🍋‹Rep_cfun›, Case1_tr')] end ›
translations "x" <= "_match (CONST succeed) (_variable x)"
subsection‹Pattern combinators for data constructors›
type_synonym ('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_bind⋅(p1⋅x)⋅(Λ a. match_bind⋅(p2⋅y)⋅(Λ b. succeed⋅(a, b))))"
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 (Case_Translation.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 **************) (******************************************************************************)
(* 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 (🍋‹cpair_pat›, pat_typ); in
pat_const $ p1 $ p2 end; fun mk_tuple_pat [] = succeed_const 🍋‹unit›
| mk_tuple_pat ps = foldr1 mk_pair_pat ps;
(* define pattern combinators *) local
val tns = map (fst o dest_TFree) (dest_Type_args 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)
|> Case_Translation.indexify_names
|> Name.variant_list tns
|> map (fn t => TFree (t, 🍋‹pcpo›));
val patNs = Case_Translation.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'; inif 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 funsyntax c = Lexicon.mark_const (dest_Const_name c); fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r];
val capp = app 🍋‹Rep_cfun›;
val capps = Library.foldl capp
fun app_var x = Ast.mk_appl (Ast.Constant "_variable") [x, Ast.Variable "rhs"]; fun app_pat x = Ast.mk_appl (Ast.Constant "_pat") [x]; fun args_list [] = Ast.Constant "_noargs"
| args_list xs = foldr1 (app "_args") xs; fun one_case_trans (pat, (con, args)) = let
val cname = Ast.Constant (syntax con);
val pname = Ast.Constant (syntax pat);
val ns = 1 upto length args;
val xs = map (fn n => Ast.Variable ("x"^(string_of_int n))) ns;
val ps = map (fn n => Ast.Variable ("p"^(string_of_int n))) ns;
val vs = map (fn n => Ast.Variable ("v"^(string_of_int n))) ns; in
[Syntax.Parse_Rule (app_pat (capps (cname, xs)),
Ast.mk_appl pname (map app_pat xs)), Syntax.Parse_Rule (app_var (capps (cname, xs)),
app_var (args_list xs)), Syntax.Print_Rule (capps (cname, ListPair.map (app "_match") (ps,vs)),
app "_match" (Ast.mk_appl pname ps, args_list vs))] end;
val trans_rules : Ast.ast Syntax.trrule list =
maps one_case_trans (pat_consts ~~ spec); in
val thy = Sign.translations_global true trans_rules thy; end;
(* prove strictness and reduction rules of pattern combinators *) local
val tns = map (fst o dest_TFree) (dest_Type_args lhsT);
val rn = singleton (Name.variant_list tns) "'r";
val R = TFree (rn, 🍋‹pcpo›); fun pat_lhs (pat, args) = let
val Ts = map snd args;
val Vs =
(map (K "'t") args)
|> Case_Translation.indexify_names
|> Name.variant_list (rn::tns)
|> map (fn t => TFree (t, 🍋‹pcpo›));
val patNs = Case_Translation.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 lhsT ‹mk_tupleT Vs› R›;
val fun1 = (branch1 $ list_comb (pat, pats)) ` k;
val branch2 = 🍋‹branch ‹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_bind_simps} @ case_rews; fun tacs ctxt = [simp_tac (put_simpset beta_ss ctxt addsimps rules) 1]; in prove thy defs goal (tacs o #context) 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_bind_simps} @ case_rews; fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps rules) 1]; in prove thy defs goal (tacs o #context) 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
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
