src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
author bulwahn
Fri, 11 Nov 2011 10:40:36 +0100
changeset 45452 414732ebf891
parent 45450 dc2236b19a3d
child 45461 130c90bb80b4
permissions -rw-r--r--
increasing values_timeout to avoid failures of isatest with HOL-IMP
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33265
01c9c6dbd890 proper headers;
wenzelm
parents: 33256
diff changeset
     1
(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_core.ML
01c9c6dbd890 proper headers;
wenzelm
parents: 33256
diff changeset
     2
    Author:     Lukas Bulwahn, TU Muenchen
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
     3
33265
01c9c6dbd890 proper headers;
wenzelm
parents: 33256
diff changeset
     4
A compiler from predicates specified by intro/elim rules to equations.
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
     5
*)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
     6
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
     7
signature PREDICATE_COMPILE_CORE =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
     8
sig
36048
1d2faa488166 clarifying the Predicate_Compile_Core signature
bulwahn
parents: 36046
diff changeset
     9
  type mode = Predicate_Compile_Aux.mode
1d2faa488166 clarifying the Predicate_Compile_Core signature
bulwahn
parents: 36046
diff changeset
    10
  type options = Predicate_Compile_Aux.options
1d2faa488166 clarifying the Predicate_Compile_Core signature
bulwahn
parents: 36046
diff changeset
    11
  type compilation = Predicate_Compile_Aux.compilation
1d2faa488166 clarifying the Predicate_Compile_Core signature
bulwahn
parents: 36046
diff changeset
    12
  type compilation_funs = Predicate_Compile_Aux.compilation_funs
1d2faa488166 clarifying the Predicate_Compile_Core signature
bulwahn
parents: 36046
diff changeset
    13
  
33478
b70fe083694d moved values command from core to predicate compile
bulwahn
parents: 33476
diff changeset
    14
  val setup : theory -> theory
36048
1d2faa488166 clarifying the Predicate_Compile_Core signature
bulwahn
parents: 36046
diff changeset
    15
  val code_pred : options -> string -> Proof.context -> Proof.state
1d2faa488166 clarifying the Predicate_Compile_Core signature
bulwahn
parents: 36046
diff changeset
    16
  val code_pred_cmd : options -> string -> Proof.context -> Proof.state
1d2faa488166 clarifying the Predicate_Compile_Core signature
bulwahn
parents: 36046
diff changeset
    17
  val values_cmd : string list -> mode option list option
1d2faa488166 clarifying the Predicate_Compile_Core signature
bulwahn
parents: 36046
diff changeset
    18
    -> ((string option * bool) * (compilation * int list)) -> int -> string -> Toplevel.state -> unit
40053
3fa49ea76cbb using a signature in core_data and moving some more functions to core_data
bulwahn
parents: 40052
diff changeset
    19
42141
2c255ba8f299 changing values_timeout from a static option to a dynamic option as required for testing with SML/NJ
bulwahn
parents: 42094
diff changeset
    20
  val values_timeout : real Config.T
2c255ba8f299 changing values_timeout from a static option to a dynamic option as required for testing with SML/NJ
bulwahn
parents: 42094
diff changeset
    21
  
37007
116670499530 changing operations for accessing data to work with contexts
bulwahn
parents: 37006
diff changeset
    22
  val print_stored_rules : Proof.context -> unit
37003
a393a588b82e moving towards working with proof contexts in the predicate compiler
bulwahn
parents: 37002
diff changeset
    23
  val print_all_modes : compilation -> Proof.context -> unit
39388
fdbb2c55ffc2 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents: 39310
diff changeset
    24
fdbb2c55ffc2 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents: 39310
diff changeset
    25
  val put_pred_result : (unit -> term Predicate.pred) -> Proof.context -> Proof.context
fdbb2c55ffc2 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents: 39310
diff changeset
    26
  val put_pred_random_result : (unit -> int * int -> term Predicate.pred * (int * int)) ->
fdbb2c55ffc2 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents: 39310
diff changeset
    27
    Proof.context -> Proof.context
fdbb2c55ffc2 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents: 39310
diff changeset
    28
  val put_dseq_result : (unit -> term DSequence.dseq) -> Proof.context -> Proof.context
fdbb2c55ffc2 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents: 39310
diff changeset
    29
  val put_dseq_random_result : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) ->
fdbb2c55ffc2 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents: 39310
diff changeset
    30
    Proof.context -> Proof.context
40102
a9e4e94b3022 restructuring values command and adding generator compilation
bulwahn
parents: 40053
diff changeset
    31
  val put_new_dseq_result : (unit -> int -> term Lazy_Sequence.lazy_sequence) ->
a9e4e94b3022 restructuring values command and adding generator compilation
bulwahn
parents: 40053
diff changeset
    32
    Proof.context -> Proof.context
39388
fdbb2c55ffc2 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents: 39310
diff changeset
    33
  val put_lseq_random_result :
fdbb2c55ffc2 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents: 39310
diff changeset
    34
    (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) ->
fdbb2c55ffc2 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents: 39310
diff changeset
    35
    Proof.context -> Proof.context
fdbb2c55ffc2 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents: 39310
diff changeset
    36
  val put_lseq_random_stats_result :
fdbb2c55ffc2 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents: 39310
diff changeset
    37
    (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) ->
fdbb2c55ffc2 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents: 39310
diff changeset
    38
    Proof.context -> Proof.context
fdbb2c55ffc2 replaced ML_Context.evaluate by ML_Context.value -- using context data instead of bare metal references
haftmann
parents: 39310
diff changeset
    39
33628
ed2111a5c3ed renaming code_pred_intros to code_pred_intro
bulwahn
parents: 33626
diff changeset
    40
  val code_pred_intro_attrib : attribute
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    41
  (* used by Quickcheck_Generator *) 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    42
  (* temporary for testing of the compilation *)
36048
1d2faa488166 clarifying the Predicate_Compile_Core signature
bulwahn
parents: 36046
diff changeset
    43
  val add_equations : options -> string list -> theory -> theory
1d2faa488166 clarifying the Predicate_Compile_Core signature
bulwahn
parents: 36046
diff changeset
    44
  val add_depth_limited_random_equations : options -> string list -> theory -> theory
1d2faa488166 clarifying the Predicate_Compile_Core signature
bulwahn
parents: 36046
diff changeset
    45
  val add_random_dseq_equations : options -> string list -> theory -> theory
1d2faa488166 clarifying the Predicate_Compile_Core signature
bulwahn
parents: 36046
diff changeset
    46
  val add_new_random_dseq_equations : options -> string list -> theory -> theory
40103
ef73a90ab6e6 adding generator quickcheck
bulwahn
parents: 40102
diff changeset
    47
  val add_generator_dseq_equations : options -> string list -> theory -> theory
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
    48
  val add_generator_cps_equations : options -> string list -> theory -> theory
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
    49
  val mk_tracing : string -> term -> term
39310
17ef4415b17c removing obsolete argument in prepare_intrs; passing context instead of theory in prepare_intrs
bulwahn
parents: 39299
diff changeset
    50
  val prepare_intrs : options -> Proof.context -> string list -> thm list ->
38957
2eb265efa1b0 exporting mode analysis for use in prolog generation
bulwahn
parents: 38864
diff changeset
    51
    ((string * typ) list * string list * string list * (string * mode list) list *
2eb265efa1b0 exporting mode analysis for use in prolog generation
bulwahn
parents: 38864
diff changeset
    52
      (string *  (Term.term list * Predicate_Compile_Aux.indprem list) list) list)
39761
c2a76ec6e2d9 renaming use_random to use_generators in the predicate compiler
bulwahn
parents: 39760
diff changeset
    53
  type mode_analysis_options =
c2a76ec6e2d9 renaming use_random to use_generators in the predicate compiler
bulwahn
parents: 39760
diff changeset
    54
   {use_generators : bool,
c2a76ec6e2d9 renaming use_random to use_generators in the predicate compiler
bulwahn
parents: 39760
diff changeset
    55
    reorder_premises : bool,
c2a76ec6e2d9 renaming use_random to use_generators in the predicate compiler
bulwahn
parents: 39760
diff changeset
    56
    infer_pos_and_neg_modes : bool}  
38957
2eb265efa1b0 exporting mode analysis for use in prolog generation
bulwahn
parents: 38864
diff changeset
    57
  datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
39310
17ef4415b17c removing obsolete argument in prepare_intrs; passing context instead of theory in prepare_intrs
bulwahn
parents: 39299
diff changeset
    58
    | Mode_Pair of mode_derivation * mode_derivation | Term of mode
39461
0ed0f015d140 adding mode inference to prolog compilation; separate between (ad-hoc) code modifications and system_configuration; adapting quickcheck
bulwahn
parents: 39403
diff changeset
    59
  val head_mode_of : mode_derivation -> mode
38957
2eb265efa1b0 exporting mode analysis for use in prolog generation
bulwahn
parents: 38864
diff changeset
    60
  type moded_clause = term list * (Predicate_Compile_Aux.indprem * mode_derivation) list
2eb265efa1b0 exporting mode analysis for use in prolog generation
bulwahn
parents: 38864
diff changeset
    61
  type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
