src/HOL/Tools/SMT/smt_monomorph.ML
author boehmes
Wed Nov 24 15:33:35 2010 +0100 (2010-11-24)
changeset 40686 4725ed462387
parent 40512 fd218201da5e
child 41063 0828bfa70b20
permissions -rw-r--r--
swap names for built-in tester functions (to better reflect the intuition of what they do);
eta-expand all built-in functions (even those which are only partially supported)
     1 (*  Title:      HOL/Tools/SMT/smt_monomorph.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Monomorphization of theorems, i.e., computation of all (necessary) instances.
     5 *)
     6 
     7 signature SMT_MONOMORPH =
     8 sig
     9   val monomorph: (int * thm) list -> Proof.context ->
    10     (int * thm) list * Proof.context
    11 end
    12 
    13 structure SMT_Monomorph: SMT_MONOMORPH =
    14 struct
    15 
    16 val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
    17 
    18 val ignored = member (op =) [
    19   @{const_name All}, @{const_name Ex}, @{const_name Let}, @{const_name If},
    20   @{const_name HOL.eq}]
    21 
    22 fun is_const f (n, T) = not (ignored n) andalso f T
    23 fun add_const_if f g (Const c) = if is_const f c then g c else I
    24   | add_const_if _ _ _ = I
    25 
    26 fun collect_consts_if f g thm =
    27   Term.fold_aterms (add_const_if f g) (Thm.prop_of thm)
    28 
    29 fun add_consts f =
    30   collect_consts_if f (fn (n, T) => Symtab.map_entry n (insert (op =) T))
    31 
    32 val insert_const = Ord_List.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
    33 fun tvar_consts_of thm = collect_consts_if typ_has_tvars insert_const thm []
    34 
    35 
    36 fun incr_indexes irules =
    37   let
    38     fun inc (i, thm) idx =
    39       ((i, Thm.incr_indexes idx thm), Thm.maxidx_of thm + idx + 1)
    40   in fst (fold_map inc irules 0) end
    41 
    42 
    43 (* Compute all substitutions from the types "Ts" to all relevant
    44    types in "grounds", with respect to the given substitution. *)
    45 fun new_substitutions thy grounds (n, T) subst =
    46   if not (typ_has_tvars T) then [subst]
    47   else
    48     Symtab.lookup_list grounds n
    49     |> map_filter (try (fn U => Sign.typ_match thy (T, U) subst))
    50     |> cons subst
    51 
    52 
    53 (* Instantiate a set of constants with a substitution.  Also collect
    54    all new ground instances for the next round of specialization. *)
    55 fun apply_subst grounds consts subst =
    56   let
    57     fun is_new_ground (n, T) = not (typ_has_tvars T) andalso
    58       not (member (op =) (Symtab.lookup_list grounds n) T)
    59 
    60     fun apply_const (n, T) new_grounds =
    61       let val c = (n, Envir.subst_type subst T)
    62       in
    63         new_grounds
    64         |> is_new_ground c ? Symtab.insert_list (op =) c
    65         |> pair c
    66       end
    67   in fold_map apply_const consts #>> pair subst end
    68 
    69 
    70 (* Compute new substitutions for the theorem "thm", based on
    71    previously found substitutions.
    72      Also collect new grounds, i.e., instantiated constants
    73    (without schematic types) which do not occur in any of the
    74    previous rounds. Note that thus no schematic type variables are
    75    shared among theorems. *)
    76 fun specialize thy all_grounds new_grounds (irule, scs) =
    77   let
    78     fun spec (subst, consts) next_grounds =
    79       [subst]
    80       |> fold (maps o new_substitutions thy new_grounds) consts
    81       |> rpair next_grounds
    82       |-> fold_map (apply_subst all_grounds consts)
    83   in
    84     fold_map spec scs #>> (fn scss =>
    85     (irule, fold (fold (insert (eq_snd (op =)))) scss []))
    86   end
    87 
    88 
    89 (* Compute all necessary substitutions.
    90      Instead of operating on the propositions of the theorems, the
    91    computation uses only the constants occurring with schematic type
    92    variables in the propositions. To ease comparisons, such sets of
    93    costants are always kept in their initial order. *)
    94 fun incremental_monomorph ctxt limit all_grounds new_grounds irules =
    95   let
    96     val thy = ProofContext.theory_of ctxt
    97     val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds)
    98     val spec = specialize thy all_grounds' new_grounds
    99     val (irs, new_grounds') = fold_map spec irules Symtab.empty
   100   in
   101     if Symtab.is_empty new_grounds' then irs
   102     else if limit > 0
   103     then incremental_monomorph ctxt (limit-1) all_grounds' new_grounds' irs
   104     else
   105      (SMT_Config.verbose_msg ctxt (K "Warning: Monomorphization limit reached")
   106       (); irs)
   107   end
   108 
   109 
   110 fun filter_most_specific thy =
   111   let
   112     fun typ_match (_, T) (_, U) = Sign.typ_match thy (T, U)
   113 
   114     fun is_trivial subst = Vartab.is_empty subst orelse
   115       forall (fn (v, (S, T)) => TVar (v, S) = T) (Vartab.dest subst)
   116 
   117     fun match general specific =
   118       (case try (fold2 typ_match general specific) Vartab.empty of
   119         NONE => false
   120       | SOME subst => not (is_trivial subst))
   121 
   122     fun most_specific _ [] = []
   123       | most_specific css ((ss, cs) :: scs) =
   124           let val substs = most_specific (cs :: css) scs
   125           in
   126             if exists (match cs) css orelse exists (match cs o snd) scs
   127             then substs else ss :: substs
   128           end
   129 
   130   in most_specific [] end
   131 
   132 
   133 fun instantiate thy Tenv =
   134   let
   135     fun replace (v, (_, T)) (U as TVar (u, _)) = if u = v then T else U
   136       | replace _ T = T
   137 
   138     fun complete (vT as (v, _)) subst =
   139       subst
   140       |> not (Vartab.defined subst v) ? Vartab.update vT
   141       |> Vartab.map (K (apsnd (Term.map_atyps (replace vT))))
   142 
   143     fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
   144 
   145     fun inst (i, thm) subst =
   146       let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) []
   147       in (i, Thm.instantiate (cTs, []) thm) end
   148 
   149   in uncurry (map o inst) end
   150 
   151 
   152 fun mono_all ctxt _ [] monos = (monos, ctxt)
   153   | mono_all ctxt limit polys monos =
   154       let
   155         fun invent_types (_, thm) ctxt =
   156           let val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) [])
   157           in
   158             ctxt
   159             |> Variable.invent_types Ss
   160             |>> map2 (fn v => fn (n, S) => (v, (S, TFree (n, S)))) vs
   161           end
   162         val (Tenvs, ctxt') = fold_map invent_types polys ctxt
   163 
   164         val thy = ProofContext.theory_of ctxt'
   165 
   166         val ths = polys
   167           |> map (fn (_, thm) => (thm, [(Vartab.empty, tvar_consts_of thm)]))
   168 
   169         (* all constant names occurring with schematic types *)
   170         val ns = fold (fold (fold (insert (op =) o fst) o snd) o snd) ths []
   171 
   172         (* all known instances with non-schematic types *)
   173         val grounds =
   174           Symtab.make (map (rpair []) ns)
   175           |> fold (add_consts (K true) o snd) monos
   176           |> fold (add_consts (not o typ_has_tvars) o snd) polys
   177       in
   178         polys
   179         |> map (fn (i, thm) => ((i, thm), [(Vartab.empty, tvar_consts_of thm)]))
   180         |> incremental_monomorph ctxt' limit Symtab.empty grounds
   181         |> map (apsnd (filter_most_specific thy))
   182         |> flat o map2 (instantiate thy) Tenvs
   183         |> append monos
   184         |> rpair ctxt'
   185       end
   186 
   187 
   188 (* Instantiate all polymorphic constants (i.e., constants occurring
   189    both with ground types and type variables) with all (necessary)
   190    ground types; thereby create copies of theorems containing those
   191    constants.
   192      To prevent non-termination, there is an upper limit for the
   193    number of recursions involved in the fixpoint construction.
   194      The initial set of theorems must not contain any schematic term
   195    variables, and the final list of theorems does not contain any
   196    schematic type variables anymore. *)
   197 fun monomorph irules ctxt =
   198   irules
   199   |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd)
   200   |>> incr_indexes
   201   |-> mono_all ctxt (Config.get ctxt SMT_Config.monomorph_limit)
   202 
   203 end