src/HOL/Tools/inductive_codegen.ML
author bulwahn
Fri, 03 Dec 2010 08:40:47 +0100
changeset 40905 647142607448
parent 40132 7ee65dbffa31
child 40911 7febf76e0a69
permissions -rw-r--r--
only handle TimeOut exception if used interactively
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24584
01e83ffa6c54 fixed title
haftmann
parents: 24458
diff changeset
     1
(*  Title:      HOL/Tools/inductive_codegen.ML
11539
0f17da240450 tuned headers;
wenzelm
parents: 11537
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
     3
11539
0f17da240450 tuned headers;
wenzelm
parents: 11537
diff changeset
     4
Code generator for inductive predicates.
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
     5
*)
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
     6
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
     7
signature INDUCTIVE_CODEGEN =
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
     8
sig
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
     9
  val add : string option -> int option -> attribute
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
    10
  val test_fn : (int * int * int -> term list option) Unsynchronized.ref
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35021
diff changeset
    11
  val test_term:
39253
0c47d615a69b removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents: 39252
diff changeset
    12
    Proof.context -> term -> int -> term list option * (bool list * bool)
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18388
diff changeset
    13
  val setup : theory -> theory
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
    14
  val quickcheck_setup : theory -> theory
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
    15
end;
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
    16
37390
8781d80026fc moved inductive_codegen to place where product type is available; tuned structure name
haftmann
parents: 37198
diff changeset
    17
structure Inductive_Codegen : INDUCTIVE_CODEGEN =
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
    18
struct
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
    19
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
    20
open Codegen;
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
    21
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
    22
(**** theory data ****)
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
    23
18930
29d39c10822e replaced Symtab.merge_multi by local merge_rules;
wenzelm
parents: 18928
diff changeset
    24
fun merge_rules tabs =
22642
bfdb29f11eb4 canonical merge operations
haftmann
parents: 22556
diff changeset
    25
  Symtab.join (fn _ => AList.merge (Thm.eq_thm_prop) (K true)) tabs;
18930
29d39c10822e replaced Symtab.merge_multi by local merge_rules;
wenzelm
parents: 18928
diff changeset
    26
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33338
diff changeset
    27
structure CodegenData = Theory_Data
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22791
diff changeset
    28
(
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
    29
  type T =
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    30
    {intros : (thm * (string * int)) list Symtab.table,
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
    31
     graph : unit Graph.T,
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    32
     eqns : (thm * string) list Symtab.table};
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
    33
  val empty =
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
    34
    {intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty};
16424
18a07ad8fea8 accomodate change of TheoryDataFun;
wenzelm
parents: 15660
diff changeset
    35
  val extend = I;
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33338
diff changeset
    36
  fun merge ({intros=intros1, graph=graph1, eqns=eqns1},
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33338
diff changeset
    37
    {intros=intros2, graph=graph2, eqns=eqns2}) : T =
18930
29d39c10822e replaced Symtab.merge_multi by local merge_rules;
wenzelm
parents: 18928
diff changeset
    38
    {intros = merge_rules (intros1, intros2),
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
    39
     graph = Graph.merge (K true) (graph1, graph2),
18930
29d39c10822e replaced Symtab.merge_multi by local merge_rules;
wenzelm
parents: 18928
diff changeset
    40
     eqns = merge_rules (eqns1, eqns2)};
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22791
diff changeset
    41
);
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
    42
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
    43
37390
8781d80026fc moved inductive_codegen to place where product type is available; tuned structure name
haftmann
parents: 37198
diff changeset
    44
fun warn thm = warning ("Inductive_Codegen: Not a proper clause:\n" ^
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 31998
diff changeset
    45
  Display.string_of_thm_without_context thm);
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
    46
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
    47
fun add_node x g = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
14162
f05f299512e9 Fixed problem with "code ind" attribute that caused code generator to
berghofe
parents: 13105
diff changeset
    48
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    49
fun add optmod optnparms = Thm.declaration_attribute (fn thm => Context.mapping (fn thy =>
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    50
  let
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    51
    val {intros, graph, eqns} = CodegenData.get thy;
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    52
    fun thyname_of s = (case optmod of
27398
768da1da59d6 simplified retrieval of theory names of consts and types
haftmann
parents: 26975
diff changeset
    53
      NONE => Codegen.thyname_of_const thy s | SOME s => s);
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    54
  in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38329
diff changeset
    55
      SOME (Const (@{const_name HOL.eq}, _), [t, _]) =>
35364
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
    56
        (case head_of t of
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
    57
          Const (s, _) =>
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
    58
            CodegenData.put {intros = intros, graph = graph,
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
    59
               eqns = eqns |> Symtab.map_default (s, [])
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
    60
                 (AList.update Thm.eq_thm_prop (thm, thyname_of s))} thy
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
    61
        | _ => (warn thm; thy))
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    62
    | SOME (Const (s, _), _) =>
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    63
        let
29287
5b0bfd63b5da eliminated OldTerm.(add_)term_consts;
wenzelm
parents: 29270
diff changeset
    64
          val cs = fold Term.add_const_names (Thm.prems_of thm) [];
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    65
          val rules = Symtab.lookup_list intros s;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    66
          val nparms = (case optnparms of
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    67
            SOME k => k
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    68
          | NONE => (case rules of
36610
bafd82950e24 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents: 36001
diff changeset
    69
             [] => (case try (Inductive.the_inductive (ProofContext.init_global thy)) s of
22791
992222f3d2eb Moved function params_of to inductive_package.ML.
berghofe
parents: 22661
diff changeset
    70
                 SOME (_, {raw_induct, ...}) =>
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 30190
diff changeset
    71
                   length (Inductive.params_of raw_induct)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    72
               | NONE => 0)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    73
            | xs => snd (snd (snd (split_last xs)))))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    74
        in CodegenData.put
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    75
          {intros = intros |>
22642
bfdb29f11eb4 canonical merge operations
haftmann
parents: 22556
diff changeset
    76
           Symtab.update (s, (AList.update Thm.eq_thm_prop
bfdb29f11eb4 canonical merge operations
haftmann
parents: 22556
diff changeset
    77
             (thm, (thyname_of s, nparms)) rules)),
33338
de76079f973a eliminated some old folds;
wenzelm
parents: 33317
diff changeset
    78
           graph = fold_rev (Graph.add_edge o pair s) cs (fold add_node (s :: cs) graph),
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    79
           eqns = eqns} thy
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    80
        end
18728
6790126ab5f6 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    81
    | _ => (warn thm; thy))
20897
3f8d2834b2c4 attribute: Context.mapping;
wenzelm
parents: 20071
diff changeset
    82
  end) I);
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
    83
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
    84
fun get_clauses thy s =
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
    85
  let val {intros, graph, ...} = CodegenData.get thy
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17261
diff changeset
    86
  in case Symtab.lookup intros s of
36610
bafd82950e24 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents: 36001
diff changeset
    87
      NONE => (case try (Inductive.the_inductive (ProofContext.init_global thy)) s of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15257
diff changeset
    88
        NONE => NONE
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
    89
      | SOME ({names, ...}, {intrs, raw_induct, ...}) =>
27398
768da1da59d6 simplified retrieval of theory names of consts and types
haftmann
parents: 26975
diff changeset
    90
          SOME (names, Codegen.thyname_of_const thy s,
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 30190
diff changeset
    91
            length (Inductive.params_of raw_induct),
22661
f3ba63a2663e Removed erroneous application of rev in get_clauses that caused
berghofe
parents: 22642
diff changeset
    92
            preprocess thy intrs))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15257
