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