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