src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
author bulwahn
Mon, 22 Mar 2010 08:30:13 +0100
changeset 35879 99818df5b8f5
parent 35845 e5980f0ad025
child 35880 2623b23e41fc
permissions -rw-r--r--
reviving the classical depth-limited computation in the predicate compiler
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
33478
b70fe083694d moved values command from core to predicate compile
bulwahn
parents: 33476
diff changeset
     9
  val setup : theory -> theory
b70fe083694d moved values command from core to predicate compile
bulwahn
parents: 33476
diff changeset
    10
  val code_pred : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
b70fe083694d moved values command from core to predicate compile
bulwahn
parents: 33476
diff changeset
    11
  val code_pred_cmd : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    12
  val values_cmd : string list -> Predicate_Compile_Aux.mode option list option
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    13
    -> (string option * (Predicate_Compile_Aux.compilation * int list))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    14
    -> int -> string -> Toplevel.state -> unit
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    15
  val register_predicate : (string * thm list * thm) -> theory -> theory
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
    16
  val register_intros : string * thm list -> theory -> theory
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    17
  val is_registered : theory -> string -> bool
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    18
  val function_name_of : Predicate_Compile_Aux.compilation -> theory
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
    19
    -> string -> bool * Predicate_Compile_Aux.mode -> string
33328
1d93dd8a02c9 moved datatype mode and string functions to the auxillary structure
bulwahn
parents: 33327
diff changeset
    20
  val predfun_intro_of: theory -> string -> Predicate_Compile_Aux.mode -> thm
1d93dd8a02c9 moved datatype mode and string functions to the auxillary structure
bulwahn
parents: 33327
diff changeset
    21
  val predfun_elim_of: theory -> string -> Predicate_Compile_Aux.mode -> thm
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    22
  val all_preds_of : theory -> string list
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    23
  val modes_of: Predicate_Compile_Aux.compilation
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    24
    -> theory -> string -> Predicate_Compile_Aux.mode list
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    25
  val all_modes_of : Predicate_Compile_Aux.compilation
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    26
    -> theory -> (string * Predicate_Compile_Aux.mode list) list
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
    27
  val all_random_modes_of : theory -> (string * Predicate_Compile_Aux.mode list) list
33478
b70fe083694d moved values command from core to predicate compile
bulwahn
parents: 33476
diff changeset
    28
  val intros_of : theory -> string -> thm list
b70fe083694d moved values command from core to predicate compile
bulwahn
parents: 33476
diff changeset
    29
  val add_intro : thm -> theory -> theory
b70fe083694d moved values command from core to predicate compile
bulwahn
parents: 33476
diff changeset
    30
  val set_elim : thm -> theory -> theory
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    31
  val preprocess_intro : theory -> thm -> thm
33478
b70fe083694d moved values command from core to predicate compile
bulwahn
parents: 33476
diff changeset
    32
  val print_stored_rules : theory -> unit
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    33
  val print_all_modes : Predicate_Compile_Aux.compilation -> theory -> unit
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    34
  val mk_casesrule : Proof.context -> term -> thm list -> term
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    35
  
33137
0d16c07f8d24 added option to generate random values to values command in the predicate compiler
bulwahn
parents: 33135
diff changeset
    36
  val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
    37
  val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int))
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
    38
    option Unsynchronized.ref
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    39
  val dseq_eval_ref : (unit -> term DSequence.dseq) option Unsynchronized.ref
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    40
  val random_dseq_eval_ref : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    41
    option Unsynchronized.ref
33628
ed2111a5c3ed renaming code_pred_intros to code_pred_intro
bulwahn
parents: 33626
diff changeset
    42
  val code_pred_intro_attrib : attribute
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    43
  
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    44
  (* used by Quickcheck_Generator *) 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    45
  (* temporary for testing of the compilation *)
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    46
  
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    47
  datatype compilation_funs = CompilationFuns of {
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    48
    mk_predT : typ -> typ,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    49
    dest_predT : typ -> typ,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    50
    mk_bot : typ -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    51
    mk_single : term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    52
    mk_bind : term * term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    53
    mk_sup : term * term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    54
    mk_if : term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    55
    mk_not : term -> term,
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
    56
    mk_map : typ -> typ -> term -> term -> term
33140
83951822bfd0 cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
bulwahn
parents: 33139
diff changeset
    57
  };
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    58
  
32672
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
    59
  val pred_compfuns : compilation_funs
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
    60
  val randompred_compfuns : compilation_funs
33256
b350516cb1f9 adding a prototype of a counter-example generator based on the predicate compiler to HOL/ex
bulwahn
parents: 33251
diff changeset
    61
  val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    62
  val add_random_dseq_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
    63
  val mk_tracing : string -> term -> term
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    64
end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    65
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    66
structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    67
struct
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    68
32668
b2de45007537 added first prototype of the extended predicate compiler
bulwahn
parents: 32667
diff changeset
    69