diff changeset
    93
    | SOME _ =>
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    94
        let
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
    95
          val SOME names = find_first
22642
bfdb29f11eb4 canonical merge operations
haftmann
parents: 22556
diff changeset
    96
            (fn xs => member (op =) xs s) (Graph.strong_conn graph);
bfdb29f11eb4 canonical merge operations
haftmann
parents: 22556
diff changeset
    97
          val intrs as (_, (thyname, nparms)) :: _ =
bfdb29f11eb4 canonical merge operations
haftmann
parents: 22556
diff changeset
    98
            maps (the o Symtab.lookup intros) names;
bfdb29f11eb4 canonical merge operations
haftmann
parents: 22556
diff changeset
    99
        in SOME (names, thyname, nparms, preprocess thy (map fst (rev intrs))) end
14162
f05f299512e9 Fixed problem with "code ind" attribute that caused code generator to
berghofe
parents: 13105
diff changeset
   100
  end;
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   101
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   102
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   103
(**** check if a term contains only constructor functions ****)
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   104
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   105
fun is_constrt thy =
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   106
  let
31784
bd3486c57ba3 tuned interfaces of datatype module
haftmann
parents: 31723
diff changeset
   107
    val cnstrs = flat (maps
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   108
      (map (fn (_, (_, _, cs)) => map (apsnd length) cs) o #descr o snd)
33963
977b94b64905 renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33771
diff changeset
   109
      (Symtab.dest (Datatype_Data.get_all thy)));
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   110
    fun check t = (case strip_comb t of
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   111
        (Var _, []) => true
17521
0f1c48de39f5 introduced AList module in favor of assoc etc.
haftmann
parents: 17412
diff changeset
   112
      | (Const (s, _), ts) => (case AList.lookup (op =) cnstrs s of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15257
diff changeset
   113
            NONE => false
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15257
diff changeset
   114
          | SOME i => length ts = i andalso forall check ts)
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   115
      | _ => false)
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   116
  in check end;
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   117
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   118
(**** check if a type is an equality type (i.e. doesn't contain fun) ****)
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   119
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   120
fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   121
  | is_eqT _ = true;
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   122
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   123
(**** mode inference ****)
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   124
15204
d15f85347fcb - Inserted additional check for equality types in check_mode_clause that
berghofe
parents: 15126
diff changeset
   125
fun string_of_mode (iss, is) = space_implode " -> " (map
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15257
diff changeset
   126
  (fn NONE => "X"
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15257
diff changeset
   127
    | SOME js => enclose "[" "]" (commas (map string_of_int js)))
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15257
diff changeset
   128
       (iss @ [SOME is]));
15204
d15f85347fcb - Inserted additional check for equality types in check_mode_clause that
berghofe
parents: 15126
diff changeset
   129
d15f85347fcb - Inserted additional check for equality types in check_mode_clause that
berghofe
parents: 15126
diff changeset
   130
fun print_modes modes = message ("Inferred modes:\n" ^
26931
aa226d8405a8 cat_lines;
wenzelm
parents: 26928
diff changeset
   131
  cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   132
    (fn (m, rnd) => string_of_mode m ^
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   133
       (if rnd then " (random)" else "")) ms)) modes));
15204
d15f85347fcb - Inserted additional check for equality types in check_mode_clause that
berghofe
parents: 15126
diff changeset
   134
29265
5b4247055bd7 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents: 28537
diff changeset
   135
val term_vs = map (fst o fst o dest_Var) o OldTerm.term_vars;
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32342
diff changeset
   136
val terms_vs = distinct (op =) o maps term_vs;
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   137
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   138
(** collect all Vars in a term (with duplicates!) **)
16861
7446b4be013b tuned fold on terms;
wenzelm
parents: 16645
diff changeset
   139
fun term_vTs tm =
7446b4be013b tuned fold on terms;
wenzelm
parents: 16645
diff changeset
   140
  fold_aterms (fn Var ((x, _), T) => cons (x, T) | _ => I) tm [];
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   141
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   142
fun get_args _ _ [] = ([], [])
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36610
diff changeset
   143
  | get_args is i (x::xs) = (if member (op =) is i then apfst else apsnd) (cons x)
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   144
      (get_args is (i+1) xs);
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   145
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   146
fun merge xs [] = xs
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   147
  | merge [] ys = ys
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   148
  | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys)
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   149
      else y::merge (x::xs) ys;
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   150
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   151
fun subsets i j = if i <= j then
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   152
       let val is = subsets (i+1) j
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   153
       in merge (map (fn ks => i::ks) is) is end
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   154
     else [[]];
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   155
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   156
fun cprod ([], ys) = []
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   157
  | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   158
30190
479806475f3c use long names for old-style fold combinators;
wenzelm
parents: 29287
diff changeset
   159
