src/HOL/ex/predicate_compile.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 33004 715566791eb0
child 33038 8f9594c31de4
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
haftmann@31217
     1
(* Author: Lukas Bulwahn, TU Muenchen
haftmann@30374
     2
haftmann@30374
     3
(Prototype of) A compiler from predicates specified by intro/elim rules
haftmann@30374
     4
to equations.
haftmann@30374
     5
*)
haftmann@30374
     6
haftmann@30374
     7
signature PREDICATE_COMPILE =
haftmann@30374
     8
sig
haftmann@30972
     9
  type mode = int list option list * int list
bulwahn@32311
    10
  (*val add_equations_of: bool -> string list -> theory -> theory *)
bulwahn@31514
    11
  val register_predicate : (thm list * thm * int) -> theory -> theory
bulwahn@31877
    12
  val is_registered : theory -> string -> bool
bulwahn@32314
    13
 (* val fetch_pred_data : theory -> string -> (thm list * thm * int)  *)
bulwahn@31514
    14
  val predfun_intro_of: theory -> string -> mode -> thm
bulwahn@31514
    15
  val predfun_elim_of: theory -> string -> mode -> thm
bulwahn@31514
    16
  val strip_intro_concl: int -> term -> term * (term list * term list)
bulwahn@31514
    17
  val predfun_name_of: theory -> string -> mode -> string
bulwahn@31514
    18
  val all_preds_of : theory -> string list
haftmann@30972
    19
  val modes_of: theory -> string -> mode list
bulwahn@32306
    20
  val string_of_mode : mode -> string
bulwahn@31514
    21
  val intros_of: theory -> string -> thm list
bulwahn@31514
    22
  val nparams_of: theory -> string -> int
bulwahn@31876
    23
  val add_intro: thm -> theory -> theory
bulwahn@31876
    24
  val set_elim: thm -> theory -> theory
haftmann@31124
    25
  val setup: theory -> theory
haftmann@31124
    26
  val code_pred: string -> Proof.context -> Proof.state
haftmann@31124
    27
  val code_pred_cmd: string -> Proof.context -> Proof.state
bulwahn@31876
    28
  val print_stored_rules: theory -> unit
bulwahn@32306
    29
  val print_all_modes: theory -> unit
wenzelm@32740
    30
  val do_proofs: bool Unsynchronized.ref
bulwahn@31876
    31
  val mk_casesrule : Proof.context -> int -> thm list -> term
haftmann@31217
    32
  val analyze_compr: theory -> term -> term
wenzelm@32740
    33
  val eval_ref: (unit -> term Predicate.pred) option Unsynchronized.ref
bulwahn@32311
    34
  val add_equations : string list -> theory -> theory
bulwahn@31876
    35
  val code_pred_intros_attrib : attribute
bulwahn@32306
    36
  (* used by Quickcheck_Generator *) 
bulwahn@32308
    37
  (*val funT_of : mode -> typ -> typ
bulwahn@32306
    38
  val mk_if_pred : term -> term
bulwahn@32308
    39
  val mk_Eval : term * term -> term*)
bulwahn@32307
    40
  val mk_tupleT : typ list -> typ
bulwahn@32308
    41
(*  val mk_predT :  typ -> typ *)
bulwahn@32310
    42
  (* temporary for testing of the compilation *)
bulwahn@32310
    43
  datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term |
bulwahn@32310
    44
    GeneratorPrem of term list * term | Generator of (string * typ);
bulwahn@32308
    45
  val prepare_intrs: theory -> string list ->
bulwahn@32308
    46
    (string * typ) list * int * string list * string list * (string * mode list) list *
bulwahn@32308
    47
    (string * (term list * indprem list) list) list * (string * (int option list * int)) list
bulwahn@32310
    48
  datatype compilation_funs = CompilationFuns of {
bulwahn@32310
    49
    mk_predT : typ -> typ,
bulwahn@32310
    50
    dest_predT : typ -> typ,
bulwahn@32310
    51
    mk_bot : typ -> term,
bulwahn@32310
    52
    mk_single : term -> term,
bulwahn@32310
    53
    mk_bind : term * term -> term,
bulwahn@32310
    54
    mk_sup : term * term -> term,
bulwahn@32310
    55
    mk_if : term -> term,
bulwahn@32310
    56
    mk_not : term -> term,
haftmann@32351
    57
    mk_map : typ -> typ -> term -> term -> term,
bulwahn@32310
    58
    lift_pred : term -> term
bulwahn@32310
    59
  };  
bulwahn@32309
    60
  datatype tmode = Mode of mode * int list * tmode option list;
bulwahn@32310
    61
  type moded_clause = term list * (indprem * tmode) list
bulwahn@32310
    62
  type 'a pred_mode_table = (string * (mode * 'a) list) list
bulwahn@32310
    63
  val infer_modes : bool -> theory -> (string * (int list option list * int list) list) list
bulwahn@32308
    64
    -> (string * (int option list * int)) list -> string list
bulwahn@32309
    65
    -> (string * (term list * indprem list) list) list
bulwahn@32310
    66
    -> (moded_clause list) pred_mode_table
bulwahn@32310
    67
  val infer_modes_with_generator : theory -> (string * (int list option list * int list) list) list
bulwahn@32310
    68
    -> (string * (int option list * int)) list -> string list
bulwahn@32310
    69
    -> (string * (term list * indprem list) list) list
bulwahn@32310
    70
    -> (moded_clause list) pred_mode_table  
bulwahn@32311
    71
  (*val compile_preds : theory -> compilation_funs -> string list -> string list
bulwahn@32312
    72
    -> (string * typ) list -> (moded_clause list) pred_mode_table -> term pred_mode_table
bulwahn@32312
    73
  val rpred_create_definitions :(string * typ) list -> string * mode list
bulwahn@32310
    74
    -> theory -> theory 
bulwahn@32312
    75
  val split_smode : int list -> term list -> (term list * term list) *)
bulwahn@32310
    76
  val print_moded_clauses :
bulwahn@32310
    77
    theory -> (moded_clause list) pred_mode_table -> unit
bulwahn@32310
    78
  val print_compiled_terms : theory -> term pred_mode_table -> unit
bulwahn@32311
    79
  (*val rpred_prove_preds : theory -> term pred_mode_table -> thm pred_mode_table*)
bulwahn@32310
    80
  val rpred_compfuns : compilation_funs
bulwahn@32310
    81
  val dest_funT : typ -> typ * typ
bulwahn@32314
    82
 (* val depending_preds_of : theory -> thm list -> string list *)
bulwahn@32311
    83
  val add_quickcheck_equations : string list -> theory -> theory
bulwahn@32311
    84
  val add_sizelim_equations : string list -> theory -> theory
bulwahn@32311
    85
  val is_inductive_predicate : theory -> string -> bool
bulwahn@32311
    86
  val terms_vs : term list -> string list
bulwahn@32311
    87
  val subsets : int -> int -> int list list
bulwahn@32311
    88
  val check_mode_clause : bool -> theory -> string list ->
bulwahn@32311
    89
    (string * mode list) list -> (string * mode list) list -> mode -> (term list * indprem list)
bulwahn@32311
    90
      -> (term list * (indprem * tmode) list) option
bulwahn@32311
    91
  val string_of_moded_prem : theory -> (indprem * tmode) -> string
bulwahn@32311
    92
  val all_modes_of : theory -> (string * mode list) list
bulwahn@32311
    93
  val all_generator_modes_of : theory -> (string * mode list) list
bulwahn@32311
    94
  val compile_clause : compilation_funs -> term option -> (term list -> term) ->
bulwahn@32311
    95
    theory -> string list -> string list -> mode -> term -> moded_clause -> term
bulwahn@32312
    96
  val preprocess_intro : theory -> thm -> thm
bulwahn@32315
    97
  val is_constrt : theory -> term -> bool
bulwahn@32315
    98
  val is_predT : typ -> bool
bulwahn@32315
    99
  val guess_nparams : typ -> int
haftmann@30374
   100
end;
haftmann@30374
   101
haftmann@31124
   102
structure Predicate_Compile : PREDICATE_COMPILE =
haftmann@30374
   103
struct
haftmann@30374
   104
haftmann@30972
   105
(** auxiliary **)
haftmann@30972
   106
haftmann@30972
   107
(* debug stuff *)
wenzelm@31320
   108
wenzelm@32950
   109
fun tracing s = (if ! Toplevel.debug then tracing s else ());
haftmann@30972
   110
bulwahn@32314
   111
fun print_tac s = Seq.single; (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *)
wenzelm@32950
   112
fun debug_tac msg = Seq.single; (* (fn st => (tracing msg; Seq.single st)); *)
haftmann@30972
   113
wenzelm@32740
   114
val do_proofs = Unsynchronized.ref true;
haftmann@30972
   115
bulwahn@31514
   116
fun mycheat_tac thy i st =
wenzelm@32970
   117
  (Tactic.rtac (Skip_Proof.make_thm thy (Var (("A", 0), propT))) i) st
bulwahn@31514
   118
bulwahn@31550
   119
fun remove_last_goal thy st =
wenzelm@32970
   120
  (Tactic.rtac (Skip_Proof.make_thm thy (Var (("A", 0), propT))) (nprems_of st)) st
bulwahn@31550
   121
bulwahn@31514
   122
(* reference to preprocessing of InductiveSet package *)
bulwahn@31514
   123
haftmann@31723
   124
val ind_set_codegen_preproc = Inductive_Set.codegen_preproc;
haftmann@30972
   125
haftmann@30972
   126
(** fundamentals **)
haftmann@30972
   127
haftmann@30972
   128
(* syntactic operations *)
haftmann@30972
   129
haftmann@30972
   130
fun mk_eq (x, xs) =
haftmann@30972
   131
  let fun mk_eqs _ [] = []
haftmann@30972
   132
        | mk_eqs a (b::cs) =
haftmann@30972
   133
            HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
haftmann@30972
   134
  in mk_eqs x xs end;
haftmann@30972
   135
haftmann@30972
   136
fun mk_tupleT [] = HOLogic.unitT
haftmann@30972
   137
  | mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts;
haftmann@30972
   138
bulwahn@31514
   139
fun dest_tupleT (Type (@{type_name Product_Type.unit}, [])) = []
bulwahn@31514
   140
  | dest_tupleT (Type (@{type_name "*"}, [T1, T2])) = T1 :: (dest_tupleT T2)
bulwahn@31514
   141
  | dest_tupleT t = [t]
bulwahn@31514
   142
haftmann@30972
   143
fun mk_tuple [] = HOLogic.unit
haftmann@30972
   144
  | mk_tuple ts = foldr1 HOLogic.mk_prod ts;
haftmann@30972
   145
haftmann@30972
   146
fun dest_tuple (Const (@{const_name Product_Type.Unity}, _)) = []
haftmann@30972
   147
  | dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2)
haftmann@30972
   148
  | dest_tuple t = [t]
haftmann@30972
   149
bulwahn@32310
   150
fun mk_scomp (t, u) =
bulwahn@32310
   151
  let
bulwahn@32310
   152
    val T = fastype_of t
bulwahn@32310
   153
    val U = fastype_of u
bulwahn@32310
   154
    val [A] = binder_types T
bulwahn@32310
   155
    val D = body_type U 
bulwahn@32310
   156
  in 
bulwahn@32310
   157
    Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u
haftmann@30972
   158
  end;
haftmann@30972
   159
bulwahn@32310
   160
fun dest_funT (Type ("fun",[S, T])) = (S, T)
bulwahn@32310
   161
  | dest_funT T = raise TYPE ("dest_funT", [T], [])
bulwahn@32310
   162
 
bulwahn@32310
   163
fun mk_fun_comp (t, u) =
bulwahn@32310
   164
  let
bulwahn@32310
   165
    val (_, B) = dest_funT (fastype_of t)
bulwahn@32310
   166
    val (C, A) = dest_funT (fastype_of u)
bulwahn@32308
   167
  in
bulwahn@32310
   168
    Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
bulwahn@32308
   169
  end;
bulwahn@32308
   170
bulwahn@32312
   171
