# HG changeset patch # User wenzelm # Date 1121362116 -7200 # Node ID 551462cc8ca02152215e79917b1e1e366316c098 # Parent 35e07087aba215970a0543077d902af4f78984a1 use sys_error instead of exception Internal; actually use Termtab; tuned; diff -r 35e07087aba2 -r 551462cc8ca0 src/Pure/Tools/compute.ML --- a/src/Pure/Tools/compute.ML Thu Jul 14 19:28:34 2005 +0200 +++ b/src/Pure/Tools/compute.ML Thu Jul 14 19:28:36 2005 +0200 @@ -11,7 +11,7 @@ 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 @@ -19,11 +19,9 @@ 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 @@ -36,7 +34,6 @@ | 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) @@ -44,201 +41,212 @@ 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 +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 + | 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 + | 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) + | 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 + 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 + infer end -structure Inttab = TableFun (type key = int val ord=int_ord); - -type computer = theory_ref * (AbstractMachine.term TermTab.table * term AMTermTab.table * int * +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 = +fun basic_make thy raw_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 ths = map (Thm.transfer thy) raw_ths; + + fun thm2rule table invtable ccount th = + let + val prop = Drule.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") - 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") - | _ => ()) + 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 - (* 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) + 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 *) - in - (table, invtable, ccount, (pattern, rename 0 vars right)) - end + 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) - 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) + in + (table, invtable, ccount, (pattern, rename 0 vars right)) + end - val prog = AbstractMachine.compile rules + 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)) + (Theory.self_ref thy, (table, invtable, ccount, prog)) end -fun make thy ths = +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']) @@ -249,23 +257,23 @@ fun compute r naming ct = let - val {t=t, T=ty, thy=ctthy, ...} = rep_cterm ct - val (rthy, (table, invtable, ccount, prog)) = r + 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 + 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)) + t + end fun theory_of (rthy, _) = Theory.deref rthy - -fun default_naming i = "v_"^(Int.toString i) + +fun default_naming i = "v_" ^ Int.toString i exception Param of computer * (int -> string) * cterm; -fun rewrite_param r n ct = +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 @@ -273,17 +281,14 @@ 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 +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') + 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] +val _ = Context.add_setup [Theory.add_oracle ("compute", compute_oracle)] end -