--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML Wed Jul 21 18:13:15 2010 +0200
@@ -8,8 +8,8 @@
Unsynchronized.set timing;
warning "\nset quick_and_dirty\n"; Unsynchronized.set quick_and_dirty;
-List.app time_use_thy tests;
+use_thys tests;
warning "\nreset quick_and_dirty\n"; Unsynchronized.reset quick_and_dirty;
-List.app ThyInfo.remove_thy tests;
-List.app time_use_thy tests;
+List.app Thy_Info.remove_thy tests;
+use_thys tests;
--- a/Admin/Benchmarks/HOL-record/ROOT.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/Admin/Benchmarks/HOL-record/ROOT.ML Wed Jul 21 18:13:15 2010 +0200
@@ -8,7 +8,7 @@
Unsynchronized.set timing;
warning "\nset quick_and_dirty\n"; Unsynchronized.set quick_and_dirty;
-List.app time_use_thy tests;
+use_thys tests;
warning "\nreset quick_and_dirty\n"; Unsynchronized.reset quick_and_dirty;
-List.app time_use_thy tests;
+use_thys tests;
--- a/Admin/isatest/isatest-makeall Wed Jul 21 18:11:51 2010 +0200
+++ b/Admin/isatest/isatest-makeall Wed Jul 21 18:13:15 2010 +0200
@@ -82,7 +82,7 @@
NICE=""
;;
- macbroy23)
+ macbroy28)
MFLAGS="-k -j 2"
NICE="nice"
;;
--- a/Admin/isatest/isatest-makedist Wed Jul 21 18:11:51 2010 +0200
+++ b/Admin/isatest/isatest-makedist Wed Jul 21 18:13:15 2010 +0200
@@ -100,7 +100,7 @@
sleep 15
$SSH macbroy22 "$MAKEALL $HOME/settings/at-poly"
sleep 15
-$SSH macbroy23 "$MAKEALL -l HOL HOL-Library $HOME/settings/at-sml-dev-e"
+$SSH macbroy28 "$MAKEALL -l HOL HOL-Library $HOME/settings/at-sml-dev-e"
sleep 15
$SSH macbroy24 "$MAKEALL $HOME/settings/at64-poly"
sleep 15
--- a/NEWS Wed Jul 21 18:11:51 2010 +0200
+++ b/NEWS Wed Jul 21 18:13:15 2010 +0200
@@ -103,6 +103,15 @@
similar to inductive_cases.
+*** ML ***
+
+* ML antiquotations @{theory} and @{theory_ref} refer to named
+theories from the ancestry of the current context, not any accidental
+theory loader state as before. Potential INCOMPATIBILITY, subtle
+change in semantics.
+
+
+
New in Isabelle2009-2 (June 2010)
---------------------------------
--- a/doc-src/IsarImplementation/Thy/Integration.thy Wed Jul 21 18:11:51 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Integration.thy Wed Jul 21 18:13:15 2010 +0200
@@ -360,9 +360,9 @@
text %mlref {*
\begin{mldecls}
- @{index_ML theory: "string -> theory"} \\
@{index_ML use_thy: "string -> unit"} \\
@{index_ML use_thys: "string list -> unit"} \\
+ @{index_ML Thy_Info.get_theory: "string -> theory"} \\
@{index_ML Thy_Info.touch_thy: "string -> unit"} \\
@{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex]
@{index_ML Thy_Info.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
@@ -374,10 +374,6 @@
\begin{description}
- \item @{ML theory}~@{text A} retrieves the theory value presently
- associated with name @{text A}. Note that the result might be
- outdated.
-
\item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully
up-to-date wrt.\ the external file store, reloading outdated
ancestors as required. In batch mode, the simultaneous @{ML
@@ -390,6 +386,10 @@
intrinsic parallelism can be exploited by the system, to speedup
loading.
+ \item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value
+ presently associated with name @{text A}. Note that the result
+ might be outdated.
+
\item @{ML Thy_Info.touch_thy}~@{text A} performs and @{text outdate} action
on theory @{text A} and all descendants.
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex Wed Jul 21 18:11:51 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex Wed Jul 21 18:13:15 2010 +0200
@@ -433,9 +433,9 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{theory}\verb|theory: string -> theory| \\
\indexdef{}{ML}{use\_thy}\verb|use_thy: string -> unit| \\
\indexdef{}{ML}{use\_thys}\verb|use_thys: string list -> unit| \\
+ \indexdef{}{ML}{Thy\_Info.get\_theory}\verb|Thy_Info.get_theory: string -> theory| \\
\indexdef{}{ML}{Thy\_Info.touch\_thy}\verb|Thy_Info.touch_thy: string -> unit| \\
\indexdef{}{ML}{Thy\_Info.remove\_thy}\verb|Thy_Info.remove_thy: string -> unit| \\[1ex]
\indexdef{}{ML}{Thy\_Info.begin\_theory}\verb|Thy_Info.begin_theory|\verb|: ... -> bool -> theory| \\
@@ -447,10 +447,6 @@
\begin{description}
- \item \verb|theory|~\isa{A} retrieves the theory value presently
- associated with name \isa{A}. Note that the result might be
- outdated.
-
\item \verb|use_thy|~\isa{A} ensures that theory \isa{A} is fully
up-to-date wrt.\ the external file store, reloading outdated
ancestors as required. In batch mode, the simultaneous \verb|use_thys| should be used exclusively.
@@ -462,6 +458,10 @@
intrinsic parallelism can be exploited by the system, to speedup
loading.
+ \item \verb|Thy_Info.get_theory|~\isa{A} retrieves the theory value
+ presently associated with name \isa{A}. Note that the result
+ might be outdated.
+
\item \verb|Thy_Info.touch_thy|~\isa{A} performs and \isa{outdate} action
on theory \isa{A} and all descendants.
--- a/src/HOL/Import/proof_kernel.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Wed Jul 21 18:13:15 2010 +0200
@@ -466,13 +466,11 @@
fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
-val check_name_thy = theory "Main"
-
fun valid_boundvarname s =
- can (fn () => Syntax.read_term_global check_name_thy ("SOME "^s^". True")) ();
+ can (fn () => Syntax.read_term_global @{theory Main} ("SOME "^s^". True")) ();
fun valid_varname s =
- can (fn () => Syntax.read_term_global check_name_thy s) ();
+ can (fn () => Syntax.read_term_global @{theory Main} s) ();
fun protect_varname s =
if innocent_varname s andalso valid_varname s then s else
--- a/src/HOL/IsaMakefile Wed Jul 21 18:11:51 2010 +0200
+++ b/src/HOL/IsaMakefile Wed Jul 21 18:13:15 2010 +0200
@@ -1038,21 +1038,17 @@
HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
-$(LOG)/HOL-Matrix.gz: $(OUT)/HOL \
- $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy \
- $(SRC)/Tools/Compute_Oracle/am_compiler.ML \
- $(SRC)/Tools/Compute_Oracle/am_interpreter.ML \
- $(SRC)/Tools/Compute_Oracle/am.ML \
- $(SRC)/Tools/Compute_Oracle/linker.ML \
- $(SRC)/Tools/Compute_Oracle/am_ghc.ML \
- $(SRC)/Tools/Compute_Oracle/am_sml.ML \
- $(SRC)/Tools/Compute_Oracle/compute.ML Matrix/ComputeFloat.thy \
- Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy Tools/float_arith.ML \
- Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy \
- Matrix/document/root.tex Matrix/ROOT.ML Matrix/Cplex.thy \
+$(LOG)/HOL-Matrix.gz: $(OUT)/HOL Matrix/ComputeFloat.thy \
+ Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy \
+ Matrix/Compute_Oracle/Compute_Oracle.thy Matrix/Compute_Oracle/am.ML \
+ Matrix/Compute_Oracle/am_compiler.ML Matrix/Compute_Oracle/am_ghc.ML \
+ Matrix/Compute_Oracle/am_interpreter.ML \
+ Matrix/Compute_Oracle/am_sml.ML Matrix/Compute_Oracle/compute.ML \
+ Matrix/Compute_Oracle/linker.ML Matrix/Cplex.thy \
Matrix/CplexMatrixConverter.ML Matrix/Cplex_tools.ML \
- Matrix/FloatSparseMatrixBuilder.ML Matrix/fspmlp.ML \
- Matrix/matrixlp.ML
+ Matrix/FloatSparseMatrixBuilder.ML Matrix/LP.thy Matrix/Matrix.thy \
+ Matrix/ROOT.ML Matrix/SparseMatrix.thy Matrix/document/root.tex \
+ Matrix/fspmlp.ML Matrix/matrixlp.ML Tools/float_arith.ML
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix
--- a/src/HOL/Matrix/ComputeHOL.thy Wed Jul 21 18:11:51 2010 +0200
+++ b/src/HOL/Matrix/ComputeHOL.thy Wed Jul 21 18:13:15 2010 +0200
@@ -1,5 +1,5 @@
theory ComputeHOL
-imports Complex_Main "~~/src/Tools/Compute_Oracle/Compute_Oracle"
+imports Complex_Main "Compute_Oracle/Compute_Oracle"
begin
lemma Trueprop_eq_eq: "Trueprop X == (X == True)" by (simp add: atomize_eq)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/Compute_Oracle/Compute_Oracle.thy Wed Jul 21 18:13:15 2010 +0200
@@ -0,0 +1,11 @@
+(* Title: Tools/Compute_Oracle/Compute_Oracle.thy
+ Author: Steven Obua, TU Munich
+
+Steven Obua's evaluator.
+*)
+
+theory Compute_Oracle imports HOL
+uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
+begin
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/Compute_Oracle/am.ML Wed Jul 21 18:13:15 2010 +0200
@@ -0,0 +1,75 @@
+signature ABSTRACT_MACHINE =
+sig
+
+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)
+
+datatype guard = Guard of term * term
+
+type program
+
+exception Compile of string;
+
+(* The de-Bruijn index 0 occurring on the right hand side refers to the LAST pattern variable, when traversing the pattern from left to right,
+ 1 to the second last, and so on. *)
+val compile : pattern list -> (int -> int option) -> (guard list * pattern * term) list -> program
+
+val discard : program -> unit
+
+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 | Computed of term
+
+datatype pattern = PVar | PConst of int * (pattern list)
+
+datatype guard = Guard of term * term
+
+type program = unit
+
+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"
+
+exception Run of string;
+
+fun run p t = raise Run "abstract machine stub"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/Compute_Oracle/am_compiler.ML Wed Jul 21 18:13:15 2010 +0200
@@ -0,0 +1,211 @@
+(* Title: Tools/Compute_Oracle/am_compiler.ML
+ Author: Steven Obua
+*)
+
+signature COMPILING_AM =
+sig
+ include ABSTRACT_MACHINE
+
+ val set_compiled_rewriter : (term -> term) -> unit
+ val list_nth : 'a list * int -> 'a
+ val list_map : ('a -> 'b) -> 'a list -> 'b list
+end
+
+structure AM_Compiler : COMPILING_AM = struct
+
+val list_nth = List.nth;
+val list_map = map;
+
+open AbstractMachine;
+
+val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option)
+
+fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
+
+type program = (term -> term)
+
+fun count_patternvars PVar = 1
+ | count_patternvars (PConst (_, ps)) =
+ List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
+
+fun print_rule (p, t) =
+ let
+ fun str x = Int.toString x
+ fun print_pattern n PVar = (n+1, "x"^(str n))
+ | print_pattern n (PConst (c, [])) = (n, "c"^(str c))
+ | print_pattern n (PConst (c, args)) =
+ let
+ val h = print_pattern n (PConst (c,[]))
+ in
+ print_pattern_list h args
+ end
+ and print_pattern_list r [] = r
+ | print_pattern_list (n, p) (t::ts) =
+ let
+ val (n, t) = print_pattern n t
+ in
+ print_pattern_list (n, "App ("^p^", "^t^")") ts
+ end
+
+ val (n, pattern) = print_pattern 0 p
+ val pattern =
+ if exists_string Symbol.is_ascii_blank pattern then "(" ^ pattern ^")"
+ else pattern
+
+ fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*)
+ "Var " ^ str x
+ | 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))
+
+ val term = print_term 0 t
+ val term =
+ if n > 0 then "Closure (["^(listvars (n-1))^"], "^term^")"
+ else "Closure ([], "^term^")"
+
+ in
+ " | weak_reduce (false, stack, "^pattern^") = Continue (false, stack, "^term^")"
+ end
+
+fun constants_of PVar = []
+ | constants_of (PConst (c, ps)) = c :: maps constants_of ps
+
+fun constants_of_term (Var _) = []
+ | 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
+ val buffer = Unsynchronized.ref ""
+ fun write s = (buffer := (!buffer)^s)
+ fun writeln s = (write s; write "\n")
+ fun writelist [] = ()
+ | writelist (s::ss) = (writeln s; writelist ss)
+ fun str i = Int.toString i
+ val _ = writelist [
+ "structure "^name^" = struct",
+ "",
+ "datatype term = Dummy | App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"]
+ val constants = distinct (op =) (maps (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog)
+ val _ = map (fn x => write (" | c"^(str x))) constants
+ val _ = writelist [
+ "",
+ "datatype stack = SEmpty | SAppL of term * stack | SAppR of term * stack | SAbs of stack",
+ "",
+ "type state = bool * stack * term",
+ "",
+ "datatype loopstate = Continue of state | Stop of stack * term",
+ "",
+ "fun proj_C (Continue s) = s",
+ " | proj_C _ = raise Match",
+ "",
+ "fun proj_S (Stop s) = s",
+ " | proj_S _ = raise Match",
+ "",
+ "fun cont (Continue _) = true",
+ " | cont _ = false",
+ "",
+ "fun do_reduction reduce p =",
+ " let",
+ " val s = Unsynchronized.ref (Continue p)",
+ " val _ = while cont (!s) do (s := reduce (proj_C (!s)))",
+ " in",
+ " proj_S (!s)",
+ " end",
+ ""]
+
+ val _ = writelist [
+ "fun weak_reduce (false, stack, Closure (e, App (a, b))) = Continue (false, SAppL (Closure (e, b), stack), Closure (e, a))",
+ " | weak_reduce (false, SAppL (b, stack), Closure (e, Abs m)) = Continue (false, stack, Closure (b::e, m))",
+ " | weak_reduce (false, stack, c as Closure (e, Abs m)) = Continue (true, stack, c)",
+ " | weak_reduce (false, stack, Closure (e, Var n)) = Continue (false, stack, case "^sname^".list_nth (e, n) of Dummy => Var n | r => r)",
+ " | weak_reduce (false, stack, Closure (e, c)) = Continue (false, stack, c)"]
+ val _ = writelist (map print_rule prog)
+ val _ = writelist [
+ " | weak_reduce (false, stack, clos) = Continue (true, stack, clos)",
+ " | weak_reduce (true, SAppR (a, stack), b) = Continue (false, stack, App (a,b))",
+ " | weak_reduce (true, s as (SAppL (b, stack)), a) = Continue (false, SAppR (a, stack), b)",
+ " | weak_reduce (true, stack, c) = Stop (stack, c)",
+ "",
+ "fun strong_reduce (false, stack, Closure (e, Abs m)) =",
+ " let",
+ " val (stack', wnf) = do_reduction weak_reduce (false, SEmpty, Closure (Dummy::e, m))",
+ " in",
+ " case stack' of",
+ " SEmpty => Continue (false, SAbs stack, wnf)",
+ " | _ => raise ("^sname^".Run \"internal error in strong: weak failed\")",
+ " end",
+ " | strong_reduce (false, stack, clos as (App (u, v))) = Continue (false, SAppL (v, stack), u)",
+ " | strong_reduce (false, stack, clos) = Continue (true, stack, clos)",
+ " | strong_reduce (true, SAbs stack, m) = Continue (false, stack, Abs m)",
+ " | strong_reduce (true, SAppL (b, stack), a) = Continue (false, SAppR (a, stack), b)",
+ " | strong_reduce (true, SAppR (a, stack), b) = Continue (true, stack, App (a, b))",
+ " | strong_reduce (true, stack, clos) = Stop (stack, clos)",
+ ""]
+
+ val ic = "(case c of "^(implode (map (fn c => (str c)^" => c"^(str c)^" | ") constants))^" _ => Const c)"
+ val _ = writelist [
+ "fun importTerm ("^sname^".Var x) = Var x",
+ " | importTerm ("^sname^".Const c) = "^ic,
+ " | importTerm ("^sname^".App (a, b)) = App (importTerm a, importTerm b)",
+ " | importTerm ("^sname^".Abs m) = Abs (importTerm m)",
+ ""]
+
+ fun ec c = " | exportTerm c"^(str c)^" = "^sname^".Const "^(str c)
+ val _ = writelist [
+ "fun exportTerm (Var x) = "^sname^".Var x",
+ " | exportTerm (Const c) = "^sname^".Const c",
+ " | exportTerm (App (a,b)) = "^sname^".App (exportTerm a, exportTerm b)",
+ " | exportTerm (Abs m) = "^sname^".Abs (exportTerm m)",
+ " | exportTerm (Closure (closlist, clos)) = raise ("^sname^".Run \"internal error, cannot export Closure\")",
+ " | exportTerm Dummy = raise ("^sname^".Run \"internal error, cannot export Dummy\")"]
+ val _ = writelist (map ec constants)
+
+ val _ = writelist [
+ "",
+ "fun rewrite t = ",
+ " let",
+ " val (stack, wnf) = do_reduction weak_reduce (false, SEmpty, Closure ([], importTerm t))",
+ " in",
+ " case stack of ",
+ " SEmpty => (case do_reduction strong_reduce (false, SEmpty, wnf) of",
+ " (SEmpty, snf) => exportTerm snf",
+ " | _ => raise ("^sname^".Run \"internal error in rewrite: strong failed\"))",
+ " | _ => (raise ("^sname^".Run \"internal error in rewrite: weak failed\"))",
+ " end",
+ "",
+ "val _ = "^sname^".set_compiled_rewriter rewrite",
+ "",
+ "end;"]
+
+ in
+ compiled_rewriter := NONE;
+ use_text ML_Env.local_context (1, "") false (!buffer);
+ case !compiled_rewriter of
+ NONE => raise (Compile "cannot communicate with compiled function")
+ | SOME r => (compiled_rewriter := NONE; r)
+ end
+
+fun compile cache_patterns const_arity eqs =
+ let
+ val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
+ val eqs = map (fn (a,b,c) => (b,c)) eqs
+ fun check (p, r) = if check_freevars (count_patternvars p) r then () else raise Compile ("unbound variables in rule")
+ val _ = map (fn (p, r) =>
+ (check (p, r);
+ case p of PVar => raise (Compile "pattern is just a variable") | _ => ())) eqs
+ in
+ load_rules "AM_Compiler" "AM_compiled_code" eqs
+ end
+
+fun run prog t = (prog t)
+
+fun discard p = ()
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Wed Jul 21 18:13:15 2010 +0200
@@ -0,0 +1,325 @@
+(* Title: Tools/Compute_Oracle/am_ghc.ML
+ Author: Steven Obua
+*)
+
+structure AM_GHC : ABSTRACT_MACHINE = struct
+
+open AbstractMachine;
+
+type program = string * string * (int Inttab.table)
+
+fun count_patternvars PVar = 1
+ | count_patternvars (PConst (_, ps)) =
+ List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
+
+fun update_arity arity code a =
+ (case Inttab.lookup arity code of
+ NONE => Inttab.update_new (code, a) arity
+ | SOME (a': int) => if a > a' then Inttab.update (code, a) arity else arity)
+
+(* We have to find out the maximal arity of each constant *)
+fun collect_pattern_arity PVar arity = arity
+ | collect_pattern_arity (PConst (c, args)) arity = fold collect_pattern_arity args (update_arity arity c (length args))
+
+local
+fun collect applevel (Var _) arity = arity
+ | collect applevel (Const c) arity = update_arity arity c applevel
+ | collect applevel (Abs m) arity = collect 0 m arity
+ | collect applevel (App (a,b)) arity = collect 0 b (collect (applevel + 1) a arity)
+in
+fun collect_term_arity t arity = collect 0 t arity
+end
+
+fun nlift level n (Var m) = if m < level then Var m else Var (m+n)
+ | nlift level n (Const c) = Const c
+ | nlift level n (App (a,b)) = App (nlift level n a, nlift level n b)
+ | nlift level n (Abs b) = Abs (nlift (level+1) n b)
+
+fun rep n x = if n = 0 then [] else x::(rep (n-1) x)
+
+fun adjust_rules rules =
+ let
+ val arity = fold (fn (p, t) => fn arity => collect_term_arity t (collect_pattern_arity p arity)) rules Inttab.empty
+ fun arity_of c = the (Inttab.lookup arity c)
+ fun adjust_pattern PVar = PVar
+ | adjust_pattern (C as PConst (c, args)) = if (length args <> arity_of c) then raise Compile ("Constant inside pattern must have maximal arity") else C
+ fun adjust_rule (PVar, t) = raise Compile ("pattern may not be a variable")
+ | adjust_rule (rule as (p as PConst (c, args),t)) =
+ let
+ val _ = if not (check_freevars (count_patternvars p) t) then raise Compile ("unbound variables on right hand side") else ()
+ val args = map adjust_pattern args
+ val len = length args
+ val arity = arity_of c
+ fun lift level n (Var m) = if m < level then Var m else Var (m+n)
+ | lift level n (Const c) = Const c
+ | lift level n (App (a,b)) = App (lift level n a, lift level n b)
+ | lift level n (Abs b) = Abs (lift (level+1) n b)
+ val lift = lift 0
+ fun adjust_term n t = if n=0 then t else adjust_term (n-1) (App (t, Var (n-1)))
+ in
+ if len = arity then
+ rule
+ else if arity >= len then
+ (PConst (c, args @ (rep (arity-len) PVar)), adjust_term (arity-len) (lift (arity-len) t))
+ else (raise Compile "internal error in adjust_rule")
+ end
+ in
+ (arity, map adjust_rule rules)
+ end
+
+fun print_term arity_of n =
+let
+ fun str x = string_of_int x
+ fun protect_blank s = if exists_string Symbol.is_ascii_blank s then "(" ^ s ^")" else s
+
+ fun print_apps d f [] = f
+ | print_apps d f (a::args) = print_apps d ("app "^(protect_blank f)^" "^(protect_blank (print_term d a))) args
+ and print_call d (App (a, b)) args = print_call d a (b::args)
+ | print_call d (Const c) args =
+ (case arity_of c of
+ NONE => print_apps d ("Const "^(str c)) args
+ | SOME a =>
+ let
+ val len = length args
+ in
+ if a <= len then
+ let
+ val s = "c"^(str c)^(implode (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, a))))
+ in
+ print_apps d s (List.drop (args, a))
+ end
+ else
+ let
+ fun mk_apps n t = if n = 0 then t else mk_apps (n-1) (App (t, Var (n-1)))
+ fun mk_lambdas n t = if n = 0 then t else mk_lambdas (n-1) (Abs t)
+ fun append_args [] t = t
+ | append_args (c::cs) t = append_args cs (App (t, c))
+ in
+ print_term d (mk_lambdas (a-len) (mk_apps (a-len) (nlift 0 (a-len) (append_args args (Const c)))))
+ end
+ end)
+ | print_call d t args = print_apps d (print_term d t) args
+ and print_term d (Var x) = if x < d then "b"^(str (d-x-1)) else "x"^(str (n-(x-d)-1))
+ | print_term d (Abs c) = "Abs (\\b"^(str d)^" -> "^(print_term (d + 1) c)^")"
+ | print_term d t = print_call d t []
+in
+ print_term 0
+end
+
+fun print_rule arity_of (p, t) =
+ let
+ fun str x = Int.toString x
+ fun print_pattern top n PVar = (n+1, "x"^(str n))
+ | print_pattern top n (PConst (c, [])) = (n, (if top then "c" else "C")^(str c))
+ | print_pattern top n (PConst (c, args)) =
+ let
+ val (n,s) = print_pattern_list (n, (if top then "c" else "C")^(str c)) args
+ in
+ (n, if top then s else "("^s^")")
+ end
+ and print_pattern_list r [] = r
+ | print_pattern_list (n, p) (t::ts) =
+ let
+ val (n, t) = print_pattern false n t
+ in
+ print_pattern_list (n, p^" "^t) ts
+ end
+ val (n, pattern) = print_pattern true 0 p
+ in
+ pattern^" = "^(print_term arity_of n t)
+ end
+
+fun group_rules rules =
+ let
+ fun add_rule (r as (PConst (c,_), _)) groups =
+ let
+ val rs = (case Inttab.lookup groups c of NONE => [] | SOME rs => rs)
+ in
+ Inttab.update (c, r::rs) groups
+ end
+ | add_rule _ _ = raise Compile "internal error group_rules"
+ in
+ fold_rev add_rule rules Inttab.empty
+ end
+
+fun haskell_prog name rules =
+ let
+ val buffer = Unsynchronized.ref ""
+ fun write s = (buffer := (!buffer)^s)
+ fun writeln s = (write s; write "\n")
+ fun writelist [] = ()
+ | writelist (s::ss) = (writeln s; writelist ss)
+ fun str i = Int.toString i
+ val (arity, rules) = adjust_rules rules
+ val rules = group_rules rules
+ val constants = Inttab.keys arity
+ fun arity_of c = Inttab.lookup arity c
+ fun rep_str s n = implode (rep n s)
+ fun indexed s n = s^(str n)
+ fun section n = if n = 0 then [] else (section (n-1))@[n-1]
+ fun make_show c =
+ let
+ val args = section (the (arity_of c))
+ in
+ " show ("^(indexed "C" c)^(implode (map (indexed " a") args))^") = "
+ ^"\""^(indexed "C" c)^"\""^(implode (map (fn a => "++(show "^(indexed "a" a)^")") args))
+ end
+ fun default_case c =
+ let
+ val args = implode (map (indexed " x") (section (the (arity_of c))))
+ in
+ (indexed "c" c)^args^" = "^(indexed "C" c)^args
+ end
+ val _ = writelist [
+ "module "^name^" where",
+ "",
+ "data Term = Const Integer | App Term Term | Abs (Term -> Term)",
+ " "^(implode (map (fn c => " | C"^(str c)^(rep_str " Term" (the (arity_of c)))) constants)),
+ "",
+ "instance Show Term where"]
+ val _ = writelist (map make_show constants)
+ val _ = writelist [
+ " show (Const c) = \"c\"++(show c)",
+ " show (App a b) = \"A\"++(show a)++(show b)",
+ " show (Abs _) = \"L\"",
+ ""]
+ val _ = writelist [
+ "app (Abs a) b = a b",
+ "app a b = App a b",
+ "",
+ "calc s c = writeFile s (show c)",
+ ""]
+ fun list_group c = (writelist (case Inttab.lookup rules c of
+ NONE => [default_case c, ""]
+ | SOME (rs as ((PConst (_, []), _)::rs')) =>
+ if not (null rs') then raise Compile "multiple declaration of constant"
+ else (map (print_rule arity_of) rs) @ [""]
+ | SOME rs => (map (print_rule arity_of) rs) @ [default_case c, ""]))
+ val _ = map list_group constants
+ in
+ (arity, !buffer)
+ end
+
+val guid_counter = Unsynchronized.ref 0
+fun get_guid () =
+ let
+ val c = !guid_counter
+ val _ = guid_counter := !guid_counter + 1
+ in
+ (LargeInt.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c)
+ end
+
+fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
+fun wrap s = "\""^s^"\""
+
+fun writeTextFile name s = File.write (Path.explode name) s
+
+val ghc = Unsynchronized.ref (case getenv "GHC_PATH" of "" => "ghc" | s => s)
+
+fun fileExists name = ((OS.FileSys.fileSize name; true) handle OS.SysErr _ => false)
+
+fun compile cache_patterns const_arity eqs =
+ let
+ val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
+ val eqs = map (fn (a,b,c) => (b,c)) eqs
+ val guid = get_guid ()
+ val module = "AMGHC_Prog_"^guid
+ val (arity, source) = haskell_prog module eqs
+ val module_file = tmp_file (module^".hs")
+ val object_file = tmp_file (module^".o")
+ val _ = writeTextFile module_file source
+ val _ = bash ((!ghc)^" -c "^module_file)
+ val _ = if not (fileExists object_file) then raise Compile ("Failure compiling haskell code (GHC_PATH = '"^(!ghc)^"')") else ()
+ in
+ (guid, module_file, arity)
+ end
+
+fun readResultFile name = File.read (Path.explode name)
+
+fun parse_result arity_of result =
+ let
+ val result = String.explode result
+ fun shift NONE x = SOME x
+ | shift (SOME y) x = SOME (y*10 + x)
+ fun parse_int' x (#"0"::rest) = parse_int' (shift x 0) rest
+ | parse_int' x (#"1"::rest) = parse_int' (shift x 1) rest
+ | parse_int' x (#"2"::rest) = parse_int' (shift x 2) rest
+ | parse_int' x (#"3"::rest) = parse_int' (shift x 3) rest
+ | parse_int' x (#"4"::rest) = parse_int' (shift x 4) rest
+ | parse_int' x (#"5"::rest) = parse_int' (shift x 5) rest
+ | parse_int' x (#"6"::rest) = parse_int' (shift x 6) rest
+ | parse_int' x (#"7"::rest) = parse_int' (shift x 7) rest
+ | parse_int' x (#"8"::rest) = parse_int' (shift x 8) rest
+ | parse_int' x (#"9"::rest) = parse_int' (shift x 9) rest
+ | parse_int' x rest = (x, rest)
+ fun parse_int rest = parse_int' NONE rest
+
+ fun parse (#"C"::rest) =
+ (case parse_int rest of
+ (SOME c, rest) =>
+ let
+ val (args, rest) = parse_list (the (arity_of c)) rest
+ fun app_args [] t = t
+ | app_args (x::xs) t = app_args xs (App (t, x))
+ in
+ (app_args args (Const c), rest)
+ end
+ | (NONE, rest) => raise Run "parse C")
+ | parse (#"c"::rest) =
+ (case parse_int rest of
+ (SOME c, rest) => (Const c, rest)
+ | _ => raise Run "parse c")
+ | parse (#"A"::rest) =
+ let
+ val (a, rest) = parse rest
+ val (b, rest) = parse rest
+ in
+ (App (a,b), rest)
+ end
+ | parse (#"L"::rest) = raise Run "there may be no abstraction in the result"
+ | parse _ = raise Run "invalid result"
+ and parse_list n rest =
+ if n = 0 then
+ ([], rest)
+ else
+ let
+ val (x, rest) = parse rest
+ val (xs, rest) = parse_list (n-1) rest
+ in
+ (x::xs, rest)
+ end
+ val (parsed, rest) = parse result
+ fun is_blank (#" "::rest) = is_blank rest
+ | is_blank (#"\n"::rest) = is_blank rest
+ | is_blank [] = true
+ | is_blank _ = false
+ in
+ if is_blank rest then parsed else raise Run "non-blank suffix in result file"
+ end
+
+fun run (guid, module_file, arity) t =
+ let
+ val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms")
+ fun arity_of c = Inttab.lookup arity c
+ val callguid = get_guid()
+ val module = "AMGHC_Prog_"^guid
+ val call = module^"_Call_"^callguid
+ val result_file = tmp_file (module^"_Result_"^callguid^".txt")
+ val call_file = tmp_file (call^".hs")
+ val term = print_term arity_of 0 t
+ val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
+ val _ = writeTextFile call_file call_source
+ val _ = bash ((!ghc)^" -e \""^call^".call\" "^module_file^" "^call_file)
+ val result = readResultFile result_file handle IO.Io _ => raise Run ("Failure running haskell compiler (GHC_PATH = '"^(!ghc)^"')")
+ val t' = parse_result arity_of result
+ val _ = OS.FileSys.remove call_file
+ val _ = OS.FileSys.remove result_file
+ in
+ t'
+ end
+
+
+fun discard _ = ()
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/Compute_Oracle/am_interpreter.ML Wed Jul 21 18:13:15 2010 +0200
@@ -0,0 +1,213 @@
+(* Title: Tools/Compute_Oracle/am_interpreter.ML
+ Author: Steven Obua
+*)
+
+signature AM_BARRAS =
+sig
+ include ABSTRACT_MACHINE
+ val max_reductions : int option Unsynchronized.ref
+end
+
+structure AM_Interpreter : AM_BARRAS = struct
+
+open AbstractMachine;
+
+datatype closure = CDummy | CVar of int | CConst of int
+ | CApp of closure * closure | CAbs of closure
+ | Closure of (closure list) * closure
+
+structure prog_struct = Table(type key = int*int val ord = prod_ord int_ord int_ord);
+
+datatype program = Program of ((pattern * closure * (closure*closure) list) list) prog_struct.table
+
+datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
+
+fun clos_of_term (Var x) = CVar x
+ | 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
+ | term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
+ | term_of_clos (CAbs u) = Abs (term_of_clos u)
+ | 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)
+
+fun len_head_of_closure n (CApp (a,b)) = len_head_of_closure (n+1) a
+ | len_head_of_closure n x = (n, x)
+
+
+(* earlier occurrence of PVar corresponds to higher de Bruijn index *)
+fun pattern_match args PVar clos = SOME (clos::args)
+ | pattern_match args (PConst (c, patterns)) clos =
+ let
+ val (f, closargs) = strip_closure [] clos
+ in
+ case f of
+ CConst d =>
+ if c = d then
+ pattern_match_list args patterns closargs
+ else
+ NONE
+ | _ => NONE
+ end
+and pattern_match_list args [] [] = SOME args
+ | pattern_match_list args (p::ps) (c::cs) =
+ (case pattern_match args p c of
+ NONE => NONE
+ | SOME args => pattern_match_list args ps cs)
+ | pattern_match_list _ _ _ = NONE
+
+fun count_patternvars PVar = 1
+ | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
+
+fun pattern_key (PConst (c, ps)) = (c, length ps)
+ | pattern_key _ = raise (Compile "pattern reduces to variable")
+
+(*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 compile cache_patterns const_arity eqs =
+ let
+ fun check p r = if check_freevars p r then () else raise Compile ("unbound variables in rule")
+ fun check_guard p (Guard (a,b)) = (check p a; check p b)
+ fun clos_of_guard (Guard (a,b)) = (clos_of_term a, clos_of_term b)
+ val eqs = map (fn (guards, p, r) => let val pcount = count_patternvars p val _ = map (check_guard pcount) (guards) val _ = check pcount r in
+ (pattern_key p, (p, clos_of_term r, map clos_of_guard guards)) end) eqs
+ fun merge (k, a) table = prog_struct.update (k, case prog_struct.lookup table k of NONE => [a] | SOME l => a::l) table
+ val p = fold merge eqs prog_struct.empty
+ in
+ Program p
+ end
+
+
+type state = bool * program * stack * closure
+
+datatype loopstate = Continue of state | Stop of stack * closure
+
+fun proj_C (Continue s) = s
+ | proj_C _ = raise Match
+
+exception InterruptedExecution of stack * closure
+
+fun proj_S (Stop s) = s
+ | proj_S (Continue (_,_,s,c)) = (s,c)
+
+fun cont (Continue _) = true
+ | cont _ = false
+
+val max_reductions = Unsynchronized.ref (NONE : int option)
+
+fun do_reduction reduce p =
+ let
+ val s = Unsynchronized.ref (Continue p)
+ val counter = Unsynchronized.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
+ 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 match_rules prog n [] clos = NONE
+ | match_rules prog n ((p,eq,guards)::rs) clos =
+ case pattern_match [] p clos of
+ NONE => match_rules prog (n+1) rs clos
+ | SOME args => if forall (guard_checks prog args) guards then SOME (Closure (args, eq)) else match_rules prog (n+1) rs clos
+and guard_checks prog args (a,b) = (simp prog (Closure (args, a)) = simp prog (Closure (args, b)))
+and match_closure (p as (Program prog)) clos =
+ case len_head_of_closure 0 clos of
+ (len, CConst c) =>
+ (case prog_struct.lookup prog (c, len) of
+ NONE => NONE
+ | SOME rules => match_rules p 0 rules clos)
+ | _ => NONE
+
+and weak_reduce (false, prog, stack, Closure (e, CApp (a, b))) = Continue (false, prog, SAppL (Closure (e, b), stack), Closure (e, a))
+ | weak_reduce (false, prog, SAppL (b, stack), Closure (e, CAbs m)) = Continue (false, prog, stack, Closure (b::e, m))
+ | weak_reduce (false, prog, stack, Closure (e, CVar n)) = Continue (false, prog, stack, case List.nth (e, n) of CDummy => CVar n | r => r)
+ | weak_reduce (false, prog, stack, Closure (e, c as CConst _)) = Continue (false, prog, stack, c)
+ | weak_reduce (false, prog, stack, clos) =
+ (case match_closure prog clos of
+ NONE => Continue (true, prog, stack, clos)
+ | SOME r => Continue (false, prog, stack, r))
+ | weak_reduce (true, prog, SAppR (a, stack), b) = Continue (false, prog, stack, CApp (a,b))
+ | weak_reduce (true, prog, s as (SAppL (b, stack)), a) = Continue (false, prog, SAppR (a, stack), b)
+ | weak_reduce (true, prog, stack, c) = Stop (stack, c)
+
+and 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 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)
+ | strong_reduce (true, prog, SAppL (b, stack), a) = Continue (false, prog, SAppR (a, stack), b)
+ | strong_reduce (true, prog, SAppR (a, stack), b) = Continue (true, prog, stack, CApp (a, b))
+ | strong_reduce (true, prog, stack, clos) = Stop (stack, clos)
+
+and simp prog t =
+ (let
+ val (stack, wnf) = do_reduction weak_reduce (false, prog, SEmpty, t)
+ in
+ case stack of
+ SEmpty => (case do_reduction strong_reduce (false, prog, SEmpty, wnf) of
+ (SEmpty, snf) => snf
+ | _ => raise (Run "internal error in run: strong failed"))
+ | _ => raise (Run "internal error in run: weak failed")
+ end handle InterruptedExecution state => resolve state)
+
+
+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 handle InterruptedExecution state => term_of_clos (resolve state))
+
+fun discard p = ()
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/Compute_Oracle/am_sml.ML Wed Jul 21 18:13:15 2010 +0200
@@ -0,0 +1,548 @@
+(* Title: Tools/Compute_Oracle/am_sml.ML
+ Author: Steven Obua
+
+TODO: "parameterless rewrite cannot be used in pattern": In a lot of
+cases it CAN be used, and these cases should be handled
+properly; right now, all cases raise an exception.
+*)
+
+signature AM_SML =
+sig
+ include ABSTRACT_MACHINE
+ val save_result : (string * term) -> unit
+ val set_compiled_rewriter : (term -> term) -> unit
+ val list_nth : 'a list * int -> 'a
+ val dump_output : (string option) Unsynchronized.ref
+end
+
+structure AM_SML : AM_SML = struct
+
+open AbstractMachine;
+
+val dump_output = Unsynchronized.ref (NONE: string option)
+
+type program = string * string * (int Inttab.table) * (int Inttab.table) * (term Inttab.table) * (term -> term)
+
+val saved_result = Unsynchronized.ref (NONE:(string*term)option)
+
+fun save_result r = (saved_result := SOME r)
+fun clear_result () = (saved_result := NONE)
+
+val list_nth = List.nth
+
+(*fun list_nth (l,n) = (writeln (makestring ("list_nth", (length l,n))); List.nth (l,n))*)
+
+val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option)
+
+fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
+
+fun count_patternvars PVar = 1
+ | count_patternvars (PConst (_, ps)) =
+ List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
+
+fun update_arity arity code a =
+ (case Inttab.lookup arity code of
+ NONE => Inttab.update_new (code, a) arity
+ | SOME (a': int) => if a > a' then Inttab.update (code, a) arity else arity)
+
+(* We have to find out the maximal arity of each constant *)
+fun collect_pattern_arity PVar arity = arity
+ | collect_pattern_arity (PConst (c, args)) arity = fold collect_pattern_arity args (update_arity arity c (length args))
+
+(* We also need to find out the maximal toplevel arity of each function constant *)
+fun collect_pattern_toplevel_arity PVar arity = raise Compile "internal error: collect_pattern_toplevel_arity"
+ | collect_pattern_toplevel_arity (PConst (c, args)) arity = update_arity arity c (length args)
+
+local
+fun collect applevel (Var _) arity = arity
+ | collect applevel (Const c) arity = update_arity arity c applevel
+ | collect applevel (Abs m) arity = collect 0 m arity
+ | collect applevel (App (a,b)) arity = collect 0 b (collect (applevel + 1) a arity)
+in
+fun collect_term_arity t arity = collect 0 t arity
+end
+
+fun collect_guard_arity (Guard (a,b)) arity = collect_term_arity b (collect_term_arity a arity)
+
+
+fun rep n x = if n < 0 then raise Compile "internal error: rep" else if n = 0 then [] else x::(rep (n-1) x)
+
+fun beta (Const c) = Const c
+ | beta (Var i) = Var i
+ | beta (App (Abs m, b)) = beta (unlift 0 (subst 0 m (lift 0 b)))
+ | beta (App (a, b)) =
+ (case beta a of
+ 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)
+ | subst x (Abs m) t = Abs (subst (x+1) m (lift 0 t))
+and lift level (Const c) = Const c
+ | lift level (App (a,b)) = App (lift level a, lift level b)
+ | lift level (Var i) = if i < level then Var i else Var (i+1)
+ | lift level (Abs m) = Abs (lift (level + 1) m)
+and unlift level (Const c) = Const c
+ | unlift level (App (a, b)) = App (unlift level a, unlift level b)
+ | unlift level (Abs m) = Abs (unlift (level+1) m)
+ | unlift level (Var i) = if i < level then Var i else Var (i-1)
+
+fun nlift level n (Var m) = if m < level then Var m else Var (m+n)
+ | nlift level n (Const c) = Const c
+ | nlift level n (App (a,b)) = App (nlift level n a, nlift level n b)
+ | nlift level n (Abs b) = Abs (nlift (level+1) n b)
+
+fun subst_const (c, t) (Const c') = if c = c' then t else Const c'
+ | subst_const _ (Var i) = Var i
+ | subst_const ct (App (a, b)) = App (subst_const ct a, subst_const ct b)
+ | subst_const ct (Abs m) = Abs (subst_const ct m)
+
+(* Remove all rules that are just parameterless rewrites. This is necessary because SML does not allow functions with no parameters. *)
+fun inline_rules rules =
+ let
+ fun term_contains_const c (App (a, b)) = term_contains_const c a orelse term_contains_const c b
+ | term_contains_const c (Abs m) = term_contains_const c m
+ | term_contains_const c (Var i) = false
+ | term_contains_const c (Const c') = (c = c')
+ fun find_rewrite [] = NONE
+ | find_rewrite ((prems, PConst (c, []), r) :: _) =
+ if check_freevars 0 r then
+ if term_contains_const c r then
+ raise Compile "parameterless rewrite is caught in cycle"
+ else if not (null prems) then
+ raise Compile "parameterless rewrite may not be guarded"
+ else
+ SOME (c, r)
+ else raise Compile "unbound variable on right hand side or guards of rule"
+ | find_rewrite (_ :: rules) = find_rewrite rules
+ fun remove_rewrite (c,r) [] = []
+ | remove_rewrite (cr as (c,r)) ((rule as (prems', PConst (c', args), r'))::rules) =
+ (if c = c' then
+ if null args andalso r = r' andalso null (prems') then
+ remove_rewrite cr rules
+ else raise Compile "incompatible parameterless rewrites found"
+ else
+ rule :: (remove_rewrite cr rules))
+ | remove_rewrite cr (r::rs) = r::(remove_rewrite cr rs)
+ fun pattern_contains_const c (PConst (c', args)) = (c = c' orelse exists (pattern_contains_const c) args)
+ | pattern_contains_const c (PVar) = false
+ fun inline_rewrite (ct as (c, _)) (prems, p, r) =
+ if pattern_contains_const c p then
+ raise Compile "parameterless rewrite cannot be used in pattern"
+ else (map (fn (Guard (a,b)) => Guard (subst_const ct a, subst_const ct b)) prems, p, subst_const ct r)
+ fun inline inlined rules =
+ (case find_rewrite rules of
+ NONE => (Inttab.make inlined, rules)
+ | SOME ct =>
+ let
+ val rules = map (inline_rewrite ct) (remove_rewrite ct rules)
+ val inlined = ct :: (map (fn (c', r) => (c', subst_const ct r)) inlined)
+ in
+ inline inlined rules
+ end)
+ in
+ inline [] rules
+ end
+
+
+(*
+ Calculate the arity, the toplevel_arity, and adjust rules so that all toplevel pattern constants have maximal arity.
+ Also beta reduce the adjusted right hand side of a rule.
+*)
+fun adjust_rules rules =
+ let
+ val arity = fold (fn (prems, p, t) => fn arity => fold collect_guard_arity prems (collect_term_arity t (collect_pattern_arity p arity))) rules Inttab.empty
+ val toplevel_arity = fold (fn (_, p, t) => fn arity => collect_pattern_toplevel_arity p arity) rules Inttab.empty
+ fun arity_of c = the (Inttab.lookup arity c)
+ fun toplevel_arity_of c = the (Inttab.lookup toplevel_arity c)
+ fun test_pattern PVar = ()
+ | test_pattern (C as PConst (c, args)) = if (length args <> arity_of c) then raise Compile ("Constant inside pattern must have maximal arity") else (map test_pattern args; ())
+ fun adjust_rule (_, PVar, _) = raise Compile ("pattern may not be a variable")
+ | adjust_rule (_, PConst (_, []), _) = raise Compile ("cannot deal with rewrites that take no parameters")
+ | adjust_rule (rule as (prems, p as PConst (c, args),t)) =
+ let
+ val patternvars_counted = count_patternvars p
+ fun check_fv t = check_freevars patternvars_counted t
+ val _ = if not (check_fv t) then raise Compile ("unbound variables on right hand side of rule") else ()
+ val _ = if not (forall (fn (Guard (a,b)) => check_fv a andalso check_fv b) prems) then raise Compile ("unbound variables in guards") else ()
+ val _ = map test_pattern args
+ val len = length args
+ val arity = arity_of c
+ val lift = nlift 0
+ fun addapps_tm n t = if n=0 then t else addapps_tm (n-1) (App (t, Var (n-1)))
+ fun adjust_term n t = addapps_tm n (lift n t)
+ fun adjust_guard n (Guard (a,b)) = Guard (lift n a, lift n b)
+ in
+ if len = arity then
+ rule
+ else if arity >= len then
+ (map (adjust_guard (arity-len)) prems, PConst (c, args @ (rep (arity-len) PVar)), adjust_term (arity-len) t)
+ else (raise Compile "internal error in adjust_rule")
+ end
+ fun beta_rule (prems, p, t) = ((prems, p, beta t) handle Match => raise Compile "beta_rule")
+ in
+ (arity, toplevel_arity, map (beta_rule o adjust_rule) rules)
+ end
+
+fun print_term module arity_of toplevel_arity_of pattern_var_count pattern_lazy_var_count =
+let
+ fun str x = string_of_int x
+ fun protect_blank s = if exists_string Symbol.is_ascii_blank s then "(" ^ s ^")" else s
+ val module_prefix = (case module of NONE => "" | SOME s => s^".")
+ fun print_apps d f [] = f
+ | print_apps d f (a::args) = print_apps d (module_prefix^"app "^(protect_blank f)^" "^(protect_blank (print_term d a))) args
+ and print_call d (App (a, b)) args = print_call d a (b::args)
+ | print_call d (Const c) args =
+ (case arity_of c of
+ NONE => print_apps d (module_prefix^"Const "^(str c)) args
+ | SOME 0 => module_prefix^"C"^(str c)
+ | SOME a =>
+ let
+ val len = length args
+ in
+ if a <= len then
+ let
+ val strict_a = (case toplevel_arity_of c of SOME sa => sa | NONE => a)
+ val _ = if strict_a > a then raise Compile "strict" else ()
+ val s = module_prefix^"c"^(str c)^(implode (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, strict_a))))
+ val s = s^(implode (map (fn t => " (fn () => "^print_term d t^")") (List.drop (List.take (args, a), strict_a))))
+ in
+ print_apps d s (List.drop (args, a))
+ end
+ else
+ let
+ fun mk_apps n t = if n = 0 then t else mk_apps (n-1) (App (t, Var (n - 1)))
+ fun mk_lambdas n t = if n = 0 then t else mk_lambdas (n-1) (Abs t)
+ fun append_args [] t = t
+ | append_args (c::cs) t = append_args cs (App (t, c))
+ in
+ print_term d (mk_lambdas (a-len) (mk_apps (a-len) (nlift 0 (a-len) (append_args args (Const c)))))
+ end
+ end)
+ | print_call d t args = print_apps d (print_term d t) args
+ and print_term d (Var x) =
+ if x < d then
+ "b"^(str (d-x-1))
+ else
+ let
+ val n = pattern_var_count - (x-d) - 1
+ val x = "x"^(str n)
+ in
+ if n < pattern_var_count - pattern_lazy_var_count then
+ x
+ else
+ "("^x^" ())"
+ end
+ | print_term d (Abs c) = module_prefix^"Abs (fn b"^(str d)^" => "^(print_term (d + 1) c)^")"
+ | print_term d t = print_call d t []
+in
+ print_term 0
+end
+
+fun section n = if n = 0 then [] else (section (n-1))@[n-1]
+
+fun print_rule gnum arity_of toplevel_arity_of (guards, p, t) =
+ let
+ fun str x = Int.toString x
+ fun print_pattern top n PVar = (n+1, "x"^(str n))
+ | print_pattern top n (PConst (c, [])) = (n, (if top then "c" else "C")^(str c)^(if top andalso gnum > 0 then "_"^(str gnum) else ""))
+ | print_pattern top n (PConst (c, args)) =
+ let
+ val f = (if top then "c" else "C")^(str c)^(if top andalso gnum > 0 then "_"^(str gnum) else "")
+ val (n, s) = print_pattern_list 0 top (n, f) args
+ in
+ (n, s)
+ end
+ and print_pattern_list' counter top (n,p) [] = if top then (n,p) else (n,p^")")
+ | print_pattern_list' counter top (n, p) (t::ts) =
+ let
+ val (n, t) = print_pattern false n t
+ in
+ print_pattern_list' (counter + 1) top (n, if top then p^" (a"^(str counter)^" as ("^t^"))" else p^", "^t) ts
+ end
+ and print_pattern_list counter top (n, p) (t::ts) =
+ let
+ val (n, t) = print_pattern false n t
+ in
+ print_pattern_list' (counter + 1) top (n, if top then p^" (a"^(str counter)^" as ("^t^"))" else p^" ("^t) ts
+ end
+ val c = (case p of PConst (c, _) => c | _ => raise Match)
+ val (n, pattern) = print_pattern true 0 p
+ val lazy_vars = the (arity_of c) - the (toplevel_arity_of c)
+ fun print_tm tm = print_term NONE arity_of toplevel_arity_of n lazy_vars tm
+ fun print_guard (Guard (a,b)) = "term_eq ("^(print_tm a)^") ("^(print_tm b)^")"
+ val else_branch = "c"^(str c)^"_"^(str (gnum+1))^(implode (map (fn i => " a"^(str i)) (section (the (arity_of c)))))
+ fun print_guards t [] = print_tm t
+ | print_guards t (g::gs) = "if ("^(print_guard g)^")"^(implode (map (fn g => " andalso ("^(print_guard g)^")") gs))^" then ("^(print_tm t)^") else "^else_branch
+ in
+ (if null guards then gnum else gnum+1, pattern^" = "^(print_guards t guards))
+ end
+
+fun group_rules rules =
+ let
+ fun add_rule (r as (_, PConst (c,_), _)) groups =
+ let
+ val rs = (case Inttab.lookup groups c of NONE => [] | SOME rs => rs)
+ in
+ Inttab.update (c, r::rs) groups
+ end
+ | add_rule _ _ = raise Compile "internal error group_rules"
+ in
+ fold_rev add_rule rules Inttab.empty
+ end
+
+fun sml_prog name code rules =
+ let
+ val buffer = Unsynchronized.ref ""
+ fun write s = (buffer := (!buffer)^s)
+ fun writeln s = (write s; write "\n")
+ fun writelist [] = ()
+ | writelist (s::ss) = (writeln s; writelist ss)
+ fun str i = Int.toString i
+ val (inlinetab, rules) = inline_rules rules
+ val (arity, toplevel_arity, rules) = adjust_rules rules
+ val rules = group_rules rules
+ val constants = Inttab.keys arity
+ fun arity_of c = Inttab.lookup arity c
+ fun toplevel_arity_of c = Inttab.lookup toplevel_arity c
+ fun rep_str s n = implode (rep n s)
+ fun indexed s n = s^(str n)
+ fun string_of_tuple [] = ""
+ | string_of_tuple (x::xs) = "("^x^(implode (map (fn s => ", "^s) xs))^")"
+ fun string_of_args [] = ""
+ | string_of_args (x::xs) = x^(implode (map (fn s => " "^s) xs))
+ fun default_case gnum c =
+ let
+ val leftargs = implode (map (indexed " x") (section (the (arity_of c))))
+ val rightargs = section (the (arity_of c))
+ 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 message = "(\"unresolved lazy call: " ^ string_of_int c ^ "\")"
+ 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
+
+ fun eval_rules c =
+ let
+ val arity = the (arity_of c)
+ val strict_arity = (case toplevel_arity_of c of NONE => arity | SOME sa => sa)
+ fun eval_rule n =
+ let
+ val sc = string_of_int c
+ val left = fold (fn i => fn s => "AbstractMachine.App ("^s^(indexed ", x" i)^")") (section n) ("AbstractMachine.Const "^sc)
+ fun arg i =
+ let
+ val x = indexed "x" i
+ val x = if i < n then "(eval bounds "^x^")" else x
+ val x = if i < strict_arity then x else "(fn () => "^x^")"
+ in
+ x
+ end
+ val right = "c"^sc^" "^(string_of_args (map arg (section arity)))
+ val right = fold_rev (fn i => fn s => "Abs (fn "^(indexed "x" i)^" => "^s^")") (List.drop (section arity, n)) right
+ val right = if arity > 0 then right else "C"^sc
+ in
+ " | eval bounds ("^left^") = "^right
+ end
+ in
+ map eval_rule (rev (section (arity + 1)))
+ end
+
+ fun convert_computed_rules (c: int) : string list =
+ 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 [
+ "structure "^name^" = struct",
+ "",
+ "datatype Term = Const of int | App of Term * Term | Abs of (Term -> Term)",
+ " "^(implode (map (fn c => " | C"^(str c)^(mk_constr_type_args (the (arity_of c)))) constants)),
+ ""]
+ fun make_constr c argprefix = "(C"^(str c)^" "^(string_of_tuple (map (fn i => argprefix^(str i)) (section (the (arity_of c)))))^")"
+ fun make_term_eq c = " | term_eq "^(make_constr c "a")^" "^(make_constr c "b")^" = "^
+ (case the (arity_of c) of
+ 0 => "true"
+ | n =>
+ let
+ val eqs = map (fn i => "term_eq a"^(str i)^" b"^(str i)) (section n)
+ val (eq, eqs) = (List.hd eqs, map (fn s => " andalso "^s) (List.tl eqs))
+ in
+ eq^(implode eqs)
+ end)
+ val _ = writelist [
+ "fun term_eq (Const c1) (Const c2) = (c1 = c2)",
+ " | term_eq (App (a1,a2)) (App (b1,b2)) = term_eq a1 b1 andalso term_eq a2 b2"]
+ val _ = writelist (map make_term_eq constants)
+ val _ = writelist [
+ " | term_eq _ _ = false",
+ ""
+ ]
+ val _ = writelist [
+ "fun app (Abs a) b = a b",
+ " | app a b = App (a, b)",
+ ""]
+ fun defcase gnum c = (case arity_of c of NONE => [] | SOME a => if a > 0 then [default_case gnum c] else [])
+ fun writefundecl [] = ()
+ | writefundecl (x::xs) = writelist ((("and "^x)::(map (fn s => " | "^s) xs)))
+ fun list_group c = (case Inttab.lookup rules c of
+ NONE => [defcase 0 c]
+ | SOME rs =>
+ let
+ val rs =
+ fold
+ (fn r =>
+ fn rs =>
+ let
+ val (gnum, l, rs) =
+ (case rs of
+ [] => (0, [], [])
+ | (gnum, l)::rs => (gnum, l, rs))
+ val (gnum', r) = print_rule gnum arity_of toplevel_arity_of r
+ in
+ if gnum' = gnum then
+ (gnum, r::l)::rs
+ else
+ let
+ val args = implode (map (fn i => " a"^(str i)) (section (the (arity_of c))))
+ fun gnumc g = if g > 0 then "c"^(str c)^"_"^(str g)^args else "c"^(str c)^args
+ val s = gnumc (gnum) ^ " = " ^ gnumc (gnum')
+ in
+ (gnum', [])::(gnum, s::r::l)::rs
+ end
+ end)
+ rs []
+ val rs = (case rs of [] => [(0,defcase 0 c)] | (gnum,l)::rs => (gnum, (defcase gnum c)@l)::rs)
+ in
+ rev (map (fn z => rev (snd z)) rs)
+ end)
+ val _ = map (fn z => (map writefundecl z; writeln "")) (map list_group constants)
+ val _ = writelist [
+ "fun convert (Const i) = AM_SML.Const i",
+ " | convert (App (a, b)) = AM_SML.App (convert a, convert b)",
+ " | convert (Abs _) = raise AM_SML.Run \"no abstraction in result allowed\""]
+ fun make_convert c =
+ let
+ val args = map (indexed "a") (section (the (arity_of c)))
+ val leftargs =
+ case args of
+ [] => ""
+ | (x::xs) => "("^x^(implode (map (fn s => ", "^s) xs))^")"
+ val args = map (indexed "convert a") (section (the (arity_of c)))
+ val right = fold (fn x => fn s => "AM_SML.App ("^s^", "^x^")") args ("AM_SML.Const "^(str c))
+ in
+ " | 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)",
+ " | eval bounds (AbstractMachine.Var i) = AM_SML.list_nth (bounds, i)"]
+ 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.Computed t) = convert_computed t"]
+ val _ = writelist [
+ "",
+ "fun export term = AM_SML.save_result (\""^code^"\", convert term)",
+ "",
+ "val _ = AM_SML.set_compiled_rewriter (fn t => (convert (eval [] t)))",
+ "",
+ "end"]
+ in
+ (arity, toplevel_arity, inlinetab, !buffer)
+ end
+
+val guid_counter = Unsynchronized.ref 0
+fun get_guid () =
+ let
+ val c = !guid_counter
+ val _ = guid_counter := !guid_counter + 1
+ in
+ (LargeInt.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c)
+ end
+
+
+fun writeTextFile name s = File.write (Path.explode name) s
+
+fun use_source src = use_text ML_Env.local_context (1, "") false src
+
+fun compile cache_patterns const_arity eqs =
+ let
+ val guid = get_guid ()
+ val code = Real.toString (random ())
+ val module = "AMSML_"^guid
+ val (arity, toplevel_arity, inlinetab, source) = sml_prog module code eqs
+ val _ = case !dump_output of NONE => () | SOME p => writeTextFile p source
+ val _ = compiled_rewriter := NONE
+ val _ = use_source source
+ in
+ case !compiled_rewriter of
+ NONE => raise Compile "broken link to compiled function"
+ | SOME f => (module, code, arity, toplevel_arity, inlinetab, f)
+ end
+
+
+fun run' (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t =
+ let
+ val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms")
+ fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t)
+ | inline (Var i) = Var i
+ | inline (App (a, b)) = App (inline a, inline b)
+ | inline (Abs m) = Abs (inline m)
+ val t = beta (inline t)
+ fun arity_of c = Inttab.lookup arity c
+ fun toplevel_arity_of c = Inttab.lookup toplevel_arity c
+ val term = print_term NONE arity_of toplevel_arity_of 0 0 t
+ val source = "local open "^module^" in val _ = export ("^term^") end"
+ val _ = writeTextFile "Gencode_call.ML" source
+ val _ = clear_result ()
+ val _ = use_source source
+ in
+ case !saved_result of
+ NONE => raise Run "broken link to compiled code"
+ | SOME (code', t) => (clear_result (); if code' = code then t else raise Run "link to compiled code was hijacked")
+ end
+
+fun run (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t =
+ let
+ val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms")
+ fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t)
+ | 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
+
+fun discard p = ()
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/Compute_Oracle/compute.ML Wed Jul 21 18:13:15 2010 +0200
@@ -0,0 +1,683 @@
+(* Title: Tools/Compute_Oracle/compute.ML
+ Author: Steven Obua
+*)
+
+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
+ val make_with_cache : machine -> theory -> term list -> thm list -> computer
+ val theory_of : computer -> theory
+ val hyps_of : computer -> term list
+ val shyps_of : computer -> sort list
+ (* ! *) val update : computer -> thm list -> unit
+ (* ! *) val update_with_cache : computer -> term list -> 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 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
+
+end
+
+structure Compute :> COMPUTE = struct
+
+open Report;
+
+datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML
+
+(* Terms are mapped to integer codes *)
+structure Encode :>
+sig
+ type encoding
+ val empty : encoding
+ val insert : term -> encoding -> int * encoding
+ val lookup_code : term -> encoding -> int option
+ val lookup_term : int -> encoding -> term option
+ val remove_code : int -> encoding -> encoding
+ val remove_term : term -> encoding -> encoding
+ val fold : ((term * int) -> 'a -> 'a) -> encoding -> 'a -> 'a
+end
+=
+struct
+
+type encoding = int * (int Termtab.table) * (term Inttab.table)
+
+val empty = (0, Termtab.empty, Inttab.empty)
+
+fun insert t (e as (count, term2int, int2term)) =
+ (case Termtab.lookup term2int t of
+ NONE => (count, (count+1, Termtab.update_new (t, count) term2int, Inttab.update_new (count, t) int2term))
+ | SOME code => (code, e))
+
+fun lookup_code t (_, term2int, _) = Termtab.lookup term2int t
+
+fun lookup_term c (_, _, int2term) = Inttab.lookup int2term c
+
+fun remove_code c (e as (count, term2int, int2term)) =
+ (case lookup_term c e of NONE => e | SOME t => (count, Termtab.delete t term2int, Inttab.delete c int2term))
+
+fun remove_term t (e as (count, term2int, int2term)) =
+ (case lookup_code t e of NONE => e | SOME c => (count, Termtab.delete t term2int, Inttab.delete c int2term))
+
+fun fold f (_, term2int, _) = Termtab.fold f term2int
+
+end
+
+exception Make of string;
+exception Compute of string;
+
+local
+ fun make_constant t ty encoding =
+ let
+ val (code, encoding) = Encode.insert t encoding
+ in
+ (encoding, AbstractMachine.Const code)
+ end
+in
+
+fun remove_types encoding t =
+ case t of
+ Var (_, ty) => make_constant t ty encoding
+ | Free (_, ty) => make_constant t ty encoding
+ | Const (_, ty) => make_constant t ty encoding
+ | Abs (_, ty, t') =>
+ let val (encoding, t'') = remove_types encoding t' in
+ (encoding, AbstractMachine.Abs t'')
+ end
+ | a $ b =>
+ let
+ val (encoding, a) = remove_types encoding a
+ val (encoding, b) = remove_types encoding b
+ in
+ (encoding, AbstractMachine.App (a,b))
+ end
+ | Bound b => (encoding, AbstractMachine.Var b)
+end
+
+local
+ fun type_of (Free (_, ty)) = ty
+ | type_of (Const (_, ty)) = ty
+ | type_of (Var (_, ty)) = ty
+ | type_of _ = sys_error "infer_types: type_of error"
+in
+fun infer_types naming encoding =
+ let
+ fun infer_types _ bounds _ (AbstractMachine.Var v) = (Bound v, List.nth (bounds, v))
+ | infer_types _ bounds _ (AbstractMachine.Const code) =
+ let
+ val c = the (Encode.lookup_term code encoding)
+ in
+ (c, type_of c)
+ end
+ | infer_types level bounds _ (AbstractMachine.App (a, b)) =
+ let
+ val (a, aty) = infer_types level bounds NONE a
+ val (adom, arange) =
+ case aty of
+ Type ("fun", [dom, range]) => (dom, range)
+ | _ => sys_error "infer_types: function type expected"
+ val (b, bty) = infer_types level bounds (SOME adom) b
+ in
+ (a $ b, arange)
+ end
+ | infer_types level bounds (SOME (ty as Type ("fun", [dom, range]))) (AbstractMachine.Abs m) =
+ let
+ val (m, _) = infer_types (level+1) (dom::bounds) (SOME range) m
+ in
+ (Abs (naming level, dom, m), ty)
+ end
+ | infer_types _ _ NONE (AbstractMachine.Abs m) = sys_error "infer_types: cannot infer type of abstraction"
+
+ fun infer ty term =
+ let
+ val (term', _) = infer_types 0 [] (SOME ty) term
+ in
+ term'
+ end
+ in
+ infer
+ end
+end
+
+datatype prog =
+ ProgBarras of AM_Interpreter.program
+ | ProgBarrasC of AM_Compiler.program
+ | 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
+
+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 Unsynchronized.ref * naming)
+ option Unsynchronized.ref
+
+fun theory_of (Computer (Unsynchronized.ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy
+fun hyps_of (Computer (Unsynchronized.ref (SOME (_,_,hyps,_,_,_,_)))) = hyps
+fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable)
+fun shyptab_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable
+fun stamp_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,stamp,_)))) = stamp
+fun prog_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,prog,_,_)))) = prog
+fun encoding_of (Computer (Unsynchronized.ref (SOME (_,encoding,_,_,_,_,_)))) = encoding
+fun set_encoding (Computer (r as Unsynchronized.ref (SOME (p1,encoding,p2,p3,p4,p5,p6)))) encoding' =
+ (r := SOME (p1,encoding',p2,p3,p4,p5,p6))
+fun naming_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,_,n)))) = n
+fun set_naming (Computer (r as Unsynchronized.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
+
+fun thm2cthm th =
+ let
+ val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th
+ val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else ()
+ in
+ ComputeThm (hyps, shyps, prop)
+ end
+
+fun make_internal machine thy stamp encoding cache_pattern_terms raw_ths =
+ let
+ fun transfer (x:thm) = Thm.transfer thy x
+ val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths
+
+ fun make_pattern encoding n vars (var as AbstractMachine.Abs _) =
+ raise (Make "no lambda abstractions allowed in pattern")
+ | make_pattern encoding n vars (var as AbstractMachine.Var _) =
+ raise (Make "no bound variables allowed in pattern")
+ | make_pattern encoding n vars (AbstractMachine.Const code) =
+ (case the (Encode.lookup_term code encoding) of
+ Var _ => ((n+1, Inttab.update_new (code, n) vars, AbstractMachine.PVar)
+ handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed"))
+ | _ => (n, vars, AbstractMachine.PConst (code, [])))
+ | make_pattern encoding n vars (AbstractMachine.App (a, b)) =
+ let
+ val (n, vars, pa) = make_pattern encoding n vars a
+ val (n, vars, pb) = make_pattern encoding n vars b
+ in
+ case pa of
+ AbstractMachine.PVar =>
+ raise (Make "patterns may not start with a variable")
+ | AbstractMachine.PConst (c, args) =>
+ (n, vars, AbstractMachine.PConst (c, args@[pb]))
+ end
+
+ fun thm2rule (encoding, hyptable, shyptable) th =
+ let
+ val (ComputeThm (hyps, shyps, prop)) = th
+ val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable
+ val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable
+ val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop)
+ val (a, b) = Logic.dest_equals prop
+ handle TERM _ => raise (Make "theorems must be meta-level equations (with optional guards)")
+ val a = Envir.eta_contract a
+ val b = Envir.eta_contract b
+ val prems = map Envir.eta_contract prems
+
+ val (encoding, left) = remove_types encoding a
+ val (encoding, right) = remove_types encoding b
+ fun remove_types_of_guard encoding g =
+ (let
+ val (t1, t2) = Logic.dest_equals g
+ val (encoding, t1) = remove_types encoding t1
+ val (encoding, t2) = remove_types encoding t2
+ in
+ (encoding, AbstractMachine.Guard (t1, t2))
+ end handle TERM _ => raise (Make "guards must be meta-level equations"))
+ 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, [])
+
+ (* Principally, a check should be made here to see if the (meta-) hyps contain any of the variables of the rule.
+ As it is, all variables of the rule are schematic, and there are no schematic variables in meta-hyps, therefore
+ this check can be left out. *)
+
+ val (vcount, vars, pattern) = make_pattern encoding 0 Inttab.empty left
+ val _ = (case pattern of
+ AbstractMachine.PVar =>
+ raise (Make "patterns may not start with a variable")
+ (* | AbstractMachine.PConst (_, []) =>
+ (print th; raise (Make "no parameter rewrite found"))*)
+ | _ => ())
+
+ (* finally, provide a function for renaming the
+ pattern bound variables on the right hand side *)
+
+ fun rename level vars (var as AbstractMachine.Var _) = var
+ | rename level vars (c as AbstractMachine.Const code) =
+ (case Inttab.lookup vars code of
+ NONE => c
+ | SOME n => AbstractMachine.Var (vcount-n-1+level))
+ | rename level vars (AbstractMachine.App (a, b)) =
+ AbstractMachine.App (rename level vars a, rename level vars b)
+ | rename level vars (AbstractMachine.Abs m) =
+ AbstractMachine.Abs (rename (level+1) vars m)
+
+ fun rename_guard (AbstractMachine.Guard (a,b)) =
+ AbstractMachine.Guard (rename 0 vars a, rename 0 vars b)
+ in
+ ((encoding, hyptable, shyptable), (map rename_guard prems, pattern, rename 0 vars right))
+ end
+
+ val ((encoding, hyptable, shyptable), rules) =
+ fold_rev (fn th => fn (encoding_hyptable, rules) =>
+ let
+ val (encoding_hyptable, rule) = thm2rule encoding_hyptable th
+ in (encoding_hyptable, rule::rules) end)
+ ths ((encoding, Termtab.empty, Sorttab.empty), [])
+
+ fun make_cache_pattern t (encoding, cache_patterns) =
+ let
+ val (encoding, a) = remove_types encoding t
+ val (_,_,p) = make_pattern encoding 0 Inttab.empty a
+ in
+ (encoding, p::cache_patterns)
+ end
+
+ val (encoding, cache_patterns) = fold_rev make_cache_pattern cache_pattern_terms (encoding, [])
+
+ fun arity (Type ("fun", [a,b])) = 1 + arity b
+ | arity _ = 0
+
+ fun make_arity (Const (s, _), i) tab =
+ (Inttab.update (i, arity (Sign.the_const_type thy s)) tab handle TYPE _ => tab)
+ | make_arity _ tab = tab
+
+ val const_arity_tab = Encode.fold make_arity encoding Inttab.empty
+ fun const_arity x = Inttab.lookup const_arity_tab x
+
+ val prog =
+ case machine of
+ BARRAS => ProgBarras (AM_Interpreter.compile cache_patterns const_arity rules)
+ | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile cache_patterns const_arity rules)
+ | HASKELL => ProgHaskell (AM_GHC.compile cache_patterns const_arity rules)
+ | SML => ProgSML (AM_SML.compile cache_patterns const_arity rules)
+
+ fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
+
+ val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable
+
+ in (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end
+
+fun make_with_cache machine thy cache_patterns raw_thms =
+ Computer (Unsynchronized.ref (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty cache_patterns raw_thms)))
+
+fun make machine thy raw_thms = make_with_cache machine thy [] raw_thms
+
+fun update_with_cache computer cache_patterns raw_thms =
+ let
+ val c = make_internal (machine_of_prog (prog_of computer)) (theory_of computer) (stamp_of computer)
+ (encoding_of computer) cache_patterns raw_thms
+ val _ = (ref_of computer) := SOME c
+ in
+ ()
+ end
+
+fun update computer raw_thms = update_with_cache computer [] raw_thms
+
+fun discard computer =
+ let
+ 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
+ ()
+ 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! *)
+(* ------------------------------------------------------------------------------------- *)
+
+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))
+
+val (_, export_oracle) = Context.>>> (Context.map_theory_result
+ (Thm.add_oracle (Binding.name "compute", fn (thy, 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: " ^
+ commas (map (Syntax.string_of_sort_global thy) shyps))
+ else ()
+ in
+ Thm.cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop)
+ end)));
+
+fun export_thm thy hyps shyps prop =
+ let
+ val th = export_oracle (thy, hyps, shyps, prop)
+ val hyps = map (fn h => Thm.assume (cterm_of thy h)) hyps
+ in
+ fold (fn h => fn p => Thm.implies_elim p h) hyps th
+ end
+
+(* --------- Rewrite ----------- *)
+
+fun rewrite computer ct =
+ let
+ val thy = Thm.theory_of_cterm ct
+ val {t=t',T=ty,...} = 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 ------------ *)
+
+datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int
+ | Prem of AbstractMachine.term
+datatype theorem = Theorem of theory_ref * unit Unsynchronized.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))
+
+ (* 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 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 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
+
+ val vs = fold compute_inst insts (varsubst_of_theorem th)
+in
+ update_varsubst vs th
+end
+
+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
+ 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 splicein n l L = List.take (L, n) @ l @ List.drop (L, n+1)
+
+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 = Syntax.string_of_term_global Pure.thy
+ (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
+
+fun prem2term (Prem t) = t
+ | prem2term (EqPrem (a,b,_,eq)) =
+ AbstractMachine.App (AbstractMachine.App (AbstractMachine.Const eq, a), b)
+
+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 Theory.subthy (thy1, thy2) then thy2
+ else if Theory.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
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/Compute_Oracle/linker.ML Wed Jul 21 18:13:15 2010 +0200
@@ -0,0 +1,472 @@
+(* Title: Tools/Compute_Oracle/linker.ML
+ Author: Steven Obua
+
+This module solves the problem that the computing oracle does not
+instantiate polymorphic rules. By going through the PCompute
+interface, all possible instantiations are resolved by compiling new
+programs, if necessary. The obvious disadvantage of this approach is
+that in the worst case for each new term to be rewritten, a new
+program may be compiled.
+*)
+
+(*
+ Given constants/frees c_1::t_1, c_2::t_2, ...., c_n::t_n,
+ and constants/frees d_1::d_1, d_2::s_2, ..., d_m::s_m
+
+ Find all substitutions S such that
+ a) the domain of S is tvars (t_1, ..., t_n)
+ b) there are indices i_1, ..., i_k, and j_1, ..., j_k with
+ 1. S (c_i_1::t_i_1) = d_j_1::s_j_1, ..., S (c_i_k::t_i_k) = d_j_k::s_j_k
+ 2. tvars (t_i_1, ..., t_i_k) = tvars (t_1, ..., t_n)
+*)
+signature LINKER =
+sig
+ exception Link of string
+
+ datatype constant = Constant of bool * string * typ
+ val constant_of : term -> constant
+
+ type instances
+ type subst = Type.tyenv
+
+ val empty : constant list -> instances
+ val typ_of_constant : constant -> typ
+ val add_instances : theory -> instances -> constant list -> subst list * instances
+ val substs_of : instances -> subst list
+ val is_polymorphic : constant -> bool
+ val distinct_constants : constant list -> constant list
+ val collect_consts : term list -> constant list
+end
+
+structure Linker : LINKER = struct
+
+exception Link of string;
+
+type subst = Type.tyenv
+
+datatype constant = Constant of bool * string * typ
+fun constant_of (Const (name, ty)) = Constant (false, name, ty)
+ | constant_of (Free (name, ty)) = Constant (true, name, ty)
+ | constant_of _ = raise Link "constant_of"
+
+fun bool_ord (x,y) = if x then (if y then EQUAL else GREATER) else (if y then LESS else EQUAL)
+fun constant_ord (Constant (x1,x2,x3), Constant (y1,y2,y3)) = (prod_ord (prod_ord bool_ord fast_string_ord) Term_Ord.typ_ord) (((x1,x2),x3), ((y1,y2),y3))
+fun constant_modty_ord (Constant (x1,x2,_), Constant (y1,y2,_)) = (prod_ord bool_ord fast_string_ord) ((x1,x2), (y1,y2))
+
+
+structure Consttab = Table(type key = constant val ord = constant_ord);
+structure ConsttabModTy = Table(type key = constant val ord = constant_modty_ord);
+
+fun typ_of_constant (Constant (_, _, ty)) = ty
+
+val empty_subst = (Vartab.empty : Type.tyenv)
+
+fun merge_subst (A:Type.tyenv) (B:Type.tyenv) =
+ SOME (Vartab.fold (fn (v, t) =>
+ fn tab =>
+ (case Vartab.lookup tab v of
+ NONE => Vartab.update (v, t) tab
+ | SOME t' => if t = t' then tab else raise Type.TYPE_MATCH)) A B)
+ handle Type.TYPE_MATCH => NONE
+
+fun subst_ord (A:Type.tyenv, B:Type.tyenv) =
+ (list_ord (prod_ord Term_Ord.fast_indexname_ord (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))) (Vartab.dest A, Vartab.dest B)
+
+structure Substtab = Table(type key = Type.tyenv val ord = subst_ord);
+
+fun substtab_union c = Substtab.fold Substtab.update c
+fun substtab_unions [] = Substtab.empty
+ | substtab_unions [c] = c
+ | substtab_unions (c::cs) = substtab_union c (substtab_unions cs)
+
+datatype instances = Instances of unit ConsttabModTy.table * Type.tyenv Consttab.table Consttab.table * constant list list * unit Substtab.table
+
+fun is_polymorphic (Constant (_, _, ty)) = not (null (Term.add_tvarsT ty []))
+
+fun distinct_constants cs =
+ Consttab.keys (fold (fn c => Consttab.update (c, ())) cs Consttab.empty)
+
+fun empty cs =
+ let
+ val cs = distinct_constants (filter is_polymorphic cs)
+ val old_cs = cs
+(* fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (OldTerm.typ_tvars ty) tab
+ val tvars_count = length (Typtab.keys (fold (fn c => fn tab => collect_tvars (typ_of_constant c) tab) cs Typtab.empty))
+ fun tvars_of ty = collect_tvars ty Typtab.empty
+ val cs = map (fn c => (c, tvars_of (typ_of_constant c))) cs
+
+ fun tyunion A B =
+ Typtab.fold
+ (fn (v,()) => fn tab => Typtab.update (v, case Typtab.lookup tab v of NONE => 1 | SOME n => n+1) tab)
+ A B
+
+ fun is_essential A B =
+ Typtab.fold
+ (fn (v, ()) => fn essential => essential orelse (case Typtab.lookup B v of NONE => raise Link "is_essential" | SOME n => n=1))
+ A false
+
+ fun add_minimal (c', tvs') (tvs, cs) =
+ let
+ val tvs = tyunion tvs' tvs
+ val cs = (c', tvs')::cs
+ in
+ if forall (fn (c',tvs') => is_essential tvs' tvs) cs then
+ SOME (tvs, cs)
+ else
+ NONE
+ end
+
+ fun is_spanning (tvs, _) = (length (Typtab.keys tvs) = tvars_count)
+
+ fun generate_minimal_subsets subsets [] = subsets
+ | generate_minimal_subsets subsets (c::cs) =
+ let
+ val subsets' = map_filter (add_minimal c) subsets
+ in
+ generate_minimal_subsets (subsets@subsets') cs
+ end*)
+
+ val minimal_subsets = [old_cs] (*map (fn (tvs, cs) => map fst cs) (filter is_spanning (generate_minimal_subsets [(Typtab.empty, [])] cs))*)
+
+ val constants = Consttab.keys (fold (fold (fn c => Consttab.update (c, ()))) minimal_subsets Consttab.empty)
+
+ in
+ Instances (
+ fold (fn c => fn tab => ConsttabModTy.update (c, ()) tab) constants ConsttabModTy.empty,
+ Consttab.make (map (fn c => (c, Consttab.empty : Type.tyenv Consttab.table)) constants),
+ minimal_subsets, Substtab.empty)
+ end
+
+local
+fun calc ctab substtab [] = substtab
+ | calc ctab substtab (c::cs) =
+ let
+ val csubsts = map snd (Consttab.dest (the (Consttab.lookup ctab c)))
+ fun merge_substs substtab subst =
+ Substtab.fold (fn (s,_) =>
+ fn tab =>
+ (case merge_subst subst s of NONE => tab | SOME s => Substtab.update (s, ()) tab))
+ substtab Substtab.empty
+ val substtab = substtab_unions (map (merge_substs substtab) csubsts)
+ in
+ calc ctab substtab cs
+ end
+in
+fun calc_substs ctab (cs:constant list) = calc ctab (Substtab.update (empty_subst, ()) Substtab.empty) cs
+end
+
+fun add_instances thy (Instances (cfilter, ctab,minsets,substs)) cs =
+ let
+(* val _ = writeln (makestring ("add_instances: ", length_cs, length cs, length (Consttab.keys ctab)))*)
+ fun calc_instantiations (constant as Constant (free, name, ty)) instantiations =
+ Consttab.fold (fn (constant' as Constant (free', name', ty'), insttab) =>
+ fn instantiations =>
+ if free <> free' orelse name <> name' then
+ instantiations
+ else case Consttab.lookup insttab constant of
+ SOME _ => instantiations
+ | NONE => ((constant', (constant, Sign.typ_match thy (ty', ty) empty_subst))::instantiations
+ handle TYPE_MATCH => instantiations))
+ ctab instantiations
+ val instantiations = fold calc_instantiations cs []
+ (*val _ = writeln ("instantiations = "^(makestring (length instantiations)))*)
+ fun update_ctab (constant', entry) ctab =
+ (case Consttab.lookup ctab constant' of
+ NONE => raise Link "internal error: update_ctab"
+ | SOME tab => Consttab.update (constant', Consttab.update entry tab) ctab)
+ val ctab = fold update_ctab instantiations ctab
+ val new_substs = fold (fn minset => fn substs => substtab_union (calc_substs ctab minset) substs)
+ minsets Substtab.empty
+ val (added_substs, substs) =
+ Substtab.fold (fn (ns, _) =>
+ fn (added, substtab) =>
+ (case Substtab.lookup substs ns of
+ NONE => (ns::added, Substtab.update (ns, ()) substtab)
+ | SOME () => (added, substtab)))
+ new_substs ([], substs)
+ in
+ (added_substs, Instances (cfilter, ctab, minsets, substs))
+ end
+
+fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
+
+fun eq_to_meta th = (@{thm HOL.eq_reflection} OF [th] handle THM _ => th)
+
+
+local
+
+fun collect (Var x) tab = tab
+ | collect (Bound _) tab = tab
+ | collect (a $ b) tab = collect b (collect a tab)
+ | collect (Abs (_, _, body)) tab = collect body tab
+ | collect t tab = Consttab.update (constant_of t, ()) tab
+
+in
+ fun collect_consts tms = Consttab.keys (fold collect tms Consttab.empty)
+end
+
+end
+
+signature PCOMPUTE =
+sig
+ type pcomputer
+
+ val make : Compute.machine -> theory -> thm list -> Linker.constant list -> pcomputer
+ val make_with_cache : Compute.machine -> theory -> term list -> thm list -> Linker.constant list -> pcomputer
+
+ 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
+
+structure PCompute : PCOMPUTE = struct
+
+exception PCompute of string
+
+datatype theorem = MonoThm of thm | PolyThm of thm * Linker.instances * thm list
+datatype pattern = MonoPattern of term | PolyPattern of term * Linker.instances * term list
+
+datatype pcomputer =
+ PComputer of theory_ref * Compute.computer * theorem list Unsynchronized.ref *
+ pattern list Unsynchronized.ref
+
+(*fun collect_consts (Var x) = []
+ | collect_consts (Bound _) = []
+ | collect_consts (a $ b) = (collect_consts a)@(collect_consts b)
+ | collect_consts (Abs (_, _, body)) = collect_consts body
+ | collect_consts t = [Linker.constant_of t]*)
+
+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)
+ val (left, right) = Logic.dest_equals th
+ in
+ (Linker.collect_consts [left], Linker.collect_consts (right::prems))
+ end
+
+fun create_theorem th =
+let
+ val (left, right) = collect_consts_of_thm th
+ val polycs = filter Linker.is_polymorphic left
+ val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (OldTerm.typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty
+ fun check_const (c::cs) cs' =
+ let
+ val tvars = OldTerm.typ_tvars (Linker.typ_of_constant c)
+ val wrong = fold (fn n => fn wrong => wrong orelse is_none (Typtab.lookup tytab (TVar n))) tvars false
+ in
+ if wrong then raise PCompute "right hand side of theorem contains type variables which do not occur on the left hand side"
+ else
+ if null (tvars) then
+ check_const cs (c::cs')
+ else
+ check_const cs cs'
+ end
+ | check_const [] cs' = cs'
+ val monocs = check_const right []
+in
+ if null (polycs) then
+ (monocs, MonoThm th)
+ else
+ (monocs, PolyThm (th, Linker.empty polycs, []))
+end
+
+fun create_pattern pat =
+let
+ val cs = Linker.collect_consts [pat]
+ val polycs = filter Linker.is_polymorphic cs
+in
+ if null (polycs) then
+ MonoPattern pat
+ else
+ PolyPattern (pat, Linker.empty polycs, [])
+end
+
+fun create_computer machine thy pats ths =
+ let
+ fun add (MonoThm th) ths = th::ths
+ | add (PolyThm (_, _, ths')) ths = ths'@ths
+ fun addpat (MonoPattern p) pats = p::pats
+ | addpat (PolyPattern (_, _, ps)) pats = ps@pats
+ val ths = fold_rev add ths []
+ val pats = fold_rev addpat pats []
+ in
+ Compute.make_with_cache machine thy pats ths
+ end
+
+fun update_computer computer pats ths =
+ let
+ fun add (MonoThm th) ths = th::ths
+ | add (PolyThm (_, _, ths')) ths = ths'@ths
+ fun addpat (MonoPattern p) pats = p::pats
+ | addpat (PolyPattern (_, _, ps)) pats = ps@pats
+ val ths = fold_rev add ths []
+ val pats = fold_rev addpat pats []
+ in
+ Compute.update_with_cache computer pats 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)
+
+fun add_monos thy monocs pats ths =
+ let
+ val changed = Unsynchronized.ref false
+ fun add monocs (th as (MonoThm _)) = ([], th)
+ | add monocs (PolyThm (th, instances, instanceths)) =
+ let
+ val (newsubsts, instances) = Linker.add_instances thy instances monocs
+ val _ = if not (null newsubsts) then changed := true else ()
+ val newths = map (fn subst => Thm.instantiate (conv_subst thy subst, []) th) newsubsts
+(* val _ = if not (null newths) then (print ("added new theorems: ", newths); ()) else ()*)
+ val newmonos = fold (fn th => fn monos => (snd (collect_consts_of_thm th))@monos) newths []
+ in
+ (newmonos, PolyThm (th, instances, instanceths@newths))
+ end
+ fun addpats monocs (pat as (MonoPattern _)) = pat
+ | addpats monocs (PolyPattern (p, instances, instancepats)) =
+ let
+ val (newsubsts, instances) = Linker.add_instances thy instances monocs
+ val _ = if not (null newsubsts) then changed := true else ()
+ val newpats = map (fn subst => Envir.subst_term_types subst p) newsubsts
+ in
+ PolyPattern (p, instances, instancepats@newpats)
+ end
+ fun step monocs ths =
+ fold_rev (fn th =>
+ fn (newmonos, ths) =>
+ let
+ val (newmonos', th') = add monocs th
+ in
+ (newmonos'@newmonos, th'::ths)
+ end)
+ ths ([], [])
+ fun loop monocs pats ths =
+ let
+ val (monocs', ths') = step monocs ths
+ val pats' = map (addpats monocs) pats
+ in
+ if null (monocs') then
+ (pats', ths')
+ else
+ loop monocs' pats' ths'
+ end
+ val result = loop monocs pats ths
+ in
+ (!changed, result)
+ end
+
+datatype cthm = ComputeThm of term list * sort list * term
+
+fun thm2cthm th =
+ let
+ val {hyps, prop, shyps, ...} = Thm.rep_thm th
+ in
+ ComputeThm (hyps, shyps, prop)
+ end
+
+val cthm_ord' = prod_ord (prod_ord (list_ord Term_Ord.term_ord) (list_ord Term_Ord.sort_ord)) Term_Ord.term_ord
+
+fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
+
+structure CThmtab = Table(type key = cthm val ord = cthm_ord)
+
+fun remove_duplicates ths =
+ let
+ val counter = Unsynchronized.ref 0
+ val tab = Unsynchronized.ref (CThmtab.empty : unit CThmtab.table)
+ val thstab = Unsynchronized.ref (Inttab.empty : thm Inttab.table)
+ fun update th =
+ let
+ val key = thm2cthm th
+ in
+ case CThmtab.lookup (!tab) key of
+ NONE => ((tab := CThmtab.update_new (key, ()) (!tab)); thstab := Inttab.update_new (!counter, th) (!thstab); counter := !counter + 1)
+ | _ => ()
+ end
+ val _ = map update ths
+ in
+ map snd (Inttab.dest (!thstab))
+ end
+
+fun make_with_cache machine thy pats 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 pats = map create_pattern pats
+ val (_, (pats, ths)) = add_monos thy monocs pats ths
+ val computer = create_computer machine thy pats ths
+ in
+ PComputer (Theory.check_thy thy, computer, Unsynchronized.ref ths, Unsynchronized.ref pats)
+ end
+
+fun make machine thy ths cs = make_with_cache machine thy [] ths cs
+
+fun add_instances (PComputer (thyref, computer, rths, rpats)) cs =
+ let
+ val thy = Theory.deref thyref
+ val (changed, (pats, ths)) = add_monos thy cs (!rpats) (!rths)
+ in
+ if changed then
+ (update_computer computer pats ths;
+ rths := ths;
+ rpats := pats;
+ 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 simplify pc th = Compute.simplify (computer_of pc) th
+
+fun make_theorem pc th vars =
+ let
+ val _ = add_instances' pc [prop_of th]
+
+ in
+ 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/Compute_Oracle/report.ML Wed Jul 21 18:13:15 2010 +0200
@@ -0,0 +1,33 @@
+structure Report =
+struct
+
+local
+
+ val report_depth = Unsynchronized.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 = #message (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
--- a/src/HOL/Mutabelle/mutabelle.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML Wed Jul 21 18:13:15 2010 +0200
@@ -82,7 +82,7 @@
(*helper function in order to properly print a term*)
-fun prt x = Pretty.writeln (Syntax.pretty_term_global (theory "Main") x);
+fun prt x = Pretty.writeln (Syntax.pretty_term_global @{theory Main} x);
(*possibility to print a given term for debugging purposes*)
@@ -460,7 +460,7 @@
(*mutate origTerm iter times by only exchanging subterms*)
fun mutate_exc origTerm commutatives iter =
- mutate 0 origTerm (theory "Main") commutatives [] iter;
+ mutate 0 origTerm @{theory Main} commutatives [] iter;
(*mutate origTerm iter times by only inserting signature functions*)
--- a/src/HOL/Tools/inductive.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Jul 21 18:13:15 2010 +0200
@@ -414,7 +414,7 @@
(* prove simplification equations *)
-fun prove_eqs quiet_mode cs params intr_ts intrs elims ctxt ctxt'' =
+fun prove_eqs quiet_mode cs params intr_ts intrs (elims: (thm * bstring list * int) list) ctxt ctxt'' =
let
val _ = clean_message quiet_mode " Proving the simplification rules ...";
@@ -422,7 +422,7 @@
(the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))),
Logic.strip_assums_hyp r, Logic.strip_params r);
val intr_ts' = map dest_intr intr_ts;
- fun prove_eq c elim =
+ fun prove_eq c (elim: thm * 'a * 'b) =
let
val Ts = arg_types_of (length params) c;
val (anames, ctxt') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt;
--- a/src/HOL/Tools/inductive_set.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/HOL/Tools/inductive_set.ML Wed Jul 21 18:13:15 2010 +0200
@@ -32,7 +32,7 @@
(**** simplify {(x1, ..., xn). (x1, ..., xn) : S} to S ****)
val collect_mem_simproc =
- Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
+ Simplifier.simproc @{theory Set} "Collect_mem" ["Collect t"] (fn thy => fn ss =>
fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
let val (u, _, ps) = HOLogic.strip_psplits t
in case u of
--- a/src/HOL/Typedef.thy Wed Jul 21 18:11:51 2010 +0200
+++ b/src/HOL/Typedef.thy Wed Jul 21 18:13:15 2010 +0200
@@ -13,7 +13,7 @@
begin
ML {*
-structure HOL = struct val thy = theory "HOL" end;
+structure HOL = struct val thy = @{theory HOL} end;
*} -- "belongs to theory HOL"
locale type_definition =
--- a/src/Pure/Concurrent/future.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/Concurrent/future.ML Wed Jul 21 18:13:15 2010 +0200
@@ -36,6 +36,7 @@
val is_worker: unit -> bool
val worker_task: unit -> Task_Queue.task option
val worker_group: unit -> Task_Queue.group option
+ val worker_subgroup: unit -> Task_Queue.group
type 'a future
val task_of: 'a future -> task
val group_of: 'a future -> group
@@ -83,8 +84,7 @@
val is_worker = is_some o thread_data;
val worker_task = Option.map #1 o thread_data;
val worker_group = Option.map #2 o thread_data;
-
-fun new_group () = Task_Queue.new_group (worker_group ());
+fun worker_subgroup () = Task_Queue.new_group (worker_group ());
(* datatype future *)
@@ -106,9 +106,13 @@
fun assign_result group result res =
let
- val _ = Single_Assignment.assign result res;
+ val _ = Single_Assignment.assign result res
+ handle exn as Fail _ =>
+ (case Single_Assignment.peek result of
+ SOME (Exn.Exn Exn.Interrupt) => raise Exn.Interrupt
+ | _ => reraise exn);
val ok =
- (case res of
+ (case the (Single_Assignment.peek result) of
Exn.Exn exn => (Task_Queue.cancel_group group exn; false)
| Exn.Result _ => true);
in ok end;
@@ -384,7 +388,7 @@
let
val group =
(case opt_group of
- NONE => new_group ()
+ NONE => worker_subgroup ()
| SOME group => group);
val (result, job) = future_job group e;
val task = SYNCHRONIZED "enqueue" (fn () =>
@@ -409,7 +413,7 @@
fun get_result x =
(case peek x of
- NONE => Exn.Exn (SYS_ERROR "unfinished future")
+ NONE => Exn.Exn (Fail "Unfinished future")
| SOME (exn as Exn.Exn Exn.Interrupt) =>
(case Exn.flatten_list (Task_Queue.group_status (group_of x)) of
[] => exn
@@ -481,11 +485,12 @@
fun promise_group group : 'a future =
let
val result = Single_Assignment.var "promise" : 'a result;
- val task = SYNCHRONIZED "enqueue" (fn () =>
- Unsynchronized.change_result queue (Task_Queue.enqueue_passive group));
+ fun abort () = assign_result group result (Exn.Exn Exn.Interrupt) handle Fail _ => true;
+ val task = SYNCHRONIZED "enqueue_passive" (fn () =>
+ Unsynchronized.change_result queue (Task_Queue.enqueue_passive group abort));
in Future {promised = true, task = task, group = group, result = result} end;
-fun promise () = promise_group (new_group ());
+fun promise () = promise_group (worker_subgroup ());
fun fulfill_result (Future {promised, task, group, result}) res =
let
@@ -509,8 +514,10 @@
else interruptible f x;
(*cancel: present and future group members will be interrupted eventually*)
-fun cancel_group group =
- SYNCHRONIZED "cancel" (fn () => if cancel_now group then () else cancel_later group);
+fun cancel_group group = SYNCHRONIZED "cancel" (fn () =>
+ (if cancel_now group then () else cancel_later group;
+ signal work_available; scheduler_check ()));
+
fun cancel x = cancel_group (group_of x);
--- a/src/Pure/Concurrent/par_list.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/Concurrent/par_list.ML Wed Jul 21 18:13:15 2010 +0200
@@ -28,8 +28,8 @@
fun raw_map f xs =
if Multithreading.enabled () andalso not (Multithreading.self_critical ()) then
- let val group = Task_Queue.new_group (Future.worker_group ())
- in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end
+ let val shared_group = Task_Queue.new_group (Future.worker_group ())
+ in Future.join_results (map (fn x => Future.fork_group shared_group (fn () => f x)) xs) end
else map (Exn.capture f) xs;
fun map f xs = Exn.release_first (raw_map f xs);
--- a/src/Pure/Concurrent/task_queue.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Wed Jul 21 18:13:15 2010 +0200
@@ -24,7 +24,7 @@
val status: queue -> {ready: int, pending: int, running: int, passive: int}
val cancel: queue -> group -> bool
val cancel_all: queue -> group list
- val enqueue_passive: group -> queue -> task * queue
+ val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> (task * bool) * queue
val extend: task -> (bool -> bool) -> queue -> queue option
val dequeue: Thread.thread -> queue -> (task * group * (bool -> bool) list) option * queue
@@ -88,8 +88,6 @@
not (null (Synchronized.value status)) orelse
(case parent of NONE => false | SOME group => is_canceled group);
-fun is_ready deps group = null deps orelse is_canceled group;
-
fun group_status (Group {parent, status, ...}) =
Synchronized.value status @
(case parent of NONE => [] | SOME group => group_status group);
@@ -105,7 +103,7 @@
datatype job =
Job of (bool -> bool) list |
Running of Thread.thread |
- Passive;
+ Passive of unit -> bool;
type jobs = (group * job) Task_Graph.T;
@@ -135,9 +133,21 @@
val empty = make_queue Inttab.empty Task_Graph.empty;
+
+(* job status *)
+
+fun ready_job task ((group, Job list), ([], _)) = SOME (task, group, rev list)
+ | ready_job task ((group, Passive abort), ([], _)) =
+ if is_canceled group then SOME (task, group, [fn _ => abort ()])
+ else NONE
+ | ready_job _ _ = NONE;
+
+fun active_job (_, Job _) = SOME ()
+ | active_job (_, Running _) = SOME ()
+ | active_job (group, Passive _) = if is_canceled group then SOME () else NONE;
+
fun all_passive (Queue {jobs, ...}) =
- Task_Graph.get_first
- ((fn Job _ => SOME () | Running _ => SOME () | Passive => NONE) o #2 o #1 o #2) jobs |> is_none;
+ is_none (Task_Graph.get_first (active_job o #1 o #2) jobs);
(* queue status *)
@@ -145,11 +155,11 @@
fun status (Queue {jobs, ...}) =
let
val (x, y, z, w) =
- Task_Graph.fold (fn (_, ((group, job), (deps, _))) => fn (x, y, z, w) =>
+ Task_Graph.fold (fn (_, ((_, job), (deps, _))) => fn (x, y, z, w) =>
(case job of
- Job _ => if is_ready deps group then (x + 1, y, z, w) else (x, y + 1, z, w)
+ Job _ => if null deps then (x + 1, y, z, w) else (x, y + 1, z, w)
| Running _ => (x, y, z + 1, w)
- | Passive => (x, y, z, w + 1)))
+ | Passive _ => (x, y, z, w + 1)))
jobs (0, 0, 0, 0);
in {ready = x, pending = y, running = z, passive = w} end;
@@ -165,7 +175,7 @@
val _ = List.app Simple_Thread.interrupt running;
in null running end;
-fun cancel_all (Queue {groups, jobs}) =
+fun cancel_all (Queue {jobs, ...}) =
let
fun cancel_job (group, job) (groups, running) =
(cancel_group group Exn.Interrupt;
@@ -179,12 +189,12 @@
(* enqueue *)
-fun enqueue_passive group (Queue {groups, jobs}) =
+fun enqueue_passive group abort (Queue {groups, jobs}) =
let
val task = new_task NONE;
val groups' = groups
|> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group);
- val jobs' = jobs |> Task_Graph.new_node (task, (group, Passive));
+ val jobs' = jobs |> Task_Graph.new_node (task, (group, Passive abort));
in (task, make_queue groups' jobs') end;
fun enqueue group deps pri job (Queue {groups, jobs}) =
@@ -208,17 +218,11 @@
(* dequeue *)
fun dequeue thread (queue as Queue {groups, jobs}) =
- let
- fun ready (task, ((group, Job list), (deps, _))) =
- if is_ready deps group then SOME (task, group, rev list) else NONE
- | ready _ = NONE;
- in
- (case Task_Graph.get_first ready jobs of
- NONE => (NONE, queue)
- | SOME (result as (task, _, _)) =>
- let val jobs' = set_job task (Running thread) jobs
- in (SOME result, make_queue groups jobs') end)
- end;
+ (case Task_Graph.get_first (uncurry ready_job) jobs of
+ NONE => (NONE, queue)
+ | SOME (result as (task, _, _)) =>
+ let val jobs' = set_job task (Running thread) jobs
+ in (SOME result, make_queue groups jobs') end);
(* dequeue_towards -- adhoc dependencies *)
@@ -228,13 +232,7 @@
fun dequeue_towards thread deps (queue as Queue {groups, jobs}) =
let
- fun ready task =
- (case Task_Graph.get_node jobs task of
- (group, Job list) =>
- if is_ready (get_deps jobs task) group
- then SOME (task, group, rev list)
- else NONE
- | _ => NONE);
+ fun ready task = ready_job task (Task_Graph.get_entry jobs task);
val tasks = filter (can (Task_Graph.get_node jobs)) deps;
fun result (res as (task, _, _)) =
let val jobs' = set_job task (Running thread) jobs
--- a/src/Pure/General/graph.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/General/graph.ML Wed Jul 21 18:13:15 2010 +0200
@@ -20,6 +20,7 @@
val minimals: 'a T -> key list
val maximals: 'a T -> key list
val subgraph: (key -> bool) -> 'a T -> 'a T
+ val get_entry: 'a T -> key -> 'a * (key list * key list) (*exception UNDEF*)
val map_nodes: ('a -> 'b) -> 'a T -> 'b T
val get_node: 'a T -> key -> 'a (*exception UNDEF*)
val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
--- a/src/Pure/Isar/isar_cmd.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Wed Jul 21 18:13:15 2010 +0200
@@ -408,14 +408,16 @@
val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
let
val thy = Toplevel.theory_of state;
+ val thy_session = Present.session_name thy;
+
val all_thys = sort Thy_Info.thy_ord (thy :: Theory.ancestors_of thy);
val gr = all_thys |> map (fn node =>
let
val name = Context.theory_name node;
val parents = map Context.theory_name (Theory.parents_of node);
- val dir = Present.session_name node;
- val unfold = not (Thy_Info.known_thy name andalso Thy_Info.is_finished name);
- in {name = name, ID = name, parents = parents, dir = dir, unfold = unfold, path = ""} end);
+ val session = Present.session_name node;
+ val unfold = (session = thy_session);
+ in {name = name, ID = name, parents = parents, dir = session, unfold = unfold, path = ""} end);
in Present.display_graph gr end);
val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
@@ -432,7 +434,8 @@
in Present.display_graph gr end);
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
- Thm_Deps.thm_deps (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
+ Thm_Deps.thm_deps (Toplevel.theory_of state)
+ (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
(* find unused theorems *)
@@ -442,12 +445,13 @@
val thy = Toplevel.theory_of state;
val ctxt = Toplevel.context_of state;
fun pretty_thm (a, th) = ProofContext.pretty_fact ctxt (a, [th]);
+ val get_theory = Context.get_theory thy;
in
Thm_Deps.unused_thms
(case opt_range of
NONE => (Theory.parents_of thy, [thy])
- | SOME (xs, NONE) => (map Thy_Info.get_theory xs, [thy])
- | SOME (xs, SOME ys) => (map Thy_Info.get_theory xs, map Thy_Info.get_theory ys))
+ | SOME (xs, NONE) => (map get_theory xs, [thy])
+ | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
|> map pretty_thm |> Pretty.chunks |> Pretty.writeln
end);
--- a/src/Pure/Isar/isar_document.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML Wed Jul 21 18:13:15 2010 +0200
@@ -241,8 +241,8 @@
let
val old_execution = ! execution;
val _ = Future.cancel old_execution;
- val new_execution = Future.fork (fn () =>
- (Future.join_result old_execution;
+ val new_execution = Future.fork_pri 1 (fn () =>
+ (uninterruptible (K Future.join_result) old_execution;
fold_entries no_id (fn (_, {state, ...}) => fn () => force_state state) document ()));
in execution := new_execution end);
--- a/src/Pure/Isar/isar_syn.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Jul 21 18:13:15 2010 +0200
@@ -184,9 +184,9 @@
val _ =
Outer_Syntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
(Scan.repeat1 Parse_Spec.spec >>
- (Toplevel.theory o
- (Isar_Cmd.add_axioms o
- tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"))));
+ (fn spec => Toplevel.theory (fn thy =>
+ (legacy_feature "Old 'axioms' command -- use 'axiomatization' instead";
+ Isar_Cmd.add_axioms spec thy))));
val opt_unchecked_overloaded =
Scan.optional (Parse.$$$ "(" |-- Parse.!!!
@@ -314,7 +314,7 @@
val _ =
Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
(Parse.path >>
- (fn path => Toplevel.generic_theory (Thy_Info.exec_file false path #> propagate_env)));
+ (fn path => Toplevel.generic_theory (Thy_Info.exec_file path #> propagate_env)));
val _ =
Outer_Syntax.command "ML" "ML text within theory or local theory"
--- a/src/Pure/Isar/outer_syntax.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Wed Jul 21 18:13:15 2010 +0200
@@ -31,7 +31,7 @@
type isar
val isar: bool -> isar
val prepare_command: Position.T -> string -> Toplevel.transition
- val load_thy: string -> Position.T -> string list -> bool -> unit -> unit
+ val load_thy: string -> Position.T -> string list -> unit -> unit
end;
structure Outer_Syntax: OUTER_SYNTAX =
@@ -62,7 +62,7 @@
(case cmd name of
SOME (Command {int_only, parse, ...}) =>
Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
- | NONE => sys_error ("no parser for outer syntax command " ^ quote name));
+ | NONE => raise Fail ("No parser for outer syntax command " ^ quote name));
in
@@ -268,9 +268,10 @@
(* load_thy *)
-fun load_thy name pos text time =
+fun load_thy name pos text =
let
val (lexs, commands) = get_syntax ();
+ val time = ! Output.timing;
val _ = Present.init_theory name;
--- a/src/Pure/Isar/toplevel.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Jul 21 18:13:15 2010 +0200
@@ -24,6 +24,7 @@
val enter_proof_body: state -> Proof.state
val print_state_context: state -> unit
val print_state: bool -> state -> unit
+ val pretty_abstract: state -> Pretty.T
val quiet: bool Unsynchronized.ref
val debug: bool Unsynchronized.ref
val interact: bool Unsynchronized.ref
@@ -212,6 +213,8 @@
| SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)])
|> Pretty.markup_chunks Markup.state |> Pretty.writeln;
+fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
+
(** toplevel transitions **)
@@ -564,8 +567,7 @@
fun async_state (tr as Transition {print, ...}) st =
if print then
ignore
- (Future.fork_group (Task_Queue.new_group (Future.worker_group ()))
- (fn () =>
+ (Future.fork (fn () =>
setmp_thread_position tr (fn () => Future.report (fn () => print_state false st)) ()))
else ();
@@ -630,11 +632,14 @@
SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
| NONE => Exn.Result ()) of
Exn.Result () =>
- (case transition false tr st of
- SOME (st', NONE) => (status tr Markup.finished; async_state tr st'; SOME st')
- | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
- | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
- | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
+ let val int = is_some (init_of tr) in
+ (case transition int tr st of
+ SOME (st', NONE) =>
+ (status tr Markup.finished; if int then () else async_state tr st'; SOME st')
+ | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
+ | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
+ | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
+ end
| Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
@@ -699,7 +704,7 @@
val states =
(case States.get (presentation_context_of st'') of
- NONE => sys_error ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
+ NONE => raise Fail ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
| SOME states => states);
val result = Lazy.lazy
(fn () => (tr, st') :: (body_trs ~~ Future.join states) @ [(end_tr, st'')]);
--- a/src/Pure/ML/ml_antiquote.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Wed Jul 21 18:13:15 2010 +0200
@@ -64,12 +64,14 @@
>> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
val _ = value "theory"
- (Scan.lift Args.name >> (fn name => "Thy_Info.get_theory " ^ ML_Syntax.print_string name)
+ (Scan.lift Args.name >> (fn name =>
+ "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
|| Scan.succeed "ML_Context.the_global_context ()");
val _ = value "theory_ref"
(Scan.lift Args.name >> (fn name =>
- "Theory.check_thy (Thy_Info.theory " ^ ML_Syntax.print_string name ^ ")")
+ "Theory.check_thy (Context.get_theory (ML_Context.the_global_context ()) " ^
+ ML_Syntax.print_string name ^ ")")
|| Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
--- a/src/Pure/PIDE/document.scala Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/PIDE/document.scala Wed Jul 21 18:13:15 2010 +0200
@@ -162,6 +162,12 @@
if (range.hasNext) Some(range.next) else None
}
+ def proper_command_at(i: Int): Option[Command] =
+ command_at(i) match {
+ case Some((command, _)) => commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
+ case None => None
+ }
+
/* command state assignment */
--- a/src/Pure/ProofGeneral/pgip_parser.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML Wed Jul 21 18:13:15 2010 +0200
@@ -78,7 +78,7 @@
|> command Keyword.prf_script proofstep;
val _ = subset (op =) (Keyword.kinds, Symtab.keys command_keywords)
- orelse sys_error "Incomplete coverage of command keywords";
+ orelse raise Fail "Incomplete coverage of command keywords";
fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
| parse_command name text =
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Jul 21 18:13:15 2010 +0200
@@ -505,7 +505,7 @@
isarcmd ("undos_proof " ^ Int.toString times)
end
-fun redostep _ = sys_error "redo unavailable"
+fun redostep _ = raise Fail "redo unavailable"
fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
--- a/src/Pure/Syntax/parser.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/Syntax/parser.ML Wed Jul 21 18:13:15 2010 +0200
@@ -828,7 +828,7 @@
| SOME (Lexicon.Token (_, _, (_, end_pos))) => end_pos);
val r =
(case earley prods tags chains start (toks @ [Lexicon.mk_eof end_pos]) of
- [] => raise Fail "no parse trees"
+ [] => raise Fail "Inner syntax: no parse trees"
| pts => pts);
in r end;
--- a/src/Pure/Syntax/printer.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/Syntax/printer.ML Wed Jul 21 18:13:15 2010 +0200
@@ -80,7 +80,7 @@
Ast.mk_appl (simple_ast_of f) (map simple_ast_of args)
end
| simple_ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
- | simple_ast_of (Abs _) = sys_error "simple_ast_of: Abs";
+ | simple_ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
@@ -246,7 +246,7 @@
in
(case xsyms_to_syms xsymbs of
(symbs, []) => SOME (const, (symbs, nargs symbs, pri))
- | _ => sys_error "xprod_to_fmt: unbalanced blocks")
+ | _ => raise Fail "Unbalanced pretty-printing blocks")
end;
--- a/src/Pure/System/session.scala Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/System/session.scala Wed Jul 21 18:13:15 2010 +0200
@@ -16,6 +16,7 @@
/* events */
case object Global_Settings
+ case object Perspective
/* managed entities */
@@ -32,12 +33,25 @@
class Session(system: Isabelle_System)
{
+ /* real time parameters */ // FIXME properties or settings (!?)
+
+ // user input (e.g. text edits, cursor movement)
+ val input_delay = 300
+
+ // prover output (markup, common messages)
+ val output_delay = 100
+
+ // GUI layout updates
+ val update_delay = 500
+
+
/* pervasive event buses */
val global_settings = new Event_Bus[Session.Global_Settings.type]
val raw_results = new Event_Bus[Isabelle_Process.Result]
val raw_output = new Event_Bus[Isabelle_Process.Result]
val commands_changed = new Event_Bus[Command_Set]
+ val perspective = new Event_Bus[Session.Perspective.type]
/* unique ids */
@@ -263,7 +277,7 @@
{
val now = currentTime
flush_time match {
- case None => flush_time = Some(now + 100) // FIXME output_delay property
+ case None => flush_time = Some(now + output_delay)
case Some(time) => if (now >= time) flush()
}
}
--- a/src/Pure/Thy/thm_deps.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/Thy/thm_deps.ML Wed Jul 21 18:13:15 2010 +0200
@@ -6,7 +6,7 @@
signature THM_DEPS =
sig
- val thm_deps: thm list -> unit
+ val thm_deps: theory -> thm list -> unit
val unused_thms: theory list * theory list -> (string * thm) list
end;
@@ -15,7 +15,7 @@
(* thm_deps *)
-fun thm_deps thms =
+fun thm_deps thy thms =
let
fun add_dep ("", _, _) = I
| add_dep (name, _, PBody {thms = thms', ...}) =
@@ -24,7 +24,7 @@
val session =
(case prefix of
a :: _ =>
- (case Thy_Info.lookup_theory a of
+ (case try (Context.get_theory thy) a of
SOME thy =>
(case Present.session_name thy of
"" => []
--- a/src/Pure/Thy/thy_info.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML Wed Jul 21 18:13:15 2010 +0200
@@ -16,7 +16,6 @@
val if_known_thy: (string -> unit) -> string -> unit
val lookup_theory: string -> theory option
val get_theory: string -> theory
- val the_theory: string -> theory -> theory
val is_finished: string -> bool
val master_directory: string -> Path.T
val loaded_files: string -> Path.T list
@@ -27,13 +26,11 @@
val remove_thy: string -> unit
val kill_thy: string -> unit
val provide_file: Path.T -> string -> unit
- val load_file: bool -> Path.T -> unit
- val exec_file: bool -> Path.T -> Context.generic -> Context.generic
+ val load_file: Path.T -> unit
+ val exec_file: Path.T -> Context.generic -> Context.generic
val use: string -> unit
- val time_use: string -> unit
val use_thys: string list -> unit
val use_thy: string -> unit
- val time_use_thy: string -> unit
val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
val end_theory: theory -> unit
val register_thy: string -> unit
@@ -176,10 +173,6 @@
SOME theory => theory
| _ => error (loader_msg "undefined theory entry for" [name]));
-fun the_theory name thy =
- if Context.theory_name thy = name then thy
- else get_theory name;
-
(** thy operations **)
@@ -311,8 +304,8 @@
| NONE => error ("Could not find file " ^ quote (Path.implode path)))
end;
-fun load_file time path =
- if time then
+fun load_file path =
+ if ! Output.timing then
let val name = Path.implode path in
timeit (fn () =>
(priority ("\n**** Starting file " ^ quote name ^ " ****");
@@ -321,10 +314,9 @@
end
else run_file path;
-fun exec_file time path = ML_Context.exec (fn () => load_file time path);
+fun exec_file path = ML_Context.exec (fn () => load_file path);
-val use = load_file false o Path.explode;
-val time_use = load_file true o Path.explode;
+val use = load_file o Path.explode;
end;
@@ -334,7 +326,7 @@
fun required_by _ [] = ""
| required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
-fun load_thy time upd_time initiators name =
+fun load_thy upd_time initiators name =
let
val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
val (pos, text, _) =
@@ -346,7 +338,7 @@
val _ = CRITICAL (fn () =>
change_deps name (Option.map (fn {master, text, parents, files, ...} =>
make_deps upd_time master text parents files)));
- val after_load = Outer_Syntax.load_thy name pos text (time orelse ! Output.timing);
+ val after_load = Outer_Syntax.load_thy name pos text;
val _ =
CRITICAL (fn () =>
(change_deps name
@@ -463,9 +455,9 @@
in
-fun require_thys time initiators dir strs tasks =
- fold_map (require_thy time initiators dir) strs tasks |>> forall I
-and require_thy time initiators dir str tasks =
+fun require_thys initiators dir strs tasks =
+ fold_map (require_thy initiators dir) strs tasks |>> forall I
+and require_thy initiators dir str tasks =
let
val path = Path.expand (Path.explode str);
val name = Path.implode (Path.base path);
@@ -483,8 +475,7 @@
val parent_names = map base_name parents;
val (parents_current, tasks_graph') =
- require_thys time (name :: initiators)
- (Path.append dir (master_dir' deps)) parents tasks;
+ require_thys (name :: initiators) (Path.append dir (master_dir' deps)) parents tasks;
val all_current = current andalso parents_current;
val _ = if not all_current andalso known_thy name then outdate_thy name else ();
@@ -496,7 +487,7 @@
val upd_time = serial ();
val tasks_graph'' = tasks_graph' |> new_deps name parent_names
(if all_current then Finished
- else Task (fn () => load_thy time upd_time initiators name));
+ else Task (fn () => load_thy upd_time initiators name));
in (all_current, tasks_graph'') end)
end;
@@ -505,25 +496,16 @@
(* use_thy etc. *)
-local
+fun use_thys_dir dir arg =
+ schedule_tasks (snd (require_thys [] dir arg Graph.empty));
-fun gen_use_thy' req dir arg =
- schedule_tasks (snd (req [] dir arg Graph.empty));
+val use_thys = use_thys_dir Path.current;
-fun gen_use_thy req str =
- let val name = base_name str in
- check_unfinished warning name;
- gen_use_thy' req Path.current str
- end;
-
-in
-
-val use_thys_dir = gen_use_thy' (require_thys false);
-val use_thys = use_thys_dir Path.current;
-val use_thy = gen_use_thy (require_thy false);
-val time_use_thy = gen_use_thy (require_thy true);
-
-end;
+fun use_thy str =
+ let
+ val name = base_name str;
+ val _ = check_unfinished warning name;
+ in use_thys [str] end;
(* begin / end theory *)
@@ -550,7 +532,7 @@
val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
val theory'' =
- fold (fn x => Context.theory_map (exec_file false x) o Theory.checkpoint) uses_now theory';
+ fold (fn x => Context.theory_map (exec_file x) o Theory.checkpoint) uses_now theory';
in theory'' end;
fun end_theory theory =
--- a/src/Pure/context.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/context.ML Wed Jul 21 18:13:15 2010 +0200
@@ -40,6 +40,8 @@
val string_of_thy: theory -> string
val pretty_abbrev_thy: theory -> Pretty.T
val str_of_thy: theory -> string
+ val get_theory: theory -> string -> theory
+ val this_theory: theory -> string -> theory
val deref: theory_ref -> theory
val check_thy: theory -> theory_ref
val eq_thy: theory * theory -> bool
@@ -120,7 +122,7 @@
fun invoke f k =
(case Datatab.lookup (! kinds) k of
SOME kind => f kind
- | NONE => sys_error "Invalid theory data identifier");
+ | NONE => raise Fail "Invalid theory data identifier");
in
@@ -244,6 +246,18 @@
val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
+fun get_theory thy name =
+ if theory_name thy <> name then
+ (case find_first (fn thy' => theory_name thy' = name) (ancestors_of thy) of
+ SOME thy' => thy'
+ | NONE => error ("Unknown ancestor theory " ^ quote name))
+ else if #stage (history_of thy) = finished then thy
+ else error ("Unfinished theory " ^ quote name);
+
+fun this_theory thy name =
+ if theory_name thy = name then thy
+ else get_theory thy name;
+
(* theory references *)
@@ -459,7 +473,7 @@
fun invoke_init k =
(case Datatab.lookup (! kinds) k of
SOME init => init
- | NONE => sys_error "Invalid proof data identifier");
+ | NONE => raise Fail "Invalid proof data identifier");
fun init_data thy =
Datatab.map' (fn k => fn _ => invoke_init k thy) (! kinds);
--- a/src/Pure/library.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/library.ML Wed Jul 21 18:13:15 2010 +0200
@@ -1000,21 +1000,23 @@
(*Partition a list into buckets [ bi, b(i+1), ..., bj ]
putting x in bk if p(k)(x) holds. Preserve order of elements if possible.*)
fun partition_list p i j =
- let fun part k xs =
- if k>j then
- (case xs of [] => []
- | _ => raise Fail "partition_list")
- else
- let val (ns, rest) = List.partition (p k) xs;
- in ns :: part(k+1)rest end
- in part (i: int) end;
+ let
+ fun part (k: int) xs =
+ if k > j then
+ (case xs of
+ [] => []
+ | _ => raise Fail "partition_list")
+ else
+ let val (ns, rest) = List.partition (p k) xs
+ in ns :: part (k + 1) rest end;
+ in part (i: int) end;
-fun partition_eq (eq:'a * 'a -> bool) =
+fun partition_eq (eq: 'a * 'a -> bool) =
let
fun part [] = []
| part (x :: ys) =
let val (xs, xs') = List.partition (fn y => eq (x, y)) ys
- in (x::xs)::(part xs') end
+ in (x :: xs) :: part xs' end;
in part end;
--- a/src/Pure/pure_setup.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/pure_setup.ML Wed Jul 21 18:13:15 2010 +0200
@@ -6,8 +6,6 @@
(* the Pure theories *)
-val theory = Thy_Info.get_theory;
-
Context.>> (Context.map_theory
(Outer_Syntax.process_file (Path.explode "Pure.thy") #>
Theory.end_theory));
@@ -18,7 +16,9 @@
(* ML toplevel pretty printing *)
-toplevel_pp ["String", "string"] "ML_Syntax.pretty_string";
+if String.isPrefix "smlnj" ml_system then ()
+else toplevel_pp ["String", "string"] "ML_Syntax.pretty_string";
+
toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
@@ -34,6 +34,8 @@
toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
+toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
+toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
if ml_system = "polyml-5.3.0"
then use "ML-Systems/install_pp_polyml-5.3.ML"
@@ -52,8 +54,6 @@
fun use name = Toplevel.program (fn () => Thy_Info.use name);
fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
-fun time_use name = Toplevel.program (fn () => Thy_Info.time_use name);
-fun time_use_thy name = Toplevel.program (fn () => Thy_Info.time_use_thy name);
(* misc *)
--- a/src/Pure/term_ord.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Pure/term_ord.ML Wed Jul 21 18:13:15 2010 +0200
@@ -84,7 +84,7 @@
| atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
| atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
| atoms_ord (Bound i, Bound j) = int_ord (i, j)
- | atoms_ord _ = sys_error "atoms_ord";
+ | atoms_ord _ = raise Fail "atoms_ord";
fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
(case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
@@ -94,7 +94,7 @@
| types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
| types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
| types_ord (Bound _, Bound _) = EQUAL
- | types_ord _ = sys_error "types_ord";
+ | types_ord _ = raise Fail "types_ord";
in
--- a/src/Tools/Code/code_printer.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Tools/Code/code_printer.ML Wed Jul 21 18:13:15 2010 +0200
@@ -358,7 +358,7 @@
val _ = List.app Keyword.keyword [infixK, infixlK, infixrK];
-val parse_tyco_syntax = parse_syntax (fn s => (0, (K o K o K o str) s)) I I;
+fun parse_tyco_syntax x = parse_syntax (fn s => (0, (K o K o K o str) s)) I I x;
val parse_const_syntax = parse_syntax plain_const_syntax simple_const_syntax fst;
--- a/src/Tools/Code/code_target.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Tools/Code/code_target.ML Wed Jul 21 18:13:15 2010 +0200
@@ -603,7 +603,7 @@
fun shell_command thyname cmd = Toplevel.program (fn _ =>
(use_thy thyname; case Scan.read Token.stopper (Parse.!!! code_exprP)
((filter Token.is_proper o Outer_Syntax.scan Position.none) cmd)
- of SOME f => (writeln "Now generating code..."; f (theory thyname))
+ of SOME f => (writeln "Now generating code..."; f (Thy_Info.get_theory thyname))
| NONE => error ("Bad directive " ^ quote cmd)))
handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
--- a/src/Tools/Code/code_thingol.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML Wed Jul 21 18:13:15 2010 +0200
@@ -910,7 +910,7 @@
fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
fun read_const_expr "*" = ([], consts_of thy)
| read_const_expr s = if String.isSuffix ".*" s
- then ([], consts_of_select (Thy_Info.the_theory (unsuffix ".*" s) thy))
+ then ([], consts_of_select (Context.this_theory thy (unsuffix ".*" s)))
else ([Code.read_const thy s], []);
in pairself flat o split_list o map read_const_expr end;
--- a/src/Tools/Compute_Oracle/Compute_Oracle.thy Wed Jul 21 18:11:51 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(* Title: Tools/Compute_Oracle/Compute_Oracle.thy
- Author: Steven Obua, TU Munich
-
-Steven Obua's evaluator.
-*)
-
-theory Compute_Oracle imports Pure
-uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
-begin
-
-end
\ No newline at end of file
--- a/src/Tools/Compute_Oracle/am.ML Wed Jul 21 18:11:51 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-signature ABSTRACT_MACHINE =
-sig
-
-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)
-
-datatype guard = Guard of term * term
-
-type program
-
-exception Compile of string;
-
-(* The de-Bruijn index 0 occurring on the right hand side refers to the LAST pattern variable, when traversing the pattern from left to right,
- 1 to the second last, and so on. *)
-val compile : pattern list -> (int -> int option) -> (guard list * pattern * term) list -> program
-
-val discard : program -> unit
-
-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 | Computed of term
-
-datatype pattern = PVar | PConst of int * (pattern list)
-
-datatype guard = Guard of term * term
-
-type program = unit
-
-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"
-
-exception Run of string;
-
-fun run p t = raise Run "abstract machine stub"
-
-end
--- a/src/Tools/Compute_Oracle/am_compiler.ML Wed Jul 21 18:11:51 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,211 +0,0 @@
-(* Title: Tools/Compute_Oracle/am_compiler.ML
- Author: Steven Obua
-*)
-
-signature COMPILING_AM =
-sig
- include ABSTRACT_MACHINE
-
- val set_compiled_rewriter : (term -> term) -> unit
- val list_nth : 'a list * int -> 'a
- val list_map : ('a -> 'b) -> 'a list -> 'b list
-end
-
-structure AM_Compiler : COMPILING_AM = struct
-
-val list_nth = List.nth;
-val list_map = map;
-
-open AbstractMachine;
-
-val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option)
-
-fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
-
-type program = (term -> term)
-
-fun count_patternvars PVar = 1
- | count_patternvars (PConst (_, ps)) =
- List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
-
-fun print_rule (p, t) =
- let
- fun str x = Int.toString x
- fun print_pattern n PVar = (n+1, "x"^(str n))
- | print_pattern n (PConst (c, [])) = (n, "c"^(str c))
- | print_pattern n (PConst (c, args)) =
- let
- val h = print_pattern n (PConst (c,[]))
- in
- print_pattern_list h args
- end
- and print_pattern_list r [] = r
- | print_pattern_list (n, p) (t::ts) =
- let
- val (n, t) = print_pattern n t
- in
- print_pattern_list (n, "App ("^p^", "^t^")") ts
- end
-
- val (n, pattern) = print_pattern 0 p
- val pattern =
- if exists_string Symbol.is_ascii_blank pattern then "(" ^ pattern ^")"
- else pattern
-
- fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*)
- "Var " ^ str x
- | 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))
-
- val term = print_term 0 t
- val term =
- if n > 0 then "Closure (["^(listvars (n-1))^"], "^term^")"
- else "Closure ([], "^term^")"
-
- in
- " | weak_reduce (false, stack, "^pattern^") = Continue (false, stack, "^term^")"
- end
-
-fun constants_of PVar = []
- | constants_of (PConst (c, ps)) = c :: maps constants_of ps
-
-fun constants_of_term (Var _) = []
- | 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
- val buffer = Unsynchronized.ref ""
- fun write s = (buffer := (!buffer)^s)
- fun writeln s = (write s; write "\n")
- fun writelist [] = ()
- | writelist (s::ss) = (writeln s; writelist ss)
- fun str i = Int.toString i
- val _ = writelist [
- "structure "^name^" = struct",
- "",
- "datatype term = Dummy | App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"]
- val constants = distinct (op =) (maps (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog)
- val _ = map (fn x => write (" | c"^(str x))) constants
- val _ = writelist [
- "",
- "datatype stack = SEmpty | SAppL of term * stack | SAppR of term * stack | SAbs of stack",
- "",
- "type state = bool * stack * term",
- "",
- "datatype loopstate = Continue of state | Stop of stack * term",
- "",
- "fun proj_C (Continue s) = s",
- " | proj_C _ = raise Match",
- "",
- "fun proj_S (Stop s) = s",
- " | proj_S _ = raise Match",
- "",
- "fun cont (Continue _) = true",
- " | cont _ = false",
- "",
- "fun do_reduction reduce p =",
- " let",
- " val s = Unsynchronized.ref (Continue p)",
- " val _ = while cont (!s) do (s := reduce (proj_C (!s)))",
- " in",
- " proj_S (!s)",
- " end",
- ""]
-
- val _ = writelist [
- "fun weak_reduce (false, stack, Closure (e, App (a, b))) = Continue (false, SAppL (Closure (e, b), stack), Closure (e, a))",
- " | weak_reduce (false, SAppL (b, stack), Closure (e, Abs m)) = Continue (false, stack, Closure (b::e, m))",
- " | weak_reduce (false, stack, c as Closure (e, Abs m)) = Continue (true, stack, c)",
- " | weak_reduce (false, stack, Closure (e, Var n)) = Continue (false, stack, case "^sname^".list_nth (e, n) of Dummy => Var n | r => r)",
- " | weak_reduce (false, stack, Closure (e, c)) = Continue (false, stack, c)"]
- val _ = writelist (map print_rule prog)
- val _ = writelist [
- " | weak_reduce (false, stack, clos) = Continue (true, stack, clos)",
- " | weak_reduce (true, SAppR (a, stack), b) = Continue (false, stack, App (a,b))",
- " | weak_reduce (true, s as (SAppL (b, stack)), a) = Continue (false, SAppR (a, stack), b)",
- " | weak_reduce (true, stack, c) = Stop (stack, c)",
- "",
- "fun strong_reduce (false, stack, Closure (e, Abs m)) =",
- " let",
- " val (stack', wnf) = do_reduction weak_reduce (false, SEmpty, Closure (Dummy::e, m))",
- " in",
- " case stack' of",
- " SEmpty => Continue (false, SAbs stack, wnf)",
- " | _ => raise ("^sname^".Run \"internal error in strong: weak failed\")",
- " end",
- " | strong_reduce (false, stack, clos as (App (u, v))) = Continue (false, SAppL (v, stack), u)",
- " | strong_reduce (false, stack, clos) = Continue (true, stack, clos)",
- " | strong_reduce (true, SAbs stack, m) = Continue (false, stack, Abs m)",
- " | strong_reduce (true, SAppL (b, stack), a) = Continue (false, SAppR (a, stack), b)",
- " | strong_reduce (true, SAppR (a, stack), b) = Continue (true, stack, App (a, b))",
- " | strong_reduce (true, stack, clos) = Stop (stack, clos)",
- ""]
-
- val ic = "(case c of "^(implode (map (fn c => (str c)^" => c"^(str c)^" | ") constants))^" _ => Const c)"
- val _ = writelist [
- "fun importTerm ("^sname^".Var x) = Var x",
- " | importTerm ("^sname^".Const c) = "^ic,
- " | importTerm ("^sname^".App (a, b)) = App (importTerm a, importTerm b)",
- " | importTerm ("^sname^".Abs m) = Abs (importTerm m)",
- ""]
-
- fun ec c = " | exportTerm c"^(str c)^" = "^sname^".Const "^(str c)
- val _ = writelist [
- "fun exportTerm (Var x) = "^sname^".Var x",
- " | exportTerm (Const c) = "^sname^".Const c",
- " | exportTerm (App (a,b)) = "^sname^".App (exportTerm a, exportTerm b)",
- " | exportTerm (Abs m) = "^sname^".Abs (exportTerm m)",
- " | exportTerm (Closure (closlist, clos)) = raise ("^sname^".Run \"internal error, cannot export Closure\")",
- " | exportTerm Dummy = raise ("^sname^".Run \"internal error, cannot export Dummy\")"]
- val _ = writelist (map ec constants)
-
- val _ = writelist [
- "",
- "fun rewrite t = ",
- " let",
- " val (stack, wnf) = do_reduction weak_reduce (false, SEmpty, Closure ([], importTerm t))",
- " in",
- " case stack of ",
- " SEmpty => (case do_reduction strong_reduce (false, SEmpty, wnf) of",
- " (SEmpty, snf) => exportTerm snf",
- " | _ => raise ("^sname^".Run \"internal error in rewrite: strong failed\"))",
- " | _ => (raise ("^sname^".Run \"internal error in rewrite: weak failed\"))",
- " end",
- "",
- "val _ = "^sname^".set_compiled_rewriter rewrite",
- "",
- "end;"]
-
- in
- compiled_rewriter := NONE;
- use_text ML_Env.local_context (1, "") false (!buffer);
- case !compiled_rewriter of
- NONE => raise (Compile "cannot communicate with compiled function")
- | SOME r => (compiled_rewriter := NONE; r)
- end
-
-fun compile cache_patterns const_arity eqs =
- let
- val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
- val eqs = map (fn (a,b,c) => (b,c)) eqs
- fun check (p, r) = if check_freevars (count_patternvars p) r then () else raise Compile ("unbound variables in rule")
- val _ = map (fn (p, r) =>
- (check (p, r);
- case p of PVar => raise (Compile "pattern is just a variable") | _ => ())) eqs
- in
- load_rules "AM_Compiler" "AM_compiled_code" eqs
- end
-
-fun run prog t = (prog t)
-
-fun discard p = ()
-
-end
-
--- a/src/Tools/Compute_Oracle/am_ghc.ML Wed Jul 21 18:11:51 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,325 +0,0 @@
-(* Title: Tools/Compute_Oracle/am_ghc.ML
- Author: Steven Obua
-*)
-
-structure AM_GHC : ABSTRACT_MACHINE = struct
-
-open AbstractMachine;
-
-type program = string * string * (int Inttab.table)
-
-fun count_patternvars PVar = 1
- | count_patternvars (PConst (_, ps)) =
- List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
-
-fun update_arity arity code a =
- (case Inttab.lookup arity code of
- NONE => Inttab.update_new (code, a) arity
- | SOME (a': int) => if a > a' then Inttab.update (code, a) arity else arity)
-
-(* We have to find out the maximal arity of each constant *)
-fun collect_pattern_arity PVar arity = arity
- | collect_pattern_arity (PConst (c, args)) arity = fold collect_pattern_arity args (update_arity arity c (length args))
-
-local
-fun collect applevel (Var _) arity = arity
- | collect applevel (Const c) arity = update_arity arity c applevel
- | collect applevel (Abs m) arity = collect 0 m arity
- | collect applevel (App (a,b)) arity = collect 0 b (collect (applevel + 1) a arity)
-in
-fun collect_term_arity t arity = collect 0 t arity
-end
-
-fun nlift level n (Var m) = if m < level then Var m else Var (m+n)
- | nlift level n (Const c) = Const c
- | nlift level n (App (a,b)) = App (nlift level n a, nlift level n b)
- | nlift level n (Abs b) = Abs (nlift (level+1) n b)
-
-fun rep n x = if n = 0 then [] else x::(rep (n-1) x)
-
-fun adjust_rules rules =
- let
- val arity = fold (fn (p, t) => fn arity => collect_term_arity t (collect_pattern_arity p arity)) rules Inttab.empty
- fun arity_of c = the (Inttab.lookup arity c)
- fun adjust_pattern PVar = PVar
- | adjust_pattern (C as PConst (c, args)) = if (length args <> arity_of c) then raise Compile ("Constant inside pattern must have maximal arity") else C
- fun adjust_rule (PVar, t) = raise Compile ("pattern may not be a variable")
- | adjust_rule (rule as (p as PConst (c, args),t)) =
- let
- val _ = if not (check_freevars (count_patternvars p) t) then raise Compile ("unbound variables on right hand side") else ()
- val args = map adjust_pattern args
- val len = length args
- val arity = arity_of c
- fun lift level n (Var m) = if m < level then Var m else Var (m+n)
- | lift level n (Const c) = Const c
- | lift level n (App (a,b)) = App (lift level n a, lift level n b)
- | lift level n (Abs b) = Abs (lift (level+1) n b)
- val lift = lift 0
- fun adjust_term n t = if n=0 then t else adjust_term (n-1) (App (t, Var (n-1)))
- in
- if len = arity then
- rule
- else if arity >= len then
- (PConst (c, args @ (rep (arity-len) PVar)), adjust_term (arity-len) (lift (arity-len) t))
- else (raise Compile "internal error in adjust_rule")
- end
- in
- (arity, map adjust_rule rules)
- end
-
-fun print_term arity_of n =
-let
- fun str x = string_of_int x
- fun protect_blank s = if exists_string Symbol.is_ascii_blank s then "(" ^ s ^")" else s
-
- fun print_apps d f [] = f
- | print_apps d f (a::args) = print_apps d ("app "^(protect_blank f)^" "^(protect_blank (print_term d a))) args
- and print_call d (App (a, b)) args = print_call d a (b::args)
- | print_call d (Const c) args =
- (case arity_of c of
- NONE => print_apps d ("Const "^(str c)) args
- | SOME a =>
- let
- val len = length args
- in
- if a <= len then
- let
- val s = "c"^(str c)^(implode (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, a))))
- in
- print_apps d s (List.drop (args, a))
- end
- else
- let
- fun mk_apps n t = if n = 0 then t else mk_apps (n-1) (App (t, Var (n-1)))
- fun mk_lambdas n t = if n = 0 then t else mk_lambdas (n-1) (Abs t)
- fun append_args [] t = t
- | append_args (c::cs) t = append_args cs (App (t, c))
- in
- print_term d (mk_lambdas (a-len) (mk_apps (a-len) (nlift 0 (a-len) (append_args args (Const c)))))
- end
- end)
- | print_call d t args = print_apps d (print_term d t) args
- and print_term d (Var x) = if x < d then "b"^(str (d-x-1)) else "x"^(str (n-(x-d)-1))
- | print_term d (Abs c) = "Abs (\\b"^(str d)^" -> "^(print_term (d + 1) c)^")"
- | print_term d t = print_call d t []
-in
- print_term 0
-end
-
-fun print_rule arity_of (p, t) =
- let
- fun str x = Int.toString x
- fun print_pattern top n PVar = (n+1, "x"^(str n))
- | print_pattern top n (PConst (c, [])) = (n, (if top then "c" else "C")^(str c))
- | print_pattern top n (PConst (c, args)) =
- let
- val (n,s) = print_pattern_list (n, (if top then "c" else "C")^(str c)) args
- in
- (n, if top then s else "("^s^")")
- end
- and print_pattern_list r [] = r
- | print_pattern_list (n, p) (t::ts) =
- let
- val (n, t) = print_pattern false n t
- in
- print_pattern_list (n, p^" "^t) ts
- end
- val (n, pattern) = print_pattern true 0 p
- in
- pattern^" = "^(print_term arity_of n t)
- end
-
-fun group_rules rules =
- let
- fun add_rule (r as (PConst (c,_), _)) groups =
- let
- val rs = (case Inttab.lookup groups c of NONE => [] | SOME rs => rs)
- in
- Inttab.update (c, r::rs) groups
- end
- | add_rule _ _ = raise Compile "internal error group_rules"
- in
- fold_rev add_rule rules Inttab.empty
- end
-
-fun haskell_prog name rules =
- let
- val buffer = Unsynchronized.ref ""
- fun write s = (buffer := (!buffer)^s)
- fun writeln s = (write s; write "\n")
- fun writelist [] = ()
- | writelist (s::ss) = (writeln s; writelist ss)
- fun str i = Int.toString i
- val (arity, rules) = adjust_rules rules
- val rules = group_rules rules
- val constants = Inttab.keys arity
- fun arity_of c = Inttab.lookup arity c
- fun rep_str s n = implode (rep n s)
- fun indexed s n = s^(str n)
- fun section n = if n = 0 then [] else (section (n-1))@[n-1]
- fun make_show c =
- let
- val args = section (the (arity_of c))
- in
- " show ("^(indexed "C" c)^(implode (map (indexed " a") args))^") = "
- ^"\""^(indexed "C" c)^"\""^(implode (map (fn a => "++(show "^(indexed "a" a)^")") args))
- end
- fun default_case c =
- let
- val args = implode (map (indexed " x") (section (the (arity_of c))))
- in
- (indexed "c" c)^args^" = "^(indexed "C" c)^args
- end
- val _ = writelist [
- "module "^name^" where",
- "",
- "data Term = Const Integer | App Term Term | Abs (Term -> Term)",
- " "^(implode (map (fn c => " | C"^(str c)^(rep_str " Term" (the (arity_of c)))) constants)),
- "",
- "instance Show Term where"]
- val _ = writelist (map make_show constants)
- val _ = writelist [
- " show (Const c) = \"c\"++(show c)",
- " show (App a b) = \"A\"++(show a)++(show b)",
- " show (Abs _) = \"L\"",
- ""]
- val _ = writelist [
- "app (Abs a) b = a b",
- "app a b = App a b",
- "",
- "calc s c = writeFile s (show c)",
- ""]
- fun list_group c = (writelist (case Inttab.lookup rules c of
- NONE => [default_case c, ""]
- | SOME (rs as ((PConst (_, []), _)::rs')) =>
- if not (null rs') then raise Compile "multiple declaration of constant"
- else (map (print_rule arity_of) rs) @ [""]
- | SOME rs => (map (print_rule arity_of) rs) @ [default_case c, ""]))
- val _ = map list_group constants
- in
- (arity, !buffer)
- end
-
-val guid_counter = Unsynchronized.ref 0
-fun get_guid () =
- let
- val c = !guid_counter
- val _ = guid_counter := !guid_counter + 1
- in
- (LargeInt.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c)
- end
-
-fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
-fun wrap s = "\""^s^"\""
-
-fun writeTextFile name s = File.write (Path.explode name) s
-
-val ghc = Unsynchronized.ref (case getenv "GHC_PATH" of "" => "ghc" | s => s)
-
-fun fileExists name = ((OS.FileSys.fileSize name; true) handle OS.SysErr _ => false)
-
-fun compile cache_patterns const_arity eqs =
- let
- val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
- val eqs = map (fn (a,b,c) => (b,c)) eqs
- val guid = get_guid ()
- val module = "AMGHC_Prog_"^guid
- val (arity, source) = haskell_prog module eqs
- val module_file = tmp_file (module^".hs")
- val object_file = tmp_file (module^".o")
- val _ = writeTextFile module_file source
- val _ = bash ((!ghc)^" -c "^module_file)
- val _ = if not (fileExists object_file) then raise Compile ("Failure compiling haskell code (GHC_PATH = '"^(!ghc)^"')") else ()
- in
- (guid, module_file, arity)
- end
-
-fun readResultFile name = File.read (Path.explode name)
-
-fun parse_result arity_of result =
- let
- val result = String.explode result
- fun shift NONE x = SOME x
- | shift (SOME y) x = SOME (y*10 + x)
- fun parse_int' x (#"0"::rest) = parse_int' (shift x 0) rest
- | parse_int' x (#"1"::rest) = parse_int' (shift x 1) rest
- | parse_int' x (#"2"::rest) = parse_int' (shift x 2) rest
- | parse_int' x (#"3"::rest) = parse_int' (shift x 3) rest
- | parse_int' x (#"4"::rest) = parse_int' (shift x 4) rest
- | parse_int' x (#"5"::rest) = parse_int' (shift x 5) rest
- | parse_int' x (#"6"::rest) = parse_int' (shift x 6) rest
- | parse_int' x (#"7"::rest) = parse_int' (shift x 7) rest
- | parse_int' x (#"8"::rest) = parse_int' (shift x 8) rest
- | parse_int' x (#"9"::rest) = parse_int' (shift x 9) rest
- | parse_int' x rest = (x, rest)
- fun parse_int rest = parse_int' NONE rest
-
- fun parse (#"C"::rest) =
- (case parse_int rest of
- (SOME c, rest) =>
- let
- val (args, rest) = parse_list (the (arity_of c)) rest
- fun app_args [] t = t
- | app_args (x::xs) t = app_args xs (App (t, x))
- in
- (app_args args (Const c), rest)
- end
- | (NONE, rest) => raise Run "parse C")
- | parse (#"c"::rest) =
- (case parse_int rest of
- (SOME c, rest) => (Const c, rest)
- | _ => raise Run "parse c")
- | parse (#"A"::rest) =
- let
- val (a, rest) = parse rest
- val (b, rest) = parse rest
- in
- (App (a,b), rest)
- end
- | parse (#"L"::rest) = raise Run "there may be no abstraction in the result"
- | parse _ = raise Run "invalid result"
- and parse_list n rest =
- if n = 0 then
- ([], rest)
- else
- let
- val (x, rest) = parse rest
- val (xs, rest) = parse_list (n-1) rest
- in
- (x::xs, rest)
- end
- val (parsed, rest) = parse result
- fun is_blank (#" "::rest) = is_blank rest
- | is_blank (#"\n"::rest) = is_blank rest
- | is_blank [] = true
- | is_blank _ = false
- in
- if is_blank rest then parsed else raise Run "non-blank suffix in result file"
- end
-
-fun run (guid, module_file, arity) t =
- let
- val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms")
- fun arity_of c = Inttab.lookup arity c
- val callguid = get_guid()
- val module = "AMGHC_Prog_"^guid
- val call = module^"_Call_"^callguid
- val result_file = tmp_file (module^"_Result_"^callguid^".txt")
- val call_file = tmp_file (call^".hs")
- val term = print_term arity_of 0 t
- val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
- val _ = writeTextFile call_file call_source
- val _ = bash ((!ghc)^" -e \""^call^".call\" "^module_file^" "^call_file)
- val result = readResultFile result_file handle IO.Io _ => raise Run ("Failure running haskell compiler (GHC_PATH = '"^(!ghc)^"')")
- val t' = parse_result arity_of result
- val _ = OS.FileSys.remove call_file
- val _ = OS.FileSys.remove result_file
- in
- t'
- end
-
-
-fun discard _ = ()
-
-end
-
--- a/src/Tools/Compute_Oracle/am_interpreter.ML Wed Jul 21 18:11:51 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,213 +0,0 @@
-(* Title: Tools/Compute_Oracle/am_interpreter.ML
- Author: Steven Obua
-*)
-
-signature AM_BARRAS =
-sig
- include ABSTRACT_MACHINE
- val max_reductions : int option Unsynchronized.ref
-end
-
-structure AM_Interpreter : AM_BARRAS = struct
-
-open AbstractMachine;
-
-datatype closure = CDummy | CVar of int | CConst of int
- | CApp of closure * closure | CAbs of closure
- | Closure of (closure list) * closure
-
-structure prog_struct = Table(type key = int*int val ord = prod_ord int_ord int_ord);
-
-datatype program = Program of ((pattern * closure * (closure*closure) list) list) prog_struct.table
-
-datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
-
-fun clos_of_term (Var x) = CVar x
- | 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
- | term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
- | term_of_clos (CAbs u) = Abs (term_of_clos u)
- | 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)
-
-fun len_head_of_closure n (CApp (a,b)) = len_head_of_closure (n+1) a
- | len_head_of_closure n x = (n, x)
-
-
-(* earlier occurrence of PVar corresponds to higher de Bruijn index *)
-fun pattern_match args PVar clos = SOME (clos::args)
- | pattern_match args (PConst (c, patterns)) clos =
- let
- val (f, closargs) = strip_closure [] clos
- in
- case f of
- CConst d =>
- if c = d then
- pattern_match_list args patterns closargs
- else
- NONE
- | _ => NONE
- end
-and pattern_match_list args [] [] = SOME args
- | pattern_match_list args (p::ps) (c::cs) =
- (case pattern_match args p c of
- NONE => NONE
- | SOME args => pattern_match_list args ps cs)
- | pattern_match_list _ _ _ = NONE
-
-fun count_patternvars PVar = 1
- | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
-
-fun pattern_key (PConst (c, ps)) = (c, length ps)
- | pattern_key _ = raise (Compile "pattern reduces to variable")
-
-(*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 compile cache_patterns const_arity eqs =
- let
- fun check p r = if check_freevars p r then () else raise Compile ("unbound variables in rule")
- fun check_guard p (Guard (a,b)) = (check p a; check p b)
- fun clos_of_guard (Guard (a,b)) = (clos_of_term a, clos_of_term b)
- val eqs = map (fn (guards, p, r) => let val pcount = count_patternvars p val _ = map (check_guard pcount) (guards) val _ = check pcount r in
- (pattern_key p, (p, clos_of_term r, map clos_of_guard guards)) end) eqs
- fun merge (k, a) table = prog_struct.update (k, case prog_struct.lookup table k of NONE => [a] | SOME l => a::l) table
- val p = fold merge eqs prog_struct.empty
- in
- Program p
- end
-
-
-type state = bool * program * stack * closure
-
-datatype loopstate = Continue of state | Stop of stack * closure
-
-fun proj_C (Continue s) = s
- | proj_C _ = raise Match
-
-exception InterruptedExecution of stack * closure
-
-fun proj_S (Stop s) = s
- | proj_S (Continue (_,_,s,c)) = (s,c)
-
-fun cont (Continue _) = true
- | cont _ = false
-
-val max_reductions = Unsynchronized.ref (NONE : int option)
-
-fun do_reduction reduce p =
- let
- val s = Unsynchronized.ref (Continue p)
- val counter = Unsynchronized.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
- 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 match_rules prog n [] clos = NONE
- | match_rules prog n ((p,eq,guards)::rs) clos =
- case pattern_match [] p clos of
- NONE => match_rules prog (n+1) rs clos
- | SOME args => if forall (guard_checks prog args) guards then SOME (Closure (args, eq)) else match_rules prog (n+1) rs clos
-and guard_checks prog args (a,b) = (simp prog (Closure (args, a)) = simp prog (Closure (args, b)))
-and match_closure (p as (Program prog)) clos =
- case len_head_of_closure 0 clos of
- (len, CConst c) =>
- (case prog_struct.lookup prog (c, len) of
- NONE => NONE
- | SOME rules => match_rules p 0 rules clos)
- | _ => NONE
-
-and weak_reduce (false, prog, stack, Closure (e, CApp (a, b))) = Continue (false, prog, SAppL (Closure (e, b), stack), Closure (e, a))
- | weak_reduce (false, prog, SAppL (b, stack), Closure (e, CAbs m)) = Continue (false, prog, stack, Closure (b::e, m))
- | weak_reduce (false, prog, stack, Closure (e, CVar n)) = Continue (false, prog, stack, case List.nth (e, n) of CDummy => CVar n | r => r)
- | weak_reduce (false, prog, stack, Closure (e, c as CConst _)) = Continue (false, prog, stack, c)
- | weak_reduce (false, prog, stack, clos) =
- (case match_closure prog clos of
- NONE => Continue (true, prog, stack, clos)
- | SOME r => Continue (false, prog, stack, r))
- | weak_reduce (true, prog, SAppR (a, stack), b) = Continue (false, prog, stack, CApp (a,b))
- | weak_reduce (true, prog, s as (SAppL (b, stack)), a) = Continue (false, prog, SAppR (a, stack), b)
- | weak_reduce (true, prog, stack, c) = Stop (stack, c)
-
-and 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 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)
- | strong_reduce (true, prog, SAppL (b, stack), a) = Continue (false, prog, SAppR (a, stack), b)
- | strong_reduce (true, prog, SAppR (a, stack), b) = Continue (true, prog, stack, CApp (a, b))
- | strong_reduce (true, prog, stack, clos) = Stop (stack, clos)
-
-and simp prog t =
- (let
- val (stack, wnf) = do_reduction weak_reduce (false, prog, SEmpty, t)
- in
- case stack of
- SEmpty => (case do_reduction strong_reduce (false, prog, SEmpty, wnf) of
- (SEmpty, snf) => snf
- | _ => raise (Run "internal error in run: strong failed"))
- | _ => raise (Run "internal error in run: weak failed")
- end handle InterruptedExecution state => resolve state)
-
-
-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 handle InterruptedExecution state => term_of_clos (resolve state))
-
-fun discard p = ()
-
-end
--- a/src/Tools/Compute_Oracle/am_sml.ML Wed Jul 21 18:11:51 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,548 +0,0 @@
-(* Title: Tools/Compute_Oracle/am_sml.ML
- Author: Steven Obua
-
-TODO: "parameterless rewrite cannot be used in pattern": In a lot of
-cases it CAN be used, and these cases should be handled
-properly; right now, all cases raise an exception.
-*)
-
-signature AM_SML =
-sig
- include ABSTRACT_MACHINE
- val save_result : (string * term) -> unit
- val set_compiled_rewriter : (term -> term) -> unit
- val list_nth : 'a list * int -> 'a
- val dump_output : (string option) Unsynchronized.ref
-end
-
-structure AM_SML : AM_SML = struct
-
-open AbstractMachine;
-
-val dump_output = Unsynchronized.ref (NONE: string option)
-
-type program = string * string * (int Inttab.table) * (int Inttab.table) * (term Inttab.table) * (term -> term)
-
-val saved_result = Unsynchronized.ref (NONE:(string*term)option)
-
-fun save_result r = (saved_result := SOME r)
-fun clear_result () = (saved_result := NONE)
-
-val list_nth = List.nth
-
-(*fun list_nth (l,n) = (writeln (makestring ("list_nth", (length l,n))); List.nth (l,n))*)
-
-val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option)
-
-fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
-
-fun count_patternvars PVar = 1
- | count_patternvars (PConst (_, ps)) =
- List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
-
-fun update_arity arity code a =
- (case Inttab.lookup arity code of
- NONE => Inttab.update_new (code, a) arity
- | SOME (a': int) => if a > a' then Inttab.update (code, a) arity else arity)
-
-(* We have to find out the maximal arity of each constant *)
-fun collect_pattern_arity PVar arity = arity
- | collect_pattern_arity (PConst (c, args)) arity = fold collect_pattern_arity args (update_arity arity c (length args))
-
-(* We also need to find out the maximal toplevel arity of each function constant *)
-fun collect_pattern_toplevel_arity PVar arity = raise Compile "internal error: collect_pattern_toplevel_arity"
- | collect_pattern_toplevel_arity (PConst (c, args)) arity = update_arity arity c (length args)
-
-local
-fun collect applevel (Var _) arity = arity
- | collect applevel (Const c) arity = update_arity arity c applevel
- | collect applevel (Abs m) arity = collect 0 m arity
- | collect applevel (App (a,b)) arity = collect 0 b (collect (applevel + 1) a arity)
-in
-fun collect_term_arity t arity = collect 0 t arity
-end
-
-fun collect_guard_arity (Guard (a,b)) arity = collect_term_arity b (collect_term_arity a arity)
-
-
-fun rep n x = if n < 0 then raise Compile "internal error: rep" else if n = 0 then [] else x::(rep (n-1) x)
-
-fun beta (Const c) = Const c
- | beta (Var i) = Var i
- | beta (App (Abs m, b)) = beta (unlift 0 (subst 0 m (lift 0 b)))
- | beta (App (a, b)) =
- (case beta a of
- 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)
- | subst x (Abs m) t = Abs (subst (x+1) m (lift 0 t))
-and lift level (Const c) = Const c
- | lift level (App (a,b)) = App (lift level a, lift level b)
- | lift level (Var i) = if i < level then Var i else Var (i+1)
- | lift level (Abs m) = Abs (lift (level + 1) m)
-and unlift level (Const c) = Const c
- | unlift level (App (a, b)) = App (unlift level a, unlift level b)
- | unlift level (Abs m) = Abs (unlift (level+1) m)
- | unlift level (Var i) = if i < level then Var i else Var (i-1)
-
-fun nlift level n (Var m) = if m < level then Var m else Var (m+n)
- | nlift level n (Const c) = Const c
- | nlift level n (App (a,b)) = App (nlift level n a, nlift level n b)
- | nlift level n (Abs b) = Abs (nlift (level+1) n b)
-
-fun subst_const (c, t) (Const c') = if c = c' then t else Const c'
- | subst_const _ (Var i) = Var i
- | subst_const ct (App (a, b)) = App (subst_const ct a, subst_const ct b)
- | subst_const ct (Abs m) = Abs (subst_const ct m)
-
-(* Remove all rules that are just parameterless rewrites. This is necessary because SML does not allow functions with no parameters. *)
-fun inline_rules rules =
- let
- fun term_contains_const c (App (a, b)) = term_contains_const c a orelse term_contains_const c b
- | term_contains_const c (Abs m) = term_contains_const c m
- | term_contains_const c (Var i) = false
- | term_contains_const c (Const c') = (c = c')
- fun find_rewrite [] = NONE
- | find_rewrite ((prems, PConst (c, []), r) :: _) =
- if check_freevars 0 r then
- if term_contains_const c r then
- raise Compile "parameterless rewrite is caught in cycle"
- else if not (null prems) then
- raise Compile "parameterless rewrite may not be guarded"
- else
- SOME (c, r)
- else raise Compile "unbound variable on right hand side or guards of rule"
- | find_rewrite (_ :: rules) = find_rewrite rules
- fun remove_rewrite (c,r) [] = []
- | remove_rewrite (cr as (c,r)) ((rule as (prems', PConst (c', args), r'))::rules) =
- (if c = c' then
- if null args andalso r = r' andalso null (prems') then
- remove_rewrite cr rules
- else raise Compile "incompatible parameterless rewrites found"
- else
- rule :: (remove_rewrite cr rules))
- | remove_rewrite cr (r::rs) = r::(remove_rewrite cr rs)
- fun pattern_contains_const c (PConst (c', args)) = (c = c' orelse exists (pattern_contains_const c) args)
- | pattern_contains_const c (PVar) = false
- fun inline_rewrite (ct as (c, _)) (prems, p, r) =
- if pattern_contains_const c p then
- raise Compile "parameterless rewrite cannot be used in pattern"
- else (map (fn (Guard (a,b)) => Guard (subst_const ct a, subst_const ct b)) prems, p, subst_const ct r)
- fun inline inlined rules =
- (case find_rewrite rules of
- NONE => (Inttab.make inlined, rules)
- | SOME ct =>
- let
- val rules = map (inline_rewrite ct) (remove_rewrite ct rules)
- val inlined = ct :: (map (fn (c', r) => (c', subst_const ct r)) inlined)
- in
- inline inlined rules
- end)
- in
- inline [] rules
- end
-
-
-(*
- Calculate the arity, the toplevel_arity, and adjust rules so that all toplevel pattern constants have maximal arity.
- Also beta reduce the adjusted right hand side of a rule.
-*)
-fun adjust_rules rules =
- let
- val arity = fold (fn (prems, p, t) => fn arity => fold collect_guard_arity prems (collect_term_arity t (collect_pattern_arity p arity))) rules Inttab.empty
- val toplevel_arity = fold (fn (_, p, t) => fn arity => collect_pattern_toplevel_arity p arity) rules Inttab.empty
- fun arity_of c = the (Inttab.lookup arity c)
- fun toplevel_arity_of c = the (Inttab.lookup toplevel_arity c)
- fun test_pattern PVar = ()
- | test_pattern (C as PConst (c, args)) = if (length args <> arity_of c) then raise Compile ("Constant inside pattern must have maximal arity") else (map test_pattern args; ())
- fun adjust_rule (_, PVar, _) = raise Compile ("pattern may not be a variable")
- | adjust_rule (_, PConst (_, []), _) = raise Compile ("cannot deal with rewrites that take no parameters")
- | adjust_rule (rule as (prems, p as PConst (c, args),t)) =
- let
- val patternvars_counted = count_patternvars p
- fun check_fv t = check_freevars patternvars_counted t
- val _ = if not (check_fv t) then raise Compile ("unbound variables on right hand side of rule") else ()
- val _ = if not (forall (fn (Guard (a,b)) => check_fv a andalso check_fv b) prems) then raise Compile ("unbound variables in guards") else ()
- val _ = map test_pattern args
- val len = length args
- val arity = arity_of c
- val lift = nlift 0
- fun addapps_tm n t = if n=0 then t else addapps_tm (n-1) (App (t, Var (n-1)))
- fun adjust_term n t = addapps_tm n (lift n t)
- fun adjust_guard n (Guard (a,b)) = Guard (lift n a, lift n b)
- in
- if len = arity then
- rule
- else if arity >= len then
- (map (adjust_guard (arity-len)) prems, PConst (c, args @ (rep (arity-len) PVar)), adjust_term (arity-len) t)
- else (raise Compile "internal error in adjust_rule")
- end
- fun beta_rule (prems, p, t) = ((prems, p, beta t) handle Match => raise Compile "beta_rule")
- in
- (arity, toplevel_arity, map (beta_rule o adjust_rule) rules)
- end
-
-fun print_term module arity_of toplevel_arity_of pattern_var_count pattern_lazy_var_count =
-let
- fun str x = string_of_int x
- fun protect_blank s = if exists_string Symbol.is_ascii_blank s then "(" ^ s ^")" else s
- val module_prefix = (case module of NONE => "" | SOME s => s^".")
- fun print_apps d f [] = f
- | print_apps d f (a::args) = print_apps d (module_prefix^"app "^(protect_blank f)^" "^(protect_blank (print_term d a))) args
- and print_call d (App (a, b)) args = print_call d a (b::args)
- | print_call d (Const c) args =
- (case arity_of c of
- NONE => print_apps d (module_prefix^"Const "^(str c)) args
- | SOME 0 => module_prefix^"C"^(str c)
- | SOME a =>
- let
- val len = length args
- in
- if a <= len then
- let
- val strict_a = (case toplevel_arity_of c of SOME sa => sa | NONE => a)
- val _ = if strict_a > a then raise Compile "strict" else ()
- val s = module_prefix^"c"^(str c)^(implode (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, strict_a))))
- val s = s^(implode (map (fn t => " (fn () => "^print_term d t^")") (List.drop (List.take (args, a), strict_a))))
- in
- print_apps d s (List.drop (args, a))
- end
- else
- let
- fun mk_apps n t = if n = 0 then t else mk_apps (n-1) (App (t, Var (n - 1)))
- fun mk_lambdas n t = if n = 0 then t else mk_lambdas (n-1) (Abs t)
- fun append_args [] t = t
- | append_args (c::cs) t = append_args cs (App (t, c))
- in
- print_term d (mk_lambdas (a-len) (mk_apps (a-len) (nlift 0 (a-len) (append_args args (Const c)))))
- end
- end)
- | print_call d t args = print_apps d (print_term d t) args
- and print_term d (Var x) =
- if x < d then
- "b"^(str (d-x-1))
- else
- let
- val n = pattern_var_count - (x-d) - 1
- val x = "x"^(str n)
- in
- if n < pattern_var_count - pattern_lazy_var_count then
- x
- else
- "("^x^" ())"
- end
- | print_term d (Abs c) = module_prefix^"Abs (fn b"^(str d)^" => "^(print_term (d + 1) c)^")"
- | print_term d t = print_call d t []
-in
- print_term 0
-end
-
-fun section n = if n = 0 then [] else (section (n-1))@[n-1]
-
-fun print_rule gnum arity_of toplevel_arity_of (guards, p, t) =
- let
- fun str x = Int.toString x
- fun print_pattern top n PVar = (n+1, "x"^(str n))
- | print_pattern top n (PConst (c, [])) = (n, (if top then "c" else "C")^(str c)^(if top andalso gnum > 0 then "_"^(str gnum) else ""))
- | print_pattern top n (PConst (c, args)) =
- let
- val f = (if top then "c" else "C")^(str c)^(if top andalso gnum > 0 then "_"^(str gnum) else "")
- val (n, s) = print_pattern_list 0 top (n, f) args
- in
- (n, s)
- end
- and print_pattern_list' counter top (n,p) [] = if top then (n,p) else (n,p^")")
- | print_pattern_list' counter top (n, p) (t::ts) =
- let
- val (n, t) = print_pattern false n t
- in
- print_pattern_list' (counter + 1) top (n, if top then p^" (a"^(str counter)^" as ("^t^"))" else p^", "^t) ts
- end
- and print_pattern_list counter top (n, p) (t::ts) =
- let
- val (n, t) = print_pattern false n t
- in
- print_pattern_list' (counter + 1) top (n, if top then p^" (a"^(str counter)^" as ("^t^"))" else p^" ("^t) ts
- end
- val c = (case p of PConst (c, _) => c | _ => raise Match)
- val (n, pattern) = print_pattern true 0 p
- val lazy_vars = the (arity_of c) - the (toplevel_arity_of c)
- fun print_tm tm = print_term NONE arity_of toplevel_arity_of n lazy_vars tm
- fun print_guard (Guard (a,b)) = "term_eq ("^(print_tm a)^") ("^(print_tm b)^")"
- val else_branch = "c"^(str c)^"_"^(str (gnum+1))^(implode (map (fn i => " a"^(str i)) (section (the (arity_of c)))))
- fun print_guards t [] = print_tm t
- | print_guards t (g::gs) = "if ("^(print_guard g)^")"^(implode (map (fn g => " andalso ("^(print_guard g)^")") gs))^" then ("^(print_tm t)^") else "^else_branch
- in
- (if null guards then gnum else gnum+1, pattern^" = "^(print_guards t guards))
- end
-
-fun group_rules rules =
- let
- fun add_rule (r as (_, PConst (c,_), _)) groups =
- let
- val rs = (case Inttab.lookup groups c of NONE => [] | SOME rs => rs)
- in
- Inttab.update (c, r::rs) groups
- end
- | add_rule _ _ = raise Compile "internal error group_rules"
- in
- fold_rev add_rule rules Inttab.empty
- end
-
-fun sml_prog name code rules =
- let
- val buffer = Unsynchronized.ref ""
- fun write s = (buffer := (!buffer)^s)
- fun writeln s = (write s; write "\n")
- fun writelist [] = ()
- | writelist (s::ss) = (writeln s; writelist ss)
- fun str i = Int.toString i
- val (inlinetab, rules) = inline_rules rules
- val (arity, toplevel_arity, rules) = adjust_rules rules
- val rules = group_rules rules
- val constants = Inttab.keys arity
- fun arity_of c = Inttab.lookup arity c
- fun toplevel_arity_of c = Inttab.lookup toplevel_arity c
- fun rep_str s n = implode (rep n s)
- fun indexed s n = s^(str n)
- fun string_of_tuple [] = ""
- | string_of_tuple (x::xs) = "("^x^(implode (map (fn s => ", "^s) xs))^")"
- fun string_of_args [] = ""
- | string_of_args (x::xs) = x^(implode (map (fn s => " "^s) xs))
- fun default_case gnum c =
- let
- val leftargs = implode (map (indexed " x") (section (the (arity_of c))))
- val rightargs = section (the (arity_of c))
- 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 message = "(\"unresolved lazy call: " ^ string_of_int c ^ "\")"
- 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
-
- fun eval_rules c =
- let
- val arity = the (arity_of c)
- val strict_arity = (case toplevel_arity_of c of NONE => arity | SOME sa => sa)
- fun eval_rule n =
- let
- val sc = string_of_int c
- val left = fold (fn i => fn s => "AbstractMachine.App ("^s^(indexed ", x" i)^")") (section n) ("AbstractMachine.Const "^sc)
- fun arg i =
- let
- val x = indexed "x" i
- val x = if i < n then "(eval bounds "^x^")" else x
- val x = if i < strict_arity then x else "(fn () => "^x^")"
- in
- x
- end
- val right = "c"^sc^" "^(string_of_args (map arg (section arity)))
- val right = fold_rev (fn i => fn s => "Abs (fn "^(indexed "x" i)^" => "^s^")") (List.drop (section arity, n)) right
- val right = if arity > 0 then right else "C"^sc
- in
- " | eval bounds ("^left^") = "^right
- end
- in
- map eval_rule (rev (section (arity + 1)))
- end
-
- fun convert_computed_rules (c: int) : string list =
- 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 [
- "structure "^name^" = struct",
- "",
- "datatype Term = Const of int | App of Term * Term | Abs of (Term -> Term)",
- " "^(implode (map (fn c => " | C"^(str c)^(mk_constr_type_args (the (arity_of c)))) constants)),
- ""]
- fun make_constr c argprefix = "(C"^(str c)^" "^(string_of_tuple (map (fn i => argprefix^(str i)) (section (the (arity_of c)))))^")"
- fun make_term_eq c = " | term_eq "^(make_constr c "a")^" "^(make_constr c "b")^" = "^
- (case the (arity_of c) of
- 0 => "true"
- | n =>
- let
- val eqs = map (fn i => "term_eq a"^(str i)^" b"^(str i)) (section n)
- val (eq, eqs) = (List.hd eqs, map (fn s => " andalso "^s) (List.tl eqs))
- in
- eq^(implode eqs)
- end)
- val _ = writelist [
- "fun term_eq (Const c1) (Const c2) = (c1 = c2)",
- " | term_eq (App (a1,a2)) (App (b1,b2)) = term_eq a1 b1 andalso term_eq a2 b2"]
- val _ = writelist (map make_term_eq constants)
- val _ = writelist [
- " | term_eq _ _ = false",
- ""
- ]
- val _ = writelist [
- "fun app (Abs a) b = a b",
- " | app a b = App (a, b)",
- ""]
- fun defcase gnum c = (case arity_of c of NONE => [] | SOME a => if a > 0 then [default_case gnum c] else [])
- fun writefundecl [] = ()
- | writefundecl (x::xs) = writelist ((("and "^x)::(map (fn s => " | "^s) xs)))
- fun list_group c = (case Inttab.lookup rules c of
- NONE => [defcase 0 c]
- | SOME rs =>
- let
- val rs =
- fold
- (fn r =>
- fn rs =>
- let
- val (gnum, l, rs) =
- (case rs of
- [] => (0, [], [])
- | (gnum, l)::rs => (gnum, l, rs))
- val (gnum', r) = print_rule gnum arity_of toplevel_arity_of r
- in
- if gnum' = gnum then
- (gnum, r::l)::rs
- else
- let
- val args = implode (map (fn i => " a"^(str i)) (section (the (arity_of c))))
- fun gnumc g = if g > 0 then "c"^(str c)^"_"^(str g)^args else "c"^(str c)^args
- val s = gnumc (gnum) ^ " = " ^ gnumc (gnum')
- in
- (gnum', [])::(gnum, s::r::l)::rs
- end
- end)
- rs []
- val rs = (case rs of [] => [(0,defcase 0 c)] | (gnum,l)::rs => (gnum, (defcase gnum c)@l)::rs)
- in
- rev (map (fn z => rev (snd z)) rs)
- end)
- val _ = map (fn z => (map writefundecl z; writeln "")) (map list_group constants)
- val _ = writelist [
- "fun convert (Const i) = AM_SML.Const i",
- " | convert (App (a, b)) = AM_SML.App (convert a, convert b)",
- " | convert (Abs _) = raise AM_SML.Run \"no abstraction in result allowed\""]
- fun make_convert c =
- let
- val args = map (indexed "a") (section (the (arity_of c)))
- val leftargs =
- case args of
- [] => ""
- | (x::xs) => "("^x^(implode (map (fn s => ", "^s) xs))^")"
- val args = map (indexed "convert a") (section (the (arity_of c)))
- val right = fold (fn x => fn s => "AM_SML.App ("^s^", "^x^")") args ("AM_SML.Const "^(str c))
- in
- " | 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)",
- " | eval bounds (AbstractMachine.Var i) = AM_SML.list_nth (bounds, i)"]
- 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.Computed t) = convert_computed t"]
- val _ = writelist [
- "",
- "fun export term = AM_SML.save_result (\""^code^"\", convert term)",
- "",
- "val _ = AM_SML.set_compiled_rewriter (fn t => (convert (eval [] t)))",
- "",
- "end"]
- in
- (arity, toplevel_arity, inlinetab, !buffer)
- end
-
-val guid_counter = Unsynchronized.ref 0
-fun get_guid () =
- let
- val c = !guid_counter
- val _ = guid_counter := !guid_counter + 1
- in
- (LargeInt.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c)
- end
-
-
-fun writeTextFile name s = File.write (Path.explode name) s
-
-fun use_source src = use_text ML_Env.local_context (1, "") false src
-
-fun compile cache_patterns const_arity eqs =
- let
- val guid = get_guid ()
- val code = Real.toString (random ())
- val module = "AMSML_"^guid
- val (arity, toplevel_arity, inlinetab, source) = sml_prog module code eqs
- val _ = case !dump_output of NONE => () | SOME p => writeTextFile p source
- val _ = compiled_rewriter := NONE
- val _ = use_source source
- in
- case !compiled_rewriter of
- NONE => raise Compile "broken link to compiled function"
- | SOME f => (module, code, arity, toplevel_arity, inlinetab, f)
- end
-
-
-fun run' (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t =
- let
- val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms")
- fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t)
- | inline (Var i) = Var i
- | inline (App (a, b)) = App (inline a, inline b)
- | inline (Abs m) = Abs (inline m)
- val t = beta (inline t)
- fun arity_of c = Inttab.lookup arity c
- fun toplevel_arity_of c = Inttab.lookup toplevel_arity c
- val term = print_term NONE arity_of toplevel_arity_of 0 0 t
- val source = "local open "^module^" in val _ = export ("^term^") end"
- val _ = writeTextFile "Gencode_call.ML" source
- val _ = clear_result ()
- val _ = use_source source
- in
- case !saved_result of
- NONE => raise Run "broken link to compiled code"
- | SOME (code', t) => (clear_result (); if code' = code then t else raise Run "link to compiled code was hijacked")
- end
-
-fun run (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t =
- let
- val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms")
- fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t)
- | 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
-
-fun discard p = ()
-
-end
--- a/src/Tools/Compute_Oracle/compute.ML Wed Jul 21 18:11:51 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,683 +0,0 @@
-(* Title: Tools/Compute_Oracle/compute.ML
- Author: Steven Obua
-*)
-
-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
- val make_with_cache : machine -> theory -> term list -> thm list -> computer
- val theory_of : computer -> theory
- val hyps_of : computer -> term list
- val shyps_of : computer -> sort list
- (* ! *) val update : computer -> thm list -> unit
- (* ! *) val update_with_cache : computer -> term list -> 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 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
-
-end
-
-structure Compute :> COMPUTE = struct
-
-open Report;
-
-datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML
-
-(* Terms are mapped to integer codes *)
-structure Encode :>
-sig
- type encoding
- val empty : encoding
- val insert : term -> encoding -> int * encoding
- val lookup_code : term -> encoding -> int option
- val lookup_term : int -> encoding -> term option
- val remove_code : int -> encoding -> encoding
- val remove_term : term -> encoding -> encoding
- val fold : ((term * int) -> 'a -> 'a) -> encoding -> 'a -> 'a
-end
-=
-struct
-
-type encoding = int * (int Termtab.table) * (term Inttab.table)
-
-val empty = (0, Termtab.empty, Inttab.empty)
-
-fun insert t (e as (count, term2int, int2term)) =
- (case Termtab.lookup term2int t of
- NONE => (count, (count+1, Termtab.update_new (t, count) term2int, Inttab.update_new (count, t) int2term))
- | SOME code => (code, e))
-
-fun lookup_code t (_, term2int, _) = Termtab.lookup term2int t
-
-fun lookup_term c (_, _, int2term) = Inttab.lookup int2term c
-
-fun remove_code c (e as (count, term2int, int2term)) =
- (case lookup_term c e of NONE => e | SOME t => (count, Termtab.delete t term2int, Inttab.delete c int2term))
-
-fun remove_term t (e as (count, term2int, int2term)) =
- (case lookup_code t e of NONE => e | SOME c => (count, Termtab.delete t term2int, Inttab.delete c int2term))
-
-fun fold f (_, term2int, _) = Termtab.fold f term2int
-
-end
-
-exception Make of string;
-exception Compute of string;
-
-local
- fun make_constant t ty encoding =
- let
- val (code, encoding) = Encode.insert t encoding
- in
- (encoding, AbstractMachine.Const code)
- end
-in
-
-fun remove_types encoding t =
- case t of
- Var (_, ty) => make_constant t ty encoding
- | Free (_, ty) => make_constant t ty encoding
- | Const (_, ty) => make_constant t ty encoding
- | Abs (_, ty, t') =>
- let val (encoding, t'') = remove_types encoding t' in
- (encoding, AbstractMachine.Abs t'')
- end
- | a $ b =>
- let
- val (encoding, a) = remove_types encoding a
- val (encoding, b) = remove_types encoding b
- in
- (encoding, AbstractMachine.App (a,b))
- end
- | Bound b => (encoding, AbstractMachine.Var b)
-end
-
-local
- fun type_of (Free (_, ty)) = ty
- | type_of (Const (_, ty)) = ty
- | type_of (Var (_, ty)) = ty
- | type_of _ = sys_error "infer_types: type_of error"
-in
-fun infer_types naming encoding =
- let
- fun infer_types _ bounds _ (AbstractMachine.Var v) = (Bound v, List.nth (bounds, v))
- | infer_types _ bounds _ (AbstractMachine.Const code) =
- let
- val c = the (Encode.lookup_term code encoding)
- in
- (c, type_of c)
- end
- | infer_types level bounds _ (AbstractMachine.App (a, b)) =
- let
- val (a, aty) = infer_types level bounds NONE a
- val (adom, arange) =
- case aty of
- Type ("fun", [dom, range]) => (dom, range)
- | _ => sys_error "infer_types: function type expected"
- val (b, bty) = infer_types level bounds (SOME adom) b
- in
- (a $ b, arange)
- end
- | infer_types level bounds (SOME (ty as Type ("fun", [dom, range]))) (AbstractMachine.Abs m) =
- let
- val (m, _) = infer_types (level+1) (dom::bounds) (SOME range) m
- in
- (Abs (naming level, dom, m), ty)
- end
- | infer_types _ _ NONE (AbstractMachine.Abs m) = sys_error "infer_types: cannot infer type of abstraction"
-
- fun infer ty term =
- let
- val (term', _) = infer_types 0 [] (SOME ty) term
- in
- term'
- end
- in
- infer
- end
-end
-
-datatype prog =
- ProgBarras of AM_Interpreter.program
- | ProgBarrasC of AM_Compiler.program
- | 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
-
-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 Unsynchronized.ref * naming)
- option Unsynchronized.ref
-
-fun theory_of (Computer (Unsynchronized.ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy
-fun hyps_of (Computer (Unsynchronized.ref (SOME (_,_,hyps,_,_,_,_)))) = hyps
-fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable)
-fun shyptab_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable
-fun stamp_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,stamp,_)))) = stamp
-fun prog_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,prog,_,_)))) = prog
-fun encoding_of (Computer (Unsynchronized.ref (SOME (_,encoding,_,_,_,_,_)))) = encoding
-fun set_encoding (Computer (r as Unsynchronized.ref (SOME (p1,encoding,p2,p3,p4,p5,p6)))) encoding' =
- (r := SOME (p1,encoding',p2,p3,p4,p5,p6))
-fun naming_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,_,n)))) = n
-fun set_naming (Computer (r as Unsynchronized.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
-
-fun thm2cthm th =
- let
- val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th
- val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else ()
- in
- ComputeThm (hyps, shyps, prop)
- end
-
-fun make_internal machine thy stamp encoding cache_pattern_terms raw_ths =
- let
- fun transfer (x:thm) = Thm.transfer thy x
- val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths
-
- fun make_pattern encoding n vars (var as AbstractMachine.Abs _) =
- raise (Make "no lambda abstractions allowed in pattern")
- | make_pattern encoding n vars (var as AbstractMachine.Var _) =
- raise (Make "no bound variables allowed in pattern")
- | make_pattern encoding n vars (AbstractMachine.Const code) =
- (case the (Encode.lookup_term code encoding) of
- Var _ => ((n+1, Inttab.update_new (code, n) vars, AbstractMachine.PVar)
- handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed"))
- | _ => (n, vars, AbstractMachine.PConst (code, [])))
- | make_pattern encoding n vars (AbstractMachine.App (a, b)) =
- let
- val (n, vars, pa) = make_pattern encoding n vars a
- val (n, vars, pb) = make_pattern encoding n vars b
- in
- case pa of
- AbstractMachine.PVar =>
- raise (Make "patterns may not start with a variable")
- | AbstractMachine.PConst (c, args) =>
- (n, vars, AbstractMachine.PConst (c, args@[pb]))
- end
-
- fun thm2rule (encoding, hyptable, shyptable) th =
- let
- val (ComputeThm (hyps, shyps, prop)) = th
- val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable
- val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable
- val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop)
- val (a, b) = Logic.dest_equals prop
- handle TERM _ => raise (Make "theorems must be meta-level equations (with optional guards)")
- val a = Envir.eta_contract a
- val b = Envir.eta_contract b
- val prems = map Envir.eta_contract prems
-
- val (encoding, left) = remove_types encoding a
- val (encoding, right) = remove_types encoding b
- fun remove_types_of_guard encoding g =
- (let
- val (t1, t2) = Logic.dest_equals g
- val (encoding, t1) = remove_types encoding t1
- val (encoding, t2) = remove_types encoding t2
- in
- (encoding, AbstractMachine.Guard (t1, t2))
- end handle TERM _ => raise (Make "guards must be meta-level equations"))
- 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, [])
-
- (* Principally, a check should be made here to see if the (meta-) hyps contain any of the variables of the rule.
- As it is, all variables of the rule are schematic, and there are no schematic variables in meta-hyps, therefore
- this check can be left out. *)
-
- val (vcount, vars, pattern) = make_pattern encoding 0 Inttab.empty left
- val _ = (case pattern of
- AbstractMachine.PVar =>
- raise (Make "patterns may not start with a variable")
- (* | AbstractMachine.PConst (_, []) =>
- (print th; raise (Make "no parameter rewrite found"))*)
- | _ => ())
-
- (* finally, provide a function for renaming the
- pattern bound variables on the right hand side *)
-
- fun rename level vars (var as AbstractMachine.Var _) = var
- | rename level vars (c as AbstractMachine.Const code) =
- (case Inttab.lookup vars code of
- NONE => c
- | SOME n => AbstractMachine.Var (vcount-n-1+level))
- | rename level vars (AbstractMachine.App (a, b)) =
- AbstractMachine.App (rename level vars a, rename level vars b)
- | rename level vars (AbstractMachine.Abs m) =
- AbstractMachine.Abs (rename (level+1) vars m)
-
- fun rename_guard (AbstractMachine.Guard (a,b)) =
- AbstractMachine.Guard (rename 0 vars a, rename 0 vars b)
- in
- ((encoding, hyptable, shyptable), (map rename_guard prems, pattern, rename 0 vars right))
- end
-
- val ((encoding, hyptable, shyptable), rules) =
- fold_rev (fn th => fn (encoding_hyptable, rules) =>
- let
- val (encoding_hyptable, rule) = thm2rule encoding_hyptable th
- in (encoding_hyptable, rule::rules) end)
- ths ((encoding, Termtab.empty, Sorttab.empty), [])
-
- fun make_cache_pattern t (encoding, cache_patterns) =
- let
- val (encoding, a) = remove_types encoding t
- val (_,_,p) = make_pattern encoding 0 Inttab.empty a
- in
- (encoding, p::cache_patterns)
- end
-
- val (encoding, cache_patterns) = fold_rev make_cache_pattern cache_pattern_terms (encoding, [])
-
- fun arity (Type ("fun", [a,b])) = 1 + arity b
- | arity _ = 0
-
- fun make_arity (Const (s, _), i) tab =
- (Inttab.update (i, arity (Sign.the_const_type thy s)) tab handle TYPE _ => tab)
- | make_arity _ tab = tab
-
- val const_arity_tab = Encode.fold make_arity encoding Inttab.empty
- fun const_arity x = Inttab.lookup const_arity_tab x
-
- val prog =
- case machine of
- BARRAS => ProgBarras (AM_Interpreter.compile cache_patterns const_arity rules)
- | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile cache_patterns const_arity rules)
- | HASKELL => ProgHaskell (AM_GHC.compile cache_patterns const_arity rules)
- | SML => ProgSML (AM_SML.compile cache_patterns const_arity rules)
-
- fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
-
- val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable
-
- in (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end
-
-fun make_with_cache machine thy cache_patterns raw_thms =
- Computer (Unsynchronized.ref (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty cache_patterns raw_thms)))
-
-fun make machine thy raw_thms = make_with_cache machine thy [] raw_thms
-
-fun update_with_cache computer cache_patterns raw_thms =
- let
- val c = make_internal (machine_of_prog (prog_of computer)) (theory_of computer) (stamp_of computer)
- (encoding_of computer) cache_patterns raw_thms
- val _ = (ref_of computer) := SOME c
- in
- ()
- end
-
-fun update computer raw_thms = update_with_cache computer [] raw_thms
-
-fun discard computer =
- let
- 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
- ()
- 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! *)
-(* ------------------------------------------------------------------------------------- *)
-
-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))
-
-val (_, export_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (Binding.name "compute", fn (thy, 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: " ^
- commas (map (Syntax.string_of_sort_global thy) shyps))
- else ()
- in
- Thm.cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop)
- end)));
-
-fun export_thm thy hyps shyps prop =
- let
- val th = export_oracle (thy, hyps, shyps, prop)
- val hyps = map (fn h => Thm.assume (cterm_of thy h)) hyps
- in
- fold (fn h => fn p => Thm.implies_elim p h) hyps th
- end
-
-(* --------- Rewrite ----------- *)
-
-fun rewrite computer ct =
- let
- val thy = Thm.theory_of_cterm ct
- val {t=t',T=ty,...} = 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 ------------ *)
-
-datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int
- | Prem of AbstractMachine.term
-datatype theorem = Theorem of theory_ref * unit Unsynchronized.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))
-
- (* 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 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 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
-
- val vs = fold compute_inst insts (varsubst_of_theorem th)
-in
- update_varsubst vs th
-end
-
-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
- 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 splicein n l L = List.take (L, n) @ l @ List.drop (L, n+1)
-
-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 = Syntax.string_of_term_global Pure.thy
- (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
-
-fun prem2term (Prem t) = t
- | prem2term (EqPrem (a,b,_,eq)) =
- AbstractMachine.App (AbstractMachine.App (AbstractMachine.Const eq, a), b)
-
-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 Theory.subthy (thy1, thy2) then thy2
- else if Theory.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
-
--- a/src/Tools/Compute_Oracle/linker.ML Wed Jul 21 18:11:51 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,477 +0,0 @@
-(* Title: Tools/Compute_Oracle/linker.ML
- Author: Steven Obua
-
-This module solves the problem that the computing oracle does not
-instantiate polymorphic rules. By going through the PCompute
-interface, all possible instantiations are resolved by compiling new
-programs, if necessary. The obvious disadvantage of this approach is
-that in the worst case for each new term to be rewritten, a new
-program may be compiled.
-*)
-
-(*
- Given constants/frees c_1::t_1, c_2::t_2, ...., c_n::t_n,
- and constants/frees d_1::d_1, d_2::s_2, ..., d_m::s_m
-
- Find all substitutions S such that
- a) the domain of S is tvars (t_1, ..., t_n)
- b) there are indices i_1, ..., i_k, and j_1, ..., j_k with
- 1. S (c_i_1::t_i_1) = d_j_1::s_j_1, ..., S (c_i_k::t_i_k) = d_j_k::s_j_k
- 2. tvars (t_i_1, ..., t_i_k) = tvars (t_1, ..., t_n)
-*)
-signature LINKER =
-sig
- exception Link of string
-
- datatype constant = Constant of bool * string * typ
- val constant_of : term -> constant
-
- type instances
- type subst = Type.tyenv
-
- val empty : constant list -> instances
- val typ_of_constant : constant -> typ
- val add_instances : theory -> instances -> constant list -> subst list * instances
- val substs_of : instances -> subst list
- val is_polymorphic : constant -> bool
- val distinct_constants : constant list -> constant list
- val collect_consts : term list -> constant list
-end
-
-structure Linker : LINKER = struct
-
-exception Link of string;
-
-type subst = Type.tyenv
-
-datatype constant = Constant of bool * string * typ
-fun constant_of (Const (name, ty)) = Constant (false, name, ty)
- | constant_of (Free (name, ty)) = Constant (true, name, ty)
- | constant_of _ = raise Link "constant_of"
-
-fun bool_ord (x,y) = if x then (if y then EQUAL else GREATER) else (if y then LESS else EQUAL)
-fun constant_ord (Constant (x1,x2,x3), Constant (y1,y2,y3)) = (prod_ord (prod_ord bool_ord fast_string_ord) Term_Ord.typ_ord) (((x1,x2),x3), ((y1,y2),y3))
-fun constant_modty_ord (Constant (x1,x2,_), Constant (y1,y2,_)) = (prod_ord bool_ord fast_string_ord) ((x1,x2), (y1,y2))
-
-
-structure Consttab = Table(type key = constant val ord = constant_ord);
-structure ConsttabModTy = Table(type key = constant val ord = constant_modty_ord);
-
-fun typ_of_constant (Constant (_, _, ty)) = ty
-
-val empty_subst = (Vartab.empty : Type.tyenv)
-
-fun merge_subst (A:Type.tyenv) (B:Type.tyenv) =
- SOME (Vartab.fold (fn (v, t) =>
- fn tab =>
- (case Vartab.lookup tab v of
- NONE => Vartab.update (v, t) tab
- | SOME t' => if t = t' then tab else raise Type.TYPE_MATCH)) A B)
- handle Type.TYPE_MATCH => NONE
-
-fun subst_ord (A:Type.tyenv, B:Type.tyenv) =
- (list_ord (prod_ord Term_Ord.fast_indexname_ord (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))) (Vartab.dest A, Vartab.dest B)
-
-structure Substtab = Table(type key = Type.tyenv val ord = subst_ord);
-
-fun substtab_union c = Substtab.fold Substtab.update c
-fun substtab_unions [] = Substtab.empty
- | substtab_unions [c] = c
- | substtab_unions (c::cs) = substtab_union c (substtab_unions cs)
-
-datatype instances = Instances of unit ConsttabModTy.table * Type.tyenv Consttab.table Consttab.table * constant list list * unit Substtab.table
-
-fun is_polymorphic (Constant (_, _, ty)) = not (null (Term.add_tvarsT ty []))
-
-fun distinct_constants cs =
- Consttab.keys (fold (fn c => Consttab.update (c, ())) cs Consttab.empty)
-
-fun empty cs =
- let
- val cs = distinct_constants (filter is_polymorphic cs)
- val old_cs = cs
-(* fun collect_tvars ty tab = fold (fn v => fn tab => Typtab.update (TVar v, ()) tab) (OldTerm.typ_tvars ty) tab
- val tvars_count = length (Typtab.keys (fold (fn c => fn tab => collect_tvars (typ_of_constant c) tab) cs Typtab.empty))
- fun tvars_of ty = collect_tvars ty Typtab.empty
- val cs = map (fn c => (c, tvars_of (typ_of_constant c))) cs
-
- fun tyunion A B =
- Typtab.fold
- (fn (v,()) => fn tab => Typtab.update (v, case Typtab.lookup tab v of NONE => 1 | SOME n => n+1) tab)
- A B
-
- fun is_essential A B =
- Typtab.fold
- (fn (v, ()) => fn essential => essential orelse (case Typtab.lookup B v of NONE => raise Link "is_essential" | SOME n => n=1))
- A false
-
- fun add_minimal (c', tvs') (tvs, cs) =
- let
- val tvs = tyunion tvs' tvs
- val cs = (c', tvs')::cs
- in
- if forall (fn (c',tvs') => is_essential tvs' tvs) cs then
- SOME (tvs, cs)
- else
- NONE
- end
-
- fun is_spanning (tvs, _) = (length (Typtab.keys tvs) = tvars_count)
-
- fun generate_minimal_subsets subsets [] = subsets
- | generate_minimal_subsets subsets (c::cs) =
- let
- val subsets' = map_filter (add_minimal c) subsets
- in
- generate_minimal_subsets (subsets@subsets') cs
- end*)
-
- val minimal_subsets = [old_cs] (*map (fn (tvs, cs) => map fst cs) (filter is_spanning (generate_minimal_subsets [(Typtab.empty, [])] cs))*)
-
- val constants = Consttab.keys (fold (fold (fn c => Consttab.update (c, ()))) minimal_subsets Consttab.empty)
-
- in
- Instances (
- fold (fn c => fn tab => ConsttabModTy.update (c, ()) tab) constants ConsttabModTy.empty,
- Consttab.make (map (fn c => (c, Consttab.empty : Type.tyenv Consttab.table)) constants),
- minimal_subsets, Substtab.empty)
- end
-
-local
-fun calc ctab substtab [] = substtab
- | calc ctab substtab (c::cs) =
- let
- val csubsts = map snd (Consttab.dest (the (Consttab.lookup ctab c)))
- fun merge_substs substtab subst =
- Substtab.fold (fn (s,_) =>
- fn tab =>
- (case merge_subst subst s of NONE => tab | SOME s => Substtab.update (s, ()) tab))
- substtab Substtab.empty
- val substtab = substtab_unions (map (merge_substs substtab) csubsts)
- in
- calc ctab substtab cs
- end
-in
-fun calc_substs ctab (cs:constant list) = calc ctab (Substtab.update (empty_subst, ()) Substtab.empty) cs
-end
-
-fun add_instances thy (Instances (cfilter, ctab,minsets,substs)) cs =
- let
-(* val _ = writeln (makestring ("add_instances: ", length_cs, length cs, length (Consttab.keys ctab)))*)
- fun calc_instantiations (constant as Constant (free, name, ty)) instantiations =
- Consttab.fold (fn (constant' as Constant (free', name', ty'), insttab) =>
- fn instantiations =>
- if free <> free' orelse name <> name' then
- instantiations
- else case Consttab.lookup insttab constant of
- SOME _ => instantiations
- | NONE => ((constant', (constant, Sign.typ_match thy (ty', ty) empty_subst))::instantiations
- handle TYPE_MATCH => instantiations))
- ctab instantiations
- val instantiations = fold calc_instantiations cs []
- (*val _ = writeln ("instantiations = "^(makestring (length instantiations)))*)
- fun update_ctab (constant', entry) ctab =
- (case Consttab.lookup ctab constant' of
- NONE => raise Link "internal error: update_ctab"
- | SOME tab => Consttab.update (constant', Consttab.update entry tab) ctab)
- val ctab = fold update_ctab instantiations ctab
- val new_substs = fold (fn minset => fn substs => substtab_union (calc_substs ctab minset) substs)
- minsets Substtab.empty
- val (added_substs, substs) =
- Substtab.fold (fn (ns, _) =>
- fn (added, substtab) =>
- (case Substtab.lookup substs ns of
- NONE => (ns::added, Substtab.update (ns, ()) substtab)
- | SOME () => (added, substtab)))
- new_substs ([], substs)
- in
- (added_substs, Instances (cfilter, ctab, minsets, substs))
- end
-
-fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
-
-local
- fun get_thm thmname = PureThy.get_thm (theory "Main") thmname
- val eq_th = get_thm "HOL.eq_reflection"
-in
- fun eq_to_meta th = (eq_th OF [th] handle THM _ => th)
-end
-
-
-local
-
-fun collect (Var x) tab = tab
- | collect (Bound _) tab = tab
- | collect (a $ b) tab = collect b (collect a tab)
- | collect (Abs (_, _, body)) tab = collect body tab
- | collect t tab = Consttab.update (constant_of t, ()) tab
-
-in
- fun collect_consts tms = Consttab.keys (fold collect tms Consttab.empty)
-end
-
-end
-
-signature PCOMPUTE =
-sig
- type pcomputer
-
- val make : Compute.machine -> theory -> thm list -> Linker.constant list -> pcomputer
- val make_with_cache : Compute.machine -> theory -> term list -> thm list -> Linker.constant list -> pcomputer
-
- 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
-
-structure PCompute : PCOMPUTE = struct
-
-exception PCompute of string
-
-datatype theorem = MonoThm of thm | PolyThm of thm * Linker.instances * thm list
-datatype pattern = MonoPattern of term | PolyPattern of term * Linker.instances * term list
-
-datatype pcomputer =
- PComputer of theory_ref * Compute.computer * theorem list Unsynchronized.ref *
- pattern list Unsynchronized.ref
-
-(*fun collect_consts (Var x) = []
- | collect_consts (Bound _) = []
- | collect_consts (a $ b) = (collect_consts a)@(collect_consts b)
- | collect_consts (Abs (_, _, body)) = collect_consts body
- | collect_consts t = [Linker.constant_of t]*)
-
-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)
- val (left, right) = Logic.dest_equals th
- in
- (Linker.collect_consts [left], Linker.collect_consts (right::prems))
- end
-
-fun create_theorem th =
-let
- val (left, right) = collect_consts_of_thm th
- val polycs = filter Linker.is_polymorphic left
- val tytab = fold (fn p => fn tab => fold (fn n => fn tab => Typtab.update (TVar n, ()) tab) (OldTerm.typ_tvars (Linker.typ_of_constant p)) tab) polycs Typtab.empty
- fun check_const (c::cs) cs' =
- let
- val tvars = OldTerm.typ_tvars (Linker.typ_of_constant c)
- val wrong = fold (fn n => fn wrong => wrong orelse is_none (Typtab.lookup tytab (TVar n))) tvars false
- in
- if wrong then raise PCompute "right hand side of theorem contains type variables which do not occur on the left hand side"
- else
- if null (tvars) then
- check_const cs (c::cs')
- else
- check_const cs cs'
- end
- | check_const [] cs' = cs'
- val monocs = check_const right []
-in
- if null (polycs) then
- (monocs, MonoThm th)
- else
- (monocs, PolyThm (th, Linker.empty polycs, []))
-end
-
-fun create_pattern pat =
-let
- val cs = Linker.collect_consts [pat]
- val polycs = filter Linker.is_polymorphic cs
-in
- if null (polycs) then
- MonoPattern pat
- else
- PolyPattern (pat, Linker.empty polycs, [])
-end
-
-fun create_computer machine thy pats ths =
- let
- fun add (MonoThm th) ths = th::ths
- | add (PolyThm (_, _, ths')) ths = ths'@ths
- fun addpat (MonoPattern p) pats = p::pats
- | addpat (PolyPattern (_, _, ps)) pats = ps@pats
- val ths = fold_rev add ths []
- val pats = fold_rev addpat pats []
- in
- Compute.make_with_cache machine thy pats ths
- end
-
-fun update_computer computer pats ths =
- let
- fun add (MonoThm th) ths = th::ths
- | add (PolyThm (_, _, ths')) ths = ths'@ths
- fun addpat (MonoPattern p) pats = p::pats
- | addpat (PolyPattern (_, _, ps)) pats = ps@pats
- val ths = fold_rev add ths []
- val pats = fold_rev addpat pats []
- in
- Compute.update_with_cache computer pats 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)
-
-fun add_monos thy monocs pats ths =
- let
- val changed = Unsynchronized.ref false
- fun add monocs (th as (MonoThm _)) = ([], th)
- | add monocs (PolyThm (th, instances, instanceths)) =
- let
- val (newsubsts, instances) = Linker.add_instances thy instances monocs
- val _ = if not (null newsubsts) then changed := true else ()
- val newths = map (fn subst => Thm.instantiate (conv_subst thy subst, []) th) newsubsts
-(* val _ = if not (null newths) then (print ("added new theorems: ", newths); ()) else ()*)
- val newmonos = fold (fn th => fn monos => (snd (collect_consts_of_thm th))@monos) newths []
- in
- (newmonos, PolyThm (th, instances, instanceths@newths))
- end
- fun addpats monocs (pat as (MonoPattern _)) = pat
- | addpats monocs (PolyPattern (p, instances, instancepats)) =
- let
- val (newsubsts, instances) = Linker.add_instances thy instances monocs
- val _ = if not (null newsubsts) then changed := true else ()
- val newpats = map (fn subst => Envir.subst_term_types subst p) newsubsts
- in
- PolyPattern (p, instances, instancepats@newpats)
- end
- fun step monocs ths =
- fold_rev (fn th =>
- fn (newmonos, ths) =>
- let
- val (newmonos', th') = add monocs th
- in
- (newmonos'@newmonos, th'::ths)
- end)
- ths ([], [])
- fun loop monocs pats ths =
- let
- val (monocs', ths') = step monocs ths
- val pats' = map (addpats monocs) pats
- in
- if null (monocs') then
- (pats', ths')
- else
- loop monocs' pats' ths'
- end
- val result = loop monocs pats ths
- in
- (!changed, result)
- end
-
-datatype cthm = ComputeThm of term list * sort list * term
-
-fun thm2cthm th =
- let
- val {hyps, prop, shyps, ...} = Thm.rep_thm th
- in
- ComputeThm (hyps, shyps, prop)
- end
-
-val cthm_ord' = prod_ord (prod_ord (list_ord Term_Ord.term_ord) (list_ord Term_Ord.sort_ord)) Term_Ord.term_ord
-
-fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
-
-structure CThmtab = Table(type key = cthm val ord = cthm_ord)
-
-fun remove_duplicates ths =
- let
- val counter = Unsynchronized.ref 0
- val tab = Unsynchronized.ref (CThmtab.empty : unit CThmtab.table)
- val thstab = Unsynchronized.ref (Inttab.empty : thm Inttab.table)
- fun update th =
- let
- val key = thm2cthm th
- in
- case CThmtab.lookup (!tab) key of
- NONE => ((tab := CThmtab.update_new (key, ()) (!tab)); thstab := Inttab.update_new (!counter, th) (!thstab); counter := !counter + 1)
- | _ => ()
- end
- val _ = map update ths
- in
- map snd (Inttab.dest (!thstab))
- end
-
-fun make_with_cache machine thy pats 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 pats = map create_pattern pats
- val (_, (pats, ths)) = add_monos thy monocs pats ths
- val computer = create_computer machine thy pats ths
- in
- PComputer (Theory.check_thy thy, computer, Unsynchronized.ref ths, Unsynchronized.ref pats)
- end
-
-fun make machine thy ths cs = make_with_cache machine thy [] ths cs
-
-fun add_instances (PComputer (thyref, computer, rths, rpats)) cs =
- let
- val thy = Theory.deref thyref
- val (changed, (pats, ths)) = add_monos thy cs (!rpats) (!rths)
- in
- if changed then
- (update_computer computer pats ths;
- rths := ths;
- rpats := pats;
- 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 simplify pc th = Compute.simplify (computer_of pc) th
-
-fun make_theorem pc th vars =
- let
- val _ = add_instances' pc [prop_of th]
-
- in
- 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
--- a/src/Tools/Compute_Oracle/report.ML Wed Jul 21 18:11:51 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-structure Report =
-struct
-
-local
-
- val report_depth = Unsynchronized.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 = #message (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
--- a/src/Tools/WWW_Find/find_theorems.ML Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML Wed Jul 21 18:13:15 2010 +0200
@@ -207,7 +207,7 @@
fun do_find () =
let
- val ctxt = ProofContext.init_global (theory thy_name);
+ val ctxt = ProofContext.init_global (Thy_Info.get_theory thy_name);
val query = get_query ();
val (othmslen, thms) = apsnd rev
(Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query);
--- a/src/Tools/jEdit/README Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Tools/jEdit/README Wed Jul 21 18:13:15 2010 +0200
@@ -44,14 +44,19 @@
e.g. between the editor and the Console plugin, which is a standard
swing text box. Similar for search boxes etc.
+- ToggleButton selected state is not rendered if window focus is lost,
+ which is probably a genuine feature of the Apple look-and-feel.
+
- Anti-aliasing does not really work as well as for Linux or Windows.
(General Apple/Swing problem?)
- Font.createFont mangles the font family of non-regular fonts,
e.g. bold. IsabelleText font files need to be installed manually.
-- ToggleButton selected state is not rendered if window focus is lost,
- which is probably a genuine feature of the Apple look-and-feel.
+- Missing glyphs are collected from other fonts (like Emacs, Firefox).
+ This is actually an advantage over the Oracle/Sun JVM on Windows or
+ Linux, but probably also the deeper reason for the other oddities of
+ Apple font management.
Windows/Linux
--- a/src/Tools/jEdit/src/jedit/document_model.scala Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Wed Jul 21 18:13:15 2010 +0200
@@ -100,7 +100,7 @@
private val edits_buffer = new mutable.ListBuffer[Text_Edit] // owned by Swing thread
- private val edits_delay = Swing_Thread.delay_last(300) { // FIXME input_delay property
+ private val edits_delay = Swing_Thread.delay_last(session.input_delay) {
if (!edits_buffer.isEmpty) {
val new_change = current_change().edit(session, edits_buffer.toList)
edits_buffer.clear
--- a/src/Tools/jEdit/src/jedit/document_view.scala Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Wed Jul 21 18:13:15 2010 +0200
@@ -211,23 +211,14 @@
/* caret handling */
- def selected_command: Option[Command] =
- model.recent_document().command_at(text_area.getCaretPosition) match {
- case Some((command, _)) => Some(command)
- case None => None
- }
+ def selected_command(): Option[Command] =
+ model.recent_document().proper_command_at(text_area.getCaretPosition)
- private val caret_listener = new CaretListener
- {
- private var last_selected_command: Option[Command] = None
- override def caretUpdate(e: CaretEvent)
- {
- val selected = selected_command
- if (selected != last_selected_command) {
- last_selected_command = selected
- if (selected.isDefined) session.indicate_command_change(selected.get)
- }
+ private val caret_listener = new CaretListener {
+ private val delay = Swing_Thread.delay_last(session.input_delay) {
+ session.perspective.event(Session.Perspective)
}
+ override def caretUpdate(e: CaretEvent) { delay() }
}
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Wed Jul 21 18:11:51 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Wed Jul 21 18:13:15 2010 +0200
@@ -46,20 +46,21 @@
}
}
- private def handle_caret()
- {
+ private def handle_perspective(): Boolean =
Swing_Thread.now {
Document_View(view.getTextArea) match {
- case Some(doc_view) => current_command = doc_view.selected_command
- case None =>
+ case Some(doc_view) =>
+ val cmd = doc_view.selected_command()
+ if (current_command == cmd) false
+ else { current_command = cmd; true }
+ case None => false
}
}
- }
private def handle_update(restriction: Option[Set[Command]] = None)
{
Swing_Thread.now {
- if (follow_caret) handle_caret()
+ if (follow_caret) handle_perspective()
Document_View(view.getTextArea) match {
case Some(doc_view) =>
current_command match {
@@ -87,6 +88,7 @@
react {
case Session.Global_Settings => handle_resize()
case Command_Set(changed) => handle_update(Some(changed))
+ case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
}
}
@@ -94,21 +96,23 @@
override def init()
{
+ Isabelle.session.global_settings += main_actor
Isabelle.session.commands_changed += main_actor
- Isabelle.session.global_settings += main_actor
+ Isabelle.session.perspective += main_actor
}
override def exit()
{
+ Isabelle.session.global_settings -= main_actor
Isabelle.session.commands_changed -= main_actor
- Isabelle.session.global_settings -= main_actor
+ Isabelle.session.perspective -= main_actor
}
/* resize */
addComponentListener(new ComponentAdapter {
- val delay = Swing_Thread.delay_last(500) { handle_resize() } // FIXME update_delay property
+ val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() }
override def componentResized(e: ComponentEvent) { delay() }
})
@@ -138,7 +142,7 @@
auto_update.tooltip = "Indicate automatic update following cursor movement"
private val update = new Button("Update") {
- reactions += { case ButtonClicked(_) => handle_caret(); handle_update() }
+ reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() }
}
update.tooltip = "Update display according to the command at cursor position"