open Predicate_Compile_Aux;
33144
1831516747d4 removed obsolete GeneratorPrem; clean-up after modularization; tuned
bulwahn
parents: 33143
diff changeset
    70
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    71
(** auxiliary **)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    72
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    73
(* debug stuff *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    74
33108
9d9afd478016 added test for higher-order function inductification; added debug messages
bulwahn
parents: 33106
diff changeset
    75
fun print_tac s = Seq.single;
33139
9c01ee6f8ee9 added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents: 33138
diff changeset
    76
33127
eb91ec1ef6f0 added option show_proof_trace
bulwahn
parents: 33126
diff changeset
    77
fun print_tac' options s = 
eb91ec1ef6f0 added option show_proof_trace
bulwahn
parents: 33126
diff changeset
    78
  if show_proof_trace options then Tactical.print_tac s else Seq.single;
eb91ec1ef6f0 added option show_proof_trace
bulwahn
parents: 33126
diff changeset
    79
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    80
fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    81
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    82
fun assert b = if not b then error "Assertion failed" else warning "Assertion holds"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
    83
33108
9d9afd478016 added test for higher-order function inductification; added debug messages
bulwahn
parents: 33106
diff changeset
    84
datatype assertion = Max_number_of_subgoals of int
9d9afd478016 added test for higher-order function inductification; added debug messages
bulwahn
parents: 33106
diff changeset
    85
fun assert_tac (Max_number_of_subgoals i) st =
9d9afd478016 added test for higher-order function inductification; added debug messages
bulwahn
parents: 33106
diff changeset
    86
  if (nprems_of st <= i) then Seq.single st
9d9afd478016 added test for higher-order function inductification; added debug messages
bulwahn
parents: 33106
diff changeset
    87
  else error ("assert_tac: Numbers of subgoals mismatch at goal state :"
9d9afd478016 added test for higher-order function inductification; added debug messages
bulwahn
parents: 33106
diff changeset
    88
    ^ "\n" ^ Pretty.string_of (Pretty.chunks
9d9afd478016 added test for higher-order function inductification; added debug messages
bulwahn
parents: 33106
diff changeset
    89
      (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));
9d9afd478016 added test for higher-order function inductification; added debug messages
bulwahn
parents: 33106
diff changeset
    90
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    91
(** fundamentals **)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    92
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    93
(* syntactic operations *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    94
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    95
fun mk_eq (x, xs) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    96
  let fun mk_eqs _ [] = []
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    97
        | mk_eqs a (b::cs) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    98
            HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    99
  in mk_eqs x xs end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   100
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   101
fun mk_scomp (t, u) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   102
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   103
    val T = fastype_of t
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   104
    val U = fastype_of u
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   105
    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
   106
    val D = body_type U                   
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   107
  in 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   108
    Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   109
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   110
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   111
fun dest_funT (Type ("fun",[S, T])) = (S, T)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   112
  | dest_funT T = raise TYPE ("dest_funT", [T], [])
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   113
 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   114
fun mk_fun_comp (t, u) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   115
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   116
    val (_, B) = dest_funT (fastype_of t)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   117
    val (C, A) = dest_funT (fastype_of u)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   118
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   119
    Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   120
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   121
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   122
fun dest_randomT (Type ("fun", [@{typ Random.seed},
32674
b629fbcc5313 merged; adopted to changes from Code_Evaluation in the predicate compiler
bulwahn
parents: 32673
diff changeset
   123
  Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   124
  | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   125
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   126
fun mk_tracing s t =
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   127
  Const(@{const_name Code_Evaluation.tracing},
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   128
    @{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
   129
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   130
val strip_intro_concl = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   131
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   132
(* derivation trees for modes of premises *)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   133
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   134
datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   135
  | Mode_Pair of mode_derivation * mode_derivation | Term of mode
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   136
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   137
fun string_of_derivation (Mode_App (m1, m2)) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   138
  "App (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   139
  | string_of_derivation (Mode_Pair (m1, m2)) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   140
  "Pair (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   141
  | string_of_derivation (Term m) = "Term (" ^ string_of_mode m ^ ")"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   142
  | string_of_derivation (Context m) = "Context (" ^ string_of_mode m ^ ")"
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   143
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   144
fun strip_mode_derivation deriv =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   145
  let
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   146
    fun strip (Mode_App (deriv1, deriv2)) ds = strip deriv1 (deriv2 :: ds)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   147
      | strip deriv ds = (deriv, ds)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   148
  in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   149
    strip deriv []
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   150
  end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   151
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   152
fun mode_of (Context m) = m
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   153
  | mode_of (Term m) = m
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   154
  | mode_of (Mode_App (d1, d2)) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   155
    (case mode_of d1 of Fun (m, 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
   156
        (if eq_mode (m, mode_of d2) then m' else error "mode_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
   157
      | _ => error "mode_of2")
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   158
  | mode_of (Mode_Pair (d1, d2)) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   159
    Pair (mode_of d1, mode_of d2)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   160
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   161
fun head_mode_of deriv = mode_of (fst (strip_mode_derivation deriv))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   162
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   163
fun param_derivations_of deriv =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   164
  let
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   165
    val (_, argument_derivs) = strip_mode_derivation deriv
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   166
    fun param_derivation (Mode_Pair (m1, m2)) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   167
        param_derivation m1 @ param_derivation m2
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   168
      | param_derivation (Term _) = []
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   169
      | param_derivation m = [m]
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   170
  in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   171
    maps param_derivation argument_derivs
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   172
  end
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   173
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   174
fun collect_context_modes (Mode_App (m1, m2)) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   175
      collect_context_modes m1 @ collect_context_modes m2
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   176
  | collect_context_modes (Mode_Pair (m1, m2)) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   177
      collect_context_modes m1 @ collect_context_modes m2
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   178
  | collect_context_modes (Context m) = [m]
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   179
  | collect_context_modes (Term _) = []
32668
b2de45007537 added first prototype of the extended predicate compiler
bulwahn
parents: 32667
diff changeset
   180
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   181
(* representation of inferred clauses with modes *)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   182
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   183
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
   184
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
   185
type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   186
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   187
(* book-keeping *)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   188
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   189
datatype predfun_data = PredfunData of {
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   190
  definition : thm,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   191
  intro : thm,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   192
  elim : thm
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   193
};
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   194
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   195
fun rep_predfun_data (PredfunData data) = data;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   196
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   197
fun mk_predfun_data (definition, intro, elim) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   198
  PredfunData {definition = definition, intro = intro, elim = elim}
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   199
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   200
datatype pred_data = PredData of {
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   201
  intros : thm list,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   202
  elim : thm option,
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   203
  function_names : (compilation * (mode * string) list) list,
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   204
  predfun_data : (mode * predfun_data) list,
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   205
  needs_random : mode list
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   206
};
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   207
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   208
fun rep_pred_data (PredData data) = data;
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   209
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   210
fun mk_pred_data ((intros, elim), (function_names, predfun_data, needs_random)) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   211
  PredData {intros = intros, elim = elim,
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   212
    function_names = function_names, predfun_data = predfun_data, needs_random = needs_random}
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   213
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   214
fun map_pred_data f (PredData {intros, elim, function_names, predfun_data, needs_random}) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   215
  mk_pred_data (f ((intros, elim), (function_names, predfun_data, needs_random)))
33144
1831516747d4 removed obsolete GeneratorPrem; clean-up after modularization; tuned
bulwahn
parents: 33143
diff changeset
   216
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   217
fun eq_option eq (NONE, NONE) = true
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   218
  | eq_option eq (SOME x, SOME y) = eq (x, y)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   219
  | eq_option eq _ = false
33144
1831516747d4 removed obsolete GeneratorPrem; clean-up after modularization; tuned
bulwahn
parents: 33143
diff changeset
   220
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   221
fun eq_pred_data (PredData d1, PredData d2) = 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   222
  eq_list (Thm.eq_thm) (#intros d1, #intros d2) andalso
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   223
  eq_option (Thm.eq_thm) (#elim d1, #elim d2)
33144
1831516747d4 removed obsolete GeneratorPrem; clean-up after modularization; tuned
bulwahn
parents: 33143
diff changeset
   224
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33519
diff changeset
   225
structure PredData = Theory_Data
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   226
(
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   227
  type T = pred_data Graph.T;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   228
  val empty = Graph.empty;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   229
  val extend = I;
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33519
diff changeset
   230
  val merge = Graph.merge eq_pred_data;
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   231
);
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   232
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   233
(* queries *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   234
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   235
fun lookup_pred_data thy name =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   236
  Option.map rep_pred_data (try (Graph.get_node (PredData.get thy)) name)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   237
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   238
fun the_pred_data thy name = case lookup_pred_data thy name
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   239
 of NONE => error ("No such predicate " ^ quote name)  
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   240
  | SOME data => data;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   241
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   242
val is_registered = is_some oo lookup_pred_data
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   243
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   244
val all_preds_of = Graph.keys o PredData.get
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   245
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   246
fun intros_of thy = map (Thm.transfer thy) o #intros o the_pred_data thy
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   247
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   248
fun the_elim_of thy name = case #elim (the_pred_data thy name)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   249
 of NONE => error ("No elimination rule for predicate " ^ quote name)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   250
  | SOME thm => Thm.transfer thy thm 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   251
  
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   252
val has_elim = is_some o #elim oo the_pred_data;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   253
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   254
fun function_names_of compilation thy name =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   255
  case AList.lookup (op =) (#function_names (the_pred_data thy name)) compilation of
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   256
    NONE => error ("No " ^ string_of_compilation compilation
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   257
      ^ "functions defined for predicate " ^ quote name)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   258
  | SOME fun_names => fun_names
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   259
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
   260
fun function_name_of compilation thy name (pol, mode) =
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
   261
  case AList.lookup eq_mode
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
   262
    (function_names_of (compilation_for_polarity pol compilation) thy name) mode 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
   263
    NONE => error ("No " ^ string_of_compilation compilation
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   264
      ^ "function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   265
  | SOME function_name => function_name
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   266
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   267
fun modes_of compilation thy name = map fst (function_names_of compilation thy name)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   268
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   269
fun all_modes_of compilation thy =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   270
  map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   271
    (all_preds_of thy)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   272
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   273
val all_random_modes_of = all_modes_of Random
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   274
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   275
fun defined_functions compilation thy name =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   276
  AList.defined (op =) (#function_names (the_pred_data thy name)) compilation
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   277
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   278
fun lookup_predfun_data thy name mode =
33483
a15a2f7f7560 improved handling of already defined functions in the predicate compiler; could cause trouble before when no modes for a predicate were infered
bulwahn
parents: 33482
diff changeset
   279
  Option.map rep_predfun_data
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   280
    (AList.lookup (op =) (#predfun_data (the_pred_data thy name)) mode)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   281
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   282
fun the_predfun_data thy name mode =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   283
  case lookup_predfun_data thy name mode of
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   284
    NONE => error ("No function defined for mode " ^ string_of_mode mode ^
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   285
      " of predicate " ^ name)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   286
  | SOME data => data;
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   287
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   288
val predfun_definition_of = #definition ooo the_predfun_data
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   289
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   290
val predfun_intro_of = #intro ooo the_predfun_data
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   291
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   292
val predfun_elim_of = #elim ooo the_predfun_data
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   293
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   294
(* diagnostic display functions *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   295
33619
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   296
fun print_modes options thy modes =
33251
4b13ab778b78 added option show_modes to predicate compiler
bulwahn
parents: 33250
diff changeset
   297
  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
   298
    tracing ("Inferred modes:\n" ^
33251
4b13ab778b78 added option show_modes to predicate compiler
bulwahn
parents: 33250
diff changeset
   299
      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
   300
        (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
   301
  else ()
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   302
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   303
fun print_pred_mode_table string_of_entry thy pred_mode_table =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   304
  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
   305
    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
   306
      ^ string_of_entry pred mode entry
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   307
    fun print_pred (pred, modes) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   308
      "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
   309
    val _ = tracing (cat_lines (map print_pred pred_mode_table))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   310
  in () end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   311
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   312
fun string_of_prem thy (Prem t) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   313
    (Syntax.string_of_term_global thy t) ^ "(premise)"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   314
  | string_of_prem thy (Negprem t) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   315
    (Syntax.string_of_term_global thy (HOLogic.mk_not t)) ^ "(negative premise)"
33130
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   316
  | string_of_prem thy (Sidecond t) =
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   317
    (Syntax.string_of_term_global thy t) ^ "(sidecondition)"
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   318
  | string_of_prem thy _ = error "string_of_prem: unexpected input"
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   319
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   320
fun string_of_clause thy pred (ts, prems) =
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   321
  (space_implode " --> "
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   322
  (map (string_of_prem thy) prems)) ^ " --> " ^ pred ^ " "
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   323
   ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   324
33139
9c01ee6f8ee9 added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents: 33138
diff changeset
   325
fun print_compiled_terms options thy =
9c01ee6f8ee9 added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents: 33138
diff changeset
   326
  if show_compilation options then
9c01ee6f8ee9 added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents: 33138
diff changeset
   327
    print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy
9c01ee6f8ee9 added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents: 33138
diff changeset
   328
  else K ()
9c01ee6f8ee9 added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents: 33138
diff changeset
   329
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   330
fun print_stored_rules thy =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   331
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   332
    val preds = (Graph.keys o PredData.get) thy
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   333
    fun print pred () = let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   334
      val _ = writeln ("predicate: " ^ pred)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   335
      val _ = writeln ("introrules: ")
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   336
      val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   337
        (rev (intros_of thy pred)) ()
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   338
    in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   339
      if (has_elim thy pred) then
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   340
        writeln ("elimrule: " ^ Display.string_of_thm_global thy (the_elim_of thy pred))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   341
      else
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   342
        writeln ("no elimrule defined")
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   343
    end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   344
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   345
    fold print preds ()
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   346
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   347
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   348
fun print_all_modes compilation thy =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   349
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   350
    val _ = writeln ("Inferred modes:")
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   351
    fun print (pred, modes) u =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   352
      let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   353
        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
   354
        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
   355
      in u end
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   356
  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
   357
    fold print (all_modes_of compilation thy) ()
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   358
  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
   359
33132
07efd452a698 moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents: 33131
diff changeset
   360
(* validity checks *)
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   361
(* EXPECTED MODE and PROPOSED_MODE are largely the same; define a clear semantics for those! *)
33132
07efd452a698 moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents: 33131
diff changeset
   362
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   363
fun check_expected_modes preds options modes =
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   364
  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
   365
    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
   366
      SOME modes =>
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   367
        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
   368
          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
   369
        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
   370
          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
   371
            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
   372
            ^ "  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
   373
            ^ "  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
   374
          else ()
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   375
        end
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   376
      | NONE => ())
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   377
  | NONE => ()
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   378
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   379
fun check_proposed_modes preds options modes extra_modes errors =
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   380
  case proposed_modes options of
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   381
    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
   382
      SOME inferred_ms =>
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   383
        let
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   384
          val preds_without_modes = map fst (filter (null o snd) (modes @ extra_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
   385
          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
   386
        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
   387
          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
   388
            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
   389
            ^ "  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
   390
            ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms) ^ "\n"
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   391
            ^ "For the following clauses, the following modes could not be inferred: " ^ "\n"
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   392
            ^ cat_lines errors ^
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   393
            (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
   394
              "\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
   395
            else ""))
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   396
          else ()
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   397
        end
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   398
      | NONE => ())
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   399
  | NONE => ()
33132
07efd452a698 moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents: 33131
diff changeset
   400
33144
1831516747d4 removed obsolete GeneratorPrem; clean-up after modularization; tuned
bulwahn
parents: 33143
diff changeset
   401
(* importing introduction rules *)
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
   402
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   403
fun unify_consts thy cs intr_ts =
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   404
  (let
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   405
     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   406
     fun varify (t, (i, ts)) =
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35411
diff changeset
   407
       let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t))
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
   408
       in (maxidx_of_term t', t'::ts) end;
33150
75eddea4abef further changes due to the previous merge in the predicate compiler
bulwahn
parents: 33149
diff changeset
   409
     val (i, cs') = List.foldr varify (~1, []) cs;
75eddea4abef further changes due to the previous merge in the predicate compiler
bulwahn
parents: 33149
diff changeset
   410
     val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
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
   411
     val rec_consts = fold add_term_consts_2 cs' [];
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   412
     val intr_consts = fold add_term_consts_2 intr_ts' [];
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   413
     fun unify (cname, cT) =
33317
b4534348b8fd standardized filter/filter_out;
wenzelm
parents: 33268
diff changeset
   414
       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
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
   415
       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   416
     val (env, _) = fold unify rec_consts (Vartab.empty, i');
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   417
     val subst = map_types (Envir.norm_type env)
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   418
   in (map subst cs', map subst intr_ts')
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   419
   end) handle Type.TUNIFY =>
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   420
     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   421
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   422
fun import_intros inp_pred [] ctxt =
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   423
  let
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   424
    val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   425
    val T = fastype_of outp_pred
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   426
    (* TODO: put in a function for this next line! *)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   427
    val paramTs = ho_argsT_of (hd (all_modes_of_typ T)) (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
   428
    val (param_names, ctxt'') = Variable.variant_fixes
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   429
      (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
33629
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   430
    val params = map2 (curry Free) param_names paramTs
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   431
  in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   432
    (((outp_pred, params), []), ctxt')
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   433
  end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   434
  | import_intros inp_pred (th :: ths) ctxt =
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
   435
    let
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   436
      val ((_, [th']), ctxt') = Variable.import true [th] ctxt
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
   437
      val thy = ProofContext.theory_of 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
   438
      val (pred, args) = strip_intro_concl th'
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   439
      val T = 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
   440
      val ho_args = ho_args_of (hd (all_modes_of_typ T)) args
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   441
      fun subst_of (pred', pred) =
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   442
        let
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   443
          val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   444
        in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) 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
   445
      fun instantiate_typ th =
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   446
        let
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   447
          val (pred', _) = strip_intro_concl th
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
   448
          val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   449
            error "Trying to instantiate another predicate" else ()
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   450
        in Thm.certify_instantiate (subst_of (pred', pred), []) th 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
   451
      fun instantiate_ho_args th =
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   452
        let
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   453
          val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   454
          val ho_args' = map dest_Var (ho_args_of (hd (all_modes_of_typ T)) args')
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   455
        in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   456
      val outp_pred =
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   457
        Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
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
   458
      val ((_, ths'), ctxt1) =
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   459
        Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   460
    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
   461
      (((outp_pred, ho_args), th' :: ths'), ctxt1)
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
   462
    end
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   463
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   464
(* generation of case rules from user-given introduction rules *)
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   465
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   466
fun mk_args2 (Type ("*", [T1, T2])) st =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   467
    let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   468
      val (t1, st') = mk_args2 T1 st
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   469
      val (t2, st'') = mk_args2 T2 st'
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   470
    in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   471
      (HOLogic.mk_prod (t1, t2), st'')
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   472
    end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   473
  | mk_args2 (T as Type ("fun", _)) (params, ctxt) = 
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   474
    let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   475
      val (S, U) = strip_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
   476
    in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   477
      if U = HOLogic.boolT then
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   478
        (hd params, (tl params, ctxt))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   479
      else
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   480
        let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   481
          val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   482
        in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   483
          (Free (x, T), (params, ctxt'))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   484
        end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   485
    end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   486
  | mk_args2 T (params, ctxt) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   487
    let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   488
      val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   489
    in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   490
      (Free (x, T), (params, ctxt'))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   491
    end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   492
  
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   493
fun mk_casesrule ctxt pred introrules =
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
   494
  let
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   495
    val (((pred, params), intros_th), ctxt1) = import_intros pred introrules ctxt
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
   496
    val intros = map prop_of intros_th
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   497
    val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   498
    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   499
    val argsT = 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
   500
    val (argvs, _) = fold_map mk_args2 argsT (params, ctxt2)
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
   501
    fun mk_case intro =
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   502
      let
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   503
        val (_, args) = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl) intro
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
   504
        val prems = Logic.strip_imp_prems intro
33629
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   505
        val eqprems = map2 (HOLogic.mk_Trueprop oo (curry HOLogic.mk_eq)) argvs args
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
   506
        val frees = (fold o fold_aterms)
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   507
          (fn t as Free _ =>
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   508
              if member (op aconv) params t then I else insert (op aconv) t
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   509
           | _ => I) (args @ prems) []
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   510
      in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) 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
   511
    val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs))
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
   512
    val cases = map mk_case intros
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   513
  in Logic.list_implies (assm :: cases, prop) end;
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   514
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   515
(** preprocessing rules **)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   516
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   517
fun imp_prems_conv cv ct =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   518
  case Thm.term_of ct of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   519
    Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   520
  | _ => Conv.all_conv ct
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   521
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   522
fun Trueprop_conv cv ct =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   523
  case Thm.term_of ct of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   524
    Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct  
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   525
  | _ => error "Trueprop_conv"
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   526
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   527
fun preprocess_intro thy rule =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   528
  Conv.fconv_rule
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   529
    (imp_prems_conv
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   530
      (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq})))))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   531
    (Thm.transfer thy rule)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   532
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   533
fun preprocess_elim thy elimrule =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   534
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   535
    fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   536
       HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   537
     | replace_eqs t = t
33128
1f990689349f further cleaning up
bulwahn
parents: 33127
diff changeset
   538
    val ctxt = ProofContext.init thy
1f990689349f further cleaning up
bulwahn
parents: 33127
diff changeset
   539
    val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt
1f990689349f further cleaning up
bulwahn
parents: 33127
diff changeset
   540
    val prems = Thm.prems_of elimrule
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   541
    val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems))))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   542
    fun preprocess_case t =
33128
1f990689349f further cleaning up
bulwahn
parents: 33127
diff changeset
   543
      let
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   544
       val params = Logic.strip_params t
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   545
       val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   546
       val assums_hyp' = assums1 @ (map replace_eqs assums2)
33128
1f990689349f further cleaning up
bulwahn
parents: 33127
diff changeset
   547
      in
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   548
       list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t))
33128
1f990689349f further cleaning up
bulwahn
parents: 33127
diff changeset
   549
      end
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   550
    val cases' = map preprocess_case (tl prems)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   551
    val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   552
    val bigeq = (Thm.symmetric (Conv.implies_concl_conv
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   553
      (MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}])
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   554
        (cterm_of thy elimrule')))
33150
75eddea4abef further changes due to the previous merge in the predicate compiler
bulwahn
parents: 33149
diff changeset
   555
    val tac = (fn _ => Skip_Proof.cheat_tac thy)    
33109
7025bc7a5054 changed elimination preprocessing due to an error with a JinjaThread predicate
bulwahn
parents: 33108
diff changeset
   556
    val eq = Goal.prove ctxt' [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   557
  in
33109
7025bc7a5054 changed elimination preprocessing due to an error with a JinjaThread predicate
bulwahn
parents: 33108
diff changeset
   558
    Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   559
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   560
33124
5378e61add1a continued cleaning up; moved tuple expanding to core
bulwahn
parents: 33123
diff changeset
   561
fun expand_tuples_elim th = th
5378e61add1a continued cleaning up; moved tuple expanding to core
bulwahn
parents: 33123
diff changeset
   562
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   563
val no_compilation = ([], [], [])
33483
a15a2f7f7560 improved handling of already defined functions in the predicate compiler; could cause trouble before when no modes for a predicate were infered
bulwahn
parents: 33482
diff changeset
   564
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   565
fun fetch_pred_data thy name =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   566
  case try (Inductive.the_inductive (ProofContext.init thy)) name of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   567
    SOME (info as (_, result)) => 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   568
      let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   569
        fun is_intro_of intro =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   570
          let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   571
            val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   572
          in (fst (dest_Const const) = name) end;      
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   573
        val intros =
33124
5378e61add1a continued cleaning up; moved tuple expanding to core
bulwahn
parents: 33123
diff changeset
   574
          (map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result)))
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   575
        val index = find_index (fn s => s = name) (#names (fst info))
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   576
        val pre_elim = nth (#elims result) index
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   577
        val pred = nth (#preds result) index
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   578
        (*val elim = singleton (Inductive_Set.codegen_preproc thy) (preprocess_elim thy nparams 
33124
5378e61add1a continued cleaning up; moved tuple expanding to core
bulwahn
parents: 33123
diff changeset
   579
          (expand_tuples_elim pre_elim))*)
5378e61add1a continued cleaning up; moved tuple expanding to core
bulwahn
parents: 33123
diff changeset
   580
        val elim =
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 34974
diff changeset
   581
          (Drule.export_without_context o Skip_Proof.make_thm thy)
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   582
          (mk_casesrule (ProofContext.init thy) pred intros)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   583
      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
   584
        mk_pred_data ((intros, SOME elim), no_compilation)
33483
a15a2f7f7560 improved handling of already defined functions in the predicate compiler; could cause trouble before when no modes for a predicate were infered
bulwahn
parents: 33482
diff changeset
   585
      end
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   586
  | NONE => error ("No such predicate: " ^ quote name)
33124
5378e61add1a continued cleaning up; moved tuple expanding to core
bulwahn
parents: 33123
diff changeset
   587
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   588
fun add_predfun_data name mode data =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   589
  let
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   590
    val add = (apsnd o apsnd3) (cons (mode, mk_predfun_data data))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   591
  in PredData.map (Graph.map_node name (map_pred_data add)) end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   592
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   593
fun is_inductive_predicate thy name =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   594
  is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   595
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   596
fun depending_preds_of thy (key, value) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   597
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   598
    val intros = (#intros o rep_pred_data) value
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   599
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   600
    fold Term.add_const_names (map Thm.prop_of intros) []
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   601
      |> filter (fn c => (not (c = key)) andalso
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   602
        (is_inductive_predicate thy c orelse is_registered thy c))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   603
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   604
33629
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   605
fun add_intro thm thy =
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   606
  let
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   607
    val (name, T) = dest_Const (fst (strip_intro_concl thm))
33629
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   608
    fun cons_intro gr =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   609
     case try (Graph.get_node gr) name of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   610
       SOME pred_data => Graph.map_node name (map_pred_data
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   611
         (apfst (fn (intros, elim) => (intros @ [thm], elim)))) gr
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   612
     | NONE => Graph.new_node (name, mk_pred_data (([thm], NONE), no_compilation)) gr
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   613
  in PredData.map cons_intro thy end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   614
33629
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   615
fun set_elim thm =
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   616
  let
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   617
    val (name, _) = dest_Const (fst 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   618
      (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   619
    fun set (intros, _) = (intros, SOME thm)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   620
  in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   621
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   622
fun register_predicate (constname, pre_intros, pre_elim) thy =
33629
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   623
  let
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   624
    val intros = map (preprocess_intro thy) pre_intros
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   625
    val elim = preprocess_elim thy pre_elim
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   626
  in
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   627
    if not (member (op =) (Graph.keys (PredData.get thy)) constname) then
32668
b2de45007537 added first prototype of the extended predicate compiler
bulwahn
parents: 32667
diff changeset
   628
      PredData.map
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   629
        (Graph.new_node (constname,
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   630
          mk_pred_data ((intros, SOME elim), no_compilation))) thy
32668
b2de45007537 added first prototype of the extended predicate compiler
bulwahn
parents: 32667
diff changeset
   631
    else thy
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   632
  end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   633
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   634
fun register_intros (constname, pre_intros) thy =
32668
b2de45007537 added first prototype of the extended predicate compiler
bulwahn
parents: 32667
diff changeset
   635
  let
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   636
    val T = Sign.the_const_type thy constname
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   637
    fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl intr)))
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   638
    val _ = if not (forall (fn intr => constname_of_intro intr = constname) pre_intros) then
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   639
      error ("register_intros: Introduction rules of different constants are used\n" ^
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   640
        "expected rules for " ^ constname ^ ", but received rules for " ^
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   641
          commas (map constname_of_intro pre_intros))
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   642
      else ()
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   643
    val pred = Const (constname, T)
32672
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   644
    val pre_elim = 
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 34974
diff changeset
   645
      (Drule.export_without_context o Skip_Proof.make_thm thy)
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   646
      (mk_casesrule (ProofContext.init thy) pred pre_intros)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   647
  in register_predicate (constname, pre_intros, pre_elim) thy end
32668
b2de45007537 added first prototype of the extended predicate compiler
bulwahn
parents: 32667
diff changeset
   648
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   649
fun defined_function_of compilation pred =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   650
  let
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   651
    val set = (apsnd o apfst3) (cons (compilation, []))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   652
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   653
    PredData.map (Graph.map_node pred (map_pred_data set))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   654
  end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   655
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   656
fun set_function_name compilation pred mode name =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   657
  let
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   658
    val set = (apsnd o apfst3)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   659
      (AList.map_default (op =) (compilation, [(mode, name)]) (cons (mode, name)))
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   660
  in
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   661
    PredData.map (Graph.map_node pred (map_pred_data set))
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   662
  end
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   663
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   664
fun set_needs_random name modes =
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   665
  let
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   666
    val set = (apsnd o aptrd3) (K modes)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   667
  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
   668
    PredData.map (Graph.map_node name (map_pred_data set))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   669
  end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   670
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   671
(* datastructures and setup for generic compilation *)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   672
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   673
datatype compilation_funs = CompilationFuns of {
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   674
  mk_predT : typ -> typ,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   675
  dest_predT : typ -> typ,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   676
  mk_bot : typ -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   677
  mk_single : term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   678
  mk_bind : term * term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   679
  mk_sup : term * term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   680
  mk_if : term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   681
  mk_not : term -> term,
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   682
  mk_map : typ -> typ -> term -> term -> term
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   683
};
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   684
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   685
fun mk_predT (CompilationFuns funs) = #mk_predT funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   686
fun dest_predT (CompilationFuns funs) = #dest_predT funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   687
fun mk_bot (CompilationFuns funs) = #mk_bot funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   688
fun mk_single (CompilationFuns funs) = #mk_single funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   689
fun mk_bind (CompilationFuns funs) = #mk_bind funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   690
fun mk_sup (CompilationFuns funs) = #mk_sup funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   691
fun mk_if (CompilationFuns funs) = #mk_if funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   692
fun mk_not (CompilationFuns funs) = #mk_not funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   693
fun mk_map (CompilationFuns funs) = #mk_map funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   694
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   695
structure PredicateCompFuns =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   696
struct
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   697
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   698
fun mk_predT T = Type (@{type_name Predicate.pred}, [T])
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   699
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   700
fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   701
  | dest_predT T = raise TYPE ("dest_predT", [T], []);
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   702
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   703
fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   704
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   705
fun mk_single t =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   706
  let val T = fastype_of t
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   707
  in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   708
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   709
fun mk_bind (x, f) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   710
  let val T as Type ("fun", [_, U]) = fastype_of f
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   711
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   712
    Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   713
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   714
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   715
val mk_sup = HOLogic.mk_binop @{const_name sup};
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   716
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   717
fun mk_if cond = Const (@{const_name Predicate.if_pred},
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   718
  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   719
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   720
fun mk_not t = let val T = mk_predT HOLogic.unitT
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   721
  in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   722
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   723
fun mk_Enum f =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   724
  let val T as Type ("fun", [T', _]) = fastype_of f
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   725
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   726
    Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f    
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   727
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   728
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   729
fun mk_Eval (f, x) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   730
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   731
    val T = fastype_of x
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   732
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   733
    Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   734
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   735
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   736
fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   737
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   738
fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   739
  (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   740
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   741
val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   742
  mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   743
  mk_map = mk_map};
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   744
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   745
end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   746
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   747
structure RandomPredCompFuns =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   748
struct
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   749
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   750
fun mk_randompredT T =
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   751
  @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed})
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   752
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   753
fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"},
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   754
  [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   755
  | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   756
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   757
fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   758
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   759
fun mk_single 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
   760
  let               
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   761
    val T = fastype_of t
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   762
  in
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   763
    Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   764
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   765
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   766
fun mk_bind (x, f) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   767
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   768
    val T as (Type ("fun", [_, U])) = fastype_of f
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   769
  in
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   770
    Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   771
  end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   772
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   773
val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union}
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   774
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   775
fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   776
  HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   777
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   778
fun mk_not t = let val T = mk_randompredT HOLogic.unitT
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   779
  in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   780
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   781
fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   782
  (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   783
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   784
val compfuns = CompilationFuns {mk_predT = mk_randompredT, dest_predT = dest_randompredT,
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   785
    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   786
    mk_not = mk_not, mk_map = mk_map};
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   787
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   788
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
   789
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   790
structure DSequence_CompFuns =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   791
struct
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   792
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   793
fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   794
  Type (@{type_name Option.option}, [Type  ("Lazy_Sequence.lazy_sequence", [T])])])])
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   795
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   796
fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   797
  Type (@{type_name Option.option}, [Type ("Lazy_Sequence.lazy_sequence", [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
   798
  | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   799
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   800
fun mk_bot T = Const ("DSequence.empty", mk_dseqT T);
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   801
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   802
fun mk_single t =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   803
  let val T = 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
   804
  in Const("DSequence.single", T --> mk_dseqT T) $ t end;
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   805
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   806
fun mk_bind (x, f) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   807
  let val T as Type ("fun", [_, U]) = fastype_of f
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   808
  in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   809
    Const ("DSequence.bind", fastype_of x --> T --> U) $ x $ f
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   810
  end;
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   811
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   812
val mk_sup = HOLogic.mk_binop "DSequence.union";
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   813
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   814
fun mk_if cond = Const ("DSequence.if_seq",
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   815
  HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   816
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   817
fun mk_not t = let val T = mk_dseqT HOLogic.unitT
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   818
  in Const ("DSequence.not_seq", T --> T) $ t end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   819
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   820
fun mk_map T1 T2 tf tp = Const ("DSequence.map",
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   821
  (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   822
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   823
val compfuns = CompilationFuns {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   824
    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   825
    mk_not = mk_not, mk_map = mk_map}
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   826
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   827
end;
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   828
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   829
structure Random_Sequence_CompFuns =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   830
struct
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   831
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   832
fun mk_random_dseqT T =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   833
  @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   834
    HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, @{typ Random.seed})
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   835
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   836
fun dest_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   837
  Type ("fun", [@{typ Random.seed},
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   838
  Type (@{type_name "*"}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   839
  | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   840
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   841
fun mk_bot T = Const ("Random_Sequence.empty", mk_random_dseqT T);
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   842
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   843
fun mk_single t =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   844
  let val T = 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
   845
  in Const("Random_Sequence.single", T --> mk_random_dseqT T) $ t end;
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   846
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   847
fun mk_bind (x, f) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   848
  let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   849
    val T as Type ("fun", [_, U]) = fastype_of f
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   850
  in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   851
    Const ("Random_Sequence.bind", fastype_of x --> T --> U) $ x $ f
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   852
  end;
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   853
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   854
val mk_sup = HOLogic.mk_binop "Random_Sequence.union";
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   855
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   856
fun mk_if cond = Const ("Random_Sequence.if_random_dseq",
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   857
  HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   858
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   859
fun mk_not t = let val T = mk_random_dseqT HOLogic.unitT
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   860
  in Const ("Random_Sequence.not_random_dseq", T --> T) $ t end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   861
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   862
fun mk_map T1 T2 tf tp = Const ("Random_Sequence.map",
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   863
  (T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   864
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   865
val compfuns = CompilationFuns {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT,
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   866
    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   867
    mk_not = mk_not, mk_map = mk_map}
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   868
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   869
end;
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   870
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   871
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   872
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   873
fun mk_random T =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   874
  let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   875
    val random = Const ("Quickcheck.random_class.random",
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   876
      @{typ code_numeral} --> @{typ Random.seed} -->
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   877
        HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed}))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   878
  in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   879
    Const ("Random_Sequence.Random", (@{typ code_numeral} --> @{typ Random.seed} -->
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   880
      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   881
      Random_Sequence_CompFuns.mk_random_dseqT T) $ random
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   882
  end;
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   883
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   884
(* for external use with interactive mode *)
32672
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   885
val pred_compfuns = PredicateCompFuns.compfuns
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   886
val randompred_compfuns = Random_Sequence_CompFuns.compfuns;
32672
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   887
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   888
(* function types and names of different compilations *)
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   889
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   890
fun funT_of compfuns mode T =
32672
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   891
  let
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   892
    val Ts = 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
   893
    val (inTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts
32672
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   894
  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
   895
    inTs ---> (mk_predT compfuns (HOLogic.mk_tupleT outTs))
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   896
  end;
32672
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   897
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   898
(** mode analysis **)
32672
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   899
35411
cafb74a131da made smlnj happy
bulwahn
parents: 35402
diff changeset
   900
type mode_analysis_options = {use_random : bool, reorder_premises : bool, infer_pos_and_neg_modes : bool}
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
   901
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   902
fun is_constrt thy =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   903
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   904
    val cnstrs = flat (maps
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   905
      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   906
      (Symtab.dest (Datatype.get_all thy)));
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   907
    fun check t = (case strip_comb t of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   908
        (Free _, []) => true
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   909
      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   910
            (SOME (i, Tname), Type (Tname', _)) =>
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   911
              length ts = i andalso Tname = Tname' andalso forall check ts
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   912
          | _ => false)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   913
      | _ => false)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   914
  in check end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   915
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   916
(*** check if a type is an equality type (i.e. doesn't contain fun)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   917
  FIXME this is only an approximation ***)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   918
fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   919
  | is_eqT _ = true;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   920
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   921
fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   922
val terms_vs = distinct (op =) o maps term_vs;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   923
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   924
(** collect all Frees in a term (with duplicates!) **)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   925
fun term_vTs tm =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   926
  fold_aterms (fn Free xT => cons xT | _ => I) tm [];
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   927
33138
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   928
fun subsets i j =
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   929
  if i <= j then
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   930
    let
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   931
      fun merge xs [] = xs
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   932
        | merge [] ys = ys
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   933
        | merge (x::xs) (y::ys) = if length x >= length y then x::merge xs (y::ys)
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   934
            else y::merge (x::xs) ys;
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   935
      val is = subsets (i+1) j
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   936
    in merge (map (fn ks => i::ks) is) is end
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   937
  else [[]];
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   938
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
   939
fun print_failed_mode options thy modes p (pol, m) rs is =
33130
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   940
  if show_mode_inference options then
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   941
    let
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   942
      val _ = tracing ("Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " 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
   943
        p ^ " violates mode " ^ string_of_mode m)
33130
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   944
    in () end
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   945
  else ()
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   946
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
   947
fun error_of p (pol, m) is =
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   948
  ("  Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " 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
   949
        p ^ " violates mode " ^ string_of_mode m)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   950
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   951
fun is_all_input mode =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   952
  let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   953
    fun is_all_input' (Fun _) = true
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   954
      | is_all_input' (Pair (m1, m2)) = is_all_input' m1 andalso is_all_input' m2
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   955
      | is_all_input' Input = true
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   956
      | is_all_input' Output = false
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   957
  in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   958
    forall is_all_input' (strip_fun_mode mode)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   959
  end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   960
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   961
fun all_input_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
   962
  let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   963
    val (Ts, U) = strip_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
   964
    fun input_of (Type ("*", [T1, T2])) = Pair (input_of T1, input_of T2)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   965
      | input_of _ = Input
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   966
  in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   967
    if U = HOLogic.boolT then
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   968
      fold_rev (curry Fun) (map input_of Ts) Bool
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   969
    else
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   970
      error "all_input_of: not a predicate"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   971
  end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   972
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   973
fun partial_hd [] = NONE
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   974
  | partial_hd (x :: xs) = SOME x
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   975
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   976
fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   977
val terms_vs = distinct (op =) o maps term_vs;
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   978
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   979
fun input_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
   980
  let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   981
    val (Ts, U) = strip_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
  in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   983
    fold_rev (curry Fun) (map (K Input) Ts) Input
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   984
  end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   985
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   986
fun output_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
  let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   988
    val (Ts, U) = strip_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
   989
  in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   990
    fold_rev (curry Fun) (map (K Output) Ts) Output
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   991
  end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   992
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   993
fun is_invertible_function thy (Const (f, _)) = is_constr thy f
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   994
  | is_invertible_function thy _ = false
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   995
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
   996
fun non_invertible_subterms thy (t as Free _) = []
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   997
  | non_invertible_subterms thy t = 
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   998
  case (strip_comb t) of (f, args) =>
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
   999
    if is_invertible_function thy f then
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1000
      maps (non_invertible_subterms thy) args
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1001
    else
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1002
      [t]
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1003
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1004
fun collect_non_invertible_subterms thy (f as Free _) (names, eqs) = (f, (names, eqs))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1005
  | collect_non_invertible_subterms thy t (names, eqs) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1006
    case (strip_comb t) of (f, args) =>
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1007
      if is_invertible_function thy f then
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1008
          let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1009
            val (args', (names', eqs')) =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1010
              fold_map (collect_non_invertible_subterms thy) args (names, eqs)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1011
          in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1012
            (list_comb (f, args'), (names', eqs'))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1013
          end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1014
        else
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1015
          let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1016
            val s = Name.variant names "x"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1017
            val v = Free (s, 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
  1018
          in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1019
            (v, (s :: names, HOLogic.mk_eq (v, t) :: eqs))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1020
          end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1021
(*
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1022
  if is_constrt thy t then (t, (names, eqs)) else
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1023
    let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1024
      val s = Name.variant names "x"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1025
      val v = Free (s, 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
  1026
    in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end;
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1027
*)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1028
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1029
fun is_possible_output thy vs t =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1030
  forall
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1031
    (fn t => is_eqT (fastype_of t) andalso forall (member (op =) vs) (term_vs t))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1032
      (non_invertible_subterms thy t)
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
  1033
  andalso
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
  1034
    (forall (is_eqT o snd)
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
  1035
      (inter (fn ((f', _), f) => f = f') vs (Term.add_frees t [])))
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1036
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1037
fun vars_of_destructable_term thy (Free (x, _)) = [x]
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1038
  | vars_of_destructable_term thy t =
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1039
  case (strip_comb t) of (f, args) =>
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1040
    if is_invertible_function thy f then
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1041
      maps (vars_of_destructable_term thy) args
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1042
    else
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1043
      []
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1044
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1045
fun is_constructable thy vs t = forall (member (op =) vs) (term_vs t)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1046
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1047
fun missing_vars vs t = subtract (op =) vs (term_vs t)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1048
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
  1049
fun output_terms (Const ("Pair", _) $ t1 $ t2, Mode_Pair (d1, d2)) =
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
    output_terms (t1, d1)  @ output_terms (t2, d2)
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
  1051
  | output_terms (t1 $ t2, Mode_App (d1, d2)) =
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
  1052
    output_terms (t1, d1)  @ output_terms (t2, d2)
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
  1053
  | output_terms (t, Term Output) = [t]
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
  1054
  | output_terms _ = []
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
  1055
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
  1056
fun lookup_mode modes (Const (s, T)) =
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
  1057
   (case (AList.lookup (op =) modes s) 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
  1058
      SOME ms => SOME (map (fn m => (Context m, [])) ms)
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
  1059
    | NONE => NONE)
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
  1060
  | lookup_mode modes (Free (x, _)) =
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
  1061
    (case (AList.lookup (op =) modes x) 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
  1062
      SOME ms => SOME (map (fn m => (Context m , [])) ms)
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
  1063
    | NONE => NONE)
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
  1064
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
  1065
fun derivations_of thy modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) =
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
    map_product
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1067
      (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1068
        (derivations_of thy modes vs t1 m1) (derivations_of thy modes vs t2 m2)
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
  1069
  | derivations_of thy modes vs t (m as Fun _) =
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
  1070
    (*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
  1071
      val (p, args) = strip_comb t
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
  1072
    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
  1073
      (case lookup_mode modes p 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
  1074
        SOME ms => map_filter (fn (Context m, []) => 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
  1075
          val ms = strip_fun_mode m
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
  1076
          val (argms, restms) = chop (length args) ms
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
  1077
          val m' = fold_rev (curry Fun) restms Bool
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
  1078
        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
  1079
          if forall (fn m => eq_mode (Input, m)) argms andalso eq_mode (m', mode) 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
  1080
            SOME (fold (curry Mode_App) (map Term argms) (Context m), missing_vars vs t)
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
  1081
          else NONE
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
  1082
        end) ms
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
  1083
      | NONE => (if is_all_input mode then [(Context mode, [])] 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
  1084
    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
  1085
    (case try (all_derivations_of thy modes vs) t  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
  1086
      SOME derivs =>
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
  1087
        filter (fn (d, mvars) => eq_mode (mode_of d, m) andalso null (output_terms (t, d))) derivs
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
  1088
    | NONE => (if is_all_input m then [(Context m, [])] else []))
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1089
  | derivations_of thy modes vs t 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
  1090
    if eq_mode (m, Input) 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
  1091
      [(Term Input, missing_vars vs t)]
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
  1092
    else if 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
  1093
      (if is_possible_output thy vs t then [(Term Output, [])] 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
  1094
    else []
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1095
and all_derivations_of thy modes vs (Const ("Pair", _) $ 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
  1096
  let
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1097
    val derivs1 = all_derivations_of thy modes vs t1
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1098
    val derivs2 = all_derivations_of thy modes vs t2
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1099
  in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1100
    map_product
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1101
      (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2))
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1102
        derivs1 derivs2
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1103
  end
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1104
  | all_derivations_of thy modes vs (t1 $ t2) =
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
  1105
  let
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1106
    val derivs1 = all_derivations_of thy modes vs t1
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1107
  in
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1108
    maps (fn (d1, mvars1) =>
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1109
      case mode_of d1 of
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1110
        Fun (m', _) => map (fn (d2, mvars2) =>
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1111
          (Mode_App (d1, d2), union (op =) mvars1 mvars2)) (derivations_of thy modes vs t2 m')
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1112
        | _ => error "Something went wrong") derivs1
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1113
  end
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
  1114
  | all_derivations_of thy modes vs (Const (s, T)) = the (lookup_mode modes (Const (s, T)))
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
  1115
  | all_derivations_of thy modes vs (Free (x, T)) = the (lookup_mode modes (Free (x, 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
  1116
  | all_derivations_of _ modes vs _ = error "all_derivations_of"
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1117
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1118
fun rev_option_ord ord (NONE, NONE) = EQUAL
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1119
  | rev_option_ord ord (NONE, SOME _) = GREATER
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1120
  | rev_option_ord ord (SOME _, NONE) = LESS
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1121
  | rev_option_ord ord (SOME x, SOME y) = ord (x, y)
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff changeset
  1122
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34028
diff c