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