src/Tools/Compute_Oracle/linker.ML
author wenzelm
Fri Jul 17 23:11:40 2009 +0200 (2009-07-17)
changeset 32035 8e77b6a250d5
parent 31971 8c1b845ed105
child 32740 9dd0a2f83429
permissions -rw-r--r--
tuned/modernized Envir.subst_XXX;
haftmann@24584
     1
(*  Title:      Tools/Compute_Oracle/linker.ML
obua@23663
     2
    Author:     Steven Obua
obua@23663
     3
wenzelm@24271
     4
Linker.ML solves the problem that the computing oracle does not
wenzelm@24271
     5
instantiate polymorphic rules. By going through the PCompute interface,
wenzelm@24271
     6
all possible instantiations are resolved by compiling new programs, if
wenzelm@24271
     7
necessary. The obvious disadvantage of this approach is that in the
wenzelm@24271
     8
worst case for each new term to be rewritten, a new program may be
wenzelm@24271
     9
compiled.
obua@23663
    10
*)
obua@23663
    11
wenzelm@24271
    12
(*
obua@23663
    13
   Given constants/frees c_1::t_1, c_2::t_2, ...., c_n::t_n,
obua@23663
    14
   and constants/frees d_1::d_1, d_2::s_2, ..., d_m::s_m
obua@23663
    15
obua@23663
    16
   Find all substitutions S such that
wenzelm@24271
    17
   a) the domain of S is tvars (t_1, ..., t_n)
obua@23663
    18
   b) there are indices i_1, ..., i_k, and j_1, ..., j_k with
obua@23663
    19
      1. S (c_i_1::t_i_1) = d_j_1::s_j_1, ..., S (c_i_k::t_i_k) = d_j_k::s_j_k
obua@23663
    20
      2. tvars (t_i_1, ..., t_i_k) = tvars (t_1, ..., t_n)
obua@23663
    21
*)
wenzelm@24271
    22
signature LINKER =
obua@23663
    23
sig
obua@23663
    24
    exception Link of string
wenzelm@24271
    25
obua@23663
    26
    datatype constant = Constant of bool * string * typ
obua@23663
    27
    val constant_of : term -> constant
obua@23663
    28
obua@23663
    29
    type instances
obua@23663
    30
    type subst = Type.tyenv
wenzelm@24271
    31
obua@23663
    32
    val empty : constant list -> instances
obua@23663
    33
    val typ_of_constant : constant -> typ
wenzelm@24271
    34
    val add_instances : theory -> instances -> constant list -> subst list * instances
obua@23663
    35
    val substs_of : instances -> subst list
obua@23663
    36
    val is_polymorphic : constant -> bool
obua@23663
    37
    val distinct_constants : constant list -> constant list
obua@23663
    38
    val collect_consts : term list -> constant list
obua@23663
    39
end
obua@23663
    40
obua@23663
    41
structure Linker : LINKER = struct
obua@23663
    42
obua@23663
    43
exception Link of string;
obua@23663
    44
obua@23663
    45
type subst = Type.tyenv
obua@23663
    46
obua@23663
    47
datatype constant = Constant of bool * string * typ
obua@23663
    48
fun constant_of (Const (name, ty)) = Constant (false, name, ty)
obua@23663
    49
  | constant_of (Free (name, ty)) = Constant (true, name, ty)
obua@23663
    50
  | constant_of _ = raise Link "constant_of"
obua@23663
    51
obua@23663
    52
fun bool_ord (x,y) = if x then (if y then EQUAL else GREATER) else (if y then LESS else EQUAL)
wenzelm@29269
    53
fun constant_ord (Constant (x1,x2,x3), Constant (y1,y2,y3)) = (prod_ord (prod_ord bool_ord fast_string_ord) TermOrd.typ_ord) (((x1,x2),x3), ((y1,y2),y3))
obua@23663
    54
fun constant_modty_ord (Constant (x1,x2,_), Constant (y1,y2,_)) = (prod_ord bool_ord fast_string_ord) ((x1,x2), (y1,y2))
obua@23663
    55
obua@23663
    56
wenzelm@31971
    57
structure Consttab = Table(type key = constant val ord = constant_ord);
wenzelm@31971
    58
structure ConsttabModTy = Table(type key = constant val ord = constant_modty_ord);
obua@23663
    59
obua@23663
    60
fun typ_of_constant (Constant (_, _, ty)) = ty
obua@23663
    61
