src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
author blanchet
Wed, 14 Jul 2021 10:02:43 +0200
changeset 73977 2d8a0f8e30ec
parent 71214 5727bcc3c47c
child 74561 8e6c973003c8
permissions -rw-r--r--
correctly translate constructor argument in 'primrec'
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55061
a0adf838e2d1 adjusted comments
blanchet
parents: 55060
diff changeset
     1
(*  Title:      HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
     2
    Author:     Lorenz Panny, TU Muenchen
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
     4
    Copyright   2013
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
     5
58315
6d8458bc6e27 tuning terminology
blanchet
parents: 58304
diff changeset
     6
Recursor sugar ("primrec").
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
     7
*)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
     8
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
     9
signature BNF_LFP_REC_SUGAR =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
    10
sig
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
    11
  datatype rec_option =
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
    12
    Plugins_Option of Proof.context -> Plugin_Name.filter |
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
    13
    Nonexhaustive_Option |
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
    14
    Transfer_Option
56121
52e8f110fec3 print warning if some constructors are missing;
panny
parents: 55869
diff changeset
    15
58223
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    16
  datatype rec_call =
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    17
    No_Rec of int * typ |
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    18
    Mutual_Rec of (int * typ) * (int * typ) |
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    19
    Nested_Rec of int * typ
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    20
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    21
  type rec_ctr_spec =
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    22
    {ctr: term,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    23
     offset: int,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    24
     calls: rec_call list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    25
     rec_thm: thm}
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    26
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    27
  type rec_spec =
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    28
    {recx: term,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    29
     fp_nesting_map_ident0s: thm list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    30
     fp_nesting_map_comps: thm list,
62326
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
    31
     fp_nesting_pred_maps: thm list,
58223
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    32
     ctr_specs: rec_ctr_spec list}
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    33
55571
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
    34
  type basic_lfp_sugar =
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
    35
    {T: typ,
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
    36
     fp_res_index: int,
55574
4a940ebceef8 rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents: 55573
diff changeset
    37
     C: typ,
4a940ebceef8 rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents: 55573
diff changeset
    38
     fun_arg_Tsss : typ list list list,
55571
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
    39
     ctr_sugar: Ctr_Sugar.ctr_sugar,
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
    40
     recx: term,
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
    41
     rec_thms: thm list};
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
    42
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
    43
  type lfp_rec_extension =
55575
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55574
diff changeset
    44
    {nested_simps: thm list,
66290
88714f2e40e8 strengthened tactic
blanchet
parents: 66288
diff changeset
    45
     special_endgame_tac: Proof.context -> thm list -> thm list -> thm list -> tactic,
55575
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55574
diff changeset
    46
     is_new_datatype: Proof.context -> string -> bool,
58389
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
    47
     basic_lfp_sugars_of: binding list -> typ list -> term list ->
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55576
diff changeset
    48
       (term * term list list) list list -> local_theory ->
62326
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
    49
       typ list * int list * basic_lfp_sugar list * thm list * thm list * thm list * thm
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
    50
       * Token.src list * bool * local_theory,
58389
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
    51
     rewrite_nested_rec_call: (Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
    52
       term -> term -> term -> term) option};
55575
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55574
diff changeset
    53
55571
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
    54
  val register_lfp_rec_extension: lfp_rec_extension -> theory -> theory
58389
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
    55
  val default_basic_lfp_sugars_of: binding list -> typ list -> term list ->
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
    56
    (term * term list list) list list -> local_theory ->
62326
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
    57
    typ list * int list * basic_lfp_sugar list * thm list * thm list * thm list * thm
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
    58
    * Token.src list * bool * local_theory