2eb265efa1b0 exporting mode analysis for use in prolog generation
bulwahn
parents: 38864
diff changeset
    62
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    63
end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    64
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    65
structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    66
struct
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    67
32668
b2de45007537 added first prototype of the extended predicate compiler
bulwahn
parents: 32667
diff changeset
    68
open Predicate_Compile_Aux;
40052
ea46574ca815 splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents: 40051
diff changeset
    69
open Core_Data;
ea46574ca815 splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents: 40051
diff changeset
    70
open Mode_Inference;
ea46574ca815 splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents: 40051
diff changeset
    71
open Predicate_Compile_Proof;
33108
9d9afd478016 added test for higher-order function inductification; added debug messages
bulwahn
parents: 33106
diff changeset
    72
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    73
(** fundamentals **)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    74
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    75
(* syntactic operations *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    76
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    77
fun mk_eq (x, xs) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    78
  let fun mk_eqs _ [] = []
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    79
        | mk_eqs a (b::cs) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    80
            HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    81
  in mk_eqs x xs end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    82
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    83
fun mk_scomp (t, u) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    84
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    85
    val T = fastype_of t
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    86
    val U = fastype_of u
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    87
    val [A] = binder_types T
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    88
    val D = body_type U                   
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    89
  in 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    90
    Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    91
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    92
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    93
fun dest_randomT (Type ("fun", [@{typ Random.seed},
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37591
diff changeset
    94
  Type (@{type_name Product_Type.prod}, [Type (@{type_name Product_Type.prod}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    95
  | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    96
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
    97
fun mk_tracing s t =
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
    98
  Const(@{const_name Code_Evaluation.tracing},
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
    99
    @{typ String.literal} --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   100
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   101
(* representation of inferred clauses with modes *)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   102
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   103
type moded_clause = term list * (indprem * mode_derivation) list
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   104
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
   105
type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   106
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   107
(* diagnostic display functions *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   108
37004
c62f743e37d4 removing unused argument in print_modes function
bulwahn
parents: 37003
diff changeset
   109
fun print_modes options modes =
33251
4b13ab778b78 added option show_modes to predicate compiler
bulwahn
parents: 33250
diff changeset
   110
  if show_modes options then
33326
7d0288d90535 improved handling of alternative rules; added test cases for alternative rules; normalized tracing in the predicate compiler
bulwahn
parents: 33268
diff changeset
   111
    tracing ("Inferred modes:\n" ^
33251
4b13ab778b78 added option show_modes to predicate compiler
bulwahn
parents: 33250
diff changeset
   112
      cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
   113
        (fn (p, m) => string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes))
33251
4b13ab778b78 added option show_modes to predicate compiler
bulwahn
parents: 33250
diff changeset
   114
  else ()
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   115
37004
c62f743e37d4 removing unused argument in print_modes function
bulwahn
parents: 37003
diff changeset
   116
fun print_pred_mode_table string_of_entry pred_mode_table =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   117
  let
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
   118
    fun print_mode pred ((pol, mode), entry) =  "mode : " ^ string_of_mode mode
33619
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   119
      ^ string_of_entry pred mode entry
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   120
    fun print_pred (pred, modes) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   121
      "predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
33326
7d0288d90535 improved handling of alternative rules; added test cases for alternative rules; normalized tracing in the predicate compiler
bulwahn
parents: 33268
diff changeset
   122
    val _ = tracing (cat_lines (map print_pred pred_mode_table))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   123
  in () end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   124
37005
842a73dc6d0e changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents: 37004
diff changeset
   125
fun print_compiled_terms options ctxt =
33139
9c01ee6f8ee9 added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents: 33138
diff changeset
   126
  if show_compilation options then
37005
842a73dc6d0e changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents: 37004
diff changeset
   127
    print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term ctxt)
33139
9c01ee6f8ee9 added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents: 33138
diff changeset
   128
  else K ()
9c01ee6f8ee9 added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents: 33138
diff changeset
   129
37007
116670499530 changing operations for accessing data to work with contexts
bulwahn
parents: 37006
diff changeset
   130
fun print_stored_rules ctxt =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   131
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42141
diff changeset
   132
    val preds = Graph.keys (PredData.get (Proof_Context.theory_of ctxt))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   133
    fun print pred () = let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   134
      val _ = writeln ("predicate: " ^ pred)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   135
      val _ = writeln ("introrules: ")
37007
116670499530 changing operations for accessing data to work with contexts
bulwahn
parents: 37006
diff changeset
   136
      val _ = fold (fn thm => fn u => writeln (Display.string_of_thm ctxt thm))
116670499530 changing operations for accessing data to work with contexts
bulwahn
parents: 37006
diff changeset
   137
        (rev (intros_of ctxt pred)) ()
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   138
    in
37007
116670499530 changing operations for accessing data to work with contexts
bulwahn
parents: 37006
diff changeset
   139
      if (has_elim ctxt pred) then
116670499530 changing operations for accessing data to work with contexts
bulwahn
parents: 37006
diff changeset
   140
        writeln ("elimrule: " ^ Display.string_of_thm ctxt (the_elim_of ctxt pred))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   141
      else
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   142
        writeln ("no elimrule defined")
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   143
    end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   144
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   145
    fold print preds ()
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   146
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   147
37003
a393a588b82e moving towards working with proof contexts in the predicate compiler
bulwahn
parents: 37002
diff changeset
   148
fun print_all_modes compilation ctxt =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   149
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   150
    val _ = writeln ("Inferred modes:")
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   151
    fun print (pred, modes) u =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   152
      let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   153
        val _ = writeln ("predicate: " ^ pred)
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   154
        val _ = writeln ("modes: " ^ (commas (map string_of_mode modes)))
33619
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   155
      in u end
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   156
  in
37003
a393a588b82e moving towards working with proof contexts in the predicate compiler
bulwahn
parents: 37002
diff changeset
   157
    fold print (all_modes_of compilation ctxt) ()
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   158
  end
33129
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   159
33132
07efd452a698 moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents: 33131
diff changeset
   160
(* validity checks *)
07efd452a698 moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents: 33131
diff changeset
   161
40138
432a776c4aee options as first argument to check functions
bulwahn
parents: 40135
diff changeset
   162
fun check_expected_modes options preds modes =
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   163
  case expected_modes options of
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   164
    SOME (s, ms) => (case AList.lookup (op =) modes s of
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   165
      SOME modes =>
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   166
        let
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
   167
          val modes' = map snd modes
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   168
        in
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   169
          if not (eq_set eq_mode (ms, modes')) then
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   170
            error ("expected modes were not inferred:\n"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   171
            ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes')  ^ "\n"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   172
            ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms))
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   173
          else ()
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   174
        end
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   175
      | NONE => ())
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   176
  | NONE => ()
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   177
40138
432a776c4aee options as first argument to check functions
bulwahn
parents: 40135
diff changeset
   178
fun check_proposed_modes options preds modes errors =
39382
c797f3ab2ae1 proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents: 39310
diff changeset
   179
  map (fn (s, _) => case proposed_modes options s of
c797f3ab2ae1 proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents: 39310
diff changeset
   180
    SOME ms => (case AList.lookup (op =) modes s of
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   181
      SOME inferred_ms =>
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   182
        let
39201
234e6ef4ff67 using the proposed modes for starting the fixpoint iteration in the mode analysis
bulwahn
parents: 39194
diff changeset
   183
          val preds_without_modes = map fst (filter (null o snd) modes)
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
   184
          val modes' = map snd inferred_ms
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   185
        in
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   186
          if not (eq_set eq_mode (ms, modes')) then
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   187
            error ("expected modes were not inferred:\n"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   188
            ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes')  ^ "\n"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   189
            ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms) ^ "\n"
39383
ddfafa97da2f adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents: 39382
diff changeset
   190
            ^ (if show_invalid_clauses options then
ddfafa97da2f adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents: 39382
diff changeset
   191
            ("For the following clauses, the following modes could not be inferred: " ^ "\n"
ddfafa97da2f adding option show_invalid_clauses for a more detailed message when modes are not inferred
bulwahn
parents: 39382
diff changeset
   192
            ^ cat_lines errors) else "") ^
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   193
            (if not (null preds_without_modes) then
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   194
              "\n" ^ "No mode inferred for the predicates " ^ commas preds_without_modes
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   195
            else ""))
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   196
          else ()
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   197
        end
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   198
      | NONE => ())
39382
c797f3ab2ae1 proposed modes for code_pred now supports modes for mutual predicates
bulwahn
parents: 39310
diff changeset
   199
  | NONE => ()) preds
33132
07efd452a698 moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents: 33131
diff changeset
   200
39651
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   201
fun check_matches_type ctxt predname T ms =
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   202
  let
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   203
    fun check (m as Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2
39763
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   204
      | check m (T as Type("fun", _)) = (m = Input orelse m = Output)
39651
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   205
      | check (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   206
          check m1 T1 andalso check m2 T2 
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   207
      | check Input T = true
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   208
      | check Output T = true
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   209
      | check Bool @{typ bool} = true
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   210
      | check _ _ = false
39763
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   211
    fun check_consistent_modes ms =
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   212
      if forall (fn Fun (m1', m2') => true | _ => false) ms then
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   213
        pairself check_consistent_modes (split_list (map (fn Fun (m1, m2) => (m1, m2)) ms))
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   214
        |> (fn (res1, res2) => res1 andalso res2) 
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   215
      else if forall (fn Input => true | Output => true | Pair _ => true | _ => false) ms then
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   216
        true
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   217
      else if forall (fn Bool => true | _ => false) ms then
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   218
        true
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   219
      else
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   220
        false
39651
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   221
    val _ = map
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   222
      (fn mode =>
39763
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   223
        if length (strip_fun_mode mode) = length (binder_types T)
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   224
          andalso (forall (uncurry check) (strip_fun_mode mode ~~ binder_types T)) then ()
39651
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   225
        else error (string_of_mode mode ^ " is not a valid mode for " ^ Syntax.string_of_typ ctxt T
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   226
        ^ " at predicate " ^ predname)) ms
39763
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   227
    val _ =
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   228
     if check_consistent_modes ms then ()
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   229
     else error (commas (map string_of_mode ms) ^
03f95582ef63 weakening check for higher-order relations, but adding check for consistent modes
bulwahn
parents: 39762
diff changeset
   230
       " are inconsistent modes for predicate " ^ predname)
39651
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   231
  in
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   232
    ms
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   233
  end
2e06dad03dd3 adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
bulwahn
parents: 39649
diff changeset
   234
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   235
(* compilation modifiers *)
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   236
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   237
structure Comp_Mod =
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   238
struct
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   239
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   240
datatype comp_modifiers = Comp_Modifiers of
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   241
{
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   242
  compilation : compilation,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   243
  function_name_prefix : string,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   244
  compfuns : compilation_funs,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   245
  mk_random : typ -> term list -> term,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   246
  modify_funT : typ -> typ,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   247
  additional_arguments : string list -> term list,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   248
  wrap_compilation : compilation_funs -> string -> typ -> mode -> term list -> term -> term,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   249
  transform_additional_arguments : indprem -> term list -> term list
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   250
}
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   251
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   252
fun dest_comp_modifiers (Comp_Modifiers c) = c
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   253
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   254
val compilation = #compilation o dest_comp_modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   255
val function_name_prefix = #function_name_prefix o dest_comp_modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   256
val compfuns = #compfuns o dest_comp_modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   257
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   258
val mk_random = #mk_random o dest_comp_modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   259
val funT_of' = funT_of o compfuns
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   260
val modify_funT = #modify_funT o dest_comp_modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   261
fun funT_of comp mode = modify_funT comp o funT_of' comp mode
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   262
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   263
val additional_arguments = #additional_arguments o dest_comp_modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   264
val wrap_compilation = #wrap_compilation o dest_comp_modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   265
val transform_additional_arguments = #transform_additional_arguments o dest_comp_modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   266
40049
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   267
fun set_compfuns compfuns' (Comp_Modifiers {compilation, function_name_prefix, compfuns, mk_random,
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   268
    modify_funT, additional_arguments, wrap_compilation, transform_additional_arguments}) =
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   269
    (Comp_Modifiers {compilation = compilation, function_name_prefix = function_name_prefix,
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   270
    compfuns = compfuns', mk_random = mk_random, modify_funT = modify_funT,
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   271
    additional_arguments = additional_arguments, wrap_compilation = wrap_compilation,
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   272
    transform_additional_arguments = transform_additional_arguments})
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   273
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   274
end;
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   275
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   276
fun unlimited_compfuns_of true New_Pos_Random_DSeq =
40049
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   277
    New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   278
  | unlimited_compfuns_of false New_Pos_Random_DSeq =
40049
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   279
    New_Neg_Random_Sequence_CompFuns.depth_unlimited_compfuns
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   280
  | unlimited_compfuns_of true Pos_Generator_DSeq =
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   281
    New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   282
  | unlimited_compfuns_of false Pos_Generator_DSeq =
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   283
    New_Neg_DSequence_CompFuns.depth_unlimited_compfuns
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   284
  | unlimited_compfuns_of _ c =
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   285
    raise Fail ("No unlimited compfuns for compilation " ^ string_of_compilation c)
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   286
40049
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   287
fun limited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq =
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   288
    New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   289
  | limited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq =
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   290
    New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   291
  | limited_compfuns_of true Pos_Generator_DSeq =
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   292
    New_Pos_DSequence_CompFuns.depth_limited_compfuns
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   293
  | limited_compfuns_of false Pos_Generator_DSeq =
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   294
    New_Neg_DSequence_CompFuns.depth_limited_compfuns
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   295
  | limited_compfuns_of _ c =
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   296
    raise Fail ("No limited compfuns for compilation " ^ string_of_compilation c)
40049
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   297
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   298
val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   299
  {
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   300
  compilation = Depth_Limited,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   301
  function_name_prefix = "depth_limited_",
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   302
  compfuns = Predicate_Comp_Funs.compfuns,
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   303
  mk_random = (fn _ => error "no random generation"),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   304
  additional_arguments = fn names =>
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   305
    let
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 43253
diff changeset
   306
      val depth_name = singleton (Name.variant_list names) "depth"
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   307
    in [Free (depth_name, @{typ code_numeral})] end,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   308
  modify_funT = (fn T => let val (Ts, U) = strip_type T
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   309
  val Ts' = [@{typ code_numeral}] in (Ts @ Ts') ---> U end),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   310
  wrap_compilation =
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   311
    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   312
    let
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   313
      val [depth] = additional_arguments
40139
6a53d57fa902 renaming split_modeT' to split_modeT
bulwahn
parents: 40138
diff changeset
   314
      val (_, Ts) = split_modeT mode (binder_types T)
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   315
      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   316
      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   317
    in
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   318
      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   319
        $ mk_bot compfuns (dest_predT compfuns T')
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   320
        $ compilation
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   321
    end,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   322
  transform_additional_arguments =
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   323
    fn prem => fn additional_arguments =>
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   324
    let
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   325
      val [depth] = additional_arguments
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   326
      val depth' =
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   327
        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   328
          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   329
    in [depth'] end
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   330
  }
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   331
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   332
val random_comp_modifiers = Comp_Mod.Comp_Modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   333
  {
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   334
  compilation = Random,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   335
  function_name_prefix = "random_",
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   336
  compfuns = Predicate_Comp_Funs.compfuns,
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   337
  mk_random = (fn T => fn additional_arguments =>
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   338
  list_comb (Const(@{const_name Quickcheck.iter},
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   339
  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   340
    Predicate_Comp_Funs.mk_predT T), additional_arguments)),
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   341
  modify_funT = (fn T =>
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   342
    let
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   343
      val (Ts, U) = strip_type T
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   344
      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ "code_numeral * code_numeral"}]
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   345
    in (Ts @ Ts') ---> U end),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   346
  additional_arguments = (fn names =>
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   347
    let
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   348
      val [nrandom, size, seed] = Name.variant_list names ["nrandom", "size", "seed"]
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   349
    in
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   350
      [Free (nrandom, @{typ code_numeral}), Free (size, @{typ code_numeral}),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   351
        Free (seed, @{typ "code_numeral * code_numeral"})]
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   352
    end),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   353
  wrap_compilation = K (K (K (K (K I))))
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   354
    : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   355
  transform_additional_arguments = K I : (indprem -> term list -> term list)
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   356
  }
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   357
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   358
val depth_limited_random_comp_modifiers = Comp_Mod.Comp_Modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   359
  {
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   360
  compilation = Depth_Limited_Random,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   361
  function_name_prefix = "depth_limited_random_",
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   362
  compfuns = Predicate_Comp_Funs.compfuns,
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   363
  mk_random = (fn T => fn additional_arguments =>
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   364
  list_comb (Const(@{const_name Quickcheck.iter},
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   365
  [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   366
    Predicate_Comp_Funs.mk_predT T), tl additional_arguments)),
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   367
  modify_funT = (fn T =>
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   368
    let
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   369
      val (Ts, U) = strip_type T
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   370
      val Ts' = [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   371
        @{typ "code_numeral * code_numeral"}]
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   372
    in (Ts @ Ts') ---> U end),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   373
  additional_arguments = (fn names =>
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   374
    let
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   375
      val [depth, nrandom, size, seed] = Name.variant_list names ["depth", "nrandom", "size", "seed"]
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   376
    in
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   377
      [Free (depth, @{typ code_numeral}), Free (nrandom, @{typ code_numeral}),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   378
        Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   379
    end),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   380
  wrap_compilation =
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   381
  fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   382
    let
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   383
      val depth = hd (additional_arguments)
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   384
      val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE))
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   385
        mode (binder_types T)
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   386
      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   387
      val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   388
    in
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   389
      if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   390
        $ mk_bot compfuns (dest_predT compfuns T')
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   391
        $ compilation
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   392
    end,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   393
  transform_additional_arguments =
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   394
    fn prem => fn additional_arguments =>
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   395
    let
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   396
      val [depth, nrandom, size, seed] = additional_arguments
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   397
      val depth' =
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   398
        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   399
          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   400
    in [depth', nrandom, size, seed] end
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   401
}
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   402
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   403
val predicate_comp_modifiers = Comp_Mod.Comp_Modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   404
  {
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   405
  compilation = Pred,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   406
  function_name_prefix = "",
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   407
  compfuns = Predicate_Comp_Funs.compfuns,
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   408
  mk_random = (fn _ => error "no random generation"),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   409
  modify_funT = I,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   410
  additional_arguments = K [],
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   411
  wrap_compilation = K (K (K (K (K I))))
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   412
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   413
  transform_additional_arguments = K I : (indprem -> term list -> term list)
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   414
  }
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   415
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   416
val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   417
  {
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   418
  compilation = Annotated,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   419
  function_name_prefix = "annotated_",
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   420
  compfuns = Predicate_Comp_Funs.compfuns,
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   421
  mk_random = (fn _ => error "no random generation"),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   422
  modify_funT = I,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   423
  additional_arguments = K [],
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   424
  wrap_compilation =
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   425
    fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   426
      mk_tracing ("calling predicate " ^ s ^
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   427
        " with mode " ^ string_of_mode mode) compilation,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   428
  transform_additional_arguments = K I : (indprem -> term list -> term list)
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   429
  }
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   430
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   431
val dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   432
  {
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   433
  compilation = DSeq,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   434
  function_name_prefix = "dseq_",
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   435
  compfuns = DSequence_CompFuns.compfuns,
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   436
  mk_random = (fn _ => error "no random generation in dseq"),
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   437
  modify_funT = I,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   438
  additional_arguments = K [],
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   439
  wrap_compilation = K (K (K (K (K I))))
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   440
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   441
  transform_additional_arguments = K I : (indprem -> term list -> term list)
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   442
  }
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   443
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   444
val pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   445
  {
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   446
  compilation = Pos_Random_DSeq,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   447
  function_name_prefix = "random_dseq_",
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   448
  compfuns = Random_Sequence_CompFuns.compfuns,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   449
  mk_random = (fn T => fn additional_arguments =>
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   450
  let
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   451
    val random = Const ("Quickcheck.random_class.random",
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   452
      @{typ code_numeral} --> @{typ Random.seed} -->
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   453
        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   454
  in
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   455
    Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   456
      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   457
      Random_Sequence_CompFuns.mk_random_dseqT T) $ random
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   458
  end),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   459
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   460
  modify_funT = I,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   461
  additional_arguments = K [],
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   462
  wrap_compilation = K (K (K (K (K I))))
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   463
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   464
  transform_additional_arguments = K I : (indprem -> term list -> term list)
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   465
  }
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   466
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   467
val neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   468
  {
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   469
  compilation = Neg_Random_DSeq,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   470
  function_name_prefix = "random_dseq_neg_",
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   471
  compfuns = Random_Sequence_CompFuns.compfuns,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   472
  mk_random = (fn _ => error "no random generation"),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   473
  modify_funT = I,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   474
  additional_arguments = K [],
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   475
  wrap_compilation = K (K (K (K (K I))))
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   476
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   477
  transform_additional_arguments = K I : (indprem -> term list -> term list)
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   478
  }
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   479
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   480
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   481
val new_pos_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   482
  {
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   483
  compilation = New_Pos_Random_DSeq,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   484
  function_name_prefix = "new_random_dseq_",
40049
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   485
  compfuns = New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns,
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   486
  mk_random = (fn T => fn additional_arguments =>
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   487
  let
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   488
    val random = Const ("Quickcheck.random_class.random",
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   489
      @{typ code_numeral} --> @{typ Random.seed} -->
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   490
        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   491
  in
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   492
    Const ("New_Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   493
      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   494
      New_Pos_Random_Sequence_CompFuns.mk_pos_random_dseqT T) $ random
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   495
  end),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   496
  modify_funT = I,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   497
  additional_arguments = K [],
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   498
  wrap_compilation = K (K (K (K (K I))))
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   499
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   500
  transform_additional_arguments = K I : (indprem -> term list -> term list)
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   501
  }
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   502
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   503
val new_neg_random_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   504
  {
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   505
  compilation = New_Neg_Random_DSeq,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   506
  function_name_prefix = "new_random_dseq_neg_",
40049
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   507
  compfuns = New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns,
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   508
  mk_random = (fn _ => error "no random generation"),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   509
  modify_funT = I,
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   510
  additional_arguments = K [],
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   511
  wrap_compilation = K (K (K (K (K I))))
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   512
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   513
  transform_additional_arguments = K I : (indprem -> term list -> term list)
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   514
  }
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   515
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   516
val pos_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   517
  {
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   518
  compilation = Pos_Generator_DSeq,
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   519
  function_name_prefix = "generator_dseq_",
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   520
  compfuns = New_Pos_DSequence_CompFuns.depth_limited_compfuns,
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   521
  mk_random =
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   522
    (fn T => fn additional_arguments =>
45214
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   523
      Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"},
66ba67adafab modernizing predicate_compile_quickcheck
bulwahn
parents: 44241
diff changeset
   524
        @{typ "Code_Numeral.code_numeral"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T]))),
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   525
  modify_funT = I,
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   526
  additional_arguments = K [],
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   527
  wrap_compilation = K (K (K (K (K I))))
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   528
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   529
  transform_additional_arguments = K I : (indprem -> term list -> term list)
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   530
  }
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   531
  
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   532
val neg_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   533
  {
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   534
  compilation = Neg_Generator_DSeq,
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   535
  function_name_prefix = "generator_dseq_neg_",
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   536
  compfuns = New_Neg_DSequence_CompFuns.depth_limited_compfuns,
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   537
  mk_random = (fn _ => error "no random generation"),
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   538
  modify_funT = I,
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   539
  additional_arguments = K [],
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   540
  wrap_compilation = K (K (K (K (K I))))
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   541
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   542
  transform_additional_arguments = K I : (indprem -> term list -> term list)
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   543
  }
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   544
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   545
val pos_generator_cps_comp_modifiers = Comp_Mod.Comp_Modifiers
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   546
  {
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   547
  compilation = Pos_Generator_CPS,
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   548
  function_name_prefix = "generator_cps_pos_",
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   549
  compfuns = Pos_Bounded_CPS_Comp_Funs.compfuns,
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   550
  mk_random =
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   551
    (fn T => fn additional_arguments =>
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   552
       Const (@{const_name "Quickcheck_Exhaustive.exhaustive"},
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   553
       (T --> @{typ "term list option"}) --> @{typ "code_numeral => term list option"})),
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   554
  modify_funT = I,
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   555
  additional_arguments = K [],
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   556
  wrap_compilation = K (K (K (K (K I))))
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   557
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   558
  transform_additional_arguments = K I : (indprem -> term list -> term list)
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   559
  }  
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   560
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   561
val neg_generator_cps_comp_modifiers = Comp_Mod.Comp_Modifiers
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   562
  {
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   563
  compilation = Neg_Generator_CPS,
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   564
  function_name_prefix = "generator_cps_neg_",
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   565
  compfuns = Neg_Bounded_CPS_Comp_Funs.compfuns,
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   566
  mk_random = (fn _ => error "No enumerators"),
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   567
  modify_funT = I,
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   568
  additional_arguments = K [],
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   569
  wrap_compilation = K (K (K (K (K I))))
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   570
   : (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   571
  transform_additional_arguments = K I : (indprem -> term list -> term list)
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   572
  }
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   573
  
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   574
fun negative_comp_modifiers_of comp_modifiers =
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   575
    (case Comp_Mod.compilation comp_modifiers of
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   576
      Pos_Random_DSeq => neg_random_dseq_comp_modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   577
    | Neg_Random_DSeq => pos_random_dseq_comp_modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   578
    | New_Pos_Random_DSeq => new_neg_random_dseq_comp_modifiers
40051
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   579
    | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers 
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   580
    | Pos_Generator_DSeq => neg_generator_dseq_comp_modifiers
b6acda4d1c29 added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents: 40050
diff changeset
   581
    | Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   582
    | Pos_Generator_CPS => neg_generator_cps_comp_modifiers
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   583
    | Neg_Generator_CPS => pos_generator_cps_comp_modifiers
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   584
    | c => comp_modifiers)
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   585
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   586
(* term construction *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   587
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   588
fun mk_v (names, vs) s T = (case AList.lookup (op =) vs s of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   589
      NONE => (Free (s, T), (names, (s, [])::vs))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   590
    | SOME xs =>
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   591
        let
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 43253
diff changeset
   592
          val s' = singleton (Name.variant_list names) s;
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   593
          val v = Free (s', T)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   594
        in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   595
          (v, (s'::names, AList.update (op =) (s, v::xs) vs))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   596
        end);
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   597
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   598
fun distinct_v (Free (s, T)) nvs = mk_v nvs s T
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   599
  | distinct_v (t $ u) nvs =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   600
      let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   601
        val (t', nvs') = distinct_v t nvs;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   602
        val (u', nvs'') = distinct_v u nvs';
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   603
      in (t' $ u', nvs'') end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   604
  | distinct_v x nvs = (x, nvs);
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   605
33147
180dc60bd88c improving the compilation with higher-order arguments in the predicate compiler
bulwahn
parents: 33146
diff changeset
   606
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   607
(** specific rpred functions -- move them to the correct place in this file *)
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   608
fun mk_Eval_of (P as (Free (f, _)), T) mode =
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   609
  let
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   610
    fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i =
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   611
          let
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   612
            val (bs2, i') = mk_bounds T2 i 
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   613
            val (bs1, i'') = mk_bounds T1 i'
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   614
          in
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   615
            (HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1)
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   616
          end
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   617
      | mk_bounds T i = (Bound i, i + 1)
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   618
    fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2))
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   619
    fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT)
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   620
      | mk_tuple tTs = foldr1 mk_prod tTs
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   621
    fun mk_split_abs (T as Type (@{type_name Product_Type.prod}, [T1, T2])) t =
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   622
          absdummy T
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   623
            (HOLogic.split_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t)))
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   624
      | mk_split_abs T t = absdummy T t
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   625
    val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   626
    val (inargs, outargs) = split_mode mode args
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   627
    val (inTs, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
   628
    val inner_term = Predicate_Comp_Funs.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   629
  in
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   630
    fold_rev mk_split_abs (binder_types T) inner_term
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43948
diff changeset
   631
  end
33147
180dc60bd88c improving the compilation with higher-order arguments in the predicate compiler
bulwahn
parents: 33146
diff changeset
   632
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   633
fun compile_arg compilation_modifiers additional_arguments ctxt param_modes arg = 
33147
180dc60bd88c improving the compilation with higher-order arguments in the predicate compiler
bulwahn
parents: 33146
diff changeset
   634
  let
180dc60bd88c improving the compilation with higher-order arguments in the predicate compiler
bulwahn
parents: 33146
diff changeset
   635
    fun map_params (t as Free (f, T)) =
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   636
      (case (AList.lookup (op =) param_modes f) of
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   637
          SOME mode =>
33147
180dc60bd88c improving the compilation with higher-order arguments in the predicate compiler
bulwahn
parents: 33146
diff changeset
   638
            let
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   639
              val T' = Comp_Mod.funT_of compilation_modifiers mode T
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   640
            in
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   641
              mk_Eval_of (Free (f, T'), T) mode
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   642
            end
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   643
        | NONE => t)
33147
180dc60bd88c improving the compilation with higher-order arguments in the predicate compiler
bulwahn
parents: 33146
diff changeset
   644
      | map_params t = t
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   645
  in
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   646
    map_aterms map_params arg
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   647
  end
33147
180dc60bd88c improving the compilation with higher-order arguments in the predicate compiler
bulwahn
parents: 33146
diff changeset
   648
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   649
fun compile_match compilation_modifiers additional_arguments ctxt param_modes
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   650
      eqs eqs' out_ts success_t =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   651
  let
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   652
    val compfuns = Comp_Mod.compfuns compilation_modifiers
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   653
    val eqs'' = maps mk_eq eqs @ eqs'
33147
180dc60bd88c improving the compilation with higher-order arguments in the predicate compiler
bulwahn
parents: 33146
diff changeset
   654
    val eqs'' =
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   655
      map (compile_arg compilation_modifiers additional_arguments ctxt param_modes) eqs''
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   656
    val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 43253
diff changeset
   657
    val name = singleton (Name.variant_list names) "x";
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 43253
diff changeset
   658
    val name' = singleton (Name.variant_list (name :: names)) "y";
33148
0808f7d0d0d7 removed tuple functions from the predicate compiler
bulwahn
parents: 33147
diff changeset
   659
    val T = HOLogic.mk_tupleT (map fastype_of out_ts);
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   660
    val U = fastype_of success_t;
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   661
    val U' = dest_predT compfuns U;
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   662
    val v = Free (name, T);
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   663
    val v' = Free (name', T);
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   664
  in
43253
fa3c61dc9f2c removed generation of instantiated pattern set, which is never actually used
krauss
parents: 43123
diff changeset
   665
    lambda v (Datatype.make_case ctxt Datatype_Case.Quiet [] v
33148
0808f7d0d0d7 removed tuple functions from the predicate compiler
bulwahn
parents: 33147
diff changeset
   666
      [(HOLogic.mk_tuple out_ts,
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   667
        if null eqs'' then success_t
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   668
        else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   669
          foldr1 HOLogic.mk_conj eqs'' $ success_t $
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   670
            mk_bot compfuns U'),
43253
fa3c61dc9f2c removed generation of instantiated pattern set, which is never actually used
krauss
parents: 43123
diff changeset
   671
       (v', mk_bot compfuns U')])
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   672
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   673
35891
3122bdd95275 contextifying the compilation of the predicate compiler
bulwahn
parents: 35889
diff changeset
   674
fun string_of_tderiv ctxt (t, deriv) = 
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
   675
  (case (t, deriv) of
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
   676
    (t1 $ t2, Mode_App (deriv1, deriv2)) =>
35891
3122bdd95275 contextifying the compilation of the predicate compiler
bulwahn
parents: 35889
diff changeset
   677
      string_of_tderiv ctxt (t1, deriv1) ^ " $ " ^ string_of_tderiv ctxt (t2, deriv2)
37391
476270a6c2dc tuned quotes, antiquotations and whitespace
haftmann
parents: 37146
diff changeset
   678
  | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (deriv1, deriv2)) =>
35891
3122bdd95275 contextifying the compilation of the predicate compiler
bulwahn
parents: 35889
diff changeset
   679
    "(" ^ string_of_tderiv ctxt (t1, deriv1) ^ ", " ^ string_of_tderiv ctxt (t2, deriv2) ^ ")"
3122bdd95275 contextifying the compilation of the predicate compiler
bulwahn
parents: 35889
diff changeset
   680
  | (t, Term Input) => Syntax.string_of_term ctxt t ^ "[Input]"
3122bdd95275 contextifying the compilation of the predicate compiler
bulwahn
parents: 35889
diff changeset
   681
  | (t, Term Output) => Syntax.string_of_term ctxt t ^ "[Output]"
3122bdd95275 contextifying the compilation of the predicate compiler
bulwahn
parents: 35889
diff changeset
   682
  | (t, Context m) => Syntax.string_of_term ctxt t ^ "[" ^ string_of_mode m ^ "]")
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
   683
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   684
fun compile_expr compilation_modifiers ctxt (t, deriv) param_modes additional_arguments =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   685
  let
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   686
    val compfuns = Comp_Mod.compfuns compilation_modifiers
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   687
    fun expr_of (t, deriv) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   688
      (case (t, deriv) of
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   689
        (t, Term Input) => SOME (compile_arg compilation_modifiers additional_arguments ctxt param_modes t)
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   690
      | (t, Term Output) => NONE
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   691
      | (Const (name, T), Context mode) =>
37003
a393a588b82e moving towards working with proof contexts in the predicate compiler
bulwahn
parents: 37002
diff changeset
   692
        (case alternative_compilation_of ctxt name mode of
36038
385f706eff24 generalized alternative functions to alternative compilation to handle arithmetic functions better
bulwahn
parents: 36037
diff changeset
   693
          SOME alt_comp => SOME (alt_comp compfuns T)
36034
ee84eac07290 added book-keeping, registration and compilation with alternative functions for predicates in the predicate compiler
bulwahn
parents: 36031
diff changeset
   694
        | NONE =>
ee84eac07290 added book-keeping, registration and compilation with alternative functions for predicates in the predicate compiler
bulwahn
parents: 36031
diff changeset
   695
          SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
37003
a393a588b82e moving towards working with proof contexts in the predicate compiler
bulwahn
parents: 37002
diff changeset
   696
            ctxt name mode,
36034
ee84eac07290 added book-keeping, registration and compilation with alternative functions for predicates in the predicate compiler
bulwahn
parents: 36031
diff changeset
   697
            Comp_Mod.funT_of compilation_modifiers mode T)))
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   698
      | (Free (s, T), Context m) =>
39785
05c4e9ecf5f6 improving the compilation to handle predicate arguments in higher-order argument positions
bulwahn
parents: 39783
diff changeset
   699
        (case (AList.lookup (op =) param_modes s) of
05c4e9ecf5f6 improving the compilation to handle predicate arguments in higher-order argument positions
bulwahn
parents: 39783
diff changeset
   700
          SOME mode => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
05c4e9ecf5f6 improving the compilation to handle predicate arguments in higher-order argument positions
bulwahn
parents: 39783
diff changeset
   701
        | NONE =>
05c4e9ecf5f6 improving the compilation to handle predicate arguments in higher-order argument positions
bulwahn
parents: 39783
diff changeset
   702
        let
05c4e9ecf5f6 improving the compilation to handle predicate arguments in higher-order argument positions
bulwahn
parents: 39783
diff changeset
   703
          val bs = map (pair "x") (binder_types (fastype_of t))
05c4e9ecf5f6 improving the compilation to handle predicate arguments in higher-order argument positions
bulwahn
parents: 39783
diff changeset
   704
          val bounds = map Bound (rev (0 upto (length bs) - 1))
05c4e9ecf5f6 improving the compilation to handle predicate arguments in higher-order argument positions
bulwahn
parents: 39783
diff changeset
   705
        in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end)
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   706
      | (t, Context m) =>
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   707
        let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   708
          val bs = map (pair "x") (binder_types (fastype_of t))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   709
          val bounds = map Bound (rev (0 upto (length bs) - 1))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   710
        in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end
37391
476270a6c2dc tuned quotes, antiquotations and whitespace
haftmann
parents: 37146
diff changeset
   711
      | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   712
        (case (expr_of (t1, d1), expr_of (t2, d2)) of
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   713
          (NONE, NONE) => NONE
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   714
        | (NONE, SOME t) => SOME t
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   715
        | (SOME t, NONE) => SOME t
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   716
        | (SOME t1, SOME t2) => SOME (HOLogic.mk_prod (t1, t2)))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   717
      | (t1 $ t2, Mode_App (deriv1, deriv2)) =>
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   718
        (case (expr_of (t1, deriv1), expr_of (t2, deriv2)) of
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   719
          (SOME t, NONE) => SOME t
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   720
         | (SOME t, SOME u) => SOME (t $ u)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   721
         | _ => error "something went wrong here!"))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   722
  in
35879
99818df5b8f5 reviving the classical depth-limited computation in the predicate compiler
bulwahn
parents: 35845
diff changeset
   723
    list_comb (the (expr_of (t, deriv)), additional_arguments)
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   724
  end
33145
1a22f7ca1dfc removed dead code; added examples
bulwahn
parents: 33144
diff changeset
   725
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   726
fun compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   727
  inp (in_ts, out_ts) moded_ps =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   728
  let
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   729
    val compfuns = Comp_Mod.compfuns compilation_modifiers
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   730
    val compile_match = compile_match compilation_modifiers
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   731
      additional_arguments ctxt param_modes
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   732
    val (in_ts', (all_vs', eqs)) =
35891
3122bdd95275 contextifying the compilation of the predicate compiler
bulwahn
parents: 35889
diff changeset
   733
      fold_map (collect_non_invertible_subterms ctxt) in_ts (all_vs, []);
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   734
    fun compile_prems out_ts' vs names [] =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   735
          let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   736
            val (out_ts'', (names', eqs')) =
35891
3122bdd95275 contextifying the compilation of the predicate compiler
bulwahn
parents: 35889
diff changeset
   737
              fold_map (collect_non_invertible_subterms ctxt) out_ts' (names, []);
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   738
            val (out_ts''', (names'', constr_vs)) = fold_map distinct_v
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   739
              out_ts'' (names', map (rpair []) vs);
39762
02fb709ab3cb handling higher-order relations in output terms; improving proof procedure; added test case
bulwahn
parents: 39761
diff changeset
   740
            val processed_out_ts = map (compile_arg compilation_modifiers additional_arguments
02fb709ab3cb handling higher-order relations in output terms; improving proof procedure; added test case
bulwahn
parents: 39761
diff changeset
   741
              ctxt param_modes) out_ts
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   742
          in
33147
180dc60bd88c improving the compilation with higher-order arguments in the predicate compiler
bulwahn
parents: 33146
diff changeset
   743
            compile_match constr_vs (eqs @ eqs') out_ts'''
39762
02fb709ab3cb handling higher-order relations in output terms; improving proof procedure; added test case
bulwahn
parents: 39761
diff changeset
   744
              (mk_single compfuns (HOLogic.mk_tuple processed_out_ts))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   745
          end
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   746
      | compile_prems out_ts vs names ((p, deriv) :: ps) =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   747
          let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   748
            val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   749
            val (out_ts', (names', eqs)) =
35891
3122bdd95275 contextifying the compilation of the predicate compiler
bulwahn
parents: 35889
diff changeset
   750
              fold_map (collect_non_invertible_subterms ctxt) out_ts (names, [])
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   751
            val (out_ts'', (names'', constr_vs')) = fold_map distinct_v
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   752
              out_ts' ((names', map (rpair []) vs))
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   753
            val mode = head_mode_of deriv
33143
730a2e8a6ec6 modularized the compilation in the predicate compiler
bulwahn
parents: 33141
diff changeset
   754
            val additional_arguments' =
33330
d6eb7f19bfc6 encapsulating records with datatype constructors and adding type annotations to make SML/NJ happy
bulwahn
parents: 33328
diff changeset
   755
              Comp_Mod.transform_additional_arguments compilation_modifiers p additional_arguments
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   756
            val (compiled_clause, rest) = case p of
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   757
               Prem t =>
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   758
                 let
33138
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   759
                   val u =
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   760
                     compile_expr compilation_modifiers ctxt (t, deriv) param_modes additional_arguments'
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   761
                   val (_, out_ts''') = split_mode mode (snd (strip_comb t))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   762
                   val rest = compile_prems out_ts''' vs' names'' ps
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   763
                 in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   764
                   (u, rest)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   765
                 end
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   766
             | Negprem t =>
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   767
                 let
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   768
                   val neg_compilation_modifiers =
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   769
                     negative_comp_modifiers_of compilation_modifiers
33143
730a2e8a6ec6 modularized the compilation in the predicate compiler
bulwahn
parents: 33141
diff changeset
   770
                   val u = mk_not compfuns
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   771
                     (compile_expr neg_compilation_modifiers ctxt (t, deriv) param_modes additional_arguments')
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   772
                   val (_, out_ts''') = split_mode mode (snd (strip_comb t))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   773
                   val rest = compile_prems out_ts''' vs' names'' ps
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   774
                 in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   775
                   (u, rest)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   776
                 end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   777
             | Sidecond t =>
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   778
                 let
36019
64bbbd858c39 generalizing the compilation process of the predicate compiler
bulwahn
parents: 36018
diff changeset
   779
                   val t = compile_arg compilation_modifiers additional_arguments
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   780
                     ctxt param_modes t
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   781
                   val rest = compile_prems [] vs' names'' ps;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   782
                 in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   783
                   (mk_if compfuns t, rest)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   784
                 end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   785
             | Generator (v, T) =>
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   786
                 let
35880
2623b23e41fc a new simpler random compilation for the predicate compiler
bulwahn
parents: 35879
diff changeset
   787
                   val u = Comp_Mod.mk_random compilation_modifiers T additional_arguments
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   788
                   val rest = compile_prems [Free (v, T)]  vs' names'' ps;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   789
                 in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   790
                   (u, rest)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   791
                 end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   792
          in
33147
180dc60bd88c improving the compilation with higher-order arguments in the predicate compiler
bulwahn
parents: 33146
diff changeset
   793
            compile_match constr_vs' eqs out_ts''
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   794
              (mk_bind compfuns (compiled_clause, rest))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   795
          end
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   796
    val prem_t = compile_prems in_ts' (map fst param_modes) all_vs' moded_ps;
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   797
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   798
    mk_bind compfuns (mk_single compfuns inp, prem_t)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   799
  end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   800
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   801
(* switch detection *)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   802
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   803
(** argument position of an inductive predicates and the executable functions **)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   804
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   805
type position = int * int list
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   806
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   807
fun input_positions_pair Input = [[]]
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   808
  | input_positions_pair Output = []
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   809
  | input_positions_pair (Fun _) = []
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   810
  | input_positions_pair (Pair (m1, m2)) =
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   811
    map (cons 1) (input_positions_pair m1) @ map (cons 2) (input_positions_pair m2)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   812
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   813
fun input_positions_of_mode mode = flat (map_index
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   814
   (fn (i, Input) => [(i, [])]
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   815
   | (_, Output) => []
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   816
   | (_, Fun _) => []
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   817
   | (i, m as Pair (m1, m2)) => map (pair i) (input_positions_pair m))
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   818
     (Predicate_Compile_Aux.strip_fun_mode mode))
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   819
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   820
fun argument_position_pair mode [] = []
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   821
  | argument_position_pair (Pair (Fun _, m2)) (2 :: is) = argument_position_pair m2 is
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   822
  | argument_position_pair (Pair (m1, m2)) (i :: is) =
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   823
    (if eq_mode (m1, Output) andalso i = 2 then
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   824
      argument_position_pair m2 is
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   825
    else if eq_mode (m2, Output) andalso i = 1 then
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   826
      argument_position_pair m1 is
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   827
    else (i :: argument_position_pair (if i = 1 then m1 else m2) is))
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   828
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   829
fun argument_position_of mode (i, is) =
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   830
  (i - (length (filter (fn Output => true | Fun _ => true | _ => false)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   831
    (List.take (strip_fun_mode mode, i)))),
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   832
  argument_position_pair (nth (strip_fun_mode mode) i) is)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   833
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   834
fun nth_pair [] t = t
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   835
  | nth_pair (1 :: is) (Const (@{const_name Pair}, _) $ t1 $ _) = nth_pair is t1
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   836
  | nth_pair (2 :: is) (Const (@{const_name Pair}, _) $ _ $ t2) = nth_pair is t2
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   837
  | nth_pair _ _ = raise Fail "unexpected input for nth_tuple"
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   838
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   839
(** switch detection analysis **)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   840
37005
842a73dc6d0e changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents: 37004
diff changeset
   841
fun find_switch_test ctxt (i, is) (ts, prems) =
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   842
  let
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   843
    val t = nth_pair is (nth ts i)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   844
    val T = fastype_of t
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   845
  in
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   846
    case T of
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   847
      TFree _ => NONE
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   848
    | Type (Tcon, _) =>
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42141
diff changeset
   849
      (case Datatype_Data.get_constrs (Proof_Context.theory_of ctxt) Tcon of
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   850
        NONE => NONE
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   851
      | SOME cs =>
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   852
        (case strip_comb t of
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   853
          (Var _, []) => NONE
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   854
        | (Free _, []) => NONE
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   855
        | (Const (c, T), _) => if AList.defined (op =) cs c then SOME (c, T) else NONE))
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   856
  end
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   857
37005
842a73dc6d0e changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents: 37004
diff changeset
   858
fun partition_clause ctxt pos moded_clauses =
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   859
  let
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   860
    fun insert_list eq (key, value) = AList.map_default eq (key, []) (cons value)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   861
    fun find_switch_test' moded_clause (cases, left) =
37005
842a73dc6d0e changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents: 37004
diff changeset
   862
      case find_switch_test ctxt pos moded_clause of
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   863
        SOME (c, T) => (insert_list (op =) ((c, T), moded_clause) cases, left)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   864
      | NONE => (cases, moded_clause :: left)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   865
  in
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   866
    fold find_switch_test' moded_clauses ([], [])
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   867
  end
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   868
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   869
datatype switch_tree =
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   870
  Atom of moded_clause list | Node of (position * ((string * typ) * switch_tree) list) * switch_tree
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   871
37005
842a73dc6d0e changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents: 37004
diff changeset
   872
fun mk_switch_tree ctxt mode moded_clauses =
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   873
  let
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   874
    fun select_best_switch moded_clauses input_position best_switch =
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   875
      let
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   876
        val ord = option_ord (rev_order o int_ord o (pairself (length o snd o snd)))
37005
842a73dc6d0e changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents: 37004
diff changeset
   877
        val partition = partition_clause ctxt input_position moded_clauses
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   878
        val switch = if (length (fst partition) > 1) then SOME (input_position, partition) else NONE
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   879
      in
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   880
        case ord (switch, best_switch) of LESS => best_switch
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   881
          | EQUAL => best_switch | GREATER => switch
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   882
      end
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   883
    fun detect_switches moded_clauses =
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   884
      case fold (select_best_switch moded_clauses) (input_positions_of_mode mode) NONE of
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   885
        SOME (best_pos, (switched_on, left_clauses)) =>
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   886
          Node ((best_pos, map (apsnd detect_switches) switched_on),
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   887
            detect_switches left_clauses)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   888
      | NONE => Atom moded_clauses
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   889
  in
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   890
    detect_switches moded_clauses
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   891
  end
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   892
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   893
(** compilation of detected switches **)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   894
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   895
fun destruct_constructor_pattern (pat, obj) =
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   896
  (case strip_comb pat of
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   897
    (f as Free _, []) => cons (pat, obj)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   898
  | (Const (c, T), pat_args) =>
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   899
    (case strip_comb obj of
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   900
      (Const (c', T'), obj_args) =>
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   901
        (if c = c' andalso T = T' then
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   902
          fold destruct_constructor_pattern (pat_args ~~ obj_args)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   903
        else raise Fail "pattern and object mismatch")
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   904
    | _ => raise Fail "unexpected object")
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   905
  | _ => raise Fail "unexpected pattern")
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   906
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   907
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   908
fun compile_switch compilation_modifiers ctxt all_vs param_modes additional_arguments mode
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   909
  in_ts' outTs switch_tree =
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   910
  let
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   911
    val compfuns = Comp_Mod.compfuns compilation_modifiers
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42141
diff changeset
   912
    val thy = Proof_Context.theory_of ctxt
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   913
    fun compile_switch_tree _ _ (Atom []) = NONE
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   914
      | compile_switch_tree all_vs ctxt_eqs (Atom moded_clauses) =
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   915
        let
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   916
          val in_ts' = map (Pattern.rewrite_term thy ctxt_eqs []) in_ts'
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   917
          fun compile_clause' (ts, moded_ps) =
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   918
            let
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   919
              val (ts, out_ts) = split_mode mode ts
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   920
              val subst = fold destruct_constructor_pattern (in_ts' ~~ ts) []
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   921
              val (fsubst, pat') = List.partition (fn (_, Free _) => true | _ => false) subst
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   922
              val moded_ps' = (map o apfst o map_indprem)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   923
                (Pattern.rewrite_term thy (map swap fsubst) []) moded_ps
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   924
              val inp = HOLogic.mk_tuple (map fst pat')
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   925
              val in_ts' = map (Pattern.rewrite_term thy (map swap fsubst) []) (map snd pat')
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   926
              val out_ts' = map (Pattern.rewrite_term thy (map swap fsubst) []) out_ts
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   927
            in
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   928
              compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   929
                inp (in_ts', out_ts') moded_ps'
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   930
            end
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   931
        in SOME (foldr1 (mk_sup compfuns) (map compile_clause' moded_clauses)) end
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   932
    | compile_switch_tree all_vs ctxt_eqs (Node ((position, switched_clauses), left_clauses)) =
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   933
      let
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   934
        val (i, is) = argument_position_of mode position
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   935
        val inp_var = nth_pair is (nth in_ts' i)
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 43253
diff changeset
   936
        val x = singleton (Name.variant_list all_vs) "x"
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   937
        val xt = Free (x, fastype_of inp_var)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   938
        fun compile_single_case ((c, T), switched) =
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   939
          let
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   940
            val Ts = binder_types T
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   941
            val argnames = Name.variant_list (x :: all_vs)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   942
              (map (fn i => "c" ^ string_of_int i) (1 upto length Ts))
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   943
            val args = map2 (curry Free) argnames Ts
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   944
            val pattern = list_comb (Const (c, T), args)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   945
            val ctxt_eqs' = (inp_var, pattern) :: ctxt_eqs
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   946
            val compilation = the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs))
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   947
              (compile_switch_tree (argnames @ x :: all_vs) ctxt_eqs' switched)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   948
        in
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   949
          (pattern, compilation)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   950
        end
43253
fa3c61dc9f2c removed generation of instantiated pattern set, which is never actually used
krauss
parents: 43123
diff changeset
   951
        val switch = Datatype.make_case ctxt Datatype_Case.Quiet [] inp_var
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   952
          ((map compile_single_case switched_clauses) @
43253
fa3c61dc9f2c removed generation of instantiated pattern set, which is never actually used
krauss
parents: 43123
diff changeset
   953
            [(xt, mk_bot compfuns (HOLogic.mk_tupleT outTs))])
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   954
      in
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   955
        case compile_switch_tree all_vs ctxt_eqs left_clauses of
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   956
          NONE => SOME switch
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   957
        | SOME left_comp => SOME (mk_sup compfuns (switch, left_comp))
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   958
      end
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   959
  in
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   960
    compile_switch_tree all_vs [] switch_tree
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   961
  end
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   962
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   963
(* compilation of predicates *)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   964
37005
842a73dc6d0e changing compilation to work only with contexts; adapting quickcheck
bulwahn
parents: 37004
diff changeset
   965
fun compile_pred options compilation_modifiers ctxt all_vs param_vs s T (pol, mode) moded_cls =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   966
  let
40050
638ce4dabe53 for now safely but unpractically assume no predicate is terminating
bulwahn
parents: 40049
diff changeset
   967
    val is_terminating = false (* FIXME: requires an termination analysis *)  
40049
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   968
    val compilation_modifiers =
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   969
      (if pol then compilation_modifiers else
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   970
        negative_comp_modifiers_of compilation_modifiers)
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   971
      |> (if is_depth_limited_compilation (Comp_Mod.compilation compilation_modifiers) then
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   972
           (if is_terminating then
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   973
             (Comp_Mod.set_compfuns (unlimited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers)))
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   974
           else
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   975
             (Comp_Mod.set_compfuns (limited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers))))
75d9f57123d6 adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents: 39785
diff changeset
   976
         else I)
35879
99818df5b8f5 reviving the classical depth-limited computation in the predicate compiler
bulwahn
parents: 35845
diff changeset
   977
    val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   978
      (all_vs @ param_vs)
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   979
    val compfuns = Comp_Mod.compfuns compilation_modifiers
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   980
    fun is_param_type (T as Type ("fun",[_ , T'])) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   981
      is_some (try (dest_predT compfuns) T) orelse is_param_type T'
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   982
      | is_param_type T = is_some (try (dest_predT compfuns) T)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   983
    val (inpTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   984
      (binder_types T)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   985
    val predT = mk_predT compfuns (HOLogic.mk_tupleT outTs)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   986
    val funT = Comp_Mod.funT_of compilation_modifiers mode T
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   987
    val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   988
      (fn T => fn (param_vs, names) =>
36018
096ec83348f3 added new compilation to predicate_compiler
bulwahn
parents: 36004
diff changeset
   989
        if is_param_type T then
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   990
          (Free (hd param_vs, T), (tl param_vs, names))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   991
        else
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   992
          let
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 43253
diff changeset
   993
            val new = singleton (Name.variant_list names) "x"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   994
          in (Free (new, T), (param_vs, new :: names)) end)) inpTs
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   995
        (param_vs, (all_vs @ param_vs))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   996
    val in_ts' = map_filter (map_filter_prod
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   997
      (fn t as Free (x, _) => if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
   998
    val param_modes = param_vs ~~ ho_arg_modes_of mode
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
   999
    val compilation =
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
  1000
      if detect_switches options then
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
  1001
        the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs))
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
  1002
          (compile_switch compilation_modifiers ctxt all_vs param_modes additional_arguments mode
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
  1003
            in_ts' outTs (mk_switch_tree ctxt mode moded_cls))
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
  1004
      else
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
  1005
        let
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
  1006
          val cl_ts =
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
  1007
            map (fn (ts, moded_prems) => 
39648
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
  1008
              compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments
655307cb8489 rewriting function mk_Eval_of in predicate compiler
bulwahn
parents: 39557
diff changeset
  1009
                (HOLogic.mk_tuple in_ts') (split_mode mode ts) moded_prems) moded_cls;
36254
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
  1010
        in
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
  1011
          Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
  1012
            (if null cl_ts then
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
  1013
              mk_bot compfuns (HOLogic.mk_tupleT outTs)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
  1014
            else
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
  1015
              foldr1 (mk_sup compfuns) cl_ts)
95ef0a3cf31c added switch detection to the predicate compiler
bulwahn
parents: 36252
diff changeset
  1016
        end
33143
730a2e8a6ec6 modularized the compilation in the predicate compiler
bulwahn
parents: 33141
diff changeset
  1017
    val fun_const =
35891
3122bdd95275 contextifying the compilation of the predicate compiler
bulwahn
parents: 35889
diff changeset
  1018
      Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
37003
a393a588b82e moving towards working with proof contexts in the predicate compiler
bulwahn
parents: 37002
diff changeset
  1019
      ctxt s mode, funT)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1020
  in
33143
730a2e8a6ec6 modularized the compilation in the predicate compiler
bulwahn
parents: 33141
diff changeset
  1021
    HOLogic.mk_Trueprop
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1022
      (HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1023
  end;
33143
730a2e8a6ec6 modularized the compilation in the predicate compiler
bulwahn
parents: 33141
diff changeset
  1024
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1025
(* Definition of executable functions and their intro and elim rules *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1026
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1027
fun print_arities arities = tracing ("Arities:\n" ^
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1028
  cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1029
    space_implode " -> " (map
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1030
      (fn NONE => "X" | SOME k' => string_of_int k')
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1031
        (ks @ [SOME k]))) arities));
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1032
37591
d3daea901123 merged constants "split" and "prod_case"
haftmann
parents: 37558
diff changeset
  1033
fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs t
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1034
  | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1035
  | strip_split_abs t = t
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1036
37678
0040bafffdef "prod" and "sum" replace "*" and "+" respectively
haftmann
parents: 37591
diff changeset
  1037
fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names =
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
  1038
    if eq_mode (m, Input) orelse eq_mode (m, Output) then
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
  1039
      let
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 43253
diff changeset
  1040
        val x = singleton (Name.variant_list names) "x"
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
  1041
      in
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
  1042
        (Free (x, T), x :: names)
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
  1043
      end
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
  1044
    else
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
  1045
      let
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
  1046
        val (t1, names') = mk_args is_eval (m1, T1) names
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
  1047
        val (t2, names'') = mk_args is_eval (m2, T2) names'
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
  1048
      in
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
  1049
        (HOLogic.mk_prod (t1, t2), names'')
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35267
diff changeset
  1050
      end
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1051
  | mk_args is_eval ((m as Fun _), T) names =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1052
    let
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
  1053
      val funT = funT_of Predicate_Comp_Funs.compfuns m T
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 43253
diff changeset
  1054
      val x = singleton (Name.variant_list names) "x"
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1055
      val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1056
      val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
  1057
      val t = fold_rev HOLogic.tupled_lambda args (Predicate_Comp_Funs.mk_Eval
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1058
        (list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1059
    in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1060
      (if is_eval then t else Free (x, funT), x :: names)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1061
    end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1062
  | mk_args is_eval (_, T) names =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1063
    let
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 43253
diff changeset
  1064
      val x = singleton (Name.variant_list names) "x"
33268
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33265
diff changeset
  1065
    in
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1066
      (Free (x, T), x :: names)
33268
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33265
diff changeset
  1067
    end
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1068
37003
a393a588b82e moving towards working with proof contexts in the predicate compiler
bulwahn
parents: 37002
diff changeset
  1069
fun create_intro_elim_rule ctxt mode defthm mode_id funT pred =
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1070
  let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1071
    val funtrm = Const (mode_id, funT)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1072
    val Ts = binder_types (fastype_of pred)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1073
    val (args, argnames) = fold_map (mk_args true) (strip_fun_mode mode ~~ Ts) []
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1074
    fun strip_eval _ t =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1075
      let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1076
        val t' = strip_split_abs t
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
  1077
        val (r, _) = Predicate_Comp_Funs.dest_Eval t'
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1078
      in (SOME (fst (strip_comb r)), NONE) end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1079
    val (inargs, outargs) = split_map_mode strip_eval mode args
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1080
    val eval_hoargs = ho_args_of mode args
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1081
    val hoargTs = ho_argsT_of mode Ts
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1082
    val hoarg_names' =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1083
      Name.variant_list argnames ((map (fn i => "x" ^ string_of_int i)) (1 upto (length hoargTs)))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1084
    val hoargs' = map2 (curry Free) hoarg_names' hoargTs
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1085
    val args' = replace_ho_args mode hoargs' args
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1086
    val predpropI = HOLogic.mk_Trueprop (list_comb (pred, args'))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1087
    val predpropE = HOLogic.mk_Trueprop (list_comb (pred, args))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1088
    val param_eqs = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) eval_hoargs hoargs'
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
  1089
    val funpropE = HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval (list_comb (funtrm, inargs),
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1090
                    if null outargs then Free("y", HOLogic.unitT) else HOLogic.mk_tuple outargs))
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
  1091
    val funpropI = HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval (list_comb (funtrm, inargs),
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1092
                     HOLogic.mk_tuple outargs))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1093
    val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1094
    val simprules = [defthm, @{thm eval_pred},
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1095
      @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1096
    val unfolddef_tac = Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1
37003
a393a588b82e moving towards working with proof contexts in the predicate compiler
bulwahn
parents: 37002
diff changeset
  1097
    val introthm = Goal.prove ctxt
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1098
      (argnames @ hoarg_names' @ ["y"]) [] introtrm (fn _ => unfolddef_tac)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1099
    val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1100
    val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
37003
a393a588b82e moving towards working with proof contexts in the predicate compiler
bulwahn
parents: 37002
diff changeset
  1101
    val elimthm = Goal.prove ctxt
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1102
      (argnames @ ["y", "P"]) [] elimtrm (fn _ => unfolddef_tac)
35884
362bfc2ca0ee adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents: 35881
diff changeset
  1103
    val opt_neg_introthm =
362bfc2ca0ee adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents: 35881
diff changeset
  1104
      if is_all_input mode then
362bfc2ca0ee adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents: 35881
diff changeset
  1105
        let
362bfc2ca0ee adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents: 35881
diff changeset
  1106
          val neg_predpropI = HOLogic.mk_Trueprop (HOLogic.mk_not (list_comb (pred, args')))
362bfc2ca0ee adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents: 35881
diff changeset
  1107
          val neg_funpropI =
45450
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
  1108
            HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval
dc2236b19a3d adding CPS compilation to predicate compiler;
bulwahn
parents: 45214
diff changeset
  1109
              (Predicate_Comp_Funs.mk_not (list_comb (funtrm, inargs)), HOLogic.unit))
35884
362bfc2ca0ee adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents: 35881
diff changeset
  1110
          val neg_introtrm = Logic.list_implies (neg_predpropI :: param_eqs, neg_funpropI)
362bfc2ca0ee adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents: 35881
diff changeset
  1111
          val tac =
362bfc2ca0ee adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents: 35881
diff changeset
  1112
            Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps
362bfc2ca0ee adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents: 35881
diff changeset
  1113
              (@{thm if_False} :: @{thm Predicate.not_pred_eq} :: simprules)) 1
362bfc2ca0ee adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents: 35881
diff changeset
  1114
            THEN rtac @{thm Predicate.singleI} 1
37003
a393a588b82e moving towards working with proof contexts in the predicate compiler
bulwahn
parents: 37002
diff changeset
  1115
        in SOME (Goal.prove ctxt (argnames @ hoarg_names') []
35884
362bfc2ca0ee adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents: 35881
diff changeset
  1116
            neg_introtrm (fn _ => tac))
362bfc2ca0ee adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents: 35881
diff changeset
  1117
        end
362bfc2ca0ee adding proof procedure for cases rule with tuples; adding introduction rule for negated premises; improving proof procedure with negated premises
bulwahn
parents: 35881
diff changeset
  1118
      else NONE
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset