src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
author haftmann
Fri, 22 Jan 2010 16:56:51 +0100
changeset 34962 807f6ce0273d
parent 34028 1e6206763036
child 34963 366a1a44aac2
permissions -rw-r--r--
HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
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
33623
4ec42d38224f changed modes to expected_modes; added UNION to code_pred_inlining; fixed some examples; tuned
bulwahn
parents: 33620
diff changeset
    12
  val values_cmd : string list -> Predicate_Compile_Aux.mode' option list option
33479
428ddcc16e7b added optional mode annotations for parameters in the values command
bulwahn
parents: 33478
diff changeset
    13
    -> int option * (bool * bool) -> int -> string -> Toplevel.state -> unit
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
    14
  val register_predicate : (string * thm list * thm * int) -> theory -> theory
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
    15
  val register_intros : string * thm list -> theory -> theory
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    16
  val is_registered : theory -> string -> bool
33328
1d93dd8a02c9 moved datatype mode and string functions to the auxillary structure
bulwahn
parents: 33327
diff changeset
    17
  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
    18
  val predfun_elim_of: theory -> string -> Predicate_Compile_Aux.mode -> thm
1d93dd8a02c9 moved datatype mode and string functions to the auxillary structure
bulwahn
parents: 33327
diff changeset
    19
  val predfun_name_of: theory -> string -> Predicate_Compile_Aux.mode -> string
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    20
  val all_preds_of : theory -> string list
33328
1d93dd8a02c9 moved datatype mode and string functions to the auxillary structure
bulwahn
parents: 33327
diff changeset
    21
  val modes_of: theory -> string -> Predicate_Compile_Aux.mode list
1d93dd8a02c9 moved datatype mode and string functions to the auxillary structure
bulwahn
parents: 33327
diff changeset
    22
  val depth_limited_modes_of: theory -> string -> Predicate_Compile_Aux.mode list
1d93dd8a02c9 moved datatype mode and string functions to the auxillary structure
bulwahn
parents: 33327
diff changeset
    23
  val depth_limited_function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
    24
  val random_modes_of: theory -> string -> Predicate_Compile_Aux.mode list
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
    25
  val random_function_name_of : theory -> string -> Predicate_Compile_Aux.mode -> string
33328
1d93dd8a02c9 moved datatype mode and string functions to the auxillary structure
bulwahn
parents: 33327
diff changeset
    26
  val all_modes_of : 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 nparams_of : theory -> string -> int
b70fe083694d moved values command from core to predicate compile
bulwahn
parents: 33476
diff changeset
    30
  val add_intro : thm -> theory -> theory
b70fe083694d moved values command from core to predicate compile
bulwahn
parents: 33476
diff changeset
    31
  val set_elim : thm -> theory -> theory
32668
b2de45007537 added first prototype of the extended predicate compiler
bulwahn
parents: 32667
diff changeset
    32
  val set_nparams : string -> int -> theory -> theory
33478
b70fe083694d moved values command from core to predicate compile
bulwahn
parents: 33476
diff changeset
    33
  val print_stored_rules : theory -> unit
