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