removed old (unused) SMT monomorphizer
authorboehmes
Wed Jul 20 09:23:09 2011 +0200 (2011-07-20)
changeset 439273a87cb597832
parent 43917 bce3de79c8ce
child 43928 24d6e759753f
removed old (unused) SMT monomorphizer
src/HOL/IsaMakefile
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_monomorph.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Jul 20 08:46:17 2011 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Jul 20 09:23:09 2011 +0200
     1.3 @@ -373,7 +373,6 @@
     1.4    Tools/SMT/smt_config.ML \
     1.5    Tools/SMT/smt_datatypes.ML \
     1.6    Tools/SMT/smt_failure.ML \
     1.7 -  Tools/SMT/smt_monomorph.ML \
     1.8    Tools/SMT/smt_normalize.ML \
     1.9    Tools/SMT/smt_setup_solvers.ML \
    1.10    Tools/SMT/smt_solver.ML \
     2.1 --- a/src/HOL/SMT.thy	Wed Jul 20 08:46:17 2011 +0200
     2.2 +++ b/src/HOL/SMT.thy	Wed Jul 20 09:23:09 2011 +0200
     2.3 @@ -10,7 +10,6 @@
     2.4    "Tools/SMT/smt_utils.ML"
     2.5    "Tools/SMT/smt_failure.ML"
     2.6    "Tools/SMT/smt_config.ML"
     2.7 -  ("Tools/SMT/smt_monomorph.ML")
     2.8    ("Tools/SMT/smt_builtin.ML")
     2.9    ("Tools/SMT/smt_datatypes.ML")
    2.10    ("Tools/SMT/smt_normalize.ML")
    2.11 @@ -135,7 +134,6 @@
    2.12  
    2.13  subsection {* Setup *}
    2.14  
    2.15 -use "Tools/SMT/smt_monomorph.ML"
    2.16  use "Tools/SMT/smt_builtin.ML"
    2.17  use "Tools/SMT/smt_datatypes.ML"
    2.18  use "Tools/SMT/smt_normalize.ML"
     3.1 --- a/src/HOL/Tools/SMT/smt_monomorph.ML	Wed Jul 20 08:46:17 2011 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,229 +0,0 @@
     3.4 -(*  Title:      HOL/Tools/SMT/smt_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 non-termination, 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 SMT_MONOMORPH =
    3.33 -sig
    3.34 -  val typ_has_tvars: typ -> bool
    3.35 -  val monomorph: ('a * thm) list -> Proof.context ->
    3.36 -    ('a * thm) list * Proof.context
    3.37 -end
    3.38 -
    3.39 -structure SMT_Monomorph: SMT_MONOMORPH =
    3.40 -struct
    3.41 -
    3.42 -(* utility functions *)
    3.43 -
    3.44 -fun fold_maps f = fold (fn x => uncurry (fold_map (f x)) #>> flat)
    3.45 -
    3.46 -fun pair_trans ((x, y), z) = (x, (y, z))
    3.47 -
    3.48 -val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
    3.49 -
    3.50 -val ignored = member (op =) [@{const_name All}, @{const_name Ex},
    3.51 -  @{const_name Let}, @{const_name If}, @{const_name HOL.eq}]
    3.52 -
    3.53 -fun is_const pred (n, T) = not (ignored n) andalso pred T
    3.54 -
    3.55 -fun collect_consts_if pred f =
    3.56 -  let
    3.57 -    fun collect (@{const SMT.trigger} $ p $ t) = collect_trigger p #> collect t
    3.58 -      | collect (t $ u) = collect t #> collect u
    3.59 -      | collect (Abs (_, _, t)) = collect t
    3.60 -      | collect (Const c) = if is_const pred c then f c else I
    3.61 -      | collect _ = I
    3.62 -    and collect_trigger t =
    3.63 -      let val dest = these o try HOLogic.dest_list 
    3.64 -      in fold (fold collect_pat o dest) (dest t) end
    3.65 -    and collect_pat (Const (@{const_name SMT.pat}, _) $ t) = collect t
    3.66 -      | collect_pat (Const (@{const_name SMT.nopat}, _) $ t) = collect t
    3.67 -      | collect_pat _ = I
    3.68 -  in collect o Thm.prop_of end
    3.69 -
    3.70 -val insert_const = Ord_List.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
    3.71 -
    3.72 -fun tvar_consts_of thm = collect_consts_if typ_has_tvars insert_const thm []
    3.73 -
    3.74 -fun add_const_types pred =
    3.75 -  collect_consts_if pred (fn (n, T) => Symtab.map_entry n (insert (op =) T))
    3.76 -
    3.77 -fun incr_indexes ithms =
    3.78 -  let
    3.79 -    fun inc (i, thm) idx =
    3.80 -      ((i, Thm.incr_indexes idx thm), Thm.maxidx_of thm + idx + 1)
    3.81 -  in fst (fold_map inc ithms 0) end
    3.82 -
    3.83 -
    3.84 -
    3.85 -(* search for necessary substitutions *)
    3.86 -
    3.87 -fun new_substitutions thy limit grounds (n, T) subst instances =
    3.88 -  if not (typ_has_tvars T) then ([subst], instances)
    3.89 -  else
    3.90 -    Symtab.lookup_list grounds n
    3.91 -    |> map_filter (try (fn U => Sign.typ_match thy (T, U) subst))
    3.92 -    |> (fn substs => (substs, instances - length substs))
    3.93 -    |>> take limit (* limit the breadth of the search as well as the width *)
    3.94 -    |>> cons subst
    3.95 -
    3.96 -fun apply_subst grounds consts subst =
    3.97 -  let
    3.98 -    fun is_new_ground (n, T) = not (typ_has_tvars T) andalso
    3.99 -      not (member (op =) (Symtab.lookup_list grounds n) T)
   3.100 -
   3.101 -    fun apply_const (n, T) new_grounds =
   3.102 -      let val c = (n, Envir.subst_type subst T)
   3.103 -      in
   3.104 -        new_grounds
   3.105 -        |> is_new_ground c ? Symtab.insert_list (op =) c
   3.106 -        |> pair c
   3.107 -      end
   3.108 -  in fold_map apply_const consts #>> pair subst end
   3.109 -
   3.110 -fun specialize thy limit all_grounds new_grounds scs =
   3.111 -  let
   3.112 -    fun spec (subst, consts) (next_grounds, instances) =
   3.113 -      ([subst], instances)
   3.114 -      |> fold_maps (new_substitutions thy limit new_grounds) consts
   3.115 -      |>> rpair next_grounds
   3.116 -      |>> uncurry (fold_map (apply_subst all_grounds consts))
   3.117 -      |> pair_trans
   3.118 -  in
   3.119 -    fold_map spec scs #>> (fn scss =>
   3.120 -    fold (fold (insert (eq_snd (op =)))) scss [])
   3.121 -  end
   3.122 -
   3.123 -val limit_reached_warning = "Warning: Monomorphization limit reached"
   3.124 -
   3.125 -fun search_substitutions ctxt limit instances all_grounds new_grounds scss =
   3.126 -  let
   3.127 -    val thy = Proof_Context.theory_of ctxt
   3.128 -    val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
   3.129 -    val spec = specialize thy limit all_grounds' new_grounds
   3.130 -    val (scss', (new_grounds', instances')) =
   3.131 -      fold_map spec scss (Symtab.empty, instances)
   3.132 -  in
   3.133 -    if Symtab.is_empty new_grounds' then scss'
   3.134 -    else if limit > 0 andalso instances' > 0 then
   3.135 -      search_substitutions ctxt (limit-1) instances' all_grounds' new_grounds'
   3.136 -        scss'
   3.137 -    else (SMT_Config.verbose_msg ctxt (K limit_reached_warning) (); scss')
   3.138 -  end
   3.139 -
   3.140 -
   3.141 -
   3.142 -(* instantiation *)
   3.143 -
   3.144 -fun filter_most_specific thy =
   3.145 -  let
   3.146 -    fun typ_match (_, T) (_, U) = Sign.typ_match thy (T, U)
   3.147 -
   3.148 -    fun is_trivial subst = Vartab.is_empty subst orelse
   3.149 -      forall (fn (v, (S, T)) => TVar (v, S) = T) (Vartab.dest subst)
   3.150 -
   3.151 -    fun match general specific =
   3.152 -      (case try (fold2 typ_match general specific) Vartab.empty of
   3.153 -        NONE => false
   3.154 -      | SOME subst => not (is_trivial subst))
   3.155 -
   3.156 -    fun most_specific _ [] = []
   3.157 -      | most_specific css ((ss, cs) :: scs) =
   3.158 -          let val substs = most_specific (cs :: css) scs
   3.159 -          in
   3.160 -            if exists (match cs) css orelse exists (match cs o snd) scs
   3.161 -            then substs else ss :: substs
   3.162 -          end
   3.163 -
   3.164 -  in most_specific [] end
   3.165 -
   3.166 -fun instantiate full (i, thm) substs (ithms, ctxt) =
   3.167 -  let
   3.168 -    val thy = Proof_Context.theory_of ctxt
   3.169 -
   3.170 -    val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) [])
   3.171 -    val (Tenv, ctxt') =
   3.172 -      ctxt
   3.173 -      |> Variable.invent_types Ss
   3.174 -      |>> map2 (fn v => fn (n, S) => (v, (S, TFree (n, S)))) vs
   3.175 -
   3.176 -    exception PARTIAL_INST of unit
   3.177 -
   3.178 -    fun update_subst vT subst =
   3.179 -      if full then Vartab.update vT subst
   3.180 -      else raise PARTIAL_INST ()
   3.181 -
   3.182 -    fun replace (v, (_, T)) (U as TVar (u, _)) = if u = v then T else U
   3.183 -      | replace _ T = T
   3.184 -
   3.185 -    fun complete (vT as (v, _)) subst =
   3.186 -      subst
   3.187 -      |> not (Vartab.defined subst v) ? update_subst vT
   3.188 -      |> Vartab.map (K (apsnd (Term.map_atyps (replace vT))))
   3.189 -
   3.190 -    fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
   3.191 -
   3.192 -    fun inst subst =
   3.193 -      let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) []
   3.194 -      in SOME (i, Thm.instantiate (cTs, []) thm) end
   3.195 -      handle PARTIAL_INST () => NONE
   3.196 -
   3.197 -  in (map_filter inst substs @ ithms, if full then ctxt' else ctxt) end
   3.198 -
   3.199 -
   3.200 -
   3.201 -(* overall procedure *)
   3.202 -
   3.203 -fun mono_all ctxt polys monos =
   3.204 -  let
   3.205 -    val scss = map (single o pair Vartab.empty o tvar_consts_of o snd) polys
   3.206 -
   3.207 -    (* all known non-schematic instances of polymorphic constants: find all
   3.208 -       names of polymorphic constants, then add all known ground types *)
   3.209 -    val grounds =
   3.210 -      Symtab.empty
   3.211 -      |> fold (fold (fold (Symtab.update o rpair [] o fst) o snd)) scss
   3.212 -      |> fold (add_const_types (K true) o snd) monos
   3.213 -      |> fold (add_const_types (not o typ_has_tvars) o snd) polys
   3.214 -
   3.215 -    val limit = Config.get ctxt SMT_Config.monomorph_limit
   3.216 -    val instances = Config.get ctxt SMT_Config.monomorph_instances
   3.217 -    val full = Config.get ctxt SMT_Config.monomorph_full
   3.218 -  in
   3.219 -    scss
   3.220 -    |> search_substitutions ctxt limit instances Symtab.empty grounds
   3.221 -    |> map (filter_most_specific (Proof_Context.theory_of ctxt))
   3.222 -    |> rpair (monos, ctxt)
   3.223 -    |-> fold2 (instantiate full) polys
   3.224 -  end
   3.225 -
   3.226 -fun monomorph irules ctxt =
   3.227 -  irules
   3.228 -  |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd)
   3.229 -  |>> incr_indexes  (* avoid clashes of schematic type variables *)
   3.230 -  |-> (fn [] => rpair ctxt | polys => mono_all ctxt polys)
   3.231 -
   3.232 -end