b70fe083694d moved values command from core to predicate compile
bulwahn
parents: 33476
diff changeset
    34
  val print_all_modes : theory -> unit
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
    35
  val mk_casesrule : Proof.context -> term -> int -> thm list -> term
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
33628
ed2111a5c3ed renaming code_pred_intros to code_pred_intro
bulwahn
parents: 33626
diff changeset
    39
  val code_pred_intro_attrib : attribute
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    40
  (* used by Quickcheck_Generator *) 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    41
  (* temporary for testing of the compilation *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    42
  datatype compilation_funs = CompilationFuns of {
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    43
    mk_predT : typ -> typ,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    44
    dest_predT : typ -> typ,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    45
    mk_bot : typ -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    46
    mk_single : term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    47
    mk_bind : term * term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    48
    mk_sup : term * term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    49
    mk_if : term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    50
    mk_not : term -> term,
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
    51
    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
    52
  };
32672
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
    53
  val pred_compfuns : compilation_funs
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
    54
  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
    55
  val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
33132
07efd452a698 moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents: 33131
diff changeset
    56
  val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
    57
  val add_depth_limited_equations : Predicate_Compile_Aux.options
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
    58
    -> string list -> theory -> theory
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
    59
  val mk_tracing : string -> term -> term
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    60
end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    61
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    62
structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    63
struct
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    64
32668
b2de45007537 added first prototype of the extended predicate compiler
bulwahn
parents: 32667
diff changeset
    65
open Predicate_Compile_Aux;
33144
1831516747d4 removed obsolete GeneratorPrem; clean-up after modularization; tuned
bulwahn
parents: 33143
diff changeset
    66
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    67
(** auxiliary **)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    68
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    69
(* debug stuff *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    70
33108
9d9afd478016 added test for higher-order function inductification; added debug messages
bulwahn
parents: 33106
diff changeset
    71
fun print_tac s = Seq.single;
33139
9c01ee6f8ee9 added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents: 33138
diff changeset
    72
33127
eb91ec1ef6f0 added option show_proof_trace
bulwahn
parents: 33126
diff changeset
    73
fun print_tac' options s = 
eb91ec1ef6f0 added option show_proof_trace
bulwahn
parents: 33126
diff changeset
    74
  if show_proof_trace options then Tactical.print_tac s else Seq.single;
eb91ec1ef6f0 added option show_proof_trace
bulwahn
parents: 33126
diff changeset
    75
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    76
fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    77
33108
9d9afd478016 added test for higher-order function inductification; added debug messages
bulwahn
parents: 33106
diff changeset
    78
datatype assertion = Max_number_of_subgoals of int
9d9afd478016 added test for higher-order function inductification; added debug messages
bulwahn
parents: 33106
diff changeset
    79
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
    80
  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
    81
  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
    82
    ^ "\n" ^ Pretty.string_of (Pretty.chunks
9d9afd478016 added test for higher-order function inductification; added debug messages
bulwahn
parents: 33106
diff changeset
    83
      (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
    84
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    85
(** fundamentals **)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    86
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    87
(* syntactic operations *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    88
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    89
fun mk_eq (x, xs) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    90
  let fun mk_eqs _ [] = []
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    91
        | mk_eqs a (b::cs) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    92
            HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    93
  in mk_eqs x xs end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    94
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    95
fun mk_scomp (t, u) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    96
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    97
    val T = fastype_of t
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    98
    val U = fastype_of u
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
    99
    val [A] = binder_types T
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   100
    val D = body_type U 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   101
  in 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   102
    Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   103
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   104
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   105
fun dest_funT (Type ("fun",[S, T])) = (S, T)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   106
  | dest_funT T = raise TYPE ("dest_funT", [T], [])
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   107
 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   108
fun mk_fun_comp (t, u) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   109
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   110
    val (_, B) = dest_funT (fastype_of t)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   111
    val (C, A) = dest_funT (fastype_of u)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   112
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   113
    Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   114
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   115
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   116
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
   117
  Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   118
  | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   119
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   120
fun mk_tracing s t =
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   121
  Const(@{const_name Code_Evaluation.tracing},
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   122
    @{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
   123
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   124
(* destruction of intro rules *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   125
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   126
(* FIXME: look for other place where this functionality was used before *)
33619
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   127
fun strip_intro_concl nparams intro =
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   128
  let
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   129
    val _ $ u = Logic.strip_imp_concl intro
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   130
    val (pred, all_args) = strip_comb u
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   131
    val (params, args) = chop nparams all_args
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   132
  in (pred, (params, args)) end
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   133
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   134
(** data structures **)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   135
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   136
fun gen_split_smode (mk_tuple, strip_tuple) smode ts =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   137
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   138
    fun split_tuple' _ _ [] = ([], [])
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   139
    | split_tuple' is i (t::ts) =
33629
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   140
      (if member (op =) is i then apfst else apsnd) (cons t)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   141
        (split_tuple' is (i+1) ts)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   142
    fun split_tuple is t = split_tuple' is 1 (strip_tuple t)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   143
    fun split_smode' _ _ [] = ([], [])
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   144
      | split_smode' smode i (t::ts) =
33629
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   145
        (if member (op =) (map fst smode) i then
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   146
          case (the (AList.lookup (op =) smode i)) of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   147
            NONE => apfst (cons t)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   148
            | SOME is =>
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   149
              let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   150
                val (ts1, ts2) = split_tuple is t
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   151
                fun cons_tuple ts = if null ts then I else cons (mk_tuple ts)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   152
                in (apfst (cons_tuple ts1)) o (apsnd (cons_tuple ts2)) end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   153
          else apsnd (cons t))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   154
        (split_smode' smode (i+1) ts)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   155
  in split_smode' smode 1 ts end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   156
33330
d6eb7f19bfc6 encapsulating records with datatype constructors and adding type annotations to make SML/NJ happy
bulwahn
parents: 33328
diff changeset
   157
fun split_smode smode ts = gen_split_smode (HOLogic.mk_tuple, HOLogic.strip_tuple) smode ts
d6eb7f19bfc6 encapsulating records with datatype constructors and adding type annotations to make SML/NJ happy
bulwahn
parents: 33328
diff changeset
   158
fun split_smodeT smode ts = gen_split_smode (HOLogic.mk_tupleT, HOLogic.strip_tupleT) smode ts
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   159
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   160
fun gen_split_mode split_smode (iss, is) ts =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   161
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   162
    val (t1, t2) = chop (length iss) ts 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   163
  in (t1, split_smode is t2) end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   164
33330
d6eb7f19bfc6 encapsulating records with datatype constructors and adding type annotations to make SML/NJ happy
bulwahn
parents: 33328
diff changeset
   165
fun split_mode (iss, is) ts = gen_split_mode split_smode (iss, is) ts
d6eb7f19bfc6 encapsulating records with datatype constructors and adding type annotations to make SML/NJ happy
bulwahn
parents: 33328
diff changeset
   166
fun split_modeT (iss, is) ts = gen_split_mode split_smodeT (iss, is) ts
32668
b2de45007537 added first prototype of the extended predicate compiler
bulwahn
parents: 32667
diff changeset
   167
33144
1831516747d4 removed obsolete GeneratorPrem; clean-up after modularization; tuned
bulwahn
parents: 33143
diff changeset
   168
datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term
1831516747d4 removed obsolete GeneratorPrem; clean-up after modularization; tuned
bulwahn
parents: 33143
diff changeset
   169
  | Generator of (string * typ);
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   170
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   171
type moded_clause = term list * (indprem * tmode) list
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   172
type 'a pred_mode_table = (string * (mode * 'a) list) list
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   173
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   174
datatype predfun_data = PredfunData of {
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   175
  name : string,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   176
  definition : thm,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   177
  intro : thm,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   178
  elim : thm
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   179
};
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   180
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   181
fun rep_predfun_data (PredfunData data) = data;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   182
fun mk_predfun_data (name, definition, intro, elim) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   183
  PredfunData {name = name, definition = definition, intro = intro, elim = elim}
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   184
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   185
datatype function_data = FunctionData of {
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   186
  name : string,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   187
  equation : thm option (* is not used at all? *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   188
};
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   189
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   190
fun rep_function_data (FunctionData data) = data;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   191
fun mk_function_data (name, equation) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   192
  FunctionData {name = name, equation = equation}
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   193
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   194
datatype pred_data = PredData of {
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   195
  intros : thm list,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   196
  elim : thm option,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   197
  nparams : int,
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
   198
  functions : bool * (mode * predfun_data) list,
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
   199
  random_functions : bool * (mode * function_data) list,
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
   200
  depth_limited_functions : bool * (mode * function_data) list,
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
   201
  annotated_functions : bool * (mode * function_data) list
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   202
};
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   203
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   204
fun rep_pred_data (PredData data) = data;
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   205
fun mk_pred_data ((intros, elim, nparams),
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
   206
  (functions, random_functions, depth_limited_functions, annotated_functions)) =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   207
  PredData {intros = intros, elim = elim, nparams = nparams,
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
   208
    functions = functions, random_functions = random_functions,
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   209
    depth_limited_functions = depth_limited_functions, annotated_functions = annotated_functions}
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   210
fun map_pred_data f (PredData {intros, elim, nparams,
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
   211
  functions, random_functions, depth_limited_functions, annotated_functions}) =
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
   212
  mk_pred_data (f ((intros, elim, nparams), (functions, random_functions,
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   213
    depth_limited_functions, annotated_functions)))
33144
1831516747d4 removed obsolete GeneratorPrem; clean-up after modularization; tuned
bulwahn
parents: 33143
diff changeset
   214
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   215
fun eq_option eq (NONE, NONE) = true
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   216
  | eq_option eq (SOME x, SOME y) = eq (x, y)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   217
  | eq_option eq _ = false
33144
1831516747d4 removed obsolete GeneratorPrem; clean-up after modularization; tuned
bulwahn
parents: 33143
diff changeset
   218
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   219
fun eq_pred_data (PredData d1, PredData d2) = 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   220
  eq_list (Thm.eq_thm) (#intros d1, #intros d2) andalso
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   221
  eq_option (Thm.eq_thm) (#elim d1, #elim d2) andalso
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   222
  #nparams d1 = #nparams d2
33144
1831516747d4 removed obsolete GeneratorPrem; clean-up after modularization; tuned
bulwahn
parents: 33143
diff changeset
   223
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33519
diff changeset
   224
structure PredData = Theory_Data
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   225
(
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   226
  type T = pred_data Graph.T;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   227
  val empty = Graph.empty;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   228
  val extend = I;
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33519
diff changeset
   229
  val merge = Graph.merge eq_pred_data;
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   230
);
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   231
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   232
(* queries *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   233
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   234
fun lookup_pred_data thy name =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   235
  Option.map rep_pred_data (try (Graph.get_node (PredData.get thy)) name)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   236
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   237
fun the_pred_data thy name = case lookup_pred_data thy name
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   238
 of NONE => error ("No such predicate " ^ quote name)  
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   239
  | SOME data => data;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   240
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   241
val is_registered = is_some oo lookup_pred_data 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   242
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   243
val all_preds_of = Graph.keys o PredData.get
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   244
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   245
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
   246
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   247
fun the_elim_of thy name = case #elim (the_pred_data thy name)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   248
 of NONE => error ("No elimination rule for predicate " ^ quote name)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   249
  | SOME thm => Thm.transfer thy thm 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   250
  
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   251
val has_elim = is_some o #elim oo the_pred_data;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   252
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   253
val nparams_of = #nparams oo the_pred_data
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   254
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
   255
val modes_of = (map fst) o snd o #functions oo the_pred_data
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   256
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   257
fun all_modes_of thy = map (fn name => (name, modes_of thy name)) (all_preds_of thy) 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   258
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
   259
val defined_functions = fst o #functions oo the_pred_data
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   260
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   261
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
   262
  Option.map rep_predfun_data
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
   263
    (AList.lookup (op =) (snd (#functions (the_pred_data thy name))) mode)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   264
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   265
fun the_predfun_data thy name mode = case lookup_predfun_data thy name 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
   266
  of NONE => error ("No function defined for mode " ^ string_of_mode thy name mode ^
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   267
    " of predicate " ^ name)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   268
   | SOME data => data;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   269
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   270
val predfun_name_of = #name ooo the_predfun_data
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   271
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   272
val predfun_definition_of = #definition ooo the_predfun_data
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   273
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   274
val predfun_intro_of = #intro ooo the_predfun_data
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   275
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   276
val predfun_elim_of = #elim ooo the_predfun_data
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   277
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
   278
fun lookup_random_function_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_function_data
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
   280
  (AList.lookup (op =) (snd (#random_functions (the_pred_data thy name))) mode)
33144
1831516747d4 removed obsolete GeneratorPrem; clean-up after modularization; tuned
bulwahn
parents: 33143
diff changeset
   281
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
   282
fun the_random_function_data thy name mode = case lookup_random_function_data thy name mode of
33619
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   283
     NONE => error ("No random function defined for mode " ^ string_of_mode thy name mode ^
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
   284
       " of predicate " ^ name)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   285
   | SOME data => data
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   286
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
   287
val random_function_name_of = #name ooo the_random_function_data
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   288
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
   289
val random_modes_of = (map fst) o snd o #random_functions oo the_pred_data
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   290
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
   291
val defined_random_functions = fst o #random_functions oo the_pred_data
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   292
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
   293
fun all_random_modes_of thy =
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
   294
  map (fn name => (name, random_modes_of thy name)) (all_preds_of thy) 
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   295
33134
88c9c3460fe7 renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler
bulwahn
parents: 33133
diff changeset
   296
fun lookup_depth_limited_function_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
   297
  Option.map rep_function_data
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
   298
    (AList.lookup (op =) (snd (#depth_limited_functions (the_pred_data thy name))) mode)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   299
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   300
fun the_depth_limited_function_data thy name mode =
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   301
  case lookup_depth_limited_function_data thy name mode of
33619
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   302
    NONE => error ("No depth-limited function defined for mode " ^ string_of_mode thy name mode
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   303
      ^ " of predicate " ^ name)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   304
   | SOME data => data
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   305
33134
88c9c3460fe7 renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler
bulwahn
parents: 33133
diff changeset
   306
val depth_limited_function_name_of = #name ooo the_depth_limited_function_data
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   307
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
   308
val depth_limited_modes_of = (map fst) o snd o #depth_limited_functions oo the_pred_data
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
   309
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
   310
val defined_depth_limited_functions = fst o #depth_limited_functions oo the_pred_data
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
   311
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   312
fun lookup_annotated_function_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
   313
  Option.map rep_function_data
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
   314
    (AList.lookup (op =) (snd (#annotated_functions (the_pred_data thy name))) mode)
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   315
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   316
fun the_annotated_function_data thy name mode = case lookup_annotated_function_data thy name 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
   317
  of NONE => error ("No annotated function defined for mode " ^ string_of_mode thy name mode
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   318
    ^ " of predicate " ^ name)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   319
   | SOME data => data
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   320
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
   321
val annotated_function_name_of = #name ooo the_annotated_function_data
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   322
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
   323
val annotated_modes_of = (map fst) o snd o #annotated_functions oo the_pred_data
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
   324
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
   325
val defined_annotated_functions = fst o #annotated_functions oo the_pred_data
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   326
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   327
(* diagnostic display functions *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   328
33619
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   329
fun print_modes options thy modes =
33251
4b13ab778b78 added option show_modes to predicate compiler
bulwahn
parents: 33250
diff changeset
   330
  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
   331
    tracing ("Inferred modes:\n" ^
33251
4b13ab778b78 added option show_modes to predicate compiler
bulwahn
parents: 33250
diff changeset
   332
      cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
33619
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   333
        (string_of_mode thy s) ms)) modes))
33251
4b13ab778b78 added option show_modes to predicate compiler
bulwahn
parents: 33250
diff changeset
   334
  else ()
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   335
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   336
fun print_pred_mode_table string_of_entry thy pred_mode_table =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   337
  let
33619
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   338
    fun print_mode pred (mode, entry) =  "mode : " ^ string_of_mode thy pred mode
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   339
      ^ string_of_entry pred mode entry
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   340
    fun print_pred (pred, modes) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   341
      "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
   342
    val _ = tracing (cat_lines (map print_pred pred_mode_table))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   343
  in () end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   344
33130
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   345
fun string_of_prem thy (Prem (ts, p)) =
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   346
    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^ "(premise)"
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   347
  | string_of_prem thy (Negprem (ts, p)) =
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   348
    (Syntax.string_of_term_global thy (HOLogic.mk_not (list_comb (p, ts)))) ^ "(negative premise)"
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   349
  | string_of_prem thy (Sidecond t) =
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   350
    (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
   351
  | 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
   352
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   353
fun string_of_moded_prem thy (Prem (ts, p), tmode) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   354
    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   355
    "(" ^ (string_of_tmode tmode) ^ ")"
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   356
  | string_of_moded_prem thy (Generator (v, T), _) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   357
    "Generator for " ^ v ^ " of Type " ^ (Syntax.string_of_typ_global thy T)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   358
  | string_of_moded_prem thy (Negprem (ts, p), Mode (_, is, _)) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   359
    (Syntax.string_of_term_global thy (list_comb (p, ts))) ^
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   360
    "(negative mode: " ^ string_of_smode is ^ ")"
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   361
  | string_of_moded_prem thy (Sidecond t, Mode (_, is, _)) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   362
    (Syntax.string_of_term_global thy t) ^
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   363
    "(sidecond mode: " ^ string_of_smode is ^ ")"    
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   364
  | string_of_moded_prem _ _ = error "string_of_moded_prem: unimplemented"
33130
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   365
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   366
fun print_moded_clauses thy =
33130
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   367
  let
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   368
    fun string_of_clause pred mode clauses =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   369
      cat_lines (map (fn (ts, prems) => (space_implode " --> "
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   370
        (map (string_of_moded_prem thy) prems)) ^ " --> " ^ pred ^ " "
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   371
        ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts))) clauses)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   372
  in print_pred_mode_table string_of_clause thy end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   373
33130
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   374
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
   375
  (space_implode " --> "
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
   376
  (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
   377
   ^ (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
   378
33139
9c01ee6f8ee9 added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents: 33138
diff changeset
   379
fun print_compiled_terms options thy =
9c01ee6f8ee9 added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents: 33138
diff changeset
   380
  if show_compilation options then
9c01ee6f8ee9 added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents: 33138
diff changeset
   381
    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
   382
  else K ()
9c01ee6f8ee9 added skip_proof option; playing with compilation of depth-limited predicates
bulwahn
parents: 33138
diff changeset
   383
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   384
fun print_stored_rules thy =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   385
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   386
    val preds = (Graph.keys o PredData.get) thy
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   387
    fun print pred () = let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   388
      val _ = writeln ("predicate: " ^ pred)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   389
      val _ = writeln ("number of parameters: " ^ string_of_int (nparams_of thy pred))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   390
      val _ = writeln ("introrules: ")
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   391
      val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   392
        (rev (intros_of thy pred)) ()
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   393
    in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   394
      if (has_elim thy pred) then
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   395
        writeln ("elimrule: " ^ Display.string_of_thm_global thy (the_elim_of thy pred))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   396
      else
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   397
        writeln ("no elimrule defined")
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   398
    end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   399
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   400
    fold print preds ()
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   401
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   402
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   403
fun print_all_modes thy =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   404
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   405
    val _ = writeln ("Inferred modes:")
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   406
    fun print (pred, modes) u =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   407
      let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   408
        val _ = writeln ("predicate: " ^ pred)
33619
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   409
        val _ = writeln ("modes: " ^ (commas (map (string_of_mode thy pred) modes)))
d93a3cb55068 first steps towards a new mode datastructure; new syntax for mode annotations and new output of modes
bulwahn
parents: 33526
diff changeset
   410
      in u end
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   411
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   412
    fold print (all_modes_of thy) ()
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   413
  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
   414
33132
07efd452a698 moved argument expected_modes into options; improved mode check to only check mode of the named predicate
bulwahn
parents: 33131
diff changeset
   415
(* validity checks *)
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   416
(* 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
   417
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   418
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
   419
  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
   420
    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
   421
      SOME modes =>
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   422
        let
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   423
          val modes' = map (translate_mode (the (AList.lookup (op =) preds s))) modes
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   424
        in
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   425
          if not (eq_set eq_mode' (ms, modes')) then
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   426
            error ("expected modes were not inferred:\n"
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   427
            ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode' modes')  ^ "\n"
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   428
            ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode' ms))
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   429
          else ()
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   430
        end
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   431
      | NONE => ())
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   432
  | NONE => ()
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   433
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   434
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
   435
  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
   436
    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
   437
      SOME inferred_ms =>
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   438
        let
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   439
          val preds_without_modes = map fst (filter (null o snd) (modes @ extra_modes))
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   440
          val modes' = map (translate_mode (the (AList.lookup (op =) preds s))) inferred_ms
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   441
        in
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   442
          if not (eq_set eq_mode' (ms, modes')) then
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   443
            error ("expected modes were not inferred:\n"
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   444
            ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode' modes')  ^ "\n"
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   445
            ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode' ms) ^ "\n"
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   446
            ^ "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
   447
            ^ cat_lines errors ^
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   448
            (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
   449
              "\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
   450
            else ""))
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   451
          else ()
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   452
        end
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   453
      | NONE => ())
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   454
  | 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
   455
33144
1831516747d4 removed obsolete GeneratorPrem; clean-up after modularization; tuned
bulwahn
parents: 33143
diff changeset
   456
(* 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
   457
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
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
   459
  (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
   460
     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
   461
     fun varify (t, (i, 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
   462
       let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify [] 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
   463
       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
   464
     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
   465
     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
   466
     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
   467
     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
   468
     fun unify (cname, cT) =
33317
b4534348b8fd standardized filter/filter_out;
wenzelm
parents: 33268
diff changeset
   469
       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
   470
       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
   471
     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
   472
     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
   473
   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
   474
   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
   475
     (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
   476
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   477
fun import_intros inp_pred nparams [] ctxt =
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   478
  let
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   479
    val ([outp_pred], ctxt') = Variable.import_terms false [inp_pred] ctxt
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   480
    val (paramTs, _) = chop nparams (binder_types (fastype_of outp_pred))
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   481
    val (param_names, ctxt'') = Variable.variant_fixes (map (fn i => "p" ^ (string_of_int i))
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   482
      (1 upto nparams)) ctxt'
33629
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   483
    val params = map2 (curry Free) param_names paramTs
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   484
    in (((outp_pred, params), []), ctxt') end
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   485
  | import_intros inp_pred nparams (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
   486
    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
   487
      val ((_, [th']), ctxt') = Variable.import false [th] 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
   488
      val thy = ProofContext.theory_of 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
   489
      val (pred, (params, args)) = strip_intro_concl nparams (prop_of 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
   490
      val ho_args = filter (is_predT o fastype_of) args
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   491
      fun subst_of (pred', pred) =
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   492
        let
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   493
          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
   494
        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
   495
      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
   496
        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
   497
          val (pred', _) = strip_intro_concl 0 (prop_of 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
   498
          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
   499
            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
   500
        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
   501
      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
   502
        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
   503
          val (_, (params', args')) = strip_intro_concl nparams (prop_of 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
   504
          val ho_args' = map dest_Var (filter (is_predT o fastype_of) args')
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   505
        in Thm.certify_instantiate ([], map dest_Var params' ~~ params) th end
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   506
      val outp_pred =
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   507
        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
   508
      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
   509
        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
   510
    in
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   511
      (((outp_pred, params), 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
   512
    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
   513
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
(* 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
   515
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   516
fun mk_casesrule ctxt pred nparams 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
   517
  let
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   518
    val (((pred, params), intros_th), ctxt1) = import_intros pred nparams 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
   519
    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
   520
    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
   521
    val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   522
    val (_, argsT) = chop nparams (binder_types (fastype_of 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
   523
    val (argnames, ctxt3) = Variable.variant_fixes
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   524
      (map (fn i => "a" ^ string_of_int i) (1 upto length argsT)) ctxt2
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   525
    val argvs = map2 (curry Free) argnames argsT
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
   526
    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
   527
      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
   528
        val (_, (_, args)) = strip_intro_concl nparams 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
   529
        val prems = Logic.strip_imp_prems intro
33629
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   530
        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
   531
        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
   532
          (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
   533
              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
   534
           | _ => 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
   535
      in fold Logic.all frees (Logic.list_implies (eqprems @ prems, 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
   536
    val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
3085da75ed54 changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
bulwahn
parents: 33128
diff changeset
   537
    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
   538
  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
   539
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   540
(** preprocessing rules **)  
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   541
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   542
fun imp_prems_conv cv ct =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   543
  case Thm.term_of ct of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   544
    Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   545
  | _ => Conv.all_conv ct
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   546
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   547
fun Trueprop_conv cv ct =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   548
  case Thm.term_of ct of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   549
    Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct  
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   550
  | _ => error "Trueprop_conv"
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   551
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   552
fun preprocess_intro thy rule =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   553
  Conv.fconv_rule
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   554
    (imp_prems_conv
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   555
      (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
   556
    (Thm.transfer thy rule)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   557
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   558
fun preprocess_elim thy nparams elimrule =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   559
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   560
    fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   561
       HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   562
     | replace_eqs t = t
33128
1f990689349f further cleaning up
bulwahn
parents: 33127
diff changeset
   563
    val ctxt = ProofContext.init thy
1f990689349f further cleaning up
bulwahn
parents: 33127
diff changeset
   564
    val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt
1f990689349f further cleaning up
bulwahn
parents: 33127
diff changeset
   565
    val prems = Thm.prems_of elimrule
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   566
    val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems)))) - nparams
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   567
    fun preprocess_case t =
33128
1f990689349f further cleaning up
bulwahn
parents: 33127
diff changeset
   568
      let
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   569
       val params = Logic.strip_params t
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   570
       val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   571
       val assums_hyp' = assums1 @ (map replace_eqs assums2)
33128
1f990689349f further cleaning up
bulwahn
parents: 33127
diff changeset
   572
      in
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   573
       list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t))
33128
1f990689349f further cleaning up
bulwahn
parents: 33127
diff changeset
   574
      end
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   575
    val cases' = map preprocess_case (tl prems)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   576
    val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   577
    val bigeq = (Thm.symmetric (Conv.implies_concl_conv
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   578
      (MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}])
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   579
        (cterm_of thy elimrule')))
33150
75eddea4abef further changes due to the previous merge in the predicate compiler
bulwahn
parents: 33149
diff changeset
   580
    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
   581
    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
   582
  in
33109
7025bc7a5054 changed elimination preprocessing due to an error with a JinjaThread predicate
bulwahn
parents: 33108
diff changeset
   583
    Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   584
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   585
33124
5378e61add1a continued cleaning up; moved tuple expanding to core
bulwahn
parents: 33123
diff changeset
   586
fun expand_tuples_elim th = th
5378e61add1a continued cleaning up; moved tuple expanding to core
bulwahn
parents: 33123
diff changeset
   587
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
   588
(* updaters *)
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
   589
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
   590
fun apfst4 f (x1, x2, x3, x4) = (f x1, x2, x3, x4)
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
   591
fun apsnd4 f (x1, x2, x3, x4) = (x1, f x2, x3, x4)
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
   592
fun aptrd4 f (x1, x2, x3, x4) = (x1, x2, f x3, x4)
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
   593
fun apfourth4 f (x1, x2, x3, x4) = (x1, x2, x3, f x4)
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
   594
fun appair f g (x, y) = (f x, g x)
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
   595
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
   596
val no_compilation = ((false, []), (false, []), (false, []), (false, []))
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
   597
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   598
fun fetch_pred_data thy name =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   599
  case try (Inductive.the_inductive (ProofContext.init thy)) name of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   600
    SOME (info as (_, result)) => 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   601
      let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   602
        fun is_intro_of intro =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   603
          let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   604
            val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   605
          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
   606
        val intros =
33124
5378e61add1a continued cleaning up; moved tuple expanding to core
bulwahn
parents: 33123
diff changeset
   607
          (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
   608
        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
   609
        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
   610
        val pred = nth (#preds result) index
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   611
        val nparams = length (Inductive.params_of (#raw_induct result))
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   612
        (*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
   613
          (expand_tuples_elim pre_elim))*)
5378e61add1a continued cleaning up; moved tuple expanding to core
bulwahn
parents: 33123
diff changeset
   614
        val elim =
33150
75eddea4abef further changes due to the previous merge in the predicate compiler
bulwahn
parents: 33149
diff changeset
   615
          (Drule.standard o Skip_Proof.make_thm thy)
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   616
          (mk_casesrule (ProofContext.init thy) pred nparams intros)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   617
      in
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
   618
        mk_pred_data ((intros, SOME elim, nparams), no_compilation)
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
   619
      end
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   620
  | NONE => error ("No such predicate: " ^ quote name)
33124
5378e61add1a continued cleaning up; moved tuple expanding to core
bulwahn
parents: 33123
diff changeset
   621
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   622
fun add_predfun name mode data =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   623
  let
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
   624
    val add = (apsnd o apfst4) (fn (x, y) => (true, cons (mode, mk_predfun_data data) y))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   625
  in PredData.map (Graph.map_node name (map_pred_data add)) end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   626
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   627
fun is_inductive_predicate thy name =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   628
  is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   629
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   630
fun depending_preds_of thy (key, value) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   631
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   632
    val intros = (#intros o rep_pred_data) value
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   633
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   634
    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
   635
      |> filter (fn c => (not (c = key)) andalso
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   636
        (is_inductive_predicate thy c orelse is_registered thy c))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   637
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   638
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   639
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   640
(* code dependency graph *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   641
(*
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   642
fun dependencies_of thy name =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   643
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   644
    val (intros, elim, nparams) = fetch_pred_data thy name 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   645
    val data = mk_pred_data ((intros, SOME elim, nparams), ([], [], []))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   646
    val keys = depending_preds_of thy intros
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   647
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   648
    (data, keys)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   649
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   650
*)
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   651
33629
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   652
fun add_intro thm thy =
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   653
  let
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   654
    val (name, T) = dest_Const (fst (strip_intro_concl 0 (prop_of thm)))
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   655
    fun cons_intro gr =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   656
     case try (Graph.get_node gr) name of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   657
       SOME pred_data => Graph.map_node name (map_pred_data
33326
7d0288d90535 improved handling of alternative rules; added test cases for alternative rules; normalized tracing in the predicate compiler
bulwahn
parents: 33268
diff changeset
   658
         (apfst (fn (intros, elim, nparams) => (intros @ [thm], elim, nparams)))) gr
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   659
     | NONE =>
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   660
       let
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   661
         val nparams = the_default (guess_nparams T)
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   662
           (try (#nparams o rep_pred_data o (fetch_pred_data thy)) name)
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
   663
       in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), no_compilation)) gr end;
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   664
  in PredData.map cons_intro thy end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   665
33629
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   666
fun set_elim thm =
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   667
  let
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   668
    val (name, _) = dest_Const (fst 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   669
      (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   670
    fun set (intros, _, nparams) = (intros, SOME thm, nparams)  
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   671
  in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   672
33629
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   673
fun set_nparams name nparams =
5f35cf91c6a4 improving code quality thanks to Florian's code review
bulwahn
parents: 33628
diff changeset
   674
  let
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   675
    fun set (intros, elim, _ ) = (intros, elim, nparams) 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   676
  in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   677
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   678
fun register_predicate (constname, pre_intros, pre_elim, nparams) thy =
32668
b2de45007537 added first prototype of the extended predicate compiler
bulwahn
parents: 32667
diff changeset
   679
  let
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   680
    (* preprocessing *)
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   681
    val intros = map (preprocess_intro thy) pre_intros
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
   682
    val elim = preprocess_elim thy nparams pre_elim
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   683
  in
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   684
    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
   685
      PredData.map
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   686
        (Graph.new_node (constname,
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
   687
          mk_pred_data ((intros, SOME elim, nparams), no_compilation))) thy
32668
b2de45007537 added first prototype of the extended predicate compiler
bulwahn
parents: 32667
diff changeset
   688
    else thy
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   689
  end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   690
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   691
fun register_intros (constname, pre_intros) thy =
32668
b2de45007537 added first prototype of the extended predicate compiler
bulwahn
parents: 32667
diff changeset
   692
  let
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   693
    val T = Sign.the_const_type thy constname
33120
ca77d8c34ce2 cleaned up
bulwahn
parents: 33118
diff changeset
   694
    fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl 0 (prop_of intr))))
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   695
    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
   696
      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
   697
        "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
   698
          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
   699
      else ()
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   700
    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
   701
    val nparams = guess_nparams T
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   702
    val pre_elim = 
33150
75eddea4abef further changes due to the previous merge in the predicate compiler
bulwahn
parents: 33149
diff changeset
   703
      (Drule.standard o Skip_Proof.make_thm thy)
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   704
      (mk_casesrule (ProofContext.init thy) pred nparams pre_intros)
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
   705
  in register_predicate (constname, pre_intros, pre_elim, nparams) thy end
32668
b2de45007537 added first prototype of the extended predicate compiler
bulwahn
parents: 32667
diff changeset
   706
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
   707
fun set_random_function_name pred mode name = 
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   708
  let
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
   709
    val set = (apsnd o apsnd4) (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   710
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   711
    PredData.map (Graph.map_node pred (map_pred_data set))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   712
  end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   713
33134
88c9c3460fe7 renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler
bulwahn
parents: 33133
diff changeset
   714
fun set_depth_limited_function_name pred mode name = 
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   715
  let
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
   716
    val set = (apsnd o aptrd4) (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y))
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   717
  in
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   718
    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
   719
  end
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   720
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   721
fun set_annotated_function_name pred mode name =
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   722
  let
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
   723
    val set = (apsnd o apfourth4)
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
   724
      (fn (x, y) => (true, cons (mode, mk_function_data (name, NONE)) y))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   725
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   726
    PredData.map (Graph.map_node pred (map_pred_data set))
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
datatype compilation_funs = CompilationFuns of {
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   730
  mk_predT : typ -> typ,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   731
  dest_predT : typ -> typ,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   732
  mk_bot : typ -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   733
  mk_single : term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   734
  mk_bind : term * term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   735
  mk_sup : term * term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   736
  mk_if : term -> term,
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   737
  mk_not : term -> term,
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   738
  mk_map : typ -> typ -> term -> term -> term
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   739
};
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   740
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   741
fun mk_predT (CompilationFuns funs) = #mk_predT funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   742
fun dest_predT (CompilationFuns funs) = #dest_predT funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   743
fun mk_bot (CompilationFuns funs) = #mk_bot funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   744
fun mk_single (CompilationFuns funs) = #mk_single funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   745
fun mk_bind (CompilationFuns funs) = #mk_bind funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   746
fun mk_sup (CompilationFuns funs) = #mk_sup funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   747
fun mk_if (CompilationFuns funs) = #mk_if funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   748
fun mk_not (CompilationFuns funs) = #mk_not funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   749
fun mk_map (CompilationFuns funs) = #mk_map funs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   750
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   751
structure PredicateCompFuns =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   752
struct
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   753
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   754
fun mk_predT T = Type (@{type_name Predicate.pred}, [T])
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   755
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   756
fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   757
  | dest_predT T = raise TYPE ("dest_predT", [T], []);
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   758
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   759
fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   760
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   761
fun mk_single t =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   762
  let val T = fastype_of t
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   763
  in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   764
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   765
fun mk_bind (x, f) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   766
  let val T as Type ("fun", [_, U]) = fastype_of f
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   767
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   768
    Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   769
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   770
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   771
val mk_sup = HOLogic.mk_binop @{const_name sup};
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   772
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   773
fun mk_if cond = Const (@{const_name Predicate.if_pred},
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   774
  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   775
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   776
fun mk_not t = let val T = mk_predT HOLogic.unitT
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   777
  in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   778
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   779
fun mk_Enum f =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   780
  let val T as Type ("fun", [T', _]) = fastype_of f
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   781
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   782
    Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f    
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   783
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   784
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   785
fun mk_Eval (f, x) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   786
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   787
    val T = fastype_of x
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   788
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   789
    Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   790
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   791
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   792
fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   793
  (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   794
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   795
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
   796
  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
   797
  mk_map = mk_map};
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   798
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   799
end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   800
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   801
structure RandomPredCompFuns =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   802
struct
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   803
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   804
fun mk_randompredT T =
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   805
  @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed})
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   806
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   807
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
   808
  [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
   809
  | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   810
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   811
fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   812
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   813
fun mk_single t =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   814
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   815
    val T = fastype_of t
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   816
  in
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   817
    Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   818
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   819
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   820
fun mk_bind (x, f) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   821
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   822
    val T as (Type ("fun", [_, U])) = fastype_of f
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   823
  in
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   824
    Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   825
  end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   826
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   827
val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union}
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   828
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   829
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
   830
  HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   831
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   832
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
   833
  in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   834
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   835
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
   836
  (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
   837
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   838
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
   839
    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
   840
    mk_not = mk_not, mk_map = mk_map};
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   841
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   842
end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   843
(* 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
   844
val pred_compfuns = PredicateCompFuns.compfuns
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   845
val randompred_compfuns = RandomPredCompFuns.compfuns;
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   846
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   847
fun lift_random random =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   848
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   849
    val T = dest_randomT (fastype_of random)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   850
  in
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   851
    Const (@{const_name Quickcheck.Random}, (@{typ Random.seed} -->
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   852
      HOLogic.mk_prodT (HOLogic.mk_prodT (T, @{typ "unit => term"}), @{typ Random.seed})) -->
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33150
diff changeset
   853
      RandomPredCompFuns.mk_randompredT T) $ random
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   854
  end;
32672
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   855
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   856
(* 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
   857
33485
0df4f6e46e5e made definition of functions generically for the different instances
bulwahn
parents: 33484
diff changeset
   858
fun funT_of compfuns (iss, is) T =
0df4f6e46e5e made definition of functions generically for the different instances
bulwahn
parents: 33484
diff changeset
   859
  let
0df4f6e46e5e made definition of functions generically for the different instances
bulwahn
parents: 33484
diff changeset
   860
    val Ts = binder_types T
0df4f6e46e5e made definition of functions generically for the different instances
bulwahn
parents: 33484
diff changeset
   861
    val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
0df4f6e46e5e made definition of functions generically for the different instances
bulwahn
parents: 33484
diff changeset
   862
    val paramTs' = map2 (fn NONE => I | SOME is => funT_of compfuns ([], is)) iss paramTs
0df4f6e46e5e made definition of functions generically for the different instances
bulwahn
parents: 33484
diff changeset
   863
  in
0df4f6e46e5e made definition of functions generically for the different instances
bulwahn
parents: 33484
diff changeset
   864
    (paramTs' @ inargTs) ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
0df4f6e46e5e made definition of functions generically for the different instances
bulwahn
parents: 33484
diff changeset
   865
  end;
0df4f6e46e5e made definition of functions generically for the different instances
bulwahn
parents: 33484
diff changeset
   866
33134
88c9c3460fe7 renamed functions from sizelim to more natural name depth_limited for compilation of depth-limited search in the predicate compiler
bulwahn
parents: 33133
diff changeset
   867
fun depth_limited_funT_of compfuns (iss, is) T =
32672
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   868
  let
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   869
    val Ts = binder_types T
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   870
    val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   871
    val paramTs' =
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   872
      map2 (fn SOME is => depth_limited_funT_of compfuns ([], is) | NONE => I) iss paramTs
32672
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   873
  in
33148
0808f7d0d0d7 removed tuple functions from the predicate compiler
bulwahn
parents: 33147
diff changeset
   874
    (paramTs' @ inargTs @ [@{typ bool}, @{typ "code_numeral"}])
0808f7d0d0d7 removed tuple functions from the predicate compiler
bulwahn
parents: 33147
diff changeset
   875
      ---> (mk_predT compfuns (HOLogic.mk_tupleT outargTs))
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   876
  end;
32672
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   877
33485
0df4f6e46e5e made definition of functions generically for the different instances
bulwahn
parents: 33484
diff changeset
   878
fun random_function_funT_of (iss, is) T =
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   879
  let
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   880
    val Ts = binder_types T
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   881
    val (paramTs, (inargTs, outargTs)) = split_modeT (iss, is) Ts
33485
0df4f6e46e5e made definition of functions generically for the different instances
bulwahn
parents: 33484
diff changeset
   882
    val paramTs' = map2 (fn SOME is => random_function_funT_of ([], is) | NONE => I) iss paramTs
33473
3b275a0bf18c adding tracing function for evaluated code; annotated compilation in the predicate compiler
bulwahn
parents: 33377
diff changeset
   883
  in
33485
0df4f6e46e5e made definition of functions generically for the different instances
bulwahn
parents: 33484
diff changeset
   884
    (paramTs' @ inargTs @ [@{typ code_numeral}]) --->
0df4f6e46e5e made definition of functions generically for the different instances
bulwahn
parents: 33484
diff changeset
   885
      (mk_predT RandomPredCompFuns.compfuns (HOLogic.mk_tupleT outargTs))
0df4f6e46e5e made definition of functions generically for the different instances
bulwahn
parents: 33484
diff changeset
   886
  end
32672
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
   887
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   888
(* Mode analysis *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   889
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   890
(*** check if a term contains only constructor functions ***)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   891
fun is_constrt thy =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   892
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   893
    val cnstrs = flat (maps
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   894
      (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
   895
      (Symtab.dest (Datatype.get_all thy)));
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   896
    fun check t = (case strip_comb t of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   897
        (Free _, []) => true
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   898
      | (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
   899
            (SOME (i, Tname), Type (Tname', _)) =>
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
   900
              length ts = i andalso Tname = Tname' andalso forall check ts
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   901
          | _ => false)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   902
      | _ => false)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   903
  in check end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   904
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   905
(*** check if a type is an equality type (i.e. doesn't contain fun)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   906
  FIXME this is only an approximation ***)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   907
fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   908
  | is_eqT _ = true;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   909
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   910
fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   911
val terms_vs = distinct (op =) o maps term_vs;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   912
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   913
(** collect all Frees in a term (with duplicates!) **)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   914
fun term_vTs tm =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   915
  fold_aterms (fn Free xT => cons xT | _ => I) tm [];
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   916
33138
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   917
fun subsets i j =
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   918
  if i <= j then
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   919
    let
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   920
      fun merge xs [] = xs
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   921
        | merge [] ys = ys
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   922
        | 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
   923
            else y::merge (x::xs) ys;
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   924
      val is = subsets (i+1) j
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   925
    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
   926
  else [[]];
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   927
     
32668
b2de45007537 added first prototype of the extended predicate compiler
bulwahn
parents: 32667
diff changeset
   928
(* FIXME: should be in library - cprod = map_prod I *)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   929
fun cprod ([], ys) = []
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   930
  | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   931
33004
715566791eb0 always qualify NJ's old List.foldl/foldr in Isabelle/ML;
wenzelm
parents: 32970
diff changeset
   932
fun cprods xss = List.foldr (map op :: o cprod) [[]] xss;
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   933
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   934
fun cprods_subset [] = [[]]
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   935
  | cprods_subset (xs :: xss) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   936
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   937
    val yss = (cprods_subset xss)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   938
  in maps (fn ys => map (fn x => cons x ys) xs) yss @ yss end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   939
  
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   940
fun modes_of_term modes t =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   941
  let
33138
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
   942
    val ks = map_index (fn (i, T) => (i + 1, NONE)) (binder_types (fastype_of t));
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   943
    val default = [Mode (([], ks), ks, [])];
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   944
    fun mk_modes name args = Option.map (maps (fn (m as (iss, is)) =>
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   945
        let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   946
          val (args1, args2) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   947
            if length args < length iss then
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   948
              error ("Too few arguments for inductive predicate " ^ name)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   949
            else chop (length iss) args;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   950
          val k = length args2;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   951
          val prfx = map (rpair NONE) (1 upto k)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   952
        in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   953
          if not (is_prefix op = prfx is) then [] else
33116
b379ee2cddb1 changed importing introduction rules to fix the same type variables in all introduction rules; improved mode analysis for partially applied relations; added test case; tuned
bulwahn
parents: 33115
diff changeset
   954
          let val is' = map (fn (i, t) => (i - k, t)) (List.drop (is, k))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   955
          in map (fn x => Mode (m, is', x)) (cprods (map
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   956
            (fn (NONE, _) => [NONE]
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   957
              | (SOME js, arg) => map SOME (filter
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   958
                  (fn Mode (_, js', _) => js=js') (modes_of_term modes arg)))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   959
                    (iss ~~ args1)))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   960
          end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   961
        end)) (AList.lookup op = modes name)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   962
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   963
    case strip_comb (Envir.eta_contract t) of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   964
      (Const (name, _), args) => the_default default (mk_modes name args)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   965
    | (Var ((name, _), _), args) => the (mk_modes name args)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   966
    | (Free (name, _), args) => the (mk_modes name args)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   967
    | (Abs _, []) => error "Abs at param position" (* modes_of_param default modes t *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   968
    | _ => default
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   969
  end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   970
  
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   971
fun select_mode_prem thy modes vs ps =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   972
  find_first (is_some o snd) (ps ~~ map
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   973
    (fn Prem (us, t) => find_first (fn Mode (_, is, _) =>
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   974
          let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   975
            val (in_ts, out_ts) = split_smode is us;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   976
            val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   977
            val vTs = maps term_vTs out_ts';
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   978
            val dupTs = map snd (duplicates (op =) vTs) @
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32950
diff changeset
   979
              map_filter (AList.lookup (op =) vTs) vs;
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   980
          in
33038
8f9594c31de4 dropped redundant gen_ prefix
haftmann
parents: 33037
diff changeset
   981
            subset (op =) (terms_vs (in_ts @ in_ts'), vs) andalso
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   982
            forall (is_eqT o fastype_of) in_ts' andalso
33038
8f9594c31de4 dropped redundant gen_ prefix
haftmann
parents: 33037
diff changeset
   983
            subset (op =) (term_vs t, vs) andalso
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   984
            forall is_eqT dupTs
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   985
          end)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   986
            (modes_of_term modes t handle Option =>
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   987
               error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   988
      | Negprem (us, t) => find_first (fn Mode (_, is, _) =>
33149
2c8f1c450b47 merge -- imported from bulwahn d759e2728188;
wenzelm
parents: 33043 33148
diff changeset
   989
            is = map (rpair NONE) (1 upto length us) andalso
33038
8f9594c31de4 dropped redundant gen_ prefix
haftmann
parents: 33037
diff changeset
   990
            subset (op =) (terms_vs us, vs) andalso
8f9594c31de4 dropped redundant gen_ prefix
haftmann
parents: 33037
diff changeset
   991
            subset (op =) (term_vs t, vs))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   992
            (modes_of_term modes t handle Option =>
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   993
               error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
33038
8f9594c31de4 dropped redundant gen_ prefix
haftmann
parents: 33037
diff changeset
   994
      | Sidecond t => if subset (op =) (term_vs t, vs) then SOME (Mode (([], []), [], []))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   995
          else NONE
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   996
      ) ps);
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   997
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   998
fun fold_prem f (Prem (args, _)) = fold f args
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
   999
  | fold_prem f (Negprem (args, _)) = fold f args
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1000
  | fold_prem f (Sidecond t) = f t
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1001
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1002
fun all_subsets [] = [[]]
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1003
  | all_subsets (x::xs) = let val xss' = all_subsets xs in xss' @ (map (cons x) xss') end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1004
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1005
fun generator vTs v = 
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1006
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1007
    val T = the (AList.lookup (op =) vTs v)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1008
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1009
    (Generator (v, T), Mode (([], []), [], []))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1010
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1011
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1012
fun check_mode_clause with_generator thy param_vs modes gen_modes (iss, is) (ts, ps) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1013
  let
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32950
diff changeset
  1014
    val modes' = modes @ map_filter
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1015
      (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1016
        (param_vs ~~ iss);
32952
aeb1e44fbc19 replaced String.concat by implode;
wenzelm
parents: 32950
diff changeset
  1017
    val gen_modes' = gen_modes @ map_filter
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1018
      (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1019
        (param_vs ~~ iss);  
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1020
    val vTs = distinct (op =) ((fold o fold_prem) Term.add_frees ps (fold Term.add_frees ts []))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1021
    val prem_vs = distinct (op =) ((fold o fold_prem) Term.add_free_names ps [])
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1022
    fun check_mode_prems acc_ps vs [] = SOME (acc_ps, vs)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1023
      | check_mode_prems acc_ps vs ps = (case select_mode_prem thy modes' vs ps of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1024
          NONE =>
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1025
            (if with_generator then
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1026
              (case select_mode_prem thy gen_modes' vs ps of
33144
1831516747d4 removed obsolete GeneratorPrem; clean-up after modularization; tuned
bulwahn
parents: 33143
diff changeset
  1027
                SOME (p as Prem _, SOME mode) => check_mode_prems ((p, mode) :: acc_ps) 
33042
ddf1f03a9ad9 curried union as canonical list operation
haftmann
parents: 33039
diff changeset
  1028
                  (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1029
                  (filter_out (equal p) ps)
32672
90f3ce5d27ae added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
bulwahn
parents: 32671
diff changeset
  1030
              | _ =>
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1031
                  let 
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
  1032
                    val all_generator_vs = all_subsets (subtract (op =) vs prem_vs)
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
  1033
                      |> sort (int_ord o (pairself length))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1034
                  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1035
                    case (find_first (fn generator_vs => is_some
33482
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
  1036
                      (select_mode_prem thy modes' (union (op =) vs generator_vs) ps))
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
  1037
                        all_generator_vs) of
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
  1038
                      SOME generator_vs => check_mode_prems
5029ec373036 strictly respecting the line margin in the predicate compiler core
bulwahn
parents: 33479
diff changeset
  1039
                        ((map (generator vTs) generator_vs) @ acc_ps)
33042
ddf1f03a9ad9 curried union as canonical list operation
haftmann
parents: 33039
diff changeset
  1040
                        (union (op =) vs generator_vs) ps
33128
1f990689349f further cleaning up
bulwahn
parents: 33127
diff changeset
  1041
                    | NONE => NONE
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1042
                  end)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1043
            else
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1044
              NONE)
33144
1831516747d4 removed obsolete GeneratorPrem; clean-up after modularization; tuned
bulwahn
parents: 33143
diff changeset
  1045
        | SOME (p, SOME mode) => check_mode_prems ((p, mode) :: acc_ps) 
33042
ddf1f03a9ad9 curried union as canonical list operation
haftmann
parents: 33039
diff changeset
  1046
            (case p of Prem (us, _) => union (op =) vs (terms_vs us) | _ => vs)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1047
            (filter_out (equal p) ps))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1048
    val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (split_smode is ts));
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1049
    val in_vs = terms_vs in_ts;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1050
    val concl_vs = terms_vs ts
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1051
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1052
    if forall is_eqT (map snd (duplicates (op =) (maps term_vTs in_ts))) andalso
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1053
    forall (is_eqT o fastype_of) in_ts' then
33042
ddf1f03a9ad9 curried union as canonical list operation
haftmann
parents: 33039
diff changeset
  1054
      case check_mode_prems [] (union (op =) param_vs in_vs) ps of
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1055
         NONE => NONE
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1056
       | SOME (acc_ps, vs) =>
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1057
         if with_generator then
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 33039
diff changeset
  1058
           SOME (ts, (rev acc_ps) @ (map (generator vTs) (subtract (op =) vs concl_vs)))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1059
         else
33038
8f9594c31de4 dropped redundant gen_ prefix
haftmann
parents: 33037
diff changeset
  1060
           if subset (op =) (concl_vs, vs) then SOME (ts, rev acc_ps) else NONE
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1061
    else NONE
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1062
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1063
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1064
fun print_failed_mode options thy modes p m rs is =
33130
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
  1065
  if show_mode_inference options then
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
  1066
    let
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1067
      val _ = tracing ("Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1068
        p ^ " violates mode " ^ string_of_mode thy p m)
33130
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
  1069
    in () end
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
  1070
  else ()
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
  1071
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1072
fun error_of thy p m is =
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1073
  ("  Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1074
        p ^ " violates mode " ^ string_of_mode thy p m)
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1075
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1076
fun find_indices f xs =
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1077
  map_filter (fn (i, true) => SOME i | (i, false) => NONE) (map_index (apsnd f) xs)
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1078
33130
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
  1079
fun check_modes_pred options with_generator thy param_vs clauses modes gen_modes (p, ms) =
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
  1080
  let
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
  1081
    val rs = case AList.lookup (op =) clauses p of SOME rs => rs | NONE => []
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1082
    fun invalid_mode m =
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1083
      case find_indices
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1084
        (is_none o check_mode_clause with_generator thy param_vs modes gen_modes m) rs of
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1085
        [] => NONE
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1086
      | is => SOME (error_of thy p m is)
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1087
    val res = map (fn m => (m, invalid_mode m)) ms
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1088
    val ms' = map_filter (fn (m, NONE) => SOME m | _ => NONE) res
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1089
    val errors = map_filter snd res
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1090
  in
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1091
    ((p, ms'), errors)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1092
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1093
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1094
fun get_modes_pred with_generator thy param_vs clauses modes gen_modes (p, ms) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1095
  let
33146
bf852ef586f2 now the predicate compilere handles the predicate without introduction rules better as before
bulwahn
parents: 33145
diff changeset
  1096
    val rs = case AList.lookup (op =) clauses p of SOME rs => rs | NONE => []
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1097
  in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1098
    (p, map (fn m =>
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1099
      (m, map (the o check_mode_clause with_generator thy param_vs modes gen_modes m) rs)) ms)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1100
  end;
33137
0d16c07f8d24 added option to generate random values to values command in the predicate compiler
bulwahn
parents: 33135
diff changeset
  1101
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1102
fun fixp f (x : (string * mode list) list) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1103
  let val y = f x
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1104
  in if x = y then x else fixp f y end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1105
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1106
fun fixp_with_state f ((x : (string * mode list) list), state) =
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1107
  let
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1108
    val (y, state') = f (x, state)
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1109
  in
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1110
    if x = y then (y, state') else fixp_with_state f (y, state')
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1111
  end
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1112
33130
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
  1113
fun infer_modes options thy extra_modes all_modes param_vs clauses =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1114
  let
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1115
    val (modes, errors) =
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1116
      fixp_with_state (fn (modes, errors) =>
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1117
        let
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1118
          val res = map
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1119
            (check_modes_pred options false thy param_vs clauses (modes @ extra_modes) []) modes
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1120
        in (map fst res, errors @ maps snd res) end)
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1121
          (all_modes, [])
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1122
  in
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1123
    (map (get_modes_pred false thy param_vs clauses (modes @ extra_modes) []) modes, errors)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1124
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1125
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1126
fun remove_from rem [] = []
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1127
  | remove_from rem ((k, vs) :: xs) =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1128
    (case AList.lookup (op =) rem k of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1129
      NONE => (k, vs)
33040
cffdb7b28498 removed old-style \ and \\ infixes
haftmann
parents: 33039
diff changeset
  1130
    | SOME vs' => (k, subtract (op =) vs' vs))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1131
    :: remove_from rem xs
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1132
33130
7eac458c2b22 added option show_mode_inference; added splitting of conjunctions in expand_tuples
bulwahn
parents: 33129
diff changeset
  1133
fun infer_modes_with_generator options thy extra_modes all_modes param_vs clauses =
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1134
  let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1135
    val prednames = map fst clauses
33138
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
  1136
    val extra_modes' = all_modes_of thy
33484
e96a0c52d74b renamed generator to random_function in the predicate compiler
bulwahn
parents: 33483
diff changeset
  1137
    val gen_modes = all_random_modes_of thy
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1138
      |> filter_out (fn (name, _) => member (op =) prednames name)
33138
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
  1139
    val starting_modes = remove_from extra_modes' all_modes
e2e23987c59a reinvestigating the compilation of the random computation in the predicate compiler
bulwahn
parents: 33137
diff changeset
  1140
    fun eq_mode (m1, m2) = (m1 = m2)
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1141
    val (modes, errors) =
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1142
      fixp_with_state (fn (modes, errors) =>
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1143
        let
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1144
          val res = map
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1145
            (check_modes_pred options true thy param_vs clauses extra_modes'
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1146
              (gen_modes @ modes)) modes
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1147
        in (map fst res, errors @ maps snd res) end) (starting_modes, [])
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1148
    val moded_clauses =
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1149
      map (get_modes_pred true thy param_vs clauses extra_modes (gen_modes @ modes)) modes
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1150
    val (moded_clauses', _) = infer_modes options thy extra_modes all_modes param_vs clauses
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1151
    val join_moded_clauses_table = AList.join (op =)
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1152
      (fn _ => fn ((mps1, mps2)) =>
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1153
        merge (fn ((m1, _), (m2, _)) => eq_mode (m1, m2)) (mps1, mps2))
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1154
  in
33752
9aa8e961f850 adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned
bulwahn
parents: 33671
diff changeset
  1155
    (join_moded_clauses_table (moded_clauses', moded_clauses), errors)
32667
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1156
  end;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1157
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1158
(* term construction *)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1159
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1160
fun mk_v (names, vs) s T = (case AList.lookup (op =) vs s of
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1161
      NONE => (Free (s, T), (names, (s, [])::vs))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1162
    | SOME xs =>
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1163
        let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1164
          val s' = Name.variant names s;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1165
          val v = Free (s', T)
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1166
        in
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1167
          (v, (s'::names, AList.update (op =) (s, v::xs) vs))
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1168
        end);
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1169
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1170
fun distinct_v (Free (s, T)) nvs = mk_v nvs s T
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1171
  | distinct_v (t $ u) nvs =
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1172
      let
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1173
        val (t', nvs') = distinct_v t nvs;
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1174
        val (u', nvs'') = distinct_v u nvs';
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1175
      in (t' $ u', nvs'') end
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1176
  | distinct_v x nvs = (x, nvs);
09546e654222 moved predicate compiler to Tools
bulwahn
parents:
diff changeset
  1177
33147
180dc60bd88c improving the compilation with higher-order arguments in the predicate compiler
bulwahn
parents: 33146
diff changeset
  1178
(** specific rpred functions -- move them to the correct place in this file *)
180dc60bd88c improving the compilation with higher-order arguments in the predicate compiler
bulwahn
parents: 33146
diff changeset
  1179
180dc60bd88c improving the compilation with higher-order arguments in the predicate compiler
bulwahn
parents: 33146
diff changeset
  1180
fun mk_Eval_of additional_arguments ((x, T), NONE) names = (x, names)
180dc60bd88c improving the compilation with higher-order arguments in the predicate compiler
bulwahn
parents: 33146
diff changeset
  1181
  | mk_Eval_of additional_arguments ((x, T), SOME mode) names =
33268
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33265
diff changeset
  1182
  let
33147
180dc60bd88c improving the compilation with higher-order arguments in the predicate compiler
bulwahn
parents: 33146
diff changeset
  1183
    val Ts = binder_types T
33268
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33265
diff changeset
  1184
    fun mk_split_lambda [] t = lambda (Free (Name.variant names "x", HOLogic.unitT)) t
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33265
diff changeset
  1185
      | mk_split_lambda [x] t = lambda x t
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33265
diff changeset
  1186
      | mk_split_lambda xs t =
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33265
diff changeset
  1187
      let
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33265
diff changeset
  1188
        fun mk_split_lambda' (x::y::[]) t = HOLogic.mk_split (lambda x (lambda y t))
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33265
diff changeset
  1189
          | mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33265
diff changeset
  1190
      in
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33265
diff changeset
  1191
        mk_split_lambda' xs t
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33265
diff changeset
  1192
      end;
02de0317f66f eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 33265
diff changeset
  1193