src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
author bulwahn
Wed Oct 28 12:29:02 2009 +0100 (2009-10-28)
changeset 33328 1d93dd8a02c9
parent 33327 9d03957622a2
child 33375 fd3e861f8d31
permissions -rw-r--r--
moved datatype mode and string functions to the auxillary structure
wenzelm@33265
     1
(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
wenzelm@33265
     2
    Author:     Lukas Bulwahn, TU Muenchen
bulwahn@33250
     3
wenzelm@33265
     4
Auxilary functions for predicate compiler.
bulwahn@33250
     5
*)
bulwahn@33250
     6
wenzelm@33265
     7
(* FIXME proper signature *)
wenzelm@33265
     8
bulwahn@33250
     9
structure Predicate_Compile_Aux =
bulwahn@33250
    10
struct
bulwahn@33250
    11
bulwahn@33328
    12
bulwahn@33328
    13
(* mode *)
bulwahn@33328
    14
bulwahn@33327
    15
type smode = (int * int list option) list
bulwahn@33327
    16
type mode = smode option list * smode
bulwahn@33328
    17
datatype tmode = Mode of mode * smode * tmode option list;
bulwahn@33328
    18
bulwahn@33328
    19
fun string_of_smode js =
bulwahn@33328
    20
    commas (map
bulwahn@33328
    21
      (fn (i, is) =>
bulwahn@33328
    22
        string_of_int i ^ (case is of NONE => ""
bulwahn@33328
    23
    | SOME is => "p" ^ enclose "[" "]" (commas (map string_of_int is)))) js)
bulwahn@33328
    24
bulwahn@33328
    25
fun string_of_mode (iss, is) = space_implode " -> " (map
bulwahn@33328
    26
  (fn NONE => "X"
bulwahn@33328
    27
    | SOME js => enclose "[" "]" (string_of_smode js))
bulwahn@33328
    28
       (iss @ [SOME is]));
bulwahn@33328
    29
bulwahn@33328
    30
fun string_of_tmode (Mode (predmode, termmode, param_modes)) =
bulwahn@33328
    31
  "predmode: " ^ (string_of_mode predmode) ^ 
bulwahn@33328
    32
  (if null param_modes then "" else
bulwahn@33328
    33
    "; " ^ "params: " ^ commas (map (the_default "NONE" o Option.map string_of_tmode) param_modes))
bulwahn@33327
    34
bulwahn@33250
    35
(* general syntactic functions *)
bulwahn@33250
    36
bulwahn@33250
    37
(*Like dest_conj, but flattens conjunctions however nested*)
bulwahn@33250
    38
fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
bulwahn@33250
    39
  | conjuncts_aux t conjs = t::conjs;
bulwahn@33250
    40
bulwahn@33250
    41
fun conjuncts t = conjuncts_aux t [];
bulwahn@33250
    42
bulwahn@33250
    43
(* syntactic functions *)
bulwahn@33250
    44
bulwahn@33250
    45
fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
bulwahn@33250
    46
  | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
bulwahn@33250
    47
  | is_equationlike_term _ = false
bulwahn@33250
    48
  
bulwahn@33250
    49
val is_equationlike = is_equationlike_term o prop_of 
bulwahn@33250
    50
bulwahn@33250
    51
fun is_pred_equation_term (Const ("==", _) $ u $ v) =
bulwahn@33250
    52
  (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
bulwahn@33250
    53
  | is_pred_equation_term _ = false
bulwahn@33250
    54
  
bulwahn@33250
    55
val is_pred_equation = is_pred_equation_term o prop_of 
bulwahn@33250
    56
bulwahn@33250
    57
fun is_intro_term constname t =
bulwahn@33250
    58
  case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of
bulwahn@33250
    59
    Const (c, _) => c = constname
bulwahn@33250
    60
  | _ => false
bulwahn@33250
    61
  
bulwahn@33250
    62
fun is_intro constname t = is_intro_term constname (prop_of t)
bulwahn@33250
    63
bulwahn@33250
    64
fun is_pred thy constname =
bulwahn@33250
    65
  let
bulwahn@33250
    66
    val T = (Sign.the_const_type thy constname)
bulwahn@33250
    67
  in body_type T = @{typ "bool"} end;
bulwahn@33250
    68
  
bulwahn@33250
    69
bulwahn@33250
    70
fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT)
bulwahn@33250
    71
  | is_predT _ = false
bulwahn@33250
    72
bulwahn@33250
    73
  
bulwahn@33250
    74
(*** check if a term contains only constructor functions ***)
bulwahn@33250
    75
fun is_constrt thy =
bulwahn@33250
    76
  let
bulwahn@33250
    77
    val cnstrs = flat (maps
bulwahn@33250
    78
      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
bulwahn@33250
    79
      (Symtab.dest (Datatype.get_all thy)));
bulwahn@33250
    80
    fun check t = (case strip_comb t of
bulwahn@33250
    81
        (Free _, []) => true
bulwahn@33250
    82
      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
bulwahn@33250
    83
            (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
bulwahn@33250
    84
          | _ => false)
bulwahn@33250
    85
      | _ => false)
