move metis to new monomorphizer
authorblanchet
Mon Sep 09 15:22:04 2013 +0200 (2013-09-09)
changeset 53479f7d8224641de
parent 53478 8c3ccb314469
child 53480 247817dbb990
move metis to new monomorphizer
src/HOL/ATP.thy
src/HOL/Tools/Metis/metis_generate.ML
src/HOL/Tools/legacy_monomorph.ML
     1.1 --- a/src/HOL/ATP.thy	Mon Sep 09 15:22:04 2013 +0200
     1.2 +++ b/src/HOL/ATP.thy	Mon Sep 09 15:22:04 2013 +0200
     1.3 @@ -11,7 +11,6 @@
     1.4  
     1.5  ML_file "Tools/lambda_lifting.ML"
     1.6  ML_file "Tools/monomorph.ML"
     1.7 -ML_file "Tools/legacy_monomorph.ML"
     1.8  ML_file "Tools/ATP/atp_util.ML"
     1.9  ML_file "Tools/ATP/atp_problem.ML"
    1.10  ML_file "Tools/ATP/atp_proof.ML"
     2.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Mon Sep 09 15:22:04 2013 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Mon Sep 09 15:22:04 2013 +0200
     2.3 @@ -215,9 +215,8 @@
     2.4        else
     2.5          conj_clauses @ fact_clauses
     2.6          |> map (pair 0)
     2.7 -        |> rpair (ctxt |> Config.put Legacy_Monomorph.keep_partial_instances false)
     2.8 -        |-> Legacy_Monomorph.monomorph atp_schematic_consts_of
     2.9 -        |> fst |> chop (length conj_clauses)
    2.10 +        |> Monomorph.monomorph atp_schematic_consts_of ctxt
    2.11 +        |> chop (length conj_clauses)
    2.12          |> pairself (maps (map (zero_var_indexes o snd)))
    2.13      val num_conjs = length conj_clauses
    2.14      (* Pretend every clause is a "simp" rule, to guide the term ordering. *)
     3.1 --- a/src/HOL/Tools/legacy_monomorph.ML	Mon Sep 09 15:22:04 2013 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,331 +0,0 @@
     3.4 -(*  Title:      HOL/Tools/legacy_monomorph.ML
     3.5 -    Author:     Sascha Boehme, TU Muenchen
     3.6 -
     3.7 -Monomorphization of theorems, i.e., computation of all (necessary)
     3.8 -instances.  This procedure is incomplete in general, but works well for
     3.9 -most practical problems.
    3.10 -
    3.11 -For a list of universally closed theorems (without schematic term
    3.12 -variables), monomorphization computes a list of theorems with schematic
    3.13 -term variables: all polymorphic constants (i.e., constants occurring both
    3.14 -with ground types and schematic type variables) are instantiated with all
    3.15 -(necessary) ground types; thereby theorems containing these constants are
    3.16 -copied.  To prevent nontermination, there is an upper limit for the number
    3.17 -of iterations involved in the fixpoint construction.
    3.18 -
    3.19 -The search for instances is performed on the constants with schematic
    3.20 -types, which are extracted from the initial set of theorems.  The search
    3.21 -constructs, for each theorem with those constants, a set of substitutions,
    3.22 -which, in the end, is applied to all corresponding theorems.  Remaining
    3.23 -schematic type variables are substituted with fresh types.
    3.24 -
    3.25 -Searching for necessary substitutions is an iterative fixpoint
    3.26 -construction: each iteration computes all required instances required by
    3.27 -the ground instances computed in the previous step and which haven't been
    3.28 -found before.  Computed substitutions are always nontrivial: schematic type
    3.29 -variables are never mapped to schematic type variables.
    3.30 -*)
    3.31 -
    3.32 -signature LEGACY_MONOMORPH =
    3.33 -sig
    3.34 -  (* utility function *)
    3.35 -  val typ_has_tvars: typ -> bool
    3.36 -  val all_schematic_consts_of: term -> typ list Symtab.table
    3.37 -  val add_schematic_consts_of: term -> typ list Symtab.table ->
    3.38 -    typ list Symtab.table
    3.39 -
    3.40 -  (* configuration options *)
    3.41 -  val max_rounds: int Config.T
    3.42 -  val max_new_instances: int Config.T
    3.43 -  val keep_partial_instances: bool Config.T
    3.44 -
    3.45 -  (* monomorphization *)
    3.46 -  val monomorph: (term -> typ list Symtab.table) -> (int * thm) list ->
    3.47 -    Proof.context -> (int * thm) list list * Proof.context
    3.48 -end
    3.49 -
    3.50 -structure Legacy_Monomorph: LEGACY_MONOMORPH =
    3.51 -struct
    3.52 -
    3.53 -(* utility functions *)
    3.54 -
    3.55 -val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
    3.56 -
    3.57 -fun add_schematic_const (c as (_, T)) =
    3.58 -  if typ_has_tvars T then Symtab.insert_list (op =) c else I
    3.59 -
    3.60 -fun add_schematic_consts_of t =
    3.61 -  Term.fold_aterms (fn Const c => add_schematic_const c | _ => I) t
    3.62 -
    3.63 -fun all_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
    3.64 -
    3.65 -
    3.66 -
    3.67 -(* configuration options *)
    3.68 -
    3.69 -val max_rounds = Attrib.setup_config_int @{binding legacy_monomorph_max_rounds} (K 5)
    3.70 -val max_new_instances =
    3.71 -  Attrib.setup_config_int @{binding legacy_monomorph_max_new_instances} (K 300)
    3.72 -val keep_partial_instances =
    3.73 -  Attrib.setup_config_bool @{binding legacy_monomorph_keep_partial_instances} (K true)
    3.74 -
    3.75 -
    3.76 -
    3.77 -(* monomorphization *)
    3.78 -
    3.79 -(** preparing the problem **)
    3.80 -
    3.81 -datatype thm_info =
    3.82 -  Ground of thm |
    3.83 -  Schematic of {
    3.84 -    index: int,
    3.85 -    theorem: thm,
    3.86 -    tvars: (indexname * sort) list,
    3.87 -    schematics: typ list Symtab.table,
    3.88 -    initial_round: int }
    3.89 -
    3.90 -fun prepare schematic_consts_of rthms =
    3.91 -  let
    3.92 -    val empty_sub = ((0, false, false), Vartab.empty)
    3.93 -
    3.94 -    fun prep (r, thm) ((i, idx), (consts, subs)) =
    3.95 -      if not (Term.exists_type typ_has_tvars (Thm.prop_of thm)) then
    3.96 -        (Ground thm, ((i+1, idx + Thm.maxidx_of thm + 1), (consts, subs)))
    3.97 -      else
    3.98 -        let
    3.99 -          (* increase indices to avoid clashes of type variables *)
   3.100 -          val thm' = Thm.incr_indexes idx thm
   3.101 -          val idx' = Thm.maxidx_of thm' + 1
   3.102 -          val schematics = schematic_consts_of (Thm.prop_of thm')
   3.103 -          val consts' =
   3.104 -            Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts
   3.105 -          val subs' = Inttab.update (i, [empty_sub]) subs
   3.106 -          val thm_info = Schematic {
   3.107 -            index = i,
   3.108 -            theorem = thm',
   3.109 -            tvars = Term.add_tvars (Thm.prop_of thm') [],
   3.110 -            schematics = schematics,
   3.111 -            initial_round = r }
   3.112 -      in (thm_info, ((i+1, idx'), (consts', subs'))) end
   3.113 -  in fold_map prep rthms ((0, 0), (Symtab.empty, Inttab.empty)) ||> snd end
   3.114 -
   3.115 -
   3.116 -
   3.117 -(** collecting substitutions **)
   3.118 -
   3.119 -fun exceeded limit = (limit <= 0)
   3.120 -fun exceeded_limit (limit, _, _) = exceeded limit
   3.121 -
   3.122 -
   3.123 -fun derived_subst subst' subst = subst' |> Vartab.forall (fn (n, (_, T)) => 
   3.124 -  Vartab.lookup subst n |> Option.map (equal T o snd) |> the_default false)
   3.125 -
   3.126 -fun eq_subst (subst1, subst2) =
   3.127 -  derived_subst subst1 subst2 andalso derived_subst subst2 subst1
   3.128 -
   3.129 -
   3.130 -fun with_all_grounds cx grounds f =
   3.131 -  if exceeded_limit cx then I else Symtab.fold f grounds
   3.132 -
   3.133 -fun with_all_type_combinations cx schematics f (n, Ts) =
   3.134 -  if exceeded_limit cx then I
   3.135 -  else fold_product f (Symtab.lookup_list schematics n) Ts
   3.136 -
   3.137 -fun derive_new_substs thy cx new_grounds schematics subst =
   3.138 -  with_all_grounds cx new_grounds
   3.139 -    (with_all_type_combinations cx schematics (fn T => fn U =>
   3.140 -      (case try (Sign.typ_match thy (T, U)) subst of
   3.141 -        NONE => I
   3.142 -      | SOME subst' => insert eq_subst subst'))) []
   3.143 -
   3.144 -
   3.145 -fun known_subst sub subs1 subs2 subst' =
   3.146 -  let fun derived (_, subst) = derived_subst subst' subst
   3.147 -  in derived sub orelse exists derived subs1 orelse exists derived subs2 end
   3.148 -
   3.149 -fun within_limit f cx = if exceeded_limit cx then cx else f cx
   3.150 -
   3.151 -fun fold_partial_substs derive add = within_limit (
   3.152 -  let
   3.153 -    fun fold_partial [] cx = cx
   3.154 -      | fold_partial (sub :: subs) (limit, subs', next) =
   3.155 -          if exceeded limit then (limit, sub :: subs @ subs', next)
   3.156 -          else sub |> (fn ((generation, full, _), subst) =>
   3.157 -            if full then fold_partial subs (limit, sub :: subs', next)
   3.158 -            else
   3.159 -              (case filter_out (known_subst sub subs subs') (derive subst) of
   3.160 -                [] => fold_partial subs (limit, sub :: subs', next)
   3.161 -              | substs =>
   3.162 -                  (limit, ((generation, full, true), subst) :: subs', next)
   3.163 -                  |> fold (within_limit o add) substs
   3.164 -                  |> fold_partial subs))
   3.165 -  in (fn (limit, subs, next) => fold_partial subs (limit, [], next)) end)
   3.166 -
   3.167 -
   3.168 -fun refine ctxt round known_grounds new_grounds (tvars, schematics) cx =
   3.169 -  let
   3.170 -    val thy = Proof_Context.theory_of ctxt
   3.171 -    val count_partial = Config.get ctxt keep_partial_instances
   3.172 -
   3.173 -    fun add_new_ground subst n T =
   3.174 -      let val T' = Envir.subst_type subst T
   3.175 -      in
   3.176 -        (* FIXME: maybe keep types in a table or net for known_grounds,
   3.177 -           that might improve efficiency here
   3.178 -        *)
   3.179 -        if typ_has_tvars T' then I
   3.180 -        else if member (op =) (Symtab.lookup_list known_grounds n) T' then I
   3.181 -        else Symtab.cons_list (n, T')
   3.182 -      end
   3.183 -
   3.184 -    fun add_new_subst subst (limit, subs, next_grounds) =
   3.185 -      let
   3.186 -        val full = forall (Vartab.defined subst o fst) tvars
   3.187 -        val limit' =
   3.188 -          if full orelse count_partial then limit - 1 else limit
   3.189 -        val sub = ((round, full, false), subst)
   3.190 -        val next_grounds' =
   3.191 -          (schematics, next_grounds)
   3.192 -          |-> Symtab.fold (uncurry (fold o add_new_ground subst))
   3.193 -      in (limit', sub :: subs, next_grounds') end
   3.194 -  in
   3.195 -    fold_partial_substs (derive_new_substs thy cx new_grounds schematics)
   3.196 -      add_new_subst cx
   3.197 -  end
   3.198 -
   3.199 -
   3.200 -(*
   3.201 -  'known_grounds' are all constant names known to occur schematically
   3.202 -  associated with all ground instances considered so far
   3.203 -*)
   3.204 -fun add_relevant_instances known_grounds (Const (c as (n, T))) =
   3.205 -      if typ_has_tvars T orelse not (Symtab.defined known_grounds n) then I
   3.206 -      else if member (op =) (Symtab.lookup_list known_grounds n) T then I
   3.207 -      else Symtab.insert_list (op =) c
   3.208 -  | add_relevant_instances _ _ = I
   3.209 -
   3.210 -fun collect_instances known_grounds thm =
   3.211 -  Term.fold_aterms (add_relevant_instances known_grounds) (Thm.prop_of thm)
   3.212 -
   3.213 -
   3.214 -fun make_subst_ctxt ctxt thm_infos known_grounds substitutions =
   3.215 -  let
   3.216 -    (* The total limit of returned (ground) facts is the number of facts
   3.217 -       given to the monomorphizer increased by max_new_instances.  Since
   3.218 -       initially ground facts are returned anyway, the limit here is not
   3.219 -       counting them. *)
   3.220 -    val limit = Config.get ctxt max_new_instances + 
   3.221 -      fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos 0
   3.222 -
   3.223 -    fun add_ground_consts (Ground thm) = collect_instances known_grounds thm
   3.224 -      | add_ground_consts (Schematic _) = I
   3.225 -    val initial_grounds = fold add_ground_consts thm_infos Symtab.empty
   3.226 -  in (known_grounds, (limit, substitutions, initial_grounds)) end
   3.227 -
   3.228 -fun is_new round initial_round = (round = initial_round)
   3.229 -fun is_active round initial_round = (round > initial_round)
   3.230 -
   3.231 -fun fold_schematic pred f = fold (fn
   3.232 -    Schematic {index, theorem, tvars, schematics, initial_round} =>
   3.233 -      if pred initial_round then f theorem (index, tvars, schematics) else I
   3.234 -  | Ground _ => I)
   3.235 -
   3.236 -fun focus f _ (index, tvars, schematics) (limit, subs, next_grounds) =
   3.237 -  let
   3.238 -    val (limit', isubs', next_grounds') =
   3.239 -      (limit, Inttab.lookup_list subs index, next_grounds)
   3.240 -      |> f (tvars, schematics)
   3.241 -  in (limit', Inttab.update (index, isubs') subs, next_grounds') end
   3.242 -
   3.243 -fun collect_substitutions thm_infos ctxt round subst_ctxt =
   3.244 -  let val (known_grounds, (limit, subs, next_grounds)) = subst_ctxt
   3.245 -  in
   3.246 -    if exceeded limit then subst_ctxt
   3.247 -    else
   3.248 -      let
   3.249 -        fun collect thm _ = collect_instances known_grounds thm
   3.250 -        val new = fold_schematic (is_new round) collect thm_infos next_grounds
   3.251 -
   3.252 -        val known' = Symtab.merge_list (op =) (known_grounds, new)
   3.253 -        val step = focus o refine ctxt round known'
   3.254 -      in
   3.255 -        (limit, subs, Symtab.empty)
   3.256 -        |> not (Symtab.is_empty new) ?
   3.257 -            fold_schematic (is_active round) (step new) thm_infos
   3.258 -        |> fold_schematic (is_new round) (step known') thm_infos
   3.259 -        |> pair known'
   3.260 -      end
   3.261 -  end
   3.262 -
   3.263 -
   3.264 -
   3.265 -(** instantiating schematic theorems **)
   3.266 -
   3.267 -fun super_sort (Ground _) S = S
   3.268 -  | super_sort (Schematic {tvars, ...}) S = merge (op =) (S, maps snd tvars)
   3.269 -
   3.270 -fun new_super_type ctxt thm_infos =
   3.271 -  let val S = fold super_sort thm_infos @{sort type}
   3.272 -  in yield_singleton Variable.invent_types S ctxt |>> SOME o TFree end
   3.273 -
   3.274 -fun add_missing_tvar T (ix, S) subst =
   3.275 -  if Vartab.defined subst ix then subst
   3.276 -  else Vartab.update (ix, (S, T)) subst
   3.277 -
   3.278 -fun complete tvars subst T =
   3.279 -  subst
   3.280 -  |> Vartab.map (K (apsnd (Term.map_atyps (fn TVar _ => T | U => U))))
   3.281 -  |> fold (add_missing_tvar T) tvars
   3.282 -
   3.283 -fun instantiate_all' (mT, ctxt) subs thm_infos =
   3.284 -  let
   3.285 -    val thy = Proof_Context.theory_of ctxt
   3.286 -
   3.287 -    fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
   3.288 -    fun cert' subst = Vartab.fold (cons o cert) subst []
   3.289 -    fun instantiate thm subst = Thm.instantiate (cert' subst, []) thm
   3.290 -
   3.291 -    fun with_subst tvars f ((generation, full, _), subst) =
   3.292 -      if full then SOME (generation, f subst)
   3.293 -      else Option.map (pair generation o f o complete tvars subst) mT
   3.294 -
   3.295 -    fun inst (Ground thm) = [(0, thm)]
   3.296 -      | inst (Schematic {theorem, tvars, index, ...}) =
   3.297 -          Inttab.lookup_list subs index
   3.298 -          |> map_filter (with_subst tvars (instantiate theorem))
   3.299 -  in (map inst thm_infos, ctxt) end
   3.300 -
   3.301 -fun instantiate_all ctxt thm_infos (_, (_, subs, _)) =
   3.302 -  if Config.get ctxt keep_partial_instances then
   3.303 -    let fun is_refined ((_, _, refined), _) = refined
   3.304 -    in
   3.305 -      (Inttab.map (K (filter_out is_refined)) subs, thm_infos)
   3.306 -      |-> instantiate_all' (new_super_type ctxt thm_infos)
   3.307 -    end
   3.308 -  else instantiate_all' (NONE, ctxt) subs thm_infos
   3.309 -
   3.310 -
   3.311 -
   3.312 -(** overall procedure **)
   3.313 -
   3.314 -fun limit_rounds ctxt f =
   3.315 -  let
   3.316 -    val max = Config.get ctxt max_rounds
   3.317 -    fun round i x = if i > max then x else round (i + 1) (f ctxt i x)
   3.318 -  in round 1 end
   3.319 -
   3.320 -fun monomorph schematic_consts_of rthms ctxt =
   3.321 -  let
   3.322 -    val (thm_infos, (known_grounds, subs)) = prepare schematic_consts_of rthms
   3.323 -  in
   3.324 -    if Symtab.is_empty known_grounds then
   3.325 -      (map (fn Ground thm => [(0, thm)] | _ => []) thm_infos, ctxt)
   3.326 -    else
   3.327 -      make_subst_ctxt ctxt thm_infos known_grounds subs
   3.328 -      |> limit_rounds ctxt (collect_substitutions thm_infos)
   3.329 -      |> instantiate_all ctxt thm_infos
   3.330 -  end
   3.331 -
   3.332 -
   3.333 -end
   3.334 -