src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
author blanchet
Thu, 10 Mar 2016 19:15:06 +0100
changeset 62583 8c7301325f9f
parent 62582 969480bdef55
child 62686 6e8924f957f6
permissions -rw-r--r--
don't throw an exception when trying to print an error message
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_gfp_rec_sugar.ML
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     2
    Author:     Lorenz Panny, TU Muenchen
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     4
    Copyright   2013
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     5
55538
blanchet
parents: 55529
diff changeset
     6
Corecursor sugar ("primcorec" and "primcorecursive").
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     7
*)
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     8
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
     9
signature BNF_GFP_REC_SUGAR =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    10
sig
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
    11
  datatype corec_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
    Sequential_Option |
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
    14
    Exhaustive_Option |
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
    15
    Transfer_Option
54899
7a01387c47d5 added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents: 54883
diff changeset
    16
58223
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    17
  datatype corec_call =
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    18
    Dummy_No_Corec of int |
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    19
    No_Corec of int |
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    20
    Mutual_Corec of int * int * int |
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    21
    Nested_Corec of int
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    22
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    23
  type corec_ctr_spec =
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    24
    {ctr: term,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    25
     disc: term,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    26
     sels: term list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    27
     pred: int option,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    28
     calls: corec_call list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    29
     discI: thm,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    30
     sel_thms: thm list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    31
     distinct_discss: thm list list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    32
     collapse: thm,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    33
     corec_thm: thm,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    34
     corec_disc: thm,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    35
     corec_sels: thm list}
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    36
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    37
  type corec_spec =
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
    38
    {T: typ,
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
    39
     corec: term,
58223
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    40
     exhaust_discs: thm list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    41
     sel_defs: thm list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    42
     fp_nesting_maps: thm list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    43
     fp_nesting_map_ident0s: thm list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    44
     fp_nesting_map_comps: thm list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    45
     ctr_specs: corec_ctr_spec list}
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    46
60704
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
    47
  val abstract_over_list: term list -> term -> term
59945
cfbaee8cdf1d export ML function
blanchet
parents: 59936
diff changeset
    48
  val abs_tuple_balanced: term list -> term -> term
cfbaee8cdf1d export ML function
blanchet
parents: 59936
diff changeset
    49
60704
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
    50
  val mk_conjs: term list -> term
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
    51
  val mk_disjs: term list -> term
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
    52
  val mk_dnf: term list list -> term
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
    53
  val conjuncts_s: term -> term list
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
    54
  val s_not: term -> term
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
    55
  val s_not_conj: term list -> term list
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
    56
  val s_conjs: term list -> term
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
    57
  val s_disjs: term list -> term
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
    58
  val s_dnf: term list list -> term list
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
    59
59674
198eaf28a8b8 export more functions (for future 'corec')
blanchet
parents: 59673
diff changeset
    60
  val fold_rev_let_if_case: Proof.context -> (term list -> term -> 'a -> 'a) -> typ list ->
198eaf28a8b8 export more functions (for future 'corec')
blanchet
parents: 59673
diff changeset
    61
    term -> 'a -> 'a
198eaf28a8b8 export more functions (for future 'corec')
blanchet
parents: 59673
diff changeset
    62
  val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->
62318
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
    63
    (typ list -> term -> unit) -> (typ list -> term -> term) -> typ list -> term -> term
59674
198eaf28a8b8 export more functions (for future 'corec')
blanchet
parents: 59673
diff changeset
    64
  val massage_nested_corec_call: Proof.context -> (term -> bool) ->
59989
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
    65
    (typ list -> typ -> typ -> term -> term) -> (typ list -> typ -> typ -> term -> term) ->
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
    66
    typ list -> typ -> typ -> term -> term
60683
d34e1b0b331a tuned ML signature
blanchet
parents: 60362
diff changeset
    67
  val expand_to_ctr_term: Proof.context -> typ -> term -> term
59674
198eaf28a8b8 export more functions (for future 'corec')
blanchet
parents: 59673
diff changeset
    68
  val massage_corec_code_rhs: Proof.context -> (typ list -> term -> term list -> term) ->
198eaf28a8b8 export more functions (for future 'corec')
blanchet
parents: 59673
diff changeset
    69
    typ list -> term -> term
198eaf28a8b8 export more functions (for future 'corec')
blanchet
parents: 59673
diff changeset
    70
  val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) ->
198eaf28a8b8 export more functions (for future 'corec')
blanchet
parents: 59673
diff changeset
    71
    typ list -> term -> 'a -> 'a
198eaf28a8b8 export more functions (for future 'corec')
blanchet
parents: 59673
diff changeset
    72
  val case_thms_of_term: Proof.context -> term ->
198eaf28a8b8 export more functions (for future 'corec')
blanchet
parents: 59673
diff changeset
    73
    thm list * thm list * thm list * thm list * thm list
198eaf28a8b8 export more functions (for future 'corec')
blanchet
parents: 59673
diff changeset
    74
  val map_thms_of_type: Proof.context -> typ -> thm list
198eaf28a8b8 export more functions (for future 'corec')
blanchet
parents: 59673
diff changeset
    75
58223
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    76
  val corec_specs_of: binding list -> typ list -> typ list -> term list ->
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    77
    (term * term list list) list list -> local_theory ->
58283
71d74e641538 preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents: 58223
diff changeset
    78
    corec_spec list * typ list * thm * thm * thm list * thm list * (Token.src list * Token.src list)
