--- a/src/HOL/Matrix/cplex/MatrixLP.thy Thu May 31 20:55:32 2007 +0200
+++ b/src/HOL/Matrix/cplex/MatrixLP.thy Thu May 31 20:55:33 2007 +0200
@@ -4,7 +4,7 @@
*)
theory MatrixLP
-imports Cplex
+imports Cplex "~~/src/Tools/Compute_Oracle/Compute_Oracle"
uses ("matrixlp.ML")
begin
--- a/src/Pure/IsaMakefile Thu May 31 20:55:32 2007 +0200
+++ b/src/Pure/IsaMakefile Thu May 31 20:55:33 2007 +0200
@@ -58,18 +58,17 @@
Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML Thy/latex.ML \
Thy/ml_context.ML Thy/present.ML Thy/term_style.ML Thy/thm_database.ML \
Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \
- Thy/thy_output.ML Tools/ROOT.ML Tools/am_compiler.ML Tools/am_interpreter.ML \
- Tools/am_util.ML Tools/class_package.ML Tools/codegen_consts.ML \
- Tools/codegen_data.ML Tools/codegen_func.ML Tools/codegen_funcgr.ML \
- Tools/codegen_names.ML Tools/codegen_package.ML Tools/codegen_serializer.ML \
- Tools/codegen_thingol.ML Tools/compute.ML Tools/invoke.ML Tools/nbe.ML \
- Tools/nbe_codegen.ML Tools/nbe_eval.ML Tools/xml_syntax.ML assumption.ML \
- axclass.ML codegen.ML compress.ML conjunction.ML consts.ML context.ML conv.ML \
- defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML install_pp.ML \
- library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML \
- old_goals.ML pattern.ML proofterm.ML pure_thy.ML search.ML sign.ML \
- simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML \
- theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML
+ Thy/thy_output.ML Tools/ROOT.ML Tools/class_package.ML \
+ Tools/codegen_consts.ML Tools/codegen_data.ML Tools/codegen_func.ML \
+ Tools/codegen_funcgr.ML Tools/codegen_names.ML Tools/codegen_package.ML \
+ Tools/codegen_serializer.ML Tools/codegen_thingol.ML Tools/invoke.ML \
+ Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML Tools/xml_syntax.ML \
+ assumption.ML axclass.ML codegen.ML compress.ML conjunction.ML consts.ML \
+ context.ML conv.ML defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML \
+ install_pp.ML library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML \
+ name.ML net.ML old_goals.ML pattern.ML proofterm.ML pure_thy.ML search.ML \
+ sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML \
+ term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML
@./mk
--- a/src/Pure/Tools/ROOT.ML Thu May 31 20:55:32 2007 +0200
+++ b/src/Pure/Tools/ROOT.ML Thu May 31 20:55:33 2007 +0200
@@ -9,7 +9,6 @@
(*derived theory and proof elements*)
use "invoke.ML";
-(* use "class_package.ML"; see Pure/Isar/ROOT.ML *)
(*code generator, 1st generation*)
use "../codegen.ML";
@@ -21,12 +20,6 @@
use "codegen_serializer.ML";
use "codegen_package.ML";
-(*Steven Obua's evaluator*)
-use "am_interpreter.ML";
-use "am_compiler.ML";
-use "am_util.ML";
-use "compute.ML";
-
(*norm-by-eval*)
use "nbe_eval.ML";
use "nbe_codegen.ML";
--- a/src/Pure/Tools/am_compiler.ML Thu May 31 20:55:32 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,238 +0,0 @@
-(* Title: Pure/Tools/am_compiler.ML
- ID: $Id$
- Author: Steven Obua
-*)
-
-signature COMPILING_AM =
-sig
- include ABSTRACT_MACHINE
-
- datatype closure = CVar of int | CConst of int
- | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
-
- val set_compiled_rewriter : (term -> closure) -> 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;
-
-datatype term = Var of int | Const of int | App of term * term | Abs of term
-
-datatype pattern = PVar | PConst of int * (pattern list)
-
-datatype closure = CVar of int | CConst of int
- | CApp of closure * closure | CAbs of closure
- | Closure of (closure list) * closure
-
-val compiled_rewriter = ref (NONE:(term -> closure)Option.option)
-
-fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
-
-type program = (term -> term)
-
-datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
-
-exception Compile of string;
-exception Run of string;
-
-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)
-
-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")
-
-fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
- | strip_closure args x = (x, args)
-
-(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
- check_freevars 0 t iff t is closed*)
-fun check_freevars free (Var x) = x < free
- | check_freevars free (Const c) = true
- | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
- | check_freevars free (Abs m) = check_freevars (free+1) m
-
-fun count_patternvars PVar = 1
- | count_patternvars (PConst (_, ps)) =
- List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
-
-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 ^ ")"
-
- 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
- "lookup stack "^pattern^" = weak 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]
-
-fun load_rules sname name prog =
- let
- (* FIXME consider using more readable/efficient Buffer.empty |> fold Buffer.add etc. *)
- val buffer = 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 = 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",
- ""]
- val _ = (case prog of
- r::rs => (writeln ("fun "^(print_rule r));
- map (fn r => writeln(" | "^(print_rule r))) rs;
- writeln (" | lookup stack clos = weak_last stack clos"); ())
- | [] => (writeln "fun lookup stack clos = weak_last stack clos"))
- val _ = writelist [
- "and weak stack (Closure (e, App (a, b))) = weak (SAppL (Closure (e, b), stack)) (Closure (e, a))",
- " | weak (SAppL (b, stack)) (Closure (e, Abs m)) = weak stack (Closure (b::e, m))",
- " | weak stack (clos as Closure (_, Abs _)) = weak_last stack clos",
- " | weak stack (Closure (e, Var n)) = weak stack ("^sname^".list_nth (e, n) handle _ => (Var (n-(length e))))",
- " | weak stack (Closure (e, c)) = weak stack c",
- " | weak stack clos = lookup stack clos",
- "and weak_last (SAppR (a, stack)) b = weak stack (App(a, b))",
- " | weak_last (SAppL (b, stack)) a = weak (SAppR (a, stack)) b",
- " | weak_last stack c = (stack, c)",
- "",
- "fun lift n (v as Var m) = if m < n then v else Var (m+1)",
- " | lift n (Abs t) = Abs (lift (n+1) t)",
- " | lift n (App (a,b)) = App (lift n a, lift n b)",
- " | lift n (Closure (e, a)) = Closure (lift_env n e, lift (n+(length e)) a)",
- " | lift n c = c",
- "and lift_env n e = map (lift n) e",
- "",
- "fun strong stack (Closure (e, Abs m)) = ",
- " let",
- " val (stack', wnf) = weak SEmpty (Closure ((Var 0)::(lift_env 0 e), m))",
- " in",
- " case stack' of",
- " SEmpty => strong (SAbs stack) wnf",
- " | _ => raise ("^sname^".Run \"internal error in strong: weak failed\")",
- " end",
- " | strong stack (clos as (App (u, v))) = strong (SAppL (v, stack)) u",
- " | strong stack clos = strong_last stack clos",
- "and strong_last (SAbs stack) m = strong stack (Abs m)",
- " | strong_last (SAppL (b, stack)) a = strong (SAppR (a, stack)) b",
- " | strong_last (SAppR (a, stack)) b = strong_last stack (App (a, b))",
- " | strong_last stack clos = (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^".CConst "^(str c)
- val _ = writelist [
- "fun exportTerm (Var x) = "^sname^".CVar x",
- " | exportTerm (Const c) = "^sname^".CConst c",
- " | exportTerm (App (a,b)) = "^sname^".CApp (exportTerm a, exportTerm b)",
- " | exportTerm (Abs m) = "^sname^".CAbs (exportTerm m)",
- " | exportTerm (Closure (closlist, clos)) = "^sname^".Closure ("^sname^".list_map exportTerm closlist, exportTerm clos)"]
- val _ = writelist (map ec constants)
-
- val _ = writelist [
- "",
- "fun rewrite t = ",
- " let",
- " val (stack, wnf) = weak SEmpty (Closure ([], importTerm t))",
- " in",
- " case stack of ",
- " SEmpty => (case strong 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;"]
-
- val _ =
- let
- (*val fout = TextIO.openOut "gen_code.ML"
- val _ = TextIO.output (fout, !buffer)
- val _ = TextIO.closeOut fout*)
- in
- ()
- end
- in
- compiled_rewriter := NONE;
- use_text "" Output.ml_output false (!buffer);
- case !compiled_rewriter of
- NONE => raise (Compile "cannot communicate with compiled function")
- | SOME r => (compiled_rewriter := NONE; fn t => term_of_clos (r t))
- end
-
-fun compile eqs =
- let
- val _ = map (fn (p, r) =>
- (check_freevars (count_patternvars p) r;
- case p of PVar => raise (Compile "pattern reduces to a variable") | _ => ())) eqs
- in
- load_rules "AM_Compiler" "AM_compiled_code" eqs
- end
-
-fun run prog t = (prog t)
-
-end
-
-structure AbstractMachine = AM_Compiler
--- a/src/Pure/Tools/am_interpreter.ML Thu May 31 20:55:32 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,162 +0,0 @@
-(* Title: Pure/Tools/am_interpreter.ML
- ID: $Id$
- Author: Steven Obua
-*)
-
-signature ABSTRACT_MACHINE =
-sig
-
-datatype term = Var of int | Const of int | App of term * term | Abs of term
-
-datatype pattern = PVar | PConst of int * (pattern list)
-
-type program
-
-exception Compile of string;
-val compile : (pattern * term) list -> program
-
-exception Run of string;
-val run : program -> term -> term
-
-end
-
-structure AM_Interpreter : ABSTRACT_MACHINE = struct
-
-datatype term = Var of int | Const of int | App of term * term | Abs of term
-
-datatype pattern = PVar | PConst of int * (pattern list)
-
-datatype closure = CVar of int | CConst of int
- | CApp of closure * closure | CAbs of closure
- | Closure of (closure list) * closure
-
-structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
-
-datatype program = Program of ((pattern * closure) list) prog_struct.table
-
-datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
-
-exception Compile of string;
-exception Run of string;
-
-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)
-
-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")
-
-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
-
-(* Returns true iff at most 0 .. (free-1) occur unbound. therefore check_freevars 0 t iff t is closed *)
-fun check_freevars free (Var x) = x < free
- | check_freevars free (Const c) = true
- | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
- | check_freevars free (Abs m) = check_freevars (free+1) m
-
-fun count_patternvars PVar = 1
- | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
-
-fun pattern_key (PConst (c, ps)) = (c, length ps)
- | pattern_key _ = raise (Compile "pattern reduces to variable")
-
-fun compile eqs =
- let
- val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
- (pattern_key p, (p, clos_of_term r)))) eqs
- in
- Program (prog_struct.make (map (fn (k, a) => (k, [a])) eqs))
- end
-
-fun match_rules n [] clos = NONE
- | match_rules n ((p,eq)::rs) clos =
- case pattern_match [] p clos of
- NONE => match_rules (n+1) rs clos
- | SOME args => SOME (Closure (args, eq))
-
-fun match_closure (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 0 rules clos)
- | _ => NONE
-
-fun lift n (c as (CConst _)) = c
- | lift n (v as CVar m) = if m < n then v else CVar (m+1)
- | lift n (CAbs t) = CAbs (lift (n+1) t)
- | lift n (CApp (a,b)) = CApp (lift n a, lift n b)
- | lift n (Closure (e, a)) = Closure (lift_env n e, lift (n+(length e)) a)
-and lift_env n e = map (lift n) e
-
-fun weak prog stack (Closure (e, CApp (a, b))) = weak prog (SAppL (Closure (e, b), stack)) (Closure (e, a))
- | weak prog (SAppL (b, stack)) (Closure (e, CAbs m)) = weak prog stack (Closure (b::e, m))
- | weak prog stack (Closure (e, CVar n)) = weak prog stack (List.nth (e, n) handle Subscript => (CVar (n-(length e))))
- | weak prog stack (Closure (e, c as CConst _)) = weak prog stack c
- | weak prog stack clos =
- case match_closure prog clos of
- NONE => weak_last prog stack clos
- | SOME r => weak prog stack r
-and weak_last prog (SAppR (a, stack)) b = weak prog stack (CApp (a,b))
- | weak_last prog (s as (SAppL (b, stack))) a = weak prog (SAppR (a, stack)) b
- | weak_last prog stack c = (stack, c)
-
-fun strong prog stack (Closure (e, CAbs m)) =
- let
- val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
- in
- case stack' of
- SEmpty => strong prog (SAbs stack) wnf
- | _ => raise (Run "internal error in strong: weak failed")
- end
- | strong prog stack (clos as (CApp (u, v))) = strong prog (SAppL (v, stack)) u
- | strong prog stack clos = strong_last prog stack clos
-and strong_last prog (SAbs stack) m = strong prog stack (CAbs m)
- | strong_last prog (SAppL (b, stack)) a = strong prog (SAppR (a, stack)) b
- | strong_last prog (SAppR (a, stack)) b = strong_last prog stack (CApp (a, b))
- | strong_last prog stack clos = (stack, clos)
-
-fun run prog t =
- let
- val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
- in
- case stack of
- SEmpty => (case strong 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
-
-end
-
-structure AbstractMachine = AM_Interpreter
--- a/src/Pure/Tools/am_util.ML Thu May 31 20:55:32 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,172 +0,0 @@
-(* Title: Pure/Tools/am_util.ML
- ID: $Id$
- Author: Steven Obua
-*)
-
-signature AM_UTIL = sig
-
- type naming (* = string -> int *)
-
- exception Parse of string
- exception Tokenize
-
- (* takes a naming for the constants *)
- val read_rule : naming -> string -> AbstractMachine.pattern * AbstractMachine.term
-
- (* takes a naming for the constants and one for the free variables *)
- val read_term : naming -> naming -> string -> AbstractMachine.term
-
- val term_ord : AbstractMachine.term * AbstractMachine.term -> order
-
-end
-
-structure AM_Util : AM_UTIL =
-struct
-
-fun term_ord (AbstractMachine.Var x, AbstractMachine.Var y) = int_ord (x,y)
- | term_ord (AbstractMachine.Const c1, AbstractMachine.Const c2) = int_ord (c1, c2)
- | term_ord (AbstractMachine.App a1, AbstractMachine.App a2) =
- prod_ord term_ord term_ord (a1, a2)
- | term_ord (AbstractMachine.Abs m1, AbstractMachine.Abs m2) = term_ord (m1, m2)
- | term_ord (AbstractMachine.Const _, _) = LESS
- | term_ord (AbstractMachine.Var _, AbstractMachine.Const _ ) = GREATER
- | term_ord (AbstractMachine.Var _, _) = LESS
- | term_ord (AbstractMachine.App _, AbstractMachine.Abs _) = LESS
- | term_ord (AbstractMachine.App _, _) = GREATER
- | term_ord (AbstractMachine.Abs _, _) = LESS
-
-type naming = string -> int
-
-datatype token =
- TokenConst of string | TokenLeft | TokenRight | TokenVar of string |
- TokenLambda | TokenDot | TokenNone | TokenEq
-
-exception Tokenize;
-
-fun tokenize s =
- let
- fun is_lower c = "a" <= c andalso c <= "z";
- val is_alphanum = Symbol.is_ascii_letter orf Symbol.is_ascii_digit;
- fun tz TokenNone [] = []
- | tz x [] = [x]
- | tz TokenNone (c::cs) =
- if Symbol.is_ascii_blank c then tz TokenNone cs
- else if is_lower c then (tz (TokenVar c) cs)
- else if is_alphanum c then (tz (TokenConst c) cs)
- else if c = "%" then (TokenLambda :: (tz TokenNone cs))
- else if c = "." then (TokenDot :: (tz TokenNone cs))
- else if c = "(" then (TokenLeft :: (tz TokenNone cs))
- else if c = ")" then (TokenRight :: (tz TokenNone cs))
- else if c = "=" then (TokenEq :: (tz TokenNone cs))
- else raise Tokenize
- | tz (TokenConst s) (c::cs) =
- if is_alphanum c then (tz (TokenConst (s ^ c)) cs)
- else (TokenConst s)::(tz TokenNone (c::cs))
- | tz (TokenVar s) (c::cs) =
- if is_alphanum c then (tz (TokenVar (s ^ c)) cs)
- else (TokenVar s)::(tz TokenNone (c::cs))
- | tz _ _ = raise Tokenize
- in tz TokenNone (explode s) end
-
-exception Parse of string;
-
-fun cons x xs =
- if List.exists (fn y => x = y) xs then raise (Parse ("variable occurs twice: "^x))
- else (x::xs)
-
-fun parse_pattern f pvars ((TokenConst c)::ts) =
- let
- val (pvars, ts, plist) = parse_pattern_list f pvars ts
- in
- (pvars, ts, AbstractMachine.PConst (f c, plist))
- end
- | parse_pattern _ _ _ = raise (Parse "parse_pattern: constant expected")
-and parse_pattern_single f pvars ((TokenVar x)::ts) = (cons x pvars, ts, AbstractMachine.PVar)
- | parse_pattern_single f pvars ((TokenConst c)::ts) = (pvars, ts, AbstractMachine.PConst (f c, []))
- | parse_pattern_single f pvars (TokenLeft::ts) =
- let
- val (pvars, ts, p) = parse_pattern f pvars ts
- in
- case ts of
- TokenRight::ts => (pvars, ts, p)
- | _ => raise (Parse "parse_pattern_single: closing bracket expected")
- end
- | parse_pattern_single _ _ _ = raise (Parse "parse_pattern_single: got stuck")
-and parse_pattern_list f pvars (TokenEq::ts) = (pvars, TokenEq::ts, [])
- | parse_pattern_list f pvars (TokenRight::ts) = (pvars, TokenRight::ts, [])
- | parse_pattern_list f pvars ts =
- let
- val (pvars, ts, p) = parse_pattern_single f pvars ts
- val (pvars, ts, ps) = parse_pattern_list f pvars ts
- in
- (pvars, ts, p::ps)
- end
-
-fun app_terms x (t::ts) = app_terms (AbstractMachine.App (x, t)) ts
- | app_terms x [] = x
-
-fun parse_term_single f vars ((TokenConst c)::ts) = (ts, AbstractMachine.Const (f c))
- | parse_term_single f vars ((TokenVar v)::ts) = (ts, AbstractMachine.Var (vars v))
- | parse_term_single f vars (TokenLeft::ts) =
- let
- val (ts, term) = parse_term f vars ts
- in
- case ts of
- TokenRight::ts => (ts, term)
- | _ => raise Parse ("parse_term_single: closing bracket expected")
- end
- | parse_term_single f vars (TokenLambda::(TokenVar x)::TokenDot::ts) =
- let
- val (ts, term) = parse_term f (fn s => if s=x then 0 else (vars s)+1) ts
- in
- (ts, AbstractMachine.Abs term)
- end
- | parse_term_single _ _ _ = raise Parse ("parse_term_single: got stuck")
-and parse_term_list f vars [] = ([], [])
- | parse_term_list f vars (TokenRight::ts) = (TokenRight::ts, [])
- | parse_term_list f vars ts =
- let
- val (ts, term) = parse_term_single f vars ts
- val (ts, terms) = parse_term_list f vars ts
- in
- (ts, term::terms)
- end
-and parse_term f vars ts =
- let
- val (ts, terms) = parse_term_list f vars ts
- in
- case terms of
- [] => raise (Parse "parse_term: no term found")
- | (t::terms) => (ts, app_terms t terms)
- end
-
-fun read_rule f s =
- let
- val t = tokenize s
- val (v, ts, pattern) = parse_pattern f [] t
- fun vars [] (x:string) = raise (Parse "read_rule.vars: variable not found")
- | vars (v::vs) x = if v = x then 0 else (vars vs x)+1
- in
- case ts of
- TokenEq::ts =>
- let
- val (ts, term) = parse_term f (vars v) ts
- in
- case ts of
- [] => (pattern, term)
- | _ => raise (Parse "read_rule: still tokens left, end expected")
- end
- | _ => raise (Parse ("read_rule: = expected"))
- end
-
-fun read_term f g s =
- let
- val t = tokenize s
- val (ts, term) = parse_term f g t
- in
- case ts of
- [] => term
- | _ => raise (Parse ("read_term: still tokens left, end expected"))
- end
-
-end
--- a/src/Pure/Tools/compute.ML Thu May 31 20:55:32 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,292 +0,0 @@
-(* Title: Pure/Tools/compute.ML
- ID: $Id$
- Author: Steven Obua
-*)
-
-signature COMPUTE = sig
-
- type computer
-
- exception Make of string
-
- val basic_make : theory -> thm list -> computer
- val make : theory -> thm list -> computer
-
- val compute : computer -> (int -> string) -> cterm -> term
- val theory_of : computer -> theory
-
- val rewrite_param : computer -> (int -> string) -> cterm -> thm
- val rewrite : computer -> cterm -> thm
-
-end
-
-structure Compute : COMPUTE = struct
-
-exception Make of string;
-
-fun is_mono_typ (Type (_, list)) = forall is_mono_typ list
- | is_mono_typ _ = false
-
-fun is_mono_term (Const (_, t)) = is_mono_typ t
- | is_mono_term (Var (_, t)) = is_mono_typ t
- | is_mono_term (Free (_, t)) = is_mono_typ t
- | is_mono_term (Bound _) = true
- | is_mono_term (a $ b) = is_mono_term a andalso is_mono_term b
- | is_mono_term (Abs (_, ty, t)) = is_mono_typ ty andalso is_mono_term t
-
-structure AMTermTab = TableFun (type key = AbstractMachine.term val ord = AM_Util.term_ord)
-
-fun add x y = x + y : int;
-fun inc x = x + 1;
-
-exception Mono of term;
-
-val remove_types =
- let
- fun remove_types_var table invtable ccount vcount ldepth t =
- (case Termtab.lookup table t of
- NONE =>
- let
- val a = AbstractMachine.Var vcount
- in
- (Termtab.update (t, a) table,
- AMTermTab.update (a, t) invtable,
- ccount,
- inc vcount,
- AbstractMachine.Var (add vcount ldepth))
- end
- | SOME (AbstractMachine.Var v) =>
- (table, invtable, ccount, vcount, AbstractMachine.Var (add v ldepth))
- | SOME _ => sys_error "remove_types_var: lookup should be a var")
-
- fun remove_types_const table invtable ccount vcount ldepth t =
- (case Termtab.lookup table t of
- NONE =>
- let
- val a = AbstractMachine.Const ccount
- in
- (Termtab.update (t, a) table,
- AMTermTab.update (a, t) invtable,
- inc ccount,
- vcount,
- a)
- end
- | SOME (c as AbstractMachine.Const _) =>
- (table, invtable, ccount, vcount, c)
- | SOME _ => sys_error "remove_types_const: lookup should be a const")
-
- fun remove_types table invtable ccount vcount ldepth t =
- case t of
- Var (_, ty) =>
- if is_mono_typ ty then remove_types_var table invtable ccount vcount ldepth t
- else raise (Mono t)
- | Free (_, ty) =>
- if is_mono_typ ty then remove_types_var table invtable ccount vcount ldepth t
- else raise (Mono t)
- | Const (_, ty) =>
- if is_mono_typ ty then remove_types_const table invtable ccount vcount ldepth t
- else raise (Mono t)
- | Abs (_, ty, t') =>
- if is_mono_typ ty then
- let
- val (table, invtable, ccount, vcount, t') =
- remove_types table invtable ccount vcount (inc ldepth) t'
- in
- (table, invtable, ccount, vcount, AbstractMachine.Abs t')
- end
- else
- raise (Mono t)
- | a $ b =>
- let
- val (table, invtable, ccount, vcount, a) =
- remove_types table invtable ccount vcount ldepth a
- val (table, invtable, ccount, vcount, b) =
- remove_types table invtable ccount vcount ldepth b
- in
- (table, invtable, ccount, vcount, AbstractMachine.App (a,b))
- end
- | Bound b => (table, invtable, ccount, vcount, AbstractMachine.Var b)
- in
- fn (table, invtable, ccount, vcount) => remove_types table invtable ccount vcount 0
- end
-
-fun infer_types naming =
- let
- fun infer_types invtable ldepth bounds ty (AbstractMachine.Var v) =
- if v < ldepth then (Bound v, List.nth (bounds, v)) else
- (case AMTermTab.lookup invtable (AbstractMachine.Var (v-ldepth)) of
- SOME (t as Var (_, ty)) => (t, ty)
- | SOME (t as Free (_, ty)) => (t, ty)
- | _ => sys_error "infer_types: lookup should deliver Var or Free")
- | infer_types invtable ldepth _ ty (c as AbstractMachine.Const _) =
- (case AMTermTab.lookup invtable c of
- SOME (c as Const (_, ty)) => (c, ty)
- | _ => sys_error "infer_types: lookup should deliver Const")
- | infer_types invtable ldepth bounds (n,ty) (AbstractMachine.App (a, b)) =
- let
- val (a, aty) = infer_types invtable ldepth bounds (n+1, ty) 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 invtable ldepth bounds (0, adom) b
- in
- (a $ b, arange)
- end
- | infer_types invtable ldepth bounds (0, ty as Type ("fun", [dom, range]))
- (AbstractMachine.Abs m) =
- let
- val (m, _) = infer_types invtable (ldepth+1) (dom::bounds) (0, range) m
- in
- (Abs (naming ldepth, dom, m), ty)
- end
- | infer_types invtable ldepth bounds ty (AbstractMachine.Abs m) =
- sys_error "infer_types: cannot infer type of abstraction"
-
- fun infer invtable ty term =
- let
- val (term', _) = infer_types invtable 0 [] (0, ty) term
- in
- term'
- end
- in
- infer
- end
-
-datatype computer =
- Computer of theory_ref *
- (AbstractMachine.term Termtab.table * term AMTermTab.table * int * AbstractMachine.program)
-
-fun basic_make thy raw_ths =
- let
- val ths = map (Thm.transfer thy) raw_ths;
-
- fun thm2rule table invtable ccount th =
- let
- val prop = Thm.plain_prop_of th
- handle THM _ => raise (Make "theorems must be plain propositions")
- val (a, b) = Logic.dest_equals prop
- handle TERM _ => raise (Make "theorems must be meta-level equations")
-
- val (table, invtable, ccount, vcount, prop) =
- remove_types (table, invtable, ccount, 0) (a$b)
- handle Mono _ => raise (Make "no type variables allowed")
- val (left, right) =
- (case prop of AbstractMachine.App x => x | _ =>
- sys_error "make: remove_types should deliver application")
-
- fun make_pattern table invtable n vars (var as AbstractMachine.Var v) =
- let
- val var' = the (AMTermTab.lookup invtable var)
- val table = Termtab.delete var' table
- val invtable = AMTermTab.delete var invtable
- val vars = Inttab.update_new (v, n) vars handle Inttab.DUP _ =>
- raise (Make "no duplicate variable in pattern allowed")
- in
- (table, invtable, n+1, vars, AbstractMachine.PVar)
- end
- | make_pattern table invtable n vars (AbstractMachine.Abs _) =
- raise (Make "no lambda abstractions allowed in pattern")
- | make_pattern table invtable n vars (AbstractMachine.Const c) =
- (table, invtable, n, vars, AbstractMachine.PConst (c, []))
- | make_pattern table invtable n vars (AbstractMachine.App (a, b)) =
- let
- val (table, invtable, n, vars, pa) =
- make_pattern table invtable n vars a
- val (table, invtable, n, vars, pb) =
- make_pattern table invtable n vars b
- in
- case pa of
- AbstractMachine.PVar =>
- raise (Make "patterns may not start with a variable")
- | AbstractMachine.PConst (c, args) =>
- (table, invtable, n, vars, AbstractMachine.PConst (c, args@[pb]))
- end
-
- val (table, invtable, vcount, vars, pattern) =
- make_pattern table invtable 0 Inttab.empty left
- val _ = (case pattern of
- AbstractMachine.PVar =>
- raise (Make "patterns may not start with a variable")
- | _ => ())
-
- (* at this point, there shouldn't be any variables
- left in table or invtable, only constants *)
-
- (* finally, provide a function for renaming the
- pattern bound variables on the right hand side *)
-
- fun rename ldepth vars (var as AbstractMachine.Var v) =
- if v < ldepth then var
- else (case Inttab.lookup vars (v - ldepth) of
- NONE => raise (Make "new variable on right hand side")
- | SOME n => AbstractMachine.Var ((vcount-n-1)+ldepth))
- | rename ldepth vars (c as AbstractMachine.Const _) = c
- | rename ldepth vars (AbstractMachine.App (a, b)) =
- AbstractMachine.App (rename ldepth vars a, rename ldepth vars b)
- | rename ldepth vars (AbstractMachine.Abs m) =
- AbstractMachine.Abs (rename (ldepth+1) vars m)
-
- in
- (table, invtable, ccount, (pattern, rename 0 vars right))
- end
-
- val (table, invtable, ccount, rules) =
- fold_rev (fn th => fn (table, invtable, ccount, rules) =>
- let
- val (table, invtable, ccount, rule) =
- thm2rule table invtable ccount th
- in (table, invtable, ccount, rule::rules) end)
- ths (Termtab.empty, AMTermTab.empty, 0, [])
-
- val prog = AbstractMachine.compile rules
-
- in Computer (Theory.self_ref thy, (table, invtable, ccount, prog)) end
-
-fun make thy ths =
- let
- val (_, {mk_rews={mk=mk,mk_eq_True=emk, ...},...}) = rep_ss (simpset_of thy)
- fun mk_eq_True th = (case emk th of NONE => [th] | SOME th' => [th, th'])
- in
- basic_make thy (maps mk (maps mk_eq_True ths))
- end
-
-fun compute (Computer r) naming ct =
- let
- val {t=t, T=ty, thy=ctthy, ...} = rep_cterm ct
- val (rthy, (table, invtable, ccount, prog)) = r
- val thy = Theory.merge (Theory.deref rthy, ctthy)
- val (table, invtable, ccount, vcount, t) = remove_types (table, invtable, ccount, 0) t
- val t = AbstractMachine.run prog t
- val t = infer_types naming invtable ty t
- in
- t
- end
-
-fun theory_of (Computer (rthy, _)) = Theory.deref rthy
-
-fun default_naming i = "v_" ^ Int.toString i
-
-exception Param of computer * (int -> string) * cterm;
-
-fun rewrite_param r n ct =
- let val thy = theory_of_cterm ct in
- invoke_oracle_i thy "Pure.compute" (thy, Param (r, n, ct))
- end
-
-fun rewrite r ct = rewrite_param r default_naming ct
-
-
-(* theory setup *)
-
-fun compute_oracle (thy, Param (r, naming, ct)) =
- let
- val _ = Theory.assert_super (theory_of r) thy
- val t' = compute r naming ct
- in
- Logic.mk_equals (term_of ct, t')
- end
-
-val _ = Context.add_setup (Theory.add_oracle ("compute", compute_oracle))
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Compute_Oracle/am_compiler.ML Thu May 31 20:55:33 2007 +0200
@@ -0,0 +1,238 @@
+(* Title: Tools/Compute_Oracle/am_compiler.ML
+ ID: $Id$
+ Author: Steven Obua
+*)
+
+signature COMPILING_AM =
+sig
+ include ABSTRACT_MACHINE
+
+ datatype closure = CVar of int | CConst of int
+ | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
+
+ val set_compiled_rewriter : (term -> closure) -> 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;
+
+datatype term = Var of int | Const of int | App of term * term | Abs of term
+
+datatype pattern = PVar | PConst of int * (pattern list)
+
+datatype closure = CVar of int | CConst of int
+ | CApp of closure * closure | CAbs of closure
+ | Closure of (closure list) * closure
+
+val compiled_rewriter = ref (NONE:(term -> closure)Option.option)
+
+fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
+
+type program = (term -> term)
+
+datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
+
+exception Compile of string;
+exception Run of string;
+
+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)
+
+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")
+
+fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
+ | strip_closure args x = (x, args)
+
+(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
+ check_freevars 0 t iff t is closed*)
+fun check_freevars free (Var x) = x < free
+ | check_freevars free (Const c) = true
+ | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
+ | check_freevars free (Abs m) = check_freevars (free+1) m
+
+fun count_patternvars PVar = 1
+ | count_patternvars (PConst (_, ps)) =
+ List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
+
+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 ^ ")"
+
+ 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
+ "lookup stack "^pattern^" = weak 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]
+
+fun load_rules sname name prog =
+ let
+ (* FIXME consider using more readable/efficient Buffer.empty |> fold Buffer.add etc. *)
+ val buffer = 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 = 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",
+ ""]
+ val _ = (case prog of
+ r::rs => (writeln ("fun "^(print_rule r));
+ map (fn r => writeln(" | "^(print_rule r))) rs;
+ writeln (" | lookup stack clos = weak_last stack clos"); ())
+ | [] => (writeln "fun lookup stack clos = weak_last stack clos"))
+ val _ = writelist [
+ "and weak stack (Closure (e, App (a, b))) = weak (SAppL (Closure (e, b), stack)) (Closure (e, a))",
+ " | weak (SAppL (b, stack)) (Closure (e, Abs m)) = weak stack (Closure (b::e, m))",
+ " | weak stack (clos as Closure (_, Abs _)) = weak_last stack clos",
+ " | weak stack (Closure (e, Var n)) = weak stack ("^sname^".list_nth (e, n) handle _ => (Var (n-(length e))))",
+ " | weak stack (Closure (e, c)) = weak stack c",
+ " | weak stack clos = lookup stack clos",
+ "and weak_last (SAppR (a, stack)) b = weak stack (App(a, b))",
+ " | weak_last (SAppL (b, stack)) a = weak (SAppR (a, stack)) b",
+ " | weak_last stack c = (stack, c)",
+ "",
+ "fun lift n (v as Var m) = if m < n then v else Var (m+1)",
+ " | lift n (Abs t) = Abs (lift (n+1) t)",
+ " | lift n (App (a,b)) = App (lift n a, lift n b)",
+ " | lift n (Closure (e, a)) = Closure (lift_env n e, lift (n+(length e)) a)",
+ " | lift n c = c",
+ "and lift_env n e = map (lift n) e",
+ "",
+ "fun strong stack (Closure (e, Abs m)) = ",
+ " let",
+ " val (stack', wnf) = weak SEmpty (Closure ((Var 0)::(lift_env 0 e), m))",
+ " in",
+ " case stack' of",
+ " SEmpty => strong (SAbs stack) wnf",
+ " | _ => raise ("^sname^".Run \"internal error in strong: weak failed\")",
+ " end",
+ " | strong stack (clos as (App (u, v))) = strong (SAppL (v, stack)) u",
+ " | strong stack clos = strong_last stack clos",
+ "and strong_last (SAbs stack) m = strong stack (Abs m)",
+ " | strong_last (SAppL (b, stack)) a = strong (SAppR (a, stack)) b",
+ " | strong_last (SAppR (a, stack)) b = strong_last stack (App (a, b))",
+ " | strong_last stack clos = (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^".CConst "^(str c)
+ val _ = writelist [
+ "fun exportTerm (Var x) = "^sname^".CVar x",
+ " | exportTerm (Const c) = "^sname^".CConst c",
+ " | exportTerm (App (a,b)) = "^sname^".CApp (exportTerm a, exportTerm b)",
+ " | exportTerm (Abs m) = "^sname^".CAbs (exportTerm m)",
+ " | exportTerm (Closure (closlist, clos)) = "^sname^".Closure ("^sname^".list_map exportTerm closlist, exportTerm clos)"]
+ val _ = writelist (map ec constants)
+
+ val _ = writelist [
+ "",
+ "fun rewrite t = ",
+ " let",
+ " val (stack, wnf) = weak SEmpty (Closure ([], importTerm t))",
+ " in",
+ " case stack of ",
+ " SEmpty => (case strong 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;"]
+
+ val _ =
+ let
+ (*val fout = TextIO.openOut "gen_code.ML"
+ val _ = TextIO.output (fout, !buffer)
+ val _ = TextIO.closeOut fout*)
+ in
+ ()
+ end
+ in
+ compiled_rewriter := NONE;
+ use_text "" Output.ml_output false (!buffer);
+ case !compiled_rewriter of
+ NONE => raise (Compile "cannot communicate with compiled function")
+ | SOME r => (compiled_rewriter := NONE; fn t => term_of_clos (r t))
+ end
+
+fun compile eqs =
+ let
+ val _ = map (fn (p, r) =>
+ (check_freevars (count_patternvars p) r;
+ case p of PVar => raise (Compile "pattern reduces to a variable") | _ => ())) eqs
+ in
+ load_rules "AM_Compiler" "AM_compiled_code" eqs
+ end
+
+fun run prog t = (prog t)
+
+end
+
+structure AbstractMachine = AM_Compiler
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Compute_Oracle/am_interpreter.ML Thu May 31 20:55:33 2007 +0200
@@ -0,0 +1,162 @@
+(* Title: Tools/Compute_Oracle/am_interpreter.ML
+ ID: $Id$
+ Author: Steven Obua
+*)
+
+signature ABSTRACT_MACHINE =
+sig
+
+datatype term = Var of int | Const of int | App of term * term | Abs of term
+
+datatype pattern = PVar | PConst of int * (pattern list)
+
+type program
+
+exception Compile of string;
+val compile : (pattern * term) list -> program
+
+exception Run of string;
+val run : program -> term -> term
+
+end
+
+structure AM_Interpreter : ABSTRACT_MACHINE = struct
+
+datatype term = Var of int | Const of int | App of term * term | Abs of term
+
+datatype pattern = PVar | PConst of int * (pattern list)
+
+datatype closure = CVar of int | CConst of int
+ | CApp of closure * closure | CAbs of closure
+ | Closure of (closure list) * closure
+
+structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
+
+datatype program = Program of ((pattern * closure) list) prog_struct.table
+
+datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
+
+exception Compile of string;
+exception Run of string;
+
+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)
+
+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")
+
+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
+
+(* Returns true iff at most 0 .. (free-1) occur unbound. therefore check_freevars 0 t iff t is closed *)
+fun check_freevars free (Var x) = x < free
+ | check_freevars free (Const c) = true
+ | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
+ | check_freevars free (Abs m) = check_freevars (free+1) m
+
+fun count_patternvars PVar = 1
+ | count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
+
+fun pattern_key (PConst (c, ps)) = (c, length ps)
+ | pattern_key _ = raise (Compile "pattern reduces to variable")
+
+fun compile eqs =
+ let
+ val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
+ (pattern_key p, (p, clos_of_term r)))) eqs
+ in
+ Program (prog_struct.make (map (fn (k, a) => (k, [a])) eqs))
+ end
+
+fun match_rules n [] clos = NONE
+ | match_rules n ((p,eq)::rs) clos =
+ case pattern_match [] p clos of
+ NONE => match_rules (n+1) rs clos
+ | SOME args => SOME (Closure (args, eq))
+
+fun match_closure (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 0 rules clos)
+ | _ => NONE
+
+fun lift n (c as (CConst _)) = c
+ | lift n (v as CVar m) = if m < n then v else CVar (m+1)
+ | lift n (CAbs t) = CAbs (lift (n+1) t)
+ | lift n (CApp (a,b)) = CApp (lift n a, lift n b)
+ | lift n (Closure (e, a)) = Closure (lift_env n e, lift (n+(length e)) a)
+and lift_env n e = map (lift n) e
+
+fun weak prog stack (Closure (e, CApp (a, b))) = weak prog (SAppL (Closure (e, b), stack)) (Closure (e, a))
+ | weak prog (SAppL (b, stack)) (Closure (e, CAbs m)) = weak prog stack (Closure (b::e, m))
+ | weak prog stack (Closure (e, CVar n)) = weak prog stack (List.nth (e, n) handle Subscript => (CVar (n-(length e))))
+ | weak prog stack (Closure (e, c as CConst _)) = weak prog stack c
+ | weak prog stack clos =
+ case match_closure prog clos of
+ NONE => weak_last prog stack clos
+ | SOME r => weak prog stack r
+and weak_last prog (SAppR (a, stack)) b = weak prog stack (CApp (a,b))
+ | weak_last prog (s as (SAppL (b, stack))) a = weak prog (SAppR (a, stack)) b
+ | weak_last prog stack c = (stack, c)
+
+fun strong prog stack (Closure (e, CAbs m)) =
+ let
+ val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
+ in
+ case stack' of
+ SEmpty => strong prog (SAbs stack) wnf
+ | _ => raise (Run "internal error in strong: weak failed")
+ end
+ | strong prog stack (clos as (CApp (u, v))) = strong prog (SAppL (v, stack)) u
+ | strong prog stack clos = strong_last prog stack clos
+and strong_last prog (SAbs stack) m = strong prog stack (CAbs m)
+ | strong_last prog (SAppL (b, stack)) a = strong prog (SAppR (a, stack)) b
+ | strong_last prog (SAppR (a, stack)) b = strong_last prog stack (CApp (a, b))
+ | strong_last prog stack clos = (stack, clos)
+
+fun run prog t =
+ let
+ val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
+ in
+ case stack of
+ SEmpty => (case strong 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
+
+end
+
+structure AbstractMachine = AM_Interpreter
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Compute_Oracle/am_util.ML Thu May 31 20:55:33 2007 +0200
@@ -0,0 +1,172 @@
+(* Title: Tools/Compute_Oracle/am_util.ML
+ ID: $Id$
+ Author: Steven Obua
+*)
+
+signature AM_UTIL = sig
+
+ type naming (* = string -> int *)
+
+ exception Parse of string
+ exception Tokenize
+
+ (* takes a naming for the constants *)
+ val read_rule : naming -> string -> AbstractMachine.pattern * AbstractMachine.term
+
+ (* takes a naming for the constants and one for the free variables *)
+ val read_term : naming -> naming -> string -> AbstractMachine.term
+
+ val term_ord : AbstractMachine.term * AbstractMachine.term -> order
+
+end
+
+structure AM_Util : AM_UTIL =
+struct
+
+fun term_ord (AbstractMachine.Var x, AbstractMachine.Var y) = int_ord (x,y)
+ | term_ord (AbstractMachine.Const c1, AbstractMachine.Const c2) = int_ord (c1, c2)
+ | term_ord (AbstractMachine.App a1, AbstractMachine.App a2) =
+ prod_ord term_ord term_ord (a1, a2)
+ | term_ord (AbstractMachine.Abs m1, AbstractMachine.Abs m2) = term_ord (m1, m2)
+ | term_ord (AbstractMachine.Const _, _) = LESS
+ | term_ord (AbstractMachine.Var _, AbstractMachine.Const _ ) = GREATER
+ | term_ord (AbstractMachine.Var _, _) = LESS
+ | term_ord (AbstractMachine.App _, AbstractMachine.Abs _) = LESS
+ | term_ord (AbstractMachine.App _, _) = GREATER
+ | term_ord (AbstractMachine.Abs _, _) = LESS
+
+type naming = string -> int
+
+datatype token =
+ TokenConst of string | TokenLeft | TokenRight | TokenVar of string |
+ TokenLambda | TokenDot | TokenNone | TokenEq
+
+exception Tokenize;
+
+fun tokenize s =
+ let
+ fun is_lower c = "a" <= c andalso c <= "z";
+ val is_alphanum = Symbol.is_ascii_letter orf Symbol.is_ascii_digit;
+ fun tz TokenNone [] = []
+ | tz x [] = [x]
+ | tz TokenNone (c::cs) =
+ if Symbol.is_ascii_blank c then tz TokenNone cs
+ else if is_lower c then (tz (TokenVar c) cs)
+ else if is_alphanum c then (tz (TokenConst c) cs)
+ else if c = "%" then (TokenLambda :: (tz TokenNone cs))
+ else if c = "." then (TokenDot :: (tz TokenNone cs))
+ else if c = "(" then (TokenLeft :: (tz TokenNone cs))
+ else if c = ")" then (TokenRight :: (tz TokenNone cs))
+ else if c = "=" then (TokenEq :: (tz TokenNone cs))
+ else raise Tokenize
+ | tz (TokenConst s) (c::cs) =
+ if is_alphanum c then (tz (TokenConst (s ^ c)) cs)
+ else (TokenConst s)::(tz TokenNone (c::cs))
+ | tz (TokenVar s) (c::cs) =
+ if is_alphanum c then (tz (TokenVar (s ^ c)) cs)
+ else (TokenVar s)::(tz TokenNone (c::cs))
+ | tz _ _ = raise Tokenize
+ in tz TokenNone (explode s) end
+
+exception Parse of string;
+
+fun cons x xs =
+ if List.exists (fn y => x = y) xs then raise (Parse ("variable occurs twice: "^x))
+ else (x::xs)
+
+fun parse_pattern f pvars ((TokenConst c)::ts) =
+ let
+ val (pvars, ts, plist) = parse_pattern_list f pvars ts
+ in
+ (pvars, ts, AbstractMachine.PConst (f c, plist))
+ end
+ | parse_pattern _ _ _ = raise (Parse "parse_pattern: constant expected")
+and parse_pattern_single f pvars ((TokenVar x)::ts) = (cons x pvars, ts, AbstractMachine.PVar)
+ | parse_pattern_single f pvars ((TokenConst c)::ts) = (pvars, ts, AbstractMachine.PConst (f c, []))
+ | parse_pattern_single f pvars (TokenLeft::ts) =
+ let
+ val (pvars, ts, p) = parse_pattern f pvars ts
+ in
+ case ts of
+ TokenRight::ts => (pvars, ts, p)
+ | _ => raise (Parse "parse_pattern_single: closing bracket expected")
+ end
+ | parse_pattern_single _ _ _ = raise (Parse "parse_pattern_single: got stuck")
+and parse_pattern_list f pvars (TokenEq::ts) = (pvars, TokenEq::ts, [])
+ | parse_pattern_list f pvars (TokenRight::ts) = (pvars, TokenRight::ts, [])
+ | parse_pattern_list f pvars ts =
+ let
+ val (pvars, ts, p) = parse_pattern_single f pvars ts
+ val (pvars, ts, ps) = parse_pattern_list f pvars ts
+ in
+ (pvars, ts, p::ps)
+ end
+
+fun app_terms x (t::ts) = app_terms (AbstractMachine.App (x, t)) ts
+ | app_terms x [] = x
+
+fun parse_term_single f vars ((TokenConst c)::ts) = (ts, AbstractMachine.Const (f c))
+ | parse_term_single f vars ((TokenVar v)::ts) = (ts, AbstractMachine.Var (vars v))
+ | parse_term_single f vars (TokenLeft::ts) =
+ let
+ val (ts, term) = parse_term f vars ts
+ in
+ case ts of
+ TokenRight::ts => (ts, term)
+ | _ => raise Parse ("parse_term_single: closing bracket expected")
+ end
+ | parse_term_single f vars (TokenLambda::(TokenVar x)::TokenDot::ts) =
+ let
+ val (ts, term) = parse_term f (fn s => if s=x then 0 else (vars s)+1) ts
+ in
+ (ts, AbstractMachine.Abs term)
+ end
+ | parse_term_single _ _ _ = raise Parse ("parse_term_single: got stuck")
+and parse_term_list f vars [] = ([], [])
+ | parse_term_list f vars (TokenRight::ts) = (TokenRight::ts, [])
+ | parse_term_list f vars ts =
+ let
+ val (ts, term) = parse_term_single f vars ts
+ val (ts, terms) = parse_term_list f vars ts
+ in
+ (ts, term::terms)
+ end
+and parse_term f vars ts =
+ let
+ val (ts, terms) = parse_term_list f vars ts
+ in
+ case terms of
+ [] => raise (Parse "parse_term: no term found")
+ | (t::terms) => (ts, app_terms t terms)
+ end
+
+fun read_rule f s =
+ let
+ val t = tokenize s
+ val (v, ts, pattern) = parse_pattern f [] t
+ fun vars [] (x:string) = raise (Parse "read_rule.vars: variable not found")
+ | vars (v::vs) x = if v = x then 0 else (vars vs x)+1
+ in
+ case ts of
+ TokenEq::ts =>
+ let
+ val (ts, term) = parse_term f (vars v) ts
+ in
+ case ts of
+ [] => (pattern, term)
+ | _ => raise (Parse "read_rule: still tokens left, end expected")
+ end
+ | _ => raise (Parse ("read_rule: = expected"))
+ end
+
+fun read_term f g s =
+ let
+ val t = tokenize s
+ val (ts, term) = parse_term f g t
+ in
+ case ts of
+ [] => term
+ | _ => raise (Parse ("read_term: still tokens left, end expected"))
+ end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Compute_Oracle/compute.ML Thu May 31 20:55:33 2007 +0200
@@ -0,0 +1,278 @@
+(* Title: Tools/Compute_Oracle/compute.ML
+ ID: $Id$
+ Author: Steven Obua
+*)
+
+signature COMPUTE = sig
+
+ type computer
+
+ exception Make of string
+
+ val basic_make : theory -> thm list -> computer
+ val make : theory -> thm list -> computer
+
+ val compute : computer -> (int -> string) -> cterm -> term
+ val theory_of : computer -> theory
+
+ val default_naming: int -> string
+ val oracle_fn: theory -> computer * (int -> string) * cterm -> term
+end
+
+structure Compute: COMPUTE = struct
+
+exception Make of string;
+
+fun is_mono_typ (Type (_, list)) = forall is_mono_typ list
+ | is_mono_typ _ = false
+
+fun is_mono_term (Const (_, t)) = is_mono_typ t
+ | is_mono_term (Var (_, t)) = is_mono_typ t
+ | is_mono_term (Free (_, t)) = is_mono_typ t
+ | is_mono_term (Bound _) = true
+ | is_mono_term (a $ b) = is_mono_term a andalso is_mono_term b
+ | is_mono_term (Abs (_, ty, t)) = is_mono_typ ty andalso is_mono_term t
+
+structure AMTermTab = TableFun (type key = AbstractMachine.term val ord = AM_Util.term_ord)
+
+fun add x y = x + y : int;
+fun inc x = x + 1;
+
+exception Mono of term;
+
+val remove_types =
+ let
+ fun remove_types_var table invtable ccount vcount ldepth t =
+ (case Termtab.lookup table t of
+ NONE =>
+ let
+ val a = AbstractMachine.Var vcount
+ in
+ (Termtab.update (t, a) table,
+ AMTermTab.update (a, t) invtable,
+ ccount,
+ inc vcount,
+ AbstractMachine.Var (add vcount ldepth))
+ end
+ | SOME (AbstractMachine.Var v) =>
+ (table, invtable, ccount, vcount, AbstractMachine.Var (add v ldepth))
+ | SOME _ => sys_error "remove_types_var: lookup should be a var")
+
+ fun remove_types_const table invtable ccount vcount ldepth t =
+ (case Termtab.lookup table t of
+ NONE =>
+ let
+ val a = AbstractMachine.Const ccount
+ in
+ (Termtab.update (t, a) table,
+ AMTermTab.update (a, t) invtable,
+ inc ccount,
+ vcount,
+ a)
+ end
+ | SOME (c as AbstractMachine.Const _) =>
+ (table, invtable, ccount, vcount, c)
+ | SOME _ => sys_error "remove_types_const: lookup should be a const")
+
+ fun remove_types table invtable ccount vcount ldepth t =
+ case t of
+ Var (_, ty) =>
+ if is_mono_typ ty then remove_types_var table invtable ccount vcount ldepth t
+ else raise (Mono t)
+ | Free (_, ty) =>
+ if is_mono_typ ty then remove_types_var table invtable ccount vcount ldepth t
+ else raise (Mono t)
+ | Const (_, ty) =>
+ if is_mono_typ ty then remove_types_const table invtable ccount vcount ldepth t
+ else raise (Mono t)
+ | Abs (_, ty, t') =>
+ if is_mono_typ ty then
+ let
+ val (table, invtable, ccount, vcount, t') =
+ remove_types table invtable ccount vcount (inc ldepth) t'
+ in
+ (table, invtable, ccount, vcount, AbstractMachine.Abs t')
+ end
+ else
+ raise (Mono t)
+ | a $ b =>
+ let
+ val (table, invtable, ccount, vcount, a) =
+ remove_types table invtable ccount vcount ldepth a
+ val (table, invtable, ccount, vcount, b) =
+ remove_types table invtable ccount vcount ldepth b
+ in
+ (table, invtable, ccount, vcount, AbstractMachine.App (a,b))
+ end
+ | Bound b => (table, invtable, ccount, vcount, AbstractMachine.Var b)
+ in
+ fn (table, invtable, ccount, vcount) => remove_types table invtable ccount vcount 0
+ end
+
+fun infer_types naming =
+ let
+ fun infer_types invtable ldepth bounds ty (AbstractMachine.Var v) =
+ if v < ldepth then (Bound v, List.nth (bounds, v)) else
+ (case AMTermTab.lookup invtable (AbstractMachine.Var (v-ldepth)) of
+ SOME (t as Var (_, ty)) => (t, ty)
+ | SOME (t as Free (_, ty)) => (t, ty)
+ | _ => sys_error "infer_types: lookup should deliver Var or Free")
+ | infer_types invtable ldepth _ ty (c as AbstractMachine.Const _) =
+ (case AMTermTab.lookup invtable c of
+ SOME (c as Const (_, ty)) => (c, ty)
+ | _ => sys_error "infer_types: lookup should deliver Const")
+ | infer_types invtable ldepth bounds (n,ty) (AbstractMachine.App (a, b)) =
+ let
+ val (a, aty) = infer_types invtable ldepth bounds (n+1, ty) 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 invtable ldepth bounds (0, adom) b
+ in
+ (a $ b, arange)
+ end
+ | infer_types invtable ldepth bounds (0, ty as Type ("fun", [dom, range]))
+ (AbstractMachine.Abs m) =
+ let
+ val (m, _) = infer_types invtable (ldepth+1) (dom::bounds) (0, range) m
+ in
+ (Abs (naming ldepth, dom, m), ty)
+ end
+ | infer_types invtable ldepth bounds ty (AbstractMachine.Abs m) =
+ sys_error "infer_types: cannot infer type of abstraction"
+
+ fun infer invtable ty term =
+ let
+ val (term', _) = infer_types invtable 0 [] (0, ty) term
+ in
+ term'
+ end
+ in
+ infer
+ end
+
+datatype computer =
+ Computer of theory_ref *
+ (AbstractMachine.term Termtab.table * term AMTermTab.table * int * AbstractMachine.program)
+
+fun basic_make thy raw_ths =
+ let
+ val ths = map (Thm.transfer thy) raw_ths;
+
+ fun thm2rule table invtable ccount th =
+ let
+ val prop = Thm.plain_prop_of th
+ handle THM _ => raise (Make "theorems must be plain propositions")
+ val (a, b) = Logic.dest_equals prop
+ handle TERM _ => raise (Make "theorems must be meta-level equations")
+
+ val (table, invtable, ccount, vcount, prop) =
+ remove_types (table, invtable, ccount, 0) (a$b)
+ handle Mono _ => raise (Make "no type variables allowed")
+ val (left, right) =
+ (case prop of AbstractMachine.App x => x | _ =>
+ sys_error "make: remove_types should deliver application")
+
+ fun make_pattern table invtable n vars (var as AbstractMachine.Var v) =
+ let
+ val var' = the (AMTermTab.lookup invtable var)
+ val table = Termtab.delete var' table
+ val invtable = AMTermTab.delete var invtable
+ val vars = Inttab.update_new (v, n) vars handle Inttab.DUP _ =>
+ raise (Make "no duplicate variable in pattern allowed")
+ in
+ (table, invtable, n+1, vars, AbstractMachine.PVar)
+ end
+ | make_pattern table invtable n vars (AbstractMachine.Abs _) =
+ raise (Make "no lambda abstractions allowed in pattern")
+ | make_pattern table invtable n vars (AbstractMachine.Const c) =
+ (table, invtable, n, vars, AbstractMachine.PConst (c, []))
+ | make_pattern table invtable n vars (AbstractMachine.App (a, b)) =
+ let
+ val (table, invtable, n, vars, pa) =
+ make_pattern table invtable n vars a
+ val (table, invtable, n, vars, pb) =
+ make_pattern table invtable n vars b
+ in
+ case pa of
+ AbstractMachine.PVar =>
+ raise (Make "patterns may not start with a variable")
+ | AbstractMachine.PConst (c, args) =>
+ (table, invtable, n, vars, AbstractMachine.PConst (c, args@[pb]))
+ end
+
+ val (table, invtable, vcount, vars, pattern) =
+ make_pattern table invtable 0 Inttab.empty left
+ val _ = (case pattern of
+ AbstractMachine.PVar =>
+ raise (Make "patterns may not start with a variable")
+ | _ => ())
+
+ (* at this point, there shouldn't be any variables
+ left in table or invtable, only constants *)
+
+ (* finally, provide a function for renaming the
+ pattern bound variables on the right hand side *)
+
+ fun rename ldepth vars (var as AbstractMachine.Var v) =
+ if v < ldepth then var
+ else (case Inttab.lookup vars (v - ldepth) of
+ NONE => raise (Make "new variable on right hand side")
+ | SOME n => AbstractMachine.Var ((vcount-n-1)+ldepth))
+ | rename ldepth vars (c as AbstractMachine.Const _) = c
+ | rename ldepth vars (AbstractMachine.App (a, b)) =
+ AbstractMachine.App (rename ldepth vars a, rename ldepth vars b)
+ | rename ldepth vars (AbstractMachine.Abs m) =
+ AbstractMachine.Abs (rename (ldepth+1) vars m)
+
+ in
+ (table, invtable, ccount, (pattern, rename 0 vars right))
+ end
+
+ val (table, invtable, ccount, rules) =
+ fold_rev (fn th => fn (table, invtable, ccount, rules) =>
+ let
+ val (table, invtable, ccount, rule) =
+ thm2rule table invtable ccount th
+ in (table, invtable, ccount, rule::rules) end)
+ ths (Termtab.empty, AMTermTab.empty, 0, [])
+
+ val prog = AbstractMachine.compile rules
+
+ in Computer (Theory.self_ref thy, (table, invtable, ccount, prog)) end
+
+fun make thy ths =
+ let
+ val (_, {mk_rews={mk=mk,mk_eq_True=emk, ...},...}) = rep_ss (simpset_of thy)
+ fun mk_eq_True th = (case emk th of NONE => [th] | SOME th' => [th, th'])
+ in
+ basic_make thy (maps mk (maps mk_eq_True ths))
+ end
+
+fun compute (Computer r) naming ct =
+ let
+ val {t=t, T=ty, thy=ctthy, ...} = rep_cterm ct
+ val (rthy, (table, invtable, ccount, prog)) = r
+ val thy = Theory.merge (Theory.deref rthy, ctthy)
+ val (table, invtable, ccount, vcount, t) = remove_types (table, invtable, ccount, 0) t
+ val t = AbstractMachine.run prog t
+ val t = infer_types naming invtable ty t
+ in
+ t
+ end
+
+fun theory_of (Computer (rthy, _)) = Theory.deref rthy
+
+fun default_naming i = "v_" ^ Int.toString i
+
+
+fun oracle_fn thy (r, naming, ct) =
+ let
+ val _ = Theory.assert_super (theory_of r) thy
+ val t' = compute r naming ct
+ in
+ Logic.mk_equals (term_of ct, t')
+ end
+
+end