fun dest_randomT (Type ("fun", [@{typ Random.seed},
haftmann@32657
   172
  Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
bulwahn@32310
   173
  | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
bulwahn@32308
   174
bulwahn@31514
   175
(* destruction of intro rules *)
bulwahn@31514
   176
bulwahn@31514
   177
(* FIXME: look for other place where this functionality was used before *)
bulwahn@31514
   178
fun strip_intro_concl nparams intro = let
bulwahn@31514
   179
  val _ $ u = Logic.strip_imp_concl intro
bulwahn@31514
   180
  val (pred, all_args) = strip_comb u
bulwahn@31514
   181
  val (params, args) = chop nparams all_args
bulwahn@31514
   182
in (pred, (params, args)) end
haftmann@30972
   183
bulwahn@32312
   184
(** data structures **)
haftmann@30972
   185
bulwahn@32312
   186
type smode = int list;
bulwahn@32312
   187
type mode = smode option list * smode;
bulwahn@32309
   188
datatype tmode = Mode of mode * int list * tmode option list;
bulwahn@31514
   189
bulwahn@32312
   190
fun split_smode is ts =
bulwahn@32312
   191
  let
bulwahn@32312
   192
    fun split_smode' _ _ [] = ([], [])
bulwahn@32312
   193
      | split_smode' is i (t::ts) = (if i mem is then apfst else apsnd) (cons t)
bulwahn@32312
   194
          (split_smode' is (i+1) ts)
bulwahn@32312
   195
  in split_smode' is 1 ts end
bulwahn@32312
   196
bulwahn@32312
   197
fun split_mode (iss, is) ts =
bulwahn@32312
   198
  let
bulwahn@32312
   199
    val (t1, t2) = chop (length iss) ts 
bulwahn@32312
   200
  in (t1, split_smode is t2) end
bulwahn@32312
   201
bulwahn@32312
   202
fun string_of_mode (iss, is) = space_implode " -> " (map
bulwahn@32312
   203
  (fn NONE => "X"
bulwahn@32312
   204
    | SOME js => enclose "[" "]" (commas (map string_of_int js)))
bulwahn@32312
   205
       (iss @ [SOME is]));
bulwahn@32310
   206
bulwahn@32316
   207
fun string_of_tmode (Mode (predmode, termmode, param_modes)) =
bulwahn@32316
   208
  "predmode: " ^ (string_of_mode predmode) ^ 
bulwahn@32316
   209
  (if null param_modes then "" else
bulwahn@32316
   210
    "; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes))
bulwahn@32316
   211
    
bulwahn@32310
   212
datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term |
bulwahn@32310
   213
  GeneratorPrem of term list * term | Generator of (string * typ);
bulwahn@32310
   214
bulwahn@32310
   215
type moded_clause = term list * (indprem * tmode) list
bulwahn@32310
   216
type 'a pred_mode_table = (string * (mode * 'a) list) list
bulwahn@32310
   217
bulwahn@31514
   218
datatype predfun_data = PredfunData of {
bulwahn@31514
   219
  name : string,
bulwahn@31514
   220
  definition : thm,
bulwahn@31514
   221
  intro : thm,
bulwahn@31514
   222
  elim : thm
bulwahn@31514
   223
};
bulwahn@31514
   224
bulwahn@31514
   225
fun rep_predfun_data (PredfunData data) = data;
bulwahn@31514
   226
fun mk_predfun_data (name, definition, intro, elim) =
bulwahn@31514
   227
  PredfunData {name = name, definition = definition, intro = intro, elim = elim}
haftmann@30972
   228
bulwahn@32311
   229
datatype function_data = FunctionData of {
bulwahn@32310
   230
  name : string,
bulwahn@32311
   231
  equation : thm option (* is not used at all? *)
bulwahn@32310
   232
};
bulwahn@32310
   233
bulwahn@32311
   234
fun rep_function_data (FunctionData data) = data;
bulwahn@32311
   235
fun mk_function_data (name, equation) =
bulwahn@32311
   236
  FunctionData {name = name, equation = equation}
bulwahn@32310
   237
bulwahn@31514
   238
datatype pred_data = PredData of {
bulwahn@31514
   239
  intros : thm list,
bulwahn@31514
   240
  elim : thm option,
bulwahn@31514
   241
  nparams : int,
bulwahn@32310
   242
  functions : (mode * predfun_data) list,
bulwahn@32311
   243
  generators : (mode * function_data) list,
bulwahn@32311
   244
  sizelim_functions : (mode * function_data) list 
bulwahn@31514
   245
};
haftmann@30374
   246
bulwahn@31514
   247
fun rep_pred_data (PredData data) = data;
bulwahn@32311
   248
fun mk_pred_data ((intros, elim, nparams), (functions, generators, sizelim_functions)) =
bulwahn@32310
   249
  PredData {intros = intros, elim = elim, nparams = nparams,
bulwahn@32311
   250
    functions = functions, generators = generators, sizelim_functions = sizelim_functions}
bulwahn@32311
   251
fun map_pred_data f (PredData {intros, elim, nparams, functions, generators, sizelim_functions}) =
bulwahn@32311
   252
  mk_pred_data (f ((intros, elim, nparams), (functions, generators, sizelim_functions)))
bulwahn@31514
   253
  
bulwahn@31514
   254
fun eq_option eq (NONE, NONE) = true
bulwahn@31514
   255
  | eq_option eq (SOME x, SOME y) = eq (x, y)
bulwahn@31514
   256
  | eq_option eq _ = false
bulwahn@31514
   257
  
bulwahn@31514
   258
fun eq_pred_data (PredData d1, PredData d2) = 
bulwahn@31514
   259
  eq_list (Thm.eq_thm) (#intros d1, #intros d2) andalso
bulwahn@31514
   260
  eq_option (Thm.eq_thm) (#elim d1, #elim d2) andalso
bulwahn@31514
   261
  #nparams d1 = #nparams d2
bulwahn@31514
   262
  
bulwahn@31514
   263
structure PredData = TheoryDataFun
haftmann@30374
   264
(
bulwahn@31514
   265
  type T = pred_data Graph.T;
bulwahn@31514
   266
  val empty = Graph.empty;
haftmann@30374
   267
  val copy = I;
haftmann@30374
   268
  val extend = I;
bulwahn@31514
   269
  fun merge _ = Graph.merge eq_pred_data;
haftmann@30374
   270
);
haftmann@30374
   271
bulwahn@31514
   272
(* queries *)
bulwahn@31514
   273
bulwahn@31549
   274
fun lookup_pred_data thy name =
bulwahn@31573
   275
  Option.map rep_pred_data (try (Graph.get_node (PredData.get thy)) name)
bulwahn@31514
   276
bulwahn@31514
   277
fun the_pred_data thy name = case lookup_pred_data thy name
bulwahn@32312
   278
 of NONE => error ("No such predicate " ^ quote name)  
bulwahn@31514
   279
  | SOME data => data;
bulwahn@31514
   280
bulwahn@31877
   281
val is_registered = is_some oo lookup_pred_data 
haftmann@30374
   282
bulwahn@31514
   283
val all_preds_of = Graph.keys o PredData.get
bulwahn@31514
   284
bulwahn@31514
   285
val intros_of = #intros oo the_pred_data
bulwahn@31514
   286
bulwahn@31514
   287
fun the_elim_of thy name = case #elim (the_pred_data thy name)
bulwahn@31514
   288
 of NONE => error ("No elimination rule for predicate " ^ quote name)
bulwahn@31514
   289
  | SOME thm => thm 
bulwahn@31514
   290
  
bulwahn@31514
   291
val has_elim = is_some o #elim oo the_pred_data;
bulwahn@31514
   292
bulwahn@31514
   293
val nparams_of = #nparams oo the_pred_data
haftmann@30374
   294
bulwahn@31514
   295
val modes_of = (map fst) o #functions oo the_pred_data
bulwahn@31514
   296
bulwahn@31514
   297
fun all_modes_of thy = map (fn name => (name, modes_of thy name)) (all_preds_of thy) 
bulwahn@31514
   298
bulwahn@31514
   299
val is_compiled = not o null o #functions oo the_pred_data
bulwahn@31514
   300
bulwahn@31514
   301
fun lookup_predfun_data thy name mode =
bulwahn@31514
   302
  Option.map rep_predfun_data (AList.lookup (op =)
bulwahn@31514
   303
  (#functions (the_pred_data thy name)) mode)
haftmann@30374
   304
bulwahn@31514
   305
fun the_predfun_data thy name mode = case lookup_predfun_data thy name mode
bulwahn@32310
   306
  of NONE => error ("No function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name)
bulwahn@32310
   307
   | SOME data => data;
bulwahn@31514
   308
bulwahn@31514
   309
val predfun_name_of = #name ooo the_predfun_data
bulwahn@31514
   310
bulwahn@31514
   311
val predfun_definition_of = #definition ooo the_predfun_data
bulwahn@31514
   312
bulwahn@31514
   313
val predfun_intro_of = #intro ooo the_predfun_data
bulwahn@31514
   314
bulwahn@31514
   315
val predfun_elim_of = #elim ooo the_predfun_data
bulwahn@31514
   316
bulwahn@32310
   317
fun lookup_generator_data thy name mode = 
bulwahn@32311
   318
  Option.map rep_function_data (AList.lookup (op =)
bulwahn@32310
   319
  (#generators (the_pred_data thy name)) mode)
bulwahn@32310
   320
  
bulwahn@32310
   321
fun the_generator_data thy name mode = case lookup_generator_data thy name mode
bulwahn@32310
   322
  of NONE => error ("No generator defined for mode " ^ string_of_mode mode ^ " of predicate " ^ name)
bulwahn@32310
   323
   | SOME data => data
bulwahn@32310
   324
bulwahn@32310
   325
val generator_name_of = #name ooo the_generator_data
bulwahn@32310
   326
bulwahn@32311
   327
val generator_modes_of = (map fst) o #generators oo the_pred_data
bulwahn@32311
   328
bulwahn@32311
   329
fun all_generator_modes_of thy =
bulwahn@32311
   330
  map (fn name => (name, generator_modes_of thy name)) (all_preds_of thy) 
bulwahn@32311
   331
bulwahn@32311
   332
fun lookup_sizelim_function_data thy name mode =
bulwahn@32311
   333
  Option.map rep_function_data (AList.lookup (op =)
bulwahn@32311
   334
  (#sizelim_functions (the_pred_data thy name)) mode)
bulwahn@32311
   335
bulwahn@32311
   336
fun the_sizelim_function_data thy name mode = case lookup_sizelim_function_data thy name mode
bulwahn@32311
   337
  of NONE => error ("No size-limited function defined for mode " ^ string_of_mode mode
bulwahn@32311
   338
    ^ " of predicate " ^ name)
bulwahn@32311
   339
   | SOME data => data
bulwahn@32311
   340
bulwahn@32311
   341
val sizelim_function_name_of = #name ooo the_sizelim_function_data
bulwahn@32311
   342
bulwahn@32311
   343
(*val generator_modes_of = (map fst) o #generators oo the_pred_data*)
bulwahn@32312
   344
     
bulwahn@32310
   345
(* diagnostic display functions *)
bulwahn@32308
   346
wenzelm@32950
   347
fun print_modes modes = tracing ("Inferred modes:\n" ^
bulwahn@32312
   348
  cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
bulwahn@32312
   349
    string_of_mode ms)) modes));
bulwahn@32312
   350
bulwahn@32312
   351
fun print_pred_mode_table string_of_entry thy pred_mode_table =
bulwahn@32312
   352
  let
bulwahn@32312
   353
    fun print_mode pred (mode, entry) =  "mode : " ^ (string_of_mode mode)
bulwahn@32312
   354
      ^ (string_of_entry pred mode entry)  
bulwahn@32312
   355
    fun print_pred (pred, modes) =
bulwahn@32312
   356
      "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
wenzelm@32950
   357
    val _ = tracing (cat_lines (map print_pred pred_mode_table))
bulwahn@32312
   358
  in () end;
bulwahn@32312
   359
bulwahn@32316
   360
fun string_of_moded_prem thy (Prem (ts, p), tmode) =
bulwahn@32312
   361
    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
bulwahn@32316
   362
    "(" ^ (string_of_tmode tmode) ^ ")"
bulwahn@32316
   363
  | string_of_moded_prem thy (GeneratorPrem (ts, p), Mode (predmode, is, _)) =
bulwahn@32312
   364
    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
bulwahn@32316
   365
    "(generator_mode: " ^ (string_of_mode predmode) ^ ")"
bulwahn@32312
   366
  | string_of_moded_prem thy (Generator (v, T), _) =
bulwahn@32312
   367
    "Generator for " ^ v ^ " of Type " ^ (Syntax.string_of_typ_global thy T)
bulwahn@32312
   368
  | string_of_moded_prem thy (Negprem (ts, p), Mode (_, is, _)) =
bulwahn@32312
   369
    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
bulwahn@32312
   370
    "(negative mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"
bulwahn@32312
   371
  | string_of_moded_prem thy (Sidecond t, Mode (_, is, _)) =
bulwahn@32312
   372
    (Syntax.string_of_term_global thy t) ^
bulwahn@32312
   373
    "(sidecond mode: " ^ (space_implode ", " (map string_of_int is)) ^ ")"    
bulwahn@32312
   374
  | string_of_moded_prem _ _ = error "string_of_moded_prem: unimplemented"
bulwahn@32312
   375
     
bulwahn@32312
   376
fun print_moded_clauses thy =
bulwahn@32312
   377
  let        
bulwahn@32312
   378
    fun string_of_clause pred mode clauses =
bulwahn@32312
   379
      cat_lines (map (fn (ts, prems) => (space_implode " --> "
bulwahn@32312
   380
        (map (string_of_moded_prem thy) prems)) ^ " --> " ^ pred ^ " "
bulwahn@32312
   381
        ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))) clauses)
bulwahn@32312
   382
  in print_pred_mode_table string_of_clause thy end;
bulwahn@32312
   383
bulwahn@32312
   384
fun print_compiled_terms thy =
bulwahn@32312
   385
  print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy
bulwahn@32312
   386
    
bulwahn@31876
   387
fun print_stored_rules thy =
bulwahn@31876
   388
  let
bulwahn@31876
   389
    val preds = (Graph.keys o PredData.get) thy
bulwahn@31876
   390
    fun print pred () = let
bulwahn@31876
   391
      val _ = writeln ("predicate: " ^ pred)
bulwahn@31876
   392
      val _ = writeln ("number of parameters: " ^ string_of_int (nparams_of thy pred))
bulwahn@31876
   393
      val _ = writeln ("introrules: ")
wenzelm@32091
   394
      val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm))
bulwahn@31876
   395
        (rev (intros_of thy pred)) ()
bulwahn@31876
   396
    in
bulwahn@31876
   397
      if (has_elim thy pred) then
wenzelm@32091
   398
        writeln ("elimrule: " ^ Display.string_of_thm_global thy (the_elim_of thy pred))
bulwahn@31876
   399
      else
bulwahn@31876
   400
        writeln ("no elimrule defined")
bulwahn@31876
   401
    end
bulwahn@31876
   402
  in
bulwahn@31876
   403
    fold print preds ()
bulwahn@31876
   404
  end;
haftmann@30374
   405
bulwahn@32306
   406
fun print_all_modes thy =
bulwahn@32306
   407
  let
bulwahn@32306
   408
    val _ = writeln ("Inferred modes:")
bulwahn@32306
   409
    fun print (pred, modes) u =
bulwahn@32306
   410
      let
bulwahn@32306
   411
        val _ = writeln ("predicate: " ^ pred)
bulwahn@32306
   412
        val _ = writeln ("modes: " ^ (commas (map string_of_mode modes)))
bulwahn@32306
   413
      in u end  
bulwahn@32306
   414
  in
bulwahn@32306
   415
    fold print (all_modes_of thy) ()
bulwahn@32306
   416
  end
bulwahn@32312
   417
  
bulwahn@31876
   418
(** preprocessing rules **)  
bulwahn@31573
   419
bulwahn@31573
   420
fun imp_prems_conv cv ct =
bulwahn@31573
   421
  case Thm.term_of ct of
bulwahn@31573
   422
    Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
bulwahn@31573
   423
  | _ => Conv.all_conv ct
bulwahn@31573
   424
bulwahn@31573
   425
fun Trueprop_conv cv ct =
bulwahn@31573
   426
  case Thm.term_of ct of
bulwahn@31573
   427
    Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct  
bulwahn@31573
   428
  | _ => error "Trueprop_conv"
bulwahn@31573
   429
bulwahn@31573
   430
fun preprocess_intro thy rule =
bulwahn@31573
   431
  Conv.fconv_rule
bulwahn@31573
   432
    (imp_prems_conv
bulwahn@31573
   433
      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
bulwahn@31573
   434
    (Thm.transfer thy rule)
bulwahn@31573
   435
bulwahn@32313
   436
fun preprocess_elim thy nparams elimrule =
bulwahn@32313
   437
  let
bulwahn@32313
   438
    fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
bulwahn@32313
   439
       HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
bulwahn@32313
   440
     | replace_eqs t = t
bulwahn@32313
   441
    val prems = Thm.prems_of elimrule
bulwahn@32313
   442
    val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems)))) - nparams
bulwahn@32313
   443
    fun preprocess_case t =
bulwahn@32313
   444
     let
bulwahn@32313
   445
       val params = Logic.strip_params t
bulwahn@32313
   446
       val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t)
bulwahn@32313
   447
       val assums_hyp' = assums1 @ (map replace_eqs assums2)
bulwahn@32313
   448
     in
bulwahn@32313
   449
       list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t))
bulwahn@32313
   450
     end 
bulwahn@32313
   451
    val cases' = map preprocess_case (tl prems)
bulwahn@32313
   452
    val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
bulwahn@32313
   453
  in
bulwahn@32313
   454
    Thm.equal_elim
bulwahn@32313
   455
      (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm eq_is_eq}])
bulwahn@32313
   456
         (cterm_of thy elimrule')))
bulwahn@32313
   457
      elimrule
bulwahn@32313
   458
  end;
bulwahn@31573
   459
bulwahn@32308
   460
(* special case: predicate with no introduction rule *)
bulwahn@32313
   461
fun noclause thy predname elim = let
bulwahn@32308
   462
  val T = (Logic.unvarifyT o Sign.the_const_type thy) predname
bulwahn@32308
   463
  val Ts = binder_types T
bulwahn@32308
   464
  val names = Name.variant_list []
bulwahn@32308
   465
        (map (fn i => "x" ^ (string_of_int i)) (1 upto (length Ts)))
bulwahn@32308
   466
  val vs = map2 (curry Free) names Ts
bulwahn@32313
   467
  val clausehd = HOLogic.mk_Trueprop (list_comb (Const (predname, T), vs))
bulwahn@32308
   468
  val intro_t = Logic.mk_implies (@{prop False}, clausehd)
bulwahn@32308
   469
  val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))
bulwahn@32308
   470
  val elim_t = Logic.list_implies ([clausehd, Logic.mk_implies (@{prop False}, P)], P)
bulwahn@32308
   471
  val intro = Goal.prove (ProofContext.init thy) names [] intro_t
bulwahn@32308
   472
        (fn {...} => etac @{thm FalseE} 1)
bulwahn@32308
   473
  val elim = Goal.prove (ProofContext.init thy) ("P" :: names) [] elim_t
bulwahn@32313
   474
        (fn {...} => etac elim 1) 
bulwahn@32308
   475
in
bulwahn@32314
   476
  ([intro], elim)
bulwahn@32308
   477
end
bulwahn@32308
   478
bulwahn@31573
   479
fun fetch_pred_data thy name =
haftmann@31723
   480
  case try (Inductive.the_inductive (ProofContext.init thy)) name of
bulwahn@31573
   481
    SOME (info as (_, result)) => 
bulwahn@31573
   482
      let
bulwahn@31573
   483
        fun is_intro_of intro =
bulwahn@31573
   484
          let
bulwahn@31573
   485
            val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
bulwahn@32313
   486
          in (fst (dest_Const const) = name) end;      
bulwahn@32313
   487
        val intros = ind_set_codegen_preproc thy ((map (preprocess_intro thy))
bulwahn@32313
   488
          (filter is_intro_of (#intrs result)))
bulwahn@32313
   489
        val pre_elim = nth (#elims result) (find_index (fn s => s = name) (#names (fst info)))
haftmann@31723
   490
        val nparams = length (Inductive.params_of (#raw_induct result))
bulwahn@32313
   491
        val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams pre_elim)
bulwahn@32314
   492
        val (intros, elim) = if null intros then noclause thy name elim else (intros, elim)
bulwahn@32313
   493
      in
bulwahn@32314
   494
        mk_pred_data ((intros, SOME elim, nparams), ([], [], []))
bulwahn@32313
   495
      end                                                                    
bulwahn@31573
   496
  | NONE => error ("No such predicate: " ^ quote name)
bulwahn@31573
   497
  
bulwahn@31514
   498
(* updaters *)
bulwahn@31514
   499
bulwahn@32311
   500
fun apfst3 f (x, y, z) =  (f x, y, z)
bulwahn@32311
   501
fun apsnd3 f (x, y, z) =  (x, f y, z)
bulwahn@32311
   502
fun aptrd3 f (x, y, z) =  (x, y, f z)
bulwahn@32311
   503
bulwahn@32310
   504
fun add_predfun name mode data =
bulwahn@32310
   505
  let
bulwahn@32311
   506
    val add = (apsnd o apfst3 o cons) (mode, mk_predfun_data data)
bulwahn@31514
   507
  in PredData.map (Graph.map_node name (map_pred_data add)) end
haftmann@30374
   508
bulwahn@31876
   509
fun is_inductive_predicate thy name =
bulwahn@31876
   510
  is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
bulwahn@31876
   511
bulwahn@32314
   512
fun depending_preds_of thy (key, value) =
bulwahn@32314
   513
  let
bulwahn@32314
   514
    val intros = (#intros o rep_pred_data) value
bulwahn@32314
   515
  in
bulwahn@32314
   516
    fold Term.add_const_names (map Thm.prop_of intros) []
bulwahn@32314
   517
      |> filter (fn c => (not (c = key)) andalso (is_inductive_predicate thy c orelse is_registered thy c))
bulwahn@32314
   518
  end;
bulwahn@32314
   519
    
bulwahn@32314
   520
    
bulwahn@31876
   521
(* code dependency graph *)    
bulwahn@32314
   522
(*
bulwahn@31876
   523
fun dependencies_of thy name =
bulwahn@31876
   524
  let
bulwahn@31876
   525
    val (intros, elim, nparams) = fetch_pred_data thy name 
bulwahn@32311
   526
    val data = mk_pred_data ((intros, SOME elim, nparams), ([], [], []))
bulwahn@31876
   527
    val keys = depending_preds_of thy intros
bulwahn@31876
   528
  in
bulwahn@31876
   529
    (data, keys)
bulwahn@31876
   530
  end;
bulwahn@32314
   531
*)
bulwahn@32315
   532
(* guessing number of parameters *)
bulwahn@32315
   533
fun find_indexes pred xs =
bulwahn@32315
   534
  let
bulwahn@32315
   535
    fun find is n [] = is
bulwahn@32315
   536
      | find is n (x :: xs) = find (if pred x then (n :: is) else is) (n + 1) xs;
bulwahn@32315
   537
  in rev (find [] 0 xs) end;
bulwahn@31876
   538
bulwahn@32315
   539
fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT)
bulwahn@32315
   540
  | is_predT _ = false
bulwahn@32315
   541
  
bulwahn@32315
   542
fun guess_nparams T =
bulwahn@32315
   543
  let
bulwahn@32315
   544
    val argTs = binder_types T
bulwahn@32315
   545
    val nparams = fold (curry Int.max)
bulwahn@32315
   546
      (map (fn x => x + 1) (find_indexes is_predT argTs)) 0
bulwahn@32315
   547
  in nparams end;
bulwahn@32315
   548
bulwahn@31573
   549
fun add_intro thm thy = let
bulwahn@32315
   550
   val (name, T) = dest_Const (fst (strip_intro_concl 0 (prop_of thm)))
bulwahn@31573
   551
   fun cons_intro gr =
bulwahn@31573
   552
     case try (Graph.get_node gr) name of
bulwahn@31573
   553
       SOME pred_data => Graph.map_node name (map_pred_data
bulwahn@31573
   554
         (apfst (fn (intro, elim, nparams) => (thm::intro, elim, nparams)))) gr
bulwahn@31573
   555
     | NONE =>
bulwahn@31573
   556
       let
bulwahn@32315
   557
         val nparams = the_default (guess_nparams T)  (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name)
bulwahn@32311
   558
       in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), ([], [], []))) gr end;
bulwahn@31573
   559
  in PredData.map cons_intro thy end
bulwahn@31514
   560
bulwahn@31514
   561
fun set_elim thm = let
bulwahn@31514
   562
    val (name, _) = dest_Const (fst 
bulwahn@31514
   563
      (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
bulwahn@31514
   564
    fun set (intros, _, nparams) = (intros, SOME thm, nparams)  
bulwahn@31514
   565
  in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
haftmann@30374
   566
bulwahn@31514
   567
fun set_nparams name nparams = let
bulwahn@31514
   568
    fun set (intros, elim, _ ) = (intros, elim, nparams) 
bulwahn@31514
   569
  in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
bulwahn@32308
   570
    
bulwahn@32314
   571
fun register_predicate (pre_intros, pre_elim, nparams) thy = let
bulwahn@32314
   572
    val (name, _) = dest_Const (fst (strip_intro_concl nparams (prop_of (hd pre_intros))))
bulwahn@32314
   573
    (* preprocessing *)
bulwahn@32314
   574
    val intros = ind_set_codegen_preproc thy (map (preprocess_intro thy) pre_intros)
bulwahn@32314
   575
    val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams pre_elim)
bulwahn@31876
   576
  in
bulwahn@32314
   577
    PredData.map
bulwahn@32314
   578
      (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), ([], [], [])))) thy