bulwahn@33250
    86
  in check end;  
bulwahn@33250
    87
  
bulwahn@33250
    88
fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
bulwahn@33250
    89
  let
bulwahn@33250
    90
    val (xTs, t') = strip_ex t
bulwahn@33250
    91
  in
bulwahn@33250
    92
    ((x, T) :: xTs, t')
bulwahn@33250
    93
  end
bulwahn@33250
    94
  | strip_ex t = ([], t)
bulwahn@33250
    95
bulwahn@33250
    96
fun focus_ex t nctxt =
bulwahn@33250
    97
  let
bulwahn@33250
    98
    val ((xs, Ts), t') = apfst split_list (strip_ex t) 
bulwahn@33250
    99
    val (xs', nctxt') = Name.variants xs nctxt;
bulwahn@33250
   100
    val ps' = xs' ~~ Ts;
bulwahn@33250
   101
    val vs = map Free ps';
bulwahn@33250
   102
    val t'' = Term.subst_bounds (rev vs, t');
bulwahn@33250
   103
  in ((ps', t''), nctxt') end;
bulwahn@33250
   104
bulwahn@33250
   105
bulwahn@33250
   106
(* introduction rule combinators *)
bulwahn@33250
   107
bulwahn@33250
   108
(* combinators to apply a function to all literals of an introduction rules *)
bulwahn@33250
   109
bulwahn@33250
   110
fun map_atoms f intro = 
bulwahn@33250
   111
  let
bulwahn@33250
   112
    val (literals, head) = Logic.strip_horn intro
bulwahn@33250
   113
    fun appl t = (case t of
bulwahn@33250
   114
        (@{term "Not"} $ t') => HOLogic.mk_not (f t')
bulwahn@33250
   115
      | _ => f t)
bulwahn@33250
   116
  in
bulwahn@33250
   117
    Logic.list_implies
bulwahn@33250
   118
      (map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head)
bulwahn@33250
   119
  end
bulwahn@33250
   120
bulwahn@33250
   121
fun fold_atoms f intro s =
bulwahn@33250
   122
  let
bulwahn@33250
   123
    val (literals, head) = Logic.strip_horn intro
bulwahn@33250
   124
    fun appl t s = (case t of
bulwahn@33250
   125
      (@{term "Not"} $ t') => f t' s
bulwahn@33250
   126
      | _ => f t s)
bulwahn@33250
   127
  in fold appl (map HOLogic.dest_Trueprop literals) s end
bulwahn@33250
   128
bulwahn@33250
   129
fun fold_map_atoms f intro s =
bulwahn@33250
   130
  let
bulwahn@33250
   131
    val (literals, head) = Logic.strip_horn intro
bulwahn@33250
   132
    fun appl t s = (case t of
bulwahn@33250
   133
      (@{term "Not"} $ t') => apfst HOLogic.mk_not (f t' s)
bulwahn@33250
   134
      | _ => f t s)
bulwahn@33250
   135
    val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
bulwahn@33250
   136
  in
bulwahn@33250
   137
    (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
bulwahn@33250
   138
  end;
bulwahn@33250
   139
bulwahn@33250
   140
fun maps_premises f intro =
bulwahn@33250
   141
  let
bulwahn@33250
   142
    val (premises, head) = Logic.strip_horn intro
bulwahn@33250
   143
  in
bulwahn@33250
   144
    Logic.list_implies (maps f premises, head)
bulwahn@33250
   145
  end
bulwahn@33250
   146
  
bulwahn@33250
   147
(* lifting term operations to theorems *)
bulwahn@33250
   148
bulwahn@33250
   149
fun map_term thy f th =
bulwahn@33250
   150
  Skip_Proof.make_thm thy (f (prop_of th))
bulwahn@33250
   151
bulwahn@33250
   152
(*
bulwahn@33250
   153
fun equals_conv lhs_cv rhs_cv ct =
bulwahn@33250
   154
  case Thm.term_of ct of
bulwahn@33250
   155
    Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct  
bulwahn@33250
   156
  | _ => error "equals_conv"  
bulwahn@33250
   157
*)
bulwahn@33250
   158
bulwahn@33250
   159
(* Different options for compiler *)
bulwahn@33250
   160
bulwahn@33250
   161
datatype options = Options of {  
bulwahn@33327
   162
  expected_modes : (string * mode list) option,
bulwahn@33250
   163
  show_steps : bool,
bulwahn@33250
   164
  show_proof_trace : bool,
bulwahn@33250
   165
  show_intermediate_results : bool,
bulwahn@33251
   166
  show_mode_inference : bool,
bulwahn@33251
   167
  show_modes : bool,
bulwahn@33250
   168
  show_compilation : bool,
bulwahn@33250
   169
  skip_proof : bool,
bulwahn@33250
   170
bulwahn@33250
   171
  inductify : bool,
bulwahn@33250
   172
  rpred : bool,
bulwahn@33250
   173
  depth_limited : bool
bulwahn@33250
   174
};
bulwahn@33250
   175
bulwahn@33250
   176
fun expected_modes (Options opt) = #expected_modes opt
bulwahn@33250
   177
fun show_steps (Options opt) = #show_steps opt
bulwahn@33250
   178
fun show_intermediate_results (Options opt) = #show_intermediate_results opt
bulwahn@33250
   179
fun show_proof_trace (Options opt) = #show_proof_trace opt
bulwahn@33251
   180
fun show_modes (Options opt) = #show_modes opt
bulwahn@33251
   181
fun show_mode_inference (Options opt) = #show_mode_inference opt
bulwahn@33250
   182
fun show_compilation (Options opt) = #show_compilation opt
bulwahn@33250
   183
fun skip_proof (Options opt) = #skip_proof opt
bulwahn@33250
   184
bulwahn@33250
   185
fun is_inductify (Options opt) = #inductify opt
bulwahn@33250
   186
fun is_rpred (Options opt) = #rpred opt
bulwahn@33250
   187
fun is_depth_limited (Options opt) = #depth_limited opt
bulwahn@33250
   188
bulwahn@33250
   189
val default_options = Options {
bulwahn@33250
   190
  expected_modes = NONE,
bulwahn@33250
   191
  show_steps = false,
bulwahn@33250
   192
  show_intermediate_results = false,
bulwahn@33250
   193
  show_proof_trace = false,
bulwahn@33251
   194
  show_modes = false,
bulwahn@33250
   195
  show_mode_inference = false,
bulwahn@33250
   196
  show_compilation = false,
bulwahn@33250
   197
  skip_proof = false,
bulwahn@33250
   198
  
bulwahn@33250
   199
  inductify = false,
bulwahn@33250
   200
  rpred = false,
bulwahn@33250
   201
  depth_limited = false
bulwahn@33250
   202
}
bulwahn@33250
   203
bulwahn@33250
   204
bulwahn@33250
   205
fun print_step options s =
bulwahn@33250
   206
  if show_steps options then tracing s else ()
bulwahn@33250
   207
bulwahn@33250
   208
(* tuple processing *)
bulwahn@33250
   209
bulwahn@33250
   210
fun expand_tuples thy intro =
bulwahn@33250
   211
  let
bulwahn@33250
   212
    fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
bulwahn@33250
   213
      | rewrite_args (arg::args) (pats, intro_t, ctxt) = 
bulwahn@33250
   214
      (case HOLogic.strip_tupleT (fastype_of arg) of
bulwahn@33250
   215
        (Ts as _ :: _ :: _) =>
bulwahn@33250
   216
        let
bulwahn@33250
   217
          fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2]))
bulwahn@33250
   218
            (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
bulwahn@33250
   219
            | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) =
bulwahn@33250
   220
              let
bulwahn@33250
   221
                val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
bulwahn@33250
   222
                val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
bulwahn@33250
   223
                val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
bulwahn@33250
   224
                val args' = map (Pattern.rewrite_term thy [pat] []) args
bulwahn@33250
   225
              in
bulwahn@33250
   226
                rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
bulwahn@33250
   227
              end
bulwahn@33250
   228
            | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
bulwahn@33250
   229
          val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg)
bulwahn@33250
   230
            (args, (pats, intro_t, ctxt))
bulwahn@33250
   231
        in
bulwahn@33250
   232
          rewrite_args args' (pats, intro_t', ctxt')
bulwahn@33250
   233
        end
bulwahn@33250
   234
      | _ => rewrite_args args (pats, intro_t, ctxt))
bulwahn@33250
   235
    fun rewrite_prem atom =
bulwahn@33250
   236
      let
bulwahn@33250
   237
        val (_, args) = strip_comb atom
bulwahn@33250
   238
      in rewrite_args args end
bulwahn@33250
   239
    val ctxt = ProofContext.init thy
bulwahn@33250
   240
    val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
bulwahn@33250
   241
    val intro_t = prop_of intro'
bulwahn@33250
   242
    val concl = Logic.strip_imp_concl intro_t
bulwahn@33250
   243
    val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
bulwahn@33250
   244
    val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
bulwahn@33250
   245
    val (pats', intro_t', ctxt3) = 
bulwahn@33250
   246
      fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
bulwahn@33250
   247
    fun rewrite_pat (ct1, ct2) =
bulwahn@33250
   248
      (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2)))
bulwahn@33250
   249
    val t_insts' = map rewrite_pat t_insts
bulwahn@33250
   250
    val intro'' = Thm.instantiate (T_insts, t_insts') intro
bulwahn@33250
   251
    val [intro'''] = Variable.export ctxt3 ctxt [intro'']
bulwahn@33250
   252
    val intro'''' = Simplifier.full_simplify
bulwahn@33250
   253
      (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
bulwahn@33250
   254
      intro'''
bulwahn@33250
   255
    (* splitting conjunctions introduced by Pair_eq*)
bulwahn@33250
   256
    fun split_conj prem =
bulwahn@33250
   257
      map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem))
bulwahn@33250
   258
    val intro''''' = map_term thy (maps_premises split_conj) intro''''
bulwahn@33250
   259
  in
bulwahn@33250
   260
    intro'''''
bulwahn@33250
   261
  end
bulwahn@33250
   262
bulwahn@33250
   263
end;