fun cprods xss = List.foldr (map op :: o cprod) [[]] xss;
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   160
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   161
datatype mode = Mode of ((int list option list * int list) * bool) * int list * mode option list;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   162
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   163
fun needs_random (Mode ((_, b), _, ms)) =
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   164
  b orelse exists (fn NONE => false | SOME m => needs_random m) ms;
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   165
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   166
fun modes_of modes t =
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   167
  let
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   168
    val ks = 1 upto length (binder_types (fastype_of t));
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   169
    val default = [Mode ((([], ks), false), ks, [])];
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32342
diff changeset
   170
    fun mk_modes name args = Option.map
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   171
     (maps (fn (m as ((iss, is), _)) =>
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   172
        let
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   173
          val (args1, args2) =
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   174
            if length args < length iss then
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   175
              error ("Too few arguments for inductive predicate " ^ name)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   176
            else chop (length iss) args;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   177
          val k = length args2;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   178
          val prfx = 1 upto k
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   179
        in
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   180
          if not (is_prefix op = prfx is) then [] else
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   181
          let val is' = map (fn i => i - k) (List.drop (is, k))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   182
          in map (fn x => Mode (m, is', x)) (cprods (map
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   183
            (fn (NONE, _) => [NONE]
33317
b4534348b8fd standardized filter/filter_out;
wenzelm
parents: 33244
diff changeset
   184
              | (SOME js, arg) => map SOME (filter
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   185
                  (fn Mode (_, js', _) => js=js') (modes_of modes arg)))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   186
                    (iss ~~ args1)))
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   187
          end
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   188
        end)) (AList.lookup op = modes name)
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   189
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   190
  in (case strip_comb t of
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38329
diff changeset
   191
      (Const (@{const_name HOL.eq}, Type (_, [T, _])), _) =>
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   192
        [Mode ((([], [1]), false), [1], []), Mode ((([], [2]), false), [2], [])] @
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   193
        (if is_eqT T then [Mode ((([], [1, 2]), false), [1, 2], [])] else [])
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   194
    | (Const (name, _), args) => the_default default (mk_modes name args)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   195
    | (Var ((name, _), _), args) => the (mk_modes name args)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   196
    | (Free (name, _), args) => the (mk_modes name args)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   197
    | _ => default)
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   198
  end;
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   199
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 24625
diff changeset
   200
datatype indprem = Prem of term list * term * bool | Sidecond of term;
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   201
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   202
fun missing_vars vs ts = subtract (fn (x, ((y, _), _)) => x = y) vs
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   203
  (fold Term.add_vars ts []);
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   204
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   205
fun monomorphic_vars vs = null (fold (Term.add_tvarsT o snd) vs []);
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   206
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   207
fun mode_ord p = int_ord (pairself (fn (Mode ((_, rnd), _, _), vs) =>
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   208
  length vs + (if null vs then 0 else 1) + (if rnd then 1 else 0)) p);
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   209
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   210
fun select_mode_prem thy modes vs ps =
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   211
  sort (mode_ord o pairself (hd o snd))
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   212
    (filter_out (null o snd) (ps ~~ map
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   213
      (fn Prem (us, t, is_set) => sort mode_ord
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   214
          (List.mapPartial (fn m as Mode (_, is, _) =>
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   215
            let
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   216
              val (in_ts, out_ts) = get_args is 1 us;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   217
              val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   218
              val vTs = maps term_vTs out_ts';
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   219
              val dupTs = map snd (duplicates (op =) vTs) @
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   220
                map_filter (AList.lookup (op =) vTs) vs;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   221
              val missing_vs = missing_vars vs (t :: in_ts @ in_ts')
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   222
            in
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   223
              if forall (is_eqT o fastype_of) in_ts' andalso forall is_eqT dupTs
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   224
                andalso monomorphic_vars missing_vs
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   225
              then SOME (m, missing_vs)
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   226
              else NONE
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   227
            end)
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   228
              (if is_set then [Mode ((([], []), false), [], [])]
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   229
               else modes_of modes t handle Option =>
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   230
                 error ("Bad predicate: " ^ Syntax.string_of_term_global thy t)))
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   231
        | Sidecond t =>
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   232
            let val missing_vs = missing_vars vs [t]
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   233
            in
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   234
              if monomorphic_vars missing_vs
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   235
              then [(Mode ((([], []), false), [], []), missing_vs)]
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   236
              else []
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   237
            end)
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   238
              ps));
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   239
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36610
diff changeset
   240
fun use_random () = member (op =) (!Codegen.mode) "random_ind";
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   241
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   242
fun check_mode_clause thy arg_vs modes ((iss, is), rnd) (ts, ps) =
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   243
  let
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32342
diff changeset
   244
    val modes' = modes @ map_filter
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   245
      (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)]))
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   246
        (arg_vs ~~ iss);
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   247
    fun check_mode_prems vs rnd [] = SOME (vs, rnd)
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   248
      | check_mode_prems vs rnd ps = (case select_mode_prem thy modes' vs ps of
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   249
          (x, (m, []) :: _) :: _ => check_mode_prems
33042
ddf1f03a9ad9 curried union as canonical list operation
haftmann
parents: 33038
diff changeset
   250
            (case x of Prem (us, _, _) => union (op =) vs (terms_vs us) | _ => vs)
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   251
            (rnd orelse needs_random m)
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   252
            (filter_out (equal x) ps)
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   253
        | (_, (_, vs') :: _) :: _ =>
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   254
            if use_random () then
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   255
              check_mode_prems (union (op =) vs (map (fst o fst) vs')) true ps
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   256
            else NONE
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   257
        | _ => NONE);
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   258
    val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts));
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   259
    val in_vs = terms_vs in_ts;
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   260
  in
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   261
    if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   262
      forall (is_eqT o fastype_of) in_ts'
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   263
    then (case check_mode_prems (union (op =) arg_vs in_vs) rnd ps of
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   264
       NONE => NONE
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   265
     | SOME (vs, rnd') =>
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   266
         let val missing_vs = missing_vars vs ts
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   267
         in
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   268
           if null missing_vs orelse
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   269
             use_random () andalso monomorphic_vars missing_vs
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   270
           then SOME (rnd' orelse not (null missing_vs))
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   271
           else NONE
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   272
         end)
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   273
    else NONE
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   274
  end;
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   275
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   276
fun check_modes_pred thy arg_vs preds modes (p, ms) =
17521
0f1c48de39f5 introduced AList module in favor of assoc etc.
haftmann
parents: 17412
diff changeset
   277
  let val SOME rs = AList.lookup (op =) preds p
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   278
  in (p, List.mapPartial (fn m as (m', _) =>
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   279
    let val xs = map (check_mode_clause thy arg_vs modes m) rs
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   280
    in case find_index is_none xs of
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   281
        ~1 => SOME (m', exists (fn SOME b => b) xs)
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   282
      | i => (message ("Clause " ^ string_of_int (i+1) ^ " of " ^
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   283
        p ^ " violates mode " ^ string_of_mode m'); NONE)
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   284
    end) ms)
15204
d15f85347fcb - Inserted additional check for equality types in check_mode_clause that
berghofe
parents: 15126
diff changeset
   285
  end;
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   286
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   287
fun fixp f (x : (string * ((int list option list * int list) * bool) list) list) =
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   288
  let val y = f x
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   289
  in if x = y then x else fixp f y end;
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   290
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   291
fun infer_modes thy extra_modes arities arg_vs preds = fixp (fn modes =>
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   292
  map (check_modes_pred thy arg_vs preds (modes @ extra_modes)) modes)
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   293
    (map (fn (s, (ks, k)) => (s, map (rpair false) (cprod (cprods (map
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15257
diff changeset
   294
      (fn NONE => [NONE]
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   295
        | SOME k' => map SOME (subsets 1 k')) ks),
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   296
      subsets 1 k)))) arities);
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   297
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   298
(**** code generation ****)
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   299
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   300
fun mk_eq (x::xs) =
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   301
  let fun mk_eqs _ [] = []
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   302
        | mk_eqs a (b::cs) = str (a ^ " = " ^ b) :: mk_eqs b cs
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   303
  in mk_eqs x xs end;
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   304
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   305
fun mk_tuple xs = Pretty.block (str "(" ::
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32342
diff changeset
   306
  flat (separate [str ",", Pretty.brk 1] (map single xs)) @
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   307
  [str ")"]);
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   308
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   309
fun mk_v s (names, vs) =
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   310
  (case AList.lookup (op =) vs s of
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   311
    NONE => (s, (names, (s, [s])::vs))
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   312
  | SOME xs =>
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   313
      let val s' = Name.variant names s
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   314
      in (s', (s'::names, AList.update (op =) (s, s'::xs) vs)) end);
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   315
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   316
fun distinct_v (Var ((s, 0), T)) nvs =
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   317
      let val (s', nvs') = mk_v s nvs
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   318
      in (Var ((s', 0), T), nvs') end
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   319
  | distinct_v (t $ u) nvs =
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   320
      let
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   321
        val (t', nvs') = distinct_v t nvs;
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   322
        val (u', nvs'') = distinct_v u nvs';
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   323
      in (t' $ u', nvs'') end
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   324
  | distinct_v t nvs = (t, nvs);
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   325
15061
61a52739cd82 Added simple check that allows code generator to produce code containing
berghofe
parents: 15031
diff changeset
   326
fun is_exhaustive (Var _) = true
37390
8781d80026fc moved inductive_codegen to place where product type is available; tuned structure name
haftmann
parents: 37198
diff changeset
   327
  | is_exhaustive (Const (@{const_name Pair}, _) $ t $ u) =
15061
61a52739cd82 Added simple check that allows code generator to produce code containing
berghofe
parents: 15031
diff changeset
   328
      is_exhaustive t andalso is_exhaustive u
61a52739cd82 Added simple check that allows code generator to produce code containing
berghofe
parents: 15031
diff changeset
   329
  | is_exhaustive _ = false;
61a52739cd82 Added simple check that allows code generator to produce code containing
berghofe
parents: 15031
diff changeset
   330
61a52739cd82 Added simple check that allows code generator to produce code containing
berghofe
parents: 15031
diff changeset
   331
fun compile_match nvs eq_ps out_ps success_p can_fail =
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32342
diff changeset
   332
  let val eqs = flat (separate [str " andalso", Pretty.brk 1]
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32342
diff changeset
   333
    (map single (maps (mk_eq o snd) nvs @ eq_ps)));
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   334
  in
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   335
    Pretty.block
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   336
     ([str "(fn ", mk_tuple out_ps, str " =>", Pretty.brk 1] @
37527
d9c2fdd6614f avoid equality on abstract type Pretty.T;
wenzelm
parents: 37390
diff changeset
   337
      (Pretty.block ((if null eqs then [] else str "if " ::
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   338
         [Pretty.block eqs, Pretty.brk 1, str "then "]) @
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   339
         (success_p ::
37527
d9c2fdd6614f avoid equality on abstract type Pretty.T;
wenzelm
parents: 37390
diff changeset
   340
          (if null eqs then [] else [Pretty.brk 1, str "else DSeq.empty"]))) ::
15061
61a52739cd82 Added simple check that allows code generator to produce code containing
berghofe
parents: 15031
diff changeset
   341
       (if can_fail then
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   342
          [Pretty.brk 1, str "| _ => DSeq.empty)"]
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   343
        else [str ")"])))
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   344
  end;
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   345
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   346
fun modename module s (iss, is) gr =
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38329
diff changeset
   347
  let val (id, gr') = if s = @{const_name HOL.eq} then (("", "equal"), gr)
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   348
    else mk_const_id module s gr
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   349
  in (space_implode "__"
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   350
    (mk_qual_id module id ::
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32342
diff changeset
   351
      map (space_implode "_" o map string_of_int) (map_filter I iss @ [is])), gr')
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   352
  end;
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   353
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   354
fun mk_funcomp brack s k p = (if brack then parens else I)
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   355
  (Pretty.block [Pretty.block ((if k = 0 then [] else [str "("]) @
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   356
    separate (Pretty.brk 1) (str s :: replicate k (str "|> ???")) @
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   357
    (if k = 0 then [] else [str ")"])), Pretty.brk 1, p]);
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   358
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   359
fun compile_expr thy defs dep module brack modes (NONE, t) gr =
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   360
      apfst single (invoke_codegen thy defs dep module brack t gr)
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   361
  | compile_expr _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr =
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   362
      ([str name], gr)
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   363
  | compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr =
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   364
      (case strip_comb t of
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   365
         (Const (name, _), args) =>
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38329
diff changeset
   366
           if name = @{const_name HOL.eq} orelse AList.defined op = modes name then
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   367
             let
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   368
               val (args1, args2) = chop (length ms) args;
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   369
               val ((ps, mode_id), gr') = gr |> fold_map
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   370
                   (compile_expr thy defs dep module true modes) (ms ~~ args1)
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   371
                   ||>> modename module name mode;
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   372
               val (ps', gr'') = (case mode of
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   373
                   ([], []) => ([str "()"], gr')
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   374
                 | _ => fold_map
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   375
                     (invoke_codegen thy defs dep module true) args2 gr')
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   376
             in ((if brack andalso not (null ps andalso null ps') then
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   377
               single o parens o Pretty.block else I)
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32342
diff changeset
   378
                 (flat (separate [Pretty.brk 1]
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   379
                   ([str mode_id] :: ps @ map single ps'))), gr')
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   380
             end
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   381
           else apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   382
             (invoke_codegen thy defs dep module true t gr)
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   383
       | _ => apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   384
           (invoke_codegen thy defs dep module true t gr));
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   385
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   386
fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr =
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   387
  let
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32342
diff changeset
   388
    val modes' = modes @ map_filter
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   389
      (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)]))
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   390
        (arg_vs ~~ iss);
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   391
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   392
    fun check_constrt t (names, eqs) =
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   393
      if is_constrt thy t then (t, (names, eqs))
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   394
      else
20071
8f3e1ddb50e6 replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents: 19861
diff changeset
   395
        let val s = Name.variant names "x";
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   396
        in (Var ((s, 0), fastype_of t), (s::names, (s, t)::eqs)) end;
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   397
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   398
    fun compile_eq (s, t) gr =
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   399
      apfst (Pretty.block o cons (str (s ^ " = ")) o single)
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   400
        (invoke_codegen thy defs dep module false t gr);
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   401
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   402
    val (in_ts, out_ts) = get_args is 1 ts;
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   403
    val (in_ts', (all_vs', eqs)) = fold_map check_constrt in_ts (all_vs, []);
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   404
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   405
    fun compile_prems out_ts' vs names [] gr =
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   406
          let
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   407
            val (out_ps, gr2) =
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   408
              fold_map (invoke_codegen thy defs dep module false) out_ts gr;
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   409
            val (eq_ps, gr3) = fold_map compile_eq eqs gr2;
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   410
            val (out_ts'', (names', eqs')) = fold_map check_constrt out_ts' (names, []);
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   411
            val (out_ts''', nvs) =
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   412
              fold_map distinct_v out_ts'' (names', map (fn x => (x, [x])) vs);
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   413
            val (out_ps', gr4) =
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   414
              fold_map (invoke_codegen thy defs dep module false) out_ts''' gr3;
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   415
            val (eq_ps', gr5) = fold_map compile_eq eqs' gr4;
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   416
            val vs' = distinct (op =) (flat (vs :: map term_vs out_ts'));
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   417
            val missing_vs = missing_vars vs' out_ts;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   418
            val final_p = Pretty.block
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   419
              [str "DSeq.single", Pretty.brk 1, mk_tuple out_ps]
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   420
          in
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   421
            if null missing_vs then
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   422
              (compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   423
                 final_p (exists (not o is_exhaustive) out_ts'''), gr5)
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   424
            else
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   425
              let
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   426
                val (pat_p, gr6) = invoke_codegen thy defs dep module true
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   427
                  (HOLogic.mk_tuple (map Var missing_vs)) gr5;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   428
                val gen_p = mk_gen gr6 module true [] ""
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   429
                  (HOLogic.mk_tupleT (map snd missing_vs))
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   430
              in
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   431
                (compile_match (snd nvs) eq_ps' out_ps'
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   432
                   (Pretty.block [str "DSeq.generator ", gen_p,
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   433
                      str " :->", Pretty.brk 1,
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   434
                      compile_match [] eq_ps [pat_p] final_p false])
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   435
                   (exists (not o is_exhaustive) out_ts'''),
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   436
                 gr6)
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   437
              end
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   438
          end
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   439
      | compile_prems out_ts vs names ps gr =
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   440
          let
31852
a16bb835e97d explicit Set constructor for code generated for sets
haftmann
parents: 31784
diff changeset
   441
            val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   442
            val (out_ts', (names', eqs)) = fold_map check_constrt out_ts (names, []);
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   443
            val (out_ts'', nvs) = fold_map distinct_v out_ts' (names', map (fn x => (x, [x])) vs);
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   444
            val (out_ps, gr0) = fold_map (invoke_codegen thy defs dep module false) out_ts'' gr;
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   445
            val (eq_ps, gr1) = fold_map compile_eq eqs gr0;
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   446
          in
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   447
            (case hd (select_mode_prem thy modes' vs' ps) of
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   448
               (p as Prem (us, t, is_set), (mode as Mode (_, js, _), []) :: _) =>
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   449
                 let
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   450
                   val ps' = filter_out (equal p) ps;
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   451
                   val (in_ts, out_ts''') = get_args js 1 us;
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   452
                   val (in_ps, gr2) = fold_map
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   453
                     (invoke_codegen thy defs dep module true) in_ts gr1;
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   454
                   val (ps, gr3) =
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 24625
diff changeset
   455
                     if not is_set then
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   456
                       apfst (fn ps => ps @
24129
591394d9ee66 - Added cycle test to function mk_ind_def to avoid non-termination
berghofe
parents: 23761
diff changeset
   457
                           (if null in_ps then [] else [Pretty.brk 1]) @
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   458
                           separate (Pretty.brk 1) in_ps)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   459
                         (compile_expr thy defs dep module false modes
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   460
                           (SOME mode, t) gr2)
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 24625
diff changeset
   461
                     else
31852
a16bb835e97d explicit Set constructor for code generated for sets
haftmann
parents: 31784
diff changeset
   462
                       apfst (fn p => Pretty.breaks [str "DSeq.of_list", str "(case", p,
a16bb835e97d explicit Set constructor for code generated for sets
haftmann
parents: 31784
diff changeset
   463
                         str "of", str "Set", str "xs", str "=>", str "xs)"])
a16bb835e97d explicit Set constructor for code generated for sets
haftmann
parents: 31784
diff changeset
   464
                         (*this is a very strong assumption about the generated code!*)
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   465
                           (invoke_codegen thy defs dep module true t gr2);
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   466
                   val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3;
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   467
                 in
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   468
                   (compile_match (snd nvs) eq_ps out_ps
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   469
                      (Pretty.block (ps @
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   470
                         [str " :->", Pretty.brk 1, rest]))
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   471
                      (exists (not o is_exhaustive) out_ts''), gr4)
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   472
                 end
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   473
             | (p as Sidecond t, [(_, [])]) =>
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   474
                 let
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   475
                   val ps' = filter_out (equal p) ps;
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   476
                   val (side_p, gr2) = invoke_codegen thy defs dep module true t gr1;
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   477
                   val (rest, gr3) = compile_prems [] vs' (fst nvs) ps' gr2;
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   478
                 in
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   479
                   (compile_match (snd nvs) eq_ps out_ps
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   480
                      (Pretty.block [str "?? ", side_p,
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   481
                        str " :->", Pretty.brk 1, rest])
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   482
                      (exists (not o is_exhaustive) out_ts''), gr3)
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   483
                 end
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   484
             | (_, (_, missing_vs) :: _) =>
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   485
                 let
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   486
                   val T = HOLogic.mk_tupleT (map snd missing_vs);
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   487
                   val (_, gr2) = invoke_tycodegen thy defs dep module false T gr1;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   488
                   val gen_p = mk_gen gr2 module true [] "" T;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   489
                   val (rest, gr3) = compile_prems
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   490
                     [HOLogic.mk_tuple (map Var missing_vs)] vs' (fst nvs) ps gr2
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   491
                 in
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   492
                   (compile_match (snd nvs) eq_ps out_ps
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   493
                      (Pretty.block [str "DSeq.generator", Pretty.brk 1,
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   494
                        gen_p, str " :->", Pretty.brk 1, rest])
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   495
                      (exists (not o is_exhaustive) out_ts''), gr3)
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   496
                 end)
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   497
          end;
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   498
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   499
    val (prem_p, gr') = compile_prems in_ts' arg_vs all_vs' ps gr ;
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   500
  in
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   501
    (Pretty.block [str "DSeq.single", Pretty.brk 1, inp,
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   502
       str " :->", Pretty.brk 1, prem_p], gr')
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   503
  end;
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   504
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   505
fun compile_pred thy defs dep module prfx all_vs arg_vs modes s cls mode gr =
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   506
  let
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   507
    val xs = map str (Name.variant_list arg_vs
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   508
      (map (fn i => "x" ^ string_of_int i) (snd mode)));
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   509
    val ((cl_ps, mode_id), gr') = gr |>
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   510
      fold_map (fn cl => compile_clause thy defs
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   511
        dep module all_vs arg_vs modes mode cl (mk_tuple xs)) cls ||>>
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   512
      modename module s mode
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   513
  in
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   514
    (Pretty.block
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   515
      ([Pretty.block (separate (Pretty.brk 1)
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   516
         (str (prfx ^ mode_id) ::
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   517
           map str arg_vs @
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   518
           (case mode of ([], []) => [str "()"] | _ => xs)) @
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   519
         [str " ="]),
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   520
        Pretty.brk 1] @
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32342
diff changeset
   521
       flat (separate [str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and "))
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   522
  end;
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   523
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   524
fun compile_preds thy defs dep module all_vs arg_vs modes preds gr =
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   525
  let val (prs, (gr', _)) = fold_map (fn (s, cls) =>
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   526
    fold_map (fn (mode, _) => fn (gr', prfx') => compile_pred thy defs
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   527
      dep module prfx' all_vs arg_vs modes s cls mode gr')
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   528
        (((the o AList.lookup (op =) modes) s))) preds (gr, "fun ")
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   529
  in
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32342
diff changeset
   530
    (space_implode "\n\n" (map string_of (flat prs)) ^ ";\n\n", gr')
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   531
  end;
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   532
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   533
(**** processing of introduction rules ****)
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   534
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   535
exception Modes of
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   536
  (string * ((int list option list * int list) * bool) list) list *
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   537
  (string * (int option list * int)) list;
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   538
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32342
diff changeset
   539
fun lookup_modes gr dep = apfst flat (apsnd flat (ListPair.unzip
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   540
  (map ((fn (SOME (Modes x), _, _) => x | _ => ([], [])) o get_node gr)
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   541
    (Graph.all_preds (fst gr) [dep]))));
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   542
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   543
fun print_arities arities = message ("Arities:\n" ^
26931
aa226d8405a8 cat_lines;
wenzelm
parents: 26928
diff changeset
   544
  cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   545
    space_implode " -> " (map
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   546
      (fn NONE => "X" | SOME k' => string_of_int k')
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   547
        (ks @ [SOME k]))) arities));
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   548
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 34962
diff changeset
   549
fun prep_intrs intrs = map (rename_term o #prop o rep_thm o Drule.export_without_context) intrs;
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   550
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   551
fun constrain cs [] = []
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   552
  | constrain cs ((s, xs) :: ys) =
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   553
      (s,
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   554
        case AList.lookup (op =) cs (s : string) of
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   555
          NONE => xs
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   556
        | SOME xs' => inter (op = o apfst fst) xs' xs) :: constrain cs ys;
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   557
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   558
fun mk_extra_defs thy defs gr dep names module ts =
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   559
  fold (fn name => fn gr =>
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36610
diff changeset
   560
    if member (op =) names name then gr
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   561
    else
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   562
      (case get_clauses thy name of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15257
diff changeset
   563
        NONE => gr
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   564
      | SOME (names, thyname, nparms, intrs) =>
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   565
          mk_ind_def thy defs gr dep names (if_library thyname module)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   566
            [] (prep_intrs intrs) nparms))
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   567
    (fold Term.add_const_names ts []) gr
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   568
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   569
and mk_ind_def thy defs gr dep names module modecs intrs nparms =
24129
591394d9ee66 - Added cycle test to function mk_ind_def to avoid non-termination
berghofe
parents: 23761
diff changeset
   570
  add_edge_acyclic (hd names, dep) gr handle
591394d9ee66 - Added cycle test to function mk_ind_def to avoid non-termination
berghofe
parents: 23761
diff changeset
   571
    Graph.CYCLES (xs :: _) =>
37390
8781d80026fc moved inductive_codegen to place where product type is available; tuned structure name
haftmann
parents: 37198
diff changeset
   572
      error ("Inductive_Codegen: illegal cyclic dependencies:\n" ^ commas xs)
24129
591394d9ee66 - Added cycle test to function mk_ind_def to avoid non-termination
berghofe
parents: 23761
diff changeset
   573
  | Graph.UNDEF _ =>
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   574
    let
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   575
      val _ $ u = Logic.strip_imp_concl (hd intrs);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   576
      val args = List.take (snd (strip_comb u), nparms);
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32342
diff changeset
   577
      val arg_vs = maps term_vs args;
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   578
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36610
diff changeset
   579
      fun get_nparms s = if member (op =) names s then SOME nparms else
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   580
        Option.map #3 (get_clauses thy s);
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   581
37677
c5a8b612e571 qualified constants Set.member and Set.Collect
haftmann
parents: 37527
diff changeset
   582
      fun dest_prem (_ $ (Const (@{const_name Set.member}, _) $ t $ u)) =
35364
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
   583
            Prem ([t], Envir.beta_eta_contract u, true)
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38329
diff changeset
   584
        | dest_prem (_ $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u)) =
35364
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
   585
            Prem ([t, u], eq, false)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   586
        | dest_prem (_ $ t) =
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   587
            (case strip_comb t of
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36610
diff changeset
   588
              (v as Var _, ts) => if member (op =) args v then Prem (ts, v, false) else Sidecond t
35364
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
   589
            | (c as Const (s, _), ts) =>
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
   590
                (case get_nparms s of
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
   591
                  NONE => Sidecond t
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
   592
                | SOME k =>
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
   593
                    let val (ts1, ts2) = chop k ts
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
   594
                    in Prem (ts2, list_comb (c, ts1), false) end)
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
   595
            | _ => Sidecond t);
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   596
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   597
      fun add_clause intr (clauses, arities) =
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   598
        let
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   599
          val _ $ t = Logic.strip_imp_concl intr;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   600
          val (Const (name, T), ts) = strip_comb t;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   601
          val (ts1, ts2) = chop nparms ts;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   602
          val prems = map dest_prem (Logic.strip_imp_prems intr);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   603
          val (Ts, Us) = chop nparms (binder_types T)
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   604
        in
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   605
          (AList.update op = (name, these (AList.lookup op = clauses name) @
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   606
             [(ts2, prems)]) clauses,
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   607
           AList.update op = (name, (map (fn U => (case strip_type U of
35364
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
   608
                 (Rs as _ :: _, @{typ bool}) => SOME (length Rs)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   609
               | _ => NONE)) Ts,
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   610
             length Us)) arities)
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   611
        end;
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   612
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
   613
      val gr' = mk_extra_defs thy defs
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   614
        (add_edge (hd names, dep)
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   615
          (new_node (hd names, (NONE, "", "")) gr)) (hd names) names module intrs;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   616
      val (extra_modes, extra_arities) = lookup_modes gr' (hd names);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   617
      val (clauses, arities) = fold add_clause intrs ([], []);
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   618
      val modes = constrain modecs
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   619
        (infer_modes thy extra_modes arities arg_vs clauses);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   620
      val _ = print_arities arities;
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   621
      val _ = print_modes modes;
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   622
      val (s, gr'') = compile_preds thy defs (hd names) module (terms_vs intrs)
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   623
        arg_vs (modes @ extra_modes) clauses gr';
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   624
    in
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   625
      (map_node (hd names)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   626
        (K (SOME (Modes (modes, arities)), module, s)) gr'')
16645
a152d6b21c31 Adapted to modular code generation.
berghofe
parents: 16424
diff changeset
   627
    end;
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   628
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   629
fun find_mode gr dep s u modes is = (case find_first (fn Mode (_, js, _) => is=js)
15660
255055554c67 handle Option instead of OPTION;
wenzelm
parents: 15574
diff changeset
   630
  (modes_of modes u handle Option => []) of
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   631
     NONE => codegen_error gr dep
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   632
       ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   633
   | mode => mode);
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   634
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   635
fun mk_ind_call thy defs dep module is_query s T ts names thyname k intrs gr =
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   636
  let
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   637
    val (ts1, ts2) = chop k ts;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   638
    val u = list_comb (Const (s, T), ts1);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   639
35364
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
   640
    fun mk_mode (Const (@{const_name dummy_pattern}, _)) ((ts, mode), i) = ((ts, mode), i + 1)
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   641
      | mk_mode t ((ts, mode), i) = ((ts @ [t], mode @ [i]), i + 1);
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   642
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   643
    val module' = if_library thyname module;
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   644
    val gr1 = mk_extra_defs thy defs
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   645
      (mk_ind_def thy defs gr dep names module'
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   646
      [] (prep_intrs intrs) k) dep names module' [u];
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   647
    val (modes, _) = lookup_modes gr1 dep;
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   648
    val (ts', is) =
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   649
      if is_query then fst (fold mk_mode ts2 (([], []), 1))
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   650
      else (ts2, 1 upto length (binder_types T) - k);
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   651
    val mode = find_mode gr1 dep s u modes is;
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   652
    val _ = if is_query orelse not (needs_random (the mode)) then ()
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   653
      else warning ("Illegal use of random data generators in " ^ s);
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   654
    val (in_ps, gr2) = fold_map (invoke_codegen thy defs dep module true) ts' gr1;
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   655
    val (ps, gr3) = compile_expr thy defs dep module false modes (mode, u) gr2;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   656
  in
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   657
    (Pretty.block (ps @ (if null in_ps then [] else [Pretty.brk 1]) @
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   658
       separate (Pretty.brk 1) in_ps), gr3)
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   659
  end;
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   660
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   661
fun clause_of_eqn eqn =
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   662
  let
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   663
    val (t, u) = HOLogic.dest_eq (HOLogic.dest_Trueprop (concl_of eqn));
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   664
    val (Const (s, T), ts) = strip_comb t;
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   665
    val (Ts, U) = strip_type T
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   666
  in
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   667
    rename_term (Logic.list_implies (prems_of eqn, HOLogic.mk_Trueprop
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   668
      (list_comb (Const (s ^ "_aux", Ts @ [U] ---> HOLogic.boolT), ts @ [u]))))
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   669
  end;
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   670
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   671
fun mk_fun thy defs name eqns dep module module' gr =
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   672
  case try (get_node gr) name of
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   673
    NONE =>
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   674
    let
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   675
      val clauses = map clause_of_eqn eqns;
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   676
      val pname = name ^ "_aux";
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   677
      val arity = length (snd (strip_comb (fst (HOLogic.dest_eq
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   678
        (HOLogic.dest_Trueprop (concl_of (hd eqns)))))));
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   679
      val mode = 1 upto arity;
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   680
      val ((fun_id, mode_id), gr') = gr |>
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   681
        mk_const_id module' name ||>>
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   682
        modename module' pname ([], mode);
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   683
      val vars = map (fn i => str ("x" ^ string_of_int i)) mode;
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   684
      val s = string_of (Pretty.block
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   685
        [mk_app false (str ("fun " ^ snd fun_id)) vars, str " =",
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   686
         Pretty.brk 1, str "DSeq.hd", Pretty.brk 1,
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   687
         parens (Pretty.block (separate (Pretty.brk 1) (str mode_id ::
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   688
           vars)))]) ^ ";\n\n";
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   689
      val gr'' = mk_ind_def thy defs (add_edge (name, dep)
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   690
        (new_node (name, (NONE, module', s)) gr')) name [pname] module'
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   691
        [(pname, [([], mode)])] clauses 0;
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   692
      val (modes, _) = lookup_modes gr'' dep;
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   693
      val _ = find_mode gr'' dep pname (head_of (HOLogic.dest_Trueprop
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   694
        (Logic.strip_imp_concl (hd clauses)))) modes mode
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   695
    in (mk_qual_id module fun_id, gr'') end
17144
6642e0f96f44 Implemented incremental code generation.
berghofe
parents: 16861
diff changeset
   696
  | SOME _ =>
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   697
      (mk_qual_id module (get_const_id gr name), add_edge (name, dep) gr);
15031
726dc9146bb1 - Added support for conditional equations whose premises involve
berghofe
parents: 14981
diff changeset
   698
23761
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   699
(* convert n-tuple to nested pairs *)
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   700
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   701
fun conv_ntuple fs ts p =
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   702
  let
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   703
    val k = length fs;
33063
4d462963a7db map_range (and map_index) combinator
haftmann
parents: 33050
diff changeset
   704
    val xs = map_range (fn i => str ("x" ^ string_of_int i)) (k + 1);
23761
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   705
    val xs' = map (fn Bound i => nth xs (k - i)) ts;
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   706
    fun conv xs js =
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36610
diff changeset
   707
      if member (op =) fs js then
23761
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   708
        let
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   709
          val (p, xs') = conv xs (1::js);
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   710
          val (q, xs'') = conv xs' (2::js)
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   711
        in (mk_tuple [p, q], xs'') end
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   712
      else (hd xs, tl xs)
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   713
  in
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   714
    if k > 0 then
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   715
      Pretty.block
26975
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   716
        [str "DSeq.map (fn", Pretty.brk 1,
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   717
         mk_tuple xs', str " =>", Pretty.brk 1, fst (conv xs []),
103dca19ef2e Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents: 26939
diff changeset
   718
         str ")", Pretty.brk 1, parens p]
23761
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   719
    else p
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   720
  end;
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   721
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   722
fun inductive_codegen thy defs dep module brack t gr  = (case strip_comb t of
35364
b8c62d60195c more antiquotations;
wenzelm
parents: 35021
diff changeset
   723
    (Const (@{const_name Collect}, _), [u]) =>
32342
3fabf5b5fc83 path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
haftmann
parents: 32287
diff changeset
   724
      let val (r, Ts, fs) = HOLogic.strip_psplits u
23761
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   725
      in case strip_comb r of
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   726
          (Const (s, T), ts) =>
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   727
            (case (get_clauses thy s, get_assoc_code thy (s, T)) of
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   728
              (SOME (names, thyname, k, intrs), NONE) =>
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   729
                let
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   730
                  val (ts1, ts2) = chop k ts;
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   731
                  val ts2' = map
34962
807f6ce0273d HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
haftmann
parents: 33963
diff changeset
   732
                    (fn Bound i => Term.dummy_pattern (nth Ts (length Ts - i - 1)) | t => t) ts2;
23761
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   733
                  val (ots, its) = List.partition is_Bound ts2;
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   734
                  val no_loose = forall (fn t => not (loose_bvar (t, 0)))
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   735
                in
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   736
                  if null (duplicates op = ots) andalso
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   737
                    no_loose ts1 andalso no_loose its
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   738
                  then
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   739
                    let val (call_p, gr') = mk_ind_call thy defs dep module true
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   740
                      s T (ts1 @ ts2') names thyname k intrs gr 
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   741
                    in SOME ((if brack then parens else I) (Pretty.block
31852
a16bb835e97d explicit Set constructor for code generated for sets
haftmann
parents: 31784
diff changeset
   742
                      [str "Set", Pretty.brk 1, str "(DSeq.list_of", Pretty.brk 1, str "(",
a16bb835e97d explicit Set constructor for code generated for sets
haftmann
parents: 31784
diff changeset
   743
                       conv_ntuple fs ots call_p, str "))"]),
a16bb835e97d explicit Set constructor for code generated for sets
haftmann
parents: 31784
diff changeset
   744
                       (*this is a very strong assumption about the generated code!*)
a16bb835e97d explicit Set constructor for code generated for sets
haftmann
parents: 31784
diff changeset
   745
                       gr')
23761
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   746
                    end
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   747
                  else NONE
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   748
                end
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   749
            | _ => NONE)
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   750
        | _ => NONE
9cebbaccf8a2 Improved code generator for Collect.
berghofe
parents: 22921
diff changeset
   751
      end
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   752
  | (Const (s, T), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy)) s of
22921
475ff421a6a3 consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents: 22846
diff changeset
   753
      NONE => (case (get_clauses thy s, get_assoc_code thy (s, T)) of
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   754
        (SOME (names, thyname, k, intrs), NONE) =>
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   755
          if length ts < k then NONE else SOME
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   756
            (let val (call_p, gr') = mk_ind_call thy defs dep module false
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   757
               s T (map Term.no_dummy_patterns ts) names thyname k intrs gr
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   758
             in (mk_funcomp brack "?!"
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   759
               (length (binder_types T) - length ts) (parens call_p), gr')
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   760
             end handle TERM _ => mk_ind_call thy defs dep module true
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   761
               s T ts names thyname k intrs gr )
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   762
      | _ => NONE)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   763
    | SOME eqns =>
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   764
        let
22642
bfdb29f11eb4 canonical merge operations
haftmann
parents: 22556
diff changeset
   765
          val (_, thyname) :: _ = eqns;
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   766
          val (id, gr') = mk_fun thy defs s (preprocess thy (map fst (rev eqns)))
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   767
            dep module (if_library thyname module) gr;
28537
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   768
          val (ps, gr'') = fold_map
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   769
            (invoke_codegen thy defs dep module true) ts gr';
1e84256d1a8a established canonical argument order in SML code generators
haftmann
parents: 27809
diff changeset
   770
        in SOME (mk_app brack (str id) ps, gr'')
22271
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   771
        end)
51a80e238b29 Adapted to new inductive definition package.
berghofe
parents: 21022
diff changeset
   772
  | _ => NONE);
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   773
12557
bb2e4689347e Implemented higher order modes.
berghofe
parents: 12453
diff changeset
   774
val setup =
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18388
diff changeset
   775
  add_codegen "inductive" inductive_codegen #>
33244
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   776
  Attrib.setup @{binding code_ind}
db230399f890 Datatype.read_typ: standard argument order;
wenzelm
parents: 33063
diff changeset
   777
    (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36692
diff changeset
   778
      Scan.option (Args.$$$ "params" |-- Args.colon |-- Parse.nat) >> uncurry add))
31998
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31852
diff changeset
   779
    "introduction rules for executable predicates";
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   780
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   781
(**** Quickcheck involving inductive predicates ****)
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   782
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   783
val test_fn : (int * int * int -> term list option) Unsynchronized.ref =
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   784
  Unsynchronized.ref (fn _ => NONE);
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   785
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   786
fun strip_imp p =
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   787
  let val (q, r) = HOLogic.dest_imp p
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   788
  in strip_imp r |>> cons q end
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   789
  handle TERM _ => ([], p);
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   790
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   791
fun deepen bound f i =
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   792
  if i > bound then NONE
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   793
  else (case f i of
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   794
      NONE => deepen bound f (i + 1)
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   795
    | SOME x => SOME x);
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   796
36001
992839c4be90 static defaults for configuration options;
wenzelm
parents: 35997
diff changeset
   797
val (depth_bound, setup_depth_bound) = Attrib.config_int "ind_quickcheck_depth" (K 10);
992839c4be90 static defaults for configuration options;
wenzelm
parents: 35997
diff changeset
   798
val (depth_start, setup_depth_start) = Attrib.config_int "ind_quickcheck_depth_start" (K 1);
992839c4be90 static defaults for configuration options;
wenzelm
parents: 35997
diff changeset
   799
val (random_values, setup_random_values) = Attrib.config_int "ind_quickcheck_random" (K 5);
992839c4be90 static defaults for configuration options;
wenzelm
parents: 35997
diff changeset
   800
val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" (K 0);
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   801
39253
0c47d615a69b removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
bulwahn
parents: 39252
diff changeset
   802
fun test_term ctxt t =
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   803
  let
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   804
    val thy = ProofContext.theory_of ctxt;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   805
    val (xs, p) = strip_abs t;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   806
    val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   807
    val args = map Free args';
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   808
    val (ps, q) = strip_imp p;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   809
    val Ts = map snd xs;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   810
    val T = Ts ---> HOLogic.boolT;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   811
    val rl = Logic.list_implies
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   812
      (map (HOLogic.mk_Trueprop o curry subst_bounds (rev args)) ps @
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   813
       [HOLogic.mk_Trueprop (HOLogic.mk_not (subst_bounds (rev args, q)))],
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   814
       HOLogic.mk_Trueprop (list_comb (Free ("quickcheckp", T), args)));
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   815
    val (_, thy') = Inductive.add_inductive_global
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   816
      {quiet_mode=true, verbose=false, alt_name=Binding.empty, coind=false,
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   817
       no_elim=true, no_ind=false, skip_mono=false, fork_mono=false}
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   818
      [((Binding.name "quickcheckp", T), NoSyn)] []
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   819
      [(Attrib.empty_binding, rl)] [] (Theory.copy thy);
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   820
    val pred = HOLogic.mk_Trueprop (list_comb
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   821
      (Const (Sign.intern_const thy' "quickcheckp", T),
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   822
       map Term.dummy_pattern Ts));
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   823
    val (code, gr) = setmp_CRITICAL mode ["term_of", "test", "random_ind"]
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   824
      (generate_code_i thy' [] "Generated") [("testf", pred)];
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   825
    val s = "structure TestTerm =\nstruct\n\n" ^
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   826
      cat_lines (map snd code) ^
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   827
      "\nopen Generated;\n\n" ^ string_of
37390
8781d80026fc moved inductive_codegen to place where product type is available; tuned structure name
haftmann
parents: 37198
diff changeset
   828
        (Pretty.block [str "val () = Inductive_Codegen.test_fn :=",
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   829
          Pretty.brk 1, str "(fn p =>", Pretty.brk 1,
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   830
          str "case Seq.pull (testf p) of", Pretty.brk 1,
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   831
          str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"],
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   832
          str " =>", Pretty.brk 1, str "SOME ",
38329
16bb1e60204b use Pretty.enum convenience;
wenzelm
parents: 37677
diff changeset
   833
          Pretty.enum "," "[" "]"
16bb1e60204b use Pretty.enum convenience;
wenzelm
parents: 37677
diff changeset
   834
            (map (fn (s, T) => Pretty.block
16bb1e60204b use Pretty.enum convenience;
wenzelm
parents: 37677
diff changeset
   835
              [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args'),
16bb1e60204b use Pretty.enum convenience;
wenzelm
parents: 37677
diff changeset
   836
          Pretty.brk 1,
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   837
          str "| NONE => NONE);"]) ^
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   838
      "\n\nend;\n";
37198
3af985b10550 replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents: 36960
diff changeset
   839
    val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   840
    val values = Config.get ctxt random_values;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   841
    val bound = Config.get ctxt depth_bound;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   842
    val start = Config.get ctxt depth_start;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   843
    val offset = Config.get ctxt size_offset;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   844
    val test_fn' = !test_fn;
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35021
diff changeset
   845
    val dummy_report = ([], false)
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35021
diff changeset
   846
    fun test k = (deepen bound (fn i =>
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 39253
diff changeset
   847
      (Output.urgent_message ("Search depth: " ^ string_of_int i);
35378
95d0e3adf38e added basic reporting of test cases to quickcheck
bulwahn
parents: 35021
diff changeset
   848
       test_fn' (i, values, k+offset))) start, dummy_report);
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   849
  in test end;
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   850
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   851
val quickcheck_setup =
35997
07bce2802939 use regular Attrib.config instead of low-level Config.declare/Attrib.register_config;
wenzelm
parents: 35382
diff changeset
   852
  setup_depth_bound #>
07bce2802939 use regular Attrib.config instead of low-level Config.declare/Attrib.register_config;
wenzelm
parents: 35382
diff changeset
   853
  setup_depth_start #>
07bce2802939 use regular Attrib.config instead of low-level Config.declare/Attrib.register_config;
wenzelm
parents: 35382
diff changeset
   854
  setup_random_values #>
07bce2802939 use regular Attrib.config instead of low-level Config.declare/Attrib.register_config;
wenzelm
parents: 35382
diff changeset
   855
  setup_size_offset #>
39252
8f176e575a49 changing the container for the quickcheck options to a generic data
bulwahn
parents: 38864
diff changeset
   856
  Context.theory_map (Quickcheck.add_generator ("SML_inductive", test_term));
33771
17926df64f0f Added new counterexample generator SML_inductive for goals involving
berghofe
parents: 33522
diff changeset
   857
11537
e007d35359c3 New code generators for HOL.
berghofe
parents:
diff changeset
   858
end;