src/HOL/Tools/Nitpick/nitpick_preproc.ML
changeset 41875 e3cd0dce9b1a
parent 41870 a14a492f472f
child 41876 03f699556955
equal deleted inserted replaced
41874:a3035d56171d 41875:e3cd0dce9b1a
  1242 
  1242 
  1243 val max_skolem_depth = 3
  1243 val max_skolem_depth = 3
  1244 
  1244 
  1245 fun preprocess_formulas
  1245 fun preprocess_formulas
  1246         (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
  1246         (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
  1247                       preconstrs, ...}) assm_ts neg_t =
  1247                       needs, ...}) assm_ts neg_t =
  1248   let
  1248   let
  1249     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
  1249     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
  1250       neg_t |> unfold_defs_in_term hol_ctxt
  1250       neg_t |> unfold_defs_in_term hol_ctxt
  1251             |> close_form
  1251             |> close_form
  1252             |> skolemize_term_and_more hol_ctxt max_skolem_depth
  1252             |> skolemize_term_and_more hol_ctxt max_skolem_depth
  1279       #> distribute_quantifiers
  1279       #> distribute_quantifiers
  1280       #> push_quantifiers_inward
  1280       #> push_quantifiers_inward
  1281       #> close_form
  1281       #> close_form
  1282       #> Term.map_abs_vars shortest_name
  1282       #> Term.map_abs_vars shortest_name
  1283     val nondef_ts = nondef_ts |> map (do_middle false)
  1283     val nondef_ts = nondef_ts |> map (do_middle false)
  1284     val preconstr_ts =
  1284     val need_ts =
  1285       (* FIXME: Implement preconstruction inference. *)
  1285       (* FIXME: Implement inference. *)
  1286       preconstrs
  1286       needs |> map_filter (fn (SOME t, SOME true) =>
  1287       |> map_filter (fn (SOME t, SOME true) =>
  1287                               SOME (t |> unfold_defs_in_term hol_ctxt
  1288                         SOME (t |> unfold_defs_in_term hol_ctxt
  1288                                       |> do_middle false)
  1289                                 |> do_middle false)
  1289                             | _ => NONE)
  1290                       | _ => NONE)
       
  1291     val nondef_ts = nondef_ts |> map (do_tail false)
  1290     val nondef_ts = nondef_ts |> map (do_tail false)
  1292     val def_ts = def_ts |> map (do_middle true #> do_tail true)
  1291     val def_ts = def_ts |> map (do_middle true #> do_tail true)
  1293   in
  1292   in
  1294     (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms,
  1293     (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms, no_poly_user_axioms,
  1295      no_poly_user_axioms, binarize)
  1294      binarize)
  1296   end
  1295   end
  1297 
  1296 
  1298 end;
  1297 end;