obua@23663
    62
val empty_subst = (Vartab.empty : Type.tyenv)
obua@23663
    63
wenzelm@24271
    64
fun merge_subst (A:Type.tyenv) (B:Type.tyenv) =
wenzelm@24271
    65
    SOME (Vartab.fold (fn (v, t) =>
wenzelm@24271
    66
                       fn tab =>
wenzelm@24271
    67
                          (case Vartab.lookup tab v of
wenzelm@24271
    68
                               NONE => Vartab.update (v, t) tab
wenzelm@24271
    69
                             | SOME t' => if t = t' then tab else raise Type.TYPE_MATCH)) A B)
obua@23663
    70
    handle Type.TYPE_MATCH => NONE
obua@23663
    71
wenzelm@24271
    72
fun subst_ord (A:Type.tyenv, B:Type.tyenv) =
wenzelm@29269
    73
    (list_ord (prod_ord TermOrd.fast_indexname_ord (prod_ord TermOrd.sort_ord TermOrd.typ_ord))) (Vartab.dest A, Vartab.dest B)
obua@23663
    74
wenzelm@31971
    75
structure Substtab = Table(type key = Type.tyenv val ord = subst_ord);
obua@23663
    76
obua@23768
    77
fun substtab_union c = Substtab.fold Substtab.update c
obua@23663
    78
fun substtab_unions [] = Substtab.empty
obua@23663
    79
  | substtab_unions [c] = c
obua@23663
    80
  | substtab_unions (c::cs) = substtab_union c (substtab_unions cs)
obua@23663
    81
obua@23663
    82
datatype instances = Instances of unit ConsttabModTy.table * Type.tyenv Consttab.table Consttab.table * constant list list * unit Substtab.table
obua@23663
    83
wenzelm@29275
    84
fun is_polymorphic (Constant (_, _, ty)) = not (null (Term.add_tvarsT ty []))
obua@23663
    85
obua@23663
    86
fun distinct_constants cs =
obua@23663
    87
    Consttab.keys (fold (fn c => Consttab.update (c, ())) cs Consttab.empty)
obua@23663
    88
wenzelm@24271
    89
fun empty cs =
wenzelm@24271
    90
    let
wenzelm@24271
    91
        val cs = distinct_constants (filter is_polymorphic cs)
wenzelm@24271
    92
        val old_cs = cs
wenzelm@29275
    93
