src/HOL/Tools/SMT/smt_monomorph.ML
changeset 42183 173b0f488428
parent 42181 8f25605e646c
child 42190 b6b5846504cd
     1.1 --- a/src/HOL/Tools/SMT/smt_monomorph.ML	Thu Mar 31 11:16:54 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Thu Mar 31 14:02:03 2011 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  signature SMT_MONOMORPH =
     1.5  sig
     1.6    val typ_has_tvars: typ -> bool
     1.7 -  val monomorph: ('a * thm) list -> Proof.context ->
     1.8 +  val monomorph: bool -> ('a * thm) list -> Proof.context ->
     1.9      ('a * thm) list * Proof.context
    1.10  end
    1.11  
    1.12 @@ -160,37 +160,44 @@
    1.13  
    1.14    in most_specific [] end
    1.15  
    1.16 -fun instantiate (i, thm) substs (ithms, ctxt) =
    1.17 +fun instantiate full (i, thm) substs (ithms, ctxt) =
    1.18    let
    1.19 +    val thy = ProofContext.theory_of ctxt
    1.20 +
    1.21      val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) [])
    1.22      val (Tenv, ctxt') =
    1.23        ctxt
    1.24        |> Variable.invent_types Ss
    1.25        |>> map2 (fn v => fn (n, S) => (v, (S, TFree (n, S)))) vs
    1.26  
    1.27 -    val thy = ProofContext.theory_of ctxt'
    1.28 +    exception PARTIAL_INST of unit
    1.29 +
    1.30 +    fun update_subst vT subst =
    1.31 +      if full then Vartab.update vT subst
    1.32 +      else raise PARTIAL_INST ()
    1.33  
    1.34      fun replace (v, (_, T)) (U as TVar (u, _)) = if u = v then T else U
    1.35        | replace _ T = T
    1.36  
    1.37      fun complete (vT as (v, _)) subst =
    1.38        subst
    1.39 -      |> not (Vartab.defined subst v) ? Vartab.update vT
    1.40 +      |> not (Vartab.defined subst v) ? update_subst vT
    1.41        |> Vartab.map (K (apsnd (Term.map_atyps (replace vT))))
    1.42  
    1.43      fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
    1.44  
    1.45      fun inst subst =
    1.46        let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) []
    1.47 -      in (i, Thm.instantiate (cTs, []) thm) end
    1.48 +      in SOME (i, Thm.instantiate (cTs, []) thm) end
    1.49 +      handle PARTIAL_INST () => NONE
    1.50  
    1.51 -  in (map inst substs @ ithms, ctxt') end
    1.52 +  in (map_filter inst substs @ ithms, if full then ctxt' else ctxt) end
    1.53  
    1.54  
    1.55  
    1.56  (* overall procedure *)
    1.57  
    1.58 -fun mono_all ctxt polys monos =
    1.59 +fun mono_all full ctxt polys monos =
    1.60    let
    1.61      val scss = map (single o pair Vartab.empty o tvar_consts_of o snd) polys
    1.62  
    1.63 @@ -209,13 +216,13 @@
    1.64      |> search_substitutions ctxt limit instances Symtab.empty grounds
    1.65      |> map (filter_most_specific (ProofContext.theory_of ctxt))
    1.66      |> rpair (monos, ctxt)
    1.67 -    |-> fold2 instantiate polys
    1.68 +    |-> fold2 (instantiate full) polys
    1.69    end
    1.70  
    1.71 -fun monomorph irules ctxt =
    1.72 +fun monomorph full irules ctxt =
    1.73    irules
    1.74    |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd)
    1.75    |>> incr_indexes  (* avoid clashes of schematic type variables *)
    1.76 -  |-> (fn [] => rpair ctxt | polys => mono_all ctxt polys)
    1.77 +  |-> (fn [] => rpair ctxt | polys => mono_all full ctxt polys)
    1.78  
    1.79  end