60 (bool * rec_spec list * typ list * thm * thm list * Token.src list * typ list) * local_theory |
60 (bool * rec_spec list * typ list * thm * thm list * Token.src list * typ list) * local_theory |
61 |
61 |
62 val lfp_rec_sugar_interpretation: string -> |
62 val lfp_rec_sugar_interpretation: string -> |
63 (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory |
63 (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory |
64 |
64 |
65 val primrec: rec_option list -> (binding * typ option * mixfix) list -> |
65 val primrec: bool -> rec_option list -> (binding * typ option * mixfix) list -> |
66 Specification.multi_specs -> local_theory -> |
66 Specification.multi_specs -> local_theory -> |
67 (term list * thm list * thm list list) * local_theory |
67 (term list * thm list * thm list list) * local_theory |
68 val primrec_cmd: rec_option list -> (binding * string option * mixfix) list -> |
68 val primrec_cmd: bool -> rec_option list -> (binding * string option * mixfix) list -> |
69 Specification.multi_specs_cmd -> local_theory -> |
69 Specification.multi_specs_cmd -> local_theory -> |
70 (term list * thm list * thm list list) * local_theory |
70 (term list * thm list * thm list list) * local_theory |
71 val primrec_global: rec_option list -> (binding * typ option * mixfix) list -> |
71 val primrec_global: bool -> rec_option list -> (binding * typ option * mixfix) list -> |
72 Specification.multi_specs -> theory -> (term list * thm list * thm list list) * theory |
72 Specification.multi_specs -> theory -> (term list * thm list * thm list list) * theory |
73 val primrec_overloaded: rec_option list -> (string * (string * typ) * bool) list -> |
73 val primrec_overloaded: bool -> rec_option list -> (string * (string * typ) * bool) list -> |
74 (binding * typ option * mixfix) list -> |
74 (binding * typ option * mixfix) list -> |
75 Specification.multi_specs -> theory -> (term list * thm list * thm list list) * theory |
75 Specification.multi_specs -> theory -> (term list * thm list * thm list list) * theory |
76 val primrec_simple: ((binding * typ) * mixfix) list -> term list -> |
76 val primrec_simple: bool -> ((binding * typ) * mixfix) list -> term list -> local_theory -> |
77 local_theory -> |
77 ((string list * (binding -> binding) list) |
78 ((string list * (binding -> binding) list) * |
78 * (term list * thm list * (int list list * thm list list))) * local_theory |
79 (term list * thm list * (int list list * thm list list))) * local_theory |
|
80 end; |
79 end; |
81 |
80 |
82 structure BNF_LFP_Rec_Sugar : BNF_LFP_REC_SUGAR = |
81 structure BNF_LFP_Rec_Sugar : BNF_LFP_REC_SUGAR = |
83 struct |
82 struct |
84 |
83 |
177 {T = T, fp_res_index = 0, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar, |
176 {T = T, fp_res_index = 0, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar, |
178 recx = casex, rec_thms = case_thms}; |
177 recx = casex, rec_thms = case_thms}; |
179 in |
178 in |
180 ([], [0], [basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, ctxt) |
179 ([], [0], [basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, ctxt) |
181 end |
180 end |
|
181 | default_basic_lfp_sugars_of _ [T] _ _ ctxt = |
|
182 error ("Cannot recurse through type " ^ quote (Syntax.string_of_typ ctxt T)) |
182 | default_basic_lfp_sugars_of _ _ _ _ _ = error "Unsupported mutual recursion at this stage"; |
183 | default_basic_lfp_sugars_of _ _ _ _ _ = error "Unsupported mutual recursion at this stage"; |
183 |
184 |
184 fun basic_lfp_sugars_of bs arg_Ts callers callssss lthy = |
185 fun basic_lfp_sugars_of bs arg_Ts callers callssss lthy = |
185 (case Data.get (Proof_Context.theory_of lthy) of |
186 (case Data.get (Proof_Context.theory_of lthy) of |
186 SOME {basic_lfp_sugars_of, ...} => basic_lfp_sugars_of |
187 SOME {basic_lfp_sugars_of, ...} => basic_lfp_sugars_of |
603 (@{fold_map 2} (prove (map (snd o snd) defs)) (take actual_nn rec_specs) funs_data lthy) |
604 (@{fold_map 2} (prove (map (snd o snd) defs)) (take actual_nn rec_specs) funs_data lthy) |
604 end), |
605 end), |
605 lthy |> Local_Theory.notes (notes @ common_notes) |> snd) |
606 lthy |> Local_Theory.notes (notes @ common_notes) |> snd) |
606 end; |
607 end; |
607 |
608 |
608 fun primrec_simple0 plugins nonexhaustive transfer fixes ts lthy = |
609 fun primrec_simple0 int plugins nonexhaustive transfer fixes ts lthy = |
609 let |
610 let |
610 val actual_nn = length fixes; |
611 val actual_nn = length fixes; |
611 |
612 |
612 val nonexhaustives = replicate actual_nn nonexhaustive; |
613 val nonexhaustives = replicate actual_nn nonexhaustive; |
613 val transfers = replicate actual_nn transfer; |
614 val transfers = replicate actual_nn transfer; |
615 val (((names, qualifys, defs), prove), lthy') = |
616 val (((names, qualifys, defs), prove), lthy') = |
616 prepare_primrec plugins nonexhaustives transfers fixes ts lthy; |
617 prepare_primrec plugins nonexhaustives transfers fixes ts lthy; |
617 in |
618 in |
618 lthy' |
619 lthy' |
619 |> fold_map Local_Theory.define defs |
620 |> fold_map Local_Theory.define defs |
|
621 |> tap (uncurry (print_def_consts int)) |
620 |-> (fn defs => fn lthy => |
622 |-> (fn defs => fn lthy => |
621 let val ((jss, simpss), lthy) = prove lthy defs in |
623 let val ((jss, simpss), lthy) = prove lthy defs in |
622 (((names, qualifys), (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy) |
624 (((names, qualifys), (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy) |
623 end) |
625 end) |
624 end; |
626 end; |
625 |
627 |
626 fun primrec_simple fixes ts lthy = |
628 fun primrec_simple int fixes ts lthy = |
627 primrec_simple0 Plugin_Name.default_filter false false fixes ts lthy |
629 primrec_simple0 int Plugin_Name.default_filter false false fixes ts lthy |
628 handle OLD_PRIMREC () => |
630 handle OLD_PRIMREC () => |
629 Old_Primrec.primrec_simple fixes ts lthy |
631 Old_Primrec.primrec_simple int fixes ts lthy |
630 |>> apsnd (fn (ts, thms) => (ts, [], ([], [thms]))) o apfst single |
632 |>> apsnd (fn (ts, thms) => (ts, [], ([], [thms]))) o apfst single |
631 |>> apfst (map_split (rpair I)); |
633 |>> apfst (map_split (rpair I)); |
632 |
634 |
633 fun gen_primrec old_primrec prep_spec opts raw_fixes raw_specs lthy = |
635 fun gen_primrec old_primrec prep_spec int opts raw_fixes raw_specs lthy = |
634 let |
636 let |
635 val dups = duplicates (op =) (map (fn (x, _, _) => Binding.name_of x) raw_fixes); |
637 val dups = duplicates (op =) (map (fn (x, _, _) => Binding.name_of x) raw_fixes); |
636 val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups)); |
638 val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups)); |
637 |
639 |
638 val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts) |
640 val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts) |
656 in |
658 in |
657 ((qualify (Binding.qualify true prefix (Binding.name simpsN)), []), [(thms, [])]) :: notes |
659 ((qualify (Binding.qualify true prefix (Binding.name simpsN)), []), [(thms, [])]) :: notes |
658 end); |
660 end); |
659 in |
661 in |
660 lthy |
662 lthy |
661 |> primrec_simple0 plugins nonexhaustive transfer fixes (map snd specs) |
663 |> primrec_simple0 int plugins nonexhaustive transfer fixes (map snd specs) |
662 |-> (fn ((names, qualifys), (ts, defs, (jss, simpss))) => |
664 |-> (fn ((names, qualifys), (ts, defs, (jss, simpss))) => |
663 Spec_Rules.add Spec_Rules.Equational (ts, flat simpss) |
665 Spec_Rules.add Spec_Rules.Equational (ts, flat simpss) |
664 #> Local_Theory.notes (mk_notes jss names qualifys simpss) |
666 #> Local_Theory.notes (mk_notes jss names qualifys simpss) |
665 #>> (fn notes => (ts, defs, map_filter (fn ("", _) => NONE | (_, thms) => SOME thms) notes))) |
667 #>> (fn notes => (ts, defs, map_filter (fn ("", _) => NONE | (_, thms) => SOME thms) notes))) |
666 end |
668 end |
667 handle OLD_PRIMREC () => |
669 handle OLD_PRIMREC () => |
668 old_primrec raw_fixes raw_specs lthy |
670 old_primrec int raw_fixes raw_specs lthy |
669 |>> (fn (ts, thms) => (ts, [], [thms])); |
671 |>> (fn (ts, thms) => (ts, [], [thms])); |
670 |
672 |
671 val primrec = gen_primrec Old_Primrec.primrec Specification.check_multi_specs; |
673 val primrec = gen_primrec Old_Primrec.primrec Specification.check_multi_specs; |
672 val primrec_cmd = gen_primrec Old_Primrec.primrec_cmd Specification.read_multi_specs; |
674 val primrec_cmd = gen_primrec Old_Primrec.primrec_cmd Specification.read_multi_specs; |
673 |
675 |
674 fun primrec_global opts fixes specs = |
676 fun primrec_global int opts fixes specs = |
675 Named_Target.theory_init |
677 Named_Target.theory_init |
676 #> primrec opts fixes specs |
678 #> primrec int opts fixes specs |
677 ##> Local_Theory.exit_global; |
679 ##> Local_Theory.exit_global; |
678 |
680 |
679 fun primrec_overloaded opts ops fixes specs = |
681 fun primrec_overloaded int opts ops fixes specs = |
680 Overloading.overloading ops |
682 Overloading.overloading ops |
681 #> primrec opts fixes specs |
683 #> primrec int opts fixes specs |
682 ##> Local_Theory.exit_global; |
684 ##> Local_Theory.exit_global; |
683 |
685 |
684 val rec_option_parser = Parse.group (K "option") |
686 val rec_option_parser = Parse.group (K "option") |
685 (Plugin_Name.parse_filter >> Plugins_Option |
687 (Plugin_Name.parse_filter >> Plugins_Option |
686 || Parse.reserved "nonexhaustive" >> K Nonexhaustive_Option |
688 || Parse.reserved "nonexhaustive" >> K Nonexhaustive_Option |
688 |
690 |
689 val _ = Outer_Syntax.local_theory @{command_keyword primrec} |
691 val _ = Outer_Syntax.local_theory @{command_keyword primrec} |
690 "define primitive recursive functions" |
692 "define primitive recursive functions" |
691 ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser) |
693 ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser) |
692 --| @{keyword ")"}) []) -- Parse_Spec.specification |
694 --| @{keyword ")"}) []) -- Parse_Spec.specification |
693 >> (fn (opts, (fixes, specs)) => snd o primrec_cmd opts fixes specs)); |
695 >> (fn (opts, (fixes, specs)) => snd o primrec_cmd true opts fixes specs)); |
694 |
696 |
695 end; |
697 end; |