(*      fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (OldTerm.typ_tvars ty) tab
wenzelm@24271
    94
        val tvars_count = length (Typtab.keys (fold (fn c => fn tab => collect_tvars (typ_of_constant c) tab) cs Typtab.empty))
wenzelm@24271
    95
        fun tvars_of ty = collect_tvars ty Typtab.empty
wenzelm@24271
    96
        val cs = map (fn c => (c, tvars_of (typ_of_constant c))) cs
obua@23663
    97
wenzelm@24271
    98
        fun tyunion A B =
wenzelm@24271
    99
            Typtab.fold
wenzelm@24271
   100
                (fn (v,()) => fn tab => Typtab.update (v, case Typtab.lookup tab v of NONE => 1 | SOME n => n+1) tab)
wenzelm@24271
   101
                A B
obua@23663
   102
obua@23663
   103
        fun is_essential A B =
wenzelm@24271
   104
            Typtab.fold
wenzelm@24271
   105
            (fn (v, ()) => fn essential => essential orelse (case Typtab.lookup B v of NONE => raise Link "is_essential" | SOME n => n=1))
wenzelm@24271
   106
            A false
obua@23663
   107
wenzelm@24271
   108
        fun add_minimal (c', tvs') (tvs, cs) =
wenzelm@24271
   109
            let
wenzelm@24271
   110
                val tvs = tyunion tvs' tvs
wenzelm@24271
   111
                val cs = (c', tvs')::cs
wenzelm@24271
   112
            in
wenzelm@24271
   113
                if forall (fn (c',tvs') => is_essential tvs' tvs) cs then
wenzelm@24271
   114
                    SOME (tvs, cs)
wenzelm@24271
   115
                else
wenzelm@24271
   116
                    NONE
wenzelm@24271
   117
            end
obua@23663
   118
wenzelm@24271
   119
        fun is_spanning (tvs, _) = (length (Typtab.keys tvs) = tvars_count)
obua@23663
   120
wenzelm@24271
   121
        fun generate_minimal_subsets subsets [] = subsets
wenzelm@24271
   122
          | generate_minimal_subsets subsets (c::cs) =
wenzelm@24271
   123
            let
wenzelm@24271
   124
                val subsets' = map_filter (add_minimal c) subsets
wenzelm@24271
   125
            in
wenzelm@24271
   126
                generate_minimal_subsets (subsets@subsets') cs
wenzelm@24271
   127
            end*)
obua@23663
   128
wenzelm@24271
   129
        val minimal_subsets = [old_cs] (*map (fn (tvs, cs) => map fst cs) (filter is_spanning (generate_minimal_subsets [(Typtab.empty, [])] cs))*)
obua@23663
   130
wenzelm@24271
   131
        val constants = Consttab.keys (fold (fold (fn c => Consttab.update (c, ()))) minimal_subsets Consttab.empty)
obua@23663
   132
obua@23663
   133
    in
wenzelm@24271
   134
        Instances (
wenzelm@24271
   135
        fold (fn c => fn tab => ConsttabModTy.update (c, ()) tab) constants ConsttabModTy.empty,
wenzelm@24271
   136
        Consttab.make (map (fn c => (c, Consttab.empty : Type.tyenv Consttab.table)) constants),
wenzelm@24271
   137
        minimal_subsets, Substtab.empty)
obua@23663
   138
    end
obua@23663
   139
obua@23663
   140
local
obua@23663
   141
fun calc ctab substtab [] = substtab
wenzelm@24271
   142
  | calc ctab substtab (c::cs) =
obua@23663
   143
    let
wenzelm@24271
   144
        val csubsts = map snd (Consttab.dest (the (Consttab.lookup ctab c)))
wenzelm@24271
   145
        fun merge_substs substtab subst =
wenzelm@24271
   146
            Substtab.fold (fn (s,_) =>
wenzelm@24271
   147
                           fn tab =>
wenzelm@24271
   148
                              (case merge_subst subst s of NONE => tab | SOME s => Substtab.update (s, ()) tab))
wenzelm@24271
   149
                          substtab Substtab.empty
wenzelm@24271
   150
        val substtab = substtab_unions (map (merge_substs substtab) csubsts)
obua@23663
   151
    in
wenzelm@24271
   152
        calc ctab substtab cs
obua@23663
   153
    end
obua@23663
   154
in
obua@23663
   155
fun calc_substs ctab (cs:constant list) = calc ctab (Substtab.update (empty_subst, ()) Substtab.empty) cs
obua@23663
   156
end
wenzelm@24271
   157
wenzelm@24271
   158
fun add_instances thy (Instances (cfilter, ctab,minsets,substs)) cs =
wenzelm@24271
   159
    let
wenzelm@24271
   160
(*      val _ = writeln (makestring ("add_instances: ", length_cs, length cs, length (Consttab.keys ctab)))*)
wenzelm@24271
   161
        fun calc_instantiations (constant as Constant (free, name, ty)) instantiations =
wenzelm@24271
   162
            Consttab.fold (fn (constant' as Constant (free', name', ty'), insttab) =>
wenzelm@24271
   163
                           fn instantiations =>
wenzelm@24271
   164
                              if free <> free' orelse name <> name' then
wenzelm@24271
   165
                                  instantiations
wenzelm@24271
   166
                              else case Consttab.lookup insttab constant of
wenzelm@24271
   167
                                       SOME _ => instantiations
wenzelm@24271
   168
                                     | NONE => ((constant', (constant, Sign.typ_match thy (ty', ty) empty_subst))::instantiations
wenzelm@24271
   169
                                                handle TYPE_MATCH => instantiations))
wenzelm@24271
   170
                          ctab instantiations
wenzelm@24271
   171
        val instantiations = fold calc_instantiations cs []
wenzelm@24271
   172
        (*val _ = writeln ("instantiations = "^(makestring (length instantiations)))*)
