# HG changeset patch # User obua # Date 1193503053 -7200 # Node ID fcf0f50e478cc7b31e5116fd042acad81d63444c # Parent 3224db6415aeed4fa342f214fa50a2e06a626564 better compute oracle diff -r 3224db6415ae -r fcf0f50e478c src/Tools/Compute_Oracle/compute.ML --- a/src/Tools/Compute_Oracle/compute.ML Sat Oct 27 18:37:32 2007 +0200 +++ b/src/Tools/Compute_Oracle/compute.ML Sat Oct 27 18:37:33 2007 +0200 @@ -35,12 +35,16 @@ val setup_compute : theory -> theory + val print_encoding : bool ref + end structure Compute :> COMPUTE = struct open Report; +val print_encoding = ref false + datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML (* Terms are mapped to integer codes *) diff -r 3224db6415ae -r fcf0f50e478c src/Tools/Compute_Oracle/linker.ML --- a/src/Tools/Compute_Oracle/linker.ML Sat Oct 27 18:37:32 2007 +0200 +++ b/src/Tools/Compute_Oracle/linker.ML Sat Oct 27 18:37:33 2007 +0200 @@ -189,7 +189,6 @@ (added_substs, Instances (cfilter, ctab, minsets, substs)) end - fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs local @@ -216,16 +215,20 @@ signature PCOMPUTE = sig - type pcomputer val make : Compute.machine -> theory -> thm list -> Linker.constant list -> pcomputer - -(* val add_thms : pcomputer -> thm list -> bool*) - - val add_instances : pcomputer -> Linker.constant list -> bool + + val add_instances : pcomputer -> Linker.constant list -> bool + val add_instances' : pcomputer -> term list -> bool val rewrite : pcomputer -> cterm list -> thm list + val simplify : pcomputer -> Compute.theorem -> thm + + val make_theorem : pcomputer -> thm -> string list -> Compute.theorem + val instantiate : pcomputer -> (string * cterm) list -> Compute.theorem -> Compute.theorem + val evaluate_prem : pcomputer -> int -> Compute.theorem -> Compute.theorem + val modus_ponens : pcomputer -> int -> thm -> Compute.theorem -> Compute.theorem end @@ -235,7 +238,7 @@ datatype theorem = MonoThm of thm | PolyThm of thm * Linker.instances * thm list -datatype pcomputer = PComputer of Compute.machine * theory_ref * Compute.computer ref * theorem list ref +datatype pcomputer = PComputer of theory_ref * Compute.computer * theorem list ref (*fun collect_consts (Var x) = [] | collect_consts (Bound _) = [] @@ -243,7 +246,9 @@ | collect_consts (Abs (_, _, body)) = collect_consts body | collect_consts t = [Linker.constant_of t]*) -fun collect_consts_of_thm th = +fun computer_of (PComputer (_,computer,_)) = computer + +fun collect_consts_of_thm th = let val th = prop_of th val (prems, th) = (Logic.strip_imp_prems th, Logic.strip_imp_concl th) @@ -287,6 +292,15 @@ Compute.make machine thy ths end +fun update_computer computer ths = + let + fun add (MonoThm th) ths = th::ths + | add (PolyThm (_, _, ths')) ths = ths'@ths + val ths = fold_rev add ths [] + in + Compute.update computer ths + end + fun conv_subst thy (subst : Type.tyenv) = map (fn (iname, (sort, ty)) => (ctyp_of thy (TVar (iname, sort)), ctyp_of thy ty)) (Vartab.dest subst) @@ -356,40 +370,70 @@ map snd (Inttab.dest (!thstab)) end - fun make machine thy ths cs = let - val ths = remove_duplicates ths - val (monocs, ths) = fold_rev (fn th => - fn (monocs, ths) => - let val (m, t) = create_theorem th in - (m@monocs, t::ths) - end) - ths (cs, []) - val (_, ths) = add_monos thy monocs ths - val computer = create_computer machine thy ths + val ths = remove_duplicates ths + val (monocs, ths) = fold_rev (fn th => + fn (monocs, ths) => + let val (m, t) = create_theorem th in + (m@monocs, t::ths) + end) + ths (cs, []) + val (_, ths) = add_monos thy monocs ths + val computer = create_computer machine thy ths in - PComputer (machine, Theory.check_thy thy, ref computer, ref ths) + PComputer (Theory.check_thy thy, computer, ref ths) end -fun add_instances (PComputer (machine, thyref, rcomputer, rths)) cs = +fun add_instances (PComputer (thyref, computer, rths)) cs = let val thy = Theory.deref thyref val (changed, ths) = add_monos thy cs (!rths) in - if changed then - (rcomputer := create_computer machine thy ths; - rths := ths; - true) - else - false + if changed then + (update_computer computer ths; + rths := ths; + true) + else + false + + end + +fun add_instances' pc ts = add_instances pc (Linker.collect_consts ts) + +fun rewrite pc cts = + let + val _ = add_instances' pc (map term_of cts) + val computer = (computer_of pc) + in + map (fn ct => Compute.rewrite computer ct) cts end -fun rewrite (pc as PComputer (_, _, rcomputer, _)) cts = +fun simplify pc th = Compute.simplify (computer_of pc) th + +fun make_theorem pc th vars = let - val _ = map (fn ct => add_instances pc (Linker.collect_consts [term_of ct])) cts + val _ = add_instances' pc [prop_of th] + in - map (fn ct => Compute.rewrite (!rcomputer) ct) cts + Compute.make_theorem (computer_of pc) th vars end +fun instantiate pc insts th = + let + val _ = add_instances' pc (map (term_of o snd) insts) + in + Compute.instantiate (computer_of pc) insts th + end + +fun evaluate_prem pc prem_no th = Compute.evaluate_prem (computer_of pc) prem_no th + +fun modus_ponens pc prem_no th' th = + let + val _ = add_instances' pc [prop_of th'] + in + Compute.modus_ponens (computer_of pc) prem_no th' th + end + + end diff -r 3224db6415ae -r fcf0f50e478c src/Tools/Compute_Oracle/report.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/Compute_Oracle/report.ML Sat Oct 27 18:37:33 2007 +0200 @@ -0,0 +1,33 @@ +structure Report = +struct + +local + + val report_depth = ref 0 + fun space n = if n <= 0 then "" else (space (n-1))^" " + fun report_space () = space (!report_depth) + +in + +fun timeit f = + let + val t1 = start_timing () + val x = f () + val t2 = end_timing t1 + val _ = writeln ((report_space ()) ^ "--> "^t2) + in + x + end + +fun report s f = +let + val _ = writeln ((report_space ())^s) + val _ = report_depth := !report_depth + 1 + val x = timeit f + val _ = report_depth := !report_depth - 1 +in + x +end + +end +end \ No newline at end of file