# HG changeset patch # User panny # Date 1378339128 -7200 # Node ID ab4edf89992fb3bb6f61e3ee4d3f99afd05cd2ba # Parent 0d45f21e372d1afad629e58db483284e2d74a75e support indirect corecursion diff -r 0d45f21e372d -r ab4edf89992f src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Wed Sep 04 23:57:38 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Thu Sep 05 01:58:48 2013 +0200 @@ -536,6 +536,9 @@ fun build_corec_args_discs disc_eqns ctr_specs = if null disc_eqns then I else let +(*val _ = tracing ("d/p:\ " ^ space_implode "\n \ " (map ((op ^) o + apfst (Syntax.string_of_term @{context}) o apsnd (curry (op ^) " / " o @{make_string})) + (ctr_specs |> map_filter (fn {disc, pred = SOME pred, ...} => SOME (disc, pred) | _ => NONE))));*) val conds = map #cond disc_eqns; val fun_args = #fun_args (hd disc_eqns); val args = @@ -544,14 +547,15 @@ fst (split_last conds) else if length disc_eqns = length ctr_specs - 1 then let val n = 0 upto length ctr_specs - 1 - |> the o find_first (fn idx => not (exists (equal idx o #ctr_no) disc_eqns)) (*###*) in + |> the(*###*) o find_first (fn idx => not (exists (equal idx o #ctr_no) disc_eqns)) in if n = length ctr_specs - 1 then conds else split_last conds ||> HOLogic.mk_not - |>> chop n - |> (fn ((l, r), x) => l @ (x :: r)) + |> `(uncurry (fold (curry HOLogic.mk_conj o HOLogic.mk_not))) + ||> chop n o fst + |> (fn (x, (l, r)) => l @ (x :: r)) end else 0 upto length ctr_specs - 1 @@ -570,11 +574,12 @@ fun build_corec_arg_no_call sel_eqns sel = find_first (equal sel o #sel) sel_eqns |> try (fn SOME sel_eqn => (#fun_args sel_eqn, #rhs_term sel_eqn)) |> the_default ([], undef_const) - |-> abs_tuple; + |-> abs_tuple + |> K; fun build_corec_arg_direct_call lthy has_call sel_eqns sel = let - val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns + val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns; fun rewrite is_end U T t = if U = @{typ bool} then @{term True} |> has_call t ? K @{term False} (* stop? *) else if is_end = has_call t then undef_const @@ -587,8 +592,33 @@ abs_tuple (#fun_args (the maybe_sel_eqn)) oo massage (#rhs_term (the maybe_sel_eqn)) end; -fun build_corec_arg_indirect_call sel_eqns sel = - primrec_error "indirect corecursion not implemented yet"; +fun build_corec_arg_indirect_call lthy has_call sel_eqns sel = + let + val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns; + fun rewrite _ _ = + let + fun subst (Abs (v, T, b)) = Abs (v, T, subst b) + | subst (t as _ $ _) = + let val (u, vs) = strip_comb t in + if is_Free u andalso has_call u then + Const (@{const_name Inr}, dummyT) $ (*HOLogic.mk_tuple vs*) + (try (foldr1 (fn (x, y) => Const (@{const_name Pair}, dummyT) $ x $ y)) vs + |> the_default (hd vs)) + else if try (fst o dest_Const) u = SOME @{const_name prod_case} then + list_comb (u |> map_types (K dummyT), map subst vs) + else + list_comb (subst u, map subst vs) + end + | subst t = t; + in + subst + end; + fun massage rhs_term t = massage_indirect_corec_call + lthy has_call rewrite [] (fastype_of t |> range_type) rhs_term; + in + if is_none maybe_sel_eqn then I else + abs_tuple (#fun_args (the maybe_sel_eqn)) o massage (#rhs_term (the maybe_sel_eqn)) + end; fun build_corec_args_sel lthy has_call all_sel_eqns ctr_spec = let val sel_eqns = filter (equal (#ctr ctr_spec) o #ctr) all_sel_eqns in @@ -596,9 +626,9 @@ let val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec; -val _ = tracing ("sels / calls:\n \ " ^ space_implode "\n \ " (map ((op ^) o - apfst (Syntax.string_of_term @{context}) o apsnd (curry (op ^) " / " o @{make_string})) - (sel_call_list))); +(*val _ = tracing ("s/c:\ " ^ space_implode "\n \ " (map ((op ^) o + apfst (Syntax.string_of_term lthy) o apsnd (curry (op ^) " / " o @{make_string})) + sel_call_list));*) val no_calls' = map_filter (try (apsnd (fn No_Corec n => n))) sel_call_list; val direct_calls' = map_filter (try (apsnd (fn Direct_Corec n => n))) sel_call_list; @@ -606,12 +636,12 @@ in I #> fold (fn (sel, n) => nth_map n - (build_corec_arg_no_call sel_eqns sel |> K)) no_calls' + (build_corec_arg_no_call sel_eqns sel)) no_calls' #> fold (fn (sel, (q, g, h)) => let val f = build_corec_arg_direct_call lthy has_call sel_eqns sel in nth_map h (f false) o nth_map g (f true) o nth_map q (f true) end) direct_calls' #> fold (fn (sel, n) => nth_map n - (build_corec_arg_indirect_call sel_eqns sel |> K)) indirect_calls' + (build_corec_arg_indirect_call lthy has_call sel_eqns sel)) indirect_calls' end end; @@ -652,18 +682,19 @@ |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts; val _ = tracing ("corecursor arguments:\n \ " ^ - space_implode "\n \ " (map (Syntax.string_of_term @{context}) corec_args)); + space_implode "\n \ " (map (Syntax.string_of_term lthy) corec_args)); fun uneq_pairs_rev xs = xs (* FIXME \? *) |> these o try (split_last #> (fn (ys, y) => uneq_pairs_rev ys @ map (pair y) ys)); val proof_obligations = if sequential then [] else - maps (uneq_pairs_rev o map (fn {fun_args, cond, ...} => (fun_args, cond))) disc_eqnss + disc_eqnss + |> maps (uneq_pairs_rev o map (fn {fun_args, cond, ...} => (fun_args, cond))) |> map (fn ((fun_args, x), (_, y)) => [x, HOLogic.mk_not y] |> map (HOLogic.mk_Trueprop o curry subst_bounds (List.rev fun_args)) |> curry list_comb @{const ==>}); val _ = tracing ("proof obligations:\n \ " ^ - space_implode "\n \ " (map (Syntax.string_of_term @{context}) proof_obligations)); + space_implode "\n \ " (map (Syntax.string_of_term lthy) proof_obligations)); in map (list_comb o rpair corec_args) corecs diff -r 0d45f21e372d -r ab4edf89992f src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 04 23:57:38 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Thu Sep 05 01:58:48 2013 +0200 @@ -198,11 +198,11 @@ fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts res_U t = let val typof = curry fastype_of1 bound_Ts; - val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o fst); + val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd) fun check_and_massage_direct_call U T t = if has_call t then factor_out_types ctxt massage_direct_call dest_sumT U T t - else build_map_Inl (U, T) $ t; + else build_map_Inl (T, U) $ t; fun check_and_massage_unapplied_direct_call U T t = let val var = Var ((Name.uu, Term.maxidx_of_term t + 1), domain_type (typof t)) in @@ -241,11 +241,11 @@ | NONE => (case t of t1 $ t2 => - if has_call t2 then + (if has_call t2 then check_and_massage_direct_call U T t else massage_map U T t1 $ t2 - handle AINT_NO_MAP _ => check_and_massage_direct_call U T t + handle AINT_NO_MAP _ => check_and_massage_direct_call U T t) | _ => check_and_massage_direct_call U T t)) | _ => ill_formed_corec_call ctxt t)) U T