bulwahn@31876
   579
  end
haftmann@30374
   580
bulwahn@32310
   581
fun set_generator_name pred mode name = 
bulwahn@32310
   582
  let
bulwahn@32311
   583
    val set = (apsnd o apsnd3 o cons) (mode, mk_function_data (name, NONE))
bulwahn@32310
   584
  in
bulwahn@32310
   585
    PredData.map (Graph.map_node pred (map_pred_data set))
bulwahn@32310
   586
  end
bulwahn@32310
   587
bulwahn@32311
   588
fun set_sizelim_function_name pred mode name = 
bulwahn@32311
   589
  let
bulwahn@32311
   590
    val set = (apsnd o aptrd3 o cons) (mode, mk_function_data (name, NONE))
bulwahn@32311
   591
  in
bulwahn@32311
   592
    PredData.map (Graph.map_node pred (map_pred_data set))
bulwahn@32311
   593
  end
bulwahn@32310
   594
bulwahn@32310
   595
(** data structures for generic compilation for different monads **)
bulwahn@32310
   596
bulwahn@32310
   597
(* maybe rename functions more generic:
bulwahn@32310
   598
  mk_predT -> mk_monadT; dest_predT -> dest_monadT
bulwahn@32310
   599
  mk_single -> mk_return (?)
bulwahn@32310
   600
*)
bulwahn@32310
   601
datatype compilation_funs = CompilationFuns of {
bulwahn@32310
   602
  mk_predT : typ -> typ,
bulwahn@32310
   603
  dest_predT : typ -> typ,
bulwahn@32310
   604
  mk_bot : typ -> term,
bulwahn@32310
   605
  mk_single : term -> term,
bulwahn@32310
   606
  mk_bind : term * term -> term,
bulwahn@32310
   607
  mk_sup : term * term -> term,
bulwahn@32310
   608
  mk_if : term -> term,
bulwahn@32310
   609
  mk_not : term -> term,
bulwahn@32311
   610
(*  funT_of : mode -> typ -> typ, *)
bulwahn@32311
   611
(*  mk_fun_of : theory -> (string * typ) -> mode -> term, *) 
haftmann@32351
   612
  mk_map : typ -> typ -> term -> term -> term,
bulwahn@32310
   613
  lift_pred : term -> term
bulwahn@32310
   614
};
bulwahn@32310
   615
bulwahn@32310
   616
fun mk_predT (CompilationFuns funs) = #mk_predT funs
bulwahn@32310
   617
fun dest_predT (CompilationFuns funs) = #dest_predT funs
bulwahn@32310
   618
fun mk_bot (CompilationFuns funs) = #mk_bot funs
bulwahn@32310
   619
fun mk_single (CompilationFuns funs) = #mk_single funs
bulwahn@32310
   620
fun mk_bind (CompilationFuns funs) = #mk_bind funs
bulwahn@32310
   621
fun mk_sup (CompilationFuns funs) = #mk_sup funs
bulwahn@32310
   622
fun mk_if (CompilationFuns funs) = #mk_if funs
bulwahn@32310
   623
fun mk_not (CompilationFuns funs) = #mk_not funs
bulwahn@32311
   624
