src/Tools/Compute_Oracle/compute.ML
author wenzelm
Thu Mar 05 19:48:02 2009 +0100 (2009-03-05)
changeset 30288 a32700e45ab3
parent 29269 5c25a2012975
child 31322 526e149999cc
permissions -rw-r--r--
Thm.add_oracle interface: replaced old bstring by binding;
     1 (*  Title:      Tools/Compute_Oracle/compute.ML
     2     Author:     Steven Obua
     3 *)
     4 
     5 signature COMPUTE = sig
     6 
     7     type computer
     8     type theorem
     9     type naming = int -> string
    10 
    11     datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML
    12 
    13     (* Functions designated with a ! in front of them actually update the computer parameter *)
    14 
    15     exception Make of string
    16     val make : machine -> theory -> thm list -> computer
    17     val make_with_cache : machine -> theory -> term list -> thm list -> computer
    18     val theory_of : computer -> theory
    19     val hyps_of : computer -> term list
    20     val shyps_of : computer -> sort list
    21     (* ! *) val update : computer -> thm list -> unit
    22     (* ! *) val update_with_cache : computer -> term list -> thm list -> unit
    23     (* ! *) val discard : computer -> unit
    24     
    25     (* ! *) val set_naming : computer -> naming -> unit
    26     val naming_of : computer -> naming
    27     
    28     exception Compute of string    
    29     val simplify : computer -> theorem -> thm 
    30     val rewrite : computer -> cterm -> thm 
    31 
    32     val make_theorem : computer -> thm -> string list -> theorem
    33     (* ! *) val instantiate : computer -> (string * cterm) list -> theorem -> theorem
    34     (* ! *) val evaluate_prem : computer -> int -> theorem -> theorem
    35     (* ! *) val modus_ponens : computer -> int -> thm -> theorem -> theorem
    36 
    37 end
    38 
    39 structure Compute :> COMPUTE = struct
    40 
    41 open Report;
    42 
    43 datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML      
    44 
    45 (* Terms are mapped to integer codes *)
    46 structure Encode :> 
    47 sig
    48     type encoding
    49     val empty : encoding
    50     val insert : term -> encoding -> int * encoding
    51     val lookup_code : term -> encoding -> int option
    52     val lookup_term : int -> encoding -> term option                                    
    53     val remove_code : int -> encoding -> encoding
    54     val remove_term : term -> encoding -> encoding
    55     val fold : ((term * int) -> 'a -> 'a) -> encoding -> 'a -> 'a                                                      
    56 end 
    57 = 
    58 struct
    59 
    60 type encoding = int * (int Termtab.table) * (term Inttab.table)
    61 
    62 val empty = (0, Termtab.empty, Inttab.empty)
    63 
    64 fun insert t (e as (count, term2int, int2term)) = 
    65     (case Termtab.lookup term2int t of
    66          NONE => (count, (count+1, Termtab.update_new (t, count) term2int, Inttab.update_new (count, t) int2term))
    67        | SOME code => (code, e))
    68 
    69 fun lookup_code t (_, term2int, _) = Termtab.lookup term2int t
    70 
    71 fun lookup_term c (_, _, int2term) = Inttab.lookup int2term c
    72 
    73 fun remove_code c (e as (count, term2int, int2term)) = 
    74     (case lookup_term c e of NONE => e | SOME t => (count, Termtab.delete t term2int, Inttab.delete c int2term))
    75 
    76 fun remove_term t (e as (count, term2int, int2term)) = 
    77     (case lookup_code t e of NONE => e | SOME c => (count, Termtab.delete t term2int, Inttab.delete c int2term))
    78 
    79 fun fold f (_, term2int, _) = Termtab.fold f term2int
    80 
    81 end
    82 
    83 exception Make of string;
    84 exception Compute of string;
    85 
    86 local
    87     fun make_constant t ty encoding = 
    88         let 
    89             val (code, encoding) = Encode.insert t encoding 
    90         in 
    91             (encoding, AbstractMachine.Const code)
    92         end
    93 in
    94 
    95 fun remove_types encoding t =
    96     case t of 
    97         Var (_, ty) => make_constant t ty encoding
    98       | Free (_, ty) => make_constant t ty encoding
    99       | Const (_, ty) => make_constant t ty encoding
   100       | Abs (_, ty, t') => 
   101         let val (encoding, t'') = remove_types encoding t' in
   102             (encoding, AbstractMachine.Abs t'')
   103         end
   104       | a $ b => 
   105         let
   106             val (encoding, a) = remove_types encoding a
   107             val (encoding, b) = remove_types encoding b
   108         in
   109             (encoding, AbstractMachine.App (a,b))
   110         end
   111       | Bound b => (encoding, AbstractMachine.Var b)
   112 end
   113     
   114 local
   115     fun type_of (Free (_, ty)) = ty
   116       | type_of (Const (_, ty)) = ty
   117       | type_of (Var (_, ty)) = ty
   118       | type_of _ = sys_error "infer_types: type_of error"
   119 in
   120 fun infer_types naming encoding =
   121     let
   122         fun infer_types _ bounds _ (AbstractMachine.Var v) = (Bound v, List.nth (bounds, v))
   123           | infer_types _ bounds _ (AbstractMachine.Const code) = 
   124             let
   125                 val c = the (Encode.lookup_term code encoding)
   126             in
   127                 (c, type_of c)
   128             end
   129           | infer_types level bounds _ (AbstractMachine.App (a, b)) = 
   130             let
   131                 val (a, aty) = infer_types level bounds NONE a
   132                 val (adom, arange) =
   133                     case aty of
   134                         Type ("fun", [dom, range]) => (dom, range)
   135                       | _ => sys_error "infer_types: function type expected"
   136                 val (b, bty) = infer_types level bounds (SOME adom) b
   137             in
   138                 (a $ b, arange)
   139             end
   140           | infer_types level bounds (SOME (ty as Type ("fun", [dom, range]))) (AbstractMachine.Abs m) =
   141             let
   142                 val (m, _) = infer_types (level+1) (dom::bounds) (SOME range) m
   143             in
   144                 (Abs (naming level, dom, m), ty)
   145             end
   146           | infer_types _ _ NONE (AbstractMachine.Abs m) = sys_error "infer_types: cannot infer type of abstraction"
   147 
   148         fun infer ty term =
   149             let
   150                 val (term', _) = infer_types 0 [] (SOME ty) term
   151             in
   152                 term'
   153             end
   154     in
   155         infer
   156     end
   157 end
   158 
   159 datatype prog = 
   160          ProgBarras of AM_Interpreter.program 
   161        | ProgBarrasC of AM_Compiler.program
   162        | ProgHaskell of AM_GHC.program
   163        | ProgSML of AM_SML.program
   164 
   165 fun machine_of_prog (ProgBarras _) = BARRAS
   166   | machine_of_prog (ProgBarrasC _) = BARRAS_COMPILED
   167   | machine_of_prog (ProgHaskell _) = HASKELL
   168   | machine_of_prog (ProgSML _) = SML
   169 
   170 structure Sorttab = TableFun(type key = sort val ord = TermOrd.sort_ord)
   171 
   172 type naming = int -> string
   173 
   174 fun default_naming i = "v_" ^ Int.toString i
   175 
   176 datatype computer = Computer of (theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit ref * naming) 
   177                     option ref
   178 
   179 fun theory_of (Computer (ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy
   180 fun hyps_of (Computer (ref (SOME (_,_,hyps,_,_,_,_)))) = hyps
   181 fun shyps_of (Computer (ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable)
   182 fun shyptab_of (Computer (ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable
   183 fun stamp_of (Computer (ref (SOME (_,_,_,_,_,stamp,_)))) = stamp
   184 fun prog_of (Computer (ref (SOME (_,_,_,_,prog,_,_)))) = prog
   185 fun encoding_of (Computer (ref (SOME (_,encoding,_,_,_,_,_)))) = encoding
   186 fun set_encoding (Computer (r as ref (SOME (p1,encoding,p2,p3,p4,p5,p6)))) encoding' = 
   187     (r := SOME (p1,encoding',p2,p3,p4,p5,p6))
   188 fun naming_of (Computer (ref (SOME (_,_,_,_,_,_,n)))) = n
   189 fun set_naming (Computer (r as ref (SOME (p1,p2,p3,p4,p5,p6,naming)))) naming'= 
   190     (r := SOME (p1,p2,p3,p4,p5,p6,naming'))
   191 
   192 fun ref_of (Computer r) = r
   193 
   194 datatype cthm = ComputeThm of term list * sort list * term
   195 
   196 fun thm2cthm th = 
   197     let
   198         val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th
   199         val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else ()
   200     in
   201         ComputeThm (hyps, shyps, prop)
   202     end
   203 
   204 fun make_internal machine thy stamp encoding cache_pattern_terms raw_ths =
   205     let
   206         fun transfer (x:thm) = Thm.transfer thy x
   207         val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths
   208 
   209         fun make_pattern encoding n vars (var as AbstractMachine.Abs _) =
   210             raise (Make "no lambda abstractions allowed in pattern")
   211           | make_pattern encoding n vars (var as AbstractMachine.Var _) =
   212             raise (Make "no bound variables allowed in pattern")
   213           | make_pattern encoding n vars (AbstractMachine.Const code) =
   214             (case the (Encode.lookup_term code encoding) of
   215                  Var _ => ((n+1, Inttab.update_new (code, n) vars, AbstractMachine.PVar)
   216                            handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed"))
   217                | _ => (n, vars, AbstractMachine.PConst (code, [])))
   218           | make_pattern encoding n vars (AbstractMachine.App (a, b)) =
   219             let
   220                 val (n, vars, pa) = make_pattern encoding n vars a
   221                 val (n, vars, pb) = make_pattern encoding n vars b
   222             in
   223                 case pa of
   224                     AbstractMachine.PVar =>
   225                     raise (Make "patterns may not start with a variable")
   226                   | AbstractMachine.PConst (c, args) =>
   227                     (n, vars, AbstractMachine.PConst (c, args@[pb]))
   228             end
   229 
   230         fun thm2rule (encoding, hyptable, shyptable) th =
   231             let
   232                 val (ComputeThm (hyps, shyps, prop)) = th
   233                 val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable
   234                 val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable
   235                 val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop)
   236                 val (a, b) = Logic.dest_equals prop
   237                   handle TERM _ => raise (Make "theorems must be meta-level equations (with optional guards)")
   238                 val a = Envir.eta_contract a
   239                 val b = Envir.eta_contract b
   240                 val prems = map Envir.eta_contract prems
   241 
   242                 val (encoding, left) = remove_types encoding a     
   243                 val (encoding, right) = remove_types encoding b  
   244                 fun remove_types_of_guard encoding g = 
   245                     (let
   246                          val (t1, t2) = Logic.dest_equals g 
   247                          val (encoding, t1) = remove_types encoding t1
   248                          val (encoding, t2) = remove_types encoding t2
   249                      in
   250                          (encoding, AbstractMachine.Guard (t1, t2))
   251                      end handle TERM _ => raise (Make "guards must be meta-level equations"))
   252                 val (encoding, prems) = fold_rev (fn p => fn (encoding, ps) => let val (e, p) = remove_types_of_guard encoding p in (e, p::ps) end) prems (encoding, [])
   253 
   254                 (* Principally, a check should be made here to see if the (meta-) hyps contain any of the variables of the rule.
   255                    As it is, all variables of the rule are schematic, and there are no schematic variables in meta-hyps, therefore
   256                    this check can be left out. *)
   257 
   258                 val (vcount, vars, pattern) = make_pattern encoding 0 Inttab.empty left
   259                 val _ = (case pattern of
   260                              AbstractMachine.PVar =>
   261                              raise (Make "patterns may not start with a variable")
   262                          (*  | AbstractMachine.PConst (_, []) => 
   263                              (print th; raise (Make "no parameter rewrite found"))*)
   264                            | _ => ())
   265 
   266                 (* finally, provide a function for renaming the
   267                    pattern bound variables on the right hand side *)
   268 
   269                 fun rename level vars (var as AbstractMachine.Var _) = var
   270                   | rename level vars (c as AbstractMachine.Const code) =
   271                     (case Inttab.lookup vars code of 
   272                          NONE => c 
   273                        | SOME n => AbstractMachine.Var (vcount-n-1+level))
   274                   | rename level vars (AbstractMachine.App (a, b)) =
   275                     AbstractMachine.App (rename level vars a, rename level vars b)
   276                   | rename level vars (AbstractMachine.Abs m) =
   277                     AbstractMachine.Abs (rename (level+1) vars m)
   278                     
   279                 fun rename_guard (AbstractMachine.Guard (a,b)) = 
   280                     AbstractMachine.Guard (rename 0 vars a, rename 0 vars b)
   281             in
   282                 ((encoding, hyptable, shyptable), (map rename_guard prems, pattern, rename 0 vars right))
   283             end
   284 
   285         val ((encoding, hyptable, shyptable), rules) =
   286           fold_rev (fn th => fn (encoding_hyptable, rules) =>
   287             let
   288               val (encoding_hyptable, rule) = thm2rule encoding_hyptable th
   289             in (encoding_hyptable, rule::rules) end)
   290           ths ((encoding, Termtab.empty, Sorttab.empty), [])
   291 
   292         fun make_cache_pattern t (encoding, cache_patterns) =
   293             let
   294                 val (encoding, a) = remove_types encoding t
   295                 val (_,_,p) = make_pattern encoding 0 Inttab.empty a
   296             in
   297                 (encoding, p::cache_patterns)
   298             end
   299         
   300         val (encoding, cache_patterns) = fold_rev make_cache_pattern cache_pattern_terms (encoding, [])
   301 
   302         fun arity (Type ("fun", [a,b])) = 1 + arity b
   303           | arity _ = 0
   304 
   305         fun make_arity (Const (s, _), i) tab = 
   306             (Inttab.update (i, arity (Sign.the_const_type thy s)) tab handle TYPE _ => tab)
   307           | make_arity _ tab = tab
   308 
   309         val const_arity_tab = Encode.fold make_arity encoding Inttab.empty
   310         fun const_arity x = Inttab.lookup const_arity_tab x 
   311 
   312         val prog = 
   313             case machine of 
   314                 BARRAS => ProgBarras (AM_Interpreter.compile cache_patterns const_arity rules)
   315               | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile cache_patterns const_arity rules)
   316               | HASKELL => ProgHaskell (AM_GHC.compile cache_patterns const_arity rules)
   317               | SML => ProgSML (AM_SML.compile cache_patterns const_arity rules)
   318 
   319         fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
   320 
   321         val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable
   322 
   323     in (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end
   324 
   325 fun make_with_cache machine thy cache_patterns raw_thms = Computer (ref (SOME (make_internal machine thy (ref ()) Encode.empty cache_patterns raw_thms)))
   326 
   327 fun make machine thy raw_thms = make_with_cache machine thy [] raw_thms
   328 
   329 fun update_with_cache computer cache_patterns raw_thms =
   330     let 
   331         val c = make_internal (machine_of_prog (prog_of computer)) (theory_of computer) (stamp_of computer) 
   332                               (encoding_of computer) cache_patterns raw_thms
   333         val _ = (ref_of computer) := SOME c     
   334     in
   335         ()
   336     end
   337 
   338 fun update computer raw_thms = update_with_cache computer [] raw_thms
   339 
   340 fun discard computer =
   341     let
   342         val _ = 
   343             case prog_of computer of
   344                 ProgBarras p => AM_Interpreter.discard p
   345               | ProgBarrasC p => AM_Compiler.discard p
   346               | ProgHaskell p => AM_GHC.discard p
   347               | ProgSML p => AM_SML.discard p
   348         val _ = (ref_of computer) := NONE
   349     in
   350         ()
   351     end 
   352                                               
   353 fun runprog (ProgBarras p) = AM_Interpreter.run p
   354   | runprog (ProgBarrasC p) = AM_Compiler.run p
   355   | runprog (ProgHaskell p) = AM_GHC.run p
   356   | runprog (ProgSML p) = AM_SML.run p    
   357 
   358 (* ------------------------------------------------------------------------------------- *)
   359 (* An oracle for exporting theorems; must only be accessible from inside this structure! *)
   360 (* ------------------------------------------------------------------------------------- *)
   361 
   362 fun merge_hyps hyps1 hyps2 = 
   363 let
   364     fun add hyps tab = fold (fn h => fn tab => Termtab.update (h, ()) tab) hyps tab
   365 in
   366     Termtab.keys (add hyps2 (add hyps1 Termtab.empty))
   367 end
   368 
   369 fun add_shyps shyps tab = fold (fn h => fn tab => Sorttab.update (h, ()) tab) shyps tab
   370 
   371 fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
   372 
   373 val (_, export_oracle) = Context.>>> (Context.map_theory_result
   374   (Thm.add_oracle (Binding.name "compute", fn (thy, hyps, shyps, prop) =>
   375     let
   376         val shyptab = add_shyps shyps Sorttab.empty
   377         fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
   378         fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab
   379         fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
   380         val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab
   381         val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab)
   382         val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else ()
   383     in
   384         Thm.cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop)
   385     end)));
   386 
   387 fun export_thm thy hyps shyps prop =
   388     let
   389         val th = export_oracle (thy, hyps, shyps, prop)
   390         val hyps = map (fn h => assume (cterm_of thy h)) hyps
   391     in
   392         fold (fn h => fn p => implies_elim p h) hyps th 
   393     end
   394         
   395 (* --------- Rewrite ----------- *)
   396 
   397 fun rewrite computer ct =
   398     let
   399         val thy = Thm.theory_of_cterm ct
   400         val {t=t',T=ty,...} = rep_cterm ct
   401         val _ = Theory.assert_super (theory_of computer) thy
   402         val naming = naming_of computer
   403         val (encoding, t) = remove_types (encoding_of computer) t'
   404         (*val _ = if (!print_encoding) then writeln (makestring ("encoding: ",Encode.fold (fn x => fn s => x::s) encoding [])) else ()*)
   405         val t = runprog (prog_of computer) t
   406         val t = infer_types naming encoding ty t
   407         val eq = Logic.mk_equals (t', t)
   408     in
   409         export_thm thy (hyps_of computer) (Sorttab.keys (shyptab_of computer)) eq
   410     end
   411 
   412 (* --------- Simplify ------------ *)
   413 
   414 datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int 
   415               | Prem of AbstractMachine.term
   416 datatype theorem = Theorem of theory_ref * unit ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table  
   417                * prem list * AbstractMachine.term * term list * sort list
   418 
   419 
   420 exception ParamSimplify of computer * theorem
   421 
   422 fun make_theorem computer th vars =
   423 let
   424     val _ = Theory.assert_super (theory_of computer) (theory_of_thm th)
   425 
   426     val (ComputeThm (hyps, shyps, prop)) = thm2cthm th 
   427 
   428     val encoding = encoding_of computer
   429  
   430     (* variables in the theorem are identified upfront *)
   431     fun collect_vars (Abs (_, _, t)) tab = collect_vars t tab
   432       | collect_vars (a $ b) tab = collect_vars b (collect_vars a tab)
   433       | collect_vars (Const _) tab = tab
   434       | collect_vars (Free _) tab = tab
   435       | collect_vars (Var ((s, i), ty)) tab = 
   436             if List.find (fn x => x=s) vars = NONE then 
   437                 tab
   438             else                
   439                 (case Symtab.lookup tab s of
   440                      SOME ((s',i'),ty') => 
   441                      if s' <> s orelse i' <> i orelse ty <> ty' then 
   442                          raise Compute ("make_theorem: variable name '"^s^"' is not unique")
   443                      else 
   444                          tab
   445                    | NONE => Symtab.update (s, ((s, i), ty)) tab)
   446     val vartab = collect_vars prop Symtab.empty 
   447     fun encodevar (s, t as (_, ty)) (encoding, tab) = 
   448         let
   449             val (x, encoding) = Encode.insert (Var t) encoding
   450         in
   451             (encoding, Symtab.update (s, (x, ty)) tab)
   452         end
   453     val (encoding, vartab) = Symtab.fold encodevar vartab (encoding, Symtab.empty)                                                     
   454     val varsubst = Inttab.make (map (fn (s, (x, _)) => (x, NONE)) (Symtab.dest vartab))
   455 
   456     (* make the premises and the conclusion *)
   457     fun mk_prem encoding t = 
   458         (let
   459              val (a, b) = Logic.dest_equals t
   460              val ty = type_of a
   461              val (encoding, a) = remove_types encoding a
   462              val (encoding, b) = remove_types encoding b
   463              val (eq, encoding) = Encode.insert (Const ("==", ty --> ty --> @{typ "prop"})) encoding 
   464          in
   465              (encoding, EqPrem (a, b, ty, eq))
   466          end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end)
   467     val (encoding, prems) = 
   468         (fold_rev (fn t => fn (encoding, l) => 
   469             case mk_prem encoding t  of 
   470                 (encoding, t) => (encoding, t::l)) (Logic.strip_imp_prems prop) (encoding, []))
   471     val (encoding, concl) = remove_types encoding (Logic.strip_imp_concl prop)
   472     val _ = set_encoding computer encoding
   473 in
   474     Theorem (Theory.check_thy (theory_of_thm th), stamp_of computer, vartab, varsubst, 
   475              prems, concl, hyps, shyps)
   476 end
   477     
   478 fun theory_of_theorem (Theorem (rthy,_,_,_,_,_,_,_)) = Theory.deref rthy
   479 fun update_theory thy (Theorem (_,p0,p1,p2,p3,p4,p5,p6)) =
   480     Theorem (Theory.check_thy thy,p0,p1,p2,p3,p4,p5,p6)
   481 fun stamp_of_theorem (Theorem (_,s, _, _, _, _, _, _)) = s     
   482 fun vartab_of_theorem (Theorem (_,_,vt,_,_,_,_,_)) = vt
   483 fun varsubst_of_theorem (Theorem (_,_,_,vs,_,_,_,_)) = vs 
   484 fun update_varsubst vs (Theorem (p0,p1,p2,_,p3,p4,p5,p6)) = Theorem (p0,p1,p2,vs,p3,p4,p5,p6)
   485 fun prems_of_theorem (Theorem (_,_,_,_,prems,_,_,_)) = prems
   486 fun update_prems prems (Theorem (p0,p1,p2,p3,_,p4,p5,p6)) = Theorem (p0,p1,p2,p3,prems,p4,p5,p6)
   487 fun concl_of_theorem (Theorem (_,_,_,_,_,concl,_,_)) = concl
   488 fun hyps_of_theorem (Theorem (_,_,_,_,_,_,hyps,_)) = hyps
   489 fun update_hyps hyps (Theorem (p0,p1,p2,p3,p4,p5,_,p6)) = Theorem (p0,p1,p2,p3,p4,p5,hyps,p6)
   490 fun shyps_of_theorem (Theorem (_,_,_,_,_,_,_,shyps)) = shyps
   491 fun update_shyps shyps (Theorem (p0,p1,p2,p3,p4,p5,p6,_)) = Theorem (p0,p1,p2,p3,p4,p5,p6,shyps)
   492 
   493 fun check_compatible computer th s = 
   494     if stamp_of computer <> stamp_of_theorem th then
   495         raise Compute (s^": computer and theorem are incompatible")
   496     else ()
   497 
   498 fun instantiate computer insts th =
   499 let
   500     val _ = check_compatible computer th
   501 
   502     val thy = theory_of computer
   503 
   504     val vartab = vartab_of_theorem th
   505 
   506     fun rewrite computer t =
   507     let  
   508         val naming = naming_of computer
   509         val (encoding, t) = remove_types (encoding_of computer) t
   510         val t = runprog (prog_of computer) t
   511         val _ = set_encoding computer encoding
   512     in
   513         t
   514     end
   515 
   516     fun assert_varfree vs t = 
   517         if AbstractMachine.forall_consts (fn x => Inttab.lookup vs x = NONE) t then
   518             ()
   519         else
   520             raise Compute "instantiate: assert_varfree failed"
   521 
   522     fun assert_closed t =
   523         if AbstractMachine.closed t then
   524             ()
   525         else 
   526             raise Compute "instantiate: not a closed term"
   527 
   528     fun compute_inst (s, ct) vs =
   529         let
   530             val _ = Theory.assert_super (theory_of_cterm ct) thy
   531             val ty = typ_of (ctyp_of_term ct) 
   532         in          
   533             (case Symtab.lookup vartab s of 
   534                  NONE => raise Compute ("instantiate: variable '"^s^"' not found in theorem")
   535                | SOME (x, ty') => 
   536                  (case Inttab.lookup vs x of 
   537                       SOME (SOME _) => raise Compute ("instantiate: variable '"^s^"' has already been instantiated")
   538                     | SOME NONE => 
   539                       if ty <> ty' then 
   540                           raise Compute ("instantiate: wrong type for variable '"^s^"'")
   541                       else
   542                           let
   543                               val t = rewrite computer (term_of ct)
   544                               val _ = assert_varfree vs t 
   545                               val _ = assert_closed t
   546                           in
   547                               Inttab.update (x, SOME t) vs
   548                           end
   549                     | NONE => raise Compute "instantiate: internal error"))
   550         end
   551 
   552     val vs = fold compute_inst insts (varsubst_of_theorem th)
   553 in
   554     update_varsubst vs th
   555 end
   556 
   557 fun match_aterms subst =
   558     let 
   559         exception no_match
   560         open AbstractMachine
   561         fun match subst (b as (Const c)) a = 
   562             if a = b then subst
   563             else 
   564                 (case Inttab.lookup subst c of 
   565                      SOME (SOME a') => if a=a' then subst else raise no_match
   566                    | SOME NONE => if AbstractMachine.closed a then 
   567                                       Inttab.update (c, SOME a) subst 
   568                                   else raise no_match
   569                    | NONE => raise no_match)
   570           | match subst (b as (Var _)) a = if a=b then subst else raise no_match
   571           | match subst (App (u, v)) (App (u', v')) = match (match subst u u') v v'
   572           | match subst (Abs u) (Abs u') = match subst u u'
   573           | match subst _ _ = raise no_match
   574     in
   575         fn b => fn a => (SOME (match subst b a) handle no_match => NONE)
   576     end
   577 
   578 fun apply_subst vars_allowed subst =
   579     let
   580         open AbstractMachine
   581         fun app (t as (Const c)) = 
   582             (case Inttab.lookup subst c of 
   583                  NONE => t 
   584                | SOME (SOME t) => Computed t
   585                | SOME NONE => if vars_allowed then t else raise Compute "apply_subst: no vars allowed")
   586           | app (t as (Var _)) = t
   587           | app (App (u, v)) = App (app u, app v)
   588           | app (Abs m) = Abs (app m)
   589     in
   590         app
   591     end
   592 
   593 fun splicein n l L = List.take (L, n) @ l @ List.drop (L, n+1)
   594 
   595 fun evaluate_prem computer prem_no th =
   596 let
   597     val _ = check_compatible computer th
   598     val prems = prems_of_theorem th
   599     val varsubst = varsubst_of_theorem th
   600     fun run vars_allowed t = 
   601         runprog (prog_of computer) (apply_subst vars_allowed varsubst t)
   602 in
   603     case List.nth (prems, prem_no) of
   604         Prem _ => raise Compute "evaluate_prem: no equality premise"
   605       | EqPrem (a, b, ty, _) =>         
   606         let
   607             val a' = run false a
   608             val b' = run true b
   609         in
   610             case match_aterms varsubst b' a' of
   611                 NONE => 
   612                 let
   613                     fun mk s = makestring (infer_types (naming_of computer) (encoding_of computer) ty s)
   614                     val left = "computed left side: "^(mk a')
   615                     val right = "computed right side: "^(mk b')
   616                 in
   617                     raise Compute ("evaluate_prem: cannot assign computed left to right hand side\n"^left^"\n"^right^"\n")
   618                 end
   619               | SOME varsubst => 
   620                 update_prems (splicein prem_no [] prems) (update_varsubst varsubst th)
   621         end
   622 end
   623 
   624 fun prem2term (Prem t) = t
   625   | prem2term (EqPrem (a,b,_,eq)) = 
   626     AbstractMachine.App (AbstractMachine.App (AbstractMachine.Const eq, a), b)
   627 
   628 fun modus_ponens computer prem_no th' th = 
   629 let
   630     val _ = check_compatible computer th
   631     val thy = 
   632         let
   633             val thy1 = theory_of_theorem th
   634             val thy2 = theory_of_thm th'
   635         in
   636             if Theory.subthy (thy1, thy2) then thy2 
   637             else if Theory.subthy (thy2, thy1) then thy1 else
   638             raise Compute "modus_ponens: theorems are not compatible with each other"
   639         end 
   640     val th' = make_theorem computer th' []
   641     val varsubst = varsubst_of_theorem th
   642     fun run vars_allowed t =
   643         runprog (prog_of computer) (apply_subst vars_allowed varsubst t)
   644     val prems = prems_of_theorem th
   645     val prem = run true (prem2term (List.nth (prems, prem_no)))
   646     val concl = run false (concl_of_theorem th')    
   647 in
   648     case match_aterms varsubst prem concl of
   649         NONE => raise Compute "modus_ponens: conclusion does not match premise"
   650       | SOME varsubst =>
   651         let
   652             val th = update_varsubst varsubst th
   653             val th = update_prems (splicein prem_no (prems_of_theorem th') prems) th
   654             val th = update_hyps (merge_hyps (hyps_of_theorem th) (hyps_of_theorem th')) th
   655             val th = update_shyps (merge_shyps (shyps_of_theorem th) (shyps_of_theorem th')) th
   656         in
   657             update_theory thy th
   658         end
   659 end
   660                      
   661 fun simplify computer th =
   662 let
   663     val _ = check_compatible computer th
   664     val varsubst = varsubst_of_theorem th
   665     val encoding = encoding_of computer
   666     val naming = naming_of computer
   667     fun infer t = infer_types naming encoding @{typ "prop"} t
   668     fun run t = infer (runprog (prog_of computer) (apply_subst true varsubst t))
   669     fun runprem p = run (prem2term p)
   670     val prop = Logic.list_implies (map runprem (prems_of_theorem th), run (concl_of_theorem th))
   671     val hyps = merge_hyps (hyps_of computer) (hyps_of_theorem th)
   672     val shyps = merge_shyps (shyps_of_theorem th) (Sorttab.keys (shyptab_of computer))
   673 in
   674     export_thm (theory_of_theorem th) hyps shyps prop
   675 end
   676 
   677 end
   678