src/Tools/Compute_Oracle/compute.ML
author wenzelm
Sun, 08 Jul 2007 19:51:58 +0200
changeset 23655 d2d1138e0ddc
parent 23174 3913451b0418
child 23663 84b5c89b8b49
permissions -rw-r--r--
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23174
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
     1
(*  Title:      Tools/Compute_Oracle/compute.ML
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
     3
    Author:     Steven Obua
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
     4
*)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
     5
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
     6
signature COMPUTE = sig
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
     7
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
     8
    type computer
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
     9
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    10
    exception Make of string
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    11
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    12
    val basic_make : theory -> thm list -> computer
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    13
    val make : theory -> thm list -> computer
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    14
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    15
    val compute : computer -> (int -> string) -> cterm -> term
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    16
    val theory_of : computer -> theory
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    17
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    18
    val default_naming: int -> string
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    19
    val oracle_fn: theory -> computer * (int -> string) * cterm -> term
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    20
end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    21
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    22
structure Compute: COMPUTE = struct
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    23
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    24
exception Make of string;
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    25
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    26
fun is_mono_typ (Type (_, list)) = forall is_mono_typ list
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    27
  | is_mono_typ _ = false
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    28
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    29
fun is_mono_term (Const (_, t)) = is_mono_typ t
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    30
  | is_mono_term (Var (_, t)) = is_mono_typ t
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    31
  | is_mono_term (Free (_, t)) = is_mono_typ t
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    32
  | is_mono_term (Bound _) = true
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    33
  | is_mono_term (a $ b) = is_mono_term a andalso is_mono_term b
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    34
  | is_mono_term (Abs (_, ty, t)) = is_mono_typ ty andalso is_mono_term t
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    35
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    36
structure AMTermTab = TableFun (type key = AbstractMachine.term val ord = AM_Util.term_ord)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    37
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    38
fun add x y = x + y : int;
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    39
fun inc x = x + 1;
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    40
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    41
exception Mono of term;
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    42
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    43
val remove_types =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    44
    let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    45
        fun remove_types_var table invtable ccount vcount ldepth t =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    46
            (case Termtab.lookup table t of
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    47
                 NONE =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    48
                 let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    49
                     val a = AbstractMachine.Var vcount
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    50
                 in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    51
                     (Termtab.update (t, a) table,
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    52
                      AMTermTab.update (a, t) invtable,
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    53
                      ccount,
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    54
                      inc vcount,
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    55
                      AbstractMachine.Var (add vcount ldepth))
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    56
                 end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    57
               | SOME (AbstractMachine.Var v) =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    58
                 (table, invtable, ccount, vcount, AbstractMachine.Var (add v ldepth))
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    59
               | SOME _ => sys_error "remove_types_var: lookup should be a var")
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    60
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    61
        fun remove_types_const table invtable ccount vcount ldepth t =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    62
            (case Termtab.lookup table t of
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    63
                 NONE =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    64
                 let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    65
                     val a = AbstractMachine.Const ccount
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    66
                 in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    67
                     (Termtab.update (t, a) table,
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    68
                      AMTermTab.update (a, t) invtable,
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    69
                      inc ccount,
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    70
                      vcount,
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    71
                      a)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    72
                 end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    73
               | SOME (c as AbstractMachine.Const _) =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    74
                 (table, invtable, ccount, vcount, c)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    75
               | SOME _ => sys_error "remove_types_const: lookup should be a const")
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    76
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    77
        fun remove_types table invtable ccount vcount ldepth t =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    78
            case t of
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    79
                Var (_, ty) =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    80
                  if is_mono_typ ty then remove_types_var table invtable ccount vcount ldepth t
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    81
                  else raise (Mono t)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    82
              | Free (_, ty) =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    83
                  if is_mono_typ ty then remove_types_var table invtable ccount vcount ldepth t
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    84
                  else raise (Mono t)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    85
              | Const (_, ty) =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    86
                  if is_mono_typ ty then remove_types_const table invtable ccount vcount ldepth t
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    87
                  else raise (Mono t)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    88
              | Abs (_, ty, t') =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    89
                if is_mono_typ ty then
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    90
                    let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    91
                        val (table, invtable, ccount, vcount, t') =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    92
                            remove_types table invtable ccount vcount (inc ldepth) t'
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    93
                    in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    94
                        (table, invtable, ccount, vcount, AbstractMachine.Abs t')
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    95
                    end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    96
                else
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    97
                    raise (Mono t)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    98
              | a $ b =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
    99
                let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   100
                    val (table, invtable, ccount, vcount, a) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   101
                        remove_types table invtable ccount vcount ldepth a
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   102
                    val (table, invtable, ccount, vcount, b) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   103
                        remove_types table invtable ccount vcount ldepth b
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   104
                in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   105
                    (table, invtable, ccount, vcount, AbstractMachine.App (a,b))
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   106
                end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   107
              | Bound b => (table, invtable, ccount, vcount, AbstractMachine.Var b)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   108
    in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   109
     fn (table, invtable, ccount, vcount) => remove_types table invtable ccount vcount 0
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   110
    end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   111
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   112
fun infer_types naming =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   113
    let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   114
        fun infer_types invtable ldepth bounds ty (AbstractMachine.Var v) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   115
            if v < ldepth then (Bound v, List.nth (bounds, v)) else
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   116
            (case AMTermTab.lookup invtable (AbstractMachine.Var (v-ldepth)) of
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   117
                 SOME (t as Var (_, ty)) => (t, ty)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   118
               | SOME (t as Free (_, ty)) => (t, ty)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   119
               | _ => sys_error "infer_types: lookup should deliver Var or Free")
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   120
          | infer_types invtable ldepth _ ty (c as AbstractMachine.Const _) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   121
            (case AMTermTab.lookup invtable c of
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   122
                 SOME (c as Const (_, ty)) => (c, ty)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   123
               | _ => sys_error "infer_types: lookup should deliver Const")
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   124
          | infer_types invtable ldepth bounds (n,ty) (AbstractMachine.App (a, b)) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   125
            let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   126
                val (a, aty) = infer_types invtable ldepth bounds (n+1, ty) a
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   127
                val (adom, arange) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   128
                    case aty of
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   129
                        Type ("fun", [dom, range]) => (dom, range)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   130
                      | _ => sys_error "infer_types: function type expected"
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   131
                val (b, bty) = infer_types invtable ldepth bounds (0, adom) b
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   132
            in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   133
                (a $ b, arange)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   134
            end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   135
          | infer_types invtable ldepth bounds (0, ty as Type ("fun", [dom, range]))
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   136
              (AbstractMachine.Abs m) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   137
            let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   138
                val (m, _) = infer_types invtable (ldepth+1) (dom::bounds) (0, range) m
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   139
            in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   140
                (Abs (naming ldepth, dom, m), ty)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   141
            end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   142
          | infer_types invtable ldepth bounds ty (AbstractMachine.Abs m) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   143
            sys_error "infer_types: cannot infer type of abstraction"
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   144
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   145
        fun infer invtable ty term =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   146
            let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   147
                val (term', _) = infer_types invtable 0 [] (0, ty) term
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   148
            in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   149
                term'
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   150
            end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   151
    in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   152
        infer
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   153
    end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   154
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   155
datatype computer =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   156
  Computer of theory_ref *
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   157
    (AbstractMachine.term Termtab.table * term AMTermTab.table * int * AbstractMachine.program)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   158
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   159
fun basic_make thy raw_ths =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   160
    let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   161
        val ths = map (Thm.transfer thy) raw_ths;
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   162
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   163
        fun thm2rule table invtable ccount th =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   164
            let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   165
                val prop = Thm.plain_prop_of th
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   166
                  handle THM _ => raise (Make "theorems must be plain propositions")
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   167
                val (a, b) = Logic.dest_equals prop
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   168
                  handle TERM _ => raise (Make "theorems must be meta-level equations")
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   169
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   170
                val (table, invtable, ccount, vcount, prop) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   171
                    remove_types (table, invtable, ccount, 0) (a$b)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   172
                    handle Mono _ => raise (Make "no type variables allowed")
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   173
                val (left, right) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   174
                    (case prop of AbstractMachine.App x => x | _ =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   175
                      sys_error "make: remove_types should deliver application")
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   176
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   177
                fun make_pattern table invtable n vars (var as AbstractMachine.Var v) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   178
                    let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   179
                        val var' = the (AMTermTab.lookup invtable var)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   180
                        val table = Termtab.delete var' table
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   181
                        val invtable = AMTermTab.delete var invtable
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   182
                        val vars = Inttab.update_new (v, n) vars handle Inttab.DUP _ =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   183
                          raise (Make "no duplicate variable in pattern allowed")
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   184
                    in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   185
                        (table, invtable, n+1, vars, AbstractMachine.PVar)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   186
                    end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   187
                  | make_pattern table invtable n vars (AbstractMachine.Abs _) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   188
                      raise (Make "no lambda abstractions allowed in pattern")
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   189
                  | make_pattern table invtable n vars (AbstractMachine.Const c) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   190
                    (table, invtable, n, vars, AbstractMachine.PConst (c, []))
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   191
                  | make_pattern table invtable n vars (AbstractMachine.App (a, b)) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   192
                    let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   193
                        val (table, invtable, n, vars, pa) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   194
                            make_pattern table invtable n vars a
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   195
                        val (table, invtable, n, vars, pb) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   196
                            make_pattern table invtable n vars b
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   197
                    in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   198
                        case pa of
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   199
                            AbstractMachine.PVar =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   200
                              raise (Make "patterns may not start with a variable")
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   201
                          | AbstractMachine.PConst (c, args) =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   202
                              (table, invtable, n, vars, AbstractMachine.PConst (c, args@[pb]))
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   203
                    end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   204
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   205
                val (table, invtable, vcount, vars, pattern) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   206
                    make_pattern table invtable 0 Inttab.empty left
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   207
                val _ = (case pattern of
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   208
                           AbstractMachine.PVar =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   209
                             raise (Make "patterns may not start with a variable")
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   210
                         | _ => ())
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   211
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   212
                (* at this point, there shouldn't be any variables
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   213
                  left in table or invtable, only constants *)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   214
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   215
                (* finally, provide a function for renaming the
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   216
                  pattern bound variables on the right hand side *)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   217
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   218
                fun rename ldepth vars (var as AbstractMachine.Var v) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   219
                    if v < ldepth then var
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   220
                    else (case Inttab.lookup vars (v - ldepth) of
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   221
                              NONE => raise (Make "new variable on right hand side")
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   222
                            | SOME n => AbstractMachine.Var ((vcount-n-1)+ldepth))
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   223
                  | rename ldepth vars (c as AbstractMachine.Const _) = c
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   224
                  | rename ldepth vars (AbstractMachine.App (a, b)) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   225
                    AbstractMachine.App (rename ldepth vars a, rename ldepth vars b)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   226
                  | rename ldepth vars (AbstractMachine.Abs m) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   227
                    AbstractMachine.Abs (rename (ldepth+1) vars m)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   228
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   229
            in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   230
                (table, invtable, ccount, (pattern, rename 0 vars right))
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   231
            end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   232
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   233
        val (table, invtable, ccount, rules) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   234
          fold_rev (fn th => fn (table, invtable, ccount, rules) =>
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   235
            let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   236
              val (table, invtable, ccount, rule) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   237
                  thm2rule table invtable ccount th
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   238
            in (table, invtable, ccount, rule::rules) end)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   239
          ths (Termtab.empty, AMTermTab.empty, 0, [])
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   240
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   241
        val prog = AbstractMachine.compile rules
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   242
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   243
    in Computer (Theory.self_ref thy, (table, invtable, ccount, prog)) end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   244
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   245
fun make thy ths =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   246
    let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   247
      val (_, {mk_rews={mk=mk,mk_eq_True=emk, ...},...}) = rep_ss (simpset_of thy)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   248
      fun mk_eq_True th = (case emk th of NONE => [th] | SOME th' => [th, th'])
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   249
    in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   250
      basic_make thy (maps mk (maps mk_eq_True ths))
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   251
    end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   252
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   253
fun compute (Computer r) naming ct =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   254
    let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   255
        val {t=t, T=ty, thy=ctthy, ...} = rep_cterm ct
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   256
        val (rthy, (table, invtable, ccount, prog)) = r
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   257
        val thy = Theory.merge (Theory.deref rthy, ctthy)
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   258
        val (table, invtable, ccount, vcount, t) = remove_types (table, invtable, ccount, 0) t
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   259
        val t = AbstractMachine.run prog t
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   260
        val t = infer_types naming invtable ty t
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   261
    in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   262
        t
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   263
    end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   264
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   265
fun theory_of (Computer (rthy, _)) = Theory.deref rthy
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   266
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   267
fun default_naming i = "v_" ^ Int.toString i
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   268
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   269
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   270
fun oracle_fn thy (r, naming, ct) =
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   271
    let
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   272
        val _ = Theory.assert_super (theory_of r) thy
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   273
        val t' = compute r naming ct
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   274
    in
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   275
        Logic.mk_equals (term_of ct, t')
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   276
    end
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   277
3913451b0418 moved Compute_Oracle from Pure/Tools to Tools;
wenzelm
parents:
diff changeset
   278
end