71d74e641538 preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents: 58223
diff changeset
    79
    * bool * local_theory
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
    80
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
    81
  val gfp_rec_sugar_interpretation: string ->
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
    82
    (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
    83
61301
484f7878ede4 export '_cmd' functions
blanchet
parents: 61271
diff changeset
    84
  val primcorec_ursive_cmd: bool -> corec_option list ->
484f7878ede4 export '_cmd' functions
blanchet
parents: 61271
diff changeset
    85
    (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
484f7878ede4 export '_cmd' functions
blanchet
parents: 61271
diff changeset
    86
    Proof.context ->
484f7878ede4 export '_cmd' functions
blanchet
parents: 61271
diff changeset
    87
    (term * 'a list) list list * (thm list list -> local_theory -> local_theory) * local_theory
60003
ba8fa0c38d66 renamed ML funs
blanchet
parents: 60001
diff changeset
    88
  val primcorecursive_cmd: corec_option list ->
53831
80423b9080cf support "of" syntax to disambiguate selector equations
panny
parents: 53830
diff changeset
    89
    (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
80423b9080cf support "of" syntax to disambiguate selector equations
panny
parents: 53830
diff changeset
    90
    Proof.context -> Proof.state
60003
ba8fa0c38d66 renamed ML funs
blanchet
parents: 60001
diff changeset
    91
  val primcorec_cmd: corec_option list ->
53831
80423b9080cf support "of" syntax to disambiguate selector equations
panny
parents: 53830
diff changeset
    92
    (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
80423b9080cf support "of" syntax to disambiguate selector equations
panny
parents: 53830
diff changeset
    93
    local_theory -> local_theory
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    94
end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    95
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    96
structure BNF_GFP_Rec_Sugar : BNF_GFP_REC_SUGAR =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    97
struct
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    98
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
    99
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: 54243
diff changeset
   100
open Ctr_Sugar
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   101
open BNF_Util
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   102
open BNF_Def
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   103
open BNF_FP_Util
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   104
open BNF_FP_Def_Sugar
54243
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54239
diff changeset
   105
open BNF_FP_N2M_Sugar
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   106
open BNF_FP_Rec_Sugar_Util
59276
blanchet
parents: 59275
diff changeset
   107
open BNF_FP_Rec_Sugar_Transfer
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   108
open BNF_GFP_Rec_Sugar_Tactics
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   109
58387
blanchet
parents: 58335
diff changeset
   110
val codeN = "code";
blanchet
parents: 58335
diff changeset
   111
val ctrN = "ctr";
blanchet
parents: 58335
diff changeset
   112
val discN = "disc";
blanchet
parents: 58335
diff changeset
   113
val disc_iffN = "disc_iff";
blanchet
parents: 58335
diff changeset
   114
val excludeN = "exclude";
blanchet
parents: 58335
diff changeset
   115
val selN = "sel";
53791
0ddf045113c9 tuned code
blanchet
parents: 53753
diff changeset
   116
54145
297d1c603999 make sure that registered code equations are actually equations
blanchet
parents: 54133
diff changeset
   117
val nitpicksimp_attrs = @{attributes [nitpick_simp]};
53794
af7d1533a25b undid copy-paste
blanchet
parents: 53793
diff changeset
   118
val simp_attrs = @{attributes [simp]};
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   119
59599
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
   120
fun extra_variable ctxt ts var =
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
   121
  error_at ctxt ts ("Extra variable " ^ quote (Syntax.string_of_term ctxt var));
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   122
fun not_codatatype ctxt T =
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   123
  error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T);
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   124
fun ill_formed_corec_call ctxt t =
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   125
  error ("Ill-formed corecursive call " ^ quote (Syntax.string_of_term ctxt t));
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   126
fun invalid_map ctxt t =
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   127
  error_at ctxt [t] "Invalid map function";
59598
c9d304d6ae98 more 'primcorec' error handling
blanchet
parents: 59597
diff changeset
   128
fun nonprimitive_corec ctxt eqns =
c9d304d6ae98 more 'primcorec' error handling
blanchet
parents: 59597
diff changeset
   129
  error_at ctxt eqns "Nonprimitive corecursive specification";
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   130
fun unexpected_corec_call ctxt eqns t =
59596
c067eba942e7 no quick_and_dirty for goals that may fail + tuned messages
blanchet
parents: 59595
diff changeset
   131
  error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t));
62318
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   132
fun unsupported_case_around_corec_call ctxt eqns t =
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   133
  error_at ctxt eqns ("Unsupported corecursive call under case expression " ^
62583
8c7301325f9f don't throw an exception when trying to print an error message
blanchet
parents: 62582
diff changeset
   134
    quote (Syntax.string_of_term ctxt t) ^ " for datatype with no discriminators and selectors");
59597
70a68edcc79b helpful error message when 'auto' fails
blanchet
parents: 59596
diff changeset
   135
fun use_primcorecursive () =
59936
b8ffc3dc9e24 @{command_spec} is superseded by @{command_keyword};
wenzelm
parents: 59873
diff changeset
   136
  error ("\"auto\" failed (try " ^ quote (#1 @{command_keyword primcorecursive}) ^ " instead of " ^
b8ffc3dc9e24 @{command_spec} is superseded by @{command_keyword};
wenzelm
parents: 59873
diff changeset
   137
    quote (#1 @{command_keyword primcorec}) ^ ")");
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   138
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   139
datatype corec_option =
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   140
  Plugins_Option of Proof.context -> Plugin_Name.filter |
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   141
  Sequential_Option |
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   142
  Exhaustive_Option |
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   143
  Transfer_Option;
54591
c822230fd22b prevent exception when equations for a function are missing;
panny
parents: 54279
diff changeset
   144
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   145
datatype corec_call =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   146
  Dummy_No_Corec of int |
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   147
  No_Corec of int |
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   148
  Mutual_Corec of int * int * int |
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   149
  Nested_Corec of int;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   150
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   151
type basic_corec_ctr_spec =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   152
  {ctr: term,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   153
   disc: term,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   154
   sels: term list};
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   155
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   156
type corec_ctr_spec =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   157
  {ctr: term,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   158
   disc: term,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   159
   sels: term list,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   160
   pred: int option,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   161
   calls: corec_call list,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   162
   discI: thm,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   163
   sel_thms: thm list,
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   164
   distinct_discss: thm list list,
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   165
   collapse: thm,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   166
   corec_thm: thm,
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   167
   corec_disc: thm,
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   168
   corec_sels: thm list};
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   169
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   170
type corec_spec =
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   171
  {T: typ,
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   172
   corec: term,
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   173
   exhaust_discs: thm list,
56858
0c3d0bc98abe simplify selectors in code views
blanchet
parents: 56806
diff changeset
   174
   sel_defs: thm list,
57397
5004aca20821 tuned variable names
blanchet
parents: 57303
diff changeset
   175
   fp_nesting_maps: thm list,
57399
cfc19f0a6261 compile
blanchet
parents: 57397
diff changeset
   176
   fp_nesting_map_ident0s: thm list,
57397
5004aca20821 tuned variable names
blanchet
parents: 57303
diff changeset
   177
   fp_nesting_map_comps: thm list,
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   178
   ctr_specs: corec_ctr_spec list};
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   179
58223
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
   180
exception NO_MAP of term;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   181
60704
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   182
fun abstract_over_list rev_vs =
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   183
  let
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   184
    val vs = rev rev_vs;
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   185
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   186
    fun abs n (t $ u) = abs n t $ abs n u
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   187
      | abs n (Abs (s, T, t)) = Abs (s, T, abs (n + 1) t)
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   188
      | abs n t =
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   189
        let val j = find_index (curry (op =) t) vs in
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   190
          if j < 0 then t else Bound (n + j)
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   191
        end;
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   192
  in
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   193
    abs 0
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   194
  end;
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   195
59945
cfbaee8cdf1d export ML function
blanchet
parents: 59936
diff changeset
   196
val abs_tuple_balanced = HOLogic.tupled_lambda o mk_tuple_balanced;
cfbaee8cdf1d export ML function
blanchet
parents: 59936
diff changeset
   197
60704
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   198
fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) =
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   199
  Ts ---> T;
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   200
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 59044
diff changeset
   201
fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs);
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
   202
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   203
val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   204
val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   205
val mk_dnf = mk_disjs o map mk_conjs;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   206
55008
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
   207
val conjuncts_s = filter_out (curry (op aconv) @{const True}) o HOLogic.conjuncts;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   208
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   209
fun s_not @{const True} = @{const False}
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   210
  | s_not @{const False} = @{const True}
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   211
  | s_not (@{const Not} $ t) = t
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   212
  | s_not (@{const conj} $ t $ u) = @{const disj} $ s_not t $ s_not u
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   213
  | s_not (@{const disj} $ t $ u) = @{const conj} $ s_not t $ s_not u
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   214
  | s_not t = @{const Not} $ t;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   215
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   216
val s_not_conj = conjuncts_s o s_not o mk_conjs;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   217
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   218
fun propagate_unit_pos u cs = if member (op aconv) cs u then [@{const False}] else cs;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   219
fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   220
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   221
fun propagate_units css =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   222
  (case List.partition (can the_single) css of
58393
blanchet
parents: 58387
diff changeset
   223
    ([], _) => css
blanchet
parents: 58387
diff changeset
   224
  | ([u] :: uss, css') =>
blanchet
parents: 58387
diff changeset
   225
    [u] :: propagate_units (map (propagate_unit_neg (s_not u))
blanchet
parents: 58387
diff changeset
   226
      (map (propagate_unit_pos u) (uss @ css'))));
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   227
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   228
fun s_conjs cs =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   229
  if member (op aconv) cs @{const False} then @{const False}
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   230
  else mk_conjs (remove (op aconv) @{const True} cs);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   231
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   232
fun s_disjs ds =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   233
  if member (op aconv) ds @{const True} then @{const True}
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   234
  else mk_disjs (remove (op aconv) @{const False} ds);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   235
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   236
fun s_dnf css0 =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   237
  let val css = propagate_units css0 in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   238
    if null css then
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   239
      [@{const False}]
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   240
    else if exists null css then
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   241
      []
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   242
    else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   243
      map (fn c :: cs => (c, cs)) css
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   244
      |> AList.coalesce (op =)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   245
      |> map (fn (c, css) => c :: s_dnf css)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   246
      |> (fn [cs] => cs | css => [s_disjs (map s_conjs css)])
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   247
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   248
55341
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   249
fun fold_rev_let_if_case ctxt f bound_Ts =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   250
  let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   251
    val thy = Proof_Context.theory_of ctxt;
53794
af7d1533a25b undid copy-paste
blanchet
parents: 53793
diff changeset
   252
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   253
    fun fld conds t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   254
      (case Term.strip_comb t of
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   255
        (Const (@{const_name Let}, _), [_, _]) => fld conds (unfold_lets_splits t)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   256
      | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   257
        fld (conds @ conjuncts_s cond) then_branch o fld (conds @ s_not_conj [cond]) else_branch
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   258
      | (Const (c, _), args as _ :: _ :: _) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   259
        let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   260
          if n >= 0 andalso n < length args then
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   261
            (case fastype_of1 (bound_Ts, nth args n) of
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   262
              Type (s, Ts) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   263
              (case dest_case ctxt s Ts t of
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   264
                SOME ({split_sels = _ :: _, ...}, conds', branches) =>
55341
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   265
                fold_rev (uncurry fld) (map (append conds o conjuncts_s) conds' ~~ branches)
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   266
              | _ => f conds t)
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   267
            | _ => f conds t)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   268
          else
55341
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   269
            f conds t
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   270
        end
55342
blanchet
parents: 55341
diff changeset
   271
      | _ => f conds t);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   272
  in
55341
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   273
    fld []
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   274
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   275
54970
891141de5672 only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents: 54969
diff changeset
   276
fun case_of ctxt s =
891141de5672 only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents: 54969
diff changeset
   277
  (case ctr_sugar_of ctxt s of
62318
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   278
    SOME {casex = Const (s', _), split_sels, ...} => SOME (s', not (null split_sels))
54970
891141de5672 only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents: 54969
diff changeset
   279
  | _ => NONE);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   280
62318
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   281
fun massage_let_if_case ctxt has_call massage_leaf unexpected_call unsupported_case bound_Ts t0 =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   282
  let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   283
    val thy = Proof_Context.theory_of ctxt;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   284
60001
0e1b220ec4c9 generalized code
blanchet
parents: 59989
diff changeset
   285
    fun check_no_call bound_Ts t = if has_call t then unexpected_call bound_Ts t else ();
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   286
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   287
    fun massage_abs bound_Ts 0 t = massage_rec bound_Ts t
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   288
      | massage_abs bound_Ts m (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) (m - 1) t)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   289
      | massage_abs bound_Ts m t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   290
        let val T = domain_type (fastype_of1 (bound_Ts, t)) in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   291
          Abs (Name.uu, T, massage_abs (T :: bound_Ts) (m - 1) (incr_boundvars 1 t $ Bound 0))
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   292
        end
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   293
    and massage_rec bound_Ts t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   294
      let val typof = curry fastype_of1 bound_Ts in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   295
        (case Term.strip_comb t of
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   296
          (Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_lets_splits t)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   297
        | (Const (@{const_name If}, _), obj :: (branches as [_, _])) =>
59612
7ea413656b64 avoid needless 'if ... undefined' in generated theorems
blanchet
parents: 59609
diff changeset
   298
          (case List.partition Term.is_dummy_pattern (map (massage_rec bound_Ts) branches) of
7ea413656b64 avoid needless 'if ... undefined' in generated theorems
blanchet
parents: 59609
diff changeset
   299
            (dummy_branch' :: _, []) => dummy_branch'
7ea413656b64 avoid needless 'if ... undefined' in generated theorems
blanchet
parents: 59609
diff changeset
   300
          | (_, [branch']) => branch'
7ea413656b64 avoid needless 'if ... undefined' in generated theorems
blanchet
parents: 59609
diff changeset
   301
          | (_, branches') =>
60001
0e1b220ec4c9 generalized code
blanchet
parents: 59989
diff changeset
   302
            Term.list_comb (If_const (typof (hd branches')) $ tap (check_no_call bound_Ts) obj,
0e1b220ec4c9 generalized code
blanchet
parents: 59989
diff changeset
   303
              branches'))
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61348
diff changeset
   304
        | (c as Const (@{const_name case_prod}, _), arg :: args) =>
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   305
          massage_rec bound_Ts
57895
a85e0ab840c1 less aggressive unfolding; removed debugging;
blanchet
parents: 57551
diff changeset
   306
            (unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   307
        | (Const (c, _), args as _ :: _ :: _) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   308
          (case try strip_fun_type (Sign.the_const_type thy c) of
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   309
            SOME (gen_branch_Ts, gen_body_fun_T) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   310
            let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   311
              val gen_branch_ms = map num_binder_types gen_branch_Ts;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   312
              val n = length gen_branch_ms;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   313
            in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   314
              if n < length args then
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   315
                (case gen_body_fun_T of
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   316
                  Type (_, [Type (T_name, _), _]) =>
62318
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   317
                  (case case_of ctxt T_name of
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   318
                    SOME (c', has_split_sels) =>
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   319
                    if c' = c then
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   320
                      if has_split_sels then
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   321
                        let
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   322
                          val (branches, obj_leftovers) = chop n args;
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   323
                          val branches' = map2 (massage_abs bound_Ts) gen_branch_ms branches;
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   324
                          val branch_Ts' = map typof branches';
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   325
                          val body_T' = snd (strip_typeN (hd gen_branch_ms) (hd branch_Ts'));
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   326
                          val casex' =
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   327
                            Const (c, branch_Ts' ---> map typof obj_leftovers ---> body_T');
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   328
                        in
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   329
                          Term.list_comb (casex',
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   330
                            branches' @ tap (List.app (check_no_call bound_Ts)) obj_leftovers)
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   331
                        end
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   332
                      else
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   333
                        unsupported_case bound_Ts t
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   334
                    else
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   335
                      massage_leaf bound_Ts t
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   336
                  | NONE => massage_leaf bound_Ts t)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   337
                | _ => massage_leaf bound_Ts t)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   338
              else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   339
                massage_leaf bound_Ts t
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   340
            end
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   341
          | NONE => massage_leaf bound_Ts t)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   342
        | _ => massage_leaf bound_Ts t)
55342
blanchet
parents: 55341
diff changeset
   343
      end;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   344
  in
59596
c067eba942e7 no quick_and_dirty for goals that may fail + tuned messages
blanchet
parents: 59595
diff changeset
   345
    massage_rec bound_Ts t0
59612
7ea413656b64 avoid needless 'if ... undefined' in generated theorems
blanchet
parents: 59609
diff changeset
   346
    |> Term.map_aterms (fn t =>
7ea413656b64 avoid needless 'if ... undefined' in generated theorems
blanchet
parents: 59609
diff changeset
   347
      if Term.is_dummy_pattern t then Const (@{const_name undefined}, fastype_of t) else t)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   348
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   349
60001
0e1b220ec4c9 generalized code
blanchet
parents: 59989
diff changeset
   350
fun massage_let_if_case_corec ctxt has_call massage_leaf bound_Ts t0 =
62318
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   351
  massage_let_if_case ctxt has_call massage_leaf (K (unexpected_corec_call ctxt [t0]))
b42858e540bb clearer error message
blanchet
parents: 61841
diff changeset
   352
    (K (unsupported_case_around_corec_call ctxt [t0])) bound_Ts t0;
60001
0e1b220ec4c9 generalized code
blanchet
parents: 59989
diff changeset
   353
59989
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
   354
fun massage_nested_corec_call ctxt has_call massage_call massage_noncall bound_Ts U T t0 =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   355
  let
59596
c067eba942e7 no quick_and_dirty for goals that may fail + tuned messages
blanchet
parents: 59595
diff changeset
   356
    fun check_no_call t = if has_call t then unexpected_corec_call ctxt [t0] t else ();
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   357
59609
7892ffd1c39d deal better with corecursion through functions
blanchet
parents: 59608
diff changeset
   358
    fun massage_mutual_call bound_Ts (Type (@{type_name fun}, [_, U2]))
7892ffd1c39d deal better with corecursion through functions
blanchet
parents: 59608
diff changeset
   359
        (Type (@{type_name fun}, [T1, T2])) t =
62582
969480bdef55 eta-expansion done right in "primcorec"
blanchet
parents: 62497
diff changeset
   360
        Abs (Name.uu, T1, massage_mutual_call (T1 :: bound_Ts) U2 T2 (incr_boundvars 1 t $ Bound 0))
59609
7892ffd1c39d deal better with corecursion through functions
blanchet
parents: 59608
diff changeset
   361
      | massage_mutual_call bound_Ts U T t =
59989
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
   362
        (if has_call t then massage_call else massage_noncall) bound_Ts U T t;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   363
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   364
    fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   365
        (case try (dest_map ctxt s) t of
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   366
          SOME (map0, fs) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   367
          let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   368
            val Type (_, dom_Ts) = domain_type (fastype_of1 (bound_Ts, t));
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   369
            val map' = mk_map (length fs) dom_Ts Us map0;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   370
            val fs' =
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   371
              map_flattened_map_args ctxt s (@{map 3} (massage_map_or_map_arg bound_Ts) Us Ts) fs;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   372
          in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   373
            Term.list_comb (map', fs')
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   374
          end
58223
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
   375
        | NONE => raise NO_MAP t)
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
   376
      | massage_map _ _ _ t = raise NO_MAP t
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   377
    and massage_map_or_map_arg bound_Ts U T t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   378
      if T = U then
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   379
        tap check_no_call t
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   380
      else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   381
        massage_map bound_Ts U T t
58223
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
   382
        handle NO_MAP _ => massage_mutual_fun bound_Ts U T t
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   383
    and massage_mutual_fun bound_Ts U T t =
60741
6349a28af772 made code less loopy
blanchet
parents: 60739
diff changeset
   384
      let
6349a28af772 made code less loopy
blanchet
parents: 60739
diff changeset
   385
        val j = Term.maxidx_of_term t + 1;
6349a28af772 made code less loopy
blanchet
parents: 60739
diff changeset
   386
        val var = Var ((Name.uu, j), domain_type (fastype_of1 (bound_Ts, t)));
6349a28af772 made code less loopy
blanchet
parents: 60739
diff changeset
   387
6349a28af772 made code less loopy
blanchet
parents: 60739
diff changeset
   388
        fun massage_body () =
59947
09317aff0ff9 generalized code
blanchet
parents: 59946
diff changeset
   389
          Term.lambda var (Term.incr_boundvars 1 (massage_any_call bound_Ts U T
60741
6349a28af772 made code less loopy
blanchet
parents: 60739
diff changeset
   390
            (betapply (t, var))));
6349a28af772 made code less loopy
blanchet
parents: 60739
diff changeset
   391
      in
6349a28af772 made code less loopy
blanchet
parents: 60739
diff changeset
   392
        (case t of
6349a28af772 made code less loopy
blanchet
parents: 60739
diff changeset
   393
          Const (@{const_name comp}, _) $ t1 $ t2 =>
6349a28af772 made code less loopy
blanchet
parents: 60739
diff changeset
   394
          if has_call t2 then massage_body ()
6349a28af772 made code less loopy
blanchet
parents: 60739
diff changeset
   395
          else mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, t2)
6349a28af772 made code less loopy
blanchet
parents: 60739
diff changeset
   396
        | _ => massage_body ())
6349a28af772 made code less loopy
blanchet
parents: 60739
diff changeset
   397
      end
59947
09317aff0ff9 generalized code
blanchet
parents: 59946
diff changeset
   398
    and massage_any_call bound_Ts U T =
60001
0e1b220ec4c9 generalized code
blanchet
parents: 59989
diff changeset
   399
      massage_let_if_case_corec ctxt has_call (fn bound_Ts => fn t =>
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   400
        if has_call t then
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   401
          (case U of
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   402
            Type (s, Us) =>
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   403
            (case try (dest_ctr ctxt s) t of
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   404
              SOME (f, args) =>
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   405
              let
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   406
                val typof = curry fastype_of1 bound_Ts;
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   407
                val f' = mk_ctr Us f
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   408
                val f'_T = typof f';
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   409
                val arg_Ts = map typof args;
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   410
              in
59598
c9d304d6ae98 more 'primcorec' error handling
blanchet
parents: 59597
diff changeset
   411
                Term.list_comb (f',
59947
09317aff0ff9 generalized code
blanchet
parents: 59946
diff changeset
   412
                  @{map 3} (massage_any_call bound_Ts) (binder_types f'_T) arg_Ts args)
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   413
              end
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   414
            | NONE =>
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   415
              (case t of
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61348
diff changeset
   416
                Const (@{const_name case_prod}, _) $ t' =>
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   417
                let
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   418
                  val U' = curried_type U;
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   419
                  val T' = curried_type T;
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   420
                in
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61348
diff changeset
   421
                  Const (@{const_name case_prod}, U' --> U) $ massage_any_call bound_Ts U' T' t'
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   422
                end
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   423
              | t1 $ t2 =>
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   424
                (if has_call t2 then
59989
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
   425
                   massage_mutual_call bound_Ts U T t
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
   426
                 else
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
   427
                   massage_map bound_Ts U T t1 $ t2
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
   428
                   handle NO_MAP _ => massage_mutual_call bound_Ts U T t)
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   429
              | Abs (s, T', t') =>
59947
09317aff0ff9 generalized code
blanchet
parents: 59946
diff changeset
   430
                Abs (s, T', massage_any_call (T' :: bound_Ts) (range_type U) (range_type T) t')
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   431
              | _ => massage_mutual_call bound_Ts U T t))
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   432
          | _ => ill_formed_corec_call ctxt t)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   433
        else
59989
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
   434
          massage_noncall bound_Ts U T t) bound_Ts;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   435
  in
59989
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
   436
    (if has_call t0 then massage_any_call else massage_noncall) bound_Ts U T t0
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   437
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   438
60683
d34e1b0b331a tuned ML signature
blanchet
parents: 60362
diff changeset
   439
fun expand_to_ctr_term ctxt (T as Type (s, Ts)) t =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   440
  (case ctr_sugar_of ctxt s of
60683
d34e1b0b331a tuned ML signature
blanchet
parents: 60362
diff changeset
   441
    SOME {ctrs, casex, ...} => Term.list_comb (mk_case Ts T casex, map (mk_ctr Ts) ctrs) $ t
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   442
  | NONE => raise Fail "expand_to_ctr_term");
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   443
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   444
fun expand_corec_code_rhs ctxt has_call bound_Ts t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   445
  (case fastype_of1 (bound_Ts, t) of
60683
d34e1b0b331a tuned ML signature
blanchet
parents: 60362
diff changeset
   446
    T as Type (s, _) =>
60001
0e1b220ec4c9 generalized code
blanchet
parents: 59989
diff changeset
   447
    massage_let_if_case_corec ctxt has_call (fn _ => fn t =>
60683
d34e1b0b331a tuned ML signature
blanchet
parents: 60362
diff changeset
   448
      if can (dest_ctr ctxt s) t then t else expand_to_ctr_term ctxt T t) bound_Ts t
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   449
  | _ => raise Fail "expand_corec_code_rhs");
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   450
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   451
fun massage_corec_code_rhs ctxt massage_ctr =
60001
0e1b220ec4c9 generalized code
blanchet
parents: 59989
diff changeset
   452
  massage_let_if_case_corec ctxt (K false)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   453
    (fn bound_Ts => uncurry (massage_ctr bound_Ts) o Term.strip_comb);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   454
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   455
fun fold_rev_corec_code_rhs ctxt f =
55341
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   456
  fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   457
55400
blanchet
parents: 55344
diff changeset
   458
fun case_thms_of_term ctxt t =
blanchet
parents: 55344
diff changeset
   459
  let val ctr_sugars = map_filter (Ctr_Sugar.ctr_sugar_of_case ctxt o fst) (Term.add_consts t []) in
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   460
    (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #exhaust_discs ctr_sugars,
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   461
     maps #split_sels ctr_sugars, maps #split_sel_asms ctr_sugars)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   462
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   463
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   464
fun basic_corec_specs_of ctxt res_T =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   465
  (case res_T of
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   466
    Type (T_name, _) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   467
    (case Ctr_Sugar.ctr_sugar_of ctxt T_name of
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   468
      NONE => not_codatatype ctxt res_T
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58131
diff changeset
   469
    | SOME {T = fpT, ctrs, discs, selss, ...} =>
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   470
      let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   471
        val thy = Proof_Context.theory_of ctxt;
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   472
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58131
diff changeset
   473
        val As_rho = tvar_subst thy [fpT] [res_T];
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   474
        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: 54243
diff changeset
   475
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   476
        fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels};
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   477
      in
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   478
        @{map 3} mk_spec ctrs discs selss
54911
6a6980245ce0 robustness
blanchet
parents: 54910
diff changeset
   479
        handle ListPair.UnequalLengths => not_codatatype ctxt res_T
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   480
      end)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   481
  | _ => not_codatatype ctxt res_T);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   482
59674
198eaf28a8b8 export more functions (for future 'corec')
blanchet
parents: 59673
diff changeset
   483
fun map_thms_of_type ctxt (Type (s, _)) =
58462
b46874f2090f refactor fp_sugar move theorems
desharna
parents: 58461
diff changeset
   484
    (case fp_sugar_of ctxt s of SOME {fp_bnf_sugar = {map_thms, ...}, ...} => map_thms | NONE => [])
59674
198eaf28a8b8 export more functions (for future 'corec')
blanchet
parents: 59673
diff changeset
   485
  | map_thms_of_type _ _ = [];
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   486
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   487
structure GFP_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
   488
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   489
fun gfp_rec_sugar_interpretation name f =
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   490
  GFP_Rec_Sugar_Plugin.interpretation name (fn fp_rec_sugar => fn lthy =>
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   491
    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
   492
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
   493
val interpret_gfp_rec_sugar = GFP_Rec_Sugar_Plugin.data;
59275
77cd4992edcd Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents: 59058
diff changeset
   494
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   495
fun corec_specs_of bs arg_Ts res_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: 54243
diff changeset
   496
  let
55005
38ea5ee18a06 use the right context in 'unfold_thms id_def'
blanchet
parents: 54979
diff changeset
   497
    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: 54243
diff changeset
   498
57397
5004aca20821 tuned variable names
blanchet
parents: 57303
diff changeset
   499
    val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs,
58461
75ee8d49c724 refactor fp_sugar move theorems
desharna
parents: 58460
diff changeset
   500
          fp_co_induct_sugar = {common_co_inducts = common_coinduct_thms, ...}, ...} :: _,
75ee8d49c724 refactor fp_sugar move theorems
desharna
parents: 58460
diff changeset
   501
          (_, gfp_sugar_thms)), lthy) =
58335
a5a3b576fcfb generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents: 58286
diff changeset
   502
      nested_to_mutual_fps (K true) Greatest_FP bs res_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: 54243
diff changeset
   503
58286
a15731cf1835 compile
blanchet
parents: 58283
diff changeset
   504
    val coinduct_attrs_pair =
a15731cf1835 compile
blanchet
parents: 58283
diff changeset
   505
      (case gfp_sugar_thms of SOME ((_, attrs_pair), _, _, _, _) => attrs_pair | NONE => ([], []));
58283
71d74e641538 preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents: 58223
diff changeset
   506
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 59044
diff changeset
   507
    val perm_fp_sugars = sort (int_ord o apply2 #fp_res_index) fp_sugars;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   508
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   509
    val indices = map #fp_res_index fp_sugars;
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   510
    val perm_indices = map #fp_res_index perm_fp_sugars;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   511
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58131
diff changeset
   512
    val perm_fpTs = map #T perm_fp_sugars;
58460
a88eb33058f7 refactor fp_sugar move theorems
desharna
parents: 58459
diff changeset
   513
    val perm_ctrXs_Tsss' =
a88eb33058f7 refactor fp_sugar move theorems
desharna
parents: 58459
diff changeset
   514
      map (repair_nullary_single_ctr o #ctrXs_Tss o #fp_ctr_sugar) perm_fp_sugars;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   515
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   516
    val nn0 = length res_Ts;
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58131
diff changeset
   517
    val nn = length perm_fpTs;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   518
    val kks = 0 upto nn - 1;
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   519
    val perm_ns' = map length perm_ctrXs_Tsss';
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   520
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   521
    val perm_Ts = map #T perm_fp_sugars;
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   522
    val perm_Xs = map #X perm_fp_sugars;
58461
75ee8d49c724 refactor fp_sugar move theorems
desharna
parents: 58460
diff changeset
   523
    val perm_Cs =
75ee8d49c724 refactor fp_sugar move theorems
desharna
parents: 58460
diff changeset
   524
      map (domain_type o body_fun_type o fastype_of o #co_rec o #fp_co_induct_sugar) perm_fp_sugars;
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   525
    val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   526
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   527
    fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)]
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   528
      | zip_corecT U =
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   529
        (case AList.lookup (op =) Xs_TCs U of
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   530
          SOME (T, C) => [T, C]
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   531
        | NONE => [U]);
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   532
55869
54ddb003e128 rationalized internals
blanchet
parents: 55863
diff changeset
   533
    val perm_p_Tss = mk_corec_p_pred_types perm_Cs perm_ns';
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   534
    val perm_f_Tssss =
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   535
      map2 (fn C => map (map (map (curry (op -->) C) o zip_corecT))) perm_Cs perm_ctrXs_Tsss';
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   536
    val perm_q_Tssss =
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   537
      map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) perm_f_Tssss;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   538
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   539
    val (perm_p_hss, h) = indexedd perm_p_Tss 0;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   540
    val (perm_q_hssss, h') = indexedddd perm_q_Tssss h;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   541
    val (perm_f_hssss, _) = indexedddd perm_f_Tssss h';
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   542
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   543
    val fun_arg_hs =
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   544
      flat (@{map 3} flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   545
55480
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55462
diff changeset
   546
    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: 55462
diff changeset
   547
    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: 54243
diff changeset
   548
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   549
    val coinduct_thmss = map (unpermute0 o conj_dests nn) common_coinduct_thms;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   550
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   551
    val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   552
    val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   553
    val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss);
53358
b46e6cd75dc6 improved interfaces
panny
parents: 53357
diff changeset
   554
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   555
    val f_Tssss = unpermute perm_f_Tssss;
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58131
diff changeset
   556
    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: 54243
diff changeset
   557
    val Cs = unpermute perm_Cs;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   558
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58131
diff changeset
   559
    val As_rho = tvar_subst thy (take nn0 fpTs) res_Ts;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   560
    val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   561
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   562
    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: 54243
diff changeset
   563
    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: 54243
diff changeset
   564
    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: 54243
diff changeset
   565
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   566
    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: 54243
diff changeset
   567
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   568
    fun call_of nullary [] [g_i] [Type (@{type_name fun}, [_, T])] =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   569
        (if exists_subtype_in Cs T then Nested_Corec
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   570
         else if nullary then Dummy_No_Corec
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   571
         else No_Corec) g_i
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   572
      | call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i');
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   573
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   574
    fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms distinct_discss collapse
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   575
        corec_thm corec_disc corec_sels =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   576
      let val nullary = not (can dest_funT (fastype_of ctr)) in
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   577
        {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_io,
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   578
         calls = @{map 3} (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   579
         distinct_discss = distinct_discss, collapse = collapse, corec_thm = corec_thm,
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   580
         corec_disc = corec_disc, corec_sels = corec_sels}
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   581
      end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   582
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   583
    fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, distinct_discsss, collapses, ...}
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   584
        : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms corec_discs corec_selss =
55863
fa3a1ec69a1b rationalize internals
blanchet
parents: 55860
diff changeset
   585
      let val p_ios = map SOME p_is @ [NONE] in
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   586
        @{map 14} mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   587
          distinct_discsss collapses corec_thms corec_discs corec_selss
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   588
      end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   589
58461
75ee8d49c724 refactor fp_sugar move theorems
desharna
parents: 58460
diff changeset
   590
    fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...},
75ee8d49c724 refactor fp_sugar move theorems
desharna
parents: 58460
diff changeset
   591
        fp_co_induct_sugar = {co_rec = corec, co_rec_thms = corec_thms, co_rec_discs = corec_discs,
58459
f70bffabd7cf refactor fp_sugar move theorems
desharna
parents: 58394
diff changeset
   592
        co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
59598
c9d304d6ae98 more 'primcorec' error handling
blanchet
parents: 59597
diff changeset
   593
      {T = T, corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec,
c9d304d6ae98 more 'primcorec' error handling
blanchet
parents: 59597
diff changeset
   594
       exhaust_discs = exhaust_discs, sel_defs = sel_defs,
59674
198eaf28a8b8 export more functions (for future 'corec')
blanchet
parents: 59673
diff changeset
   595
       fp_nesting_maps = maps (map_thms_of_type lthy o T_of_bnf) fp_nesting_bnfs,
57399
cfc19f0a6261 compile
blanchet
parents: 57397
diff changeset
   596
       fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs,
57397
5004aca20821 tuned variable names
blanchet
parents: 57303
diff changeset
   597
       fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs,
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   598
       ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms corec_discs
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   599
         corec_selss};
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   600
  in
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   601
    (@{map 5} mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
58283
71d74e641538 preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents: 58223
diff changeset
   602
     co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
71d74e641538 preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents: 58223
diff changeset
   603
     co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss, coinduct_attrs_pair,
71d74e641538 preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents: 58223
diff changeset
   604
     is_some gfp_sugar_thms, lthy)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   605
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   606
53358
b46e6cd75dc6 improved interfaces
panny
parents: 53357
diff changeset
   607
val undef_const = Const (@{const_name undefined}, dummyT);
53357
46b0c7a08af7 simplified rewriting of map arguments
panny
parents: 53354
diff changeset
   608
58393
blanchet
parents: 58387
diff changeset
   609
type coeqn_data_disc =
blanchet
parents: 58387
diff changeset
   610
  {fun_name: string,
blanchet
parents: 58387
diff changeset
   611
   fun_T: typ,
blanchet
parents: 58387
diff changeset
   612
   fun_args: term list,
blanchet
parents: 58387
diff changeset
   613
   ctr: term,
blanchet
parents: 58387
diff changeset
   614
   ctr_no: int,
blanchet
parents: 58387
diff changeset
   615
   disc: term,
blanchet
parents: 58387
diff changeset
   616
   prems: term list,
blanchet
parents: 58387
diff changeset
   617
   auto_gen: bool,
blanchet
parents: 58387
diff changeset
   618
   ctr_rhs_opt: term option,
blanchet
parents: 58387
diff changeset
   619
   code_rhs_opt: term option,
blanchet
parents: 58387
diff changeset
   620
   eqn_pos: int,
blanchet
parents: 58387
diff changeset
   621
   user_eqn: term};
54001
65fc58793ed5 made SML/NJ happier
blanchet
parents: 53925
diff changeset
   622
58393
blanchet
parents: 58387
diff changeset
   623
type coeqn_data_sel =
blanchet
parents: 58387
diff changeset
   624
  {fun_name: string,
blanchet
parents: 58387
diff changeset
   625
   fun_T: typ,
blanchet
parents: 58387
diff changeset
   626
   fun_args: term list,
blanchet
parents: 58387
diff changeset
   627
   ctr: term,
blanchet
parents: 58387
diff changeset
   628
   sel: term,
blanchet
parents: 58387
diff changeset
   629
   rhs_term: term,
blanchet
parents: 58387
diff changeset
   630
   ctr_rhs_opt: term option,
blanchet
parents: 58387
diff changeset
   631
   code_rhs_opt: term option,
blanchet
parents: 58387
diff changeset
   632
   eqn_pos: int,
blanchet
parents: 58387
diff changeset
   633
   user_eqn: term};
54001
65fc58793ed5 made SML/NJ happier
blanchet
parents: 53925
diff changeset
   634
59602
2a6226d89fa3 more primcorec messages
blanchet
parents: 59601
diff changeset
   635
fun ctr_sel_of ({ctr, sel, ...} : coeqn_data_sel) = (ctr, sel);
2a6226d89fa3 more primcorec messages
blanchet
parents: 59601
diff changeset
   636
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   637
datatype coeqn_data =
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   638
  Disc of coeqn_data_disc |
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   639
  Sel of coeqn_data_sel;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   640
59948
c8860ec6fc80 generalized slightly
blanchet
parents: 59947
diff changeset
   641
fun is_free_in frees (Free (s, _)) = member (op =) frees s
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   642
  | is_free_in _ _ = false;
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   643
59948
c8860ec6fc80 generalized slightly
blanchet
parents: 59947
diff changeset
   644
fun is_catch_all_prem (Free (s, _)) = s = Name.uu_
59799
0b21e85fd9ba clarified role of Name.uu_, which happens to be the internal replacement of the first underscore under certain assumptions about the context;
wenzelm
parents: 59674
diff changeset
   645
  | is_catch_all_prem _ = false;
0b21e85fd9ba clarified role of Name.uu_, which happens to be the internal replacement of the first underscore under certain assumptions about the context;
wenzelm
parents: 59674
diff changeset
   646
59599
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
   647
fun add_extra_frees ctxt frees names =
59948
c8860ec6fc80 generalized slightly
blanchet
parents: 59947
diff changeset
   648
  fold_aterms (fn x as Free (s, _) =>
c8860ec6fc80 generalized slightly
blanchet
parents: 59947
diff changeset
   649
    (not (member (op =) frees x) andalso not (member (op =) names s) andalso
c8860ec6fc80 generalized slightly
blanchet
parents: 59947
diff changeset
   650
     not (Variable.is_fixed ctxt s) andalso not (is_catch_all_prem x))
59599
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
   651
    ? cons x | _ => I);
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
   652
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
   653
fun check_extra_frees ctxt frees names t =
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
   654
  let val bads = add_extra_frees ctxt frees names t [] in
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
   655
    null bads orelse extra_variable ctxt [t] (hd bads)
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   656
  end;
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   657
59604
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   658
fun check_fun_args ctxt eqn fun_args =
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   659
  let
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   660
    val dups = duplicates (op =) fun_args;
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   661
    val _ = null dups orelse error_at ctxt [eqn]
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   662
        ("Duplicate variable " ^ quote (Syntax.string_of_term ctxt (hd dups)));
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   663
59607
a93592aedce4 message tuning
blanchet
parents: 59606
diff changeset
   664
    val _ = forall is_Free fun_args orelse
a93592aedce4 message tuning
blanchet
parents: 59606
diff changeset
   665
      error_at ctxt [eqn] ("Non-variable function argument on left-hand side " ^
a93592aedce4 message tuning
blanchet
parents: 59606
diff changeset
   666
        quote (Syntax.string_of_term ctxt (the (find_first (not o is_Free) fun_args))));
a93592aedce4 message tuning
blanchet
parents: 59606
diff changeset
   667
59604
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   668
    val fixeds = filter (Variable.is_fixed ctxt o fst o dest_Free) fun_args;
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   669
    val _ = null fixeds orelse error_at ctxt [eqn] ("Function argument " ^
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   670
        quote (Syntax.string_of_term ctxt (hd fixeds)) ^ " is fixed in context");
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   671
  in () end;
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   672
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   673
fun dissect_coeqn_disc ctxt fun_names sequentials
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   674
    (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos ctr_rhs_opt code_rhs_opt prems0
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   675
    concl matchedsss =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   676
  let
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   677
    fun find_subterm p =
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   678
      let (* FIXME \<exists>? *)
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   679
        fun find (t as u $ v) = if p t then SOME t else merge_options (find u, find v)
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   680
          | find t = if p t then SOME t else NONE;
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   681
      in find end;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   682
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   683
    val applied_fun = concl
55008
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
   684
      |> find_subterm (member (op = o apsnd SOME) fun_names o try (fst o dest_Free o head_of))
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   685
      |> the
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   686
      handle Option.Option => error_at ctxt [concl] "Ill-formed discriminator formula";
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   687
    val ((fun_name, fun_T), fun_args) = strip_comb applied_fun |>> dest_Free;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   688
59604
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   689
    val _ = check_fun_args ctxt concl fun_args;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   690
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   691
    val bads = filter (Term.exists_subterm (is_free_in fun_names)) prems0;
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   692
    val _ = null bads orelse error_at ctxt bads "Corecursive call(s) in condition(s)";
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   693
58393
blanchet
parents: 58387
diff changeset
   694
    val (sequential, basic_ctr_specs) =
blanchet
parents: 58387
diff changeset
   695
      the (AList.lookup (op =) (fun_names ~~ (sequentials ~~ basic_ctr_specss)) fun_name);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   696
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   697
    val discs = map #disc basic_ctr_specs;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   698
    val ctrs = map #ctr basic_ctr_specs;
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   699
    val not_disc = head_of concl = @{term Not};
53401
2101a97e6220 various refactoring;
panny
parents: 53360
diff changeset
   700
    val _ = not_disc andalso length ctrs <> 2 andalso
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   701
      error_at ctxt [concl] "Negated discriminator for a type with \<noteq> 2 constructors";
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   702
    val disc' = find_subterm (member (op =) discs o head_of) concl;
54209
blanchet
parents: 54208
diff changeset
   703
    val eq_ctr0 = concl |> perhaps (try HOLogic.dest_not) |> try (HOLogic.dest_eq #> snd)
59598
c9d304d6ae98 more 'primcorec' error handling
blanchet
parents: 59597
diff changeset
   704
      |> (fn SOME t => let val n = find_index (curry (op =) t) ctrs in
c9d304d6ae98 more 'primcorec' error handling
blanchet
parents: 59597
diff changeset
   705
        if n >= 0 then SOME n else NONE end | _ => NONE);
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   706
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   707
    val _ = is_none disc' orelse perhaps (try HOLogic.dest_not) concl = the disc' orelse
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   708
      error_at ctxt [concl] "Ill-formed discriminator formula";
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   709
    val _ = is_some disc' orelse is_some eq_ctr0 orelse
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   710
      error_at ctxt [concl] "No discriminator in equation";
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   711
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   712
    val ctr_no' =
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   713
      if is_none disc' then the eq_ctr0 else find_index (curry (op =) (head_of (the disc'))) discs;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   714
    val ctr_no = if not_disc then 1 - ctr_no' else ctr_no';
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   715
    val {ctr, disc, ...} = nth basic_ctr_specs ctr_no;
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   716
59605
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   717
    val catch_all =
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   718
      (case prems0 of
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   719
        [prem] => is_catch_all_prem prem
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   720
      | _ =>
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   721
        if exists is_catch_all_prem prems0 then error_at ctxt [concl] "Superfluous premises"
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   722
        else false);
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   723
    val matchedss = AList.lookup (op =) matchedsss fun_name |> the_default [];
60704
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   724
    val prems = map (abstract_over_list fun_args) prems0;
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   725
    val actual_prems =
54901
0b8871677e0b use same name for feature internally as in user interface, to facilitate grepping
blanchet
parents: 54900
diff changeset
   726
      (if catch_all orelse sequential then maps s_not_conj matchedss else []) @
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   727
      (if catch_all then [] else prems);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   728
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   729
    val matchedsss' = AList.delete (op =) fun_name matchedsss
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   730
      |> cons (fun_name, if sequential then matchedss @ [prems] else matchedss @ [actual_prems]);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   731
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   732
    val user_eqn =
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   733
      (actual_prems, concl)
60704
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   734
      |>> map HOLogic.mk_Trueprop ||> HOLogic.mk_Trueprop o abstract_over_list fun_args
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   735
      |> curry Logic.list_all (map dest_Free fun_args) o Logic.list_implies;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   736
59599
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
   737
    val _ = check_extra_frees ctxt fun_args fun_names user_eqn;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   738
  in
58393
blanchet
parents: 58387
diff changeset
   739
    (Disc {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = ctr_no,
blanchet
parents: 58387
diff changeset
   740
       disc = disc, prems = actual_prems, auto_gen = catch_all, ctr_rhs_opt = ctr_rhs_opt,
blanchet
parents: 58387
diff changeset
   741
       code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos, user_eqn = user_eqn},
blanchet
parents: 58387
diff changeset
   742
     matchedsss')
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   743
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   744
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   745
fun dissect_coeqn_sel ctxt fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   746
    ctr_rhs_opt code_rhs_opt eqn0 of_spec_opt eqn =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   747
  let
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   748
    val (lhs, rhs) = HOLogic.dest_eq eqn
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   749
      handle TERM _ => error_at ctxt [eqn] "Ill-formed equation (expected \"lhs = rhs\")";
59604
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   750
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   751
    val sel = head_of lhs;
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   752
    val ((fun_name, fun_T), fun_args) = dest_comb lhs |> snd |> strip_comb |> apfst dest_Free
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   753
      handle TERM _ => error_at ctxt [eqn] "Ill-formed selector argument in left-hand side";
59604
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   754
    val _ = check_fun_args ctxt eqn fun_args;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   755
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   756
    val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name)
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   757
      handle Option.Option => error_at ctxt [eqn] "Ill-formed selector argument in left-hand side";
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   758
    val {ctr, ...} =
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   759
      (case of_spec_opt of
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   760
        SOME of_spec => the (find_first (curry (op =) of_spec o #ctr) basic_ctr_specs)
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   761
      | NONE => filter (exists (curry (op =) sel) o #sels) basic_ctr_specs |> the_single
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   762
          handle List.Empty => error_at ctxt [eqn] "Ambiguous selector (without \"of\")");
54979
d7593bfccf25 correctly extract code RHS, with loose bound variables
blanchet
parents: 54978
diff changeset
   763
    val user_eqn = drop_all eqn0;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   764
59599
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
   765
    val _ = check_extra_frees ctxt fun_args fun_names user_eqn;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   766
  in
58393
blanchet
parents: 58387
diff changeset
   767
    Sel {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, sel = sel,
blanchet
parents: 58387
diff changeset
   768
      rhs_term = rhs, ctr_rhs_opt = ctr_rhs_opt, code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos,
blanchet
parents: 58387
diff changeset
   769
      user_eqn = user_eqn}
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   770
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   771
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   772
fun dissect_coeqn_ctr ctxt fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list)
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   773
    eqn_pos eqn0 code_rhs_opt prems concl matchedsss =
53910
2c5055a3583d strengthen tactic
blanchet
parents: 53909
diff changeset
   774
  let
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   775
    val (lhs, rhs) = HOLogic.dest_eq concl;
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   776
    val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   777
59604
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   778
    val _ = check_fun_args ctxt concl fun_args;
59599
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
   779
    val _ = check_extra_frees ctxt fun_args fun_names (drop_all eqn0);
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   780
58393
blanchet
parents: 58387
diff changeset
   781
    val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name);
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   782
    val (ctr, ctr_args) = strip_comb (unfold_lets_splits rhs);
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   783
    val {disc, sels, ...} = the (find_first (curry (op =) ctr o #ctr) basic_ctr_specs)
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   784
      handle Option.Option => error_at ctxt [ctr] "Not a constructor";
53341
63015d035301 handle selector formulae with no corecursive calls
panny
parents: 53335
diff changeset
   785
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   786
    val disc_concl = betapply (disc, lhs);
54976
b502f04c0442 repair 'exhaustive' feature for one-constructor types
blanchet
parents: 54975
diff changeset
   787
    val (eqn_data_disc_opt, matchedsss') =
59042
ef0074e812cd smoothly handle unit codatatypes in 'primcorec'
blanchet
parents: 59041
diff changeset
   788
      if null (tl basic_ctr_specs) andalso not (null sels) then
54976
b502f04c0442 repair 'exhaustive' feature for one-constructor types
blanchet
parents: 54975
diff changeset
   789
        (NONE, matchedsss)
b502f04c0442 repair 'exhaustive' feature for one-constructor types
blanchet
parents: 54975
diff changeset
   790
      else
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   791
        apfst SOME (dissect_coeqn_disc ctxt fun_names sequentials basic_ctr_specss eqn_pos
60704
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   792
          (SOME (abstract_over_list fun_args rhs)) code_rhs_opt prems disc_concl matchedsss);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   793
54159
eb5d58c99049 set stage for more flexible 'primrec' syntax for recursion through functions
blanchet
parents: 54157
diff changeset
   794
    val sel_concls = sels ~~ ctr_args
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   795
      |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg))
59595
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59594
diff changeset
   796
      handle ListPair.UnequalLengths =>
2d90b85b9264 tuned new primrec messages
blanchet
parents: 59594
diff changeset
   797
        error_at ctxt [rhs] "Partially applied constructor in right-hand side";
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   798
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   799
    val eqns_data_sel =
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   800
      map (dissect_coeqn_sel ctxt fun_names basic_ctr_specss eqn_pos
60704
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   801
          (SOME (abstract_over_list fun_args rhs)) code_rhs_opt eqn0 (SOME ctr))
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   802
        sel_concls;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   803
  in
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   804
    (the_list eqn_data_disc_opt @ eqns_data_sel, matchedsss')
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   805
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   806
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   807
fun dissect_coeqn_code ctxt has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss =
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   808
  let
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   809
    val (lhs, (rhs', rhs)) = HOLogic.dest_eq concl ||> `(expand_corec_code_rhs ctxt has_call []);
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   810
    val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   811
59604
b44f128d24f2 improved primcorec messages
blanchet
parents: 59603
diff changeset
   812
    val _ = check_fun_args ctxt concl fun_args;
59599
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
   813
    val _ = check_extra_frees ctxt fun_args fun_names concl;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   814
58393
blanchet
parents: 58387
diff changeset
   815
    val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name);
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   816
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   817
    val cond_ctrs = fold_rev_corec_code_rhs ctxt (fn cs => fn ctr => fn _ =>
55008
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
   818
        if member (op = o apsnd #ctr) basic_ctr_specs ctr then cons (ctr, cs)
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   819
        else error ("Not a constructor: " ^ quote (Syntax.string_of_term ctxt ctr))) [] rhs' []
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   820
      |> AList.group (op =);
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   821
54068
447354985f6a generate optimized DNF formula
blanchet
parents: 54067
diff changeset
   822
    val ctr_premss = (case cond_ctrs of [_] => [[]] | _ => map (s_dnf o snd) cond_ctrs);
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   823
    val ctr_concls = cond_ctrs |> map (fn (ctr, _) =>
58393
blanchet
parents: 58387
diff changeset
   824
      binder_types (fastype_of ctr)
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   825
      |> map_index (fn (n, T) => massage_corec_code_rhs ctxt (fn _ => fn ctr' => fn args =>
59612
7ea413656b64 avoid needless 'if ... undefined' in generated theorems
blanchet
parents: 59609
diff changeset
   826
        if ctr' = ctr then nth args n else Term.dummy_pattern T) [] rhs')
58393
blanchet
parents: 58387
diff changeset
   827
      |> curry Term.list_comb ctr
blanchet
parents: 58387
diff changeset
   828
      |> curry HOLogic.mk_eq lhs);
54902
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   829
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   830
    val bads = maps (filter (Term.exists_subterm (is_free_in fun_names))) ctr_premss;
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   831
    val _ = null bads orelse unexpected_corec_call ctxt [eqn0] rhs;
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   832
54902
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   833
    val sequentials = replicate (length fun_names) false;
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   834
  in
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   835
    @{fold_map 2} (dissect_coeqn_ctr ctxt fun_names sequentials basic_ctr_specss eqn_pos eqn0
60704
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   836
        (SOME (abstract_over_list fun_args rhs)))
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   837
      ctr_premss ctr_concls matchedsss
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   838
  end;
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   839
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   840
fun dissect_coeqn ctxt has_call fun_names sequentials
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   841
    (basic_ctr_specss : basic_corec_ctr_spec list list) (eqn_pos, eqn0) of_spec_opt matchedsss =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   842
  let
54979
d7593bfccf25 correctly extract code RHS, with loose bound variables
blanchet
parents: 54978
diff changeset
   843
    val eqn = drop_all eqn0
59600
1716da11a11c more precise primcorec messages
blanchet
parents: 59599
diff changeset
   844
      handle TERM _ => error_at ctxt [eqn0] "Ill-formed formula";
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   845
    val (prems, concl) = Logic.strip_horn eqn
57527
1b07ca054327 add helper function map_prod
desharna
parents: 57399
diff changeset
   846
      |> map_prod (map HOLogic.dest_Trueprop) HOLogic.dest_Trueprop
59607
a93592aedce4 message tuning
blanchet
parents: 59606
diff changeset
   847
        handle TERM _ => error_at ctxt [eqn] "Ill-formed equation";
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   848
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   849
    val head = concl
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   850
      |> perhaps (try HOLogic.dest_not) |> perhaps (try (fst o HOLogic.dest_eq))
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   851
      |> head_of;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   852
59601
25ae098d8de2 more precise primcorec messages
blanchet
parents: 59600
diff changeset
   853
    val rhs_opt = concl |> perhaps (try HOLogic.dest_not) |> try (HOLogic.dest_eq #> snd);
59605
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   854
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   855
    fun check_num_args () =
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   856
      is_none rhs_opt orelse not (can dest_funT (fastype_of (the rhs_opt))) orelse
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   857
        error_at ctxt [eqn] "Expected more arguments to function on left-hand side";
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   858
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   859
    val discs = maps (map #disc) basic_ctr_specss;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   860
    val sels = maps (maps #sels) basic_ctr_specss;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   861
    val ctrs = maps (map #ctr) basic_ctr_specss;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   862
  in
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   863
    if member (op =) discs head orelse
58393
blanchet
parents: 58387
diff changeset
   864
       (is_some rhs_opt andalso
blanchet
parents: 58387
diff changeset
   865
        member (op =) (map SOME fun_names) (try (fst o dest_Free) head) andalso
blanchet
parents: 58387
diff changeset
   866
        member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt)) then
59608
e41ac095f99d removed too strict checks
blanchet
parents: 59607
diff changeset
   867
      (dissect_coeqn_disc ctxt fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl
59605
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   868
         matchedsss
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   869
       |>> single)
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   870
    else if member (op =) sels head then
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   871
      (null prems orelse error_at ctxt [eqn] "Unexpected condition in selector formula";
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   872
       ([dissect_coeqn_sel ctxt fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt
57550
934a54d04a9a throw error for bad input
panny
parents: 57527
diff changeset
   873
           concl], matchedsss))
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   874
    else if is_some rhs_opt andalso is_Free head andalso is_free_in fun_names head then
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   875
      if member (op =) ctrs (head_of (unfold_lets_splits (the rhs_opt))) then
59605
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   876
        (check_num_args ();
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   877
         dissect_coeqn_ctr ctxt fun_names sequentials basic_ctr_specss eqn_pos eqn0
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   878
           (if null prems then
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   879
              SOME (snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_assums_concl eqn0))))
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   880
            else
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   881
              NONE)
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   882
           prems concl matchedsss)
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   883
      else if null prems then
59605
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   884
        (check_num_args ();
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   885
         dissect_coeqn_code ctxt has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss
bd66d9b93a6b improved primcorec messages
blanchet
parents: 59604
diff changeset
   886
         |>> flat)
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   887
      else
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   888
        error_at ctxt [eqn] "Cannot mix constructor and code views"
59600
1716da11a11c more precise primcorec messages
blanchet
parents: 59599
diff changeset
   889
    else if is_some rhs_opt then
59607
a93592aedce4 message tuning
blanchet
parents: 59606
diff changeset
   890
      error_at ctxt [eqn] ("Ill-formed equation head: " ^ quote (Syntax.string_of_term ctxt head))
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   891
    else
59607
a93592aedce4 message tuning
blanchet
parents: 59606
diff changeset
   892
      error_at ctxt [eqn] "Expected equation or discriminator formula"
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   893
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   894
54002
01c8f9d3b084 made SML/NJ happy
blanchet
parents: 54001
diff changeset
   895
fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list)
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   896
    ({fun_args, ctr_no, prems, ...} : coeqn_data_disc) =
56858
0c3d0bc98abe simplify selectors in code views
blanchet
parents: 56806
diff changeset
   897
  if is_none (#pred (nth ctr_specs ctr_no)) then
0c3d0bc98abe simplify selectors in code views
blanchet
parents: 56806
diff changeset
   898
    I
0c3d0bc98abe simplify selectors in code views
blanchet
parents: 56806
diff changeset
   899
  else
54068
447354985f6a generate optimized DNF formula
blanchet
parents: 54067
diff changeset
   900
    s_conjs prems
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   901
    |> curry subst_bounds (List.rev fun_args)
55969
8820ddb8f9f4 use balanced tuples in 'primcorec'
blanchet
parents: 55966
diff changeset
   902
    |> abs_tuple_balanced fun_args
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   903
    |> K |> nth_map (the (#pred (nth ctr_specs ctr_no)));
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   904
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   905
fun build_corec_arg_no_call (sel_eqns : coeqn_data_sel list) sel =
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   906
  find_first (curry (op =) sel o #sel) sel_eqns
55969
8820ddb8f9f4 use balanced tuples in 'primcorec'
blanchet
parents: 55966
diff changeset
   907
  |> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple_balanced fun_args rhs_term)
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   908
  |> the_default undef_const
53411
ab4edf89992f support indirect corecursion
panny
parents: 53401
diff changeset
   909
  |> K;
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   910
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   911
fun build_corec_args_mutual_call ctxt has_call (sel_eqns : coeqn_data_sel list) sel =
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   912
  (case find_first (curry (op =) sel o #sel) sel_eqns of
54208
blanchet
parents: 54207
diff changeset
   913
    NONE => (I, I, I)
blanchet
parents: 54207
diff changeset
   914
  | SOME {fun_args, rhs_term, ... } =>
53876
fabf04d43a75 simplified code
panny
parents: 53875
diff changeset
   915
    let
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   916
      val bound_Ts = List.rev (map fastype_of fun_args);
59946
c18df9eea901 generalized code
blanchet
parents: 59945
diff changeset
   917
54207
9296ebf40db0 tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents: 54206
diff changeset
   918
      fun rewrite_stop _ t = if has_call t then @{term False} else @{term True};
9296ebf40db0 tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents: 54206
diff changeset
   919
      fun rewrite_end _ t = if has_call t then undef_const else t;
9296ebf40db0 tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents: 54206
diff changeset
   920
      fun rewrite_cont bound_Ts t =
55969
8820ddb8f9f4 use balanced tuples in 'primcorec'
blanchet
parents: 55966
diff changeset
   921
        if has_call t then mk_tuple1_balanced bound_Ts (snd (strip_comb t)) else undef_const;
60001
0e1b220ec4c9 generalized code
blanchet
parents: 59989
diff changeset
   922
      fun massage f _ = massage_let_if_case_corec ctxt has_call f bound_Ts rhs_term
55969
8820ddb8f9f4 use balanced tuples in 'primcorec'
blanchet
parents: 55966
diff changeset
   923
        |> abs_tuple_balanced fun_args;
53876
fabf04d43a75 simplified code
panny
parents: 53875
diff changeset
   924
    in
54207
9296ebf40db0 tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents: 54206
diff changeset
   925
      (massage rewrite_stop, massage rewrite_end, massage rewrite_cont)
54208
blanchet
parents: 54207
diff changeset
   926
    end);
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   927
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   928
fun build_corec_arg_nested_call ctxt has_call (sel_eqns : coeqn_data_sel list) sel =
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   929
  (case find_first (curry (op =) sel o #sel) sel_eqns of
54208
blanchet
parents: 54207
diff changeset
   930
    NONE => I
blanchet
parents: 54207
diff changeset
   931
  | SOME {fun_args, rhs_term, ...} =>
53899
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   932
    let
59989
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
   933
      fun massage_call bound_Ts U T t0 =
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   934
        let
59946
c18df9eea901 generalized code
blanchet
parents: 59945
diff changeset
   935
          val U2 =
c18df9eea901 generalized code
blanchet
parents: 59945
diff changeset
   936
            (case try dest_sumT U of
c18df9eea901 generalized code
blanchet
parents: 59945
diff changeset
   937
              SOME (U1, U2) => if U1 = T then U2 else invalid_map ctxt t0
c18df9eea901 generalized code
blanchet
parents: 59945
diff changeset
   938
            | NONE => invalid_map ctxt t0);
c18df9eea901 generalized code
blanchet
parents: 59945
diff changeset
   939
59948
c8860ec6fc80 generalized slightly
blanchet
parents: 59947
diff changeset
   940
          fun rewrite bound_Ts (Abs (s, T', t')) = Abs (s, T', rewrite (T' :: bound_Ts) t')
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   941
            | rewrite bound_Ts (t as _ $ _) =
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   942
              let val (u, vs) = strip_comb t in
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   943
                if is_Free u andalso has_call u then
59946
c18df9eea901 generalized code
blanchet
parents: 59945
diff changeset
   944
                  Inr_const T U2 $ mk_tuple1_balanced bound_Ts vs
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61348
diff changeset
   945
                else if try (fst o dest_Const) u = SOME @{const_name case_prod} then
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   946
                  map (rewrite bound_Ts) vs |> chop 1
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61348
diff changeset
   947
                  |>> HOLogic.mk_case_prod o the_single
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   948
                  |> Term.list_comb
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   949
                else
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   950
                  Term.list_comb (rewrite bound_Ts u, map (rewrite bound_Ts) vs)
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   951
              end
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   952
            | rewrite _ t =
59946
c18df9eea901 generalized code
blanchet
parents: 59945
diff changeset
   953
              if is_Free t andalso has_call t then Inr_const T U2 $ HOLogic.unit else t;
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   954
          in
59946
c18df9eea901 generalized code
blanchet
parents: 59945
diff changeset
   955
            rewrite bound_Ts t0
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   956
          end;
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   957
60704
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   958
      fun massage_noncall U T t =
59989
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
   959
        build_map ctxt [] (uncurry Inl_const o dest_sumT o snd) (T, U) $ t;
59947
09317aff0ff9 generalized code
blanchet
parents: 59946
diff changeset
   960
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   961
      val bound_Ts = List.rev (map fastype_of fun_args);
53899
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   962
    in
59989
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
   963
      fn t =>
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
   964
      rhs_term
60704
fdd965b35bcd tuned ML signature (and rationalized code a bit)
blanchet
parents: 60683
diff changeset
   965
      |> massage_nested_corec_call ctxt has_call massage_call (K massage_noncall) bound_Ts
59989
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
   966
        (range_type (fastype_of t)) (fastype_of1 (bound_Ts, rhs_term))
7b80ddb65e3e tuned signature
blanchet
parents: 59948
diff changeset
   967
      |> abs_tuple_balanced fun_args
54208
blanchet
parents: 54207
diff changeset
   968
    end);
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   969
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   970
fun build_corec_args_sel ctxt has_call (all_sel_eqns : coeqn_data_sel list)
54002
01c8f9d3b084 made SML/NJ happy
blanchet
parents: 54001
diff changeset
   971
    (ctr_spec : corec_ctr_spec) =
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   972
  (case filter (curry (op =) (#ctr ctr_spec) o #ctr) all_sel_eqns of
54208
blanchet
parents: 54207
diff changeset
   973
    [] => I
blanchet
parents: 54207
diff changeset
   974
  | sel_eqns =>
blanchet
parents: 54207
diff changeset
   975
    let
blanchet
parents: 54207
diff changeset
   976
      val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec;
blanchet
parents: 54207
diff changeset
   977
      val no_calls' = map_filter (try (apsnd (fn No_Corec n => n))) sel_call_list;
blanchet
parents: 54207
diff changeset
   978
      val mutual_calls' = map_filter (try (apsnd (fn Mutual_Corec n => n))) sel_call_list;
blanchet
parents: 54207
diff changeset
   979
      val nested_calls' = map_filter (try (apsnd (fn Nested_Corec n => n))) sel_call_list;
blanchet
parents: 54207
diff changeset
   980
    in
blanchet
parents: 54207
diff changeset
   981
      I
blanchet
parents: 54207
diff changeset
   982
      #> fold (fn (sel, n) => nth_map n (build_corec_arg_no_call sel_eqns sel)) no_calls'
blanchet
parents: 54207
diff changeset
   983
      #> fold (fn (sel, (q, g, h)) =>
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   984
        let val (fq, fg, fh) = build_corec_args_mutual_call ctxt has_call sel_eqns sel in
54208
blanchet
parents: 54207
diff changeset
   985
          nth_map q fq o nth_map g fg o nth_map h fh end) mutual_calls'
blanchet
parents: 54207
diff changeset
   986
      #> fold (fn (sel, n) => nth_map n
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
   987
        (build_corec_arg_nested_call ctxt has_call sel_eqns sel)) nested_calls'
54208
blanchet
parents: 54207
diff changeset
   988
    end);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   989
59673
blanchet
parents: 59662
diff changeset
   990
fun build_defs ctxt bs mxs has_call arg_Tss (corec_specs : corec_spec list)
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   991
    (disc_eqnss : coeqn_data_disc list list) (sel_eqnss : coeqn_data_sel list list) =
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   992
  let
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   993
    val corecs = map #corec corec_specs;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   994
    val ctr_specss = map #ctr_specs corec_specs;
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   995
    val corec_args = hd corecs
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   996
      |> fst o split_last o binder_types o fastype_of
59044
c04eccae1de8 tuned whitespace
blanchet
parents: 59043
diff changeset
   997
      |> map (fn T =>
c04eccae1de8 tuned whitespace
blanchet
parents: 59043
diff changeset
   998
          if range_type T = HOLogic.boolT then Abs (Name.uu_, domain_type T, @{term False})
54806
a0f024caa04c pass auto-proved exhaustiveness properties to tactic;
panny
parents: 54628
diff changeset
   999
          else Const (@{const_name undefined}, T))
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1000
      |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
  1001
      |> fold2 (fold o build_corec_args_sel ctxt has_call) sel_eqnss ctr_specss;
59041
2a23235632b2 careful with de Bruijn indices
blanchet
parents: 58634
diff changeset
  1002
59599
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
  1003
    val bad = fold (add_extra_frees ctxt [] []) corec_args [];
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
  1004
    val _ = null bad orelse
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
  1005
      (if exists has_call corec_args then nonprimitive_corec ctxt []
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
  1006
       else extra_variable ctxt [] (hd bad));
6a7e11fc6ee2 better primcorec messages
blanchet
parents: 59598
diff changeset
  1007
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
  1008
    val excludess' =
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1009
      disc_eqnss
53822
6304b12c7627 add "primcorec" command (cf. ae7f50e70c09)
panny
parents: 53811
diff changeset
  1010
      |> map (map (fn x => (#fun_args x, #ctr_no x, #prems x, #auto_gen x))
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1011
        #> fst o (fn xs => fold_map (fn x => fn ys => ((x, ys), ys @ [x])) xs [])
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1012
        #> maps (uncurry (map o pair)
53822
6304b12c7627 add "primcorec" command (cf. ae7f50e70c09)
panny
parents: 53811
diff changeset
  1013
          #> map (fn ((fun_args, c, x, a), (_, c', y, a')) =>
54068
447354985f6a generate optimized DNF formula
blanchet
parents: 54067
diff changeset
  1014
              ((c, c', a orelse a'), (x, s_not (s_conjs y)))
57527
1b07ca054327 add helper function map_prod
desharna
parents: 57399
diff changeset
  1015
            ||> map_prod (map HOLogic.mk_Trueprop) HOLogic.mk_Trueprop
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1016
            ||> Logic.list_implies
55342
blanchet
parents: 55341
diff changeset
  1017
            ||> curry Logic.list_all (map dest_Free fun_args))));
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
  1018
  in
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
  1019
    map (Term.list_comb o rpair corec_args) corecs
59873
2d929c178283 simplified code
blanchet
parents: 59859
diff changeset
  1020
    |> map2 abs_curried_balanced arg_Tss
59598
c9d304d6ae98 more 'primcorec' error handling
blanchet
parents: 59597
diff changeset
  1021
    |> (fn ts => Syntax.check_terms ctxt ts
c9d304d6ae98 more 'primcorec' error handling
blanchet
parents: 59597
diff changeset
  1022
      handle ERROR _ => nonprimitive_corec ctxt [])
61760
1647bb489522 tuned whitespace
blanchet
parents: 61424
diff changeset
  1023
    |> @{map 3} (fn b => fn mx => fn t =>
1647bb489522 tuned whitespace
blanchet
parents: 61424
diff changeset
  1024
      ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t))) bs mxs
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
  1025
    |> rpair excludess'
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
  1026
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
  1027
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
  1028
fun mk_actual_disc_eqns fun_binding arg_Ts exhaustive ({ctr_specs, ...} : corec_spec)
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
  1029
    (sel_eqns : coeqn_data_sel list) (disc_eqns : coeqn_data_disc list) =
59603
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1030
  let
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1031
    val fun_name = Binding.name_of fun_binding;
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1032
    val num_disc_eqns = length disc_eqns;
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1033
    val num_ctrs = length ctr_specs;
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1034
  in
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1035
    if (exhaustive andalso num_disc_eqns <> 0) orelse num_disc_eqns <> num_ctrs - 1 then
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1036
      (num_disc_eqns > 0 orelse error ("Missing discriminator formula for " ^ quote fun_name);
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1037
       disc_eqns)
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
  1038
    else
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
  1039
      let
59603
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1040
        val ctr_no = 0 upto length ctr_specs
55342
blanchet
parents: 55341
diff changeset
  1041
          |> the o find_first (fn j => not (exists (curry (op =) j o #ctr_no) disc_eqns));
59603
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1042
        val {ctr, disc, ...} = nth ctr_specs ctr_no;
58393
blanchet
parents: 58387
diff changeset
  1043
        val sel_eqn_opt = find_first (equal ctr o #ctr) sel_eqns;
blanchet
parents: 58387
diff changeset
  1044
blanchet
parents: 58387
diff changeset
  1045
        val fun_T = arg_Ts ---> body_type (fastype_of (#ctr (hd ctr_specs)));
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
  1046
        val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns)
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
  1047
          |> the_default (map (curry Free Name.uu) arg_Ts) o merge_options;
58393
blanchet
parents: 58387
diff changeset
  1048
        val prems = maps (s_not_conj o #prems) disc_eqns;
blanchet
parents: 58387
diff changeset
  1049
        val ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE;
blanchet
parents: 58387
diff changeset
  1050
        val code_rhs_opt = Option.map #code_rhs_opt sel_eqn_opt |> the_default NONE;
61760
1647bb489522 tuned whitespace
blanchet
parents: 61424
diff changeset
  1051
        val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt
1647bb489522 tuned whitespace
blanchet
parents: 61424
diff changeset
  1052
          |> the_default 100000; (* FIXME *)
58393
blanchet
parents: 58387
diff changeset
  1053
blanchet
parents: 58387
diff changeset
  1054
        val extra_disc_eqn =
59603
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1055
          {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = ctr_no,
58393
blanchet
parents: 58387
diff changeset
  1056
           disc = disc, prems = prems, auto_gen = true, ctr_rhs_opt = ctr_rhs_opt,
blanchet
parents: 58387
diff changeset
  1057
           code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos, user_eqn = undef_const};
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
  1058
      in
59603
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1059
        chop ctr_no disc_eqns ||> cons extra_disc_eqn |> op @
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
  1060
      end
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
  1061
  end;
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1062
55100
697b41533e1a made SML/NJ happier
blanchet
parents: 55061
diff changeset
  1063
fun find_corec_calls ctxt has_call (basic_ctr_specs : basic_corec_ctr_spec list)
697b41533e1a made SML/NJ happier
blanchet
parents: 55061
diff changeset
  1064
    ({ctr, sel, rhs_term, ...} : coeqn_data_sel) =
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1065
  let
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
  1066
    val sel_no = find_first (curry (op =) ctr o #ctr) basic_ctr_specs
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
  1067
      |> find_index (curry (op =) sel) o #sels o the;
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1068
  in
55341
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
  1069
    K (if has_call rhs_term then fold_rev_let_if_case ctxt (K cons) [] rhs_term [] else [])
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
  1070
    |> nth_map sel_no |> AList.map_entry (op =) ctr
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1071
  end;
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1072
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1073
fun applied_fun_of fun_name fun_T fun_args =
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
  1074
  Term.list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1075
54921
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1076
fun is_trivial_implies thm =
54967
78de75e3e52a exhaustive rules like '(False ==> P) ==> P ==> P' are now filtered out as trivial
blanchet
parents: 54959
diff changeset
  1077
  uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm));
54921
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1078
60003
ba8fa0c38d66 renamed ML funs
blanchet
parents: 60001
diff changeset
  1079
fun primcorec_ursive auto opts fixes specs of_specs_opt lthy =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
  1080
  let
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
  1081
    val thy = Proof_Context.theory_of lthy;
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
  1082
53352
43a1cc050943 honor mixfix specifications
traytel
parents: 53341
diff changeset
  1083
    val (bs, mxs) = map_split (apfst fst) fixes;
55969
8820ddb8f9f4 use balanced tuples in 'primcorec'
blanchet
parents: 55966
diff changeset
  1084
    val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
  1085
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56152
diff changeset
  1086
    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ arg_Ts) of
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
  1087
        [] => ()
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
  1088
      | (b, _) :: _ => error ("Type of " ^ Binding.print b ^ " contains top sort"));
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
  1089
54902
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
  1090
    val actual_nn = length bs;
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
  1091
59281
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
  1092
    val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
  1093
      |> the_default Plugin_Name.default_filter;
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
  1094
    val sequentials = replicate actual_nn (exists (can (fn Sequential_Option => ())) opts);
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
  1095
    val exhaustives = replicate actual_nn (exists (can (fn Exhaustive_Option => ())) opts);
1b4dc8a9f7d9 added plugins syntax to prim(co)rec
blanchet
parents: 59279
diff changeset
  1096
    val transfers = replicate actual_nn (exists (can (fn Transfer_Option => ())) opts);
54591
c822230fd22b prevent exception when equations for a function are missing;
panny
parents: 54279
diff changeset
  1097
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1098
    val fun_names = map Binding.name_of bs;
62497
5b5b704f4811 respect qualification when noting theorems in prim(co)rec
traytel
parents: 62318
diff changeset
  1099
    val qualifys = map (fold_rev (uncurry Binding.qualify o swap) o Binding.path_of) bs;
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1100
    val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts;
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
  1101
    val frees = map (fst #>> Binding.name_of #> Free) fixes;
59594
43f0c669302d reworked primcorec error messages
blanchet
parents: 59582
diff changeset
  1102
    val has_call = Term.exists_subterm (member (op =) frees);
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1103
    val eqns_data =
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
  1104
      @{fold_map 2} (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss)
55871
a28817253b31 removed (co)iterators from documentation
blanchet
parents: 55870
diff changeset
  1105
        (tag_list 0 (map snd specs)) of_specs_opt []
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1106
      |> flat o fst;
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1107
59662
blanchet
parents: 59612
diff changeset
  1108
    val missing = fun_names
blanchet
parents: 59612
diff changeset
  1109
      |> filter (map (fn Disc x => #fun_name x | Sel x => #fun_name x) eqns_data
blanchet
parents: 59612
diff changeset
  1110
        |> not oo member (op =));
blanchet
parents: 59612
diff changeset
  1111
    val _ = null missing orelse error ("Missing equations for " ^ commas missing);
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
  1112
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1113
    val callssss =
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1114
      map_filter (try (fn Sel x => x)) eqns_data
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 59044
diff changeset
  1115
      |> partition_eq (op = o apply2 #fun_name)
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1116
      |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
54161
panny
parents: 54160 54159
diff changeset
  1117
      |> map (flat o snd)
54243
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54239
diff changeset
  1118
      |> map2 (fold o find_corec_calls lthy has_call) basic_ctr_specss
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1119
      |> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} =>
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1120
        (ctr, map (K []) sels))) basic_ctr_specss);
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1121
59603
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1122
    val (corec_specs0, _, coinduct_thm, coinduct_strong_thm, coinduct_thms, coinduct_strong_thms,
61334
8d40ddaa427f collect the names from goals in favor of fragile exports
traytel
parents: 61301
diff changeset
  1123
         (coinduct_attrs, common_coinduct_attrs), n2m, lthy) =
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
  1124
      corec_specs_of bs arg_Ts res_Ts frees callssss lthy;
59603
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1125
    val corec_specs = take actual_nn corec_specs0;
54178
d6dc359426b7 more informative abort
blanchet
parents: 54177
diff changeset
  1126
    val ctr_specss = map #ctr_specs corec_specs;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
  1127
59603
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1128
    val disc_eqnss0 = map_filter (try (fn Disc x => x)) eqns_data
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 59044
diff changeset
  1129
      |> partition_eq (op = o apply2 #fun_name)
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1130
      |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 59044
diff changeset
  1131
      |> map (sort (op < o apply2 #ctr_no |> make_ord) o flat o snd);
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
  1132
59603
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1133
    val _ = disc_eqnss0 |> map (fn x =>
59602
2a6226d89fa3 more primcorec messages
blanchet
parents: 59601
diff changeset
  1134
      let val dups = duplicates (op = o apply2 #ctr_no) x in
2a6226d89fa3 more primcorec messages
blanchet
parents: 59601
diff changeset
  1135
        null dups orelse
59600
1716da11a11c more precise primcorec messages
blanchet
parents: 59599
diff changeset
  1136
        error_at lthy
59602
2a6226d89fa3 more primcorec messages
blanchet
parents: 59601
diff changeset
  1137
          (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) dups
59600
1716da11a11c more precise primcorec messages
blanchet
parents: 59599
diff changeset
  1138
           |> map (fn {ctr_rhs_opt = SOME t, ...} => t | {user_eqn, ...} => user_eqn))
59606
blanchet
parents: 59605
diff changeset
  1139
          "Overspecified case(s)"
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 59044
diff changeset
  1140
      end);
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1141
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1142
    val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 59044
diff changeset
  1143
      |> partition_eq (op = o apply2 #fun_name)
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1144
      |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1145
      |> map (flat o snd);
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1146
59602
2a6226d89fa3 more primcorec messages
blanchet
parents: 59601
diff changeset
  1147
    val _ = sel_eqnss |> map (fn x =>
2a6226d89fa3 more primcorec messages
blanchet
parents: 59601
diff changeset
  1148
      let val dups = duplicates (op = o apply2 ctr_sel_of) x in
2a6226d89fa3 more primcorec messages
blanchet
parents: 59601
diff changeset
  1149
        null dups orelse
2a6226d89fa3 more primcorec messages
blanchet
parents: 59601
diff changeset
  1150
        error_at lthy
2a6226d89fa3 more primcorec messages
blanchet
parents: 59601
diff changeset
  1151
          (maps (fn t => filter (curry (op =) (ctr_sel_of t) o ctr_sel_of) x) dups
2a6226d89fa3 more primcorec messages
blanchet
parents: 59601
diff changeset
  1152
           |> map (fn {ctr_rhs_opt = SOME t, ...} => t | {user_eqn, ...} => user_eqn))
59606
blanchet
parents: 59605
diff changeset
  1153
          "Overspecified case(s)"
59602
2a6226d89fa3 more primcorec messages
blanchet
parents: 59601
diff changeset
  1154
      end);
2a6226d89fa3 more primcorec messages
blanchet
parents: 59601
diff changeset
  1155
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
  1156
    val arg_Tss = map (binder_types o snd o fst) fixes;
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
  1157
    val disc_eqnss = @{map 6} mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss
59603
427511b3d575 better primcorec messages
blanchet
parents: 59602
diff changeset
  1158
      disc_eqnss0;
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
  1159
    val (defs, excludess') =
61334
8d40ddaa427f collect the names from goals in favor of fragile exports
traytel
parents: 61301
diff changeset
  1160
      build_defs lthy bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1161
55009
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1162
    val tac_opts =
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1163
      map (fn {code_rhs_opt, ...} :: _ =>
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1164
        if auto orelse is_some code_rhs_opt then SOME (auto_tac o #context) else NONE) disc_eqnss;
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1165
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1166
    fun exclude_tac tac_opt sequential (c, c', a) =
54901
0b8871677e0b use same name for feature internally as in user interface, to facilitate grepping
blanchet
parents: 54900
diff changeset
  1167