# HG changeset patch # User obua # Date 1193503052 -7200 # Node ID 3224db6415aeed4fa342f214fa50a2e06a626564 # Parent eb512c1717ea577a594dcbacfea575ec81d759bb better compute oracle diff -r eb512c1717ea -r 3224db6415ae src/Tools/Compute_Oracle/Compute_Oracle.thy --- a/src/Tools/Compute_Oracle/Compute_Oracle.thy Sat Oct 27 18:37:06 2007 +0200 +++ b/src/Tools/Compute_Oracle/Compute_Oracle.thy Sat Oct 27 18:37:32 2007 +0200 @@ -6,9 +6,9 @@ *) theory Compute_Oracle imports CPure -uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "compute.ML" "linker.ML" +uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML" begin -setup {* Compute.setup; *} +setup {* Compute.setup_compute; *} end \ No newline at end of file diff -r eb512c1717ea -r 3224db6415ae src/Tools/Compute_Oracle/am.ML --- a/src/Tools/Compute_Oracle/am.ML Sat Oct 27 18:37:06 2007 +0200 +++ b/src/Tools/Compute_Oracle/am.ML Sat Oct 27 18:37:32 2007 +0200 @@ -1,7 +1,7 @@ signature ABSTRACT_MACHINE = sig -datatype term = Var of int | Const of int | App of term * term | Abs of term +datatype term = Var of int | Const of int | App of term * term | Abs of term | Computed of term datatype pattern = PVar | PConst of int * (pattern list) @@ -20,12 +20,19 @@ exception Run of string; val run : program -> term -> term +(* Utilities *) + +val check_freevars : int -> term -> bool +val forall_consts : (int -> bool) -> term -> bool +val closed : term -> bool +val erase_Computed : term -> term + end structure AbstractMachine : ABSTRACT_MACHINE = struct -datatype term = Var of int | Const of int | App of term * term | Abs of term +datatype term = Var of int | Const of int | App of term * term | Abs of term | Computed of term datatype pattern = PVar | PConst of int * (pattern list) @@ -35,6 +42,28 @@ exception Compile of string; +fun erase_Computed (Computed t) = erase_Computed t + | erase_Computed (App (t1, t2)) = App (erase_Computed t1, erase_Computed t2) + | erase_Computed (Abs t) = Abs (erase_Computed t) + | erase_Computed t = t + +(*Returns true iff at most 0 .. (free-1) occur unbound. therefore + check_freevars 0 t iff t is closed*) +fun check_freevars free (Var x) = x < free + | check_freevars free (Const c) = true + | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v + | check_freevars free (Abs m) = check_freevars (free+1) m + | check_freevars free (Computed t) = check_freevars free t + +fun forall_consts pred (Const c) = pred c + | forall_consts pred (Var x) = true + | forall_consts pred (App (u,v)) = forall_consts pred u + andalso forall_consts pred v + | forall_consts pred (Abs m) = forall_consts pred m + | forall_consts pred (Computed t) = forall_consts pred t + +fun closed t = check_freevars 0 t + fun compile _ = raise Compile "abstract machine stub" fun discard _ = raise Compile "abstract machine stub" diff -r eb512c1717ea -r 3224db6415ae src/Tools/Compute_Oracle/am_compiler.ML --- a/src/Tools/Compute_Oracle/am_compiler.ML Sat Oct 27 18:37:06 2007 +0200 +++ b/src/Tools/Compute_Oracle/am_compiler.ML Sat Oct 27 18:37:32 2007 +0200 @@ -25,14 +25,6 @@ type program = (term -> term) - -(*Returns true iff at most 0 .. (free-1) occur unbound. therefore - check_freevars 0 t iff t is closed*) -fun check_freevars free (Var x) = x < free - | check_freevars free (Const c) = true - | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v - | check_freevars free (Abs m) = check_freevars (free+1) m - fun count_patternvars PVar = 1 | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps @@ -66,6 +58,7 @@ | print_term d (Const c) = "c" ^ str c | print_term d (App (a,b)) = "App (" ^ print_term d a ^ ", " ^ print_term d b ^ ")" | print_term d (Abs c) = "Abs (" ^ print_term (d + 1) c ^ ")" + | print_term d (Computed c) = print_term d c fun listvars n = if n = 0 then "x0" else "x"^(str n)^", "^(listvars (n-1)) @@ -85,6 +78,7 @@ | constants_of_term (Abs m) = constants_of_term m | constants_of_term (App (a,b)) = (constants_of_term a)@(constants_of_term b) | constants_of_term (Const c) = [c] + | constants_of_term (Computed c) = constants_of_term c fun load_rules sname name prog = let diff -r eb512c1717ea -r 3224db6415ae src/Tools/Compute_Oracle/am_ghc.ML --- a/src/Tools/Compute_Oracle/am_ghc.ML Sat Oct 27 18:37:06 2007 +0200 +++ b/src/Tools/Compute_Oracle/am_ghc.ML Sat Oct 27 18:37:32 2007 +0200 @@ -9,14 +9,6 @@ type program = string * string * (int Inttab.table) - -(*Returns true iff at most 0 .. (free-1) occur unbound. therefore - check_freevars 0 t iff t is closed*) -fun check_freevars free (Var x) = x < free - | check_freevars free (Const c) = true - | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v - | check_freevars free (Abs m) = check_freevars (free+1) m - fun count_patternvars PVar = 1 | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps diff -r eb512c1717ea -r 3224db6415ae src/Tools/Compute_Oracle/am_interpreter.ML --- a/src/Tools/Compute_Oracle/am_interpreter.ML Sat Oct 27 18:37:06 2007 +0200 +++ b/src/Tools/Compute_Oracle/am_interpreter.ML Sat Oct 27 18:37:32 2007 +0200 @@ -27,6 +27,7 @@ | clos_of_term (Const c) = CConst c | clos_of_term (App (u, v)) = CApp (clos_of_term u, clos_of_term v) | clos_of_term (Abs u) = CAbs (clos_of_term u) + | clos_of_term (Computed t) = clos_of_term t fun term_of_clos (CVar x) = Var x | term_of_clos (CConst c) = Const c @@ -98,6 +99,7 @@ | check_freevars free (Const c) = true | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v | check_freevars free (Abs m) = check_freevars (free+1) m + | check_freevars free (Computed t) = check_freevars free t fun compile eqs = let diff -r eb512c1717ea -r 3224db6415ae src/Tools/Compute_Oracle/am_sml.ML --- a/src/Tools/Compute_Oracle/am_sml.ML Sat Oct 27 18:37:06 2007 +0200 +++ b/src/Tools/Compute_Oracle/am_sml.ML Sat Oct 27 18:37:32 2007 +0200 @@ -34,18 +34,6 @@ fun set_compiled_rewriter r = (compiled_rewriter := SOME r) -fun importable (Var _) = false - | importable (Const _) = true - | importable (App (a, b)) = importable a andalso importable b - | importable (Abs _) = false - -(*Returns true iff at most 0 .. (free-1) occur unbound. therefore - check_freevars 0 t iff t is closed*) -fun check_freevars free (Var x) = x < free - | check_freevars free (Const c) = true - | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v - | check_freevars free (Abs m) = check_freevars (free+1) m - fun count_patternvars PVar = 1 | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps @@ -85,6 +73,7 @@ Abs m => beta (App (Abs m, b)) | a => App (a, beta b)) | beta (Abs m) = Abs (beta m) + | beta (Computed t) = Computed t and subst x (Const c) t = Const c | subst x (Var i) t = if i = x then t else Var i | subst x (App (a,b)) t = App (subst x a t, subst x b t) @@ -361,6 +350,23 @@ in map eval_rule (rev (section (arity + 1))) end + + fun (convert_computed_rules : int -> string list) c = + let + val arity = the (arity_of c) + fun eval_rule () = + let + val sc = string_of_int c + val left = fold (fn i => fn s => "AbstractMachine.App ("^s^(indexed ", x" i)^")") (section arity) ("AbstractMachine.Const "^sc) + fun arg i = "(convert_computed "^(indexed "x" i)^")" + val right = "C"^sc^" "^(string_of_tuple (map arg (section arity))) + val right = if arity > 0 then right else "C"^sc + in + " | convert_computed ("^left^") = "^right + end + in + [eval_rule ()] + end fun mk_constr_type_args n = if n > 0 then " of Term "^(rep_str " * Term" (n-1)) else "" val _ = writelist [ @@ -444,6 +450,15 @@ " | convert (C"^(str c)^" "^leftargs^") = "^right end val _ = writelist (map make_convert constants) + val _ = writelist [ + "", + "fun convert_computed (AbstractMachine.Abs b) = raise AM_SML.Run \"no abstraction in convert_computed allowed\"", + " | convert_computed (AbstractMachine.Var i) = raise AM_SML.Run \"no bound variables in convert_computed allowed\""] + val _ = map (writelist o convert_computed_rules) constants + val _ = writelist [ + " | convert_computed (AbstractMachine.Const c) = Const c", + " | convert_computed (AbstractMachine.App (a, b)) = App (convert_computed a, convert_computed b)", + " | convert_computed (AbstractMachine.Computed a) = raise AM_SML.Run \"no nesting in convert_computed allowed\""] val _ = writelist [ "", "fun eval bounds (AbstractMachine.Abs m) = Abs (fn b => eval (b::bounds) m)", @@ -451,7 +466,8 @@ val _ = map (writelist o eval_rules) constants val _ = writelist [ " | eval bounds (AbstractMachine.App (a, b)) = app (eval bounds a) (eval bounds b)", - " | eval bounds (AbstractMachine.Const c) = Const c"] + " | eval bounds (AbstractMachine.Const c) = Const c", + " | eval bounds (AbstractMachine.Computed t) = convert_computed t"] val _ = writelist [ "", "fun export term = AM_SML.save_result (\""^code^"\", convert term)", @@ -483,7 +499,7 @@ val code = Real.toString (random ()) val module = "AMSML_"^guid val (arity, toplevel_arity, inlinetab, source) = sml_prog module code eqs -(* val _ = writeTextFile "Gencode.ML" source*) + val _ = writeTextFile "Gencode.ML" source val _ = compiled_rewriter := NONE val _ = use_source source in @@ -521,6 +537,7 @@ | inline (Var i) = Var i | inline (App (a, b)) = App (inline a, inline b) | inline (Abs m) = Abs (inline m) + | inline (Computed t) = Computed t in compiled_fun (beta (inline t)) end diff -r eb512c1717ea -r 3224db6415ae src/Tools/Compute_Oracle/compute.ML --- a/src/Tools/Compute_Oracle/compute.ML Sat Oct 27 18:37:06 2007 +0200 +++ b/src/Tools/Compute_Oracle/compute.ML Sat Oct 27 18:37:32 2007 +0200 @@ -6,32 +6,40 @@ signature COMPUTE = sig type computer + type theorem + type naming = int -> string datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML + (* Functions designated with a ! in front of them actually update the computer parameter *) + exception Make of string val make : machine -> theory -> thm list -> computer - - exception Compute of string - val compute : computer -> (int -> string) -> cterm -> term val theory_of : computer -> theory val hyps_of : computer -> term list val shyps_of : computer -> sort list - - val rewrite_param : computer -> (int -> string) -> cterm -> thm - val rewrite : computer -> cterm -> thm + (* ! *) val update : computer -> thm list -> unit + (* ! *) val discard : computer -> unit + + (* ! *) val set_naming : computer -> naming -> unit + val naming_of : computer -> naming + + exception Compute of string + val simplify : computer -> theorem -> thm + val rewrite : computer -> cterm -> thm - val discard : computer -> unit + val make_theorem : computer -> thm -> string list -> theorem + (* ! *) val instantiate : computer -> (string * cterm) list -> theorem -> theorem + (* ! *) val evaluate_prem : computer -> int -> theorem -> theorem + (* ! *) val modus_ponens : computer -> int -> thm -> theorem -> theorem - val setup : theory -> theory - - val print_encoding : bool ref + val setup_compute : theory -> theory end structure Compute :> COMPUTE = struct -val print_encoding = ref false +open Report; datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML @@ -73,7 +81,6 @@ end - exception Make of string; exception Compute of string; @@ -156,9 +163,34 @@ | ProgHaskell of AM_GHC.program | ProgSML of AM_SML.program +fun machine_of_prog (ProgBarras _) = BARRAS + | machine_of_prog (ProgBarrasC _) = BARRAS_COMPILED + | machine_of_prog (ProgHaskell _) = HASKELL + | machine_of_prog (ProgSML _) = SML + structure Sorttab = TableFun(type key = sort val ord = Term.sort_ord) -datatype computer = Computer of theory_ref * Encode.encoding * term list * unit Sorttab.table * prog +type naming = int -> string + +fun default_naming i = "v_" ^ Int.toString i + +datatype computer = Computer of (theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit ref * naming) + option ref + +fun theory_of (Computer (ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy +fun hyps_of (Computer (ref (SOME (_,_,hyps,_,_,_,_)))) = hyps +fun shyps_of (Computer (ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable) +fun shyptab_of (Computer (ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable +fun stamp_of (Computer (ref (SOME (_,_,_,_,_,stamp,_)))) = stamp +fun prog_of (Computer (ref (SOME (_,_,_,_,prog,_,_)))) = prog +fun encoding_of (Computer (ref (SOME (_,encoding,_,_,_,_,_)))) = encoding +fun set_encoding (Computer (r as ref (SOME (p1,encoding,p2,p3,p4,p5,p6)))) encoding' = + (r := SOME (p1,encoding',p2,p3,p4,p5,p6)) +fun naming_of (Computer (ref (SOME (_,_,_,_,_,_,n)))) = n +fun set_naming (Computer (r as ref (SOME (p1,p2,p3,p4,p5,p6,naming)))) naming'= + (r := SOME (p1,p2,p3,p4,p5,p6,naming')) + +fun ref_of (Computer r) = r datatype cthm = ComputeThm of term list * sort list * term @@ -170,7 +202,7 @@ ComputeThm (hyps, shyps, prop) end -fun make machine thy raw_ths = +fun make_internal machine thy stamp encoding raw_ths = let fun transfer (x:thm) = Thm.transfer thy x val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths @@ -256,7 +288,7 @@ let val (encoding_hyptable, rule) = thm2rule encoding_hyptable th in (encoding_hyptable, rule::rules) end) - ths ((Encode.empty, Termtab.empty, Sorttab.empty), []) + ths ((encoding, Termtab.empty, Sorttab.empty), []) val prog = case machine of @@ -269,97 +301,358 @@ val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable - in Computer (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog) end + in (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end + +fun make machine thy raw_thms = Computer (ref (SOME (make_internal machine thy (ref ()) Encode.empty raw_thms))) -(*fun timeit f = +fun update computer raw_thms = + let + val c = make_internal (machine_of_prog (prog_of computer)) (theory_of computer) (stamp_of computer) + (encoding_of computer) raw_thms + val _ = (ref_of computer) := SOME c + in + () + end + +fun discard computer = let - val t1 = Time.toMicroseconds (Time.now ()) - val x = f () - val t2 = Time.toMicroseconds (Time.now ()) - val _ = writeln ("### time = "^(Real.toString ((Real.fromLargeInt t2 - Real.fromLargeInt t1)/(1000000.0)))^"s") + val _ = + case prog_of computer of + ProgBarras p => AM_Interpreter.discard p + | ProgBarrasC p => AM_Compiler.discard p + | ProgHaskell p => AM_GHC.discard p + | ProgSML p => AM_SML.discard p + val _ = (ref_of computer) := NONE in - x - end*) + () + end + +fun runprog (ProgBarras p) = AM_Interpreter.run p + | runprog (ProgBarrasC p) = AM_Compiler.run p + | runprog (ProgHaskell p) = AM_GHC.run p + | runprog (ProgSML p) = AM_SML.run p + +(* ------------------------------------------------------------------------------------- *) +(* An oracle for exporting theorems; must only be accessible from inside this structure! *) +(* ------------------------------------------------------------------------------------- *) + +exception ExportThm of term list * sort list * term + +fun merge_hyps hyps1 hyps2 = +let + fun add hyps tab = fold (fn h => fn tab => Termtab.update (h, ()) tab) hyps tab +in + Termtab.keys (add hyps2 (add hyps1 Termtab.empty)) +end + +fun add_shyps shyps tab = fold (fn h => fn tab => Sorttab.update (h, ()) tab) shyps tab + +fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty)) + +fun export_oracle (thy, ExportThm (hyps, shyps, prop)) = + let + val shyptab = add_shyps shyps Sorttab.empty + fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab + fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab + fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) + val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab + val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab) + val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else () + in + fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop + end + | export_oracle _ = raise Match + +val setup_compute = (fn thy => Theory.add_oracle ("compute", export_oracle) thy) + +fun export_thm thy hyps shyps prop = + let + val th = invoke_oracle_i thy "Compute_Oracle.compute" (thy, ExportThm (hyps, shyps, prop)) + val hyps = map (fn h => assume (cterm_of thy h)) hyps + in + fold (fn h => fn p => implies_elim p h) hyps th + end + +(* --------- Rewrite ----------- *) + +fun rewrite computer ct = + let + val {t=t',T=ty,thy=thy,...} = rep_cterm ct + val _ = Theory.assert_super (theory_of computer) thy + val naming = naming_of computer + val (encoding, t) = remove_types (encoding_of computer) t' + (*val _ = if (!print_encoding) then writeln (makestring ("encoding: ",Encode.fold (fn x => fn s => x::s) encoding [])) else ()*) + val t = runprog (prog_of computer) t + val t = infer_types naming encoding ty t + val eq = Logic.mk_equals (t', t) + in + export_thm thy (hyps_of computer) (Sorttab.keys (shyptab_of computer)) eq + end + +(* --------- Simplify ------------ *) -fun report s f = f () (*writeln s; timeit f*) +datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int + | Prem of AbstractMachine.term +datatype theorem = Theorem of theory_ref * unit ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table + * prem list * AbstractMachine.term * term list * sort list + + +exception ParamSimplify of computer * theorem + +fun make_theorem computer th vars = +let + val _ = Theory.assert_super (theory_of computer) (theory_of_thm th) + + val (ComputeThm (hyps, shyps, prop)) = thm2cthm th + + val encoding = encoding_of computer + + (* variables in the theorem are identified upfront *) + fun collect_vars (Abs (_, _, t)) tab = collect_vars t tab + | collect_vars (a $ b) tab = collect_vars b (collect_vars a tab) + | collect_vars (Const _) tab = tab + | collect_vars (Free _) tab = tab + | collect_vars (Var ((s, i), ty)) tab = + if List.find (fn x => x=s) vars = NONE then + tab + else + (case Symtab.lookup tab s of + SOME ((s',i'),ty') => + if s' <> s orelse i' <> i orelse ty <> ty' then + raise Compute ("make_theorem: variable name '"^s^"' is not unique") + else + tab + | NONE => Symtab.update (s, ((s, i), ty)) tab) + val vartab = collect_vars prop Symtab.empty + fun encodevar (s, t as (_, ty)) (encoding, tab) = + let + val (x, encoding) = Encode.insert (Var t) encoding + in + (encoding, Symtab.update (s, (x, ty)) tab) + end + val (encoding, vartab) = Symtab.fold encodevar vartab (encoding, Symtab.empty) + val varsubst = Inttab.make (map (fn (s, (x, _)) => (x, NONE)) (Symtab.dest vartab)) -fun compute (Computer (rthy, encoding, hyps, shyptable, prog)) naming ct = - let - fun run (ProgBarras p) = AM_Interpreter.run p - | run (ProgBarrasC p) = AM_Compiler.run p - | run (ProgHaskell p) = AM_GHC.run p - | run (ProgSML p) = AM_SML.run p - val {t=t, T=ty, thy=ctthy, ...} = rep_cterm ct - val thy = Theory.merge (Theory.deref rthy, ctthy) - val (encoding, t) = report "remove_types" (fn () => remove_types encoding t) - val _ = if (!print_encoding) then writeln (makestring ("encoding: ",Encode.fold (fn x => fn s => x::s) encoding [])) else () - val t = report "run" (fn () => run prog t) - val t = report "infer_types" (fn () => infer_types naming encoding ty t) + (* make the premises and the conclusion *) + fun mk_prem encoding t = + (let + val (a, b) = Logic.dest_equals t + val ty = type_of a + val (encoding, a) = remove_types encoding a + val (encoding, b) = remove_types encoding b + val (eq, encoding) = Encode.insert (Const ("==", ty --> ty --> @{typ "prop"})) encoding + in + (encoding, EqPrem (a, b, ty, eq)) + end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end) + val (encoding, prems) = + (fold_rev (fn t => fn (encoding, l) => + case mk_prem encoding t of + (encoding, t) => (encoding, t::l)) (Logic.strip_imp_prems prop) (encoding, [])) + val (encoding, concl) = remove_types encoding (Logic.strip_imp_concl prop) + val _ = set_encoding computer encoding +in + Theorem (Theory.check_thy (theory_of_thm th), stamp_of computer, vartab, varsubst, + prems, concl, hyps, shyps) +end + +fun theory_of_theorem (Theorem (rthy,_,_,_,_,_,_,_)) = Theory.deref rthy +fun update_theory thy (Theorem (_,p0,p1,p2,p3,p4,p5,p6)) = + Theorem (Theory.check_thy thy,p0,p1,p2,p3,p4,p5,p6) +fun stamp_of_theorem (Theorem (_,s, _, _, _, _, _, _)) = s +fun vartab_of_theorem (Theorem (_,_,vt,_,_,_,_,_)) = vt +fun varsubst_of_theorem (Theorem (_,_,_,vs,_,_,_,_)) = vs +fun update_varsubst vs (Theorem (p0,p1,p2,_,p3,p4,p5,p6)) = Theorem (p0,p1,p2,vs,p3,p4,p5,p6) +fun prems_of_theorem (Theorem (_,_,_,_,prems,_,_,_)) = prems +fun update_prems prems (Theorem (p0,p1,p2,p3,_,p4,p5,p6)) = Theorem (p0,p1,p2,p3,prems,p4,p5,p6) +fun concl_of_theorem (Theorem (_,_,_,_,_,concl,_,_)) = concl +fun hyps_of_theorem (Theorem (_,_,_,_,_,_,hyps,_)) = hyps +fun update_hyps hyps (Theorem (p0,p1,p2,p3,p4,p5,_,p6)) = Theorem (p0,p1,p2,p3,p4,p5,hyps,p6) +fun shyps_of_theorem (Theorem (_,_,_,_,_,_,_,shyps)) = shyps +fun update_shyps shyps (Theorem (p0,p1,p2,p3,p4,p5,p6,_)) = Theorem (p0,p1,p2,p3,p4,p5,p6,shyps) + +fun check_compatible computer th s = + if stamp_of computer <> stamp_of_theorem th then + raise Compute (s^": computer and theorem are incompatible") + else () + +fun instantiate computer insts th = +let + val _ = check_compatible computer th + + val thy = theory_of computer + + val vartab = vartab_of_theorem th + + fun rewrite computer t = + let + val naming = naming_of computer + val (encoding, t) = remove_types (encoding_of computer) t + val t = runprog (prog_of computer) t + val _ = set_encoding computer encoding in t end -fun discard (Computer (rthy, encoding, hyps, shyptable, prog)) = - (case prog of - ProgBarras p => AM_Interpreter.discard p - | ProgBarrasC p => AM_Compiler.discard p - | ProgHaskell p => AM_GHC.discard p - | ProgSML p => AM_SML.discard p) + fun assert_varfree vs t = + if AbstractMachine.forall_consts (fn x => Inttab.lookup vs x = NONE) t then + () + else + raise Compute "instantiate: assert_varfree failed" + + fun assert_closed t = + if AbstractMachine.closed t then + () + else + raise Compute "instantiate: not a closed term" -fun theory_of (Computer (rthy, _, _,_,_)) = Theory.deref rthy -fun hyps_of (Computer (_, _, hyps, _, _)) = hyps -fun shyps_of (Computer (_, _, _, shyptable, _)) = Sorttab.keys (shyptable) -fun shyptab_of (Computer (_, _, _, shyptable, _)) = shyptable + fun compute_inst (s, ct) vs = + let + val _ = Theory.assert_super (theory_of_cterm ct) thy + val ty = typ_of (ctyp_of_term ct) + in + (case Symtab.lookup vartab s of + NONE => raise Compute ("instantiate: variable '"^s^"' not found in theorem") + | SOME (x, ty') => + (case Inttab.lookup vs x of + SOME (SOME _) => raise Compute ("instantiate: variable '"^s^"' has already been instantiated") + | SOME NONE => + if ty <> ty' then + raise Compute ("instantiate: wrong type for variable '"^s^"'") + else + let + val t = rewrite computer (term_of ct) + val _ = assert_varfree vs t + val _ = assert_closed t + in + Inttab.update (x, SOME t) vs + end + | NONE => raise Compute "instantiate: internal error")) + end -fun default_naming i = "v_" ^ Int.toString i - -exception Param of computer * (int -> string) * cterm; + val vs = fold compute_inst insts (varsubst_of_theorem th) +in + update_varsubst vs th +end -fun rewrite_param r n ct = - let - val thy = theory_of_cterm ct - val th = timeit (fn () => invoke_oracle_i thy "Compute_Oracle.compute" (thy, Param (r, n, ct))) - val hyps = map (fn h => assume (cterm_of thy h)) (hyps_of r) +fun match_aterms subst = + let + exception no_match + open AbstractMachine + fun match subst (b as (Const c)) a = + if a = b then subst + else + (case Inttab.lookup subst c of + SOME (SOME a') => if a=a' then subst else raise no_match + | SOME NONE => if AbstractMachine.closed a then + Inttab.update (c, SOME a) subst + else raise no_match + | NONE => raise no_match) + | match subst (b as (Var _)) a = if a=b then subst else raise no_match + | match subst (App (u, v)) (App (u', v')) = match (match subst u u') v v' + | match subst (Abs u) (Abs u') = match subst u u' + | match subst _ _ = raise no_match in - fold (fn h => fn p => implies_elim p h) hyps th + fn b => fn a => (SOME (match subst b a) handle no_match => NONE) + end + +fun apply_subst vars_allowed subst = + let + open AbstractMachine + fun app (t as (Const c)) = + (case Inttab.lookup subst c of + NONE => t + | SOME (SOME t) => Computed t + | SOME NONE => if vars_allowed then t else raise Compute "apply_subst: no vars allowed") + | app (t as (Var _)) = t + | app (App (u, v)) = App (app u, app v) + | app (Abs m) = Abs (app m) + in + app end -(*fun rewrite_param r n ct = - let - val hyps = hyps_of r - val shyps = shyps_of r - val thy = theory_of_cterm ct - val _ = Theory.assert_super (theory_of r) thy - val t' = timeit (fn () => compute r n ct) - val eq = Logic.mk_equals (term_of ct, t') - in - Thm.unchecked_oracle thy "Compute.compute" (eq, hyps, shyps) - end*) +fun splicein n l L = List.take (L, n) @ l @ List.drop (L, n+1) -fun rewrite r ct = rewrite_param r default_naming ct +fun evaluate_prem computer prem_no th = +let + val _ = check_compatible computer th + val prems = prems_of_theorem th + val varsubst = varsubst_of_theorem th + fun run vars_allowed t = + runprog (prog_of computer) (apply_subst vars_allowed varsubst t) +in + case List.nth (prems, prem_no) of + Prem _ => raise Compute "evaluate_prem: no equality premise" + | EqPrem (a, b, ty, _) => + let + val a' = run false a + val b' = run true b + in + case match_aterms varsubst b' a' of + NONE => + let + fun mk s = makestring (infer_types (naming_of computer) (encoding_of computer) ty s) + val left = "computed left side: "^(mk a') + val right = "computed right side: "^(mk b') + in + raise Compute ("evaluate_prem: cannot assign computed left to right hand side\n"^left^"\n"^right^"\n") + end + | SOME varsubst => + update_prems (splicein prem_no [] prems) (update_varsubst varsubst th) + end +end -(* theory setup *) +fun prem2term (Prem t) = t + | prem2term (EqPrem (a,b,_,eq)) = + AbstractMachine.App (AbstractMachine.App (AbstractMachine.Const eq, a), b) -fun compute_oracle (thy, Param (r, naming, ct)) = - let - val _ = Theory.assert_super (theory_of r) thy - val t' = timeit (fn () => compute r naming ct) - val eq = Logic.mk_equals (term_of ct, t') - val hyps = hyps_of r - val shyptab = shyptab_of r - fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab - fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab - val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (eq::hyps) shyptab) - val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else () - in - fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps eq - end - | compute_oracle _ = raise Match - - -val setup = (fn thy => (writeln "install oracle"; Theory.add_oracle ("compute", compute_oracle) thy)) - -(*val _ = Context.add_setup (Theory.add_oracle ("compute", compute_oracle))*) +fun modus_ponens computer prem_no th' th = +let + val _ = check_compatible computer th + val thy = + let + val thy1 = theory_of_theorem th + val thy2 = theory_of_thm th' + in + if Context.subthy (thy1, thy2) then thy2 + else if Context.subthy (thy2, thy1) then thy1 else + raise Compute "modus_ponens: theorems are not compatible with each other" + end + val th' = make_theorem computer th' [] + val varsubst = varsubst_of_theorem th + fun run vars_allowed t = + runprog (prog_of computer) (apply_subst vars_allowed varsubst t) + val prems = prems_of_theorem th + val prem = run true (prem2term (List.nth (prems, prem_no))) + val concl = run false (concl_of_theorem th') +in + case match_aterms varsubst prem concl of + NONE => raise Compute "modus_ponens: conclusion does not match premise" + | SOME varsubst => + let + val th = update_varsubst varsubst th + val th = update_prems (splicein prem_no (prems_of_theorem th') prems) th + val th = update_hyps (merge_hyps (hyps_of_theorem th) (hyps_of_theorem th')) th + val th = update_shyps (merge_shyps (shyps_of_theorem th) (shyps_of_theorem th')) th + in + update_theory thy th + end +end + +fun simplify computer th = +let + val _ = check_compatible computer th + val varsubst = varsubst_of_theorem th + val encoding = encoding_of computer + val naming = naming_of computer + fun infer t = infer_types naming encoding @{typ "prop"} t + fun run t = infer (runprog (prog_of computer) (apply_subst true varsubst t)) + fun runprem p = run (prem2term p) + val prop = Logic.list_implies (map runprem (prems_of_theorem th), run (concl_of_theorem th)) + val hyps = merge_hyps (hyps_of computer) (hyps_of_theorem th) + val shyps = merge_shyps (shyps_of_theorem th) (Sorttab.keys (shyptab_of computer)) +in + export_thm (theory_of_theorem th) hyps shyps prop +end end