# HG changeset patch # User Andreas Lochbihler # Date 1378134891 -7200 # Node ID f6629734dd2b5c36b697d2c608b869aafbb3f7d1 # Parent 735e078a64e74fec1171c074868af59e6f08a5ca# Parent 7ffc4a746a73791e4f6993be0ca0e764d5ac4e98 merged diff -r 735e078a64e7 -r f6629734dd2b README_REPOSITORY --- a/README_REPOSITORY Mon Sep 02 17:14:35 2013 +0200 +++ b/README_REPOSITORY Mon Sep 02 17:14:51 2013 +0200 @@ -38,7 +38,7 @@ 4. Access documentation (bash shell commands): - ./bin/isabelle build_doc -p -a + ./bin/isabelle build_doc -a ./bin/isabelle doc system diff -r 735e078a64e7 -r f6629734dd2b src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Mon Sep 02 17:14:35 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Mon Sep 02 17:14:51 2013 +0200 @@ -499,7 +499,7 @@ val sel_imp_rhss = (#sels ctr_spec ~~ ctr_args) |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg)); -val _ = warning ("reduced\n " ^ Syntax.string_of_term @{context} imp_rhs ^ "\nto\n \ " ^ +val _ = tracing ("reduced\n " ^ Syntax.string_of_term @{context} imp_rhs ^ "\nto\n \ " ^ (is_some maybe_eqn_data_disc ? K (Syntax.string_of_term @{context} disc_imp_rhs ^ "\n \ ")) "" ^ space_implode "\n \ " (map (Syntax.string_of_term @{context}) sel_imp_rhss)); @@ -570,45 +570,57 @@ fold2 (fn idx => nth_map idx o K o abs_tuple) (map_filter #pred ctr_specs) args' end; -fun build_corec_args_sel all_sel_eqns ctr_spec = +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 |> map dest_Free, #rhs_term sel_eqn)) + |> the_default ([], undef_const) + |-> abs_tuple oo fold_rev absfree; + +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 + + fun rewrite U T t = + if U = @{typ bool} then @{term True} |> has_call t ? K @{term False} (* stop? *) + else if T = U = has_call t then undef_const + else if T = U then t (* end *) + else HOLogic.mk_tuple (snd (strip_comb t)); (* continue *) + fun massage rhs_term t = + massage_direct_corec_call lthy has_call rewrite [] (body_type (fastype_of t)) rhs_term; + val abstract = abs_tuple oo fold_rev absfree o map dest_Free; + in + if is_none maybe_sel_eqn then I else + massage (#rhs_term (the maybe_sel_eqn)) #> abstract (#fun_args (the maybe_sel_eqn)) + end; + +fun build_corec_arg_indirect_call sel_eqns sel = + primrec_error "indirect corecursion not implemented yet"; + +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 if null sel_eqns then I else let val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec; -val _ = warning ("sels / calls:\n \ " ^ space_implode "\n \ " (map ((op ^) o +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))); - (* FIXME get rid of dummy_no_calls' *) - val dummy_no_calls' = map_filter (try (apsnd (fn Dummy_No_Corec n => n))) 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; val indirect_calls' = map_filter (try (apsnd (fn Indirect_Corec n => n))) sel_call_list; - - fun build_arg_no_call sel = find_first (equal sel o #sel) sel_eqns |> #rhs_term o the; - fun build_arg_direct_call sel = primrec_error "not implemented yet"; - fun build_arg_indirect_call sel = primrec_error "not implemented yet"; - - val update_args = I - #> fold (fn (sel, rec_arg_idx) => nth_map rec_arg_idx - (build_arg_no_call sel |> K)) no_calls' - #> fold (fn (sel, rec_arg_idx) => nth_map rec_arg_idx - (build_arg_indirect_call sel |> K)) indirect_calls' - #> fold (fn (sel, (q_idx, g_idx, h_idx)) => - let val (q, g, h) = build_arg_indirect_call sel in - nth_map q_idx (K q) o nth_map g_idx (K g) o nth_map h_idx (K h) end) direct_calls'; - - val arg_idxs = maps (fn (_, (x, y, z)) => [x, y, z]) direct_calls' @ - maps (map snd) [dummy_no_calls', no_calls', indirect_calls']; - val abs_args = fold (fn idx => nth_map idx - (abs_tuple o fold_rev absfree (sel_eqns |> #fun_args o hd |> map dest_Free))) arg_idxs; in - abs_args o update_args + I + #> fold (fn (sel, n) => nth_map n + (build_corec_arg_no_call sel_eqns sel |> K)) 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 o nth_map g f o nth_map q f end) direct_calls' + #> fold (fn (sel, n) => nth_map n + (build_corec_arg_indirect_call sel_eqns sel |> K)) indirect_calls' end end; -fun co_build_defs lthy sequential bs mxs arg_Tss fun_name_corec_spec_list eqns_data = +fun co_build_defs lthy sequential bs mxs has_call arg_Tss fun_name_corec_spec_list eqns_data = let val fun_names = map Binding.name_of bs; @@ -622,24 +634,24 @@ primrec_error_eqns "excess discriminator equations in definition" (maps (fn t => filter (equal (#ctr_no t) o #ctr_no) x) d |> map #user_eqn) end); -val _ = warning ("disc_eqnss:\n \ " ^ space_implode "\n \ " (map @{make_string} disc_eqnss)); +(*val _ = tracing ("disc_eqnss:\n \ " ^ space_implode "\n \ " (map @{make_string} disc_eqnss));*) val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data |> partition_eq ((op =) o pairself #fun_name) |> finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names |> fst |> map (flat o snd); -val _ = warning ("sel_eqnss:\n \ " ^ space_implode "\n \ " (map @{make_string} sel_eqnss)); +(*val _ = tracing ("sel_eqnss:\n \ " ^ space_implode "\n \ " (map @{make_string} sel_eqnss));*) val corecs = map (#corec o snd) fun_name_corec_spec_list; val ctr_specss = map (#ctr_specs o snd) fun_name_corec_spec_list; - val n_args = fold (curry (op +)) (map (K 1) (maps (map_filter #pred) ctr_specss) @ - map (fn Direct_Corec _ => 3 | _ => 1) (maps (maps #calls) ctr_specss)) 0; - val corec_args = replicate n_args undef_const + val corec_args = hd corecs + |> fst o split_last o binder_types o fastype_of + |> map (Const o pair @{const_name undefined}) |> fold2 build_corec_args_discs disc_eqnss ctr_specss - |> fold2 (fn sel_eqns => fold (build_corec_args_sel sel_eqns)) sel_eqnss ctr_specss; + |> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss; -val _ = warning ("corecursor arguments:\n \ " ^ +val _ = tracing ("corecursor arguments:\n \ " ^ space_implode "\n \ " (map (Syntax.string_of_term @{context}) corec_args)); fun uneq_pairs_rev xs = xs (* FIXME \? *) @@ -685,16 +697,17 @@ val fun_names = map Binding.name_of bs; val fun_name_corec_spec_list = (fun_names ~~ res_Ts, corec_specs) - |> uncurry (finds (fn ((v, T), {corec, ...}) => T = body_type (fastype_of corec))) |> fst + |> uncurry (finds (fn ((_, T), {corec, ...}) => T = body_type (fastype_of corec))) |> fst |> map (apfst fst #> apsnd the_single); (*###*) val (eqns_data, _) = fold_map (co_dissect_eqn sequential fun_name_corec_spec_list) (map snd specs) [] |>> flat; + val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =)); + val arg_Tss = map (binder_types o snd o fst) fixes; val (defs, proof_obligations) = - co_build_defs lthy' sequential bs mxs (map (binder_types o snd o fst) fixes) - fun_name_corec_spec_list eqns_data; + co_build_defs lthy' sequential bs mxs has_call arg_Tss fun_name_corec_spec_list eqns_data; in lthy' |> fold_map Local_Theory.define defs |> snd