# HG changeset patch # User wenzelm # Date 1180637733 -7200 # Node ID 3913451b04181b56c97afb5abecdeafdcd38103e # Parent 51179ca0c4295b40aaff1b377089154313ba1ca8 moved Compute_Oracle from Pure/Tools to Tools; diff -r 51179ca0c429 -r 3913451b0418 src/HOL/Matrix/cplex/MatrixLP.thy --- 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 diff -r 51179ca0c429 -r 3913451b0418 src/Pure/IsaMakefile --- 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 diff -r 51179ca0c429 -r 3913451b0418 src/Pure/Tools/ROOT.ML --- 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"; diff -r 51179ca0c429 -r 3913451b0418 src/Pure/Tools/am_compiler.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 diff -r 51179ca0c429 -r 3913451b0418 src/Pure/Tools/am_interpreter.ML --- 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 diff -r 51179ca0c429 -r 3913451b0418 src/Pure/Tools/am_util.ML --- 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 diff -r 51179ca0c429 -r 3913451b0418 src/Pure/Tools/compute.ML --- 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 diff -r 51179ca0c429 -r 3913451b0418 src/Tools/Compute_Oracle/am_compiler.ML --- /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 diff -r 51179ca0c429 -r 3913451b0418 src/Tools/Compute_Oracle/am_interpreter.ML --- /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 diff -r 51179ca0c429 -r 3913451b0418 src/Tools/Compute_Oracle/am_util.ML --- /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 diff -r 51179ca0c429 -r 3913451b0418 src/Tools/Compute_Oracle/compute.ML --- /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