1.1 --- a/src/HOL/SMT/Tools/smt_monomorph.ML Wed May 12 23:54:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,201 +0,0 @@
1.4 -(* Title: HOL/SMT/Tools/smt_monomorph.ML
1.5 - Author: Sascha Boehme, TU Muenchen
1.6 -
1.7 -Monomorphization of theorems, i.e., computation of all (necessary) instances.
1.8 -*)
1.9 -
1.10 -signature SMT_MONOMORPH =
1.11 -sig
1.12 - val monomorph: thm list -> Proof.context -> thm list * Proof.context
1.13 -end
1.14 -
1.15 -structure SMT_Monomorph: SMT_MONOMORPH =
1.16 -struct
1.17 -
1.18 -val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
1.19 -
1.20 -val ignored = member (op =) [
1.21 - @{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
1.22 - @{const_name "op ="}, @{const_name zero_class.zero},
1.23 - @{const_name one_class.one}, @{const_name number_of}]
1.24 -
1.25 -fun is_const f (n, T) = not (ignored n) andalso f T
1.26 -fun add_const_if f g (Const c) = if is_const f c then g c else I
1.27 - | add_const_if _ _ _ = I
1.28 -
1.29 -fun collect_consts_if f g thm =
1.30 - Term.fold_aterms (add_const_if f g) (Thm.prop_of thm)
1.31 -
1.32 -fun add_consts f =
1.33 - collect_consts_if f (fn (n, T) => Symtab.map_entry n (insert (op =) T))
1.34 -
1.35 -val insert_const = OrdList.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
1.36 -fun tvar_consts_of thm = collect_consts_if typ_has_tvars insert_const thm []
1.37 -
1.38 -
1.39 -fun incr_indexes thms =
1.40 - let fun inc thm idx = (Thm.incr_indexes idx thm, Thm.maxidx_of thm + idx + 1)
1.41 - in fst (fold_map inc thms 0) end
1.42 -
1.43 -
1.44 -(* Compute all substitutions from the types "Ts" to all relevant
1.45 - types in "grounds", with respect to the given substitution. *)
1.46 -fun new_substitutions thy grounds (n, T) subst =
1.47 - if not (typ_has_tvars T) then [subst]
1.48 - else
1.49 - Symtab.lookup_list grounds n
1.50 - |> map_filter (try (fn U => Sign.typ_match thy (T, U) subst))
1.51 - |> cons subst
1.52 -
1.53 -
1.54 -(* Instantiate a set of constants with a substitution. Also collect
1.55 - all new ground instances for the next round of specialization. *)
1.56 -fun apply_subst grounds consts subst =
1.57 - let
1.58 - fun is_new_ground (n, T) = not (typ_has_tvars T) andalso
1.59 - not (member (op =) (Symtab.lookup_list grounds n) T)
1.60 -
1.61 - fun apply_const (n, T) new_grounds =
1.62 - let val c = (n, Envir.subst_type subst T)
1.63 - in
1.64 - new_grounds
1.65 - |> is_new_ground c ? Symtab.insert_list (op =) c
1.66 - |> pair c
1.67 - end
1.68 - in fold_map apply_const consts #>> pair subst end
1.69 -
1.70 -
1.71 -(* Compute new substitutions for the theorem "thm", based on
1.72 - previously found substitutions.
1.73 - Also collect new grounds, i.e., instantiated constants
1.74 - (without schematic types) which do not occur in any of the
1.75 - previous rounds. Note that thus no schematic type variables are
1.76 - shared among theorems. *)
1.77 -fun specialize thy all_grounds new_grounds (thm, scs) =
1.78 - let
1.79 - fun spec (subst, consts) next_grounds =
1.80 - [subst]
1.81 - |> fold (maps o new_substitutions thy new_grounds) consts
1.82 - |> rpair next_grounds
1.83 - |-> fold_map (apply_subst all_grounds consts)
1.84 - in
1.85 - fold_map spec scs #>> (fn scss =>
1.86 - (thm, fold (fold (insert (eq_snd (op =)))) scss []))
1.87 - end
1.88 -
1.89 -
1.90 -(* Compute all necessary substitutions.
1.91 - Instead of operating on the propositions of the theorems, the
1.92 - computation uses only the constants occurring with schematic type
1.93 - variables in the propositions. To ease comparisons, such sets of
1.94 - costants are always kept in their initial order. *)
1.95 -fun incremental_monomorph thy limit all_grounds new_grounds ths =
1.96 - let
1.97 - val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
1.98 - val spec = specialize thy all_grounds' new_grounds
1.99 - val (ths', new_grounds') = fold_map spec ths Symtab.empty
1.100 - in
1.101 - if Symtab.is_empty new_grounds' then ths'
1.102 - else if limit > 0
1.103 - then incremental_monomorph thy (limit-1) all_grounds' new_grounds' ths'
1.104 - else (warning "SMT: monomorphization limit reached"; ths')
1.105 - end
1.106 -
1.107 -
1.108 -fun filter_most_specific thy =
1.109 - let
1.110 - fun typ_match (_, T) (_, U) = Sign.typ_match thy (T, U)
1.111 -
1.112 - fun is_trivial subst = Vartab.is_empty subst orelse
1.113 - forall (fn (v, (S, T)) => TVar (v, S) = T) (Vartab.dest subst)
1.114 -
1.115 - fun match general specific =
1.116 - (case try (fold2 typ_match general specific) Vartab.empty of
1.117 - NONE => false
1.118 - | SOME subst => not (is_trivial subst))
1.119 -
1.120 - fun most_specific _ [] = []
1.121 - | most_specific css ((ss, cs) :: scs) =
1.122 - let val substs = most_specific (cs :: css) scs
1.123 - in
1.124 - if exists (match cs) css orelse exists (match cs o snd) scs
1.125 - then substs else ss :: substs
1.126 - end
1.127 -
1.128 - in most_specific [] end
1.129 -
1.130 -
1.131 -fun instantiate thy Tenv =
1.132 - let
1.133 - fun replace (v, (_, T)) (U as TVar (u, _)) = if u = v then T else U
1.134 - | replace _ T = T
1.135 -
1.136 - fun complete (vT as (v, _)) subst =
1.137 - subst
1.138 - |> not (Vartab.defined subst v) ? Vartab.update vT
1.139 - |> Vartab.map (apsnd (Term.map_atyps (replace vT)))
1.140 -
1.141 - fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
1.142 -
1.143 - fun inst thm subst =
1.144 - let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) []
1.145 - in Thm.instantiate (cTs, []) thm end
1.146 -
1.147 - in uncurry (map o inst) end
1.148 -
1.149 -
1.150 -fun mono_all ctxt _ [] monos = (monos, ctxt)
1.151 - | mono_all ctxt limit polys monos =
1.152 - let
1.153 - fun invent_types thm ctxt =
1.154 - let val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) [])
1.155 - in
1.156 - ctxt
1.157 - |> Variable.invent_types Ss
1.158 - |>> map2 (fn v => fn (n, S) => (v, (S, TFree (n, S)))) vs
1.159 - end
1.160 - val (Tenvs, ctxt') = fold_map invent_types polys ctxt
1.161 -
1.162 - val thy = ProofContext.theory_of ctxt'
1.163 -
1.164 - val ths = polys
1.165 - |> map (fn thm => (thm, [(Vartab.empty, tvar_consts_of thm)]))
1.166 -
1.167 - (* all constant names occurring with schematic types *)
1.168 - val ns = fold (fold (fold (insert (op =) o fst) o snd) o snd) ths []
1.169 -
1.170 - (* all known instances with non-schematic types *)
1.171 - val grounds =
1.172 - Symtab.make (map (rpair []) ns)
1.173 - |> fold (add_consts (K true)) monos
1.174 - |> fold (add_consts (not o typ_has_tvars)) polys
1.175 - in
1.176 - polys
1.177 - |> map (fn thm => (thm, [(Vartab.empty, tvar_consts_of thm)]))
1.178 - |> incremental_monomorph thy limit Symtab.empty grounds
1.179 - |> map (apsnd (filter_most_specific thy))
1.180 - |> flat o map2 (instantiate thy) Tenvs
1.181 - |> append monos
1.182 - |> rpair ctxt'
1.183 - end
1.184 -
1.185 -
1.186 -val monomorph_limit = 10
1.187 -
1.188 -
1.189 -(* Instantiate all polymorphic constants (i.e., constants occurring
1.190 - both with ground types and type variables) with all (necessary)
1.191 - ground types; thereby create copies of theorems containing those
1.192 - constants.
1.193 - To prevent non-termination, there is an upper limit for the
1.194 - number of recursions involved in the fixpoint construction.
1.195 - The initial set of theorems must not contain any schematic term
1.196 - variables, and the final list of theorems does not contain any
1.197 - schematic type variables anymore. *)
1.198 -fun monomorph thms ctxt =
1.199 - thms
1.200 - |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of)
1.201 - |>> incr_indexes
1.202 - |-> mono_all ctxt monomorph_limit
1.203 -
1.204 -end