use new monomorphizer for SMT;
authorboehmes
Tue May 31 19:21:20 2011 +0200 (2011-05-31)
changeset 43116e0add071fa10
parent 43115 6773d8a9e351
child 43117 5de84843685f
use new monomorphizer for SMT;
simplify the monomorphizer by inlining functions and proper passing of arguments
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/monomorph.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue May 31 18:13:00 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue May 31 19:21:20 2011 +0200
     1.3 @@ -626,12 +626,44 @@
     1.4      val es = SMT_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
     1.5    in (burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms, ctxt) end
     1.6  
     1.7 +local
     1.8 +  val ignored = member (op =) [@{const_name All}, @{const_name Ex},
     1.9 +    @{const_name Let}, @{const_name If}, @{const_name HOL.eq}]
    1.10 +
    1.11 +  val schematic_consts_of =
    1.12 +    let
    1.13 +      fun collect (@{const SMT.trigger} $ p $ t) =
    1.14 +            collect_trigger p #> collect t
    1.15 +        | collect (t $ u) = collect t #> collect u
    1.16 +        | collect (Abs (_, _, t)) = collect t
    1.17 +        | collect (t as Const (n, _)) = 
    1.18 +            if not (ignored n) then Monomorph.add_schematic_consts_of t else I
    1.19 +        | collect _ = I
    1.20 +      and collect_trigger t =
    1.21 +        let val dest = these o try HOLogic.dest_list 
    1.22 +        in fold (fold collect_pat o dest) (dest t) end
    1.23 +      and collect_pat (Const (@{const_name SMT.pat}, _) $ t) = collect t
    1.24 +        | collect_pat (Const (@{const_name SMT.nopat}, _) $ t) = collect t
    1.25 +        | collect_pat _ = I
    1.26 +    in (fn t => collect t Symtab.empty) end
    1.27 +in
    1.28 +
    1.29 +fun monomorph xthms ctxt =
    1.30 +  let val (xs, thms) = split_list xthms
    1.31 +  in
    1.32 +    (map (pair 1) thms, ctxt)
    1.33 +    |-> Monomorph.monomorph schematic_consts_of
    1.34 +    |>> maps (uncurry (map o pair)) o map2 pair xs o map (map snd)
    1.35 +  end
    1.36 +
    1.37 +end
    1.38 +
    1.39  fun normalize iwthms ctxt =
    1.40    iwthms
    1.41    |> gen_normalize ctxt
    1.42    |> unfold1 ctxt
    1.43    |> rpair ctxt
    1.44 -  |-> SMT_Monomorph.monomorph
    1.45 +  |-> monomorph
    1.46    |-> unfold2
    1.47    |-> apply_extra_norms
    1.48  
     2.1 --- a/src/HOL/Tools/monomorph.ML	Tue May 31 18:13:00 2011 +0200
     2.2 +++ b/src/HOL/Tools/monomorph.ML	Tue May 31 19:21:20 2011 +0200
     2.3 @@ -91,31 +91,29 @@
     2.4      schematics: typ list Symtab.table,
     2.5      initial_round: int }
     2.6  
     2.7 -fun make_thm_info index initial_round schematics thm =
     2.8 -  if Symtab.is_empty schematics then Ground thm
     2.9 -  else Schematic {
    2.10 -    index = index,
    2.11 -    theorem = thm,
    2.12 -    tvars = Term.add_tvars (Thm.prop_of thm) [],
    2.13 -    schematics = schematics,
    2.14 -    initial_round = initial_round }
    2.15 -
    2.16  fun prepare schematic_consts_of rthms =
    2.17    let
    2.18      val empty_subst = ((0, false, false), Vartab.empty)
    2.19  
    2.20      fun prep (r, thm) ((i, idx), (consts, substs)) =
    2.21 -      let
    2.22 -        (* increase indices to avoid clashes of type variables *)
    2.23 -        val thm' = Thm.incr_indexes idx thm
    2.24 -        val idx' = Thm.maxidx_of thm' + 1
    2.25 -        val schematics = schematic_consts_of (Thm.prop_of thm')
    2.26 -        val consts' =
    2.27 -          Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts
    2.28 -        val substs' = Inttab.update (i, [empty_subst]) substs
    2.29 -      in
    2.30 -        (make_thm_info i r schematics thm', ((i+1, idx'), (consts', substs')))
    2.31 -      end
    2.32 +      if not (Term.exists_type typ_has_tvars (Thm.prop_of thm)) then
    2.33 +        (Ground thm, ((i+1, idx + Thm.maxidx_of thm + 1), (consts, substs)))
    2.34 +      else
    2.35 +        let
    2.36 +          (* increase indices to avoid clashes of type variables *)
    2.37 +          val thm' = Thm.incr_indexes idx thm
    2.38 +          val idx' = Thm.maxidx_of thm' + 1
    2.39 +          val schematics = schematic_consts_of (Thm.prop_of thm')
    2.40 +          val consts' =
    2.41 +            Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts
    2.42 +          val substs' = Inttab.update (i, [empty_subst]) substs
    2.43 +          val thm_info = Schematic {
    2.44 +            index = i,
    2.45 +            theorem = thm',
    2.46 +            tvars = Term.add_tvars (Thm.prop_of thm') [],
    2.47 +            schematics = schematics,
    2.48 +            initial_round = r }
    2.49 +      in (thm_info, ((i+1, idx'), (consts', substs'))) end
    2.50    in fold_map prep rthms ((0, 0), (Symtab.empty, Inttab.empty)) ||> snd end
    2.51  
    2.52  
    2.53 @@ -212,14 +210,14 @@
    2.54    end
    2.55  
    2.56  
    2.57 -fun make_subst_ctxt ctxt thm_infos (known_grounds, substitutions) =
    2.58 +fun make_subst_ctxt ctxt thm_infos known_grounds substitutions =
    2.59    let
    2.60      val limit = Config.get ctxt max_new_instances
    2.61  
    2.62      fun add_ground_consts (Ground thm) = collect_instances known_grounds thm
    2.63        | add_ground_consts (Schematic _) = I
    2.64      val initial_grounds = fold add_ground_consts thm_infos Symtab.empty
    2.65 -  in (thm_infos, (known_grounds, (limit, substitutions, initial_grounds))) end
    2.66 +  in (known_grounds, (limit, substitutions, initial_grounds)) end
    2.67  
    2.68  fun with_new round f thm_info =
    2.69    (case thm_info of
    2.70 @@ -235,7 +233,7 @@
    2.71        else f (round, index, theorem, tvars, schematics)
    2.72    | Ground _ => I)
    2.73  
    2.74 -fun collect_substitutions ctxt round thm_infos (known_grounds, subst_ctxt) =
    2.75 +fun collect_substitutions thm_infos ctxt round (known_grounds, subst_ctxt) =
    2.76    let val (limit, substitutions, next_grounds) = subst_ctxt
    2.77    in
    2.78      (*
    2.79 @@ -311,24 +309,31 @@
    2.80  
    2.81  (** overall procedure **)
    2.82  
    2.83 -fun limit_rounds ctxt f thm_infos =
    2.84 +fun limit_rounds ctxt f =
    2.85    let
    2.86      val max = Config.get ctxt max_rounds
    2.87  
    2.88 -    fun round _ (true, x) = (thm_infos, x)
    2.89 +    fun round _ (true, x) = x
    2.90        | round i (_, x) =
    2.91 -          if i <= max then round (i + 1) (f ctxt i thm_infos x)
    2.92 +          if i <= max then round (i + 1) (f ctxt i x)
    2.93            else (
    2.94              show_info ctxt "Warning: Monomorphization limit reached";
    2.95 -            (thm_infos, x))
    2.96 +            x)
    2.97    in round 1 o pair false end
    2.98  
    2.99  fun monomorph schematic_consts_of rthms ctxt =
   2.100 -  rthms
   2.101 -  |> prepare schematic_consts_of
   2.102 -  |-> make_subst_ctxt ctxt
   2.103 -  |-> limit_rounds ctxt collect_substitutions
   2.104 -  |-> instantiate_all ctxt
   2.105 +  let
   2.106 +    val (thm_infos, (known_grounds, substitutions)) =
   2.107 +      prepare schematic_consts_of rthms
   2.108 +  in
   2.109 +    if Symtab.is_empty known_grounds then
   2.110 +      (map (single o pair 0 o snd) rthms, ctxt)
   2.111 +    else
   2.112 +      make_subst_ctxt ctxt thm_infos known_grounds substitutions
   2.113 +      |> limit_rounds ctxt (collect_substitutions thm_infos)
   2.114 +      |> instantiate_all ctxt thm_infos
   2.115 +  end
   2.116 +
   2.117  
   2.118  end
   2.119