58223
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    59
  val rec_specs_of: binding list -> typ list -> typ list -> term list ->
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58220
diff changeset
    60
    (term * term list list) list list -> local_theory ->
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
    61
    (bool * rec_spec list * typ list * thm * thm list * Token.src list * typ list) * local_theory
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
    62
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
    63
  val lfp_rec_sugar_interpretation: string ->
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
    64
    (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
55571
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
    65
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
    66
  val primrec: bool -> rec_option list -> (binding * typ option * mixfix) list ->
63719
9084d77f1119 tuned signature
traytel
parents: 63239
diff changeset
    67
    Specification.multi_specs -> local_theory ->
9084d77f1119 tuned signature
traytel
parents: 63239
diff changeset
    68
    (term list * thm list * thm list list) * local_theory
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
    69
  val primrec_cmd: bool -> rec_option list -> (binding * string option * mixfix) list ->
63064
2f18172214c8 support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents: 62497
diff changeset
    70
    Specification.multi_specs_cmd -> local_theory ->
60004
e27e7be1f2f6 have 'primrec' return definitions
blanchet
parents: 60003
diff changeset
    71
    (term list * thm list * thm list list) * local_theory
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
    72
  val primrec_global: bool -> rec_option list -> (binding * typ option * mixfix) list ->
63064
2f18172214c8 support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents: 62497
diff changeset
    73
    Specification.multi_specs -> theory -> (term list * thm list * thm list list) * theory
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
    74
  val primrec_overloaded: bool -> rec_option list -> (string * (string * typ) * bool) list ->
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
    75
    (binding * typ option * mixfix) list ->
63064
2f18172214c8 support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents: 62497
diff changeset
    76
    Specification.multi_specs -> theory -> (term list * thm list * thm list list) * theory
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
    77
  val primrec_simple: bool -> ((binding * typ) * mixfix) list -> term list -> local_theory ->
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
    78
    ((string list * (binding -> binding) list)
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
    79
     * (term list * thm list * (int list list * thm list list))) * local_theory
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
    80
end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
    81
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
    82
structure BNF_LFP_Rec_Sugar : BNF_LFP_REC_SUGAR =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
    83
struct
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
    84
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
    85
open Ctr_Sugar
55575
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55574
diff changeset
    86
open Ctr_Sugar_Util
55574
4a940ebceef8 rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents: 55573
diff changeset
    87
open Ctr_Sugar_General_Tactics
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
    88
open BNF_FP_Rec_Sugar_Util
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
    89
58387
blanchet
parents: 58315
diff changeset
    90
val inductN = "induct";
blanchet
parents: 58315
diff changeset
    91
val simpsN = "simps";
55575
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55574
diff changeset
    92
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
    93
val nitpicksimp_attrs = @{attributes [nitpick_simp]};
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
    94
val simp_attrs = @{attributes [simp]};
59283
5ca195783da8 generate [code] only with 'code' plugin enabled
blanchet
parents: 59281
diff changeset
    95
val nitpicksimp_simp_attrs = nitpicksimp_attrs @ simp_attrs;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
    96
55528
c367f4f3e5d4 have 'primrec_new' fall back on old 'primrec' when given old-style datatypes
blanchet
parents: 55527
diff changeset
    97
exception OLD_PRIMREC of unit;
59595
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59352
diff changeset
    98
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
    99
datatype rec_option =
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   100
  Plugins_Option of Proof.context -> Plugin_Name.filter |
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   101
  Nonexhaustive_Option |
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   102
  Transfer_Option;
56121
52e8f110fec3 print warning if some constructors are missing;
panny
parents: 55869
diff changeset
   103
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   104
datatype rec_call =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   105
  No_Rec of int * typ |
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   106
  Mutual_Rec of (int * typ) * (int * typ) |
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   107
  Nested_Rec of int * typ;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   108
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   109
type rec_ctr_spec =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   110
  {ctr: term,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   111
   offset: int,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   112
   calls: rec_call list,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   113
   rec_thm: thm};
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   114
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   115
type rec_spec =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   116
  {recx: term,
57399
cfc19f0a6261 compile
blanchet
parents: 57397
diff changeset
   117
   fp_nesting_map_ident0s: thm list,
57397
5004aca20821 tuned variable names
blanchet
parents: 56945
diff changeset
   118
   fp_nesting_map_comps: thm list,
62326
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
   119
   fp_nesting_pred_maps: thm list,
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   120
   ctr_specs: rec_ctr_spec list};
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   121
55538
blanchet
parents: 55535
diff changeset
   122
type basic_lfp_sugar =
blanchet
parents: 55535
diff changeset
   123
  {T: typ,
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   124
   fp_res_index: int,
55574
4a940ebceef8 rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents: 55573
diff changeset
   125
   C: typ,
4a940ebceef8 rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents: 55573
diff changeset
   126
   fun_arg_Tsss : typ list list list,
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   127
   ctr_sugar: ctr_sugar,
55570
blanchet
parents: 55539
diff changeset
   128
   recx: term,
blanchet
parents: 55539
diff changeset
   129
   rec_thms: thm list};
55538
blanchet
parents: 55535
diff changeset
   130
55571
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   131
type lfp_rec_extension =
55575
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55574
diff changeset
   132
  {nested_simps: thm list,
66290
88714f2e40e8 strengthened tactic
blanchet
parents: 66288
diff changeset
   133
   special_endgame_tac: Proof.context -> thm list -> thm list -> thm list -> tactic,
55575
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55574
diff changeset
   134
   is_new_datatype: Proof.context -> string -> bool,
58389
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   135
   basic_lfp_sugars_of: binding list -> typ list -> term list ->
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55576
diff changeset
   136
     (term * term list list) list list -> local_theory ->
62326
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
   137
     typ list * int list * basic_lfp_sugar list * thm list * thm list * thm list * thm
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
   138
     * Token.src list * bool * local_theory,
58389
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   139
   rewrite_nested_rec_call: (Proof.context -> (term -> bool) -> (string -> int) -> typ list ->
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   140
     term -> term -> term -> term) option};
55571
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   141
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   142
structure Data = Theory_Data
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   143
(
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   144
  type T = lfp_rec_extension option;
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   145
  val empty = NONE;
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   146
  val extend = I;
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   147
  val merge = merge_options;
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   148
);
55538
blanchet
parents: 55535
diff changeset
   149
55571
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   150
val register_lfp_rec_extension = Data.put o SOME;
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   151
55575
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55574
diff changeset
   152
fun nested_simps ctxt =
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55574
diff changeset
   153
  (case Data.get (Proof_Context.theory_of ctxt) of
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55574
diff changeset
   154
    SOME {nested_simps, ...} => nested_simps
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55574
diff changeset
   155
  | NONE => []);
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55574
diff changeset
   156
66290
88714f2e40e8 strengthened tactic
blanchet
parents: 66288
diff changeset
   157
fun special_endgame_tac ctxt =
88714f2e40e8 strengthened tactic
blanchet
parents: 66288
diff changeset
   158
  (case Data.get (Proof_Context.theory_of ctxt) of
88714f2e40e8 strengthened tactic
blanchet
parents: 66288
diff changeset
   159
    SOME {special_endgame_tac, ...} => special_endgame_tac ctxt
88714f2e40e8 strengthened tactic
blanchet
parents: 66288
diff changeset
   160
  | NONE => K (K (K no_tac)));
88714f2e40e8 strengthened tactic
blanchet
parents: 66288
diff changeset
   161
55571
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   162
fun is_new_datatype ctxt =
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   163
  (case Data.get (Proof_Context.theory_of ctxt) of
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   164
    SOME {is_new_datatype, ...} => is_new_datatype ctxt
58389
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   165
  | NONE => K true);
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   166
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   167
fun default_basic_lfp_sugars_of _ [Type (arg_T_name, _)] _ _ ctxt =
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   168
    let
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   169
      val ctr_sugar as {T, ctrs, casex, case_thms, ...} =
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   170
        (case ctr_sugar_of ctxt arg_T_name of
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   171
          SOME ctr_sugar => ctr_sugar
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   172
        | NONE => error ("Unsupported type " ^ quote arg_T_name ^ " at this stage"));
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   173
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   174
      val C = body_type (fastype_of casex);
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   175
      val fun_arg_Tsss = map (map single o binder_types o fastype_of) ctrs;
55571
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   176
58389
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   177
      val basic_lfp_sugar =
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   178
        {T = T, fp_res_index = 0, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar,
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   179
         recx = casex, rec_thms = case_thms};
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   180
    in
62326
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
   181
      ([], [0], [basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, ctxt)
58389
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   182
    end
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
   183
  | default_basic_lfp_sugars_of _ [T] _ _ ctxt =
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
   184
    error ("Cannot recurse through type " ^ quote (Syntax.string_of_typ ctxt T))
58389
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   185
  | default_basic_lfp_sugars_of _ _ _ _ _ = error "Unsupported mutual recursion at this stage";
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   186
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   187
fun basic_lfp_sugars_of bs arg_Ts callers callssss lthy =
55571
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   188
  (case Data.get (Proof_Context.theory_of lthy) of
58389
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   189
    SOME {basic_lfp_sugars_of, ...} => basic_lfp_sugars_of
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   190
  | NONE => default_basic_lfp_sugars_of) bs arg_Ts callers callssss lthy;
55571
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   191
55575
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55574
diff changeset
   192
fun rewrite_nested_rec_call ctxt =
55571
a6153343c44f prepare two-stage 'primrec' setup
blanchet
parents: 55570
diff changeset
   193
  (case Data.get (Proof_Context.theory_of ctxt) of
58389
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   194
    SOME {rewrite_nested_rec_call = SOME f, ...} => f ctxt
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   195
  | _ => error "Unsupported nested recursion");
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   196
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   197
structure LFP_Rec_Sugar_Plugin = Plugin(type T = fp_rec_sugar);
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   198
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   199
fun lfp_rec_sugar_interpretation name f =
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   200
  LFP_Rec_Sugar_Plugin.interpretation name (fn fp_rec_sugar => fn lthy =>
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   201
    f (transfer_fp_rec_sugar (Proof_Context.theory_of lthy) fp_rec_sugar) lthy);
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   202
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   203
val interpret_lfp_rec_sugar = LFP_Rec_Sugar_Plugin.data;
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   204
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55576
diff changeset
   205
fun rec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =
55538
blanchet
parents: 55535
diff changeset
   206
  let
blanchet
parents: 55535
diff changeset
   207
    val thy = Proof_Context.theory_of lthy0;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   208
57399
cfc19f0a6261 compile
blanchet
parents: 57397
diff changeset
   209
    val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, fp_nesting_map_ident0s, fp_nesting_map_comps,
62326
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
   210
         fp_nesting_pred_maps, common_induct, induct_attrs, n2m, lthy) =
58389
ee1f45ca0d73 made new 'primrec' bootstrapping-capable
blanchet
parents: 58388
diff changeset
   211
      basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   212
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58996
diff changeset
   213
    val perm_basic_lfp_sugars = sort (int_ord o apply2 #fp_res_index) basic_lfp_sugars;
55538
blanchet
parents: 55535
diff changeset
   214
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   215
    val indices = map #fp_res_index basic_lfp_sugars;
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   216
    val perm_indices = map #fp_res_index perm_basic_lfp_sugars;
55538
blanchet
parents: 55535
diff changeset
   217
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   218
    val perm_ctrss = map (#ctrs o #ctr_sugar) perm_basic_lfp_sugars;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   219
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   220
    val nn0 = length arg_Ts;
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   221
    val nn = length perm_ctrss;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   222
    val kks = 0 upto nn - 1;
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   223
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   224
    val perm_ctr_offsets = map (fn kk => Integer.sum (map length (take kk perm_ctrss))) kks;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   225
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58112
diff changeset
   226
    val perm_fpTs = map #T perm_basic_lfp_sugars;
55574
4a940ebceef8 rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents: 55573
diff changeset
   227
    val perm_Cs = map #C perm_basic_lfp_sugars;
4a940ebceef8 rewrote a small portion of code to avoid dependency on low-level constant
blanchet
parents: 55573
diff changeset
   228
    val perm_fun_arg_Tssss = map #fun_arg_Tsss perm_basic_lfp_sugars;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   229
55480
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55464
diff changeset
   230
    fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs;
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55464
diff changeset
   231
    fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   232
56857
aa2de99be748 note correct induction schemes in 'primrec' (for N2M)
blanchet
parents: 56651
diff changeset
   233
    val inducts = unpermute0 (conj_dests nn common_induct);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   234
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58112
diff changeset
   235
    val fpTs = unpermute perm_fpTs;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   236
    val Cs = unpermute perm_Cs;
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   237
    val ctr_offsets = unpermute perm_ctr_offsets;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   238
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58112
diff changeset
   239
    val As_rho = tvar_subst thy (take nn0 fpTs) arg_Ts;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   240
    val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   241
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   242
    val substA = Term.subst_TVars As_rho;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   243
    val substAT = Term.typ_subst_TVars As_rho;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   244
    val substCT = Term.typ_subst_TVars Cs_rho;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   245
    val substACT = substAT o substCT;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   247
    val perm_Cs' = map substCT perm_Cs;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   248
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   249
    fun call_of [i] [T] = (if exists_subtype_in Cs T then Nested_Rec else No_Rec) (i, substACT T)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   250
      | call_of [i, i'] [T, T'] = Mutual_Rec ((i, substACT T), (i', substACT T'));
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   251
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   252
    fun mk_ctr_spec ctr offset fun_arg_Tss rec_thm =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   253
      let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   254
        val (fun_arg_hss, _) = indexedd fun_arg_Tss 0;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   255
        val fun_arg_hs = flat_rec_arg_args fun_arg_hss;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   256
        val fun_arg_iss = map (map (find_index_eq fun_arg_hs)) fun_arg_hss;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   257
      in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   258
        {ctr = substA ctr, offset = offset, calls = map2 call_of fun_arg_iss fun_arg_Tss,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   259
         rec_thm = rec_thm}
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   260
      end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   261
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   262
    fun mk_ctr_specs fp_res_index k ctrs rec_thms =
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58389
diff changeset
   263
      @{map 4} mk_ctr_spec ctrs (k upto k + length ctrs - 1) (nth perm_fun_arg_Tssss fp_res_index)
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   264
        rec_thms;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   265
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   266
    fun mk_spec ctr_offset
55570
blanchet
parents: 55539
diff changeset
   267
        ({T, fp_res_index, ctr_sugar = {ctrs, ...}, recx, rec_thms, ...} : basic_lfp_sugar) =
58211
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58187
diff changeset
   268
      {recx = mk_co_rec thy Least_FP perm_Cs' (substAT T) recx,
57399
cfc19f0a6261 compile
blanchet
parents: 57397
diff changeset
   269
       fp_nesting_map_ident0s = fp_nesting_map_ident0s, fp_nesting_map_comps = fp_nesting_map_comps,
62326
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
   270
       fp_nesting_pred_maps = fp_nesting_pred_maps,
55570
blanchet
parents: 55539
diff changeset
   271
       ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms};
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   272
  in
58283
71d74e641538 preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents: 58281
diff changeset
   273
    ((n2m, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, common_induct, inducts,
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   274
      induct_attrs, map #T basic_lfp_sugars), lthy)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   275
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   276
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67522
diff changeset
   277
val undef_const = Const (\<^const_name>\<open>undefined\<close>, dummyT);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   278
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   279
type eqn_data = {
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   280
  fun_name: string,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   281
  rec_type: typ,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   282
  ctr: term,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   283
  ctr_args: term list,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   284
  left_args: term list,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   285
  right_args: term list,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   286
  res_type: typ,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   287
  rhs_term: term,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   288
  user_eqn: term
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   289
};
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   290
59595
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59352
diff changeset
   291
fun dissect_eqn ctxt fun_names eqn0 =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   292
  let
59595
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59352
diff changeset
   293
    val eqn = drop_all eqn0 |> HOLogic.dest_Trueprop
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   294
      handle TERM _ => ill_formed_equation_lhs_rhs ctxt [eqn0];
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   295
    val (lhs, rhs) = HOLogic.dest_eq eqn
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   296
      handle TERM _ => ill_formed_equation_lhs_rhs ctxt [eqn];
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   297
    val (fun_name, args) = strip_comb lhs
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   298
      |>> (fn x => if is_Free x then fst (dest_Free x) else ill_formed_equation_head ctxt [eqn]);
67522
9e712280cc37 clarified take/drop/chop prefix/suffix;
wenzelm
parents: 66290
diff changeset
   299
    val (left_args, rest) = chop_prefix is_Free args;
9e712280cc37 clarified take/drop/chop prefix/suffix;
wenzelm
parents: 66290
diff changeset
   300
    val (nonfrees, right_args) = chop_suffix is_Free rest;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   301
    val num_nonfrees = length nonfrees;
59595
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59352
diff changeset
   302
    val _ = num_nonfrees = 1 orelse
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   303
      (if num_nonfrees = 0 then missing_pattern ctxt [eqn]
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   304
       else more_than_one_nonvar_in_lhs ctxt [eqn]);
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   305
    val _ = member (op =) fun_names fun_name orelse raise ill_formed_equation_head ctxt [eqn];
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   306
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   307
    val (ctr, ctr_args) = strip_comb (the_single nonfrees);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   308
    val _ = try (num_binder_types o fastype_of) ctr = SOME (length ctr_args) orelse
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   309
      partially_applied_ctr_in_pattern ctxt [eqn];
59595
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59352
diff changeset
   310
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   311
    val _ = check_duplicate_variables_in_lhs ctxt [eqn] (left_args @ ctr_args @ right_args)
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   312
    val _ = forall is_Free ctr_args orelse nonprimitive_pattern_in_lhs ctxt [eqn];
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   313
    val _ =
58302
blanchet
parents: 58301
diff changeset
   314
      let
59595
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59352
diff changeset
   315
        val bads =
58302
blanchet
parents: 58301
diff changeset
   316
          fold_aterms (fn x as Free (v, _) =>
blanchet
parents: 58301
diff changeset
   317
              if (not (member (op =) (left_args @ ctr_args @ right_args) x) andalso
blanchet
parents: 58301
diff changeset
   318
                  not (member (op =) fun_names v) andalso not (Variable.is_fixed ctxt v)) then
blanchet
parents: 58301
diff changeset
   319
                cons x
blanchet
parents: 58301
diff changeset
   320
              else
blanchet
parents: 58301
diff changeset
   321
                I
blanchet
parents: 58301
diff changeset
   322
            | _ => I) rhs [];
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   323
      in
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   324
        null bads orelse extra_variable_in_rhs ctxt [eqn] (hd bads)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   325
      end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   326
  in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   327
    {fun_name = fun_name,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   328
     rec_type = body_type (type_of ctr),
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   329
     ctr = ctr,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   330
     ctr_args = ctr_args,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   331
     left_args = left_args,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   332
     right_args = right_args,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   333
     res_type = map fastype_of (left_args @ right_args) ---> fastype_of rhs,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   334
     rhs_term = rhs,
59595
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59352
diff changeset
   335
     user_eqn = eqn0}
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   336
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   337
58302
blanchet
parents: 58301
diff changeset
   338
fun subst_rec_calls ctxt get_ctr_pos has_call ctr_args mutual_calls nested_calls =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   339
  let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   340
    fun try_nested_rec bound_Ts y t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   341
      AList.lookup (op =) nested_calls y
58302
blanchet
parents: 58301
diff changeset
   342
      |> Option.map (fn y' => rewrite_nested_rec_call ctxt has_call get_ctr_pos bound_Ts y y' t);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   343
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   344
    fun subst bound_Ts (t as g' $ y) =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   345
        let
58303
a0fe6d8c8ba2 fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
blanchet
parents: 58302
diff changeset
   346
          fun subst_comb (h $ z) = subst bound_Ts h $ subst bound_Ts z
a0fe6d8c8ba2 fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
blanchet
parents: 58302
diff changeset
   347
            | subst_comb t = t;
58301
de95aeedf49e fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'
blanchet
parents: 58283
diff changeset
   348
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   349
          val y_head = head_of y;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   350
        in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   351
          if not (member (op =) ctr_args y_head) then
58303
a0fe6d8c8ba2 fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
blanchet
parents: 58302
diff changeset
   352
            subst_comb t
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   353
          else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   354
            (case try_nested_rec bound_Ts y_head t of
58303
a0fe6d8c8ba2 fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
blanchet
parents: 58302
diff changeset
   355
              SOME t' => subst_comb t'
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   356
            | NONE =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   357
              let val (g, g_args) = strip_comb g' in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   358
                (case try (get_ctr_pos o fst o dest_Free) g of
58303
a0fe6d8c8ba2 fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
blanchet
parents: 58302
diff changeset
   359
                  SOME ~1 => subst_comb t
57549
7a2fbd8c1d98 catch "not found" case
panny
parents: 57527
diff changeset
   360
                | SOME ctr_pos =>
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   361
                  (length g_args >= ctr_pos orelse too_few_args_in_rec_call ctxt [] t;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   362
                   (case AList.lookup (op =) mutual_calls y of
58303
a0fe6d8c8ba2 fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
blanchet
parents: 58302
diff changeset
   363
                     SOME y' => list_comb (y', map (subst bound_Ts) g_args)
a0fe6d8c8ba2 fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
blanchet
parents: 58302
diff changeset
   364
                   | NONE => subst_comb t))
a0fe6d8c8ba2 fixed situation in 'primrec' when recursive calls are apparently nested, e.g. 'f (f x y) y', with the recursion in 'y'
blanchet
parents: 58302
diff changeset
   365
                | NONE => subst_comb t)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   366
              end)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   367
        end
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   368
      | subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
73977
2d8a0f8e30ec correctly translate constructor argument in 'primrec'
blanchet
parents: 71214
diff changeset
   369
      | subst bound_Ts t = try_nested_rec bound_Ts (head_of t) t |> the_default t;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   370
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   371
    fun subst' t =
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   372
      if has_call t then rec_call_not_apply_to_ctr_arg ctxt [] t
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   373
      else try_nested_rec [] (head_of t) t |> the_default t;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   374
  in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   375
    subst' o subst []
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   376
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   377
58302
blanchet
parents: 58301
diff changeset
   378
fun build_rec_arg ctxt (funs_data : eqn_data list list) has_call (ctr_spec : rec_ctr_spec)
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54851
diff changeset
   379
    (eqn_data_opt : eqn_data option) =
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54851
diff changeset
   380
  (case eqn_data_opt of
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   381
    NONE => undef_const
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   382
  | SOME {ctr_args, left_args, right_args, rhs_term = t, ...} =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   383
    let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   384
      val calls = #calls ctr_spec;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   385
      val n_args = fold (Integer.add o (fn Mutual_Rec _ => 2 | _ => 1)) calls 0;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   386
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   387
      val no_calls' = tag_list 0 calls
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   388
        |> map_filter (try (apsnd (fn No_Rec p => p | Mutual_Rec (p, _) => p)));
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   389
      val mutual_calls' = tag_list 0 calls
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   390
        |> map_filter (try (apsnd (fn Mutual_Rec (_, p) => p)));
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   391
      val nested_calls' = tag_list 0 calls
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   392
        |> map_filter (try (apsnd (fn Nested_Rec p => p)));
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   393
54851
48a24d371ebb prevent ambiguity when mutual recursion maps a datatype to itself, which yielded wrong definitions in some cases (e.g. nat)
panny
parents: 54272
diff changeset
   394
      fun ensure_unique frees t =
48a24d371ebb prevent ambiguity when mutual recursion maps a datatype to itself, which yielded wrong definitions in some cases (e.g. nat)
panny
parents: 54272
diff changeset
   395
        if member (op =) frees t then Free (the_single (Term.variant_frees t [dest_Free t])) else t;
48a24d371ebb prevent ambiguity when mutual recursion maps a datatype to itself, which yielded wrong definitions in some cases (e.g. nat)
panny
parents: 54272
diff changeset
   396
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   397
      val args = replicate n_args ("", dummyT)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   398
        |> Term.rename_wrt_term t
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   399
        |> map Free
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   400
        |> fold (fn (ctr_arg_idx, (arg_idx, _)) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   401
            nth_map arg_idx (K (nth ctr_args ctr_arg_idx)))
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   402
          no_calls'
54851
48a24d371ebb prevent ambiguity when mutual recursion maps a datatype to itself, which yielded wrong definitions in some cases (e.g. nat)
panny
parents: 54272
diff changeset
   403
        |> fold (fn (ctr_arg_idx, (arg_idx, T)) => fn xs =>
56651
fc105315822a localize new size function generation code
blanchet
parents: 56638
diff changeset
   404
            nth_map arg_idx (K (ensure_unique xs
fc105315822a localize new size function generation code
blanchet
parents: 56638
diff changeset
   405
              (retype_const_or_free T (nth ctr_args ctr_arg_idx)))) xs)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   406
          mutual_calls'
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   407
        |> fold (fn (ctr_arg_idx, (arg_idx, T)) =>
56651
fc105315822a localize new size function generation code
blanchet
parents: 56638
diff changeset
   408
            nth_map arg_idx (K (retype_const_or_free T (nth ctr_args ctr_arg_idx))))
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   409
          nested_calls';
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   410
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   411
      val fun_name_ctr_pos_list =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   412
        map (fn (x :: _) => (#fun_name x, length (#left_args x))) funs_data;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   413
      val get_ctr_pos = try (the o AList.lookup (op =) fun_name_ctr_pos_list) #> the_default ~1;
57527
1b07ca054327 add helper function map_prod
desharna
parents: 57399
diff changeset
   414
      val mutual_calls = map (map_prod (nth ctr_args) (nth args o fst)) mutual_calls';
1b07ca054327 add helper function map_prod
desharna
parents: 57399
diff changeset
   415
      val nested_calls = map (map_prod (nth ctr_args) (nth args o fst)) nested_calls';
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   416
    in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   417
      t
58302
blanchet
parents: 58301
diff changeset
   418
      |> subst_rec_calls ctxt get_ctr_pos has_call ctr_args mutual_calls nested_calls
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   419
      |> fold_rev lambda (args @ left_args @ right_args)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   420
    end);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   421
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   422
fun build_defs ctxt nonexhaustives bs mxs (funs_data : eqn_data list list)
56121
52e8f110fec3 print warning if some constructors are missing;
panny
parents: 55869
diff changeset
   423
    (rec_specs : rec_spec list) has_call =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   424
  let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   425
    val n_funs = length funs_data;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   426
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   427
    val ctr_spec_eqn_data_list' =
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   428
      maps (fn ((xs, ys), z) =>
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   429
        let
59595
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59352
diff changeset
   430
          val zs = replicate (length xs) z;
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59352
diff changeset
   431
          val (b, c) = finds (fn ((x, _), y) => #ctr x = #ctr y) (xs ~~ zs) ys;
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   432
          val _ = null c orelse excess_equations ctxt (map #rhs_term c);
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   433
        in b end) (map #ctr_specs (take n_funs rec_specs) ~~ funs_data ~~ nonexhaustives);
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   434
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   435
    val (_ : unit list) = ctr_spec_eqn_data_list' |> map (fn (({ctr, ...}, nonexhaustive), x) =>
59595
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59352
diff changeset
   436
      if length x > 1 then
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   437
        multiple_equations_for_ctr ctxt (map #user_eqn x)
59595
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59352
diff changeset
   438
      else if length x = 1 orelse nonexhaustive orelse not (Context_Position.is_visible ctxt) then
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59352
diff changeset
   439
        ()
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59352
diff changeset
   440
      else
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   441
        no_equation_for_ctr_warning ctxt [] ctr);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   442
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   443
    val ctr_spec_eqn_data_list =
59283
5ca195783da8 generate [code] only with 'code' plugin enabled
blanchet
parents: 59281
diff changeset
   444
      map (apfst fst) ctr_spec_eqn_data_list' @
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   445
      (drop n_funs rec_specs |> maps #ctr_specs |> map (rpair []));
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   446
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   447
    val recs = take n_funs rec_specs |> map #recx;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   448
    val rec_args = ctr_spec_eqn_data_list
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58996
diff changeset
   449
      |> sort (op < o apply2 (#offset o fst) |> make_ord)
58302
blanchet
parents: 58301
diff changeset
   450
      |> map (uncurry (build_rec_arg ctxt funs_data has_call) o apsnd (try the_single));
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   451
    val ctr_poss = map (fn x =>
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58996
diff changeset
   452
      if length (distinct (op = o apply2 (length o #left_args)) x) <> 1 then
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   453
        inconstant_pattern_pos_for_fun ctxt [] (#fun_name (hd x))
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   454
      else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   455
        hd x |> #left_args |> length) funs_data;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   456
  in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   457
    (recs, ctr_poss)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   458
    |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos)
58302
blanchet
parents: 58301
diff changeset
   459
    |> Syntax.check_terms ctxt
61760
1647bb489522 tuned whitespace
blanchet
parents: 61271
diff changeset
   460
    |> @{map 3} (fn b => fn mx => fn t =>
1647bb489522 tuned whitespace
blanchet
parents: 61271
diff changeset
   461
        ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t)))
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   462
      bs mxs
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   463
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   464
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   465
fun find_rec_calls has_call ({ctr, ctr_args, rhs_term, ...} : eqn_data) =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   466
  let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   467
    fun find bound_Ts (Abs (_, T, b)) ctr_arg = find (T :: bound_Ts) b ctr_arg
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   468
      | find bound_Ts (t as _ $ _) ctr_arg =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   469
        let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   470
          val typof = curry fastype_of1 bound_Ts;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   471
          val (f', args') = strip_comb t;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   472
          val n = find_index (equal ctr_arg o head_of) args';
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   473
        in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   474
          if n < 0 then
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   475
            find bound_Ts f' ctr_arg @ maps (fn x => find bound_Ts x ctr_arg) args'
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   476
          else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   477
            let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   478
              val (f, args as arg :: _) = chop n args' |>> curry list_comb f'
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   479
              val (arg_head, arg_args) = Term.strip_comb arg;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   480
            in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   481
              if has_call f then
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   482
                mk_partial_compN (length arg_args) (typof arg_head) f ::
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   483
                maps (fn x => find bound_Ts x ctr_arg) args
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   484
              else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   485
                find bound_Ts f ctr_arg @ maps (fn x => find bound_Ts x ctr_arg) args
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   486
            end
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   487
        end
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   488
      | find _ _ _ = [];
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   489
  in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   490
    map (find [] rhs_term) ctr_args
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   491
    |> (fn [] => NONE | callss => SOME (ctr, callss))
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   492
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   493
62326
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
   494
fun mk_primrec_tac ctxt num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
   495
    fp_nesting_pred_maps fun_defs recx =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   496
  unfold_thms_tac ctxt fun_defs THEN
60728
26ffdb966759 {r,e,d,f}tac with proper context in BNF
traytel
parents: 60007
diff changeset
   497
  HEADGOAL (rtac ctxt (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
66290
88714f2e40e8 strengthened tactic
blanchet
parents: 66288
diff changeset
   498
  unfold_thms_tac ctxt (nested_simps ctxt @ fp_nesting_map_ident0s @ fp_nesting_map_comps @
88714f2e40e8 strengthened tactic
blanchet
parents: 66288
diff changeset
   499
    fp_nesting_pred_maps) THEN
88714f2e40e8 strengthened tactic
blanchet
parents: 66288
diff changeset
   500
  REPEAT_DETERM (HEADGOAL (rtac ctxt refl) ORELSE
88714f2e40e8 strengthened tactic
blanchet
parents: 66288
diff changeset
   501
    special_endgame_tac ctxt fp_nesting_map_ident0s fp_nesting_map_comps fp_nesting_pred_maps);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   502
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   503
fun prepare_primrec plugins nonexhaustives transfers fixes specs lthy0 =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   504
  let
55535
10194808430d name derivations in 'primrec' for code extraction from proof terms
blanchet
parents: 55530
diff changeset
   505
    val thy = Proof_Context.theory_of lthy0;
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54256
diff changeset
   506
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   507
    val (bs, mxs) = map_split (apfst fst) fixes;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   508
    val fun_names = map Binding.name_of bs;
62497
5b5b704f4811 respect qualification when noting theorems in prim(co)rec
traytel
parents: 62326
diff changeset
   509
    val qualifys = map (fold_rev (uncurry Binding.qualify o swap) o Binding.path_of) bs;
55535
10194808430d name derivations in 'primrec' for code extraction from proof terms
blanchet
parents: 55530
diff changeset
   510
    val eqns_data = map (dissect_eqn lthy0 fun_names) specs;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   511
    val funs_data = eqns_data
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58996
diff changeset
   512
      |> partition_eq (op = o apply2 #fun_name)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   513
      |> finds (fn (x, y) => x = #fun_name (hd y)) fun_names |> fst
55527
blanchet
parents: 55482
diff changeset
   514
      |> map (fn (x, y) => the_single y
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   515
        handle List.Empty => missing_equations_for_fun x);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   516
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55576
diff changeset
   517
    val frees = map (fst #>> Binding.name_of #> Free) fixes;
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55576
diff changeset
   518
    val has_call = exists_subterm (member (op =) frees);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   519
    val arg_Ts = map (#rec_type o hd) funs_data;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   520
    val res_Ts = map (#res_type o hd) funs_data;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   521
    val callssss = funs_data
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58996
diff changeset
   522
      |> map (partition_eq (op = o apply2 #ctr))
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   523
      |> map (maps (map_filter (find_rec_calls has_call)));
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   524
55528
c367f4f3e5d4 have 'primrec_new' fall back on old 'primrec' when given old-style datatypes
blanchet
parents: 55527
diff changeset
   525
    fun is_only_old_datatype (Type (s, _)) =
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 57633
diff changeset
   526
        is_some (Old_Datatype_Data.get_info thy s) andalso not (is_new_datatype lthy0 s)
55528
c367f4f3e5d4 have 'primrec_new' fall back on old 'primrec' when given old-style datatypes
blanchet
parents: 55527
diff changeset
   527
      | is_only_old_datatype _ = false;
c367f4f3e5d4 have 'primrec_new' fall back on old 'primrec' when given old-style datatypes
blanchet
parents: 55527
diff changeset
   528
c367f4f3e5d4 have 'primrec_new' fall back on old 'primrec' when given old-style datatypes
blanchet
parents: 55527
diff changeset
   529
    val _ = if exists is_only_old_datatype arg_Ts then raise OLD_PRIMREC () else ();
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   530
    val _ = List.app (uncurry (check_top_sort lthy0)) (bs ~~ res_Ts);
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54256
diff changeset
   531
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   532
    val ((n2m, rec_specs, _, common_induct, inducts, induct_attrs, Ts), lthy) =
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55576
diff changeset
   533
      rec_specs_of bs arg_Ts res_Ts frees callssss lthy0;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   534
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   535
    val actual_nn = length funs_data;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   536
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   537
    val ctrs = maps (map #ctr o #ctr_specs) rec_specs;
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   538
    val _ = List.app (fn {ctr, user_eqn, ...} =>
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   539
        ignore (member (op =) ctrs ctr orelse not_constructor_in_pattern lthy0 [user_eqn] ctr))
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   540
      eqns_data;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   541
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   542
    val defs = build_defs lthy nonexhaustives bs mxs funs_data rec_specs has_call;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   543
62326
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
   544
    fun prove def_thms ({ctr_specs, fp_nesting_map_ident0s, fp_nesting_map_comps,
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
   545
        fp_nesting_pred_maps, ...} : rec_spec) (fun_data : eqn_data list) lthy' =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   546
      let
55535
10194808430d name derivations in 'primrec' for code extraction from proof terms
blanchet
parents: 55530
diff changeset
   547
        val js =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58996
diff changeset
   548
          find_indices (op = o apply2 (fn {fun_name, ctr, ...} => (fun_name, ctr)))
55535
10194808430d name derivations in 'primrec' for code extraction from proof terms
blanchet
parents: 55530
diff changeset
   549
            fun_data eqns_data;
10194808430d name derivations in 'primrec' for code extraction from proof terms
blanchet
parents: 55530
diff changeset
   550
60004
e27e7be1f2f6 have 'primrec' return definitions
blanchet
parents: 60003
diff changeset
   551
        val simps = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   552
          |> fst
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   553
          |> map_filter (try (fn (x, [y]) =>
59283
5ca195783da8 generate [code] only with 'code' plugin enabled
blanchet
parents: 59281
diff changeset
   554
            (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
5ca195783da8 generate [code] only with 'code' plugin enabled
blanchet
parents: 59281
diff changeset
   555
          |> map (fn (user_eqn, num_extra_args, rec_thm) =>
61271
0478ba10152a more canonical context threading
traytel
parents: 60728
diff changeset
   556
              Goal.prove_sorry lthy' [] [] user_eqn
0478ba10152a more canonical context threading
traytel
parents: 60728
diff changeset
   557
                (fn {context = ctxt, prems = _} =>
0478ba10152a more canonical context threading
traytel
parents: 60728
diff changeset
   558
                  mk_primrec_tac ctxt num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
62326
3cf7a067599c allow predicator instead of map function in 'primrec'
blanchet
parents: 62323
diff changeset
   559
                    fp_nesting_pred_maps def_thms rec_thm)
70494
41108e3e9ca5 formal position for PThm nodes;
wenzelm
parents: 69992
diff changeset
   560
              |> Thm.close_derivation \<^here>);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   561
      in
60004
e27e7be1f2f6 have 'primrec' return definitions
blanchet
parents: 60003
diff changeset
   562
        ((js, simps), lthy')
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   563
      end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   564
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   565
    val notes =
55482
61ffc2339a8c removed assumption in 'primrec_new' that a given constructor can only occur once
blanchet
parents: 55480
diff changeset
   566
      (if n2m then
62497
5b5b704f4811 respect qualification when noting theorems in prim(co)rec
traytel
parents: 62326
diff changeset
   567
         @{map 3} (fn name => fn qualify => fn thm => (name, qualify, inductN, [thm], induct_attrs))
5b5b704f4811 respect qualification when noting theorems in prim(co)rec
traytel
parents: 62326
diff changeset
   568
         fun_names qualifys (take actual_nn inducts)
55482
61ffc2339a8c removed assumption in 'primrec_new' that a given constructor can only occur once
blanchet
parents: 55480
diff changeset
   569
       else
61ffc2339a8c removed assumption in 'primrec_new' that a given constructor can only occur once
blanchet
parents: 55480
diff changeset
   570
         [])
62497
5b5b704f4811 respect qualification when noting theorems in prim(co)rec
traytel
parents: 62326
diff changeset
   571
      |> map (fn (prefix, qualify, thmN, thms, attrs) =>
5b5b704f4811 respect qualification when noting theorems in prim(co)rec
traytel
parents: 62326
diff changeset
   572
        ((qualify (Binding.qualify true prefix (Binding.name thmN)), attrs), [(thms, [])]));
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   573
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   574
    val common_name = mk_common_name fun_names;
62497
5b5b704f4811 respect qualification when noting theorems in prim(co)rec
traytel
parents: 62326
diff changeset
   575
    val common_qualify = fold_rev I qualifys;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   576
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   577
    val common_notes =
56857
aa2de99be748 note correct induction schemes in 'primrec' (for N2M)
blanchet
parents: 56651
diff changeset
   578
      (if n2m then [(inductN, [common_induct], [])] else [])
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   579
      |> map (fn (thmN, thms, attrs) =>
62497
5b5b704f4811 respect qualification when noting theorems in prim(co)rec
traytel
parents: 62326
diff changeset
   580
        ((common_qualify (Binding.qualify true common_name (Binding.name thmN)), attrs),
5b5b704f4811 respect qualification when noting theorems in prim(co)rec
traytel
parents: 62326
diff changeset
   581
          [(thms, [])]));
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   582
  in
69992
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69593
diff changeset
   583
    (((fun_names, qualifys, arg_Ts, defs),
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   584
      fn lthy => fn defs =>
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   585
        let
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   586
          val def_thms = map (snd o snd) defs;
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   587
          val ts = map fst defs;
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   588
          val phi = Local_Theory.target_morphism lthy;
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   589
          val fp_rec_sugar =
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   590
            {transfers = transfers, fun_names = fun_names, funs = map (Morphism.term phi) ts,
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   591
             fun_defs = Morphism.fact phi def_thms, fpTs = take actual_nn Ts};
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   592
        in
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   593
          map_prod split_list (interpret_lfp_rec_sugar plugins fp_rec_sugar)
59673
blanchet
parents: 59595
diff changeset
   594
            (@{fold_map 2} (prove (map (snd o snd) defs)) (take actual_nn rec_specs) funs_data lthy)
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   595
        end),
55535
10194808430d name derivations in 'primrec' for code extraction from proof terms
blanchet
parents: 55530
diff changeset
   596
      lthy |> Local_Theory.notes (notes @ common_notes) |> snd)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   597
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   598
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
   599
fun primrec_simple0 int plugins nonexhaustive transfer fixes ts lthy =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   600
  let
64705
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   601
    val _ = check_duplicate_const_names (map (fst o fst) fixes);
7596b0736ab9 more uniform errors in '(prim)(co)rec(ursive)' variants
blanchet
parents: 64674
diff changeset
   602
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   603
    val actual_nn = length fixes;
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   604
59283
5ca195783da8 generate [code] only with 'code' plugin enabled
blanchet
parents: 59281
diff changeset
   605
    val nonexhaustives = replicate actual_nn nonexhaustive;
5ca195783da8 generate [code] only with 'code' plugin enabled
blanchet
parents: 59281
diff changeset
   606
    val transfers = replicate actual_nn transfer;
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   607
69992
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69593
diff changeset
   608
    val (((names, qualifys, arg_Ts, defs), prove), lthy') =
59595
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59352
diff changeset
   609
      prepare_primrec plugins nonexhaustives transfers fixes ts lthy;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   610
  in
55527
blanchet
parents: 55482
diff changeset
   611
    lthy'
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   612
    |> fold_map Local_Theory.define defs
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
   613
    |> tap (uncurry (print_def_consts int))
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   614
    |-> (fn defs => fn lthy =>
69992
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69593
diff changeset
   615
      let
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69593
diff changeset
   616
        val ((jss, simpss), lthy) = prove lthy defs;
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69593
diff changeset
   617
        val res =
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69593
diff changeset
   618
          {prefix = (names, qualifys),
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69593
diff changeset
   619
           types = map (#1 o dest_Type) arg_Ts,
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69593
diff changeset
   620
           result = (map fst defs, map (snd o snd) defs, (jss, simpss))};
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69593
diff changeset
   621
      in (res, lthy) end)
59595
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59352
diff changeset
   622
  end;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   623
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
   624
fun primrec_simple int fixes ts lthy =
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
   625
  primrec_simple0 int Plugin_Name.default_filter false false fixes ts lthy
69992
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69593
diff changeset
   626
    |>> (fn {prefix, result, ...} => (prefix, result))
58220
a2afad27a0b1 wildcards in plugins
blanchet
parents: 58211
diff changeset
   627
  handle OLD_PRIMREC () =>
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
   628
    Old_Primrec.primrec_simple int fixes ts lthy
69992
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69593
diff changeset
   629
    |>> (fn {prefix, result = (ts, thms), ...} =>
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69593
diff changeset
   630
          (map_split (rpair I) [prefix], (ts, [], ([], [thms]))))
56121
52e8f110fec3 print warning if some constructors are missing;
panny
parents: 55869
diff changeset
   631
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
   632
fun gen_primrec old_primrec prep_spec int opts raw_fixes raw_specs lthy =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   633
  let
59283
5ca195783da8 generate [code] only with 'code' plugin enabled
blanchet
parents: 59281
diff changeset
   634
    val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)
5ca195783da8 generate [code] only with 'code' plugin enabled
blanchet
parents: 59281
diff changeset
   635
      |> the_default Plugin_Name.default_filter;
5ca195783da8 generate [code] only with 'code' plugin enabled
blanchet
parents: 59281
diff changeset
   636
    val nonexhaustive = exists (can (fn Nonexhaustive_Option => ())) opts;
5ca195783da8 generate [code] only with 'code' plugin enabled
blanchet
parents: 59281
diff changeset
   637
    val transfer = exists (can (fn Transfer_Option => ())) opts;
5ca195783da8 generate [code] only with 'code' plugin enabled
blanchet
parents: 59281
diff changeset
   638
56945
blanchet
parents: 56857
diff changeset
   639
    val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
71214
5727bcc3c47c proper spec_rule name via naming/binding/Morphism.binding;
wenzelm
parents: 71179
diff changeset
   640
    val spec_name = Binding.conglomerate (map (#1 o #1) fixes);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   641
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   642
    val mk_notes =
62497
5b5b704f4811 respect qualification when noting theorems in prim(co)rec
traytel
parents: 62326
diff changeset
   643
      flat oooo @{map 4} (fn js => fn prefix => fn qualify => fn thms =>
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   644
        let
55535
10194808430d name derivations in 'primrec' for code extraction from proof terms
blanchet
parents: 55530
diff changeset
   645
          val (bs, attrss) = map_split (fst o nth specs) js;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   646
          val notes =
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58389
diff changeset
   647
            @{map 3} (fn b => fn attrs => fn thm =>
66251
cd935b7cb3fb proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents: 64705
diff changeset
   648
                ((Binding.qualify false prefix b, nitpicksimp_simp_attrs @ attrs),
55464
56fa33537869 have 'Ctr_Sugar' register its 'Spec_Rules'
blanchet
parents: 55067
diff changeset
   649
                 [([thm], [])]))
56fa33537869 have 'Ctr_Sugar' register its 'Spec_Rules'
blanchet
parents: 55067
diff changeset
   650
              bs attrss thms;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   651
        in
62497
5b5b704f4811 respect qualification when noting theorems in prim(co)rec
traytel
parents: 62326
diff changeset
   652
          ((qualify (Binding.qualify true prefix (Binding.name simpsN)), []), [(thms, [])]) :: notes
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   653
        end);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   654
  in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   655
    lthy
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
   656
    |> primrec_simple0 int plugins nonexhaustive transfer fixes (map snd specs)
69992
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69593
diff changeset
   657
    |-> (fn {prefix = (names, qualifys), types, result = (ts, defs, (jss, simpss))} =>
71179
592e2afdd50c more informative spec rules: optional name;
wenzelm
parents: 70494
diff changeset
   658
      Spec_Rules.add spec_name (Spec_Rules.equational_primrec types) ts (flat simpss)
62497
5b5b704f4811 respect qualification when noting theorems in prim(co)rec
traytel
parents: 62326
diff changeset
   659
      #> Local_Theory.notes (mk_notes jss names qualifys simpss)
66251
cd935b7cb3fb proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents: 64705
diff changeset
   660
      #-> (fn notes =>
cd935b7cb3fb proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents: 64705
diff changeset
   661
        plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (maps snd notes))
cd935b7cb3fb proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents: 64705
diff changeset
   662
        #> pair (ts, defs, map_filter (fn ("", _) => NONE | (_, thms) => SOME thms) notes)))
55528
c367f4f3e5d4 have 'primrec_new' fall back on old 'primrec' when given old-style datatypes
blanchet
parents: 55527
diff changeset
   663
  end
60004
e27e7be1f2f6 have 'primrec' return definitions
blanchet
parents: 60003
diff changeset
   664
  handle OLD_PRIMREC () =>
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
   665
    old_primrec int raw_fixes raw_specs lthy
69992
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69593
diff changeset
   666
    |>> (fn {result = (ts, thms), ...} => (ts, [], [thms]));
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   667
63719
9084d77f1119 tuned signature
traytel
parents: 63239
diff changeset
   668
val primrec = gen_primrec Old_Primrec.primrec Specification.check_multi_specs;
63064
2f18172214c8 support 'assumes' in specifications, e.g. 'definition', 'inductive';
wenzelm
parents: 62497
diff changeset
   669
val primrec_cmd = gen_primrec Old_Primrec.primrec_cmd Specification.read_multi_specs;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   670
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
   671
fun primrec_global int opts fixes specs =
55535
10194808430d name derivations in 'primrec' for code extraction from proof terms
blanchet
parents: 55530
diff changeset
   672
  Named_Target.theory_init
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
   673
  #> primrec int opts fixes specs
55535
10194808430d name derivations in 'primrec' for code extraction from proof terms
blanchet
parents: 55530
diff changeset
   674
  ##> Local_Theory.exit_global;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   675
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
   676
fun primrec_overloaded int opts ops fixes specs =
55535
10194808430d name derivations in 'primrec' for code extraction from proof terms
blanchet
parents: 55530
diff changeset
   677
  Overloading.overloading ops
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
   678
  #> primrec int opts fixes specs
55535
10194808430d name derivations in 'primrec' for code extraction from proof terms
blanchet
parents: 55530
diff changeset
   679
  ##> Local_Theory.exit_global;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   680
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   681
val rec_option_parser = Parse.group (K "option")
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   682
  (Plugin_Name.parse_filter >> Plugins_Option
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   683
   || Parse.reserved "nonexhaustive" >> K Nonexhaustive_Option
59279
blanchet
parents: 59275
diff changeset
   684
   || Parse.reserved "transfer" >> K Transfer_Option);
56121
52e8f110fec3 print warning if some constructors are missing;
panny
parents: 55869
diff changeset
   685
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67522
diff changeset
   686
val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>primrec\<close>
55529
51998cb9d6b8 tuning: moved code where it belongs
blanchet
parents: 55528
diff changeset
   687
  "define primitive recursive functions"
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67522
diff changeset
   688
  ((Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.list1 rec_option_parser)
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 67522
diff changeset
   689
      --| \<^keyword>\<open>)\<close>) []) -- Parse_Spec.specification
64674
ef0a5fd30f3b print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents: 63719
diff changeset
   690
    >> (fn (opts, (fixes, specs)) => snd o primrec_cmd true opts fixes specs));
55529
51998cb9d6b8 tuning: moved code where it belongs
blanchet
parents: 55528
diff changeset
   691
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
diff changeset
   692
end;