wenzelm@24271
   173
        fun update_ctab (constant', entry) ctab =
wenzelm@24271
   174
            (case Consttab.lookup ctab constant' of
wenzelm@24271
   175
                 NONE => raise Link "internal error: update_ctab"
wenzelm@24271
   176
               | SOME tab => Consttab.update (constant', Consttab.update entry tab) ctab)
wenzelm@24271
   177
        val ctab = fold update_ctab instantiations ctab
wenzelm@24271
   178
        val new_substs = fold (fn minset => fn substs => substtab_union (calc_substs ctab minset) substs)
wenzelm@24271
   179
                              minsets Substtab.empty
wenzelm@24271
   180
        val (added_substs, substs) =
wenzelm@24271
   181
            Substtab.fold (fn (ns, _) =>
wenzelm@24271
   182
                           fn (added, substtab) =>
wenzelm@24271
   183
                              (case Substtab.lookup substs ns of
wenzelm@24271
   184
                                   NONE => (ns::added, Substtab.update (ns, ()) substtab)
wenzelm@24271
   185
                                 | SOME () => (added, substtab)))
wenzelm@24271
   186
                          new_substs ([], substs)
obua@23663
   187
    in
wenzelm@24271
   188
        (added_substs, Instances (cfilter, ctab, minsets, substs))
obua@23663
   189
    end
wenzelm@24271
   190
obua@23663
   191
fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
obua@23663
   192
obua@23663
   193
local
wenzelm@26343
   194
    fun get_thm thmname = PureThy.get_thm (theory "Main") thmname
obua@23663
   195
    val eq_th = get_thm "HOL.eq_reflection"
obua@23663
   196
in
wenzelm@26336
   197
  fun eq_to_meta th = (eq_th OF [th] handle THM _ => th)
obua@23663
   198
end
obua@23663
   199
wenzelm@24271
   200
obua@23663
   201
local
obua@23663
   202
obua@23663
   203
fun collect (Var x) tab = tab
obua@23663
   204
  | collect (Bound _) tab = tab
obua@23663
   205
  | collect (a $ b) tab = collect b (collect a tab)
obua@23663
   206
  | collect (Abs (_, _, body)) tab = collect body tab
obua@23663
   207
  | collect t tab = Consttab.update (constant_of t, ()) tab
obua@23663
   208
obua@23663
   209
in
obua@23663
   210
  fun collect_consts tms = Consttab.keys (fold collect tms Consttab.empty)
obua@23663
   211
end
obua@23663
   212
obua@23663
   213
end
obua@23663
   214
obua@23663
   215
signature PCOMPUTE =
obua@23663
   216
sig
obua@23663
   217
    type pcomputer
wenzelm@24271
   218
obua@23663
   219
    val make : Compute.machine -> theory -> thm list -> Linker.constant list -> pcomputer
obua@25520
   220
    val make_with_cache : Compute.machine -> theory -> term list -> thm list -> Linker.constant list -> pcomputer
obua@25218
   221
    
obua@25218
   222
    val add_instances : pcomputer -> Linker.constant list -> bool 
obua@25218
   223
    val add_instances' : pcomputer -> term list -> bool
obua@23663
   224
obua@23663
   225
    val rewrite : pcomputer -> cterm list -> thm list
obua@25218
   226
    val simplify : pcomputer -> Compute.theorem -> thm
obua@25218
   227
obua@25218
   228
    val make_theorem : pcomputer -> thm -> string list -> Compute.theorem
obua@25218
   229
    val instantiate : pcomputer -> (string * cterm) list -> Compute.theorem -> Compute.theorem
obua@25218
   230
    val evaluate_prem : pcomputer -> int -> Compute.theorem -> Compute.theorem
obua@25218
   231
    val modus_ponens : pcomputer -> int -> thm -> Compute.theorem -> Compute.theorem 
obua@23663
   232
obua@23663
   233
end
obua@23663
   234
obua@23663
   235
structure PCompute : PCOMPUTE = struct
obua@23663
   236
obua@23663
   237
exception PCompute of string
obua@23663
   238
obua@23663
   239
datatype theorem = MonoThm of thm | PolyThm of thm * Linker.instances * thm list
obua@25520
   240
datatype pattern = MonoPattern of term | PolyPattern of term * Linker.instances * term list
obua@23663
   241
obua@25520
   242
datatype pcomputer = PComputer of theory_ref * Compute.computer * theorem list ref * pattern list ref 
obua@23663
   243
obua@23663
   244
(*fun collect_consts (Var x) = []
obua@23663
   245
  | collect_consts (Bound _) = []
obua@23663
   246
  | collect_consts (a $ b) = (collect_consts a)@(collect_consts b)
obua@23663
   247
  | collect_consts (Abs (_, _, body)) = collect_consts body
obua@23663
   248
  | collect_consts t = [Linker.constant_of t]*)
obua@23663
   249
obua@25520
   250
fun computer_of (PComputer (_,computer,_,_)) = computer
obua@25218
   251
obua@25218
   252
fun collect_consts_of_thm th = 
obua@23663
   253
    let
wenzelm@24271
   254
        val th = prop_of th
wenzelm@24271
   255
        val (prems, th) = (Logic.strip_imp_prems th, Logic.strip_imp_concl th)
wenzelm@24271
   256
        val (left, right) = Logic.dest_equals th
obua@23663
   257
    in
wenzelm@24271
   258
        (Linker.collect_consts [left], Linker.collect_consts (right::prems))
wenzelm@24271
   259
    end
obua@23663
   260
obua@23663
   261
fun create_theorem th =
wenzelm@24271
   262
let
obua@23663
   263
    val (left, right) = collect_consts_of_thm th
obua@23663
   264
    val polycs = filter Linker.is_polymorphic left
wenzelm@29275
   265
    val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (OldTerm.typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty
wenzelm@24271
   266
    fun check_const (c::cs) cs' =
wenzelm@24271
   267
        let
wenzelm@29275
   268
            val tvars = OldTerm.typ_tvars (Linker.typ_of_constant c)
wenzelm@24271
   269
            val wrong = fold (fn n => fn wrong => wrong orelse is_none (Typtab.lookup tytab (TVar n))) tvars false
wenzelm@24271
   270
        in
wenzelm@24271
   271
            if wrong then raise PCompute "right hand side of theorem contains type variables which do not occur on the left hand side"
wenzelm@24271
   272
            else
wenzelm@24271
   273
                if null (tvars) then
wenzelm@24271
   274
                    check_const cs (c::cs')
wenzelm@24271
   275
                else
wenzelm@24271
   276
                    check_const cs cs'
wenzelm@24271
   277
        end
obua@23663
   278
      | check_const [] cs' = cs'
wenzelm@24271
   279
    val monocs = check_const right []
obua@23663
   280
in
wenzelm@24271
   281
    if null (polycs) then
wenzelm@24271
   282
        (monocs, MonoThm th)
obua@23663
   283
    else
wenzelm@24271
   284
        (monocs, PolyThm (th, Linker.empty polycs, []))
obua@23663
   285
end
obua@23663
   286
obua@25520
   287
fun create_pattern pat = 
obua@25520
   288
let
obua@25520
   289
    val cs = Linker.collect_consts [pat]
obua@25520
   290
    val polycs = filter Linker.is_polymorphic cs
obua@25520
   291
in
obua@25520
   292
    if null (polycs) then
obua@25520
   293
	MonoPattern pat
obua@25520
   294
    else
obua@25520
   295
	PolyPattern (pat, Linker.empty polycs, [])
obua@25520
   296
end
obua@25520
   297
	     
obua@25520
   298
fun create_computer machine thy pats ths =
obua@23663
   299
    let
wenzelm@24271
   300
        fun add (MonoThm th) ths = th::ths
wenzelm@24271
   301
          | add (PolyThm (_, _, ths')) ths = ths'@ths
obua@25520
   302
	fun addpat (MonoPattern p) pats = p::pats
obua@25520
   303
	  | addpat (PolyPattern (_, _, ps)) pats = ps@pats
wenzelm@24271
   304
        val ths = fold_rev add ths []
obua@25520
   305
	val pats = fold_rev addpat pats []
obua@23663
   306
    in
obua@25520
   307
        Compute.make_with_cache machine thy pats ths
obua@23663
   308
    end
obua@23663
   309
obua@25520
   310
fun update_computer computer pats ths = 
obua@25218
   311
    let
obua@25218
   312
	fun add (MonoThm th) ths = th::ths
obua@25218
   313
	  | add (PolyThm (_, _, ths')) ths = ths'@ths
obua@25520
   314
	fun addpat (MonoPattern p) pats = p::pats
obua@25520
   315
	  | addpat (PolyPattern (_, _, ps)) pats = ps@pats
obua@25218
   316
	val ths = fold_rev add ths []
obua@25520
   317
	val pats = fold_rev addpat pats []
obua@25218
   318
    in
obua@25520
   319
	Compute.update_with_cache computer pats ths
obua@25218
   320
    end
obua@25218
   321
obua@23663
   322
fun conv_subst thy (subst : Type.tyenv) =
obua@23663
   323
    map (fn (iname, (sort, ty)) => (ctyp_of thy (TVar (iname, sort)), ctyp_of thy ty)) (Vartab.dest subst)
obua@23663
   324
obua@25520
   325
fun add_monos thy monocs pats ths =
obua@23663
   326
    let
wenzelm@24271
   327
        val changed = ref false
wenzelm@24271
   328
        fun add monocs (th as (MonoThm _)) = ([], th)
wenzelm@24271
   329
          | add monocs (PolyThm (th, instances, instanceths)) =
wenzelm@24271
   330
            let
wenzelm@24271
   331
                val (newsubsts, instances) = Linker.add_instances thy instances monocs
wenzelm@24271
   332
                val _ = if not (null newsubsts) then changed := true else ()
wenzelm@24271
   333
                val newths = map (fn subst => Thm.instantiate (conv_subst thy subst, []) th) newsubsts
wenzelm@24271
   334
(*              val _ = if not (null newths) then (print ("added new theorems: ", newths); ()) else ()*)
wenzelm@24271
   335
                val newmonos = fold (fn th => fn monos => (snd (collect_consts_of_thm th))@monos) newths []
wenzelm@24271
   336
            in
wenzelm@24271
   337
                (newmonos, PolyThm (th, instances, instanceths@newths))
wenzelm@24271
   338
            end
obua@25520
   339
	fun addpats monocs (pat as (MonoPattern _)) = pat
obua@25520
   340
	  | addpats monocs (PolyPattern (p, instances, instancepats)) =
obua@25520
   341
	    let
obua@25520
   342
		val (newsubsts, instances) = Linker.add_instances thy instances monocs
obua@25520
   343
		val _ = if not (null newsubsts) then changed := true else ()
wenzelm@32035
   344
		val newpats = map (fn subst => Envir.subst_term_types subst p) newsubsts
obua@25520
   345
	    in
obua@25520
   346
		PolyPattern (p, instances, instancepats@newpats)
obua@25520
   347
	    end 
wenzelm@24271
   348
        fun step monocs ths =
wenzelm@24271
   349
            fold_rev (fn th =>
wenzelm@24271
   350
                      fn (newmonos, ths) =>
obua@25520
   351
                         let 
obua@25520
   352
			     val (newmonos', th') = add monocs th 
obua@25520
   353
			 in
wenzelm@24271
   354
                             (newmonos'@newmonos, th'::ths)
wenzelm@24271
   355
                         end)
wenzelm@24271
   356
                     ths ([], [])
obua@25520
   357
        fun loop monocs pats ths =
obua@25520
   358
            let 
obua@25520
   359
		val (monocs', ths') = step monocs ths 
obua@25520
   360
		val pats' = map (addpats monocs) pats
obua@25520
   361
	    in
wenzelm@24271
   362
                if null (monocs') then
obua@25520
   363
                    (pats', ths')
wenzelm@24271
   364
                else
obua@25520
   365
                    loop monocs' pats' ths'
wenzelm@24271
   366
            end
obua@25520
   367
        val result = loop monocs pats ths
obua@23663
   368
    in
wenzelm@24271
   369
        (!changed, result)
wenzelm@24271
   370
    end
obua@23663
   371
obua@23663
   372
datatype cthm = ComputeThm of term list * sort list * term
obua@23663
   373
wenzelm@24271
   374
fun thm2cthm th =
obua@23663
   375
    let
wenzelm@24271
   376
        val {hyps, prop, shyps, ...} = Thm.rep_thm th
obua@23663
   377
    in
wenzelm@24271
   378
        ComputeThm (hyps, shyps, prop)
obua@23663
   379
    end
obua@23663
   380
wenzelm@29269
   381
val cthm_ord' = prod_ord (prod_ord (list_ord TermOrd.term_ord) (list_ord TermOrd.sort_ord)) TermOrd.term_ord
obua@23663
   382
obua@23663
   383
fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
obua@23663
   384
wenzelm@31971
   385
structure CThmtab = Table(type key = cthm val ord = cthm_ord)
wenzelm@24271
   386
obua@23663
   387
fun remove_duplicates ths =
obua@23663
   388
    let
wenzelm@24271
   389
        val counter = ref 0
wenzelm@24271
   390
        val tab = ref (CThmtab.empty : unit CThmtab.table)
wenzelm@24271
   391
        val thstab = ref (Inttab.empty : thm Inttab.table)
wenzelm@24271
   392
        fun update th =
wenzelm@24271
   393
            let
wenzelm@24271
   394
                val key = thm2cthm th
wenzelm@24271
   395
            in
wenzelm@24271
   396
                case CThmtab.lookup (!tab) key of
wenzelm@24271
   397
                    NONE => ((tab := CThmtab.update_new (key, ()) (!tab)); thstab := Inttab.update_new (!counter, th) (!thstab); counter := !counter + 1)
wenzelm@24271
   398
                  | _ => ()
wenzelm@24271
   399
            end
wenzelm@24271
   400
        val _ = map update ths
obua@23663
   401
    in
wenzelm@24271
   402
        map snd (Inttab.dest (!thstab))
obua@23663
   403
    end
wenzelm@24271
   404
obua@25520
   405
fun make_with_cache machine thy pats ths cs =
obua@23663
   406
    let
obua@25218
   407
	val ths = remove_duplicates ths
obua@25218
   408
	val (monocs, ths) = fold_rev (fn th => 
obua@25218
   409
				      fn (monocs, ths) => 
obua@25218
   410
					 let val (m, t) = create_theorem th in 
obua@25218
   411
					     (m@monocs, t::ths)
obua@25218
   412
					 end)
obua@25218
   413
				     ths (cs, [])
obua@25520
   414
	val pats = map create_pattern pats
obua@25520
   415
	val (_, (pats, ths)) = add_monos thy monocs pats ths
obua@25520
   416
	val computer = create_computer machine thy pats ths
obua@23663
   417
    in
obua@25520
   418
	PComputer (Theory.check_thy thy, computer, ref ths, ref pats)
obua@23663
   419
    end
obua@23663
   420
obua@25520
   421
fun make machine thy ths cs = make_with_cache machine thy [] ths cs
obua@25520
   422
obua@25520
   423
fun add_instances (PComputer (thyref, computer, rths, rpats)) cs = 
obua@23663
   424
    let
wenzelm@24271
   425
        val thy = Theory.deref thyref
obua@25520
   426
        val (changed, (pats, ths)) = add_monos thy cs (!rpats) (!rths)
obua@23663
   427
    in
obua@25218
   428
	if changed then
obua@25520
   429
	    (update_computer computer pats ths;
obua@25218
   430
	     rths := ths;
obua@25520
   431
	     rpats := pats;
obua@25218
   432
	     true)
obua@25218
   433
	else
obua@25218
   434
	    false
obua@25218
   435
obua@25218
   436
    end
obua@25218
   437
obua@25218
   438
fun add_instances' pc ts = add_instances pc (Linker.collect_consts ts)
obua@25218
   439
obua@25218
   440
fun rewrite pc cts =
obua@25218
   441
    let
obua@25218
   442
	val _ = add_instances' pc (map term_of cts)
obua@25218
   443
	val computer = (computer_of pc)
obua@25218
   444
    in
obua@25218
   445
	map (fn ct => Compute.rewrite computer ct) cts
obua@23663
   446
    end
obua@23663
   447
obua@25218
   448
fun simplify pc th = Compute.simplify (computer_of pc) th
obua@25218
   449
obua@25218
   450
fun make_theorem pc th vars = 
obua@23663
   451
    let
obua@25218
   452
	val _ = add_instances' pc [prop_of th]
obua@25218
   453
obua@23663
   454
    in
obua@25218
   455
	Compute.make_theorem (computer_of pc) th vars
obua@23663
   456
    end
wenzelm@24271
   457
obua@25218
   458
fun instantiate pc insts th = 
obua@25218
   459
    let
obua@25218
   460
	val _ = add_instances' pc (map (term_of o snd) insts)
obua@25218
   461
    in
obua@25218
   462
	Compute.instantiate (computer_of pc) insts th
obua@25218
   463
    end
obua@25218
   464
obua@25218
   465
fun evaluate_prem pc prem_no th = Compute.evaluate_prem (computer_of pc) prem_no th
obua@25218
   466
obua@25218
   467
fun modus_ponens pc prem_no th' th =
obua@25218
   468
    let
obua@25218
   469
	val _ = add_instances' pc [prop_of th']
obua@25218
   470
    in
obua@25218
   471
	Compute.modus_ponens (computer_of pc) prem_no th' th
obua@25218
   472
    end    
obua@25218
   473
		 							      			    
obua@25218
   474
wenzelm@24137
   475
end