# HG changeset patch
# User obua
# Date 1121189392 -7200
# Node ID 6632354665629603da96e6b82c117cf6dc730bb0
# Parent  aa284c1b72ad13ae4d55b23ff7ac5d0069676465
- introduce Pure/Tools directory
- add compute oracle to Pure/Tools

diff -r aa284c1b72ad -r 663235466562 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Jul 12 19:18:55 2005 +0200
+++ b/src/Pure/IsaMakefile	Tue Jul 12 19:29:52 2005 +0200
@@ -55,6 +55,8 @@
   Syntax/type_ext.ML Thy/html.ML Thy/latex.ML Thy/present.ML		\
   Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_info.ML Thy/thy_load.ML	\
   Thy/thy_parse.ML Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML		\
+  Tools/am_compiler.ML Tools/am_interpreter.ML Tools/am_util.ML         \
+  Tools/compute.ML Tools/ROOT.ML                                        \
   codegen.ML context.ML display.ML drule.ML envir.ML fact_index.ML	\
   goals.ML install_pp.ML library.ML logic.ML meta_simplifier.ML net.ML	\
   pattern.ML proof_general.ML proofterm.ML pure_thy.ML search.ML	\
diff -r aa284c1b72ad -r 663235466562 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Jul 12 19:18:55 2005 +0200
+++ b/src/Pure/ROOT.ML	Tue Jul 12 19:29:52 2005 +0200
@@ -93,6 +93,9 @@
 (*configuration for Proof General*)
 use "proof_general.ML";
 
+(* loading the Tools directory *)
+cd "Tools"; use "ROOT.ML"; cd "..";
+
 (*the Pure theories*)
 use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end;
 use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end;
