src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
author haftmann
Tue Oct 13 09:21:15 2015 +0200 (2015-10-13)
changeset 61424 c3658c18b7bc
parent 61268 abe08fb15a12
child 62354 fdd6989cc8a0
permissions -rw-r--r--
prod_case as canonical name for product type eliminator
wenzelm@33265
     1
(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_core.ML
wenzelm@33265
     2
    Author:     Lukas Bulwahn, TU Muenchen
bulwahn@32667
     3
wenzelm@33265
     4
A compiler from predicates specified by intro/elim rules to equations.
bulwahn@32667
     5
*)
bulwahn@32667
     6
bulwahn@32667
     7
signature PREDICATE_COMPILE_CORE =
bulwahn@32667
     8
sig
haftmann@50057
     9
  type seed = Random_Engine.seed
bulwahn@36048
    10
  type mode = Predicate_Compile_Aux.mode
bulwahn@36048
    11
  type options = Predicate_Compile_Aux.options
bulwahn@36048
    12
  type compilation = Predicate_Compile_Aux.compilation
bulwahn@36048
    13
  type compilation_funs = Predicate_Compile_Aux.compilation_funs
wenzelm@55437
    14
bulwahn@36048
    15
  val code_pred : options -> string -> Proof.context -> Proof.state
bulwahn@36048
    16
  val code_pred_cmd : options -> string -> Proof.context -> Proof.state
wenzelm@55437
    17
  val values_cmd : string list -> mode option list option ->
wenzelm@55437
    18
    ((string option * bool) * (compilation * int list)) -> int -> string -> Toplevel.state -> unit
bulwahn@40053
    19
bulwahn@42141
    20
  val values_timeout : real Config.T
wenzelm@55437
    21
bulwahn@37007
    22
  val print_stored_rules : Proof.context -> unit
bulwahn@37003
    23
  val print_all_modes : compilation -> Proof.context -> unit
haftmann@39388
    24
haftmann@39388
    25
  val put_pred_result : (unit -> term Predicate.pred) -> Proof.context -> Proof.context
haftmann@50057
    26
  val put_pred_random_result : (unit -> seed -> term Predicate.pred * seed) ->
haftmann@39388
    27
    Proof.context -> Proof.context
haftmann@51126
    28
  val put_dseq_result : (unit -> term Limited_Sequence.dseq) -> Proof.context -> Proof.context
wenzelm@55437
    29
  val put_dseq_random_result :
wenzelm@55437
    30
    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
wenzelm@55437
    31
      term Limited_Sequence.dseq * seed) ->
haftmann@39388
    32
    Proof.context -> Proof.context
haftmann@51143
    33
  val put_new_dseq_result : (unit -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence) ->
bulwahn@40102
    34
    Proof.context -> Proof.context
haftmann@39388
    35
  val put_lseq_random_result :
wenzelm@55437
    36
    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural ->
wenzelm@55437
    37
      term Lazy_Sequence.lazy_sequence) ->
haftmann@39388
    38
    Proof.context -> Proof.context
haftmann@39388
    39
  val put_lseq_random_stats_result :
wenzelm@55437
    40
    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural ->
wenzelm@55437
    41
      (term * Code_Numeral.natural) Lazy_Sequence.lazy_sequence) ->
haftmann@39388
    42
    Proof.context -> Proof.context
haftmann@39388
    43
bulwahn@33628
    44
  val code_pred_intro_attrib : attribute
wenzelm@55437
    45
  (* used by Quickcheck_Generator *)
bulwahn@32667
    46
  (* temporary for testing of the compilation *)
bulwahn@36048
    47
  val add_equations : options -> string list -> theory -> theory
bulwahn@36048
    48
  val add_depth_limited_random_equations : options -> string list -> theory -> theory
bulwahn@36048
    49
  val add_random_dseq_equations : options -> string list -> theory -> theory
bulwahn@36048
    50
  val add_new_random_dseq_equations : options -> string list -> theory -> theory
bulwahn@40103
    51
  val add_generator_dseq_equations : options -> string list -> theory -> theory
bulwahn@45450
    52
  val add_generator_cps_equations : options -> string list -> theory -> theory
bulwahn@33473
    53
  val mk_tracing : string -> term -> term
bulwahn@39310
    54
  val prepare_intrs : options -> Proof.context -> string list -> thm list ->
bulwahn@38957
    55
    ((string * typ) list * string list * string list * (string * mode list) list *
bulwahn@38957
    56
      (string *  (Term.term list * Predicate_Compile_Aux.indprem list) list) list)
bulwahn@39761
    57
  type mode_analysis_options =
bulwahn@39761
    58
   {use_generators : bool,
bulwahn@39761
    59
    reorder_premises : bool,
wenzelm@55437
    60
    infer_pos_and_neg_modes : bool}
bulwahn@38957
    61
  datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
bulwahn@39310
    62
    | Mode_Pair of mode_derivation * mode_derivation | Term of mode
bulwahn@39461
    63
  val head_mode_of : mode_derivation -> mode
bulwahn@38957
    64
  type moded_clause = term list * (Predicate_Compile_Aux.indprem * mode_derivation) list
bulwahn@38957
    65
  type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
bulwahn@38957
    66
bulwahn@32667
    67
end;
bulwahn@32667
    68
bulwahn@32667
    69
structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
bulwahn@32667
    70
struct
bulwahn@32667
    71
haftmann@51143
    72
type random_seed = Random_Engine.seed
haftmann@51143
    73
bulwahn@32668
    74
open Predicate_Compile_Aux;
bulwahn@40052
    75
open Mode_Inference;
bulwahn@40052
    76
open Predicate_Compile_Proof;
bulwahn@33108
    77
haftmann@50057
    78
type seed = Random_Engine.seed;
haftmann@50057
    79
haftmann@50057
    80
bulwahn@32667
    81
(** fundamentals **)
bulwahn@32667
    82
bulwahn@32667
    83
(* syntactic operations *)
bulwahn@32667
    84
bulwahn@32667
    85
fun mk_eq (x, xs) =
bulwahn@32667
    86
  let fun mk_eqs _ [] = []
bulwahn@32667
    87
        | mk_eqs a (b::cs) =
bulwahn@32667
    88
            HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
bulwahn@32667
    89
  in mk_eqs x xs end;
bulwahn@32667
    90
bulwahn@33473
    91
fun mk_tracing s t =
bulwahn@33473
    92
  Const(@{const_name Code_Evaluation.tracing},
bulwahn@33473
    93
    @{typ String.literal} --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t
bulwahn@33473
    94
wenzelm@55437
    95
bulwahn@34948
    96
(* representation of inferred clauses with modes *)
bulwahn@32667
    97
bulwahn@34948
    98
type moded_clause = term list * (indprem * mode_derivation) list
bulwahn@34948
    99
bulwahn@35324
   100
type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
bulwahn@32667
   101
wenzelm@55437
   102
bulwahn@32667
   103
(* diagnostic display functions *)
bulwahn@32667
   104
bulwahn@37004
   105
fun print_modes options modes =
bulwahn@33251
   106
  if show_modes options then
bulwahn@33326
   107
    tracing ("Inferred modes:\n" ^
bulwahn@33251
   108
      cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
bulwahn@35324
   109
        (fn (p, m) => string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes))
bulwahn@33251
   110
  else ()
bulwahn@32667
   111
bulwahn@37004
   112
fun print_pred_mode_table string_of_entry pred_mode_table =
bulwahn@32667
   113
  let
haftmann@50056
   114
    fun print_mode pred ((_, mode), entry) =  "mode : " ^ string_of_mode mode
bulwahn@33619
   115
      ^ string_of_entry pred mode entry
bulwahn@32667
   116
    fun print_pred (pred, modes) =
bulwahn@32667
   117
      "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
bulwahn@33326
   118
    val _ = tracing (cat_lines (map print_pred pred_mode_table))
bulwahn@32667
   119
  in () end;
bulwahn@32667
   120
bulwahn@37005
   121
fun print_compiled_terms options ctxt =
bulwahn@33139
   122
  if show_compilation options then
bulwahn@37005
   123
    print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term ctxt)
bulwahn@33139
   124
  else K ()
bulwahn@33139
   125
bulwahn@37007
   126
fun print_stored_rules ctxt =
bulwahn@32667
   127
  let
wenzelm@61114
   128
    val preds = Graph.keys (Core_Data.PredData.get (Proof_Context.theory_of ctxt))
wenzelm@61114
   129
    fun print pred () =
wenzelm@61114
   130
      let
wenzelm@61114
   131
        val _ = writeln ("predicate: " ^ pred)
wenzelm@61114
   132
        val _ = writeln ("introrules: ")
wenzelm@61268
   133
        val _ = fold (fn thm => fn _ => writeln (Thm.string_of_thm ctxt thm))
wenzelm@61114
   134
          (rev (Core_Data.intros_of ctxt pred)) ()
wenzelm@61114
   135
      in
wenzelm@61114
   136
        if Core_Data.has_elim ctxt pred then
wenzelm@61268
   137
          writeln ("elimrule: " ^ Thm.string_of_thm ctxt (Core_Data.the_elim_of ctxt pred))
wenzelm@61114
   138
        else
wenzelm@61114
   139
          writeln ("no elimrule defined")
wenzelm@61114
   140
      end
bulwahn@32667
   141
  in
bulwahn@32667
   142
    fold print preds ()
bulwahn@32667
   143
  end;
bulwahn@32667
   144
bulwahn@37003
   145
fun print_all_modes compilation ctxt =
bulwahn@32667
   146
  let
bulwahn@32667
   147
    val _ = writeln ("Inferred modes:")
bulwahn@32667
   148
    fun print (pred, modes) u =
bulwahn@32667
   149
      let
bulwahn@32667
   150
        val _ = writeln ("predicate: " ^ pred)
bulwahn@34948
   151
        val _ = writeln ("modes: " ^ (commas (map string_of_mode modes)))
bulwahn@33619
   152
      in u end
bulwahn@32667
   153
  in
wenzelm@61114
   154
    fold print (Core_Data.all_modes_of compilation ctxt) ()
bulwahn@32667
   155
  end
bulwahn@33129
   156
bulwahn@33132
   157
(* validity checks *)
bulwahn@33132
   158
haftmann@50056
   159