(*fun funT_of (CompilationFuns funs) = #funT_of funs*)
bulwahn@32311
   625
(*fun mk_fun_of (CompilationFuns funs) = #mk_fun_of funs*)
haftmann@32351
   626
fun mk_map (CompilationFuns funs) = #mk_map funs
bulwahn@32310
   627
fun lift_pred (CompilationFuns funs) = #lift_pred funs
bulwahn@32310
   628
bulwahn@32311
   629
fun funT_of compfuns (iss, is) T =
bulwahn@32311
   630
  let
bulwahn@32311
   631
    val Ts = binder_types T
bulwahn@32312
   632
    val (paramTs, (inargTs, outargTs)) = split_mode (iss, is) Ts
bulwahn@32313
   633
    val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs 
bulwahn@32311
   634
  in
bulwahn@32311
   635
    (paramTs' @ inargTs) ---> (mk_predT compfuns (mk_tupleT outargTs))
bulwahn@32311
   636
  end;
bulwahn@32311
   637
bulwahn@32311
   638
fun sizelim_funT_of compfuns (iss, is) T =
bulwahn@32311
   639
  let
bulwahn@32311
   640
    val Ts = binder_types T
bulwahn@32312
   641
    val (paramTs, (inargTs, outargTs)) = split_mode (iss, is) Ts
bulwahn@32311
   642
    val paramTs' = map2 (fn SOME is => sizelim_funT_of compfuns ([], is) | NONE => I) iss paramTs 
bulwahn@32311
   643
  in
bulwahn@32311
   644
    (paramTs' @ inargTs @ [@{typ "code_numeral"}]) ---> (mk_predT compfuns (mk_tupleT outargTs))
bulwahn@32311
   645
  end;  
bulwahn@32311
   646
bulwahn@32311
   647
fun mk_fun_of compfuns thy (name, T) mode = 
bulwahn@32311
   648
  Const (predfun_name_of thy name mode, funT_of compfuns mode T)
bulwahn@32311
   649
bulwahn@32311
   650
fun mk_sizelim_fun_of compfuns thy (name, T) mode =
bulwahn@32311
   651
  Const (sizelim_function_name_of thy name mode, sizelim_funT_of compfuns mode T)
bulwahn@32311
   652
  
bulwahn@32311
   653
fun mk_generator_of compfuns thy (name, T) mode = 
bulwahn@32311
   654
  Const (generator_name_of thy name mode, sizelim_funT_of compfuns mode T)
bulwahn@32311
   655
bulwahn@32311
   656
bulwahn@32310
   657
structure PredicateCompFuns =
bulwahn@32310
   658
struct
bulwahn@32310
   659
bulwahn@32310
   660
fun mk_predT T = Type (@{type_name "Predicate.pred"}, [T])
bulwahn@32310
   661
bulwahn@32310
   662
fun dest_predT (Type (@{type_name "Predicate.pred"}, [T])) = T
bulwahn@32310
   663
  | dest_predT T = raise TYPE ("dest_predT", [T], []);
bulwahn@32310
   664
bulwahn@32310
   665
fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
bulwahn@32310
   666
bulwahn@32310
   667
fun mk_single t =
bulwahn@32310
   668
  let val T = fastype_of t
bulwahn@32310
   669
  in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end;
bulwahn@32310
   670
bulwahn@32310
   671
fun mk_bind (x, f) =
bulwahn@32310
   672
  let val T as Type ("fun", [_, U]) = fastype_of f
bulwahn@32310
   673
  in
bulwahn@32310
   674
    Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@32310
   675
  end;
bulwahn@32310
   676
bulwahn@32310
   677
val mk_sup = HOLogic.mk_binop @{const_name sup};
bulwahn@32310
   678
bulwahn@32310
   679
fun mk_if cond = Const (@{const_name Predicate.if_pred},
bulwahn@32310
   680
  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
bulwahn@32310
   681
bulwahn@32310
   682
fun mk_not t = let val T = mk_predT HOLogic.unitT
bulwahn@32310
   683
  in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
bulwahn@32310
   684
bulwahn@32310
   685
fun mk_Enum f =
bulwahn@32310
   686
  let val T as Type ("fun", [T', _]) = fastype_of f
bulwahn@32310
   687
  in
bulwahn@32310
   688
    Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f    
bulwahn@32310
   689
  end;
bulwahn@32310
   690
bulwahn@32310
   691
fun mk_Eval (f, x) =
bulwahn@32311
   692
  let
bulwahn@32311
   693
    val T = fastype_of x
bulwahn@32310
   694
  in
bulwahn@32310
   695
    Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
bulwahn@32310
   696
  end;
haftmann@32351
   697
haftmann@32351
   698
fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
haftmann@32351
   699
  (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
haftmann@32351
   700
bulwahn@32310
   701
val lift_pred = I
bulwahn@32310
   702
bulwahn@32310
   703
val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
bulwahn@32310
   704
  mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
haftmann@32351
   705
  mk_map = mk_map, lift_pred = lift_pred};
bulwahn@32310
   706
bulwahn@32310
   707
end;
bulwahn@32310
   708
bulwahn@32310
   709
(* termify_code:
haftmann@32657
   710
val termT = Type ("Code_Evaluation.term", []);
bulwahn@32310
   711
fun termifyT T = HOLogic.mk_prodT (T, HOLogic.unitT --> termT)
bulwahn@32310
   712
*)
bulwahn@32311
   713
(*
bulwahn@32310
   714
fun lift_random random =
bulwahn@32310
   715
  let
bulwahn@32310
   716
    val T = dest_randomT (fastype_of random)
bulwahn@32310
   717
  in
bulwahn@32310
   718
    mk_scomp (random,
bulwahn@32310
   719
      mk_fun_comp (HOLogic.pair_const (PredicateCompFuns.mk_predT T) @{typ Random.seed},
bulwahn@32310
   720
        mk_fun_comp (Const (@{const_name Predicate.single}, T --> (PredicateCompFuns.mk_predT T)),
bulwahn@32310
   721
          Const (@{const_name "fst"}, HOLogic.mk_prodT (T, @{typ "unit => term"}) --> T)))) 
bulwahn@32310
   722
  end;
bulwahn@32311
   723
*)
bulwahn@32311
   724
 
bulwahn@32310
   725
structure RPredCompFuns =
bulwahn@32310
   726
struct
bulwahn@32310
   727
bulwahn@32310
   728
fun mk_rpredT T =
bulwahn@32310
   729
  @{typ "Random.seed"} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ "Random.seed"})
bulwahn@32310
   730
bulwahn@32310
   731
fun dest_rpredT (Type ("fun", [_,
bulwahn@32310
   732
  Type (@{type_name "*"}, [Type (@{type_name "Predicate.pred"}, [T]), _])])) = T
bulwahn@32310
   733
  | dest_rpredT T = raise TYPE ("dest_rpredT", [T], []); 
bulwahn@32310
   734
bulwahn@32310
   735
fun mk_bot T = Const(@{const_name RPred.bot}, mk_rpredT T)
bulwahn@32310
   736
bulwahn@32310
   737
fun mk_single t =
bulwahn@32310
   738
  let
bulwahn@32310
   739
    val T = fastype_of t
bulwahn@32310
   740
  in
bulwahn@32310
   741
    Const (@{const_name RPred.return}, T --> mk_rpredT T) $ t
bulwahn@32310
   742
  end;
bulwahn@32310
   743
bulwahn@32310
   744
fun mk_bind (x, f) =
bulwahn@32310
   745
  let
bulwahn@32310
   746
    val T as (Type ("fun", [_, U])) = fastype_of f
bulwahn@32310
   747
  in
bulwahn@32310
   748
    Const (@{const_name RPred.bind}, fastype_of x --> T --> U) $ x $ f
bulwahn@32310
   749
  end
bulwahn@32310
   750
bulwahn@32310
   751
val mk_sup = HOLogic.mk_binop @{const_name RPred.supp}
bulwahn@32310
   752
bulwahn@32310
   753
fun mk_if cond = Const (@{const_name RPred.if_rpred},
bulwahn@32310
   754
  HOLogic.boolT --> mk_rpredT HOLogic.unitT) $ cond;
bulwahn@32310
   755
bulwahn@32310
   756
fun mk_not t = error "Negation is not defined for RPred"
haftmann@32351
   757
haftmann@32351
   758
fun mk_map t = error "FIXME" (*FIXME*)
haftmann@32351
   759
bulwahn@32310
   760
fun lift_pred t =
bulwahn@32310
   761
  let
bulwahn@32310
   762
    val T = PredicateCompFuns.dest_predT (fastype_of t)
bulwahn@32310
   763
    val lift_predT = PredicateCompFuns.mk_predT T --> mk_rpredT T 
bulwahn@32310
   764
  in
bulwahn@32310
   765
    Const (@{const_name "RPred.lift_pred"}, lift_predT) $ t  
bulwahn@32310
   766
  end;
bulwahn@32310
   767
bulwahn@32310
   768
val compfuns = CompilationFuns {mk_predT = mk_rpredT, dest_predT = dest_rpredT, mk_bot = mk_bot,
bulwahn@32310
   769
    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
haftmann@32351
   770
    mk_map = mk_map, lift_pred = lift_pred};
bulwahn@32310
   771
bulwahn@32310
   772
end;
bulwahn@32310
   773
(* for external use with interactive mode *)
bulwahn@32310
   774
val rpred_compfuns = RPredCompFuns.compfuns;
bulwahn@32310
   775
bulwahn@32311
   776
fun lift_random random =
bulwahn@32311
   777
  let
bulwahn@32311
   778
    val T = dest_randomT (fastype_of random)
bulwahn@32311
   779
  in
bulwahn@32311
   780
    Const (@{const_name lift_random}, (@{typ Random.seed} -->
bulwahn@32311
   781
      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) --> 
bulwahn@32311
   782
      RPredCompFuns.mk_rpredT T) $ random
bulwahn@32311
   783
  end;
bulwahn@32311
   784
 
bulwahn@31514
   785
(* Mode analysis *)
haftmann@30374
   786
bulwahn@31514
   787
(*** check if a term contains only constructor functions ***)
haftmann@30374
   788
fun is_constrt thy =
haftmann@30374
   789
  let
haftmann@30374
   790
    val cnstrs = flat (maps
haftmann@30374
   791
      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
haftmann@31784
   792
      (Symtab.dest (Datatype.get_all thy)));
haftmann@30374
   793
    fun check t = (case strip_comb t of
haftmann@30374
   794
        (Free _, []) => true
haftmann@30374
   795
      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
haftmann@30374
   796
            (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
haftmann@30374
   797
          | _ => false)
haftmann@30374
   798
      | _ => false)
haftmann@30374
   799
  in check end;
haftmann@30374
   800
bulwahn@31514
   801
(*** check if a type is an equality type (i.e. doesn't contain fun)
bulwahn@31514
   802
  FIXME this is only an approximation ***)
haftmann@30374
   803
fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts
haftmann@30374
   804
  | is_eqT _ = true;
haftmann@30374
   805
haftmann@30374
   806
fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
haftmann@30374
   807
val terms_vs = distinct (op =) o maps term_vs;
haftmann@30374
   808
haftmann@30374
   809
(** collect all Frees in a term (with duplicates!) **)
haftmann@30374
   810
fun term_vTs tm =
haftmann@30374
   811
  fold_aterms (fn Free xT => cons xT | _ => I) tm [];
haftmann@30374
   812
haftmann@30972
   813
(*FIXME this function should not be named merge... make it local instead*)
haftmann@30374
   814
fun merge xs [] = xs
haftmann@30374
   815
  | merge [] ys = ys
haftmann@30374
   816
  | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys)
haftmann@30374
   817
      else y::merge (x::xs) ys;
haftmann@30374
   818
haftmann@30374
   819
fun subsets i j = if i <= j then
haftmann@30374
   820
       let val is = subsets (i+1) j
haftmann@30374
   821
       in merge (map (fn ks => i::ks) is) is end
haftmann@30374
   822
     else [[]];
bulwahn@31514
   823
     
bulwahn@31514
   824
(* FIXME: should be in library - map_prod *)
haftmann@30374
   825
fun cprod ([], ys) = []
haftmann@30374
   826
  | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
haftmann@30374
   827
wenzelm@33004
   828
fun cprods xss = List.foldr (map op :: o cprod) [[]] xss;
haftmann@30374
   829
bulwahn@31514
   830
bulwahn@31515
   831
  
bulwahn@31514
   832
(*TODO: cleanup function and put together with modes_of_term *)
bulwahn@32310
   833
(*
bulwahn@31514
   834
fun modes_of_param default modes t = let
bulwahn@31514
   835
    val (vs, t') = strip_abs t
bulwahn@31514
   836
    val b = length vs
bulwahn@31514
   837
    fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) =>
bulwahn@31514
   838
        let
bulwahn@31514
   839
          val (args1, args2) =
bulwahn@31514
   840
            if length args < length iss then
bulwahn@31514
   841
              error ("Too few arguments for inductive predicate " ^ name)
bulwahn@31514
   842
            else chop (length iss) args;
bulwahn@31514
   843
          val k = length args2;
bulwahn@32308
   844
          val perm = map (fn i => (find_index_eq (Bound (b - i)) args2) + 1)
bulwahn@32308
   845
            (1 upto b)  
bulwahn@31514
   846
          val partial_mode = (1 upto k) \\ perm
bulwahn@31514
   847
        in
bulwahn@31514
   848
          if not (partial_mode subset is) then [] else
bulwahn@31514
   849
          let
bulwahn@31514
   850
            val is' = 
bulwahn@31514
   851
            (fold_index (fn (i, j) => if j mem is then cons (i + 1) else I) perm [])
bulwahn@31514
   852
            |> fold (fn i => if i > k then cons (i - k + b) else I) is
bulwahn@31514
   853
              
bulwahn@31514
   854
           val res = map (fn x => Mode (m, is', x)) (cprods (map
bulwahn@31514
   855
            (fn (NONE, _) => [NONE]
bulwahn@31514
   856
              | (SOME js, arg) => map SOME (filter
bulwahn@31514
   857
                  (fn Mode (_, js', _) => js=js') (modes_of_term modes arg)))
bulwahn@31514
   858
                    (iss ~~ args1)))
bulwahn@31514
   859
          in res end
bulwahn@31514
   860
        end)) (AList.lookup op = modes name)
bulwahn@31514
   861
  in case strip_comb t' of
bulwahn@31514
   862
    (Const (name, _), args) => the_default default (mk_modes name args)
bulwahn@31514
   863
    | (Var ((name, _), _), args) => the (mk_modes name args)
bulwahn@31514
   864
    | (Free (name, _), args) => the (mk_modes name args)
bulwahn@31514
   865
    | _ => default end
bulwahn@31514
   866
  
bulwahn@32310
   867
and
bulwahn@32310
   868
*)
bulwahn@32310
   869
fun modes_of_term modes t =
haftmann@30374
   870
  let
haftmann@30374
   871
    val ks = 1 upto length (binder_types (fastype_of t));
haftmann@30374
   872
    val default = [Mode (([], ks), ks, [])];
haftmann@30374
   873
    fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) =>
haftmann@30374
   874
        let
haftmann@30374
   875
          val (args1, args2) =
haftmann@30374
   876
            if length args < length iss then
haftmann@30374
   877
              error ("Too few arguments for inductive predicate " ^ name)
haftmann@30374
   878
            else chop (length iss) args;
haftmann@30374
   879
          val k = length args2;
haftmann@30374
   880
          val prfx = 1 upto k
haftmann@30374
   881
        in
haftmann@30374
   882
          if not (is_prefix op = prfx is) then [] else
haftmann@30374
   883
          let val is' = map (fn i => i - k) (List.drop (is, k))
haftmann@30374
   884
          in map (fn x => Mode (m, is', x)) (cprods (map
haftmann@30374
   885
            (fn (NONE, _) => [NONE]
haftmann@30374
   886
              | (SOME js, arg) => map SOME (filter
bulwahn@31170
   887
                  (fn Mode (_, js', _) => js=js') (modes_of_term modes arg)))
haftmann@30374
   888
                    (iss ~~ args1)))
haftmann@30374
   889
          end
haftmann@30374
   890
        end)) (AList.lookup op = modes name)
haftmann@30374
   891
bulwahn@32306
   892
  in
bulwahn@32306
   893
    case strip_comb (Envir.eta_contract t) of
haftmann@30374
   894
      (Const (name, _), args) => the_default default (mk_modes name args)
haftmann@30374
   895
    | (Var ((name, _), _), args) => the (mk_modes name args)
haftmann@30374
   896
    | (Free (name, _), args) => the (mk_modes name args)
bulwahn@32306
   897
    | (Abs _, []) => error "Abs at param position" (* modes_of_param default modes t *)
bulwahn@32306
   898
    | _ => default
haftmann@30374
   899
  end
bulwahn@32310
   900
  
haftmann@30374
   901
fun select_mode_prem thy modes vs ps =
haftmann@30374
   902
  find_first (is_some o snd) (ps ~~ map
haftmann@30374
   903
    (fn Prem (us, t) => find_first (fn Mode (_, is, _) =>
haftmann@30374
   904
          let
bulwahn@32312
   905
            val (in_ts, out_ts) = split_smode is us;
haftmann@30374
   906
            val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
haftmann@30374
   907
            val vTs = maps term_vTs out_ts';
haftmann@30374
   908
            val dupTs = map snd (duplicates (op =) vTs) @
wenzelm@32952
   909
              map_filter (AList.lookup (op =) vTs) vs;
haftmann@30374
   910
          in
haftmann@33037
   911
            gen_subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
haftmann@30374
   912
            forall (is_eqT o fastype_of) in_ts' andalso
haftmann@33037
   913
            gen_subset (op =) (term_vs t, vs) andalso
haftmann@30374
   914
            forall is_eqT dupTs
haftmann@30374
   915
          end)
bulwahn@31170
   916
            (modes_of_term modes t handle Option =>
haftmann@30374
   917
               error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
haftmann@30374
   918
      | Negprem (us, t) => find_first (fn Mode (_, is, _) =>
haftmann@30374
   919
            length us = length is andalso
haftmann@33037
   920
            gen_subset (op =) (terms_vs us, vs) andalso
haftmann@33037
   921
            gen_subset (op =) (term_vs t, vs)
bulwahn@31170
   922
            (modes_of_term modes t handle Option =>
haftmann@30374
   923
               error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
haftmann@33037
   924
      | Sidecond t => if gen_subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
haftmann@30374
   925
          else NONE
haftmann@30374
   926
      ) ps);
bulwahn@32310
   927
bulwahn@32310
   928
fun fold_prem f (Prem (args, _)) = fold f args
bulwahn@32310
   929
  | fold_prem f (Negprem (args, _)) = fold f args
bulwahn@32310
   930
  | fold_prem f (Sidecond t) = f t
bulwahn@32310
   931
bulwahn@32310
   932
fun all_subsets [] = [[]]
bulwahn@32310
   933
  | all_subsets (x::xs) = let val xss' = all_subsets xs in xss' @ (map (cons x) xss') end
bulwahn@32310
   934
bulwahn@32310
   935
fun generator vTs v = 
bulwahn@32310
   936
  let
bulwahn@32310
   937
    val T = the (AList.lookup (op =) vTs v)
bulwahn@32310
   938
  in
bulwahn@32310
   939
    (Generator (v, T), Mode (([], []), [], []))
bulwahn@32310
   940
  end;
bulwahn@32310
   941
bulwahn@32310
   942
fun gen_prem (Prem (us, t)) = GeneratorPrem (us, t) 
bulwahn@32310
   943
  | gen_prem _ = error "gen_prem : invalid input for gen_prem"
bulwahn@32316
   944
bulwahn@32316
   945
fun param_gen_prem param_vs (p as Prem (us, t as Free (v, _))) =
bulwahn@32316
   946
  if member (op =) param_vs v then
bulwahn@32316
   947
    GeneratorPrem (us, t)
bulwahn@32316
   948
  else p  
bulwahn@32316
   949
  | param_gen_prem param_vs p = p
bulwahn@32310
   950
  
bulwahn@32310
   951
fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) =
haftmann@30374
   952
  let
wenzelm@32952
   953
    val modes' = modes @ map_filter
haftmann@30374
   954
      (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
bulwahn@32310
   955
        (param_vs ~~ iss);
wenzelm@32952
   956
    val gen_modes' = gen_modes @ map_filter
bulwahn@32316
   957
      (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
bulwahn@32316
   958
        (param_vs ~~ iss);  
bulwahn@32310
   959
    val vTs = distinct (op =) ((fold o fold_prem) Term.add_frees ps (fold Term.add_frees ts []))
bulwahn@32310
   960
    val prem_vs = distinct (op =) ((fold o fold_prem) Term.add_free_names ps [])
bulwahn@32309
   961
    fun check_mode_prems acc_ps vs [] = SOME (acc_ps, vs)
bulwahn@32309
   962
      | check_mode_prems acc_ps vs ps = (case select_mode_prem thy modes' vs ps of
bulwahn@32310
   963
          NONE =>
bulwahn@32310
   964
            (if with_generator then
bulwahn@32316
   965
              (case select_mode_prem thy gen_modes' vs ps of
bulwahn@32310
   966
                  SOME (p, SOME mode) => check_mode_prems ((gen_prem p, mode) :: acc_ps) 
haftmann@33037
   967
                  (case p of Prem (us, _) => gen_union (op =) (vs, terms_vs us) | _ => vs)
bulwahn@32310
   968
                  (filter_out (equal p) ps)
bulwahn@32310
   969
                | NONE =>
bulwahn@32310
   970
                  let 
bulwahn@32310
   971
                    val all_generator_vs = all_subsets (prem_vs \\ vs) |> sort (int_ord o (pairself length))
bulwahn@32310
   972
                  in
bulwahn@32310
   973
                    case (find_first (fn generator_vs => is_some
haftmann@33037
   974
                      (select_mode_prem thy modes' (gen_union (op =) (vs, generator_vs)) ps)) all_generator_vs) of
bulwahn@32310
   975
                      SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps)
haftmann@33037
   976
                        (gen_union (op =) (vs, generator_vs)) ps
bulwahn@32310
   977
                    | NONE => NONE
bulwahn@32310
   978
                  end)
bulwahn@32310
   979
            else
bulwahn@32310
   980
              NONE)
bulwahn@32316
   981
        | SOME (p, SOME mode) => check_mode_prems ((if with_generator then param_gen_prem param_vs p else p, mode) :: acc_ps) 
haftmann@33037
   982
            (case p of Prem (us, _) => gen_union (op =) (vs, terms_vs us) | _ => vs)
bulwahn@32309
   983
            (filter_out (equal p) ps))
bulwahn@32312
   984
    val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
haftmann@30374
   985
    val in_vs = terms_vs in_ts;
haftmann@30374
   986
    val concl_vs = terms_vs ts
bulwahn@32307
   987
  in
bulwahn@32309
   988
    if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
bulwahn@32309
   989
    forall (is_eqT o fastype_of) in_ts' then
haftmann@33037
   990
      case check_mode_prems [] (gen_union (op =) (param_vs, in_vs)) ps of
bulwahn@32309
   991
         NONE => NONE
bulwahn@32310
   992
       | SOME (acc_ps, vs) =>
bulwahn@32310
   993
         if with_generator then
bulwahn@32310
   994
           SOME (ts, (rev acc_ps) @ (map (generator vTs) (concl_vs \\ vs))) 
bulwahn@32310
   995
         else
haftmann@33037
   996
           if gen_subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE
bulwahn@32309
   997
    else NONE
haftmann@30374
   998
  end;
haftmann@30374
   999
bulwahn@32310
  1000
fun check_modes_pred with_generator thy param_vs preds modes gen_modes (p, ms) =
haftmann@30374
  1001
  let val SOME rs = AList.lookup (op =) preds p
haftmann@30374
  1002
  in (p, List.filter (fn m => case find_index
bulwahn@32310
  1003
    (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
haftmann@30374
  1004
      ~1 => true
wenzelm@32950
  1005
    | i => (tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
haftmann@30374
  1006
      p ^ " violates mode " ^ string_of_mode m); false)) ms)
haftmann@30374
  1007
  end;
haftmann@30374
  1008
bulwahn@32310
  1009
fun get_modes_pred with_generator thy param_vs preds modes gen_modes (p, ms) =
bulwahn@32309
  1010
  let
bulwahn@32309
  1011
    val SOME rs = AList.lookup (op =) preds p 
bulwahn@32309
  1012
  in
bulwahn@32311
  1013
    (p, map (fn m =>
bulwahn@32311
  1014
      (m, map (the o check_mode_clause with_generator thy param_vs modes gen_modes m) rs)) ms)
bulwahn@32309
  1015
  end;
bulwahn@32309
  1016
  
haftmann@30972
  1017
fun fixp f (x : (string * mode list) list) =
haftmann@30374
  1018
  let val y = f x
haftmann@30374
  1019
  in if x = y then x else fixp f y end;
haftmann@30374
  1020
bulwahn@32310
  1021
fun modes_of_arities arities =
bulwahn@32310
  1022
  (map (fn (s, (ks, k)) => (s, cprod (cprods (map
bulwahn@32310
  1023
            (fn NONE => [NONE]
bulwahn@32310
  1024
              | SOME k' => map SOME (subsets 1 k')) ks),
bulwahn@32310
  1025
            subsets 1 k))) arities)
bulwahn@32310
  1026
  
bulwahn@32310
  1027
fun infer_modes with_generator thy extra_modes arities param_vs preds =
bulwahn@32309
  1028
  let
bulwahn@32309
  1029
    val modes =
bulwahn@32309
  1030
      fixp (fn modes =>
bulwahn@32310
  1031
        map (check_modes_pred with_generator thy param_vs preds (modes @ extra_modes) []) modes)
bulwahn@32310
  1032
          (modes_of_arities arities)
bulwahn@32309
  1033
  in
bulwahn@32310
  1034
    map (get_modes_pred with_generator thy param_vs preds (modes @ extra_modes) []) modes
bulwahn@32309
  1035
  end;
bulwahn@32310
  1036
bulwahn@32316
  1037
fun remove_from rem [] = []
bulwahn@32316
  1038
  | remove_from rem ((k, vs) :: xs) =
bulwahn@32316
  1039
    (case AList.lookup (op =) rem k of
bulwahn@32316
  1040
      NONE => (k, vs)
bulwahn@32316
  1041
    | SOME vs' => (k, vs \\ vs'))
bulwahn@32316
  1042
    :: remove_from rem xs
bulwahn@32316
  1043
    
bulwahn@32310
  1044
fun infer_modes_with_generator thy extra_modes arities param_vs preds =
bulwahn@32310
  1045
  let
bulwahn@32311
  1046
    val prednames = map fst preds
bulwahn@32316
  1047
    val extra_modes = all_modes_of thy
bulwahn@32311
  1048
    val gen_modes = all_generator_modes_of thy
bulwahn@32311
  1049
      |> filter_out (fn (name, _) => member (op =) prednames name)
bulwahn@32316
  1050
    val starting_modes = remove_from extra_modes (modes_of_arities arities) 
bulwahn@32310
  1051
    val modes =
bulwahn@32310
  1052
      fixp (fn modes =>
bulwahn@32311
  1053
        map (check_modes_pred true thy param_vs preds extra_modes (gen_modes @ modes)) modes)
bulwahn@32316
  1054
         starting_modes 
bulwahn@32310
  1055
  in
bulwahn@32311
  1056
    map (get_modes_pred true thy param_vs preds extra_modes (gen_modes @ modes)) modes
bulwahn@32310
  1057
  end;
bulwahn@32310
  1058
bulwahn@31514
  1059
(* term construction *)
haftmann@30374
  1060
haftmann@30374
  1061
fun mk_v (names, vs) s T = (case AList.lookup (op =) vs s of
bulwahn@31514
  1062
      NONE => (Free (s, T), (names, (s, [])::vs))
haftmann@30374
  1063
    | SOME xs =>
haftmann@30374
  1064
        let
haftmann@30374
  1065
          val s' = Name.variant names s;
haftmann@30374
  1066
          val v = Free (s', T)
haftmann@30374
  1067
        in
bulwahn@31514
  1068
          (v, (s'::names, AList.update (op =) (s, v::xs) vs))
haftmann@30374
  1069
        end);
haftmann@30374
  1070
bulwahn@31514
  1071
fun distinct_v (Free (s, T)) nvs = mk_v nvs s T
bulwahn@31514
  1072
  | distinct_v (t $ u) nvs =
haftmann@30374
  1073
      let
bulwahn@31514
  1074
        val (t', nvs') = distinct_v t nvs;
bulwahn@31514
  1075
        val (u', nvs'') = distinct_v u nvs';
bulwahn@31514
  1076
      in (t' $ u', nvs'') end
bulwahn@31514
  1077
  | distinct_v x nvs = (x, nvs);
haftmann@30374
  1078
bulwahn@32308
  1079
fun compile_match thy compfuns eqs eqs' out_ts success_t =
bulwahn@32310
  1080
  let
haftmann@30374
  1081
    val eqs'' = maps mk_eq eqs @ eqs'
haftmann@30374
  1082
    val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
haftmann@30374
  1083
    val name = Name.variant names "x";
haftmann@30374
  1084
    val name' = Name.variant (name :: names) "y";
haftmann@30374
  1085
    val T = mk_tupleT (map fastype_of out_ts);
haftmann@30374
  1086
    val U = fastype_of success_t;
bulwahn@32308
  1087
    val U' = dest_predT compfuns U;
haftmann@30374
  1088
    val v = Free (name, T);
haftmann@30374
  1089
    val v' = Free (name', T);
haftmann@30374
  1090
  in
haftmann@31723
  1091
    lambda v (fst (Datatype.make_case
haftmann@30374
  1092
      (ProofContext.init thy) false [] v
haftmann@30374
  1093
      [(mk_tuple out_ts,
haftmann@30374
  1094
        if null eqs'' then success_t
haftmann@30374
  1095
        else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
haftmann@30374
  1096
          foldr1 HOLogic.mk_conj eqs'' $ success_t $
bulwahn@32308
  1097
            mk_bot compfuns U'),
bulwahn@32308
  1098
       (v', mk_bot compfuns U')]))
haftmann@30374
  1099
  end;
haftmann@30374
  1100
haftmann@30972
  1101
(*FIXME function can be removed*)
haftmann@30374
  1102
fun mk_funcomp f t =
haftmann@30374
  1103
  let
haftmann@30374
  1104
    val names = Term.add_free_names t [];
haftmann@30374
  1105
    val Ts = binder_types (fastype_of t);
haftmann@30374
  1106
    val vs = map Free
haftmann@30374
  1107
      (Name.variant_list names (replicate (length Ts) "x") ~~ Ts)
haftmann@30374
  1108
  in
haftmann@30374
  1109
    fold_rev lambda vs (f (list_comb (t, vs)))
haftmann@30374
  1110
  end;
bulwahn@32308
  1111
(*
bulwahn@32308
  1112
fun compile_param_ext thy compfuns modes (NONE, t) = t
bulwahn@32308
  1113
  | compile_param_ext thy compfuns modes (m as SOME (Mode ((iss, is'), is, ms)), t) =
bulwahn@31514
  1114
      let
bulwahn@31514
  1115
        val (vs, u) = strip_abs t
bulwahn@32308
  1116
        val (ivs, ovs) = split_mode is vs    
bulwahn@31514
  1117
        val (f, args) = strip_comb u
bulwahn@31514
  1118
        val (params, args') = chop (length ms) args
bulwahn@32308
  1119
        val (inargs, outargs) = split_mode is' args'
bulwahn@31514
  1120
        val b = length vs
bulwahn@32308
  1121
        val perm = map (fn i => (find_index_eq (Bound (b - i)) args') + 1) (1 upto b)
bulwahn@31514
  1122
        val outp_perm =
bulwahn@32308
  1123
          snd (split_mode is perm)
bulwahn@31514
  1124
          |> map (fn i => i - length (filter (fn x => x < i) is'))
bulwahn@32308
  1125
        val names = [] -- TODO
bulwahn@31514
  1126
        val out_names = Name.variant_list names (replicate (length outargs) "x")
bulwahn@31514
  1127
        val f' = case f of
bulwahn@31514
  1128
            Const (name, T) =>
bulwahn@31514
  1129
              if AList.defined op = modes name then
bulwahn@32308
  1130
                mk_predfun_of thy compfuns (name, T) (iss, is')
bulwahn@31514
  1131
              else error "compile param: Not an inductive predicate with correct mode"
bulwahn@32308
  1132
          | Free (name, T) => Free (name, param_funT_of compfuns T (SOME is'))
bulwahn@32308
  1133
        val outTs = dest_tupleT (dest_predT compfuns (body_type (fastype_of f')))
bulwahn@31514
  1134
        val out_vs = map Free (out_names ~~ outTs)
bulwahn@31514
  1135
        val params' = map (compile_param thy modes) (ms ~~ params)
bulwahn@31514
  1136
        val f_app = list_comb (f', params' @ inargs)
bulwahn@32308
  1137
        val single_t = (mk_single compfuns (mk_tuple (map (fn i => nth out_vs (i - 1)) outp_perm)))
bulwahn@32308
  1138
        val match_t = compile_match thy compfuns [] [] out_vs single_t
bulwahn@31514
  1139
      in list_abs (ivs,
bulwahn@32308
  1140
        mk_bind compfuns (f_app, match_t))
bulwahn@31514
  1141
      end
bulwahn@32308
  1142
  | compile_param_ext _ _ _ _ = error "compile params"
bulwahn@32308
  1143
*)
bulwahn@31514
  1144
bulwahn@32315
  1145
fun compile_param size thy compfuns (NONE, t) = t
bulwahn@32315
  1146
  | compile_param size thy compfuns (m as SOME (Mode ((iss, is'), is, ms)), t) =
bulwahn@32313
  1147
   let
bulwahn@31877
  1148
     val (f, args) = strip_comb (Envir.eta_contract t)
bulwahn@31514
  1149
     val (params, args') = chop (length ms) args
bulwahn@32315
  1150
     val params' = map (compile_param size thy compfuns) (ms ~~ params)
bulwahn@32315
  1151
     val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of
bulwahn@32315
  1152
     val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of
bulwahn@32310
  1153
     val f' =
bulwahn@32310
  1154
       case f of
bulwahn@32310
  1155
         Const (name, T) =>
bulwahn@32310
  1156
           mk_fun_of compfuns thy (name, T) (iss, is')
bulwahn@32313
  1157
       | Free (name, T) => Free (name, funT_of compfuns (iss, is') T)
bulwahn@32315
  1158
       | _ => error ("PredicateCompiler: illegal parameter term")
bulwahn@31877
  1159
   in list_comb (f', params' @ args') end
bulwahn@32310
  1160
   
bulwahn@32311
  1161
fun compile_expr size thy ((Mode (mode, is, ms)), t) =
bulwahn@32310
  1162
  case strip_comb t of
bulwahn@32310
  1163
    (Const (name, T), params) =>
bulwahn@32310
  1164
       let
bulwahn@32315
  1165
         val params' = map (compile_param size thy PredicateCompFuns.compfuns) (ms ~~ params)
bulwahn@32315
  1166
         val mk_fun_of = case size of NONE => mk_fun_of | SOME _ => mk_sizelim_fun_of
bulwahn@32310
  1167
       in
bulwahn@32315
  1168
         list_comb (mk_fun_of PredicateCompFuns.compfuns thy (name, T) mode, params')
bulwahn@32310
  1169
       end
bulwahn@32310
  1170
  | (Free (name, T), args) =>
bulwahn@32315
  1171
       let 
bulwahn@32315
  1172
         val funT_of = case size of NONE => funT_of | SOME _ => sizelim_funT_of 
bulwahn@32315
  1173
       in
bulwahn@32315
  1174
         list_comb (Free (name, funT_of PredicateCompFuns.compfuns ([], is) T), args)
bulwahn@32315
  1175
       end;
bulwahn@32315
  1176
       
bulwahn@32315
  1177
fun compile_gen_expr size thy compfuns ((Mode (mode, is, ms)), t) =
bulwahn@32310
  1178
  case strip_comb t of
bulwahn@32310
  1179
    (Const (name, T), params) =>
bulwahn@32316
  1180
      let
bulwahn@32316
  1181
        val params' = map (compile_param size thy compfuns) (ms ~~ params)
bulwahn@32316
  1182
      in
bulwahn@32316
  1183
        list_comb (mk_generator_of compfuns thy (name, T) mode, params')
bulwahn@32316
  1184
      end
bulwahn@32316
  1185
    | (Free (name, T), args) =>
bulwahn@32316
  1186
      list_comb (Free (name, sizelim_funT_of RPredCompFuns.compfuns ([], is) T), args)
bulwahn@32316
  1187
          
bulwahn@32310
  1188
(** specific rpred functions -- move them to the correct place in this file *)
haftmann@30374
  1189
bulwahn@32310
  1190
(* uncommented termify code; causes more trouble than expected at first *) 
bulwahn@32310
  1191
(*
bulwahn@32310
  1192
fun mk_valtermify_term (t as Const (c, T)) = HOLogic.mk_prod (t, Abs ("u", HOLogic.unitT, HOLogic.reflect_term t))
bulwahn@32310
  1193
  | mk_valtermify_term (Free (x, T)) = Free (x, termifyT T) 
bulwahn@32310
  1194
  | mk_valtermify_term (t1 $ t2) =
bulwahn@32310
  1195
    let
bulwahn@32310
  1196
      val T = fastype_of t1
bulwahn@32310
  1197
      val (T1, T2) = dest_funT T
bulwahn@32310
  1198
      val t1' = mk_valtermify_term t1
bulwahn@32310
  1199
      val t2' = mk_valtermify_term t2
bulwahn@32310
  1200
    in
haftmann@32657
  1201
      Const ("Code_Evaluation.valapp", termifyT T --> termifyT T1 --> termifyT T2) $ t1' $ t2'
bulwahn@32310
  1202
    end
bulwahn@32310
  1203
  | mk_valtermify_term _ = error "Not a valid term for mk_valtermify_term"
bulwahn@32310
  1204
*)
haftmann@30374
  1205
bulwahn@32311
  1206
fun compile_clause compfuns size final_term thy all_vs param_vs (iss, is) inp (ts, moded_ps) =
haftmann@30374
  1207
  let
bulwahn@31514
  1208
    fun check_constrt t (names, eqs) =
bulwahn@31514
  1209
      if is_constrt thy t then (t, (names, eqs)) else
haftmann@30374
  1210
        let
haftmann@30374
  1211
          val s = Name.variant names "x";
haftmann@30374
  1212
          val v = Free (s, fastype_of t)
bulwahn@31514
  1213
        in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
haftmann@30374
  1214
bulwahn@32312
  1215
    val (in_ts, out_ts) = split_smode is ts;
bulwahn@31514
  1216
    val (in_ts', (all_vs', eqs)) =
bulwahn@31514
  1217
      fold_map check_constrt in_ts (all_vs, []);
haftmann@30374
  1218
haftmann@30374
  1219
    fun compile_prems out_ts' vs names [] =
haftmann@30374
  1220
          let
bulwahn@31514
  1221
            val (out_ts'', (names', eqs')) =
bulwahn@31514
  1222
              fold_map check_constrt out_ts' (names, []);
bulwahn@31514
  1223
            val (out_ts''', (names'', constr_vs)) = fold_map distinct_v
bulwahn@31514
  1224
              out_ts'' (names', map (rpair []) vs);
haftmann@30374
  1225
          in
bulwahn@32310
  1226
          (* termify code:
bulwahn@32310
  1227
            compile_match thy compfuns constr_vs (eqs @ eqs') out_ts'''
bulwahn@32310
  1228
              (mk_single compfuns (mk_tuple (map mk_valtermify_term out_ts)))
bulwahn@32310
  1229
           *)
bulwahn@32308
  1230
            compile_match thy compfuns constr_vs (eqs @ eqs') out_ts'''
bulwahn@32311
  1231
              (final_term out_ts)
haftmann@30374
  1232
          end
bulwahn@32309
  1233
      | compile_prems out_ts vs names ((p, mode as Mode ((_, is), _, _)) :: ps) =
haftmann@30374
  1234
          let
haftmann@30374
  1235
            val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
bulwahn@31514
  1236
            val (out_ts', (names', eqs)) =
bulwahn@31514
  1237
              fold_map check_constrt out_ts (names, [])
bulwahn@31514
  1238
            val (out_ts'', (names'', constr_vs')) = fold_map distinct_v
bulwahn@31514
  1239
              out_ts' ((names', map (rpair []) vs))
haftmann@30374
  1240
            val (compiled_clause, rest) = case p of
haftmann@30374
  1241
               Prem (us, t) =>
haftmann@30374
  1242
                 let
bulwahn@32312
  1243
                   val (in_ts, out_ts''') = split_smode is us;
bulwahn@32311
  1244
                   val args = case size of
bulwahn@32311
  1245
                     NONE => in_ts
bulwahn@32311
  1246
                   | SOME size_t => in_ts @ [size_t]
bulwahn@32310
  1247
                   val u = lift_pred compfuns
bulwahn@32311
  1248
                     (list_comb (compile_expr size thy (mode, t), args))                     
bulwahn@32309
  1249
                   val rest = compile_prems out_ts''' vs' names'' ps
haftmann@30374
  1250
                 in
haftmann@30374
  1251
                   (u, rest)
haftmann@30374
  1252
                 end
haftmann@30374
  1253
             | Negprem (us, t) =>
haftmann@30374
  1254
                 let
bulwahn@32312
  1255
                   val (in_ts, out_ts''') = split_smode is us
bulwahn@32310
  1256
                   val u = lift_pred compfuns
bulwahn@32311
  1257
                     (mk_not PredicateCompFuns.compfuns (list_comb (compile_expr NONE thy (mode, t), in_ts)))
bulwahn@32309
  1258
                   val rest = compile_prems out_ts''' vs' names'' ps
haftmann@30374
  1259
                 in
bulwahn@32311
  1260
                   (u, rest)
haftmann@30374
  1261
                 end
haftmann@30374
  1262
             | Sidecond t =>
haftmann@30374
  1263
                 let
bulwahn@32309
  1264
                   val rest = compile_prems [] vs' names'' ps;
haftmann@30374
  1265
                 in
bulwahn@32308
  1266
                   (mk_if compfuns t, rest)
haftmann@30374
  1267
                 end
bulwahn@32310
  1268
             | GeneratorPrem (us, t) =>
bulwahn@32310
  1269
                 let
bulwahn@32312
  1270
                   val (in_ts, out_ts''') = split_smode is us;
bulwahn@32311
  1271
                   val args = case size of
bulwahn@32311
  1272
                     NONE => in_ts
bulwahn@32311
  1273
                   | SOME size_t => in_ts @ [size_t]
bulwahn@32315
  1274
                   val u = list_comb (compile_gen_expr size thy compfuns (mode, t), args)
bulwahn@32310
  1275
                   val rest = compile_prems out_ts''' vs' names'' ps
bulwahn@32310
  1276
                 in
bulwahn@32310
  1277
                   (u, rest)
bulwahn@32310
  1278
                 end
bulwahn@32310
  1279
             | Generator (v, T) =>
bulwahn@32310
  1280
                 let
bulwahn@32310
  1281
                   val u = lift_random (HOLogic.mk_random T @{term "1::code_numeral"})
bulwahn@32310
  1282
                   val rest = compile_prems [Free (v, T)]  vs' names'' ps;
bulwahn@32310
  1283
                 in
bulwahn@32310
  1284
                   (u, rest)
bulwahn@32310
  1285
                 end
haftmann@30374
  1286
          in
bulwahn@32308
  1287
            compile_match thy compfuns constr_vs' eqs out_ts'' 
bulwahn@32308
  1288
              (mk_bind compfuns (compiled_clause, rest))
haftmann@30374
  1289
          end
bulwahn@32309
  1290
    val prem_t = compile_prems in_ts' param_vs all_vs' moded_ps;
haftmann@30374
  1291
  in
bulwahn@32308
  1292
    mk_bind compfuns (mk_single compfuns inp, prem_t)
haftmann@30374
  1293
  end
haftmann@30374
  1294
bulwahn@32311
  1295
fun compile_pred compfuns mk_fun_of use_size thy all_vs param_vs s T mode moded_cls =
haftmann@30374
  1296
  let
bulwahn@32312
  1297
    val (Ts1, (Us1, Us2)) = split_mode mode (binder_types T)
bulwahn@32315
  1298
    val funT_of = if use_size then sizelim_funT_of else funT_of 
bulwahn@32313
  1299
    val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) (fst mode) Ts1
bulwahn@32311
  1300
    val xnames = Name.variant_list (all_vs @ param_vs)
haftmann@30374
  1301
      (map (fn i => "x" ^ string_of_int i) (snd mode));
bulwahn@32311
  1302
    val size_name = Name.variant (all_vs @ param_vs @ xnames) "size"
bulwahn@32310
  1303
    (* termify code: val xs = map2 (fn s => fn T => Free (s, termifyT T)) xnames Us1; *)
haftmann@30374
  1304
    val xs = map2 (fn s => fn T => Free (s, T)) xnames Us1;
bulwahn@32311
  1305
    val params = map2 (fn s => fn T => Free (s, T)) param_vs Ts1'
bulwahn@32311
  1306
    val size = Free (size_name, @{typ "code_numeral"})
bulwahn@32311
  1307
    val decr_size =
bulwahn@32311
  1308
      if use_size then
bulwahn@32311
  1309
        SOME (Const ("HOL.minus_class.minus", @{typ "code_numeral => code_numeral => code_numeral"})
bulwahn@32311
  1310
          $ size $ Const ("HOL.one_class.one", @{typ "Code_Numeral.code_numeral"}))
bulwahn@32311
  1311
      else
bulwahn@32311
  1312
        NONE
haftmann@30374
  1313
    val cl_ts =
bulwahn@32311
  1314
      map (compile_clause compfuns decr_size (fn out_ts => mk_single compfuns (mk_tuple out_ts))
bulwahn@32311
  1315
        thy all_vs param_vs mode (mk_tuple xs)) moded_cls;
bulwahn@32311
  1316
    val t = foldr1 (mk_sup compfuns) cl_ts
bulwahn@32311
  1317
    val T' = mk_predT compfuns (mk_tupleT Us2)
bulwahn@32311
  1318
    val size_t = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
bulwahn@32311
  1319
      $ HOLogic.mk_eq (size, @{term "0 :: code_numeral"})
bulwahn@32311
  1320
      $ mk_bot compfuns (dest_predT compfuns T') $ t
bulwahn@32311
  1321
    val fun_const = mk_fun_of compfuns thy (s, T) mode
bulwahn@32311
  1322
    val eq = if use_size then
bulwahn@32311
  1323
      (list_comb (fun_const, params @ xs @ [size]), size_t)
bulwahn@32311
  1324
    else
bulwahn@32311
  1325
      (list_comb (fun_const, params @ xs), t)
haftmann@30374
  1326
  in
bulwahn@32311
  1327
    HOLogic.mk_Trueprop (HOLogic.mk_eq eq)
haftmann@30374
  1328
  end;
bulwahn@32311
  1329
  
haftmann@30374
  1330
(* special setup for simpset *)                  
haftmann@30374
  1331
val HOL_basic_ss' = HOL_basic_ss setSolver 
haftmann@30374
  1332
  (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
haftmann@30374
  1333
bulwahn@31514
  1334
(* Definition of executable functions and their intro and elim rules *)
haftmann@30374
  1335
haftmann@30972
  1336
fun print_arities arities = tracing ("Arities:\n" ^
haftmann@30374
  1337
  cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^
haftmann@30374
  1338
    space_implode " -> " (map
haftmann@30374
  1339
      (fn NONE => "X" | SOME k' => string_of_int k')
haftmann@30374
  1340
        (ks @ [SOME k]))) arities));
haftmann@30374
  1341
haftmann@30374
  1342
fun mk_Eval_of ((x, T), NONE) names = (x, names)
haftmann@30374
  1343
  | mk_Eval_of ((x, T), SOME mode) names = let
haftmann@30374
  1344
  val Ts = binder_types T
haftmann@30374
  1345
  val argnames = Name.variant_list names
haftmann@30374
  1346
        (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
haftmann@30374
  1347
  val args = map Free (argnames ~~ Ts)
bulwahn@32312
  1348
  val (inargs, outargs) = split_smode mode args
bulwahn@32308
  1349
  val r = PredicateCompFuns.mk_Eval (list_comb (x, inargs), mk_tuple outargs)
haftmann@30374
  1350
  val t = fold_rev lambda args r 
haftmann@30374
  1351
in
haftmann@30374
  1352
  (t, argnames @ names)
haftmann@30374
  1353
end;
haftmann@30374
  1354
bulwahn@32312
  1355
fun create_intro_elim_rule (mode as (iss, is)) defthm mode_id funT pred thy =
haftmann@30374
  1356
let
haftmann@30374
  1357
  val Ts = binder_types (fastype_of pred)
haftmann@30374
  1358
  val funtrm = Const (mode_id, funT)
haftmann@30374
  1359
  val argnames = Name.variant_list []
haftmann@30374
  1360
        (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
bulwahn@32312
  1361
  val (Ts1, Ts2) = chop (length iss) Ts;
bulwahn@32313
  1362
  val Ts1' = map2 (fn NONE => I | SOME is => funT_of (PredicateCompFuns.compfuns) ([], is)) iss Ts1
haftmann@30374
  1363
  val args = map Free (argnames ~~ (Ts1' @ Ts2))
bulwahn@32313
  1364
  val (params, ioargs) = chop (length iss) args
bulwahn@32313
  1365
  val (inargs, outargs) = split_smode is ioargs
bulwahn@31550
  1366
  val param_names = Name.variant_list argnames
bulwahn@32312
  1367
    (map (fn i => "p" ^ string_of_int i) (1 upto (length iss)))
bulwahn@31550
  1368
  val param_vs = map Free (param_names ~~ Ts1)
bulwahn@32312
  1369
  val (params', names) = fold_map mk_Eval_of ((params ~~ Ts1) ~~ iss) []
bulwahn@32313
  1370
  val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ ioargs))
bulwahn@32313
  1371
  val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ ioargs))
bulwahn@31550
  1372
  val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params')
haftmann@30374
  1373
  val funargs = params @ inargs
bulwahn@32308
  1374
  val funpropE = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs),
haftmann@30374
  1375
                  if null outargs then Free("y", HOLogic.unitT) else mk_tuple outargs))
bulwahn@32308
  1376
  val funpropI = HOLogic.mk_Trueprop (PredicateCompFuns.mk_Eval (list_comb (funtrm, funargs),
haftmann@30374
  1377
                   mk_tuple outargs))
bulwahn@31550
  1378
  val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
haftmann@30374
  1379
  val simprules = [defthm, @{thm eval_pred},
haftmann@30374
  1380
                   @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}]
bulwahn@32312
  1381
  val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
bulwahn@31550
  1382
  val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ ["y"]) [] introtrm (fn {...} => unfolddef_tac)
haftmann@30374
  1383
  val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
bulwahn@31550
  1384
  val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
bulwahn@31550
  1385
  val elimthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac)
bulwahn@31514
  1386
in 
bulwahn@31514
  1387
  (introthm, elimthm)
haftmann@30374
  1388
end;
haftmann@30374
  1389
bulwahn@32310
  1390
fun create_constname_of_mode thy prefix name mode = 
bulwahn@32308
  1391
  let
bulwahn@32308
  1392
    fun string_of_mode mode = if null mode then "0"
bulwahn@32308
  1393
      else space_implode "_" (map string_of_int mode)
bulwahn@32313
  1394
    val HOmode = space_implode "_and_"
bulwahn@32313
  1395
      (fold (fn NONE => I | SOME mode => cons (string_of_mode mode)) (fst mode) [])
bulwahn@32308
  1396
  in
bulwahn@32310
  1397
    (Sign.full_bname thy (prefix ^ (Long_Name.base_name name))) ^
bulwahn@32312
  1398
      (if HOmode = "" then "_" else "_for_" ^ HOmode ^ "_yields_") ^ (string_of_mode (snd mode))
bulwahn@32308
  1399
  end;
bulwahn@32308
  1400
  
bulwahn@32312
  1401
fun create_definitions preds (name, modes) thy =
haftmann@30374
  1402
  let
bulwahn@32308
  1403
    val compfuns = PredicateCompFuns.compfuns
haftmann@30374
  1404
    val T = AList.lookup (op =) preds name |> the
bulwahn@32312
  1405
    fun create_definition (mode as (iss, is)) thy = let
bulwahn@32310
  1406
      val mode_cname = create_constname_of_mode thy "" name mode
bulwahn@32308
  1407
      val mode_cbasename = Long_Name.base_name mode_cname
bulwahn@32313
  1408
      val Ts = binder_types T
bulwahn@32313
  1409
      val (Ts1, Ts2) = chop (length iss) Ts
bulwahn@32313
  1410
      val (Us1, Us2) =  split_smode is Ts2
bulwahn@32313
  1411
      val Ts1' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss Ts1
bulwahn@32308
  1412
      val funT = (Ts1' @ Us1) ---> (mk_predT compfuns (mk_tupleT Us2))
haftmann@30374
  1413
      val names = Name.variant_list []
haftmann@30374
  1414
        (map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
bulwahn@32313
  1415
      val xs = map Free (names ~~ (Ts1' @ Ts2));                   
bulwahn@32313
  1416
      val (xparams, xargs) = chop (length iss) xs;
bulwahn@32313
  1417
      val (xins, xouts) = split_smode is xargs 
bulwahn@32312
  1418
      val (xparams', names') = fold_map mk_Eval_of ((xparams ~~ Ts1) ~~ iss) names
haftmann@30374
  1419
      fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
bulwahn@32312
  1420
        | mk_split_lambda [x] t = lambda x t
bulwahn@32312
  1421
        | mk_split_lambda xs t =
bulwahn@32312
  1422
        let
bulwahn@32312
  1423
          fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
bulwahn@32312
  1424
            | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
bulwahn@32312
  1425
        in
bulwahn@32312
  1426
          mk_split_lambda' xs t
bulwahn@32312
  1427
        end;
bulwahn@32312
  1428
      val predterm = PredicateCompFuns.mk_Enum (mk_split_lambda xouts
bulwahn@32313
  1429
        (list_comb (Const (name, T), xparams' @ xargs)))
bulwahn@32308
  1430
      val lhs = list_comb (Const (mode_cname, funT), xparams @ xins)
haftmann@30374
  1431
      val def = Logic.mk_equals (lhs, predterm)
bulwahn@31514
  1432
      val ([definition], thy') = thy |>
bulwahn@32308
  1433
        Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
bulwahn@32308
  1434
        PureThy.add_defs false [((Binding.name (mode_cbasename ^ "_def"), def), [])]
bulwahn@32312
  1435
      val (intro, elim) =
bulwahn@32312
  1436
        create_intro_elim_rule mode definition mode_cname funT (Const (name, T)) thy'
bulwahn@32308
  1437
      in thy' |> add_predfun name mode (mode_cname, definition, intro, elim)
bulwahn@32308
  1438
        |> PureThy.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
bulwahn@32308
  1439
        |> PureThy.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
wenzelm@31554
  1440
        |> Theory.checkpoint
haftmann@30374
  1441
      end;
haftmann@30374
  1442
  in
haftmann@30374
  1443
    fold create_definition modes thy
haftmann@30374
  1444
  end;
bulwahn@32311
  1445
bulwahn@32312
  1446
fun sizelim_create_definitions preds (name, modes) thy =
bulwahn@32311
  1447
  let
bulwahn@32311
  1448
    val T = AList.lookup (op =) preds name |> the
bulwahn@32311
  1449
    fun create_definition mode thy =
bulwahn@32311
  1450
      let
bulwahn@32311
  1451
        val mode_cname = create_constname_of_mode thy "sizelim_" name mode
bulwahn@32315
  1452
        val funT = sizelim_funT_of PredicateCompFuns.compfuns mode T
bulwahn@32311
  1453
      in
bulwahn@32311
  1454
        thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
bulwahn@32311
  1455
        |> set_sizelim_function_name name mode mode_cname 
bulwahn@32311
  1456
      end;
bulwahn@32311
  1457
  in
bulwahn@32311
  1458
    fold create_definition modes thy
bulwahn@32311
  1459
  end;
bulwahn@32312
  1460
    
bulwahn@32312
  1461
fun rpred_create_definitions preds (name, modes) thy =
bulwahn@32308
  1462
  let
bulwahn@32308
  1463
    val T = AList.lookup (op =) preds name |> the
bulwahn@32308
  1464
    fun create_definition mode thy =
bulwahn@32308
  1465
      let
bulwahn@32310
  1466
        val mode_cname = create_constname_of_mode thy "gen_" name mode
bulwahn@32316
  1467
        val funT = sizelim_funT_of RPredCompFuns.compfuns mode T
bulwahn@32308
  1468
      in
bulwahn@32308
  1469
        thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
bulwahn@32310
  1470
        |> set_generator_name name mode mode_cname 
bulwahn@32308
  1471
      end;
bulwahn@32308
  1472
  in
bulwahn@32308
  1473
    fold create_definition modes thy
bulwahn@32308
  1474
  end;
bulwahn@32308
  1475
  
haftmann@30374
  1476
(* Proving equivalence of term *)
haftmann@30374
  1477
haftmann@30374
  1478
fun is_Type (Type _) = true
haftmann@30374
  1479
  | is_Type _ = false
haftmann@30374
  1480
haftmann@30374
  1481
(* returns true if t is an application of an datatype constructor *)
haftmann@30374
  1482
(* which then consequently would be splitted *)
haftmann@30374
  1483
(* else false *)
haftmann@30374
  1484
fun is_constructor thy t =
haftmann@30374
  1485
  if (is_Type (fastype_of t)) then
haftmann@31784
  1486
    (case Datatype.get_info thy ((fst o dest_Type o fastype_of) t) of
haftmann@30374
  1487
      NONE => false
haftmann@30374
  1488
    | SOME info => (let
haftmann@30374
  1489
      val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
haftmann@30374
  1490
      val (c, _) = strip_comb t
haftmann@30374
  1491
      in (case c of
haftmann@30374
  1492
        Const (name, _) => name mem_string constr_consts
haftmann@30374
  1493
        | _ => false) end))
haftmann@30374
  1494
  else false
haftmann@30374
  1495
haftmann@30374
  1496
(* MAJOR FIXME:  prove_params should be simple
haftmann@30374
  1497
 - different form of introrule for parameters ? *)
bulwahn@32313
  1498
fun prove_param thy (NONE, t) = TRY (rtac @{thm refl} 1)
bulwahn@32313
  1499
  | prove_param thy (m as SOME (Mode (mode, is, ms)), t) =
bulwahn@32313
  1500
  let
bulwahn@32315
  1501
    val  (f, args) = strip_comb (Envir.eta_contract t)
haftmann@30374
  1502
    val (params, _) = chop (length ms) args
haftmann@30374
  1503
    val f_tac = case f of
bulwahn@32313
  1504
      Const (name, T) => simp_tac (HOL_basic_ss addsimps 
bulwahn@32313
  1505
         (@{thm eval_pred}::(predfun_definition_of thy name mode)::
bulwahn@32313
  1506
         @{thm "Product_Type.split_conv"}::[])) 1
bulwahn@32313
  1507
    | Free _ => TRY (rtac @{thm refl} 1)
bulwahn@32313
  1508
    | Abs _ => error "prove_param: No valid parameter term"
bulwahn@32313
  1509
  in
bulwahn@32313
  1510
    REPEAT_DETERM (etac @{thm thin_rl} 1)
bulwahn@32313
  1511
    THEN REPEAT_DETERM (rtac @{thm ext} 1)
bulwahn@32313
  1512
    THEN print_tac "prove_param"
haftmann@30374
  1513
    THEN f_tac
haftmann@30374
  1514
    THEN print_tac "after simplification in prove_args"
bulwahn@32313
  1515
    THEN (EVERY (map (prove_param thy) (ms ~~ params)))
haftmann@30374
  1516
    THEN (REPEAT_DETERM (atac 1))
haftmann@30374
  1517
  end
bulwahn@32313
  1518
bulwahn@32309
  1519
fun prove_expr thy (Mode (mode, is, ms), t, us) (premposition : int) =
bulwahn@32309
  1520
  case strip_comb t of
bulwahn@32309
  1521
    (Const (name, T), args) =>  
bulwahn@32309
  1522
      let
bulwahn@32309
  1523
        val introrule = predfun_intro_of thy name mode
bulwahn@32309
  1524
        val (args1, args2) = chop (length ms) args
bulwahn@32309
  1525
      in
haftmann@30374
  1526
        rtac @{thm bindI} 1
haftmann@30374
  1527
        THEN print_tac "before intro rule:"
haftmann@30374
  1528
        (* for the right assumption in first position *)
haftmann@30374
  1529
        THEN rotate_tac premposition 1
bulwahn@32313
  1530
        THEN debug_tac (Display.string_of_thm (ProofContext.init thy) introrule)
haftmann@30374
  1531
        THEN rtac introrule 1
bulwahn@32306
  1532
        THEN print_tac "after intro rule"
haftmann@30374
  1533
        (* work with parameter arguments *)
bulwahn@31550
  1534
        THEN (atac 1)
bulwahn@32306
  1535
        THEN (print_tac "parameter goal")
bulwahn@32309
  1536
        THEN (EVERY (map (prove_param thy) (ms ~~ args1)))
bulwahn@32309
  1537
        THEN (REPEAT_DETERM (atac 1))
bulwahn@32309
  1538
      end
bulwahn@32309
  1539
  | _ => rtac @{thm bindI} 1 THEN atac 1
haftmann@30374
  1540
haftmann@30374
  1541
fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st; 
haftmann@30374
  1542
haftmann@30374
  1543
fun SOLVEDALL tac st = FILTER (fn st' => nprems_of st' = 0) tac st
haftmann@30374
  1544
haftmann@30374
  1545
fun prove_match thy (out_ts : term list) = let
haftmann@30374
  1546
  fun get_case_rewrite t =
haftmann@30374
  1547
    if (is_constructor thy t) then let
haftmann@31784
  1548
      val case_rewrites = (#case_rewrites (Datatype.the_info thy
haftmann@30374
  1549
        ((fst o dest_Type o fastype_of) t)))
wenzelm@32952
  1550
      in case_rewrites @ maps get_case_rewrite (snd (strip_comb t)) end
haftmann@30374
  1551
    else []
wenzelm@32952
  1552
  val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: maps get_case_rewrite out_ts
haftmann@30374
  1553
(* replace TRY by determining if it necessary - are there equations when calling compile match? *)
haftmann@30374
  1554
in
haftmann@30374
  1555
   (* make this simpset better! *)
bulwahn@31515
  1556
  asm_simp_tac (HOL_basic_ss' addsimps simprules) 1
haftmann@30374
  1557
  THEN print_tac "after prove_match:"
haftmann@30374
  1558
  THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm "HOL.if_P"}] 1
haftmann@30374
  1559
         THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss 1))))
haftmann@30374
  1560
         THEN (SOLVED (asm_simp_tac HOL_basic_ss 1)))))
haftmann@30374
  1561
  THEN print_tac "after if simplification"
haftmann@30374
  1562
end;
haftmann@30374
  1563
haftmann@30374
  1564
(* corresponds to compile_fun -- maybe call that also compile_sidecond? *)
haftmann@30374
  1565
bulwahn@31515
  1566
fun prove_sidecond thy modes t =
bulwahn@31515
  1567
  let
bulwahn@31515
  1568
    fun preds_of t nameTs = case strip_comb t of 
bulwahn@31515
  1569
      (f as Const (name, T), args) =>
bulwahn@31515
  1570
        if AList.defined (op =) modes name then (name, T) :: nameTs
bulwahn@31515
  1571
          else fold preds_of args nameTs
bulwahn@31515
  1572
      | _ => nameTs
bulwahn@31515
  1573
    val preds = preds_of t []
bulwahn@31515
  1574
    val defs = map
bulwahn@31515
  1575
      (fn (pred, T) => predfun_definition_of thy pred ([], (1 upto (length (binder_types T)))))
bulwahn@31515
  1576
        preds
bulwahn@31515
  1577
  in 
bulwahn@31515
  1578
    (* remove not_False_eq_True when simpset in prove_match is better *)
bulwahn@31515
  1579
    simp_tac (HOL_basic_ss addsimps @{thm not_False_eq_True} :: @{thm eval_pred} :: defs) 1 
bulwahn@31515
  1580
    (* need better control here! *)
bulwahn@31515
  1581
  end
haftmann@30374
  1582
bulwahn@32309
  1583
fun prove_clause thy nargs modes (iss, is) (_, clauses) (ts, moded_ps) =
bulwahn@32309
  1584
  let
bulwahn@32312
  1585
    val (in_ts, clause_out_ts) = split_smode is ts;
bulwahn@32309
  1586
    fun prove_prems out_ts [] =
bulwahn@32309
  1587
      (prove_match thy out_ts)
bulwahn@32309
  1588
      THEN asm_simp_tac HOL_basic_ss' 1
bulwahn@32309
  1589
      THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
bulwahn@32309
  1590
    | prove_prems out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
bulwahn@32309
  1591
      let
bulwahn@32309
  1592
        val premposition = (find_index (equal p) clauses) + nargs
bulwahn@32309
  1593
        val rest_tac = (case p of Prem (us, t) =>
bulwahn@32309
  1594
            let
bulwahn@32312
  1595
              val (_, out_ts''') = split_smode is us
bulwahn@32309
  1596
              val rec_tac = prove_prems out_ts''' ps
bulwahn@32309
  1597
            in
bulwahn@32309
  1598
              print_tac "before clause:"
bulwahn@32309
  1599
              THEN asm_simp_tac HOL_basic_ss 1
bulwahn@32309
  1600
              THEN print_tac "before prove_expr:"
bulwahn@32309
  1601
              THEN prove_expr thy (mode, t, us) premposition
bulwahn@32309
  1602
              THEN print_tac "after prove_expr:"
bulwahn@32309
  1603
              THEN rec_tac
bulwahn@32309
  1604
            end
bulwahn@32309
  1605
          | Negprem (us, t) =>
bulwahn@32309
  1606
            let
bulwahn@32312
  1607
              val (_, out_ts''') = split_smode is us
bulwahn@32309
  1608
              val rec_tac = prove_prems out_ts''' ps
bulwahn@32309
  1609
              val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
bulwahn@32309
  1610
              val (_, params) = strip_comb t
bulwahn@32309
  1611
            in
bulwahn@32309
  1612
              rtac @{thm bindI} 1
bulwahn@32309
  1613
              THEN (if (is_some name) then
bulwahn@32309
  1614
                  simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, is)]) 1
bulwahn@32309
  1615
                  THEN rtac @{thm not_predI} 1
bulwahn@32313
  1616
                  THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
bulwahn@32313
  1617
                  THEN (REPEAT_DETERM (atac 1))
bulwahn@32309
  1618
                  (* FIXME: work with parameter arguments *)
bulwahn@32309
  1619
                  THEN (EVERY (map (prove_param thy) (param_modes ~~ params)))
bulwahn@32309
  1620
                else
bulwahn@32309
  1621
                  rtac @{thm not_predI'} 1)
bulwahn@32313
  1622
                  THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
bulwahn@32309
  1623
              THEN rec_tac
bulwahn@32309
  1624
            end
bulwahn@32309
  1625
          | Sidecond t =>
bulwahn@32309
  1626
           rtac @{thm bindI} 1
bulwahn@32309
  1627
           THEN rtac @{thm if_predI} 1
bulwahn@32309
  1628
           THEN print_tac "before sidecond:"
bulwahn@32309
  1629
           THEN prove_sidecond thy modes t
bulwahn@32309
  1630
           THEN print_tac "after sidecond:"
bulwahn@32309
  1631
           THEN prove_prems [] ps)
bulwahn@32309
  1632
      in (prove_match thy out_ts)
bulwahn@32309
  1633
          THEN rest_tac
bulwahn@32309
  1634
      end;
bulwahn@32309
  1635
    val prems_tac = prove_prems in_ts moded_ps
bulwahn@32309
  1636
  in
bulwahn@32309
  1637
    rtac @{thm bindI} 1
bulwahn@32309
  1638
    THEN rtac @{thm singleI} 1
bulwahn@32309
  1639
    THEN prems_tac
bulwahn@32309
  1640
  end;
haftmann@30374
  1641
haftmann@30374
  1642
fun select_sup 1 1 = []
haftmann@30374
  1643
  | select_sup _ 1 = [rtac @{thm supI1}]
haftmann@30374
  1644
  | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
haftmann@30374
  1645
bulwahn@32309
  1646
fun prove_one_direction thy clauses preds modes pred mode moded_clauses =
bulwahn@32309
  1647
  let
bulwahn@32309
  1648
    val T = the (AList.lookup (op =) preds pred)
bulwahn@32309
  1649
    val nargs = length (binder_types T) - nparams_of thy pred
bulwahn@32313
  1650
    val pred_case_rule = the_elim_of thy pred
bulwahn@32309
  1651
  in
bulwahn@32309
  1652
    REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
bulwahn@32309
  1653
    THEN etac (predfun_elim_of thy pred mode) 1
bulwahn@32309
  1654
    THEN etac pred_case_rule 1
bulwahn@32309
  1655
    THEN (EVERY (map
bulwahn@32309
  1656
           (fn i => EVERY' (select_sup (length moded_clauses) i) i) 
bulwahn@32309
  1657
             (1 upto (length moded_clauses))))
bulwahn@32309
  1658
    THEN (EVERY (map2 (prove_clause thy nargs modes mode) clauses moded_clauses))
bulwahn@32309
  1659
    THEN print_tac "proved one direction"
bulwahn@32309
  1660
  end;
haftmann@30374
  1661
bulwahn@32308
  1662
(** Proof in the other direction **)
haftmann@30374
  1663
haftmann@30374
  1664
fun prove_match2 thy out_ts = let
haftmann@30374
  1665
  fun split_term_tac (Free _) = all_tac
haftmann@30374
  1666
    | split_term_tac t =
haftmann@30374
  1667
      if (is_constructor thy t) then let
haftmann@31784
  1668
        val info = Datatype.the_info thy ((fst o dest_Type o fastype_of) t)
haftmann@30374
  1669
        val num_of_constrs = length (#case_rewrites info)
haftmann@30374
  1670
        (* special treatment of pairs -- because of fishing *)
haftmann@30374
  1671
        val split_rules = case (fst o dest_Type o fastype_of) t of
haftmann@30374
  1672
          "*" => [@{thm prod.split_asm}] 
haftmann@30374
  1673
          | _ => PureThy.get_thms thy (((fst o dest_Type o fastype_of) t) ^ ".split_asm")
haftmann@30374
  1674
        val (_, ts) = strip_comb t
haftmann@30374
  1675
      in
bulwahn@31515
  1676
        (Splitter.split_asm_tac split_rules 1)
haftmann@30374
  1677
(*        THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
haftmann@30374
  1678
          THEN (DETERM (TRY (etac @{thm Pair_inject} 1))) *)
haftmann@30374
  1679
        THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2))
haftmann@30374
  1680
        THEN (EVERY (map split_term_tac ts))
haftmann@30374
  1681
      end
haftmann@30374
  1682
    else all_tac
haftmann@30374
  1683
  in
haftmann@30374
  1684
    split_term_tac (mk_tuple out_ts)
haftmann@30374
  1685
    THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1) THEN (etac @{thm botE} 2))))
haftmann@30374
  1686
  end
haftmann@30374
  1687
haftmann@30374
  1688
(* VERY LARGE SIMILIRATIY to function prove_param 
haftmann@30374
  1689
-- join both functions
bulwahn@31550
  1690
*)
bulwahn@32309
  1691
(* TODO: remove function *)
bulwahn@32313
  1692
bulwahn@32309
  1693
fun prove_param2 thy (NONE, t) = all_tac 
bulwahn@32309
  1694
  | prove_param2 thy (m as SOME (Mode (mode, is, ms)), t) = let
bulwahn@32315
  1695
    val  (f, args) = strip_comb (Envir.eta_contract t)
haftmann@30374
  1696
    val (params, _) = chop (length ms) args
haftmann@30374
  1697
    val f_tac = case f of
haftmann@30374
  1698
        Const (name, T) => full_simp_tac (HOL_basic_ss addsimps 
bulwahn@31514
  1699
           (@{thm eval_pred}::(predfun_definition_of thy name mode)
bulwahn@31514
  1700
           :: @{thm "Product_Type.split_conv"}::[])) 1
haftmann@30374
  1701
      | Free _ => all_tac
bulwahn@32315
  1702
      | _ => error "prove_param2: illegal parameter term"
haftmann@30374
  1703
  in  
haftmann@30374
  1704
    print_tac "before simplification in prove_args:"
haftmann@30374
  1705
    THEN f_tac
haftmann@30374
  1706
    THEN print_tac "after simplification in prove_args"
bulwahn@32309
  1707
    THEN (EVERY (map (prove_param2 thy) (ms ~~ params)))
haftmann@30374
  1708
  end
bulwahn@32313
  1709
bulwahn@31877
  1710
bulwahn@32309
  1711
fun prove_expr2 thy (Mode (mode, is, ms), t) = 
haftmann@30374
  1712
  (case strip_comb t of
haftmann@30374
  1713
    (Const (name, T), args) =>
bulwahn@32309
  1714
      etac @{thm bindE} 1
bulwahn@32309
  1715
      THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
bulwahn@32309
  1716
      THEN print_tac "prove_expr2-before"
bulwahn@32309
  1717
      THEN (debug_tac (Syntax.string_of_term_global thy
bulwahn@32309
  1718
        (prop_of (predfun_elim_of thy name mode))))
bulwahn@32309
  1719
      THEN (etac (predfun_elim_of thy name mode) 1)
bulwahn@32309
  1720
      THEN print_tac "prove_expr2"
bulwahn@32313
  1721
      THEN (EVERY (map (prove_param2 thy) (ms ~~ args)))
bulwahn@32309
  1722
      THEN print_tac "finished prove_expr2"      
haftmann@30374
  1723
    | _ => etac @{thm bindE} 1)
bulwahn@32309
  1724
    
bulwahn@32309
  1725
(* FIXME: what is this for? *)
bulwahn@32309
  1726
(* replace defined by has_mode thy pred *)
bulwahn@32309
  1727
(* TODO: rewrite function *)
haftmann@30374
  1728
fun prove_sidecond2 thy modes t = let
haftmann@30374
  1729
  fun preds_of t nameTs = case strip_comb t of 
haftmann@30374
  1730
    (f as Const (name, T), args) =>
haftmann@30374
  1731
      if AList.defined (op =) modes name then (name, T) :: nameTs
haftmann@30374
  1732
        else fold preds_of args nameTs
haftmann@30374
  1733
    | _ => nameTs
haftmann@30374
  1734
  val preds = preds_of t []
haftmann@30374
  1735
  val defs = map
bulwahn@31514
  1736
    (fn (pred, T) => predfun_definition_of thy pred ([], (1 upto (length (binder_types T)))))
haftmann@30374
  1737
      preds
haftmann@30374
  1738
  in
haftmann@30374
  1739
   (* only simplify the one assumption *)
haftmann@30374
  1740
   full_simp_tac (HOL_basic_ss' addsimps @{thm eval_pred} :: defs) 1 
haftmann@30374
  1741
   (* need better control here! *)
haftmann@30374
  1742
   THEN print_tac "after sidecond2 simplification"
haftmann@30374
  1743
   end
haftmann@30374
  1744
  
bulwahn@32309
  1745
fun prove_clause2 thy modes pred (iss, is) (ts, ps) i =
bulwahn@32309
  1746
  let
bulwahn@32309
  1747
    val pred_intro_rule = nth (intros_of thy pred) (i - 1)
bulwahn@32312
  1748
    val (in_ts, clause_out_ts) = split_smode is ts;
bulwahn@32309
  1749
    fun prove_prems2 out_ts [] =
bulwahn@32309
  1750
      print_tac "before prove_match2 - last call:"
bulwahn@32309
  1751
      THEN prove_match2 thy out_ts
bulwahn@32309
  1752
      THEN print_tac "after prove_match2 - last call:"
bulwahn@32309
  1753
      THEN (etac @{thm singleE} 1)
bulwahn@32309
  1754
      THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
bulwahn@32309
  1755
      THEN (asm_full_simp_tac HOL_basic_ss' 1)
bulwahn@32309
  1756
      THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
bulwahn@32309
  1757
      THEN (asm_full_simp_tac HOL_basic_ss' 1)
bulwahn@32309
  1758
      THEN SOLVED (print_tac "state before applying intro rule:"
haftmann@30374
  1759
      THEN (rtac pred_intro_rule 1)
haftmann@30374
  1760
      (* How to handle equality correctly? *)
haftmann@30374
  1761
      THEN (print_tac "state before assumption matching")
haftmann@30374
  1762
      THEN (REPEAT (atac 1 ORELSE 
haftmann@30374
  1763
         (CHANGED (asm_full_simp_tac HOL_basic_ss' 1)
haftmann@30374
  1764
          THEN print_tac "state after simp_tac:"))))
bulwahn@32309
  1765
    | prove_prems2 out_ts ((p, mode as Mode ((iss, is), _, param_modes)) :: ps) =
bulwahn@32309
  1766
      let
bulwahn@32309
  1767
        val rest_tac = (case p of
bulwahn@32309
  1768
          Prem (us, t) =>
haftmann@30374
  1769
          let
bulwahn@32312
  1770
            val (_, out_ts''') = split_smode is us
bulwahn@32309
  1771
            val rec_tac = prove_prems2 out_ts''' ps
haftmann@30374
  1772
          in
bulwahn@32309
  1773
            (prove_expr2 thy (mode, t)) THEN rec_tac
haftmann@30374
  1774
          end
haftmann@30374
  1775
        | Negprem (us, t) =>
haftmann@30374
  1776
          let
bulwahn@32312
  1777
            val (_, out_ts''') = split_smode is us
bulwahn@32309
  1778
            val rec_tac = prove_prems2 out_ts''' ps
haftmann@30374
  1779
            val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
haftmann@30374
  1780
            val (_, params) = strip_comb t
haftmann@30374
  1781
          in
haftmann@30374
  1782
            print_tac "before neg prem 2"
haftmann@30374
  1783
            THEN etac @{thm bindE} 1
haftmann@30374
  1784
            THEN (if is_some name then
bulwahn@32309
  1785
                full_simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, is)]) 1 
haftmann@30374
  1786
                THEN etac @{thm not_predE} 1
bulwahn@32313
  1787
                THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
bulwahn@32313
  1788
                THEN (EVERY (map (prove_param2 thy) (param_modes ~~ params)))
haftmann@30374
  1789
              else
haftmann@30374
  1790
                etac @{thm not_predE'} 1)
haftmann@30374
  1791
            THEN rec_tac
haftmann@30374
  1792
          end 
haftmann@30374
  1793
        | Sidecond t =>
bulwahn@32309
  1794
          etac @{thm bindE} 1
bulwahn@32309
  1795
          THEN etac @{thm if_predE} 1
bulwahn@32309
  1796
          THEN prove_sidecond2 thy modes t 
bulwahn@32309
  1797
          THEN prove_prems2 [] ps)
bulwahn@32309
  1798
      in print_tac "before prove_match2:"
bulwahn@32309
  1799
         THEN prove_match2 thy out_ts
bulwahn@32309
  1800
         THEN print_tac "after prove_match2:"
bulwahn@32309
  1801
         THEN rest_tac
bulwahn@32309
  1802
      end;
bulwahn@32309
  1803
    val prems_tac = prove_prems2 in_ts ps 
bulwahn@32309
  1804
  in
bulwahn@32309
  1805
    print_tac "starting prove_clause2"
bulwahn@32309
  1806
    THEN etac @{thm bindE} 1
bulwahn@32309
  1807
    THEN (etac @{thm singleE'} 1)
bulwahn@32309
  1808
    THEN (TRY (etac @{thm Pair_inject} 1))
bulwahn@32309
  1809
    THEN print_tac "after singleE':"
bulwahn@32309
  1810
    THEN prems_tac
bulwahn@32309
  1811
  end;
haftmann@30374
  1812
 
bulwahn@32309
  1813
fun prove_other_direction thy modes pred mode moded_clauses =
bulwahn@32309
  1814
  let
bulwahn@32309
  1815
    fun prove_clause clause i =
bulwahn@32309
  1816
      (if i < length moded_clauses then etac @{thm supE} 1 else all_tac)
bulwahn@32309
  1817
      THEN (prove_clause2 thy modes pred mode clause i)
bulwahn@32309
  1818
  in
bulwahn@32309
  1819
    (DETERM (TRY (rtac @{thm unit.induct} 1)))
bulwahn@32309
  1820
     THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
bulwahn@32309
  1821
     THEN (rtac (predfun_intro_of thy pred mode) 1)
bulwahn@32309
  1822
     THEN (REPEAT_DETERM (rtac @{thm refl} 2))
bulwahn@32309
  1823
     THEN (EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
bulwahn@32309
  1824
  end;
haftmann@30374
  1825
bulwahn@32308
  1826
(** proof procedure **)
bulwahn@32308
  1827
bulwahn@32309
  1828
fun prove_pred thy clauses preds modes pred mode (moded_clauses, compiled_term) =
bulwahn@32309
  1829
  let
bulwahn@32309
  1830
    val ctxt = ProofContext.init thy
bulwahn@32309
  1831
    val clauses = the (AList.lookup (op =) clauses pred)
bulwahn@32309
  1832
  in
bulwahn@32309
  1833
    Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
bulwahn@32309
  1834
      (if !do_proofs then
bulwahn@32309
  1835
        (fn _ =>
bulwahn@32309
  1836
        rtac @{thm pred_iffI} 1
bulwahn@32309
  1837
        THEN prove_one_direction thy clauses preds modes pred mode moded_clauses
bulwahn@32309
  1838
        THEN print_tac "proved one direction"
bulwahn@32309
  1839
        THEN prove_other_direction thy modes pred mode moded_clauses
bulwahn@32309
  1840
        THEN print_tac "proved other direction")
bulwahn@32309
  1841
       else (fn _ => mycheat_tac thy 1))
bulwahn@32309
  1842
  end;
haftmann@30374
  1843
bulwahn@32310
  1844
(* composition of mode inference, definition, compilation and proof *)
bulwahn@32310
  1845
bulwahn@32310
  1846
(** auxillary combinators for table of preds and modes **)
bulwahn@32310
  1847
bulwahn@32310
  1848
fun map_preds_modes f preds_modes_table =
bulwahn@32310
  1849
  map (fn (pred, modes) =>
bulwahn@32310
  1850
    (pred, map (fn (mode, value) => (mode, f pred mode value)) modes)) preds_modes_table
bulwahn@32310
  1851
bulwahn@32310
  1852
fun join_preds_modes table1 table2 =
bulwahn@32310
  1853
  map_preds_modes (fn pred => fn mode => fn value =>
bulwahn@32310
  1854
    (value, the (AList.lookup (op =) (the (AList.lookup (op =) table2 pred)) mode))) table1
bulwahn@32310
  1855
    
bulwahn@32310
  1856
fun maps_modes preds_modes_table =
bulwahn@32310
  1857
  map (fn (pred, modes) =>
bulwahn@32310
  1858
    (pred, map (fn (mode, value) => value) modes)) preds_modes_table  
bulwahn@32310
  1859
    
bulwahn@32311
  1860
fun compile_preds compfuns mk_fun_of use_size thy all_vs param_vs preds moded_clauses =
bulwahn@32311
  1861
  map_preds_modes (fn pred => compile_pred compfuns mk_fun_of use_size thy all_vs param_vs pred
bulwahn@32310
  1862
      (the (AList.lookup (op =) preds pred))) moded_clauses  
bulwahn@32310
  1863
  
bulwahn@32311
  1864
fun prove thy clauses preds modes moded_clauses compiled_terms =
bulwahn@32311
  1865
  map_preds_modes (prove_pred thy clauses preds modes)
bulwahn@32311
  1866
    (join_preds_modes moded_clauses compiled_terms)
haftmann@30374
  1867
bulwahn@32311
  1868
fun prove_by_skip thy _ _ _ _ compiled_terms =
wenzelm@32970
  1869
  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (Skip_Proof.make_thm thy t))
bulwahn@32311
  1870
    compiled_terms
bulwahn@32311
  1871
    
bulwahn@31514
  1872
fun prepare_intrs thy prednames =
bulwahn@31514
  1873
  let
bulwahn@32308
  1874
    val intrs = maps (intros_of thy) prednames
bulwahn@31514
  1875
      |> map (Logic.unvarify o prop_of)
bulwahn@31514
  1876
    val nparams = nparams_of thy (hd prednames)
bulwahn@32316
  1877
    val extra_modes = all_modes_of thy |> filter_out (fn (name, _) => member (op =) prednames name)
bulwahn@31514
  1878
    val preds = distinct (op =) (map (dest_Const o fst o (strip_intro_concl nparams)) intrs)
bulwahn@31514
  1879
    val _ $ u = Logic.strip_imp_concl (hd intrs);
bulwahn@31514
  1880
    val params = List.take (snd (strip_comb u), nparams);
bulwahn@31514
  1881
    val param_vs = maps term_vs params
bulwahn@31514
  1882
    val all_vs = terms_vs intrs
bulwahn@31514
  1883
    fun dest_prem t =
haftmann@30374
  1884
      (case strip_comb t of
haftmann@30374
  1885
        (v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t
bulwahn@32311
  1886
      | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem t of          
haftmann@30374
  1887
          Prem (ts, t) => Negprem (ts, t)
bulwahn@31515
  1888
        | Negprem _ => error ("Double negation not allowed in premise: " ^ (Syntax.string_of_term_global thy (c $ t))) 
haftmann@30374
  1889
        | Sidecond t => Sidecond (c $ t))
haftmann@30374
  1890
      | (c as Const (s, _), ts) =>
bulwahn@31877
  1891
        if is_registered thy s then
bulwahn@31514
  1892
          let val (ts1, ts2) = chop (nparams_of thy s) ts
haftmann@30374
  1893
          in Prem (ts2, list_comb (c, ts1)) end
haftmann@30374
  1894
        else Sidecond t
haftmann@30374
  1895
      | _ => Sidecond t)
bulwahn@31514
  1896
    fun add_clause intr (clauses, arities) =
bulwahn@31514
  1897
    let
bulwahn@31514
  1898
      val _ $ t = Logic.strip_imp_concl intr;
bulwahn@31514
  1899
      val (Const (name, T), ts) = strip_comb t;
bulwahn@31514
  1900
      val (ts1, ts2) = chop nparams ts;
bulwahn@31514
  1901
      val prems = map (dest_prem o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr);
bulwahn@31514
  1902
      val (Ts, Us) = chop nparams (binder_types T)
bulwahn@31514
  1903
    in
bulwahn@31514
  1904
      (AList.update op = (name, these (AList.lookup op = clauses name) @
bulwahn@31514
  1905
        [(ts2, prems)]) clauses,
bulwahn@31514
  1906
       AList.update op = (name, (map (fn U => (case strip_type U of
haftmann@30374
  1907
                 (Rs as _ :: _, Type ("bool", [])) => SOME (length Rs)
haftmann@30374
  1908
               | _ => NONE)) Ts,
haftmann@30374
  1909
             length Us)) arities)
bulwahn@31514
  1910
    end;
bulwahn@31514
  1911
    val (clauses, arities) = fold add_clause intrs ([], []);
bulwahn@31514
  1912
  in (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) end;
bulwahn@31514
  1913
bulwahn@32312
  1914
(** main function of predicate compiler **)
bulwahn@31514
  1915
bulwahn@32311
  1916
fun add_equations_of steps prednames thy =
bulwahn@32317
  1917
  let
wenzelm@32950
  1918
    val _ = tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
bulwahn@32317
  1919
    val (preds, nparams, all_vs, param_vs, extra_modes, clauses, arities) =
bulwahn@32317
  1920
      prepare_intrs thy prednames
wenzelm@32950
  1921
    val _ = tracing "Infering modes..."
bulwahn@32317
  1922
    val moded_clauses = #infer_modes steps thy extra_modes arities param_vs clauses 
bulwahn@32317
  1923
    val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
bulwahn@32317
  1924
    val _ = print_modes modes
bulwahn@32317
  1925
    val _ = print_moded_clauses thy moded_clauses
wenzelm@32950
  1926
    val _ = tracing "Defining executable functions..."
bulwahn@32317
  1927
    val thy' = fold (#create_definitions steps preds) modes thy
bulwahn@32317
  1928
      |> Theory.checkpoint
wenzelm@32950
  1929
    val _ = tracing "Compiling equations..."
bulwahn@32317
  1930
    val compiled_terms =
bulwahn@32317
  1931
      (#compile_preds steps) thy' all_vs param_vs preds moded_clauses
bulwahn@32317
  1932
    val _ = print_compiled_terms thy' compiled_terms
wenzelm@32950
  1933
    val _ = tracing "Proving equations..."
bulwahn@32317
  1934
    val result_thms = #prove steps thy' clauses preds (extra_modes @ modes)
bulwahn@32317
  1935
      moded_clauses compiled_terms
bulwahn@32317
  1936
    val qname = #qname steps
bulwahn@32317
  1937
    (* val attrib = gn thy => Attrib.attribute_i thy Code.add_eqn_attrib *)
bulwahn@32317
  1938
    val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
bulwahn@32317
  1939
      (fn thm => Context.mapping (Code.add_eqn thm) I))))
bulwahn@32317
  1940
    val thy'' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
bulwahn@32317
  1941
      [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
bulwahn@32317
  1942
        [attrib thy ])] thy))
bulwahn@32317
  1943
      (maps_modes result_thms) thy'
bulwahn@32317
  1944
      |> Theory.checkpoint
bulwahn@32317
  1945
  in
bulwahn@32317
  1946
    thy''
bulwahn@32317
  1947
  end
haftmann@30374
  1948
bulwahn@32314
  1949
fun extend' value_of edges_of key (G, visited) =
bulwahn@32314
  1950
  let
bulwahn@32314
  1951
    val (G', v) = case try (Graph.get_node G) key of
bulwahn@32314
  1952
        SOME v => (G, v)
bulwahn@32314
  1953
      | NONE => (Graph.new_node (key, value_of key) G, value_of key)
bulwahn@32314
  1954
    val (G'', visited') = fold (extend' value_of edges_of) (edges_of (key, v) \\ visited)
bulwahn@32314
  1955
      (G', key :: visited) 
bulwahn@32314
  1956
  in
bulwahn@32314
  1957
    (fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited')
bulwahn@32314
  1958
  end;
bulwahn@32314
  1959
bulwahn@32314
  1960
fun extend value_of edges_of key G = fst (extend' value_of edges_of key (G, [])) 
bulwahn@32314
  1961
  
bulwahn@32312
  1962
fun gen_add_equations steps names thy =
bulwahn@32312
  1963
  let
bulwahn@32316
  1964
    val thy' = PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of thy)) names) thy
bulwahn@32316
  1965
      |> Theory.checkpoint;
bulwahn@32312
  1966
    fun strong_conn_of gr keys =
bulwahn@32312
  1967
      Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
bulwahn@32312
  1968
    val scc = strong_conn_of (PredData.get thy') names
bulwahn@32312
  1969
    val thy'' = fold_rev
bulwahn@32312
  1970
      (fn preds => fn thy =>
bulwahn@32312
  1971
        if #are_not_defined steps thy preds then add_equations_of steps preds thy else thy)
bulwahn@32312
  1972
      scc thy' |> Theory.checkpoint
bulwahn@32312
  1973
  in thy'' end
bulwahn@32312
  1974
bulwahn@32312
  1975
(* different instantiantions of the predicate compiler *)
bulwahn@32312
  1976
bulwahn@32312
  1977
val add_equations = gen_add_equations
bulwahn@32312
  1978
  {infer_modes = infer_modes false,
bulwahn@32312
  1979
  create_definitions = create_definitions,
bulwahn@32312
  1980
  compile_preds = compile_preds PredicateCompFuns.compfuns mk_fun_of false,
bulwahn@32312
  1981
  prove = prove,
bulwahn@32312
  1982
  are_not_defined = (fn thy => forall (null o modes_of thy)),
bulwahn@32312
  1983
  qname = "equation"}
bulwahn@32312
  1984
bulwahn@32312
  1985
val add_sizelim_equations = gen_add_equations
bulwahn@32312
  1986
  {infer_modes = infer_modes false,
bulwahn@32312
  1987
  create_definitions = sizelim_create_definitions,
bulwahn@32312
  1988
  compile_preds = compile_preds PredicateCompFuns.compfuns mk_sizelim_fun_of true,
bulwahn@32312
  1989
  prove = prove_by_skip,
bulwahn@32312
  1990
  are_not_defined = (fn thy => fn preds => true), (* TODO *)
bulwahn@32312
  1991
  qname = "sizelim_equation"
bulwahn@32312
  1992
  }
bulwahn@32312
  1993
  
bulwahn@32312
  1994
val add_quickcheck_equations = gen_add_equations
bulwahn@32312
  1995
  {infer_modes = infer_modes_with_generator,
bulwahn@32312
  1996
  create_definitions = rpred_create_definitions,
bulwahn@32312
  1997
  compile_preds = compile_preds RPredCompFuns.compfuns mk_generator_of true,
bulwahn@32312
  1998
  prove = prove_by_skip,
bulwahn@32312
  1999
  are_not_defined = (fn thy => fn preds => true), (* TODO *)
bulwahn@32312
  2000
  qname = "rpred_equation"}
bulwahn@32312
  2001
bulwahn@32312
  2002
(** user interface **)
bulwahn@32312
  2003
bulwahn@31106
  2004
(* generation of case rules from user-given introduction rules *)
bulwahn@31106
  2005
bulwahn@31550
  2006
fun mk_casesrule ctxt nparams introrules =
haftmann@31124
  2007
  let
bulwahn@31573
  2008
    val intros = map (Logic.unvarify o prop_of) introrules
bulwahn@31514
  2009
    val (pred, (params, args)) = strip_intro_concl nparams (hd intros)
bulwahn@31106
  2010
    val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt
bulwahn@31106
  2011
    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
bulwahn@31106
  2012
    val (argnames, ctxt2) = Variable.variant_fixes
bulwahn@31106
  2013
      (map (fn i => "a" ^ string_of_int i) (1 upto (length args))) ctxt1
bulwahn@31514
  2014
    val argvs = map2 (curry Free) argnames (map fastype_of args)
bulwahn@32311
  2015
    fun mk_case intro =
bulwahn@32311
  2016
      let
bulwahn@31514
  2017
        val (_, (_, args)) = strip_intro_concl nparams intro
bulwahn@31106
  2018
        val prems = Logic.strip_imp_prems intro
bulwahn@31106
  2019
        val eqprems = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (argvs ~~ args)
bulwahn@31106
  2020
        val frees = (fold o fold_aterms)
bulwahn@31106
  2021
          (fn t as Free _ =>
bulwahn@31106
  2022
              if member (op aconv) params t then I else insert (op aconv) t
bulwahn@31106
  2023
           | _ => I) (args @ prems) []
bulwahn@32311
  2024
      in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
bulwahn@31106
  2025
    val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
bulwahn@31106
  2026
    val cases = map mk_case intros
bulwahn@31550
  2027
  in Logic.list_implies (assm :: cases, prop) end;
bulwahn@31106
  2028
bulwahn@32312
  2029
(* code_pred_intro attribute *)
bulwahn@32311
  2030
bulwahn@31876
  2031
fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
bulwahn@31876
  2032
bulwahn@31876
  2033
val code_pred_intros_attrib = attrib add_intro;
bulwahn@31876
  2034
haftmann@31124
  2035
local
haftmann@31124
  2036
bulwahn@31514
  2037
(* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
bulwahn@31514
  2038
(* TODO: must create state to prove multiple cases *)
haftmann@31124
  2039
fun generic_code_pred prep_const raw_const lthy =
haftmann@31124
  2040
  let
bulwahn@31550
  2041
    val thy = ProofContext.theory_of lthy
haftmann@31124
  2042
    val const = prep_const thy raw_const
bulwahn@32314
  2043
    val lthy' = LocalTheory.theory (PredData.map
bulwahn@32314
  2044
        (extend (fetch_pred_data thy) (depending_preds_of thy) const)) lthy
wenzelm@31554
  2045
      |> LocalTheory.checkpoint
bulwahn@31550
  2046
    val thy' = ProofContext.theory_of lthy'
bulwahn@31514
  2047
    val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy')
bulwahn@31550
  2048
    fun mk_cases const =
bulwahn@31514
  2049
      let
bulwahn@31550
  2050
        val nparams = nparams_of thy' const
bulwahn@31550
  2051
        val intros = intros_of thy' const
bulwahn@31580
  2052
      in mk_casesrule lthy' nparams intros end  
bulwahn@31550
  2053
    val cases_rules = map mk_cases preds
bulwahn@31580
  2054
    val cases =
bulwahn@31580
  2055
      map (fn case_rule => RuleCases.Case {fixes = [],
bulwahn@31580
  2056
        assumes = [("", Logic.strip_imp_prems case_rule)],
bulwahn@31580
  2057
        binds = [], cases = []}) cases_rules
bulwahn@31580
  2058
    val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
bulwahn@32318
  2059
    val lthy'' = lthy'
bulwahn@32318
  2060
      |> fold Variable.auto_fixes cases_rules 
bulwahn@32318
  2061
      |> ProofContext.add_cases true case_env
bulwahn@32318
  2062
    fun after_qed thms goal_ctxt =
bulwahn@32318
  2063
      let
bulwahn@32318
  2064
        val global_thms = ProofContext.export goal_ctxt
bulwahn@32318
  2065
          (ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms)
bulwahn@32318
  2066
      in
bulwahn@32318
  2067
        goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #> add_equations [const])
bulwahn@32318
  2068
      end  
haftmann@31124
  2069
  in
bulwahn@31580
  2070
    Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy''
haftmann@31124
  2071
  end;
haftmann@31124
  2072
haftmann@31124
  2073
structure P = OuterParse
bulwahn@31106
  2074
haftmann@31124
  2075
in
haftmann@31124
  2076
haftmann@31124
  2077
val code_pred = generic_code_pred (K I);
haftmann@31156
  2078
val code_pred_cmd = generic_code_pred Code.read_const
haftmann@31124
  2079
bulwahn@31514
  2080
val setup = PredData.put (Graph.empty) #>
bulwahn@31514
  2081
  Attrib.setup @{binding code_pred_intros} (Scan.succeed (attrib add_intro))
bulwahn@31514
  2082
    "adding alternative introduction rules for code generation of inductive predicates"
bulwahn@31514
  2083
(*  Attrib.setup @{binding code_ind_cases} (Scan.succeed add_elim_attrib)
haftmann@31124
  2084
    "adding alternative elimination rules for code generation of inductive predicates";
bulwahn@31514
  2085
    *)
haftmann@31124
  2086
  (*FIXME name discrepancy in attribs and ML code*)
haftmann@31124
  2087
  (*FIXME intros should be better named intro*)
bulwahn@31514
  2088
  (*FIXME why distinguished attribute for cases?*)
haftmann@31124
  2089
haftmann@31124
  2090
val _ = OuterSyntax.local_theory_to_proof "code_pred"
haftmann@31124
  2091
  "prove equations for predicate specified by intro/elim rules"
haftmann@31124
  2092
  OuterKeyword.thy_goal (P.term_group >> code_pred_cmd)
haftmann@31124
  2093
haftmann@31124
  2094
end
haftmann@31124
  2095
haftmann@31124
  2096
(*FIXME
haftmann@31124
  2097
- Naming of auxiliary rules necessary?
haftmann@31217
  2098
- add default code equations P x y z = P_i_i_i x y z
haftmann@31124
  2099
*)
bulwahn@31106
  2100
bulwahn@31169
  2101
(* transformation for code generation *)
bulwahn@31169
  2102
wenzelm@32740
  2103
val eval_ref = Unsynchronized.ref (NONE : (unit -> term Predicate.pred) option);
haftmann@31217
  2104
haftmann@32341
  2105
(*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
haftmann@31217
  2106
fun analyze_compr thy t_compr =
haftmann@31217
  2107
  let
haftmann@31217
  2108
    val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
haftmann@31217
  2109
      | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
haftmann@32342
  2110
    val (body, Ts, fp) = HOLogic.strip_psplits split;
haftmann@32341
  2111
    val (pred as Const (name, T), all_args) = strip_comb body;
haftmann@32341
  2112
    val (params, args) = chop (nparams_of thy name) all_args;
haftmann@31217
  2113
    val user_mode = map_filter I (map_index
haftmann@31217
  2114
      (fn (i, t) => case t of Bound j => if j < length Ts then NONE
haftmann@32341
  2115
        else SOME (i+1) | _ => SOME (i+1)) args); (*FIXME dangling bounds should not occur*)
haftmann@31217
  2116
    val modes = filter (fn Mode (_, is, _) => is = user_mode)
bulwahn@31514
  2117
      (modes_of_term (all_modes_of thy) (list_comb (pred, params)));
haftmann@31217
  2118
    val m = case modes
haftmann@31217
  2119
     of [] => error ("No mode possible for comprehension "
haftmann@31217
  2120
                ^ Syntax.string_of_term_global thy t_compr)
haftmann@31217
  2121
      | [m] => m
haftmann@31217
  2122
      | m :: _ :: _ => (warning ("Multiple modes possible for comprehension "
haftmann@31217
  2123
                ^ Syntax.string_of_term_global thy t_compr); m);
haftmann@32351
  2124
    val (inargs, outargs) = split_smode user_mode args;
haftmann@32351
  2125
    val t_pred = list_comb (compile_expr NONE thy (m, list_comb (pred, params)), inargs);
haftmann@32341
  2126
    val t_eval = if null outargs then t_pred else let
haftmann@32341
  2127
        val outargs_bounds = map (fn Bound i => i) outargs;
haftmann@32341
  2128
        val outargsTs = map (nth Ts) outargs_bounds;
haftmann@32342
  2129
        val T_pred = HOLogic.mk_tupleT outargsTs;
haftmann@32342
  2130
        val T_compr = HOLogic.mk_ptupleT fp Ts;
haftmann@32341
  2131
        val arrange_bounds = map_index I outargs_bounds
haftmann@32341
  2132
          |> sort (prod_ord (K EQUAL) int_ord)
haftmann@32341
  2133
          |> map fst;
haftmann@32341
  2134
        val arrange = funpow (length outargs_bounds - 1) HOLogic.mk_split
haftmann@32341
  2135
          (Term.list_abs (map (pair "") outargsTs,
haftmann@32342
  2136
            HOLogic.mk_ptuple fp T_compr (map Bound arrange_bounds)))
haftmann@32351
  2137
      in mk_map PredicateCompFuns.compfuns T_pred T_compr arrange t_pred end
haftmann@31217
  2138
  in t_eval end;
bulwahn@31169
  2139
haftmann@32341
  2140
fun eval thy t_compr =
haftmann@32341
  2141
  let
haftmann@32341
  2142
    val t = analyze_compr thy t_compr;
haftmann@32351
  2143
    val T = dest_predT PredicateCompFuns.compfuns (fastype_of t);
haftmann@32351
  2144
    val t' = mk_map PredicateCompFuns.compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
haftmann@32341
  2145
  in (T, Code_ML.eval NONE ("Predicate_Compile.eval_ref", eval_ref) Predicate.map thy t' []) end;
haftmann@32341
  2146
haftmann@32341
  2147
fun values ctxt k t_compr =
haftmann@32341
  2148
  let
haftmann@32341
  2149
    val thy = ProofContext.theory_of ctxt;
haftmann@32341
  2150
    val (T, t) = eval thy t_compr;
haftmann@32341
  2151
    val setT = HOLogic.mk_setT T;
haftmann@32341
  2152
    val (ts, _) = Predicate.yieldn k t;
haftmann@32341
  2153
    val elemsT = HOLogic.mk_set T ts;
haftmann@32341
  2154
  in if k = ~1 orelse length ts < k then elemsT
haftmann@32683
  2155
    else Const (@{const_name Lattices.sup}, setT --> setT --> setT) $ elemsT $ t_compr
haftmann@32341
  2156
  end;
haftmann@32341
  2157
haftmann@32341
  2158
fun values_cmd modes k raw_t state =
haftmann@32341
  2159
  let
haftmann@32341
  2160
    val ctxt = Toplevel.context_of state;
haftmann@32341
  2161
    val t = Syntax.read_term ctxt raw_t;
haftmann@32341
  2162
    val t' = values ctxt k t;
haftmann@32341
  2163
    val ty' = Term.type_of t';
haftmann@32341
  2164
    val ctxt' = Variable.auto_fixes t' ctxt;
haftmann@32341
  2165
    val p = PrintMode.with_modes modes (fn () =>
haftmann@32341
  2166
      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
haftmann@32341
  2167
        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
haftmann@32341
  2168
  in Pretty.writeln p end;
haftmann@32341
  2169
haftmann@32341
  2170
local structure P = OuterParse in
haftmann@32341
  2171
haftmann@32341
  2172
val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
haftmann@32341
  2173
haftmann@32341
  2174
val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
haftmann@32341
  2175
  (opt_modes -- Scan.optional P.nat ~1 -- P.term
haftmann@32341
  2176
    >> (fn ((modes, k), t) => Toplevel.no_timing o Toplevel.keep
haftmann@32341
  2177
        (values_cmd modes k t)));
haftmann@32341
  2178
haftmann@30374
  2179
end;
haftmann@30374
  2180
haftmann@32341
  2181
end;
haftmann@32341
  2182