diff -r aa284c1b72ad -r 663235466562 src/Pure/Tools/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/ROOT.ML	Tue Jul 12 19:29:52 2005 +0200
@@ -0,0 +1,8 @@
+(*  Title:      Pure/Tools/ROOT.ML
+    ID:         $Id$
+*)
+
+use "am_interpreter.ML";
+use "am_compiler.ML"; 
+use "am_util.ML";
+use "compute.ML";
diff -r aa284c1b72ad -r 663235466562 src/Pure/Tools/am_compiler.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/am_compiler.ML	Tue Jul 12 19:29:52 2005 +0200
@@ -0,0 +1,231 @@
+(*  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
+end
+
+structure AM_Compiler :> COMPILING_AM = 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
+
+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 List.exists Char.isSpace (String.explode 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 remove_dups (c::cs) = 
+    let val cs = remove_dups cs in
+	if (List.exists (fn x => x=c) cs) then cs else c::cs
+    end
+  | remove_dups [] = []
+
+fun constants_of PVar = []
+  | constants_of (PConst (c, ps)) = c::(List.concat (map 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
+	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 = remove_dups (List.concat (map (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 (List.nth (e, n) handle Subscript => (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 "^(String.concat (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 (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
+	    
+	val dummy = (fn s => ())		    
+    in
+	compiled_rewriter := NONE;	
+	use_text (dummy, dummy) 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
diff -r aa284c1b72ad -r 663235466562 src/Pure/Tools/am_interpreter.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/am_interpreter.ML	Tue Jul 12 19:29:52 2005 +0200
@@ -0,0 +1,227 @@
+(*  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
+
+signature BIN_TREE_KEY =
+sig
+  type key
+  val less : key * key -> bool
+  val eq : key * key -> bool
+end
+
+signature BIN_TREE = 
+sig
+    type key    
+    type 'a t
+    val tree_of_list : (key * 'a list -> 'b) -> (key * 'a) list -> 'b t
+    val lookup : 'a t -> key -> 'a Option.option
+    val empty : 'a t
+end
+
+functor BinTreeFun(Key: BIN_TREE_KEY) : BIN_TREE  =
+struct
+
+type key = Key.key
+
+datatype 'a t = Empty | Node of key * 'a * 'a t * 'a t 
+
+val empty = Empty
+
+fun insert (k, a) [] = [(k, a)]
+  | insert (k, a) ((l,b)::x') = 
+    if Key.less (k, l) then (k, a)::(l,b)::x'
+    else if Key.eq (k, l) then (k, a@b)::x'
+    else (l,b)::(insert (k, a) x')
+
+fun sort ((k, a)::x) = insert (k, a) (sort x)
+  | sort [] = []
+
+fun tree_of_sorted_list [] = Empty
+  | tree_of_sorted_list l = 
+    let
+	val len = length l
+	val leftlen = (len - 1) div 2
+	val left = tree_of_sorted_list (List.take (l, leftlen))
+	val rightl = List.drop (l, leftlen)
+	val (k, x) = hd rightl
+    in
+	Node (k, x, left, tree_of_sorted_list (tl rightl))
+    end
+	
+fun tree_of_list f l = tree_of_sorted_list (map (fn (k, a) => (k, f (k,a))) (sort (map (fn (k, a) => (k, [a])) l)))
+		 
+fun lookup Empty key = NONE
+  | lookup (Node (k, x, left, right)) key =
+    if Key.less (key, k) then
+	lookup left key
+    else if Key.less (k, key) then
+	lookup right key
+    else
+	SOME x
+end;
+
+structure IntBinTree = BinTreeFun (type key = int val less = (op <) val eq = (op = : int * int -> bool));
+
+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 IntPairKey = 
+struct
+type key = int * int
+fun less ((x1, y1), (x2, y2)) = x1 < x2 orelse (x1 = x2 andalso y1 < y2)
+fun eq (k1, k2) = (k1 = k2)
+end
+
+structure prog_struct = BinTreeFun (IntPairKey)
+
+type program = ((pattern * closure) list) prog_struct.t
+
+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
+	prog_struct.tree_of_list (fn (key, rules) => rules) 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 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
diff -r aa284c1b72ad -r 663235466562 src/Pure/Tools/am_util.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/am_util.ML	Tue Jul 12 19:29:52 2005 +0200
@@ -0,0 +1,170 @@
+(*  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
+	val s = String.explode s
+	fun str c = Char.toString c
+	fun app s c = s^(str c)
+	fun tz TokenNone [] = []
+	  | tz x [] = [x]
+	  | tz TokenNone (c::cs) = 
+	    if Char.isSpace c then tz TokenNone cs
+	    else if Char.isLower c then (tz (TokenVar (str c)) cs)
+	    else if Char.isAlphaNum c then (tz (TokenConst (str 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 Char.isAlphaNum c then (tz (TokenConst (app s c)) cs)
+	    else (TokenConst s)::(tz TokenNone (c::cs))
+	  | tz (TokenVar s) (c::cs) = 
+	    if Char.isAlphaNum c then (tz (TokenVar (app s c)) cs)
+	    else (TokenVar s)::(tz TokenNone (c::cs))
+	  | tz _ _ = raise Tokenize
+    in
+	tz TokenNone 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
diff -r aa284c1b72ad -r 663235466562 src/Pure/Tools/compute.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/compute.ML	Tue Jul 12 19:29:52 2005 +0200
@@ -0,0 +1,289 @@
+(*  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 Internal of string; (* this exception is only thrown if there is a bug *)
+
+exception Make of string;
+
+fun is_mono_typ (Type (_, list)) = List.all 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 TermTab = Termtab
+structure AMTermTab = TableFun (type key = AbstractMachine.term val ord = AM_Util.term_ord)
+
+fun add x y = Int.+ (x, y)
+fun inc x = Int.+ (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 _ => raise (Internal "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 _ => raise (Internal "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)
+	       | _ => raise (Internal "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)
+	       | _ => raise (Internal "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)
+		      | _ => raise (Internal "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) =
+	    raise (Internal "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
+
+structure Inttab = TableFun (type key = int val ord=int_ord);
+
+type computer = theory_ref * (AbstractMachine.term TermTab.table * term AMTermTab.table * int * 
+                              AbstractMachine.program)
+
+fun rthy_of_thm th = Theory.self_ref (theory_of_thm th)
+
+fun basic_make thy ths = 
+    let
+        val _ = List.foldl (fn (th, _) => Theory.assert_super (theory_of_thm th) thy) thy ths
+        val rthy = Theory.self_ref thy
+	 
+	fun thm2rule table invtable ccount th = 
+	    let
+		val prop = Drule.plain_prop_of (transfer thy th)
+		val _ = if Logic.is_equals prop then () else raise (Make "theorems must be equations")
+		val (a, b) = Logic.dest_equals prop
+			    
+		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 | _ => raise (Internal "make: remove_types should deliver application"))
+							       
+		fun make_pattern table invtable n vars (var as AbstractMachine.Var v) =
+		    let
+			val var' = valOf (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) = 
+	    List.foldl (fn (th, (table, invtable, ccount, rules)) => 
+			   let 
+			       val (table, invtable, ccount, rule) = thm2rule table invtable ccount th
+			   in
+			       (table, invtable, ccount, rule::rules)
+			   end)
+		       (TermTab.empty, AMTermTab.empty, 0, []) (List.rev ths)
+
+	val prog = AbstractMachine.compile rules
+
+    in
+	(rthy, (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'])
+      fun app f l = List.concat (map f l)
+    in
+      basic_make thy (app mk (app mk_eq_True ths))
+    end
+
+fun compute 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 handle Internal s => (writeln ("Internal error: "^s); raise (Internal s))
+
+fun theory_of (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
+
+(* setup of the Pure.compute oracle *)
+fun compute_oracle (sg, Param (r, naming, ct)) =
+    let 
+	val _ = Theory.assert_super (theory_of r) sg
+	val t' = compute r naming ct
+    in
+	Logic.mk_equals (term_of ct, t')
+    end
+
+fun setup_oracle thy = Theory.add_oracle ("compute", compute_oracle) thy
+
+val _ = Context.add_setup [setup_oracle]
+
+end
+