--- 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 = ()
--- 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
--- 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