fun check_expected_modes options _ modes =
wenzelm@55437
   160
  (case expected_modes options of
wenzelm@55437
   161
    SOME (s, ms) =>
wenzelm@55437
   162
      (case AList.lookup (op =) modes s of
wenzelm@55437
   163
        SOME modes =>
wenzelm@55437
   164
          let
wenzelm@55437
   165
            val modes' = map snd modes
wenzelm@55437
   166
          in
wenzelm@55437
   167
            if not (eq_set eq_mode (ms, modes')) then
wenzelm@55437
   168
              error ("expected modes were not inferred:\n"
wenzelm@55437
   169
              ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes')  ^ "\n"
wenzelm@55437
   170
              ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms))
wenzelm@55437
   171
            else ()
wenzelm@55437
   172
          end
wenzelm@55437
   173
        | NONE => ())
wenzelm@55437
   174
  | NONE => ())
bulwahn@33752
   175
bulwahn@40138
   176
fun check_proposed_modes options preds modes errors =
wenzelm@55437
   177
  map (fn (s, _) =>
wenzelm@55437
   178
    case proposed_modes options s of
wenzelm@55437
   179
      SOME ms =>
wenzelm@55437
   180
        (case AList.lookup (op =) modes s of
wenzelm@55437
   181
          SOME inferred_ms =>
wenzelm@55437
   182
            let
wenzelm@55437
   183
              val preds_without_modes = map fst (filter (null o snd) modes)
wenzelm@55437
   184
              val modes' = map snd inferred_ms
wenzelm@55437
   185
            in
wenzelm@55437
   186
              if not (eq_set eq_mode (ms, modes')) then
wenzelm@55437
   187
                error ("expected modes were not inferred:\n"
wenzelm@55437
   188
                ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes')  ^ "\n"
wenzelm@55437
   189
                ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms) ^ "\n"
wenzelm@55437
   190
                ^ (if show_invalid_clauses options then
wenzelm@55437
   191
                ("For the following clauses, the following modes could not be inferred: " ^ "\n"
wenzelm@55437
   192
                ^ cat_lines errors) else "") ^
wenzelm@55437
   193
                (if not (null preds_without_modes) then
wenzelm@55437
   194
                  "\n" ^ "No mode inferred for the predicates " ^ commas preds_without_modes
wenzelm@55437
   195
                else ""))
wenzelm@55437
   196
              else ()
wenzelm@55437
   197
            end
wenzelm@55437
   198
        | NONE => ())
wenzelm@55437
   199
    | NONE => ()) preds
bulwahn@33132
   200
bulwahn@39651
   201
fun check_matches_type ctxt predname T ms =
bulwahn@39651
   202
  let
haftmann@50056
   203
    fun check (Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2
haftmann@50056
   204
      | check m (Type("fun", _)) = (m = Input orelse m = Output)
bulwahn@39651
   205
      | check (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
wenzelm@55437
   206
          check m1 T1 andalso check m2 T2
haftmann@50056
   207
      | check Input _ = true
haftmann@50056
   208
      | check Output _ = true
bulwahn@39651
   209
      | check Bool @{typ bool} = true
bulwahn@39651
   210
      | check _ _ = false
bulwahn@39763
   211
    fun check_consistent_modes ms =
haftmann@50056
   212
      if forall (fn Fun _ => true | _ => false) ms then
wenzelm@59058
   213
        apply2 check_consistent_modes (split_list (map (fn Fun (m1, m2) => (m1, m2)) ms))
wenzelm@55437
   214
        |> (fn (res1, res2) => res1 andalso res2)
bulwahn@39763
   215
      else if forall (fn Input => true | Output => true | Pair _ => true | _ => false) ms then
bulwahn@39763
   216
        true
bulwahn@39763
   217
      else if forall (fn Bool => true | _ => false) ms then
bulwahn@39763
   218
        true
bulwahn@39763
   219
      else
bulwahn@39763
   220
        false
wenzelm@55437
   221
    val _ =
wenzelm@55437
   222
      map (fn mode =>
bulwahn@39763
   223
        if length (strip_fun_mode mode) = length (binder_types T)
bulwahn@39763
   224
          andalso (forall (uncurry check) (strip_fun_mode mode ~~ binder_types T)) then ()
wenzelm@55437
   225
        else
wenzelm@55437
   226
          error (string_of_mode mode ^ " is not a valid mode for " ^
wenzelm@55437
   227
            Syntax.string_of_typ ctxt T ^ " at predicate " ^ predname)) ms
bulwahn@39763
   228
    val _ =
wenzelm@55437
   229
      if check_consistent_modes ms then ()
wenzelm@55437
   230
      else
wenzelm@55437
   231
        error (commas (map string_of_mode ms) ^ " are inconsistent modes for predicate " ^ predname)
bulwahn@39651
   232
  in
bulwahn@39651
   233
    ms
bulwahn@39651
   234
  end
bulwahn@39651
   235
wenzelm@55437
   236
bulwahn@36019
   237
(* compilation modifiers *)
bulwahn@36019
   238
wenzelm@55437
   239
structure Comp_Mod =  (* FIXME proper signature *)
bulwahn@36019
   240
struct
bulwahn@36019
   241
bulwahn@36019
   242
datatype comp_modifiers = Comp_Modifiers of
bulwahn@36019
   243
{
bulwahn@36019
   244
  compilation : compilation,
bulwahn@36019
   245
  function_name_prefix : string,
bulwahn@36019
   246
  compfuns : compilation_funs,
bulwahn@36019
   247
  mk_random : typ -> term list -> term,
bulwahn@36019
   248
  modify_funT : typ -> typ,
bulwahn@36019
   249
  additional_arguments : string list -> term list,
bulwahn@36019
   250
  wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
bulwahn@36019
   251
  transform_additional_arguments : indprem -> term list -> term list
bulwahn@36019
   252
}
bulwahn@36019
   253
bulwahn@36019
   254
fun dest_comp_modifiers (Comp_Modifiers c) = c
bulwahn@36019
   255
bulwahn@36019
   256
val compilation = #compilation o dest_comp_modifiers
bulwahn@36019
   257
val function_name_prefix = #function_name_prefix o dest_comp_modifiers
bulwahn@36019
   258
val compfuns = #compfuns o dest_comp_modifiers
bulwahn@36019
   259
bulwahn@36019
   260
val mk_random = #mk_random o dest_comp_modifiers
bulwahn@36019
   261
val funT_of' = funT_of o compfuns
bulwahn@36019
   262
val modify_funT = #modify_funT o dest_comp_modifiers
bulwahn@36019
   263
fun funT_of comp mode = modify_funT comp o funT_of' comp mode
bulwahn@36019
   264
bulwahn@36019
   265
val additional_arguments = #additional_arguments o dest_comp_modifiers
bulwahn@36019
   266
val wrap_compilation = #wrap_compilation o dest_comp_modifiers
bulwahn@36019
   267
val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers
bulwahn@36019
   268
bulwahn@40049
   269
fun set_compfuns compfuns' (Comp_Modifiers {compilation, function_name_prefix, compfuns, mk_random,
bulwahn@40049
   270
    modify_funT, additional_arguments, wrap_compilation, transform_additional_arguments}) =
bulwahn@40049
   271
    (Comp_Modifiers {compilation = compilation, function_name_prefix = function_name_prefix,
bulwahn@40049
   272
    compfuns = compfuns', mk_random = mk_random, modify_funT = modify_funT,
bulwahn@40049
   273
    additional_arguments = additional_arguments, wrap_compilation = wrap_compilation,
bulwahn@40049
   274
    transform_additional_arguments = transform_additional_arguments})
bulwahn@40049
   275
wenzelm@55437
   276
end
bulwahn@36019
   277
bulwahn@40051
   278
fun unlimited_compfuns_of true New_Pos_Random_DSeq =
wenzelm@55437
   279
      New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
bulwahn@40051
   280
  | unlimited_compfuns_of false New_Pos_Random_DSeq =
wenzelm@55437
   281
      New_Neg_Random_Sequence_CompFuns.depth_unlimited_compfuns
bulwahn@40051
   282
  | unlimited_compfuns_of true Pos_Generator_DSeq =
wenzelm@55437
   283
      New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
bulwahn@40051
   284
  | unlimited_compfuns_of false Pos_Generator_DSeq =
wenzelm@55437
   285
      New_Neg_DSequence_CompFuns.depth_unlimited_compfuns
bulwahn@40051
   286
  | unlimited_compfuns_of _ c =
wenzelm@55437
   287
      raise Fail ("No unlimited compfuns for compilation " ^ string_of_compilation c)
bulwahn@40051
   288
bulwahn@40049
   289
fun limited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq =
wenzelm@55437
   290
      New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
bulwahn@40049
   291
  | limited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq =
wenzelm@55437
   292
      New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
bulwahn@40051
   293
  | limited_compfuns_of true Pos_Generator_DSeq =
wenzelm@55437
   294
      New_Pos_DSequence_CompFuns.depth_limited_compfuns
bulwahn@40051
   295
  | limited_compfuns_of false Pos_Generator_DSeq =
wenzelm@55437
   296
      New_Neg_DSequence_CompFuns.depth_limited_compfuns
bulwahn@40051
   297
  | limited_compfuns_of _ c =
wenzelm@55437
   298
      raise Fail ("No limited compfuns for compilation " ^ string_of_compilation c)
bulwahn@40049
   299
bulwahn@36019
   300
val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
bulwahn@36019
   301
  {
bulwahn@36019
   302
  compilation = Depth_Limited,
bulwahn@36019
   303
  function_name_prefix = "depth_limited_",
bulwahn@45450
   304
  compfuns = Predicate_Comp_Funs.compfuns,
bulwahn@36019
   305
  mk_random = (fn _ => error "no random generation"),
bulwahn@36019
   306
  additional_arguments = fn names =>
bulwahn@36019
   307
    let
wenzelm@43324
   308
      val depth_name = singleton (Name.variant_list names) "depth"
haftmann@51143
   309
    in [Free (depth_name, @{typ natural})] end,
bulwahn@36019
   310
  modify_funT = (fn T => let val (Ts, U) = strip_type T
haftmann@51143
   311
  val Ts' = [@{typ natural}] in (Ts @ Ts') ---> U end),
bulwahn@36019
   312
  wrap_compilation =
bulwahn@36019
   313
    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
bulwahn@36019
   314
    let
bulwahn@36019
   315
      val [depth] = additional_arguments
bulwahn@40139
   316
      val (_, Ts) = split_modeT mode (binder_types T)
bulwahn@45461
   317
      val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts)
bulwahn@36019
   318
      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
bulwahn@36019
   319
    in
haftmann@51143
   320
      if_const $ HOLogic.mk_eq (depth, @{term "0 :: natural"})
bulwahn@45461
   321
        $ mk_empty compfuns (dest_monadT compfuns T')
bulwahn@36019
   322
        $ compilation
bulwahn@36019
   323
    end,
bulwahn@36019
   324
  transform_additional_arguments =
haftmann@50056
   325
    fn _ => fn additional_arguments =>
bulwahn@36019
   326
    let
bulwahn@36019
   327
      val [depth] = additional_arguments
bulwahn@36019
   328
      val depth' =
haftmann@51143
   329
        Const (@{const_name Groups.minus}, @{typ "natural => natural => natural"})
haftmann@51143
   330
          $ depth $ Const (@{const_name Groups.one}, @{typ "natural"})
bulwahn@36019
   331
    in [depth'] end
bulwahn@36019
   332
  }
bulwahn@36019
   333
bulwahn@36019
   334
val random_comp_modifiers = Comp_Mod.Comp_Modifiers
bulwahn@36019
   335
  {
bulwahn@36019
   336
  compilation = Random,
bulwahn@36019
   337
  function_name_prefix = "random_",
bulwahn@45450
   338
  compfuns = Predicate_Comp_Funs.compfuns,
bulwahn@36019
   339
  mk_random = (fn T => fn additional_arguments =>
haftmann@51126
   340
  list_comb (Const(@{const_name Random_Pred.iter},
wenzelm@55437
   341
  [@{typ natural}, @{typ natural}, @{typ Random.seed}] --->
bulwahn@45461
   342
    Predicate_Comp_Funs.mk_monadT T), additional_arguments)),
bulwahn@36019
   343
  modify_funT = (fn T =>
bulwahn@36019
   344
    let
bulwahn@36019
   345
      val (Ts, U) = strip_type T
haftmann@51143
   346
      val Ts' = [@{typ natural}, @{typ natural}, @{typ Random.seed}]
bulwahn@36019
   347
    in (Ts @ Ts') ---> U end),
bulwahn@36019
   348
  additional_arguments = (fn names =>
bulwahn@36019
   349
    let
bulwahn@36019
   350
      val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"]
bulwahn@36019
   351
    in
haftmann@51143
   352
      [Free (nrandom, @{typ natural}), Free (size, @{typ natural}),
haftmann@51126
   353
        Free (seed, @{typ Random.seed})]
bulwahn@36019
   354
    end),
bulwahn@36019
   355
  wrap_compilation = K (K (K (K (K I))))
bulwahn@36019
   356
    : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
bulwahn@36019
   357
  transform_additional_arguments = K I : (indprem -> term list -> term list)
bulwahn@36019
   358
  }
bulwahn@36019
   359
bulwahn@36019
   360
val depth_limited_random_comp_modifiers = Comp_Mod.Comp_Modifiers
bulwahn@36019
   361
  {
bulwahn@36019
   362
  compilation = Depth_Limited_Random,
bulwahn@36019
   363
  function_name_prefix = "depth_limited_random_",
bulwahn@45450
   364
  compfuns = Predicate_Comp_Funs.compfuns,
bulwahn@36019
   365
  mk_random = (fn T => fn additional_arguments =>
haftmann@51126
   366
  list_comb (Const(@{const_name Random_Pred.iter},
wenzelm@55437
   367
  [@{typ natural}, @{typ natural}, @{typ Random.seed}] --->
bulwahn@45461
   368
    Predicate_Comp_Funs.mk_monadT T), tl additional_arguments)),
bulwahn@36019
   369
  modify_funT = (fn T =>
bulwahn@36019
   370
    let
bulwahn@36019
   371
      val (Ts, U) = strip_type T
haftmann@51143
   372
      val Ts' = [@{typ natural}, @{typ natural}, @{typ natural},
haftmann@51126
   373
        @{typ Random.seed}]
bulwahn@36019
   374
    in (Ts @ Ts') ---> U end),
bulwahn@36019
   375
  additional_arguments = (fn names =>
bulwahn@36019
   376
    let
bulwahn@36019
   377
      val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"]
bulwahn@36019
   378
    in
haftmann@51143
   379
      [Free (depth, @{typ natural}), Free (nrandom, @{typ natural}),
haftmann@51143
   380
        Free (size, @{typ natural}), Free (seed, @{typ Random.seed})]
bulwahn@36019
   381
    end),
bulwahn@36019
   382
  wrap_compilation =
haftmann@50056
   383
  fn compfuns => fn _ => fn T => fn mode => fn additional_arguments => fn compilation =>
bulwahn@36019
   384
    let
bulwahn@36019
   385
      val depth = hd (additional_arguments)
bulwahn@36019
   386
      val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE))
bulwahn@36019
   387
        mode (binder_types T)
bulwahn@45461
   388
      val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts)
bulwahn@36019
   389
      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
bulwahn@36019
   390
    in
haftmann@51143
   391
      if_const $ HOLogic.mk_eq (depth, @{term "0 :: natural"})
bulwahn@45461
   392
        $ mk_empty compfuns (dest_monadT compfuns T')
bulwahn@36019
   393
        $ compilation
bulwahn@36019
   394
    end,
bulwahn@36019
   395
  transform_additional_arguments =
haftmann@50056
   396
    fn _ => fn additional_arguments =>
bulwahn@36019
   397
    let
bulwahn@36019
   398
      val [depth, nrandom, size, seed] = additional_arguments
bulwahn@36019
   399
      val depth' =
haftmann@51143
   400
        Const (@{const_name Groups.minus}, @{typ "natural => natural => natural"})
haftmann@51143
   401
          $ depth $ Const (@{const_name Groups.one}, @{typ "natural"})
bulwahn@36019
   402
    in [depth', nrandom, size, seed] end
bulwahn@36019
   403
}
bulwahn@36019
   404
bulwahn@36019
   405
val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
bulwahn@36019
   406
  {
bulwahn@36019
   407
  compilation = Pred,
bulwahn@36019
   408
  function_name_prefix = "",
bulwahn@45450
   409
  compfuns = Predicate_Comp_Funs.compfuns,
bulwahn@36019
   410
  mk_random = (fn _ => error "no random generation"),
bulwahn@36019
   411
  modify_funT = I,
bulwahn@36019
   412
  additional_arguments = K [],
bulwahn@36019
   413
  wrap_compilation = K (K (K (K (K I))))
bulwahn@36019
   414
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
bulwahn@36019
   415
  transform_additional_arguments = K I : (indprem -> term list -> term list)
bulwahn@36019
   416
  }
bulwahn@36019
   417
bulwahn@36019
   418
val dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
bulwahn@36019
   419
  {
bulwahn@36019
   420
  compilation = DSeq,
bulwahn@36019
   421
  function_name_prefix = "dseq_",
bulwahn@36019
   422
  compfuns = DSequence_CompFuns.compfuns,
bulwahn@40051
   423
  mk_random = (fn _ => error "no random generation in dseq"),
bulwahn@36019
   424
  modify_funT = I,
bulwahn@36019
   425
  additional_arguments = K [],
bulwahn@36019
   426
  wrap_compilation = K (K (K (K (K I))))
bulwahn@36019
   427
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
bulwahn@36019
   428
  transform_additional_arguments = K I : (indprem -> term list -> term list)
bulwahn@36019
   429
  }
bulwahn@36019
   430
bulwahn@36019
   431
val pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
bulwahn@36019
   432
  {
bulwahn@36019
   433
  compilation = Pos_Random_DSeq,
bulwahn@36019
   434
  function_name_prefix = "random_dseq_",
bulwahn@36019
   435
  compfuns = Random_Sequence_CompFuns.compfuns,
haftmann@50056
   436
  mk_random = (fn T => fn _ =>
bulwahn@36019
   437
  let
haftmann@51126
   438
    val random = Const (@{const_name Quickcheck_Random.random},
haftmann@51143
   439
      @{typ natural} --> @{typ Random.seed} -->
bulwahn@36019
   440
        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
bulwahn@36019
   441
  in
haftmann@51143
   442
    Const (@{const_name Random_Sequence.Random}, (@{typ natural} --> @{typ Random.seed} -->
bulwahn@36019
   443
      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
bulwahn@36019
   444
      Random_Sequence_CompFuns.mk_random_dseqT T) $ random
bulwahn@36019
   445
  end),
bulwahn@36019
   446
bulwahn@36019
   447
  modify_funT = I,
bulwahn@36019
   448
  additional_arguments = K [],
bulwahn@36019
   449
  wrap_compilation = K (K (K (K (K I))))
bulwahn@36019
   450
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
bulwahn@36019
   451
  transform_additional_arguments = K I : (indprem -> term list -> term list)
bulwahn@36019
   452
  }
bulwahn@36019
   453
bulwahn@36019
   454
val neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
bulwahn@36019
   455
  {
bulwahn@36019
   456
  compilation = Neg_Random_DSeq,
bulwahn@36019
   457
  function_name_prefix = "random_dseq_neg_",
bulwahn@36019
   458
  compfuns = Random_Sequence_CompFuns.compfuns,
bulwahn@36019
   459
  mk_random = (fn _ => error "no random generation"),
bulwahn@36019
   460
  modify_funT = I,
bulwahn@36019
   461
  additional_arguments = K [],
bulwahn@36019
   462
  wrap_compilation = K (K (K (K (K I))))
bulwahn@36019
   463
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
bulwahn@36019
   464
  transform_additional_arguments = K I : (indprem -> term list -> term list)
bulwahn@36019
   465
  }
bulwahn@36019
   466
bulwahn@36019
   467
bulwahn@36019
   468
val new_pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
bulwahn@36019
   469
  {
bulwahn@36019
   470
  compilation = New_Pos_Random_DSeq,
bulwahn@36019
   471
  function_name_prefix = "new_random_dseq_",
bulwahn@40049
   472
  compfuns = New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns,
haftmann@50056
   473
  mk_random = (fn T => fn _ =>
bulwahn@36019
   474
  let
haftmann@51126
   475
    val random = Const (@{const_name Quickcheck_Random.random},
haftmann@51143
   476
      @{typ natural} --> @{typ Random.seed} -->
bulwahn@36019
   477
        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
bulwahn@36019
   478
  in
haftmann@51143
   479
    Const (@{const_name Random_Sequence.pos_Random}, (@{typ natural} --> @{typ Random.seed} -->
bulwahn@36019
   480
      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
bulwahn@36019
   481
      New_Pos_Random_Sequence_CompFuns.mk_pos_random_dseqT T) $ random
bulwahn@36019
   482
  end),
bulwahn@36019
   483
  modify_funT = I,
bulwahn@36019
   484
  additional_arguments = K [],
bulwahn@36019
   485
  wrap_compilation = K (K (K (K (K I))))
bulwahn@36019
   486
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
bulwahn@36019
   487
  transform_additional_arguments = K I : (indprem -> term list -> term list)
bulwahn@36019
   488
  }
bulwahn@36019
   489
bulwahn@36019
   490
val new_neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
bulwahn@36019
   491
  {
bulwahn@36019
   492
  compilation = New_Neg_Random_DSeq,
bulwahn@36019
   493
  function_name_prefix = "new_random_dseq_neg_",
bulwahn@40049
   494
  compfuns = New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns,
bulwahn@36019
   495
  mk_random = (fn _ => error "no random generation"),
bulwahn@36019
   496
  modify_funT = I,
bulwahn@36019
   497
  additional_arguments = K [],
bulwahn@36019
   498
  wrap_compilation = K (K (K (K (K I))))
bulwahn@36019
   499
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
bulwahn@36019
   500
  transform_additional_arguments = K I : (indprem -> term list -> term list)
bulwahn@36019
   501
  }
bulwahn@36019
   502
bulwahn@40051
   503
val pos_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
bulwahn@40051
   504
  {
bulwahn@40051
   505
  compilation = Pos_Generator_DSeq,
bulwahn@40051
   506
  function_name_prefix = "generator_dseq_",
bulwahn@40051
   507
  compfuns = New_Pos_DSequence_CompFuns.depth_limited_compfuns,
bulwahn@40051
   508
  mk_random =
haftmann@50056
   509
    (fn T => fn _ =>
bulwahn@45214
   510
      Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"},
haftmann@51143
   511
        @{typ "natural"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T]))),
bulwahn@40051
   512
  modify_funT = I,
bulwahn@40051
   513
  additional_arguments = K [],
bulwahn@40051
   514
  wrap_compilation = K (K (K (K (K I))))
bulwahn@40051
   515
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
bulwahn@40051
   516
  transform_additional_arguments = K I : (indprem -> term list -> term list)
bulwahn@40051
   517
  }
wenzelm@55437
   518
bulwahn@40051
   519
val neg_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
bulwahn@40051
   520
  {
bulwahn@40051
   521
  compilation = Neg_Generator_DSeq,
bulwahn@40051
   522
  function_name_prefix = "generator_dseq_neg_",
bulwahn@40051
   523
  compfuns = New_Neg_DSequence_CompFuns.depth_limited_compfuns,
bulwahn@40051
   524
  mk_random = (fn _ => error "no random generation"),
bulwahn@40051
   525
  modify_funT = I,
bulwahn@40051
   526
  additional_arguments = K [],
bulwahn@40051
   527
  wrap_compilation = K (K (K (K (K I))))
bulwahn@40051
   528
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
bulwahn@40051
   529
  transform_additional_arguments = K I : (indprem -> term list -> term list)
bulwahn@40051
   530
  }
bulwahn@40051
   531
bulwahn@45450
   532
val pos_generator_cps_comp_modifiers = Comp_Mod.Comp_Modifiers
bulwahn@45450
   533
  {
bulwahn@45450
   534
  compilation = Pos_Generator_CPS,
bulwahn@45450
   535
  function_name_prefix = "generator_cps_pos_",
bulwahn@45450
   536
  compfuns = Pos_Bounded_CPS_Comp_Funs.compfuns,
bulwahn@45450
   537
  mk_random =
haftmann@50056
   538
    (fn T => fn _ =>
bulwahn@45450
   539
       Const (@{const_name "Quickcheck_Exhaustive.exhaustive"},
bulwahn@45750
   540
       (T --> @{typ "(bool * term list) option"}) -->
haftmann@51143
   541
         @{typ "natural => (bool * term list) option"})),
bulwahn@45450
   542
  modify_funT = I,
bulwahn@45450
   543
  additional_arguments = K [],
bulwahn@45450
   544
  wrap_compilation = K (K (K (K (K I))))
bulwahn@45450
   545
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
bulwahn@45450
   546
  transform_additional_arguments = K I : (indprem -> term list -> term list)
wenzelm@55437
   547
  }
bulwahn@45450
   548
bulwahn@45450
   549
val neg_generator_cps_comp_modifiers = Comp_Mod.Comp_Modifiers
bulwahn@45450
   550
  {
bulwahn@45450
   551
  compilation = Neg_Generator_CPS,
bulwahn@45450
   552
  function_name_prefix = "generator_cps_neg_",
bulwahn@45450
   553
  compfuns = Neg_Bounded_CPS_Comp_Funs.compfuns,
bulwahn@45450
   554
  mk_random = (fn _ => error "No enumerators"),
bulwahn@45450
   555
  modify_funT = I,
bulwahn@45450
   556
  additional_arguments = K [],
bulwahn@45450
   557
  wrap_compilation = K (K (K (K (K I))))
bulwahn@45450
   558
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
bulwahn@45450
   559
  transform_additional_arguments = K I : (indprem -> term list -> term list)
bulwahn@45450
   560
  }
wenzelm@55437
   561
bulwahn@36019
   562
fun negative_comp_modifiers_of comp_modifiers =
wenzelm@55437
   563
  (case Comp_Mod.compilation comp_modifiers of
wenzelm@55437
   564
    Pos_Random_DSeq => neg_random_dseq_comp_modifiers
wenzelm@55437
   565
  | Neg_Random_DSeq => pos_random_dseq_comp_modifiers
wenzelm@55437
   566
  | New_Pos_Random_DSeq => new_neg_random_dseq_comp_modifiers
wenzelm@55437
   567
  | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers
wenzelm@55437
   568
  | Pos_Generator_DSeq => neg_generator_dseq_comp_modifiers
wenzelm@55437
   569
  | Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers
wenzelm@55437
   570
  | Pos_Generator_CPS => neg_generator_cps_comp_modifiers
wenzelm@55437
   571
  | Neg_Generator_CPS => pos_generator_cps_comp_modifiers
wenzelm@55437
   572
  | _ => comp_modifiers)
wenzelm@55437
   573
bulwahn@36019
   574
bulwahn@32667
   575
(* term construction *)
bulwahn@32667
   576
wenzelm@55437
   577
fun mk_v (names, vs) s T =
wenzelm@55437
   578
  (case AList.lookup (op =) vs s of
wenzelm@55437
   579
    NONE => (Free (s, T), (names, (s, [])::vs))
wenzelm@55437
   580
  | SOME xs =>
wenzelm@55437
   581
      let
wenzelm@55437
   582
        val s' = singleton (Name.variant_list names) s;
wenzelm@55437
   583
        val v = Free (s', T)
wenzelm@55437
   584
      in
wenzelm@55437
   585
        (v, (s'::names, AList.update (op =) (s, v::xs) vs))
wenzelm@55437
   586
      end);
bulwahn@32667
   587
bulwahn@32667
   588
fun distinct_v (Free (s, T)) nvs = mk_v nvs s T
bulwahn@32667
   589
  | distinct_v (t $ u) nvs =
bulwahn@32667
   590
      let
bulwahn@32667
   591
        val (t', nvs') = distinct_v t nvs;
bulwahn@32667
   592
        val (u', nvs'') = distinct_v u nvs';
bulwahn@32667
   593
      in (t' $ u', nvs'') end
bulwahn@32667
   594
  | distinct_v x nvs = (x, nvs);
bulwahn@32667
   595
bulwahn@33147
   596
bulwahn@39648
   597
(** specific rpred functions -- move them to the correct place in this file *)
haftmann@50056
   598
fun mk_Eval_of (P as (Free _), T) mode =
wenzelm@44241
   599
  let
wenzelm@44241
   600
    fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i =
wenzelm@44241
   601
          let
wenzelm@55437
   602
            val (bs2, i') = mk_bounds T2 i
wenzelm@44241
   603
            val (bs1, i'') = mk_bounds T1 i'
wenzelm@44241
   604
          in
wenzelm@44241
   605
            (HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1)
wenzelm@44241
   606
          end
haftmann@50056
   607
      | mk_bounds _ i = (Bound i, i + 1)
wenzelm@44241
   608
    fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2))
wenzelm@44241
   609
    fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT)
wenzelm@44241
   610
      | mk_tuple tTs = foldr1 mk_prod tTs
wenzelm@44241
   611
    fun mk_split_abs (T as Type (@{type_name Product_Type.prod}, [T1, T2])) t =
wenzelm@44241
   612
          absdummy T
haftmann@61424
   613
            (HOLogic.case_prod_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t)))
wenzelm@44241
   614
      | mk_split_abs T t = absdummy T t
wenzelm@44241
   615
    val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
wenzelm@44241
   616
    val (inargs, outargs) = split_mode mode args
haftmann@50056
   617
    val (_, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
bulwahn@45450
   618
    val inner_term = Predicate_Comp_Funs.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
wenzelm@44241
   619
  in
wenzelm@44241
   620
    fold_rev mk_split_abs (binder_types T) inner_term
wenzelm@44241
   621
  end
bulwahn@33147
   622
wenzelm@55437
   623
fun compile_arg compilation_modifiers _ _ param_modes arg =
bulwahn@33147
   624
  let
bulwahn@33147
   625
    fun map_params (t as Free (f, T)) =
wenzelm@55437
   626
          (case (AList.lookup (op =) param_modes f) of
wenzelm@55437
   627
              SOME mode =>
wenzelm@55437
   628
                let
wenzelm@55437
   629
                  val T' = Comp_Mod.funT_of compilation_modifiers mode T
wenzelm@55437
   630
                in
wenzelm@55437
   631
                  mk_Eval_of (Free (f, T'), T) mode
wenzelm@55437
   632
                end
wenzelm@55437
   633
          | NONE => t)
bulwahn@33147
   634
      | map_params t = t
bulwahn@39648
   635
  in
bulwahn@39648
   636
    map_aterms map_params arg
bulwahn@39648
   637
  end
bulwahn@33147
   638
bulwahn@39648
   639
fun compile_match compilation_modifiers additional_arguments ctxt param_modes
bulwahn@39648
   640
      eqs eqs' out_ts success_t =
bulwahn@32667
   641
  let
bulwahn@36019
   642
    val compfuns = Comp_Mod.compfuns compilation_modifiers
bulwahn@32667
   643
    val eqs'' = maps mk_eq eqs @ eqs'
bulwahn@33147
   644
    val eqs'' =
bulwahn@39648
   645
      map (compile_arg compilation_modifiers additional_arguments ctxt param_modes) eqs''
bulwahn@32667
   646
    val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
wenzelm@43324
   647
    val name = singleton (Name.variant_list names) "x";
wenzelm@43324
   648
    val name' = singleton (Name.variant_list (name :: names)) "y";
bulwahn@33148
   649
    val T = HOLogic.mk_tupleT (map fastype_of out_ts);
bulwahn@32667
   650
    val U = fastype_of success_t;
bulwahn@45461
   651
    val U' = dest_monadT compfuns U;
bulwahn@32667
   652
    val v = Free (name, T);
bulwahn@32667
   653
    val v' = Free (name', T);
bulwahn@32667
   654
  in
traytel@51673
   655
    lambda v (Case_Translation.make_case ctxt Case_Translation.Quiet Name.context v
bulwahn@33148
   656
      [(HOLogic.mk_tuple out_ts,
bulwahn@32667
   657
        if null eqs'' then success_t
bulwahn@32667
   658
        else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
bulwahn@32667
   659
          foldr1 HOLogic.mk_conj eqs'' $ success_t $
bulwahn@45461
   660
            mk_empty compfuns U'),
bulwahn@45461
   661
       (v', mk_empty compfuns U')])
bulwahn@32667
   662
  end;
bulwahn@32667
   663
bulwahn@39648
   664
fun compile_expr compilation_modifiers ctxt (t, deriv) param_modes additional_arguments =
bulwahn@32667
   665
  let
bulwahn@36019
   666
    val compfuns = Comp_Mod.compfuns compilation_modifiers
bulwahn@34948
   667
    fun expr_of (t, deriv) =
bulwahn@34948
   668
      (case (t, deriv) of
wenzelm@55437
   669
        (t, Term Input) =>
wenzelm@55437
   670
          SOME (compile_arg compilation_modifiers additional_arguments ctxt param_modes t)
haftmann@50056
   671
      | (_, Term Output) => NONE
bulwahn@34948
   672
      | (Const (name, T), Context mode) =>
wenzelm@61114
   673
          (case Core_Data.alternative_compilation_of ctxt name mode of
wenzelm@55437
   674
            SOME alt_comp => SOME (alt_comp compfuns T)
wenzelm@55437
   675
          | NONE =>
wenzelm@61114
   676
            SOME (Const (Core_Data.function_name_of (Comp_Mod.compilation compilation_modifiers)
wenzelm@55437
   677
              ctxt name mode,
wenzelm@55437
   678
              Comp_Mod.funT_of compilation_modifiers mode T)))
bulwahn@34948
   679
      | (Free (s, T), Context m) =>
wenzelm@55437
   680
          (case (AList.lookup (op =) param_modes s) of
wenzelm@55437
   681
            SOME _ => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
wenzelm@55437
   682
          | NONE =>
wenzelm@55437
   683
              let
wenzelm@55437
   684
                val bs = map (pair "x") (binder_types (fastype_of t))
wenzelm@55437
   685
                val bounds = map Bound (rev (0 upto (length bs) - 1))
wenzelm@55437
   686
              in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end)
haftmann@50056
   687
      | (t, Context _) =>
wenzelm@55437
   688
          let
wenzelm@55437
   689
            val bs = map (pair "x") (binder_types (fastype_of t))
wenzelm@55437
   690
            val bounds = map Bound (rev (0 upto (length bs) - 1))
wenzelm@55437
   691
          in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end
haftmann@37391
   692
      | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
wenzelm@55437
   693
          (case (expr_of (t1, d1), expr_of (t2, d2)) of
wenzelm@55437
   694
            (NONE, NONE) => NONE
wenzelm@55437
   695
          | (NONE, SOME t) => SOME t
wenzelm@55437
   696
          | (SOME t, NONE) => SOME t
wenzelm@55437
   697
          | (SOME t1, SOME t2) => SOME (HOLogic.mk_prod (t1, t2)))
bulwahn@34948
   698
      | (t1 $ t2, Mode_App (deriv1, deriv2)) =>
wenzelm@55437
   699
          (case (expr_of (t1, deriv1), expr_of (t2, deriv2)) of
wenzelm@55437
   700
            (SOME t, NONE) => SOME t
wenzelm@55437
   701
           | (SOME t, SOME u) => SOME (t $ u)
wenzelm@55437
   702
           | _ => error "something went wrong here!"))
bulwahn@32667
   703
  in
bulwahn@35879
   704
    list_comb (the (expr_of (t, deriv)), additional_arguments)
bulwahn@34948
   705
  end
bulwahn@33145
   706
bulwahn@39648
   707
fun compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments
bulwahn@39648
   708
  inp (in_ts, out_ts) moded_ps =
bulwahn@32667
   709
  let
bulwahn@36019
   710
    val compfuns = Comp_Mod.compfuns compilation_modifiers
bulwahn@36019
   711
    val compile_match = compile_match compilation_modifiers
bulwahn@39648
   712
      additional_arguments ctxt param_modes
bulwahn@32667
   713
    val (in_ts', (all_vs', eqs)) =
bulwahn@35891
   714
      fold_map (collect_non_invertible_subterms ctxt) in_ts (all_vs, []);
bulwahn@32667
   715
    fun compile_prems out_ts' vs names [] =
bulwahn@32667
   716
          let
bulwahn@32667
   717
            val (out_ts'', (names', eqs')) =
bulwahn@35891
   718
              fold_map (collect_non_invertible_subterms ctxt) out_ts' (names, []);
haftmann@50056
   719
            val (out_ts''', (_, constr_vs)) = fold_map distinct_v
bulwahn@32667
   720
              out_ts'' (names', map (rpair []) vs);
bulwahn@39762
   721
            val processed_out_ts = map (compile_arg compilation_modifiers additional_arguments
bulwahn@39762
   722
              ctxt param_modes) out_ts
bulwahn@32667
   723
          in
bulwahn@33147
   724
            compile_match constr_vs (eqs @ eqs') out_ts'''
bulwahn@39762
   725
              (mk_single compfuns (HOLogic.mk_tuple processed_out_ts))
bulwahn@32667
   726
          end
bulwahn@34948
   727
      | compile_prems out_ts vs names ((p, deriv) :: ps) =
bulwahn@32667
   728
          let
bulwahn@32667
   729
            val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
bulwahn@32667
   730
            val (out_ts', (names', eqs)) =
bulwahn@35891
   731
              fold_map (collect_non_invertible_subterms ctxt) out_ts (names, [])
bulwahn@32667
   732
            val (out_ts'', (names'', constr_vs')) = fold_map distinct_v
bulwahn@32667
   733
              out_ts' ((names', map (rpair []) vs))
bulwahn@34948
   734
            val mode = head_mode_of deriv
bulwahn@33143
   735
            val additional_arguments' =
bulwahn@33330
   736
              Comp_Mod.transform_additional_arguments compilation_modifiers p additional_arguments
wenzelm@55437
   737
            val (compiled_clause, rest) =
wenzelm@55437
   738
              (case p of
wenzelm@55437
   739
                Prem t =>
wenzelm@55437
   740
                  let
wenzelm@55437
   741
                    val u =
wenzelm@55437
   742
                      compile_expr compilation_modifiers ctxt (t, deriv)
wenzelm@55437
   743
                       param_modes additional_arguments'
wenzelm@55437
   744
                    val (_, out_ts''') = split_mode mode (snd (strip_comb t))
wenzelm@55437
   745
                    val rest = compile_prems out_ts''' vs' names'' ps
wenzelm@55437
   746
                  in
wenzelm@55437
   747
                    (u, rest)
wenzelm@55437
   748
                  end
wenzelm@55437
   749
              | Negprem t =>
wenzelm@55437
   750
                  let
wenzelm@55437
   751
                    val neg_compilation_modifiers =
wenzelm@55437
   752
                      negative_comp_modifiers_of compilation_modifiers
wenzelm@55437
   753
                    val u =
wenzelm@55437
   754
                     mk_not compfuns
wenzelm@55437
   755
                       (compile_expr neg_compilation_modifiers ctxt (t, deriv)
wenzelm@55437
   756
                         param_modes additional_arguments')
wenzelm@55437
   757
                    val (_, out_ts''') = split_mode mode (snd (strip_comb t))
wenzelm@55437
   758
                    val rest = compile_prems out_ts''' vs' names'' ps
wenzelm@55437
   759
                  in
wenzelm@55437
   760
                    (u, rest)
wenzelm@55437
   761
                  end
wenzelm@55437
   762
              | Sidecond t =>
wenzelm@55437
   763
                  let
wenzelm@55437
   764
                    val t = compile_arg compilation_modifiers additional_arguments
wenzelm@55437
   765
                      ctxt param_modes t
wenzelm@55437
   766
                    val rest = compile_prems [] vs' names'' ps;
wenzelm@55437
   767
                  in
wenzelm@55437
   768
                    (mk_if compfuns t, rest)
wenzelm@55437
   769
                  end
wenzelm@55437
   770
              | Generator (v, T) =>
wenzelm@55437
   771
                  let
wenzelm@55437
   772
                    val u = Comp_Mod.mk_random compilation_modifiers T additional_arguments
wenzelm@55437
   773
                    val rest = compile_prems [Free (v, T)]  vs' names'' ps;
wenzelm@55437
   774
                  in
wenzelm@55437
   775
                    (u, rest)
wenzelm@55437
   776
                  end)
bulwahn@32667
   777
          in
bulwahn@33147
   778
            compile_match constr_vs' eqs out_ts''
bulwahn@32667
   779
              (mk_bind compfuns (compiled_clause, rest))
bulwahn@32667
   780
          end
wenzelm@55437
   781
    val prem_t = compile_prems in_ts' (map fst param_modes) all_vs' moded_ps
bulwahn@32667
   782
  in
bulwahn@32667
   783
    mk_bind compfuns (mk_single compfuns inp, prem_t)
bulwahn@32667
   784
  end
bulwahn@32667
   785
wenzelm@55437
   786
bulwahn@36254
   787
(* switch detection *)
bulwahn@36254
   788
bulwahn@36254
   789
(** argument position of an inductive predicates and the executable functions **)
bulwahn@36254
   790
bulwahn@36254
   791
type position = int * int list
bulwahn@36254
   792
bulwahn@36254
   793
fun input_positions_pair Input = [[]]
bulwahn@36254
   794
  | input_positions_pair Output = []
bulwahn@36254
   795
  | input_positions_pair (Fun _) = []
bulwahn@36254
   796
  | input_positions_pair (Pair (m1, m2)) =
wenzelm@55437
   797
      map (cons 1) (input_positions_pair m1) @ map (cons 2) (input_positions_pair m2)
bulwahn@36254
   798
wenzelm@55437
   799
fun input_positions_of_mode mode =
wenzelm@55437
   800
  flat
wenzelm@55437
   801
    (map_index
wenzelm@55437
   802
      (fn (i, Input) => [(i, [])]
wenzelm@55437
   803
        | (_, Output) => []
wenzelm@55437
   804
        | (_, Fun _) => []
wenzelm@55437
   805
        | (i, m as Pair _) => map (pair i) (input_positions_pair m))
wenzelm@55437
   806
      (Predicate_Compile_Aux.strip_fun_mode mode))
bulwahn@36254
   807
haftmann@50056
   808
fun argument_position_pair _ [] = []
bulwahn@36254
   809
  | argument_position_pair (Pair (Fun _, m2)) (2 :: is) = argument_position_pair m2 is
bulwahn@36254
   810
  | argument_position_pair (Pair (m1, m2)) (i :: is) =
wenzelm@55437
   811
      (if eq_mode (m1, Output) andalso i = 2 then
wenzelm@55437
   812
        argument_position_pair m2 is
wenzelm@55437
   813
      else if eq_mode (m2, Output) andalso i = 1 then
wenzelm@55437
   814
        argument_position_pair m1 is
wenzelm@55437
   815
      else (i :: argument_position_pair (if i = 1 then m1 else m2) is))
bulwahn@36254
   816
bulwahn@36254
   817
fun argument_position_of mode (i, is) =
bulwahn@36254
   818
  (i - (length (filter (fn Output => true | Fun _ => true | _ => false)
bulwahn@36254
   819
    (List.take (strip_fun_mode mode, i)))),
bulwahn@36254
   820
  argument_position_pair (nth (strip_fun_mode mode) i) is)
bulwahn@36254
   821
bulwahn@36254
   822
fun nth_pair [] t = t
bulwahn@36254
   823
  | nth_pair (1 :: is) (Const (@{const_name Pair}, _) $ t1 $ _) = nth_pair is t1
bulwahn@36254
   824
  | nth_pair (2 :: is) (Const (@{const_name Pair}, _) $ _ $ t2) = nth_pair is t2
bulwahn@36254
   825
  | nth_pair _ _ = raise Fail "unexpected input for nth_tuple"
bulwahn@36254
   826
wenzelm@55437
   827
bulwahn@36254
   828
(** switch detection analysis **)
bulwahn@36254
   829
haftmann@50056
   830
fun find_switch_test ctxt (i, is) (ts, _) =
bulwahn@36254
   831
  let
bulwahn@36254
   832
    val t = nth_pair is (nth ts i)
bulwahn@36254
   833
    val T = fastype_of t
bulwahn@36254
   834
  in
wenzelm@55437
   835
    (case T of
bulwahn@36254
   836
      TFree _ => NONE
bulwahn@36254
   837
    | Type (Tcon, _) =>
wenzelm@55440
   838
        (case Ctr_Sugar.ctr_sugar_of ctxt Tcon of
wenzelm@55437
   839
          NONE => NONE
wenzelm@55440
   840
        | SOME {ctrs, ...} =>
wenzelm@55437
   841
            (case strip_comb t of
wenzelm@55437
   842
              (Var _, []) => NONE
wenzelm@55437
   843
            | (Free _, []) => NONE
wenzelm@55440
   844
            | (Const (c, T), _) =>
wenzelm@55440
   845
                if AList.defined (op =) (map_filter (try dest_Const) ctrs) c
wenzelm@55440
   846
                then SOME (c, T) else NONE)))
bulwahn@36254
   847
  end
bulwahn@36254
   848
bulwahn@37005
   849
fun partition_clause ctxt pos moded_clauses =
bulwahn@36254
   850
  let
bulwahn@36254
   851
    fun insert_list eq (key, value) = AList.map_default eq (key, []) (cons value)
bulwahn@36254
   852
    fun find_switch_test' moded_clause (cases, left) =
wenzelm@55437
   853
      (case find_switch_test ctxt pos moded_clause of
bulwahn@36254
   854
        SOME (c, T) => (insert_list (op =) ((c, T), moded_clause) cases, left)
wenzelm@55437
   855
      | NONE => (cases, moded_clause :: left))
bulwahn@36254
   856
  in
bulwahn@36254
   857
    fold find_switch_test' moded_clauses ([], [])
bulwahn@36254
   858
  end
bulwahn@36254
   859
bulwahn@36254
   860
datatype switch_tree =
bulwahn@36254
   861
  Atom of moded_clause list | Node of (position * ((string * typ) * switch_tree) list) * switch_tree
bulwahn@36254
   862
bulwahn@37005
   863
fun mk_switch_tree ctxt mode moded_clauses =
bulwahn@36254
   864
  let
bulwahn@36254
   865
    fun select_best_switch moded_clauses input_position best_switch =
bulwahn@36254
   866
      let
wenzelm@59058
   867
        val ord = option_ord (rev_order o int_ord o (apply2 (length o snd o snd)))
bulwahn@37005
   868
        val partition = partition_clause ctxt input_position moded_clauses
bulwahn@36254
   869
        val switch = if (length (fst partition) > 1) then SOME (input_position, partition) else NONE
bulwahn@36254
   870
      in
wenzelm@55437
   871
        (case ord (switch, best_switch) of
wenzelm@55437
   872
          LESS => best_switch
wenzelm@55437
   873
        | EQUAL => best_switch
wenzelm@55437
   874
        | GREATER => switch)
bulwahn@36254
   875
      end
bulwahn@36254
   876
    fun detect_switches moded_clauses =
wenzelm@55437
   877
      (case fold (select_best_switch moded_clauses) (input_positions_of_mode mode) NONE of
bulwahn@36254
   878
        SOME (best_pos, (switched_on, left_clauses)) =>
bulwahn@36254
   879
          Node ((best_pos, map (apsnd detect_switches) switched_on),
bulwahn@36254
   880
            detect_switches left_clauses)
wenzelm@55437
   881
      | NONE => Atom moded_clauses)
bulwahn@36254
   882
  in
bulwahn@36254
   883
    detect_switches moded_clauses
bulwahn@36254
   884
  end
bulwahn@36254
   885
wenzelm@55437
   886
bulwahn@36254
   887
(** compilation of detected switches **)
bulwahn@36254
   888
bulwahn@36254
   889
fun destruct_constructor_pattern (pat, obj) =
bulwahn@36254
   890
  (case strip_comb pat of
wenzelm@55437
   891
      (Free _, []) => cons (pat, obj)
bulwahn@36254
   892
  | (Const (c, T), pat_args) =>
wenzelm@55437
   893
      (case strip_comb obj of
wenzelm@55437
   894
        (Const (c', T'), obj_args) =>
wenzelm@55437
   895
          (if c = c' andalso T = T' then
wenzelm@55437
   896
            fold destruct_constructor_pattern (pat_args ~~ obj_args)
wenzelm@55437
   897
          else raise Fail "pattern and object mismatch")
wenzelm@55437
   898
      | _ => raise Fail "unexpected object")
bulwahn@36254
   899
  | _ => raise Fail "unexpected pattern")
bulwahn@36254
   900
bulwahn@39648
   901
fun compile_switch compilation_modifiers ctxt all_vs param_modes additional_arguments mode
bulwahn@36254
   902
  in_ts' outTs switch_tree =
bulwahn@36254
   903
  let
bulwahn@36254
   904
    val compfuns = Comp_Mod.compfuns compilation_modifiers
wenzelm@42361
   905
    val thy = Proof_Context.theory_of ctxt
bulwahn@36254
   906
    fun compile_switch_tree _ _ (Atom []) = NONE
bulwahn@36254
   907
      | compile_switch_tree all_vs ctxt_eqs (Atom moded_clauses) =
bulwahn@36254
   908
        let
bulwahn@36254
   909
          val in_ts' = map (Pattern.rewrite_term thy ctxt_eqs []) in_ts'
bulwahn@36254
   910
          fun compile_clause' (ts, moded_ps) =
bulwahn@36254
   911
            let
bulwahn@36254
   912
              val (ts, out_ts) = split_mode mode ts
bulwahn@36254
   913
              val subst = fold destruct_constructor_pattern (in_ts' ~~ ts) []
bulwahn@36254
   914
              val (fsubst, pat') = List.partition (fn (_, Free _) => true | _ => false) subst
bulwahn@36254
   915
              val moded_ps' = (map o apfst o map_indprem)
bulwahn@36254
   916
                (Pattern.rewrite_term thy (map swap fsubst) []) moded_ps
bulwahn@36254
   917
              val inp = HOLogic.mk_tuple (map fst pat')
bulwahn@36254
   918
              val in_ts' = map (Pattern.rewrite_term thy (map swap fsubst) []) (map snd pat')
bulwahn@36254
   919
              val out_ts' = map (Pattern.rewrite_term thy (map swap fsubst) []) out_ts
bulwahn@36254
   920
            in
bulwahn@39648
   921
              compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments
bulwahn@39648
   922
                inp (in_ts', out_ts') moded_ps'
bulwahn@36254
   923
            end
bulwahn@45461
   924
        in SOME (foldr1 (mk_plus compfuns) (map compile_clause' moded_clauses)) end
bulwahn@36254
   925
    | compile_switch_tree all_vs ctxt_eqs (Node ((position, switched_clauses), left_clauses)) =
bulwahn@36254
   926
      let
bulwahn@36254
   927
        val (i, is) = argument_position_of mode position
bulwahn@36254
   928
        val inp_var = nth_pair is (nth in_ts' i)
wenzelm@43324
   929
        val x = singleton (Name.variant_list all_vs) "x"
bulwahn@36254
   930
        val xt = Free (x, fastype_of inp_var)
bulwahn@36254
   931
        fun compile_single_case ((c, T), switched) =
bulwahn@36254
   932
          let
bulwahn@36254
   933
            val Ts = binder_types T
bulwahn@36254
   934
            val argnames = Name.variant_list (x :: all_vs)
bulwahn@36254
   935
              (map (fn i => "c" ^ string_of_int i) (1 upto length Ts))
bulwahn@36254
   936
            val args = map2 (curry Free) argnames Ts
bulwahn@36254
   937
            val pattern = list_comb (Const (c, T), args)
bulwahn@36254
   938
            val ctxt_eqs' = (inp_var, pattern) :: ctxt_eqs
bulwahn@45461
   939
            val compilation = the_default (mk_empty compfuns (HOLogic.mk_tupleT outTs))
bulwahn@36254
   940
              (compile_switch_tree (argnames @ x :: all_vs) ctxt_eqs' switched)
bulwahn@36254
   941
        in
bulwahn@36254
   942
          (pattern, compilation)
bulwahn@36254
   943
        end
traytel@51673
   944
        val switch = Case_Translation.make_case ctxt Case_Translation.Quiet Name.context inp_var
bulwahn@36254
   945
          ((map compile_single_case switched_clauses) @
bulwahn@45461
   946
            [(xt, mk_empty compfuns (HOLogic.mk_tupleT outTs))])
bulwahn@36254
   947
      in
wenzelm@55437
   948
        (case compile_switch_tree all_vs ctxt_eqs left_clauses of
bulwahn@36254
   949
          NONE => SOME switch
wenzelm@55437
   950
        | SOME left_comp => SOME (mk_plus compfuns (switch, left_comp)))
bulwahn@36254
   951
      end
bulwahn@36254
   952
  in
bulwahn@36254
   953
    compile_switch_tree all_vs [] switch_tree
bulwahn@36254
   954
  end
bulwahn@36254
   955
wenzelm@55437
   956
bulwahn@36254
   957
(* compilation of predicates *)
bulwahn@36254
   958
bulwahn@37005
   959
fun compile_pred options compilation_modifiers ctxt all_vs param_vs s T (pol, mode) moded_cls =
bulwahn@32667
   960
  let
wenzelm@55437
   961
    val is_terminating = false (* FIXME: requires an termination analysis *)
bulwahn@40049
   962
    val compilation_modifiers =
bulwahn@40049
   963
      (if pol then compilation_modifiers else
bulwahn@40049
   964
        negative_comp_modifiers_of compilation_modifiers)
bulwahn@40049
   965
      |> (if is_depth_limited_compilation (Comp_Mod.compilation compilation_modifiers) then
bulwahn@40049
   966
           (if is_terminating then
wenzelm@55437
   967
              (Comp_Mod.set_compfuns
wenzelm@55437
   968
                (unlimited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers)))
wenzelm@55437
   969
            else
wenzelm@55437
   970
              (Comp_Mod.set_compfuns
wenzelm@55437
   971
                (limited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers))))
wenzelm@55437
   972
          else I)
wenzelm@55437
   973
    val additional_arguments =
wenzelm@55437
   974
      Comp_Mod.additional_arguments compilation_modifiers (all_vs @ param_vs)
bulwahn@34948
   975
    val compfuns = Comp_Mod.compfuns compilation_modifiers
bulwahn@34948
   976
    fun is_param_type (T as Type ("fun",[_ , T'])) =
wenzelm@55437
   977
          is_some (try (dest_monadT compfuns) T) orelse is_param_type T'
bulwahn@45461
   978
      | is_param_type T = is_some (try (dest_monadT compfuns) T)
wenzelm@55437
   979
    val (inpTs, outTs) =
wenzelm@55437
   980
      split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode
wenzelm@55437
   981
        (binder_types T)
bulwahn@34948
   982
    val funT = Comp_Mod.funT_of compilation_modifiers mode T
wenzelm@55437
   983
    val (in_ts, _) =
wenzelm@55437
   984
      fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
wenzelm@55437
   985
        (fn T => fn (param_vs, names) =>
wenzelm@55437
   986
          if is_param_type T then
wenzelm@55437
   987
            (Free (hd param_vs, T), (tl param_vs, names))
wenzelm@55437
   988
          else
wenzelm@55437
   989
            let
wenzelm@55437
   990
              val new = singleton (Name.variant_list names) "x"
wenzelm@55437
   991
            in (Free (new, T), (param_vs, new :: names)) end)) inpTs
bulwahn@34948
   992
        (param_vs, (all_vs @ param_vs))
wenzelm@55437
   993
    val in_ts' =
wenzelm@55437
   994
      map_filter (map_filter_prod
wenzelm@55437
   995
        (fn t as Free (x, _) =>
wenzelm@55437
   996
          if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts
bulwahn@39648
   997
    val param_modes = param_vs ~~ ho_arg_modes_of mode
bulwahn@36254
   998
    val compilation =
bulwahn@36254
   999
      if detect_switches options then
bulwahn@45461
  1000
        the_default (mk_empty compfuns (HOLogic.mk_tupleT outTs))
bulwahn@39648
  1001
          (compile_switch compilation_modifiers ctxt all_vs param_modes additional_arguments mode
bulwahn@39648
  1002
            in_ts' outTs (mk_switch_tree ctxt mode moded_cls))
bulwahn@36254
  1003
      else
bulwahn@36254
  1004
        let
bulwahn@36254
  1005
          val cl_ts =
wenzelm@55437
  1006
            map (fn (ts, moded_prems) =>
bulwahn@39648
  1007
              compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments
wenzelm@55437
  1008
                (HOLogic.mk_tuple in_ts') (split_mode mode ts) moded_prems) moded_cls
bulwahn@36254
  1009
        in
bulwahn@36254
  1010
          Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments
bulwahn@36254
  1011
            (if null cl_ts then
bulwahn@45461
  1012
              mk_empty compfuns (HOLogic.mk_tupleT outTs)
bulwahn@36254
  1013
            else
bulwahn@45461
  1014
              foldr1 (mk_plus compfuns) cl_ts)
bulwahn@36254
  1015
        end
bulwahn@33143
  1016
    val fun_const =
wenzelm@61114
  1017
      Const (Core_Data.function_name_of (Comp_Mod.compilation compilation_modifiers) ctxt s mode, funT)
bulwahn@32667
  1018
  in
bulwahn@33143
  1019
    HOLogic.mk_Trueprop
bulwahn@34948
  1020
      (HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
wenzelm@55437
  1021
  end
wenzelm@55437
  1022
bulwahn@33143
  1023
bulwahn@32667
  1024
(* Definition of executable functions and their intro and elim rules *)
bulwahn@32667
  1025
haftmann@61424
  1026
fun strip_split_abs (Const (@{const_name case_prod}, _) $ t) = strip_split_abs t
bulwahn@34948
  1027
  | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
bulwahn@34948
  1028
  | strip_split_abs t = t
bulwahn@34948
  1029
haftmann@37678
  1030
fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names =
wenzelm@55437
  1031
      if eq_mode (m, Input) orelse eq_mode (m, Output) then
wenzelm@55437
  1032
        let
wenzelm@55437
  1033
          val x = singleton (Name.variant_list names) "x"
wenzelm@55437
  1034
        in
wenzelm@55437
  1035
          (Free (x, T), x :: names)
wenzelm@55437
  1036
        end
wenzelm@55437
  1037
      else
wenzelm@55437
  1038
        let
wenzelm@55437
  1039
          val (t1, names') = mk_args is_eval (m1, T1) names
wenzelm@55437
  1040
          val (t2, names'') = mk_args is_eval (m2, T2) names'
wenzelm@55437
  1041
        in
wenzelm@55437
  1042
          (HOLogic.mk_prod (t1, t2), names'')
wenzelm@55437
  1043
        end
wenzelm@55437
  1044
  | mk_args is_eval ((m as Fun _), T) names =
wenzelm@55437
  1045
      let
wenzelm@55437
  1046
        val funT = funT_of Predicate_Comp_Funs.compfuns m T
wenzelm@55437
  1047
        val x = singleton (Name.variant_list names) "x"
wenzelm@55437
  1048
        val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
wenzelm@55437
  1049
        val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
wenzelm@55437
  1050
        val t = fold_rev HOLogic.tupled_lambda args (Predicate_Comp_Funs.mk_Eval
wenzelm@55437
  1051
          (list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs))
wenzelm@55437
  1052
      in
wenzelm@55437
  1053
        (if is_eval then t else Free (x, funT), x :: names)
wenzelm@55437
  1054
      end
wenzelm@55437
  1055
  | mk_args _ (_, T) names =
bulwahn@35324
  1056
      let
wenzelm@43324
  1057
        val x = singleton (Name.variant_list names) "x"
bulwahn@35324
  1058
      in
bulwahn@35324
  1059
        (Free (x, T), x :: names)
bulwahn@35324
  1060
      end
bulwahn@34948
  1061
bulwahn@37003
  1062
fun create_intro_elim_rule ctxt mode defthm mode_id funT pred =
bulwahn@34948
  1063
  let
bulwahn@34948
  1064
    val funtrm = Const (mode_id, funT)
bulwahn@34948
  1065
    val Ts = binder_types (fastype_of pred)
bulwahn@34948
  1066
    val (args, argnames) = fold_map (mk_args true) (strip_fun_mode mode ~~ Ts) []
bulwahn@34948
  1067
    fun strip_eval _ t =
bulwahn@34948
  1068
      let
bulwahn@34948
  1069
        val t' = strip_split_abs t
bulwahn@45450
  1070
        val (r, _) = Predicate_Comp_Funs.dest_Eval t'
bulwahn@34948
  1071
      in (SOME (fst (strip_comb r)), NONE) end
bulwahn@34948
  1072
    val (inargs, outargs) = split_map_mode strip_eval mode args
bulwahn@34948
  1073
    val eval_hoargs = ho_args_of mode args
bulwahn@34948
  1074
    val hoargTs = ho_argsT_of mode Ts
bulwahn@34948
  1075
    val hoarg_names' =
bulwahn@34948
  1076
      Name.variant_list argnames ((map (fn i => "x" ^ string_of_int i)) (1 upto (length hoargTs)))
bulwahn@34948
  1077
    val hoargs' = map2 (curry Free) hoarg_names' hoargTs
bulwahn@34948
  1078
    val args' = replace_ho_args mode hoargs' args
bulwahn@34948
  1079
    val predpropI = HOLogic.mk_Trueprop (list_comb (pred, args'))
bulwahn@34948
  1080
    val predpropE = HOLogic.mk_Trueprop (list_comb (pred, args))
bulwahn@34948
  1081
    val param_eqs = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) eval_hoargs hoargs'
bulwahn@45450
  1082
    val funpropE = HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval (list_comb (funtrm, inargs),
bulwahn@34948
  1083
                    if null outargs then Free("y", HOLogic.unitT) else HOLogic.mk_tuple outargs))
bulwahn@45450
  1084
    val funpropI = HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval (list_comb (funtrm, inargs),
bulwahn@34948
  1085
                     HOLogic.mk_tuple outargs))
bulwahn@34948
  1086
    val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
wenzelm@55437
  1087
    val simprules =
wenzelm@55437
  1088
      [defthm, @{thm eval_pred},
haftmann@61424
  1089
        @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm prod.collapse}]
wenzelm@51717
  1090
    val unfolddef_tac =
wenzelm@51717
  1091
      Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simprules) 1
bulwahn@37003
  1092
    val introthm = Goal.prove ctxt
bulwahn@34948
  1093
      (argnames @ hoarg_names' @ ["y"]) [] introtrm (fn _ => unfolddef_tac)
bulwahn@34948
  1094
    val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
bulwahn@34948
  1095
    val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
bulwahn@37003
  1096
    val elimthm = Goal.prove ctxt
bulwahn@34948
  1097
      (argnames @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac)
bulwahn@35884
  1098
    val opt_neg_introthm =
bulwahn@35884
  1099
      if is_all_input mode then
bulwahn@35884
  1100
        let
bulwahn@35884
  1101
          val neg_predpropI = HOLogic.mk_Trueprop (HOLogic.mk_not (list_comb (pred, args')))
bulwahn@35884
  1102
          val neg_funpropI =
bulwahn@45450
  1103
            HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval
bulwahn@45450
  1104
              (Predicate_Comp_Funs.mk_not (list_comb (funtrm, inargs)), HOLogic.unit))
bulwahn@35884
  1105
          val neg_introtrm = Logic.list_implies (neg_predpropI :: param_eqs, neg_funpropI)
bulwahn@35884
  1106
          val tac =
wenzelm@51717
  1107
            Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
bulwahn@35884
  1108
              (@{thm if_False} :: @{thm Predicate.not_pred_eq} :: simprules)) 1
wenzelm@60752
  1109
            THEN resolve_tac ctxt @{thms Predicate.singleI} 1
bulwahn@37003
  1110
        in SOME (Goal.prove ctxt (argnames @ hoarg_names') []
bulwahn@35884
  1111
            neg_introtrm (fn _ => tac))
bulwahn@35884
  1112
        end
bulwahn@35884
  1113
      else NONE
bulwahn@34948
  1114
  in
bulwahn@35884
  1115
    ((introthm, elimthm), opt_neg_introthm)
bulwahn@34948
  1116
  end
bulwahn@32667
  1117
wenzelm@55437
  1118
fun create_constname_of_mode options thy prefix name _ mode =
bulwahn@32667
  1119
  let
wenzelm@55437
  1120
    val system_proposal = prefix ^ (Long_Name.base_name name) ^ "_" ^ ascii_string_of_mode mode
bulwahn@34948
  1121
    val name = the_default system_proposal (proposed_names options name mode)
bulwahn@32667
  1122
  in
bulwahn@33620
  1123
    Sign.full_bname thy name
wenzelm@55437
  1124
  end
bulwahn@32667
  1125
bulwahn@33620
  1126
fun create_definitions options preds (name, modes) thy =
bulwahn@32667
  1127
  let
bulwahn@45450
  1128
    val compfuns = Predicate_Comp_Funs.compfuns
bulwahn@32667
  1129
    val T = AList.lookup (op =) preds name |> the
bulwahn@34948
  1130
    fun create_definition mode thy =
bulwahn@33752
  1131
      let
bulwahn@33752
  1132
        val mode_cname = create_constname_of_mode options thy "" name T mode
bulwahn@33752
  1133
        val mode_cbasename = Long_Name.base_name mode_cname
bulwahn@34948
  1134
        val funT = funT_of compfuns mode T
wenzelm@61114
  1135
        val (args, _) = fold_map (mk_args true) (strip_fun_mode mode ~~ binder_types T) []
haftmann@50056
  1136
        fun strip_eval _ t =
bulwahn@33752
  1137
          let
bulwahn@34948
  1138
            val t' = strip_split_abs t
bulwahn@45450
  1139
            val (r, _) = Predicate_Comp_Funs.dest_Eval t'
bulwahn@34948
  1140
          in (SOME (fst (strip_comb r)), NONE) end
bulwahn@34948
  1141
        val (inargs, outargs) = split_map_mode strip_eval mode args
krauss@39756
  1142
        val predterm = fold_rev HOLogic.tupled_lambda inargs
bulwahn@45450
  1143
          (Predicate_Comp_Funs.mk_Enum (HOLogic.tupled_lambda (HOLogic.mk_tuple outargs)
bulwahn@34948
  1144
            (list_comb (Const (name, T), args))))
bulwahn@34948
  1145
        val lhs = Const (mode_cname, funT)
bulwahn@33752
  1146
        val def = Logic.mk_equals (lhs, predterm)
bulwahn@33752
  1147
        val ([definition], thy') = thy |>
wenzelm@56239
  1148
          Sign.add_consts [(Binding.name mode_cbasename, funT, NoSyn)] |>
wenzelm@46909
  1149
          Global_Theory.add_defs false [((Binding.name (Thm.def_name mode_cbasename), def), [])]
wenzelm@42361
  1150
        val ctxt' = Proof_Context.init_global thy'
bulwahn@35884
  1151
        val rules as ((intro, elim), _) =
bulwahn@37003
  1152
          create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
wenzelm@52788
  1153
        in
wenzelm@52788
  1154
          thy'
wenzelm@61114
  1155
          |> Core_Data.set_function_name Pred name mode mode_cname
wenzelm@61114
  1156
          |> Core_Data.add_predfun_data name mode (definition, rules)
wenzelm@39557
  1157
          |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
wenzelm@39557
  1158
          |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
bulwahn@32667
  1159
        end;
bulwahn@32667
  1160
  in
wenzelm@61114
  1161
    thy |> Core_Data.defined_function_of Pred name |> fold create_definition modes
bulwahn@32667
  1162
  end;
bulwahn@32667
  1163
haftmann@50056
  1164
fun define_functions comp_modifiers _ options preds (name, modes) thy =
bulwahn@32667
  1165
  let
bulwahn@32667
  1166
    val T = AList.lookup (op =) preds name |> the
bulwahn@32667
  1167
    fun create_definition mode thy =
bulwahn@32667
  1168
      let
bulwahn@33485
  1169
        val function_name_prefix = Comp_Mod.function_name_prefix comp_modifiers
bulwahn@33620
  1170
        val mode_cname = create_constname_of_mode options thy function_name_prefix name T mode
bulwahn@34948
  1171
        val funT = Comp_Mod.funT_of comp_modifiers mode T
bulwahn@32667
  1172
      in
wenzelm@56239
  1173
        thy |> Sign.add_consts [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
wenzelm@61114
  1174
        |> Core_Data.set_function_name (Comp_Mod.compilation comp_modifiers) name mode mode_cname
bulwahn@32667
  1175
      end;
bulwahn@32667
  1176
  in
bulwahn@34948
  1177
    thy
wenzelm@61114
  1178
    |> Core_Data.defined_function_of (Comp_Mod.compilation comp_modifiers) name
bulwahn@34948
  1179
    |> fold create_definition modes
bulwahn@32667
  1180
  end;
bulwahn@32672
  1181
bulwahn@32667
  1182
bulwahn@32667
  1183
(* composition of mode inference, definition, compilation and proof *)
bulwahn@32667
  1184
bulwahn@32667
  1185
(** auxillary combinators for table of preds and modes **)
bulwahn@32667
  1186
bulwahn@32667
  1187
fun map_preds_modes f preds_modes_table =
bulwahn@32667
  1188
  map (fn (pred, modes) =>
bulwahn@32667
  1189
    (pred, map (fn (mode, value) => (mode, f pred mode value)) modes)) preds_modes_table
bulwahn@32667
  1190
bulwahn@32667
  1191
fun join_preds_modes table1 table2 =
bulwahn@32667
  1192
  map_preds_modes (fn pred => fn mode => fn value =>
bulwahn@32667
  1193
    (value, the (AList.lookup (op =) (the (AList.lookup (op =) table2 pred)) mode))) table1
bulwahn@36254
  1194
bulwahn@32667
  1195
fun maps_modes preds_modes_table =
bulwahn@32667
  1196
  map (fn (pred, modes) =>
haftmann@50056
  1197
    (pred, map (fn (_, value) => value) modes)) preds_modes_table
bulwahn@36254
  1198
bulwahn@37005
  1199
fun compile_preds options comp_modifiers ctxt all_vs param_vs preds moded_clauses =
bulwahn@37005
  1200
  map_preds_modes (fn pred => compile_pred options comp_modifiers ctxt all_vs param_vs pred
bulwahn@33143
  1201
      (the (AList.lookup (op =) preds pred))) moded_clauses
bulwahn@33143
  1202
bulwahn@35324
  1203
fun prove options thy clauses preds moded_clauses compiled_terms =
bulwahn@35324
  1204
  map_preds_modes (prove_pred options thy clauses preds)
bulwahn@32667
  1205
    (join_preds_modes moded_clauses compiled_terms)
bulwahn@32667
  1206
haftmann@50056
  1207
fun prove_by_skip _ thy _ _ _ compiled_terms =
wenzelm@35021
  1208
  map_preds_modes
haftmann@50056
  1209
    (fn _ => fn _ => fn t => Drule.export_without_context (Skip_Proof.make_thm thy t))
bulwahn@32667
  1210
    compiled_terms
bulwahn@33106
  1211
bulwahn@33376
  1212
(* preparation of introduction rules into special datastructures *)
bulwahn@37003
  1213
fun dest_prem ctxt params t =
bulwahn@33106
  1214
  (case strip_comb t of
haftmann@50056
  1215
    (v as Free _, _) => if member (op =) params v then Prem t else Sidecond t
wenzelm@55437
  1216
  | (c as Const (@{const_name Not}, _), [t]) =>
wenzelm@55437
  1217
      (case dest_prem ctxt params t of
wenzelm@55437
  1218
        Prem t => Negprem t
wenzelm@55437
  1219
      | Negprem _ => error ("Double negation not allowed in premise: " ^
wenzelm@55437
  1220
          Syntax.string_of_term ctxt (c $ t))
wenzelm@55437
  1221
      | Sidecond t => Sidecond (c $ t))
haftmann@50056
  1222
  | (Const (s, _), _) =>
wenzelm@61114
  1223
      if Core_Data.is_registered ctxt s then Prem t else Sidecond t
bulwahn@33106
  1224
  | _ => Sidecond t)
bulwahn@34948
  1225
bulwahn@39310
  1226
fun prepare_intrs options ctxt prednames intros =
bulwahn@32667
  1227
  let
wenzelm@42361
  1228
    val thy = Proof_Context.theory_of ctxt
wenzelm@59582
  1229
    val intrs = map Thm.prop_of intros
bulwahn@33146
  1230
    val preds = map (fn c => Const (c, Sign.the_const_type thy c)) prednames
bulwahn@33146
  1231
    val (preds, intrs) = unify_consts thy preds intrs
bulwahn@37003
  1232
    val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs] ctxt
bulwahn@33126
  1233
    val preds = map dest_Const preds
bulwahn@34948
  1234
    val all_vs = terms_vs intrs
bulwahn@39201
  1235
    fun generate_modes s T =
bulwahn@39201
  1236
      if member (op =) (no_higher_order_predicate options) s then
bulwahn@39201
  1237
        all_smodes_of_typ T
bulwahn@39201
  1238
      else
bulwahn@39201
  1239
        all_modes_of_typ T
wenzelm@55437
  1240
    val all_modes =
bulwahn@35324
  1241
      map (fn (s, T) =>
wenzelm@55437
  1242
        (s,
wenzelm@55437
  1243
          (case proposed_modes options s of
bulwahn@39651
  1244
            SOME ms => check_matches_type ctxt s T ms
wenzelm@55437
  1245
          | NONE => generate_modes s T))) preds
bulwahn@34948
  1246
    val params =
wenzelm@55437
  1247
      (case intrs of
bulwahn@33146
  1248
        [] =>
bulwahn@33146
  1249
          let
bulwahn@34948
  1250
            val T = snd (hd preds)
bulwahn@39764
  1251
            val one_mode = hd (the (AList.lookup (op =) all_modes (fst (hd preds))))
bulwahn@34948
  1252
            val paramTs =
bulwahn@39764
  1253
              ho_argsT_of one_mode (binder_types T)
bulwahn@33482
  1254
            val param_names = Name.variant_list [] (map (fn i => "p" ^ string_of_int i)
bulwahn@33482
  1255
              (1 upto length paramTs))
bulwahn@34948
  1256
          in
bulwahn@34948
  1257
            map2 (curry Free) param_names paramTs
bulwahn@34948
  1258
          end
bulwahn@35324
  1259
      | (intr :: _) =>
wenzelm@55437
  1260
          let
wenzelm@55437
  1261
            val (p, args) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
wenzelm@55437
  1262
            val one_mode = hd (the (AList.lookup (op =) all_modes (fst (dest_Const p))))
wenzelm@55437
  1263
          in
wenzelm@55437
  1264
            ho_args_of one_mode args
wenzelm@55437
  1265
          end)
bulwahn@34948
  1266
    val param_vs = map (fst o dest_Free) params
bulwahn@34948
  1267
    fun add_clause intr clauses =
bulwahn@32667
  1268
      let
wenzelm@55437
  1269
        val (Const (name, _), ts) =
wenzelm@55437
  1270
          strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
wenzelm@55437
  1271
        val prems =
wenzelm@55437
  1272
          map (dest_prem ctxt params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr)
bulwahn@32667
  1273
      in
wenzelm@55437
  1274
        AList.update op =
wenzelm@55437
  1275
          (name, these (AList.lookup op = clauses name) @ [(ts, prems)])
wenzelm@55437
  1276
          clauses
bulwahn@34948
  1277
      end;
bulwahn@34948
  1278
    val clauses = fold add_clause intrs []
bulwahn@34948
  1279
  in
bulwahn@35324
  1280
    (preds, all_vs, param_vs, all_modes, clauses)
wenzelm@55437
  1281
  end
bulwahn@32667
  1282
bulwahn@33376
  1283
(* sanity check of introduction rules *)
bulwahn@34948
  1284
(* TODO: rethink check with new modes *)
bulwahn@34948
  1285
(*
bulwahn@33106
  1286
fun check_format_of_intro_rule thy intro =
bulwahn@33106
  1287
  let
bulwahn@33106
  1288
    val concl = Logic.strip_imp_concl (prop_of intro)
bulwahn@33106
  1289
    val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
bulwahn@33629
  1290
    val params = fst (chop (nparams_of thy (fst (dest_Const p))) args)
bulwahn@33106
  1291
    fun check_arg arg = case HOLogic.strip_tupleT (fastype_of arg) of
bulwahn@33106
  1292
      (Ts as _ :: _ :: _) =>
bulwahn@33629
  1293
        if length (HOLogic.strip_tuple arg) = length Ts then
bulwahn@33629
  1294
          true
bulwahn@33114
  1295
        else
bulwahn@33629
  1296
          error ("Format of introduction rule is invalid: tuples must be expanded:"
bulwahn@33629
  1297
          ^ (Syntax.string_of_term_global thy arg) ^ " in " ^
wenzelm@61268
  1298
          (Thm.string_of_thm_global thy intro))
bulwahn@33106
  1299
      | _ => true
bulwahn@33106
  1300
    val prems = Logic.strip_imp_prems (prop_of intro)
bulwahn@34948
  1301
    fun check_prem (Prem t) = forall check_arg args
bulwahn@34948
  1302
      | check_prem (Negprem t) = forall check_arg args
bulwahn@33106
  1303
      | check_prem _ = true
bulwahn@33106
  1304
  in
bulwahn@33106
  1305
    forall check_arg args andalso
bulwahn@33106
  1306
    forall (check_prem o dest_prem thy params o HOLogic.dest_Trueprop) prems
bulwahn@33106
  1307
  end
bulwahn@34948
  1308
*)
bulwahn@33124
  1309
(*
bulwahn@33124
  1310
fun check_intros_elim_match thy prednames =
bulwahn@33124
  1311
  let
bulwahn@33124
  1312
    fun check predname =
bulwahn@33124
  1313
      let
bulwahn@33124
  1314
        val intros = intros_of thy predname
bulwahn@33124
  1315
        val elim = the_elim_of thy predname
bulwahn@33124
  1316
        val nparams = nparams_of thy predname
bulwahn@33124
  1317
        val elim' =
wenzelm@35021
  1318
          (Drule.export_without_context o Skip_Proof.make_thm thy)
wenzelm@42361
  1319
          (mk_casesrule (Proof_Context.init_global thy) nparams intros)
bulwahn@33124
  1320
      in
bulwahn@33124
  1321
        if not (Thm.equiv_thm (elim, elim')) then
bulwahn@33124
  1322
          error "Introduction and elimination rules do not match!"
bulwahn@33124
  1323
        else true
bulwahn@33124
  1324
      end
bulwahn@33124
  1325
  in forall check prednames end
bulwahn@33124
  1326
*)
bulwahn@33113
  1327
wenzelm@55437
  1328
bulwahn@33376
  1329
(* create code equation *)
bulwahn@33376
  1330
bulwahn@37007
  1331
fun add_code_equations ctxt preds result_thmss =
bulwahn@33376
  1332
  let
bulwahn@33629
  1333
    fun add_code_equation (predname, T) (pred, result_thms) =
bulwahn@33376
  1334
      let
bulwahn@34948
  1335
        val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool
bulwahn@33376
  1336
      in
wenzelm@61114
  1337
        if member eq_mode (Core_Data.modes_of Pred ctxt predname) full_mode then
bulwahn@33376
  1338
          let
bulwahn@33376
  1339
            val Ts = binder_types T
bulwahn@33376
  1340
            val arg_names = Name.variant_list []
bulwahn@33376
  1341
              (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
bulwahn@33629
  1342
            val args = map2 (curry Free) arg_names Ts
wenzelm@61114
  1343
            val predfun = Const (Core_Data.function_name_of Pred ctxt predname full_mode,
bulwahn@45461
  1344
              Ts ---> Predicate_Comp_Funs.mk_monadT @{typ unit})
bulwahn@33754
  1345
            val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
bulwahn@33376
  1346
            val eq_term = HOLogic.mk_Trueprop
bulwahn@33376
  1347
              (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
wenzelm@61114
  1348
            val def = Core_Data.predfun_definition_of ctxt predname full_mode
wenzelm@33441
  1349
            val tac = fn _ => Simplifier.simp_tac
wenzelm@51717
  1350
              (put_simpset HOL_basic_ss ctxt addsimps [def, @{thm holds_eq}, @{thm eval_pred}]) 1
bulwahn@35888
  1351
            val eq = Goal.prove ctxt arg_names [] eq_term tac
bulwahn@33376
  1352
          in
bulwahn@33376
  1353
            (pred, result_thms @ [eq])
bulwahn@33376
  1354
          end
bulwahn@33376
  1355
        else
bulwahn@33376
  1356
          (pred, result_thms)
bulwahn@33376
  1357
      end
bulwahn@33376
  1358
  in
bulwahn@33629
  1359
    map2 add_code_equation preds result_thmss
bulwahn@33376
  1360
  end
bulwahn@33376
  1361
wenzelm@55437
  1362
bulwahn@32667
  1363
(** main function of predicate compiler **)
bulwahn@32667
  1364
bulwahn@33330
  1365
datatype steps = Steps of
bulwahn@33330
  1366
  {
bulwahn@35324
  1367
  define_functions : options -> (string * typ) list -> string * (bool * mode) list -> theory -> theory,
bulwahn@35324
  1368
  prove : options -> theory -> (string * (term list * indprem list) list) list -> (string * typ) list
bulwahn@33330
  1369
    -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table,
bulwahn@37007
  1370
  add_code_equations : Proof.context -> (string * typ) list
bulwahn@33376
  1371
    -> (string * thm list) list -> (string * thm list) list,
bulwahn@34948
  1372
  comp_modifiers : Comp_Mod.comp_modifiers,
bulwahn@39761
  1373
  use_generators : bool,
bulwahn@33330
  1374
  qname : bstring
bulwahn@33330
  1375
  }
bulwahn@33330
  1376
bulwahn@35324
  1377
fun add_equations_of steps mode_analysis_options options prednames thy =
bulwahn@32667
  1378
  let
bulwahn@33330
  1379
    fun dest_steps (Steps s) = s
bulwahn@35879
  1380
    val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps))
wenzelm@42361
  1381
    val ctxt = Proof_Context.init_global thy
wenzelm@55437
  1382
    val _ =
wenzelm@55437
  1383
      print_step options
wenzelm@55437
  1384
        ("Starting predicate compiler (compilation: " ^ string_of_compilation compilation ^
wenzelm@55437
  1385
          ") for predicates " ^ commas prednames ^ "...")
wenzelm@55437
  1386
    (*val _ = check_intros_elim_match thy prednames*)
wenzelm@55437
  1387
    (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
bulwahn@35324
  1388
    val _ =
bulwahn@35324
  1389
      if show_intermediate_results options then
wenzelm@61268
  1390
        tracing (commas (map (Thm.string_of_thm ctxt) (maps (Core_Data.intros_of ctxt) prednames)))
bulwahn@35324
  1391
      else ()
bulwahn@35324
  1392
    val (preds, all_vs, param_vs, all_modes, clauses) =
wenzelm@61114
  1393
      prepare_intrs options ctxt prednames (maps (Core_Data.intros_of ctxt) prednames)
bulwahn@33123
  1394
    val _ = print_step options "Infering modes..."
wenzelm@61114
  1395
    val (lookup_mode, lookup_neg_mode, needs_random) = (Core_Data.modes_of compilation ctxt,
wenzelm@61114
  1396
      Core_Data.modes_of (negative_compilation_of compilation) ctxt, Core_Data.needs_random ctxt)
bulwahn@39273
  1397
    val ((moded_clauses, needs_random), errors) =
bulwahn@42088
  1398
      cond_timeit (Config.get ctxt Quickcheck.timing) "Infering modes"
bulwahn@36251
  1399
      (fn _ => infer_modes mode_analysis_options
bulwahn@39273
  1400
        options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses)
wenzelm@61114
  1401
    val thy' = fold (fn (s, ms) => Core_Data.set_needs_random s ms) needs_random thy
bulwahn@33132
  1402
    val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
bulwahn@40138
  1403
    val _ = check_expected_modes options preds modes
bulwahn@40138
  1404
    val _ = check_proposed_modes options preds modes errors
bulwahn@37004
  1405
    val _ = print_modes options modes
bulwahn@33123
  1406
    val _ = print_step options "Defining executable functions..."
bulwahn@36252
  1407
    val thy'' =
bulwahn@42088
  1408
      cond_timeit (Config.get ctxt Quickcheck.timing) "Defining executable functions..."
wenzelm@52788
  1409
      (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy')
wenzelm@42361
  1410
    val ctxt'' = Proof_Context.init_global thy''
bulwahn@33123
  1411
    val _ = print_step options "Compiling equations..."
bulwahn@32667
  1412
    val compiled_terms =
bulwahn@42088
  1413
      cond_timeit (Config.get ctxt Quickcheck.timing) "Compiling equations...." (fn _ =>
bulwahn@36254
  1414
        compile_preds options
bulwahn@37005
  1415
          (#comp_modifiers (dest_steps steps)) ctxt'' all_vs param_vs preds moded_clauses)
bulwahn@37005
  1416
    val _ = print_compiled_terms options ctxt'' compiled_terms
bulwahn@33123
  1417
    val _ = print_step options "Proving equations..."
bulwahn@35324
  1418
    val result_thms =
bulwahn@42088
  1419
      cond_timeit (Config.get ctxt Quickcheck.timing) "Proving equations...." (fn _ =>
bulwahn@36252
  1420
      #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms)
bulwahn@37007
  1421
    val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
bulwahn@33376
  1422
      (maps_modes result_thms)
bulwahn@33330
  1423
    val qname = #qname (dest_steps steps)
wenzelm@47248
  1424
    val attrib = Thm.declaration_attribute (fn thm => Context.mapping (Code.add_eqn thm) I)
bulwahn@36252
  1425
    val thy''' =
bulwahn@42088
  1426
      cond_timeit (Config.get ctxt Quickcheck.timing) "Setting code equations...." (fn _ =>
wenzelm@39557
  1427
      fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
bulwahn@32667
  1428
      [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
wenzelm@47248
  1429
        [attrib])] thy))
wenzelm@52788
  1430
      result_thms' thy'')
bulwahn@32667
  1431
  in
bulwahn@34948
  1432
    thy'''
bulwahn@32667
  1433
  end
wenzelm@55437
  1434
bulwahn@33132
  1435
fun gen_add_equations steps options names thy =
bulwahn@32667
  1436
  let
bulwahn@33330
  1437
    fun dest_steps (Steps s) = s
wenzelm@61114
  1438
    val defined = Core_Data.defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps)))
wenzelm@61114
  1439
    val thy' = Core_Data.extend_intro_graph names thy;
bulwahn@32667
  1440
    fun strong_conn_of gr keys =
wenzelm@46614
  1441
      Graph.strong_conn (Graph.restrict (member (op =) (Graph.all_succs gr keys)) gr)
wenzelm@61114
  1442
    val scc = strong_conn_of (Core_Data.PredData.get thy') names
wenzelm@61114
  1443
    val thy'' = fold Core_Data.preprocess_intros (flat scc) thy'
bulwahn@39657
  1444
    val thy''' = fold_rev
bulwahn@32667
  1445
      (fn preds => fn thy =>
wenzelm@42361
  1446
        if not (forall (defined (Proof_Context.init_global thy)) preds) then
bulwahn@35324
  1447
          let
bulwahn@39761
  1448
            val mode_analysis_options = {use_generators = #use_generators (dest_steps steps),
bulwahn@35324
  1449
              reorder_premises =
bulwahn@35324
  1450
                not (no_topmost_reordering options andalso not (null (inter (op =) preds names))),
bulwahn@39761
  1451
              infer_pos_and_neg_modes = #use_generators (dest_steps steps)}
bulwahn@35324
  1452
          in
bulwahn@35324
  1453
            add_equations_of steps mode_analysis_options options preds thy
bulwahn@35324
  1454
          end
bulwahn@33483
  1455
        else thy)
wenzelm@52788
  1456
      scc thy''
bulwahn@39657
  1457
  in thy''' end
bulwahn@35879
  1458
bulwahn@34948
  1459
val add_equations = gen_add_equations
bulwahn@35324
  1460
  (Steps {
bulwahn@35324
  1461
  define_functions =
bulwahn@35324
  1462
    fn options => fn preds => fn (s, modes) =>
bulwahn@35324
  1463
      create_definitions
bulwahn@35324
  1464
      options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
bulwahn@34948
  1465
  prove = prove,
bulwahn@34948
  1466
  add_code_equations = add_code_equations,
bulwahn@34948
  1467
  comp_modifiers = predicate_comp_modifiers,
bulwahn@39761
  1468
  use_generators = false,
bulwahn@34948
  1469
  qname = "equation"})
bulwahn@33143
  1470
bulwahn@33134
  1471
val add_depth_limited_equations = gen_add_equations
bulwahn@35879
  1472
  (Steps {
bulwahn@35879
  1473
  define_functions =
bulwahn@35879
  1474
    fn options => fn preds => fn (s, modes) =>
bulwahn@45450
  1475
    define_functions depth_limited_comp_modifiers Predicate_Comp_Funs.compfuns
bulwahn@35879
  1476
    options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
bulwahn@32667
  1477
  prove = prove_by_skip,
bulwahn@34948
  1478
  add_code_equations = K (K I),
bulwahn@35879
  1479
  comp_modifiers = depth_limited_comp_modifiers,
bulwahn@39761
  1480
  use_generators = false,
bulwahn@33330
  1481
  qname = "depth_limited_equation"})
bulwahn@35879
  1482
bulwahn@35880
  1483
val add_random_equations = gen_add_equations
bulwahn@35880
  1484
  (Steps {
bulwahn@35880
  1485
  define_functions =
bulwahn@35880
  1486
    fn options => fn preds => fn (s, modes) =>
bulwahn@45450
  1487
      define_functions random_comp_modifiers Predicate_Comp_Funs.compfuns options preds
bulwahn@35880
  1488
      (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
bulwahn@35880
  1489
  comp_modifiers = random_comp_modifiers,
bulwahn@32667
  1490
  prove = prove_by_skip,
bulwahn@34948
  1491
  add_code_equations = K (K I),
bulwahn@39761
  1492
  use_generators = true,
bulwahn@33375
  1493
  qname = "random_equation"})
bulwahn@35880
  1494
bulwahn@35881
  1495
val add_depth_limited_random_equations = gen_add_equations
bulwahn@35881
  1496
  (Steps {
bulwahn@35881
  1497
  define_functions =
bulwahn@35881
  1498
    fn options => fn preds => fn (s, modes) =>
bulwahn@45450
  1499
      define_functions depth_limited_random_comp_modifiers Predicate_Comp_Funs.compfuns options preds
bulwahn@35881
  1500
      (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
bulwahn@35881
  1501
  comp_modifiers = depth_limited_random_comp_modifiers,
bulwahn@35881
  1502
  prove = prove_by_skip,
bulwahn@35881
  1503
  add_code_equations = K (K I),
bulwahn@39761
  1504
  use_generators = true,
bulwahn@35881
  1505
  qname = "depth_limited_random_equation"})
bulwahn@35881
  1506
bulwahn@34948
  1507
val add_dseq_equations = gen_add_equations
bulwahn@35324
  1508
  (Steps {
bulwahn@35324
  1509
  define_functions =
bulwahn@35324
  1510
  fn options => fn preds => fn (s, modes) =>
bulwahn@35324
  1511
    define_functions dseq_comp_modifiers DSequence_CompFuns.compfuns
bulwahn@35324
  1512
    options preds (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
bulwahn@34948
  1513
  prove = prove_by_skip,
bulwahn@34948
  1514
  add_code_equations = K (K I),
bulwahn@34948
  1515
  comp_modifiers = dseq_comp_modifiers,
bulwahn@39761
  1516
  use_generators = false,
bulwahn@34948
  1517
  qname = "dseq_equation"})
bulwahn@34948
  1518
bulwahn@34948
  1519
val add_random_dseq_equations = gen_add_equations
bulwahn@35324
  1520
  (Steps {
bulwahn@35324
  1521
  define_functions =
bulwahn@35324
  1522
    fn options => fn preds => fn (s, modes) =>
bulwahn@35324
  1523
    let
bulwahn@35324
  1524
      val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
bulwahn@35324
  1525
      val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
bulwahn@35324
  1526
    in define_functions pos_random_dseq_comp_modifiers Random_Sequence_CompFuns.compfuns
bulwahn@35324
  1527
      options preds (s, pos_modes)
bulwahn@35324
  1528
      #> define_functions neg_random_dseq_comp_modifiers Random_Sequence_CompFuns.compfuns
bulwahn@35324
  1529
      options preds (s, neg_modes)
bulwahn@35324
  1530
    end,
bulwahn@34948
  1531
  prove = prove_by_skip,
bulwahn@34948
  1532
  add_code_equations = K (K I),
bulwahn@35324
  1533
  comp_modifiers = pos_random_dseq_comp_modifiers,
bulwahn@39761
  1534
  use_generators = true,
bulwahn@34948
  1535
  qname = "random_dseq_equation"})
bulwahn@34948
  1536
bulwahn@36018
  1537
val add_new_random_dseq_equations = gen_add_equations
bulwahn@36018
  1538
  (Steps {
bulwahn@36018
  1539
  define_functions =
bulwahn@36018
  1540
    fn options => fn preds => fn (s, modes) =>
wenzelm@55437
  1541
      let
wenzelm@55437
  1542
        val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
wenzelm@55437
  1543
        val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
wenzelm@55437
  1544
      in
wenzelm@55437
  1545
        define_functions new_pos_random_dseq_comp_modifiers
wenzelm@55437
  1546
          New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
wenzelm@55437
  1547
          options preds (s, pos_modes) #>
wenzelm@55437
  1548
        define_functions new_neg_random_dseq_comp_modifiers
wenzelm@55437
  1549
          New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
wenzelm@55437
  1550
          options preds (s, neg_modes)
wenzelm@55437
  1551
      end,
bulwahn@36018
  1552
  prove = prove_by_skip,
bulwahn@36018
  1553
  add_code_equations = K (K I),
bulwahn@36018
  1554
  comp_modifiers = new_pos_random_dseq_comp_modifiers,
bulwahn@39761
  1555
  use_generators = true,
bulwahn@36018
  1556
  qname = "new_random_dseq_equation"})
bulwahn@32667
  1557
bulwahn@40051
  1558
val add_generator_dseq_equations = gen_add_equations
bulwahn@40051
  1559
  (Steps {
bulwahn@40051
  1560
  define_functions =
wenzelm@55437
  1561
    fn options => fn preds => fn (s, modes) =>
wenzelm@55437
  1562
      let
wenzelm@55437
  1563
        val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
wenzelm@55437
  1564
        val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
wenzelm@55437
  1565
      in
wenzelm@55437
  1566
        define_functions pos_generator_dseq_comp_modifiers
wenzelm@55437
  1567
          New_Pos_DSequence_CompFuns.depth_limited_compfuns options preds (s, pos_modes) #>
wenzelm@55437
  1568
        define_functions neg_generator_dseq_comp_modifiers
wenzelm@55437
  1569
          New_Neg_DSequence_CompFuns.depth_limited_compfuns options preds (s, neg_modes)
wenzelm@55437
  1570
      end,
bulwahn@40051
  1571
  prove = prove_by_skip,
bulwahn@40051
  1572
  add_code_equations = K (K I),
bulwahn@40051
  1573
  comp_modifiers = pos_generator_dseq_comp_modifiers,
bulwahn@40051
  1574
  use_generators = true,
bulwahn@40051
  1575
  qname = "generator_dseq_equation"})
bulwahn@40051
  1576
bulwahn@45450
  1577
val add_generator_cps_equations = gen_add_equations
bulwahn@45450
  1578
  (Steps {
bulwahn@45450
  1579
  define_functions =
wenzelm@55437
  1580
    fn options => fn preds => fn (s, modes) =>
wenzelm@55437
  1581
      let
wenzelm@55437
  1582
        val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
wenzelm@55437
  1583
        val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
wenzelm@55437
  1584
      in
wenzelm@55437
  1585
        define_functions pos_generator_cps_comp_modifiers Pos_Bounded_CPS_Comp_Funs.compfuns
wenzelm@55437
  1586
          options preds (s, pos_modes)
wenzelm@55437
  1587
        #> define_functions neg_generator_cps_comp_modifiers Neg_Bounded_CPS_Comp_Funs.compfuns
wenzelm@55437
  1588
          options preds (s, neg_modes)
wenzelm@55437
  1589
      end,
bulwahn@45450
  1590
  prove = prove_by_skip,
bulwahn@45450
  1591
  add_code_equations = K (K I),
bulwahn@45450
  1592
  comp_modifiers = pos_generator_cps_comp_modifiers,
bulwahn@45450
  1593
  use_generators = true,
bulwahn@45450
  1594
  qname = "generator_cps_equation"})
wenzelm@55437
  1595
wenzelm@55437
  1596
bulwahn@32667
  1597
(** user interface **)
bulwahn@32667
  1598
bulwahn@32667
  1599
(* code_pred_intro attribute *)
bulwahn@32667
  1600
bulwahn@39545
  1601
fun attrib' f opt_case_name =
bulwahn@39545
  1602
  Thm.declaration_attribute (fn thm => Context.mapping (f (opt_case_name, thm)) I);
bulwahn@32667
  1603
wenzelm@61114
  1604
val code_pred_intro_attrib = attrib' Core_Data.add_intro NONE;
bulwahn@32667
  1605
bulwahn@32668
  1606
(*FIXME
bulwahn@32668
  1607
- Naming of auxiliary rules necessary?
bulwahn@32668
  1608
*)
bulwahn@32668
  1609
bulwahn@42141
  1610
(* values_timeout configuration *)
bulwahn@42141
  1611
bulwahn@45452
  1612
val default_values_timeout = if ML_System.is_smlnj then 1200.0 else 40.0
krauss@43896
  1613
wenzelm@55437
  1614
val values_timeout =
wenzelm@55437
  1615
  Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout)
bulwahn@42141
  1616
wenzelm@58823
  1617
val _ =
wenzelm@58823
  1618
  Theory.setup
wenzelm@61114
  1619
   (Core_Data.PredData.put (Graph.empty) #>
wenzelm@61114
  1620
    Attrib.setup @{binding code_pred_intro}
wenzelm@61114
  1621
      (Scan.lift (Scan.option Args.name) >> attrib' Core_Data.add_intro)
wenzelm@58823
  1622
      "adding alternative introduction rules for code generation of inductive predicates")
bulwahn@32667
  1623
wenzelm@33522
  1624
(* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
wenzelm@38757
  1625
(* FIXME ... this is important to avoid changing the background theory below *)
bulwahn@33132
  1626
fun generic_code_pred prep_const options raw_const lthy =
bulwahn@32667
  1627
  let
wenzelm@42361
  1628
    val thy = Proof_Context.theory_of lthy
bulwahn@32667
  1629
    val const = prep_const thy raw_const
wenzelm@61114
  1630
    val lthy' = Local_Theory.background_theory (Core_Data.extend_intro_graph [const]) lthy
wenzelm@42361
  1631
    val thy' = Proof_Context.theory_of lthy'
wenzelm@42361
  1632
    val ctxt' = Proof_Context.init_global thy'
wenzelm@61114
  1633
    val preds =
wenzelm@61114
  1634
      Graph.all_succs (Core_Data.PredData.get thy') [const] |> filter_out (Core_Data.has_elim ctxt')
bulwahn@32667
  1635
    fun mk_cases const =
bulwahn@32667
  1636
      let
bulwahn@39299
  1637
        val T = Sign.the_const_type thy' const
bulwahn@33146
  1638
        val pred = Const (const, T)
wenzelm@61114
  1639
        val intros = Core_Data.intros_of ctxt' const
wenzelm@55437
  1640
      in mk_casesrule lthy' pred intros end
bulwahn@32667
  1641
    val cases_rules = map mk_cases preds
bulwahn@32667
  1642
    val cases =
wenzelm@60565
  1643
      map2 (fn pred_name => fn case_rule =>
wenzelm@60565
  1644
        Rule_Cases.Case {
wenzelm@60565
  1645
          fixes = [],
wenzelm@60565
  1646
          assumes =
wenzelm@60565
  1647
            ("that", tl (Logic.strip_imp_prems case_rule)) ::
wenzelm@60565
  1648
            map_filter (fn (fact_name, fact) => Option.map (fn a => (a, [fact])) fact_name)
wenzelm@61114
  1649
              ((SOME "prems" :: Core_Data.names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule),
wenzelm@60565
  1650
          binds = [], cases = []}) preds cases_rules
bulwahn@32667
  1651
    val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
bulwahn@32667
  1652
    val lthy'' = lthy'
bulwahn@39545
  1653
      |> fold Variable.auto_fixes cases_rules
wenzelm@60573
  1654
      |> Proof_Context.update_cases case_env
bulwahn@32667
  1655
    fun after_qed thms goal_ctxt =
bulwahn@32667
  1656
      let
wenzelm@42361
  1657
        val global_thms = Proof_Context.export goal_ctxt
wenzelm@42361
  1658
          (Proof_Context.init_global (Proof_Context.theory_of goal_ctxt)) (map the_single thms)
bulwahn@32667
  1659
      in
wenzelm@61114
  1660
        goal_ctxt |> Local_Theory.background_theory (fold Core_Data.set_elim global_thms #>
bulwahn@34948
  1661
          ((case compilation options of
bulwahn@34948
  1662
             Pred => add_equations
bulwahn@34948
  1663
           | DSeq => add_dseq_equations
bulwahn@35879
  1664
           | Pos_Random_DSeq => add_random_dseq_equations
bulwahn@35879
  1665
           | Depth_Limited => add_depth_limited_equations
bulwahn@35880
  1666
           | Random => add_random_equations
bulwahn@35881
  1667
           | Depth_Limited_Random => add_depth_limited_random_equations
bulwahn@36018
  1668
           | New_Pos_Random_DSeq => add_new_random_dseq_equations
bulwahn@40051
  1669
           | Pos_Generator_DSeq => add_generator_dseq_equations
bulwahn@45450
  1670
           | Pos_Generator_CPS => add_generator_cps_equations
haftmann@50056
  1671
           | _ => error ("Compilation not supported")
bulwahn@34948
  1672
           ) options [const]))
bulwahn@33144
  1673
      end
bulwahn@32667
  1674
  in
wenzelm@36323
  1675
    Proof.theorem NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
bulwahn@32667
  1676
  end;
bulwahn@32667
  1677
bulwahn@32667
  1678
val code_pred = generic_code_pred (K I);
bulwahn@32667
  1679
val code_pred_cmd = generic_code_pred Code.read_const
bulwahn@32667
  1680
wenzelm@55437
  1681
bulwahn@32667
  1682
(* transformation for code generation *)
bulwahn@32667
  1683
wenzelm@59154
  1684
structure Data = Proof_Data
wenzelm@41472
  1685
(
wenzelm@59154
  1686
  type T =
wenzelm@59154
  1687
    (unit -> term Predicate.pred) *
wenzelm@59154
  1688
    (unit -> seed -> term Predicate.pred * seed) *
wenzelm@59154
  1689
    (unit -> term Limited_Sequence.dseq) *
wenzelm@59154
  1690
    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
wenzelm@59154
  1691
      term Limited_Sequence.dseq * seed) *
wenzelm@59154
  1692
    (unit -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence) *
wenzelm@59154
  1693
    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
wenzelm@59154
  1694
      Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence) *
wenzelm@59154
  1695
    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
wenzelm@59154
  1696
      Code_Numeral.natural -> (term * Code_Numeral.natural) Lazy_Sequence.lazy_sequence);
wenzelm@59154
  1697
  val empty: T =
wenzelm@59154
  1698
   (fn () => raise Fail "pred_result",
wenzelm@59154
  1699
    fn () => raise Fail "pred_random_result",
wenzelm@59154
  1700
    fn () => raise Fail "dseq_result",
wenzelm@59154
  1701
    fn () => raise Fail "dseq_random_result",
wenzelm@59154
  1702
    fn () => raise Fail "new_dseq_result",
wenzelm@59154
  1703
    fn () => raise Fail "lseq_random_result",
wenzelm@59154
  1704
    fn () => raise Fail "lseq_random_stats_result");
wenzelm@59154
  1705
  fun init _ = empty;
haftmann@39388
  1706
);
bulwahn@40102
  1707
wenzelm@59154
  1708
val get_pred_result = #1 o Data.get;
wenzelm@59154
  1709
val get_pred_random_result = #2 o Data.get;
wenzelm@59154
  1710
val get_dseq_result = #3 o Data.get;
wenzelm@59154
  1711
val get_dseq_random_result = #4 o Data.get;
wenzelm@59154
  1712
val get_new_dseq_result = #5 o Data.get;
wenzelm@59154
  1713
val get_lseq_random_result = #6 o Data.get;
wenzelm@59154
  1714
val get_lseq_random_stats_result = #7 o Data.get;
haftmann@39388
  1715
wenzelm@59154
  1716
val put_pred_result = Data.map o @{apply 7(1)} o K;
wenzelm@59154
  1717
val put_pred_random_result = Data.map o @{apply 7(2)} o K;
wenzelm@59154
  1718
val put_dseq_result = Data.map o @{apply 7(3)} o K;
wenzelm@59154
  1719
val put_dseq_random_result = Data.map o @{apply 7(4)} o K;
wenzelm@59154
  1720
val put_new_dseq_result = Data.map o @{apply 7(5)} o K;
wenzelm@59154
  1721
val put_lseq_random_result = Data.map o @{apply 7(6)} o K;
wenzelm@59154
  1722
val put_lseq_random_stats_result = Data.map o @{apply 7(7)} o K;
bulwahn@32667
  1723
bulwahn@42094
  1724
fun dest_special_compr t =
bulwahn@42094
  1725
  let
wenzelm@55437
  1726
    val (inner_t, T_compr) =
wenzelm@55437
  1727
      (case t of
wenzelm@55437
  1728
        (Const (@{const_name Collect}, _) $ Abs (_, T, t)) => (t, T)
wenzelm@55437
  1729
      | _ => raise TERM ("dest_special_compr", [t]))
bulwahn@42094
  1730
    val (Ts, conj) = apfst (map snd) (Predicate_Compile_Aux.strip_ex inner_t)
bulwahn@42094
  1731
    val [eq, body] = HOLogic.dest_conj conj
wenzelm@55437
  1732
    val rhs =
wenzelm@55437
  1733
      (case HOLogic.dest_eq eq of
bulwahn@42094
  1734
        (Bound i, rhs) => if i = length Ts then rhs else raise TERM ("dest_special_compr", [t])
wenzelm@55437
  1735
      | _ => raise TERM ("dest_special_compr", [t]))
bulwahn@42094
  1736
    val output_names = Name.variant_list (fold Term.add_free_names [rhs, body] [])
bulwahn@42094
  1737
      (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
bulwahn@42094
  1738
    val output_frees = map2 (curry Free) output_names (rev Ts)
bulwahn@42094
  1739
    val body = subst_bounds (output_frees, body)
bulwahn@42094
  1740
    val output = subst_bounds (output_frees, rhs)
bulwahn@42094
  1741
  in
bulwahn@42094
  1742
    (((body, output), T_compr), output_names)
bulwahn@42094
  1743
  end
bulwahn@42094
  1744
bulwahn@42094
  1745
fun dest_general_compr ctxt t_compr =
wenzelm@55437
  1746
  let
wenzelm@55437
  1747
    val inner_t =
wenzelm@55437
  1748
      (case t_compr of
wenzelm@55437
  1749
        (Const (@{const_name Collect}, _) $ t) => t
wenzelm@55437
  1750
      | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr))
haftmann@61424
  1751
    val (body, Ts, fp) = HOLogic.strip_ptupleabs inner_t;
bulwahn@42094
  1752
    val output_names = Name.variant_list (Term.add_free_names body [])
bulwahn@42094
  1753
      (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
bulwahn@42094
  1754
    val output_frees = map2 (curry Free) output_names (rev Ts)
bulwahn@42094
  1755
    val body = subst_bounds (output_frees, body)
bulwahn@42094
  1756
    val T_compr = HOLogic.mk_ptupleT fp Ts
bulwahn@42094
  1757
    val output = HOLogic.mk_ptuple fp T_compr (rev output_frees)
bulwahn@42094
  1758
  in
bulwahn@42094
  1759
    (((body, output), T_compr), output_names)
bulwahn@42094
  1760
  end
bulwahn@42094
  1761
bulwahn@32667
  1762
(*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
bulwahn@40102
  1763
fun analyze_compr ctxt (comp_modifiers, additional_arguments) param_user_modes
haftmann@50056
  1764
  (compilation, _) t_compr =
bulwahn@32667
  1765
  let
bulwahn@40102
  1766
    val compfuns = Comp_Mod.compfuns comp_modifiers
wenzelm@61114
  1767
    val all_modes_of = Core_Data.all_modes_of compilation
bulwahn@42094
  1768
    val (((body, output), T_compr), output_names) =
wenzelm@55437
  1769
      (case try dest_special_compr t_compr of
wenzelm@55437
  1770
        SOME r => r
wenzelm@55437
  1771
      | NONE => dest_general_compr ctxt t_compr)
haftmann@50056
  1772
    val (Const (name, _), all_args) =
wenzelm@55437
  1773
      (case strip_comb body of
bulwahn@36031
  1774
        (Const (name, T), all_args) => (Const (name, T), all_args)
wenzelm@55437
  1775
      | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head))
bulwahn@34948
  1776
  in
wenzelm@61114
  1777
    if Core_Data.defined_functions compilation ctxt name then
bulwahn@32668
  1778
      let
wenzelm@55437
  1779
        fun extract_mode (Const (@{const_name Pair}, _) $ t1 $ t2) =
wenzelm@55437
  1780
              Pair (extract_mode t1, extract_mode t2)
wenzelm@55437
  1781
          | extract_mode (Free (x, _)) =
wenzelm@55437
  1782
              if member (op =) output_names x then Output else Input
bulwahn@34948
  1783
          | extract_mode _ = Input
bulwahn@34948
  1784
        val user_mode = fold_rev (curry Fun) (map extract_mode all_args) Bool
bulwahn@34948
  1785
        fun valid modes1 modes2 =
wenzelm@55437
  1786
          (case int_ord (length modes1, length modes2) of
bulwahn@34948
  1787
            GREATER => error "Not enough mode annotations"
bulwahn@34948
  1788
          | LESS => error "Too many mode annotations"
wenzelm@55437
  1789
          | EQUAL =>
wenzelm@55437
  1790
              forall (fn (_, NONE) => true | (m, SOME m2) => eq_mode (m, m2)) (modes1 ~~ modes2))
bulwahn@34948
  1791
        fun mode_instance_of (m1, m2) =
bulwahn@34948
  1792
          let
bulwahn@34948
  1793
            fun instance_of (Fun _, Input) = true
bulwahn@34948
  1794
              | instance_of (Input, Input) = true
bulwahn@34948
  1795
              | instance_of (Output, Output) = true
bulwahn@34948
  1796
              | instance_of (Pair (m1, m2), Pair (m1', m2')) =
bulwahn@34948
  1797
                  instance_of  (m1, m1') andalso instance_of (m2, m2')
bulwahn@34948
  1798
              | instance_of (Pair (m1, m2), Input) =
bulwahn@34948
  1799
                  instance_of (m1, Input) andalso instance_of (m2, Input)
bulwahn@34948
  1800
              | instance_of (Pair (m1, m2), Output) =
bulwahn@34948
  1801
                  instance_of (m1, Output) andalso instance_of (m2, Output)
bulwahn@37002
  1802
              | instance_of (Input, Pair (m1, m2)) =
bulwahn@37002
  1803
                  instance_of (Input, m1) andalso instance_of (Input, m2)
bulwahn@37002
  1804
              | instance_of (Output, Pair (m1, m2)) =
bulwahn@37002
  1805
                  instance_of (Output, m1) andalso instance_of (Output, m2)
bulwahn@34948
  1806
              | instance_of _ = false
bulwahn@34948
  1807
          in forall instance_of (strip_fun_mode m1 ~~ strip_fun_mode m2) end
bulwahn@37003
  1808
        val derivs = all_derivations_of ctxt (all_modes_of ctxt) [] body
bulwahn@34948
  1809
          |> filter (fn (d, missing_vars) =>
bulwahn@34948
  1810
            let
bulwahn@34948
  1811
              val (p_mode :: modes) = collect_context_modes d
bulwahn@34948
  1812
            in
bulwahn@34948
  1813
              null missing_vars andalso
bulwahn@34948
  1814
              mode_instance_of (p_mode, user_mode) andalso
bulwahn@34948
  1815
              the_default true (Option.map (valid modes) param_user_modes)
bulwahn@34948
  1816
            end)
bulwahn@34948
  1817
          |> map fst
wenzelm@55437
  1818
        val deriv =
wenzelm@55437
  1819
          (case derivs of
wenzelm@55437
  1820
            [] =>
wenzelm@55437
  1821
              error ("No mode possible for comprehension " ^ Syntax.string_of_term ctxt t_compr)
bulwahn@34948
  1822
          | [d] => d
wenzelm@55437
  1823
          | d :: _ :: _ =>
wenzelm@55437
  1824
              (warning ("Multiple modes possible for comprehension " ^
wenzelm@55437
  1825
                Syntax.string_of_term ctxt t_compr); d))
bulwahn@34948
  1826
        val (_, outargs) = split_mode (head_mode_of deriv) all_args
bulwahn@37003
  1827
        val t_pred = compile_expr comp_modifiers ctxt
bulwahn@39648
  1828
          (body, deriv) [] additional_arguments;
bulwahn@45461
  1829
        val T_pred = dest_monadT compfuns (fastype_of t_pred)
bulwahn@42094
  1830
        val arrange = HOLogic.tupled_lambda (HOLogic.mk_tuple outargs) output
bulwahn@34948
  1831
      in
bulwahn@34948
  1832
        if null outargs then t_pred else mk_map compfuns T_pred T_compr arrange t_pred
bulwahn@34948
  1833
      end
bulwahn@34948
  1834
    else
bulwahn@34948
  1835
      error "Evaluation with values is not possible because compilation with code_pred was not invoked"
bulwahn@34948
  1836
  end
bulwahn@32667
  1837
bulwahn@37003
  1838
fun eval ctxt stats param_user_modes (options as (compilation, arguments)) k t_compr =
bulwahn@32667
  1839
  let
bulwahn@36027
  1840
    fun count xs x =
bulwahn@36027
  1841
      let
bulwahn@36027
  1842
        fun count' i [] = i
bulwahn@36027
  1843
          | count' i (x' :: xs) = if x = x' then count' (i + 1) xs else count' i xs
bulwahn@36027
  1844
      in count' 0 xs end
haftmann@51143
  1845
    fun accumulate xs = (map (fn x => (x, count xs x)) o sort int_ord o distinct (op =)) xs;
bulwahn@40102
  1846
    val comp_modifiers =
wenzelm@55437
  1847
      (case compilation of
wenzelm@55437
  1848
        Pred => predicate_comp_modifiers
wenzelm@55437
  1849
      | Random => random_comp_modifiers
wenzelm@55437
  1850
      | Depth_Limited => depth_limited_comp_modifiers
wenzelm@55437
  1851
      | Depth_Limited_Random => depth_limited_random_comp_modifiers
wenzelm@55437
  1852
      (*| Annotated => annotated_comp_modifiers*)
wenzelm@55437
  1853
      | DSeq => dseq_comp_modifiers
wenzelm@55437
  1854
      | Pos_Random_DSeq => pos_random_dseq_comp_modifiers
wenzelm@55437
  1855
      | New_Pos_Random_DSeq => new_pos_random_dseq_comp_modifiers
wenzelm@55437
  1856
      | Pos_Generator_DSeq => pos_generator_dseq_comp_modifiers)
bulwahn@40102
  1857
    val compfuns = Comp_Mod.compfuns comp_modifiers
bulwahn@40102
  1858
    val additional_arguments =
wenzelm@55437
  1859
      (case compilation of
bulwahn@40102
  1860
        Pred => []
wenzelm@55437
  1861
      | Random =>
wenzelm@55437
  1862
          map (HOLogic.mk_number @{typ "natural"}) arguments @
wenzelm@55437
  1863
            [@{term "(1, 1) :: natural * natural"}]
bulwahn@40102
  1864
      | Annotated => []
haftmann@51143
  1865
      | Depth_Limited => [HOLogic.mk_number @{typ "natural"} (hd arguments)]
wenzelm@55437
  1866
      | Depth_Limited_Random =>
wenzelm@55437
  1867
          map (HOLogic.mk_number @{typ "natural"}) arguments @
wenzelm@55437
  1868
            [@{term "(1, 1) :: natural * natural"}]
bulwahn@40102
  1869
      | DSeq => []
bulwahn@40102
  1870
      | Pos_Random_DSeq => []
bulwahn@40102
  1871
      | New_Pos_Random_DSeq => []
wenzelm@55437
  1872
      | Pos_Generator_DSeq => [])
wenzelm@55437
  1873
    val t =
wenzelm@55437
  1874
      analyze_compr ctxt (comp_modifiers, additional_arguments) param_user_modes options t_compr
wenzelm@55437
  1875
    val T = dest_monadT compfuns (fastype_of t)
bulwahn@36027
  1876
    val t' =
bulwahn@36027
  1877
      if stats andalso compilation = New_Pos_Random_DSeq then
haftmann@51143
  1878
        mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, @{typ natural}))
wenzelm@44241
  1879
          (absdummy T (HOLogic.mk_prod (HOLogic.term_of_const T $ Bound 0,
haftmann@51143
  1880
            @{term natural_of_nat} $ (HOLogic.size_const T $ Bound 0)))) t
bulwahn@36027
  1881
      else
bulwahn@36027
  1882
        mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
bulwahn@42141
  1883
    val time_limit = seconds (Config.get ctxt values_timeout)
bulwahn@36027
  1884
    val (ts, statistics) =
bulwahn@40135
  1885
      (case compilation of
bulwahn@35880
  1886
       (* Random =>
bulwahn@34948
  1887
          fst (Predicate.yieldn k
bulwahn@34948
  1888
          (Code_Eval.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref)
bulwahn@33137
  1889
            (fn proc => fn g => fn s => g s |>> Predicate.map proc) thy t' []
bulwahn@35880
  1890
            |> Random_Engine.run))*)
bulwahn@35880
  1891
        Pos_Random_DSeq =>
bulwahn@34948
  1892
          let
haftmann@51143
  1893
            val [nrandom, size, depth] = map Code_Numeral.natural_of_integer arguments
bulwahn@34948
  1894
          in
haftmann@51126
  1895
            rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
wenzelm@59154
  1896
              (Code_Runtime.dynamic_value_strict
wenzelm@59154
  1897
                (get_dseq_random_result, put_dseq_random_result,
wenzelm@59154
  1898
                  "Predicate_Compile_Core.put_dseq_random_result")
wenzelm@59154
  1899
                  ctxt NONE
wenzelm@59154
  1900
                  (fn proc => fn g => fn nrandom => fn size => fn s =>
wenzelm@59154
  1901
                    g nrandom size s |>> Limited_Sequence.map proc)
haftmann@39471
  1902
                  t' [] nrandom size
bulwahn@34948
  1903
                |> Random_Engine.run)
bulwahn@40135
  1904
              depth true)) ())
bulwahn@34948
  1905
          end
bulwahn@34948
  1906
      | DSeq =>
haftmann@51126
  1907
          rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
wenzelm@59154
  1908
            (Code_Runtime.dynamic_value_strict
wenzelm@59154
  1909
              (get_dseq_result, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
wenzelm@59154
  1910
              ctxt NONE Limited_Sequence.map t' [])
wenzelm@59154
  1911
            (Code_Numeral.natural_of_integer (the_single arguments)) true)) ())
bulwahn@40102
  1912
      | Pos_Generator_DSeq =>
bulwahn@40102
  1913
          let
haftmann@51143
  1914
            val depth = Code_Numeral.natural_of_integer (the_single arguments)
bulwahn@40102
  1915
          in
bulwahn@42141
  1916
            rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
wenzelm@59154
  1917
              (Code_Runtime.dynamic_value_strict
wenzelm@59154
  1918
                (get_new_dseq_result, put_new_dseq_result,
wenzelm@59154
  1919
                  "Predicate_Compile_Core.put_new_dseq_result")
wenzelm@59154
  1920
                ctxt NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.map proc)
wenzelm@59154
  1921
                t' [] depth))) ())
bulwahn@40102
  1922
          end
bulwahn@36020
  1923
      | New_Pos_Random_DSeq =>
bulwahn@36020
  1924
          let
haftmann@51143
  1925
            val [nrandom, size, depth] = map Code_Numeral.natural_of_integer arguments
bulwahn@36020
  1926
            val seed = Random_Engine.next_seed ()
bulwahn@36020
  1927
          in
bulwahn@36027
  1928
            if stats then
haftmann@51143
  1929
              apsnd (SOME o accumulate o map Code_Numeral.integer_of_natural)
haftmann@51143
  1930
              (split_list (TimeLimit.timeLimit time_limit
bulwahn@40135
  1931
              (fn () => fst (Lazy_Sequence.yieldn k
haftmann@39471
  1932
                (Code_Runtime.dynamic_value_strict
wenzelm@59154
  1933
                  (get_lseq_random_stats_result, put_lseq_random_stats_result,
wenzelm@59154
  1934
                    "Predicate_Compile_Core.put_lseq_random_stats_result")
haftmann@55757
  1935
                  ctxt NONE
wenzelm@59154
  1936
                  (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
wenzelm@59154
  1937
                    g nrandom size s depth
haftmann@51126
  1938
                    |> Lazy_Sequence.map (apfst proc))
bulwahn@40135
  1939
                    t' [] nrandom size seed depth))) ()))
bulwahn@36027
  1940
            else rpair NONE
bulwahn@42141
  1941
              (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
haftmann@39471
  1942
                (Code_Runtime.dynamic_value_strict
wenzelm@59154
  1943
                  (get_lseq_random_result, put_lseq_random_result,
wenzelm@59154
  1944
                    "Predicate_Compile_Core.put_lseq_random_result")
wenzelm@59154
  1945
                    ctxt NONE
wenzelm@59154
  1946
                    (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
wenzelm@59154
  1947
                      g nrandom size s depth
wenzelm@59154
  1948
                      |> Lazy_Sequence.map proc)
wenzelm@59154
  1949
                      t' [] nrandom size seed depth))) ())
bulwahn@36020
  1950
          end
bulwahn@34948
  1951
      | _ =>
bulwahn@42141
  1952
          rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Predicate.yieldn k
wenzelm@59154
  1953
            (Code_Runtime.dynamic_value_strict
wenzelm@59154
  1954
              (get_pred_result, put_pred_result, "Predicate_Compile_Core.put_pred_result")
haftmann@55757
  1955
              ctxt NONE Predicate.map t' []))) ()))
bulwahn@40135
  1956
     handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
bulwahn@36027
  1957
  in ((T, ts), statistics) end;
bulwahn@36027
  1958
bulwahn@43123
  1959
fun values param_user_modes ((raw_expected, stats), comp_options) k t_compr ctxt =
bulwahn@32667
  1960
  let
bulwahn@37003
  1961
    val ((T, ts), statistics) = eval ctxt stats param_user_modes comp_options k t_compr
bulwahn@34948
  1962
    val setT = HOLogic.mk_setT T
bulwahn@34948
  1963
    val elems = HOLogic.mk_set T ts
bulwahn@43123
  1964
    val ([dots], ctxt') =
wenzelm@55437
  1965
      Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix ("...", [], 1000))] ctxt
bulwahn@34948
  1966
    (* check expected values *)
bulwahn@43123
  1967
    val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT)
bulwahn@34948
  1968
    val () =
wenzelm@55437
  1969
      (case raw_expected of
bulwahn@34948
  1970
        NONE => ()
bulwahn@34948
  1971
      | SOME s =>
bulwahn@34948
  1972
        if eq_set (op =) (HOLogic.dest_set (Syntax.read_term ctxt s), ts) then ()
bulwahn@34948
  1973
        else
bulwahn@34948
  1974
          error ("expected and computed values do not match:\n" ^
bulwahn@34948
  1975
            "expected values: " ^ Syntax.string_of_term ctxt (Syntax.read_term ctxt s) ^ "\n" ^
wenzelm@55437
  1976
            "computed values: " ^ Syntax.string_of_term ctxt elems ^ "\n"))
bulwahn@34948
  1977
  in
wenzelm@55437
  1978
    ((if k = ~1 orelse length ts < k then elems else union $ elems $ Free (dots, setT), statistics),
wenzelm@55437
  1979
      ctxt')
bulwahn@32667
  1980
  end;
bulwahn@33623
  1981
bulwahn@33479
  1982
fun values_cmd print_modes param_user_modes options k raw_t state =
bulwahn@32667
  1983
  let
bulwahn@34948
  1984
    val ctxt = Toplevel.context_of state
bulwahn@34948
  1985
    val t = Syntax.read_term ctxt raw_t
bulwahn@43123
  1986
    val ((t', stats), ctxt') = values param_user_modes options k t ctxt
bulwahn@34948
  1987
    val ty' = Term.type_of t'
bulwahn@43123
  1988
    val ctxt'' = Variable.auto_fixes t' ctxt'
bulwahn@36027
  1989
    val pretty_stat =
wenzelm@55437
  1990
      (case stats of
wenzelm@55437
  1991
        NONE => []
wenzelm@55437
  1992
      | SOME xs =>
bulwahn@36027
  1993
          let
bulwahn@36027
  1994
            val total = fold (curry (op +)) (map snd xs) 0
bulwahn@36027
  1995
            fun pretty_entry (s, n) =
bulwahn@36027
  1996
              [Pretty.str "size", Pretty.brk 1,
bulwahn@36027
  1997
               Pretty.str (string_of_int s), Pretty.str ":", Pretty.brk 1,
bulwahn@36027
  1998
               Pretty.str (string_of_int n), Pretty.fbrk]
bulwahn@36027
  1999
          in
bulwahn@36027
  2000
            [Pretty.fbrk, Pretty.str "Statistics:", Pretty.fbrk,
wenzelm@55437
  2001
             Pretty.str "total:", Pretty.brk 1, Pretty.str (string_of_int total), Pretty.fbrk] @
wenzelm@55437
  2002
              maps pretty_entry xs
wenzelm@55437
  2003
          end)
wenzelm@55437
  2004
  in
wenzelm@55437
  2005
    Print_Mode.with_modes print_modes (fn () =>
bulwahn@43123
  2006
      Pretty.block ([Pretty.quote (Syntax.pretty_term ctxt'' t'), Pretty.fbrk,
bulwahn@43123
  2007
        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt'' ty')]
wenzelm@55437
  2008
        @ pretty_stat)) ()
wenzelm@55437
  2009
  end |> Pretty.writeln
bulwahn@32667
  2010
wenzelm@55437
  2011
end