# HG changeset patch # User obua # Date 1190283023 -7200 # Node ID 329f1b4d9d16e900770005de459bc2150cebc18d # Parent 3d3ebc0c927c3f5b369e66f831e60ce880eb3f91 improved computing diff -r 3d3ebc0c927c -r 329f1b4d9d16 src/Tools/Compute_Oracle/am_interpreter.ML --- a/src/Tools/Compute_Oracle/am_interpreter.ML Thu Sep 20 12:09:09 2007 +0200 +++ b/src/Tools/Compute_Oracle/am_interpreter.ML Thu Sep 20 12:10:23 2007 +0200 @@ -3,7 +3,13 @@ Author: Steven Obua *) -structure AM_Interpreter : ABSTRACT_MACHINE = struct +signature AM_BARRAS = +sig + include ABSTRACT_MACHINE + val max_reductions : int option ref +end + +structure AM_Interpreter : AM_BARRAS = struct open AbstractMachine; @@ -29,6 +35,29 @@ | term_of_clos (Closure (e, u)) = raise (Run "internal error: closure in normalized term found") | term_of_clos CDummy = raise (Run "internal error: dummy in normalized term found") +fun resolve_closure closures (CVar x) = (case List.nth (closures, x) of CDummy => CVar x | r => r) + | resolve_closure closures (CConst c) = CConst c + | resolve_closure closures (CApp (u, v)) = CApp (resolve_closure closures u, resolve_closure closures v) + | resolve_closure closures (CAbs u) = CAbs (resolve_closure (CDummy::closures) u) + | resolve_closure closures (CDummy) = raise (Run "internal error: resolve_closure applied to CDummy") + | resolve_closure closures (Closure (e, u)) = resolve_closure e u + +fun resolve_closure' c = resolve_closure [] c + +fun resolve_stack tm SEmpty = tm + | resolve_stack tm (SAppL (c, s)) = resolve_stack (CApp (tm, resolve_closure' c)) s + | resolve_stack tm (SAppR (c, s)) = resolve_stack (CApp (resolve_closure' c, tm)) s + | resolve_stack tm (SAbs s) = resolve_stack (CAbs tm) s + +fun resolve (stack, closure) = + let + val _ = writeln "start resolving" + val t = resolve_stack (resolve_closure' closure) stack + val _ = writeln "finished resolving" + in + t + end + fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a | strip_closure args x = (x, args) @@ -104,18 +133,27 @@ fun proj_C (Continue s) = s | proj_C _ = raise Match +exception InterruptedExecution of stack * closure + fun proj_S (Stop s) = s - | proj_S _ = raise Match + | proj_S (Continue (_,_,s,c)) = (s,c) fun cont (Continue _) = true | cont _ = false +val max_reductions = ref (NONE : int option) + fun do_reduction reduce p = let val s = ref (Continue p) - val _ = while cont (!s) do (s := reduce (proj_C (!s))) + val counter = ref 0 + val _ = case !max_reductions of + NONE => while cont (!s) do (s := reduce (proj_C (!s))) + | SOME m => while cont (!s) andalso (!counter < m) do (s := reduce (proj_C (!s)); counter := (!counter) + 1) in - proj_S (!s) + case !max_reductions of + SOME m => if !counter >= m then raise InterruptedExecution (proj_S (!s)) else proj_S (!s) + | NONE => proj_S (!s) end fun weak_reduce (false, prog, stack, Closure (e, CApp (a, b))) = Continue (false, prog, SAppL (Closure (e, b), stack), Closure (e, a)) @@ -131,13 +169,13 @@ | weak_reduce (true, prog, stack, c) = Stop (stack, c) fun strong_reduce (false, prog, stack, Closure (e, CAbs m)) = - let - val (stack', wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure (CDummy::e, m)) - in - case stack' of - SEmpty => Continue (false, prog, SAbs stack, wnf) - | _ => raise (Run "internal error in strong: weak failed") - end + (let + val (stack', wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure (CDummy::e, m)) + in + case stack' of + SEmpty => Continue (false, prog, SAbs stack, wnf) + | _ => raise (Run "internal error in strong: weak failed") + end handle InterruptedExecution state => raise InterruptedExecution (stack, resolve state)) | strong_reduce (false, prog, stack, clos as (CApp (u, v))) = Continue (false, prog, SAppL (v, stack), u) | strong_reduce (false, prog, stack, clos) = Continue (true, prog, stack, clos) | strong_reduce (true, prog, SAbs stack, m) = Continue (false, prog, stack, CAbs m) @@ -146,15 +184,15 @@ | strong_reduce (true, prog, stack, clos) = Stop (stack, clos) fun run prog t = - let - val (stack, wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure ([], clos_of_term t)) - in - case stack of - SEmpty => (case do_reduction strong_reduce (false, prog, SEmpty, wnf) of - (SEmpty, snf) => term_of_clos snf - | _ => raise (Run "internal error in run: strong failed")) - | _ => raise (Run "internal error in run: weak failed") - end + (let + val (stack, wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure ([], clos_of_term t)) + in + case stack of + SEmpty => (case do_reduction strong_reduce (false, prog, SEmpty, wnf) of + (SEmpty, snf) => term_of_clos snf + | _ => raise (Run "internal error in run: strong failed")) + | _ => raise (Run "internal error in run: weak failed") + end handle InterruptedExecution state => term_of_clos (resolve state)) fun discard p = () diff -r 3d3ebc0c927c -r 329f1b4d9d16 src/Tools/Compute_Oracle/am_sml.ML --- a/src/Tools/Compute_Oracle/am_sml.ML Thu Sep 20 12:09:09 2007 +0200 +++ b/src/Tools/Compute_Oracle/am_sml.ML Thu Sep 20 12:10:23 2007 +0200 @@ -330,8 +330,8 @@ val strict_args = (case toplevel_arity_of c of NONE => the (arity_of c) | SOME sa => sa) val xs = map (fn n => if n < strict_args then "x"^(str n) else "x"^(str n)^"()") rightargs val right = (indexed "C" c)^" "^(string_of_tuple xs) - val debug_lazy = "(print x"^(string_of_int (strict_args - 1))^";" - val right = if strict_args < the (arity_of c) then debug_lazy^"raise AM_SML.Run \"unresolved lazy call: "^(string_of_int c)^"\")" else right + val message = "(\"unresolved lazy call: "^(string_of_int c)^", \"^(makestring x"^(string_of_int (strict_args - 1))^"))" + val right = if strict_args < the (arity_of c) then "raise AM_SML.Run "^message else right in (indexed "c" c)^(if gnum > 0 then "_"^(str gnum) else "")^leftargs^" = "^right end @@ -363,7 +363,7 @@ end fun mk_constr_type_args n = if n > 0 then " of Term "^(rep_str " * Term" (n-1)) else "" - val _ = writelist [ + val _ = writelist [ "structure "^name^" = struct", "", "datatype Term = Const of int | App of Term * Term | Abs of (Term -> Term)", @@ -456,7 +456,7 @@ "", "fun export term = AM_SML.save_result (\""^code^"\", convert term)", "", - "val _ = AM_SML.set_compiled_rewriter (fn t => convert (eval [] t))", + "val _ = AM_SML.set_compiled_rewriter (fn t => (convert (eval [] t)))", "", "end"] in diff -r 3d3ebc0c927c -r 329f1b4d9d16 src/Tools/Compute_Oracle/compute.ML --- a/src/Tools/Compute_Oracle/compute.ML Thu Sep 20 12:09:09 2007 +0200 +++ b/src/Tools/Compute_Oracle/compute.ML Thu Sep 20 12:10:23 2007 +0200 @@ -25,10 +25,14 @@ val setup : theory -> theory + val print_encoding : bool ref + end structure Compute :> COMPUTE = struct +val print_encoding = ref false + datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML (* Terms are mapped to integer codes *) @@ -261,8 +265,6 @@ | HASKELL => ProgHaskell (AM_GHC.compile rules) | SML => ProgSML (AM_SML.compile rules) -(* val _ = print (Encode.fold (fn x => fn s => x::s) encoding [])*) - fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable @@ -290,6 +292,7 @@ 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) in @@ -340,7 +343,7 @@ fun compute_oracle (thy, Param (r, naming, ct)) = let val _ = Theory.assert_super (theory_of r) thy - val t' = compute r naming ct + 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