--- 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 \
--- 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;
--- /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";
--- /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
--- /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
--- /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
--- /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
+