# HG changeset patch # User wenzelm # Date 1125934698 -7200 # Node ID 193b84a70ca4aee2c110006b09dff645780a067b # Parent df7c3b1f390a25f4eb710bebb3634f09565818c8 curried_lookup/update; diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Import/hol4rews.ML Mon Sep 05 17:38:18 2005 +0200 @@ -110,16 +110,12 @@ structure HOL4Imports = TheoryDataFun(HOL4ImportsArgs); fun get_segment2 thyname thy = - let - val imps = HOL4Imports.get thy - in - Symtab.lookup(imps,thyname) - end + Symtab.curried_lookup (HOL4Imports.get thy) thyname fun set_segment thyname segname thy = let val imps = HOL4Imports.get thy - val imps' = Symtab.update_new((thyname,segname),imps) + val imps' = Symtab.curried_update_new (thyname,segname) imps in HOL4Imports.put imps' thy end @@ -295,23 +291,19 @@ fun add_hol4_move bef aft thy = let val curmoves = HOL4Moves.get thy - val newmoves = Symtab.update_new((bef,aft),curmoves) + val newmoves = Symtab.curried_update_new (bef, aft) curmoves in HOL4Moves.put newmoves thy end fun get_hol4_move bef thy = - let - val moves = HOL4Moves.get thy - in - Symtab.lookup(moves,bef) - end + Symtab.curried_lookup (HOL4Moves.get thy) bef fun follow_name thmname thy = let val moves = HOL4Moves.get thy fun F thmname = - case Symtab.lookup(moves,thmname) of + case Symtab.curried_lookup moves thmname of SOME name => F name | NONE => thmname in @@ -321,23 +313,19 @@ fun add_hol4_cmove bef aft thy = let val curmoves = HOL4CMoves.get thy - val newmoves = Symtab.update_new((bef,aft),curmoves) + val newmoves = Symtab.curried_update_new (bef, aft) curmoves in HOL4CMoves.put newmoves thy end fun get_hol4_cmove bef thy = - let - val moves = HOL4CMoves.get thy - in - Symtab.lookup(moves,bef) - end + Symtab.curried_lookup (HOL4CMoves.get thy) bef fun follow_cname thmname thy = let val moves = HOL4CMoves.get thy fun F thmname = - case Symtab.lookup(moves,thmname) of + case Symtab.curried_lookup moves thmname of SOME name => F name | NONE => thmname in diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Matrix/cplex/CplexMatrixConverter.ML --- a/src/HOL/Matrix/cplex/CplexMatrixConverter.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Matrix/cplex/CplexMatrixConverter.ML Mon Sep 05 17:38:18 2005 +0200 @@ -57,14 +57,14 @@ let fun build_naming index i2s s2i [] = (index, i2s, s2i) | build_naming index i2s s2i (cplexBounds (cplexNeg cplexInf, cplexLeq, cplexVar v, cplexLeq, cplexInf)::bounds) - = build_naming (index+1) (Inttab.update ((index, v), i2s)) (Symtab.update_new ((v, index), s2i)) bounds + = build_naming (index+1) (Inttab.curried_update (index, v) i2s) (Symtab.curried_update_new (v, index) s2i) bounds | build_naming _ _ _ _ = raise (Converter "nonfree bound") val (varcount, i2s_tab, s2i_tab) = build_naming 0 Inttab.empty Symtab.empty bounds - fun i2s i = case Inttab.lookup (i2s_tab, i) of NONE => raise (Converter "index not found") + fun i2s i = case Inttab.curried_lookup i2s_tab i of NONE => raise (Converter "index not found") | SOME n => n - fun s2i s = case Symtab.lookup (s2i_tab, s) of NONE => raise (Converter ("name not found: "^s)) + fun s2i s = case Symtab.curried_lookup s2i_tab s of NONE => raise (Converter ("name not found: "^s)) | SOME i => i fun num2str positive (cplexNeg t) = num2str (not positive) t | num2str positive (cplexNum num) = if positive then num else "-"^num diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Mon Sep 05 17:38:18 2005 +0200 @@ -212,7 +212,7 @@ else if (approx_value_term 1 I str) = zero_interval then vector else - Inttab.update ((index, str), vector) + Inttab.curried_update (index, str) vector fun set_vector matrix index vector = if index < 0 then @@ -220,7 +220,7 @@ else if Inttab.is_empty vector then matrix else - Inttab.update ((index, vector), matrix) + Inttab.curried_update (index, vector) matrix val empty_matrix = Inttab.empty val empty_vector = Inttab.empty @@ -232,9 +232,9 @@ fun transpose_matrix matrix = let fun upd m j i x = - case Inttab.lookup (m, j) of - SOME v => Inttab.update ((j, Inttab.update ((i, x), v)), m) - | NONE => Inttab.update ((j, Inttab.update ((i, x), Inttab.empty)), m) + case Inttab.curried_lookup m j of + SOME v => Inttab.curried_update (j, Inttab.curried_update (i, x) v) m + | NONE => Inttab.curried_update (j, Inttab.curried_update (i, x) Inttab.empty) m fun updv j (m, (i, s)) = upd m i j s @@ -258,7 +258,7 @@ fun nameof i = let val s = "x"^(Int.toString i) - val _ = ytable := (Inttab.update ((i, s), !ytable)) + val _ = change ytable (Inttab.curried_update (i, s)) in s end @@ -281,7 +281,7 @@ fun mk_constr index vector c = let - val s = case Inttab.lookup (c, index) of SOME s => s | NONE => "0" + val s = case Inttab.curried_lookup c index of SOME s => s | NONE => "0" val (p, s) = split_numstr s val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s) in @@ -334,7 +334,7 @@ fun mk_constr index vector c = let - val s = case Inttab.lookup (c, index) of SOME s => s | NONE => "0" + val s = case Inttab.curried_lookup c index of SOME s => s | NONE => "0" val (p, s) = split_numstr s val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s) in @@ -358,7 +358,7 @@ val count = ref 0 fun app (v, (i, s)) = if (!count < size) then - (count := !count +1 ; Inttab.update ((i,s),v)) + (count := !count +1 ; Inttab.curried_update (i,s) v) else v in @@ -368,18 +368,18 @@ fun cut_matrix vfilter vsize m = let fun app (m, (i, v)) = - if (Inttab.lookup (vfilter, i) = NONE) then + if Inttab.curried_lookup vfilter i = NONE then m else case vsize of - NONE => Inttab.update ((i,v), m) - | SOME s => Inttab.update((i, cut_vector s v),m) + NONE => Inttab.curried_update (i,v) m + | SOME s => Inttab.curried_update (i, cut_vector s v) m in Inttab.foldl app (empty_matrix, m) end -fun v_elem_at v i = Inttab.lookup (v,i) -fun m_elem_at m i = Inttab.lookup (m,i) +fun v_elem_at v i = Inttab.curried_lookup v i +fun m_elem_at m i = Inttab.curried_lookup m i fun v_only_elem v = case Inttab.min_key v of diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Matrix/cplex/fspmlp.ML --- a/src/HOL/Matrix/cplex/fspmlp.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Matrix/cplex/fspmlp.ML Mon Sep 05 17:38:18 2005 +0200 @@ -54,11 +54,11 @@ let val x = case VarGraph.lookup (g, dest_key) of - NONE => (NONE, Inttab.update ((row_index, (row_bound, [])), Inttab.empty)) + NONE => (NONE, Inttab.curried_update (row_index, (row_bound, [])) Inttab.empty) | SOME (sure_bound, f) => (sure_bound, - case Inttab.lookup (f, row_index) of - NONE => Inttab.update ((row_index, (row_bound, [])), f) + case Inttab.curried_lookup f row_index of + NONE => Inttab.curried_update (row_index, (row_bound, [])) f | SOME _ => raise (Internal "add_row_bound")) in VarGraph.update ((dest_key, x), g) @@ -88,7 +88,7 @@ case VarGraph.lookup (g, key) of NONE => NONE | SOME (sure_bound, f) => - (case Inttab.lookup (f, row_index) of + (case Inttab.curried_lookup f row_index of NONE => NONE | SOME (row_bound, _) => (sure_bound, row_bound))*) @@ -96,10 +96,10 @@ case VarGraph.lookup (g, dest_key) of NONE => raise (Internal "add_edge: dest_key not found") | SOME (sure_bound, f) => - (case Inttab.lookup (f, row_index) of + (case Inttab.curried_lookup f row_index of NONE => raise (Internal "add_edge: row_index not found") | SOME (row_bound, sources) => - VarGraph.update ((dest_key, (sure_bound, Inttab.update ((row_index, (row_bound, (coeff, src_key) :: sources)), f))), g)) + VarGraph.curried_update (dest_key, (sure_bound, Inttab.curried_update (row_index, (row_bound, (coeff, src_key) :: sources)) f)) g) fun split_graph g = let @@ -108,8 +108,8 @@ NONE => (r1, r2) | SOME bound => (case key of - (u, UPPER) => (r1, Inttab.update ((u, bound), r2)) - | (u, LOWER) => (Inttab.update ((u, bound), r1), r2)) + (u, UPPER) => (r1, Inttab.curried_update (u, bound) r2) + | (u, LOWER) => (Inttab.curried_update (u, bound) r1, r2)) in VarGraph.foldl split ((Inttab.empty, Inttab.empty), g) end @@ -195,7 +195,7 @@ let val empty = Inttab.empty - fun instab t i x = Inttab.update ((i,x), t) + fun instab t i x = Inttab.curried_update (i, x) t fun isnegstr x = String.isPrefix "-" x fun negstr x = if isnegstr x then String.extract (x, 1, NONE) else "-"^x @@ -280,8 +280,8 @@ let val index = xlen-i val (r, (r12_1, r12_2)) = abs_estimate (i-1) r1 r2 - val b1 = case Inttab.lookup (r1, index) of NONE => raise (Load ("x-value not bounded from below: "^(names index))) | SOME x => x - val b2 = case Inttab.lookup (r2, index) of NONE => raise (Load ("x-value not bounded from above: "^(names index))) | SOME x => x + val b1 = case Inttab.curried_lookup r1 index of NONE => raise (Load ("x-value not bounded from below: "^(names index))) | SOME x => x + val b2 = case Inttab.curried_lookup r2 index of NONE => raise (Load ("x-value not bounded from above: "^(names index))) | SOME x => x val abs_max = FloatArith.max (FloatArith.neg (FloatArith.negative_part b1)) (FloatArith.positive_part b2) in (add_row_entry r index abs_max, (add_row_entry r12_1 index b1, add_row_entry r12_2 index b2)) diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/ATP/res_clasimpset.ML --- a/src/HOL/Tools/ATP/res_clasimpset.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML Mon Sep 05 17:38:18 2005 +0200 @@ -57,15 +57,14 @@ fun axioms_having_consts_aux [] tab thms = thms | axioms_having_consts_aux (c::cs) tab thms = - let val thms1 = Symtab.lookup(tab,c) - val thms2 = - case thms1 of (SOME x) => x - | NONE => [] + let val thms1 = Symtab.curried_lookup tab c + val thms2 = + case thms1 of (SOME x) => x + | NONE => [] in - axioms_having_consts_aux cs tab (thms2 union thms) + axioms_having_consts_aux cs tab (thms2 union thms) end; - fun axioms_having_consts cs tab = axioms_having_consts_aux cs tab []; diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Mon Sep 05 17:38:18 2005 +0200 @@ -168,7 +168,7 @@ val inject = map (fn r => r RS iffD1) (if i < length newTs then List.nth (constr_inject, i) - else #inject (valOf (Symtab.lookup (dt_info, tname)))); + else #inject (the (Symtab.curried_lookup dt_info tname))); fun mk_unique_constr_tac n ((tac, intr::intrs, j), (cname, cargs)) = let diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/datatype_aux.ML --- a/src/HOL/Tools/datatype_aux.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/datatype_aux.ML Mon Sep 05 17:38:18 2005 +0200 @@ -299,7 +299,7 @@ Sign.string_of_typ sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg); fun get_dt_descr T i tname dts = - (case Symtab.lookup (dt_info, tname) of + (case Symtab.curried_lookup dt_info tname of NONE => typ_error T (tname ^ " is not a datatype - can't use it in\ \ nested recursion") | (SOME {index, descr, ...}) => diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/datatype_codegen.ML Mon Sep 05 17:38:18 2005 +0200 @@ -281,7 +281,7 @@ | _ => NONE); fun datatype_tycodegen thy defs gr dep module brack (Type (s, Ts)) = - (case Symtab.lookup (DatatypePackage.get_datatypes thy, s) of + (case Symtab.curried_lookup (DatatypePackage.get_datatypes thy) s of NONE => NONE | SOME {descr, ...} => if isSome (get_assoc_type thy s) then NONE else diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/datatype_package.ML Mon Sep 05 17:38:18 2005 +0200 @@ -104,7 +104,7 @@ (** theory information about datatypes **) -fun datatype_info thy name = Symtab.lookup (get_datatypes thy, name); +val datatype_info = Symtab.curried_lookup o get_datatypes; fun datatype_info_err thy name = (case datatype_info thy name of SOME info => info @@ -681,7 +681,7 @@ Theory.add_path (space_implode "_" new_type_names) |> add_rules simps case_thms size_thms rec_thms inject distinct weak_case_congs Simplifier.cong_add_global |> - put_datatypes (foldr Symtab.update dt_info dt_infos) |> + put_datatypes (fold Symtab.curried_update dt_infos dt_info) |> add_cases_induct dt_infos induct |> Theory.parent_path |> (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |> @@ -739,7 +739,7 @@ Theory.add_path (space_implode "_" new_type_names) |> add_rules simps case_thms size_thms rec_thms inject distinct weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> - put_datatypes (foldr Symtab.update dt_info dt_infos) |> + put_datatypes (fold Symtab.curried_update dt_infos dt_info) |> add_cases_induct dt_infos induct |> Theory.parent_path |> (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |> @@ -847,7 +847,7 @@ Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |> add_rules simps case_thms size_thms rec_thms inject distinct weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> - put_datatypes (foldr Symtab.update dt_info dt_infos) |> + put_datatypes (fold Symtab.curried_update dt_infos dt_info) |> add_cases_induct dt_infos induction' |> Theory.parent_path |> (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |> diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Mon Sep 05 17:38:18 2005 +0200 @@ -35,7 +35,7 @@ fun exh_thm_of (dt_info : datatype_info Symtab.table) tname = - #exhaustion (valOf (Symtab.lookup (dt_info, tname))); + #exhaustion (the (Symtab.curried_lookup dt_info tname)); (******************************************************************************) @@ -356,7 +356,7 @@ let val ks = map fst ds; val (_, (tname, _, _)) = hd ds; - val {rec_rewrites, rec_names, ...} = valOf (Symtab.lookup (dt_info, tname)); + val {rec_rewrites, rec_names, ...} = the (Symtab.curried_lookup dt_info tname); fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) = let @@ -412,7 +412,7 @@ fun prove_iso_thms (ds, (inj_thms, elem_thms)) = let val (_, (tname, _, _)) = hd ds; - val {induction, ...} = valOf (Symtab.lookup (dt_info, tname)); + val {induction, ...} = the (Symtab.curried_lookup dt_info tname); fun mk_ind_concl (i, _) = let diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Mon Sep 05 17:38:18 2005 +0200 @@ -55,9 +55,8 @@ Const (s, _) => let val cs = foldr add_term_consts [] (prems_of thm) in (CodegenData.put - {intros = Symtab.update ((s, - getOpt (Symtab.lookup (intros, s), []) @ - [(thm, thyname_of s)]), intros), + {intros = intros |> + Symtab.curried_update (s, Symtab.curried_lookup_multi intros s @ [(thm, thyname_of s)]), graph = foldr (uncurry (Graph.add_edge o pair s)) (Library.foldl add_node (graph, s :: cs)) cs, eqns = eqns} thy, thm) @@ -66,16 +65,15 @@ | _ $ (Const ("op =", _) $ t $ _) => (case head_of t of Const (s, _) => (CodegenData.put {intros = intros, graph = graph, - eqns = Symtab.update ((s, - getOpt (Symtab.lookup (eqns, s), []) @ - [(thm, thyname_of s)]), eqns)} thy, thm) + eqns = eqns |> Symtab.curried_update + (s, Symtab.curried_lookup_multi eqns s @ [(thm, thyname_of s)])} thy, thm) | _ => (warn thm; p)) | _ => (warn thm; p)) end; fun get_clauses thy s = let val {intros, graph, ...} = CodegenData.get thy - in case Symtab.lookup (intros, s) of + in case Symtab.curried_lookup intros s of NONE => (case InductivePackage.get_inductive thy s of NONE => NONE | SOME ({names, ...}, {intrs, ...}) => @@ -86,7 +84,7 @@ val SOME names = find_first (fn xs => s mem xs) (Graph.strong_conn graph); val intrs = List.concat (map - (fn s => valOf (Symtab.lookup (intros, s))) names); + (fn s => the (Symtab.curried_lookup intros s)) names); val (_, (_, thyname)) = split_last intrs in SOME (names, thyname, preprocess thy (map fst intrs)) end end; @@ -718,7 +716,7 @@ (Pretty.block [Pretty.str "?! (", call_p, Pretty.str ")"]))) handle TERM _ => mk_ind_call thy defs gr dep module t u true) | inductive_codegen thy defs gr dep module brack t = (case strip_comb t of - (Const (s, _), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy), s) of + (Const (s, _), ts) => (case Symtab.curried_lookup (#eqns (CodegenData.get thy)) s of NONE => list_of_indset thy defs gr dep module brack t | SOME eqns => let diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/inductive_package.ML Mon Sep 05 17:38:18 2005 +0200 @@ -112,7 +112,7 @@ (* get and put data *) -fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name); +val get_inductive = Symtab.curried_lookup o #1 o InductiveData.get; fun the_inductive thy name = (case get_inductive thy name of @@ -123,7 +123,7 @@ fun put_inductives names info thy = let - fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos); + fun upd ((tab, monos), name) = (Symtab.curried_update_new (name, info) tab, monos); val tab_monos = Library.foldl upd (InductiveData.get thy, names) handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name); in InductiveData.put tab_monos thy end; diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/primrec_package.ML Mon Sep 05 17:38:18 2005 +0200 @@ -205,7 +205,7 @@ fun find_dts (dt_info : datatype_info Symtab.table) _ [] = [] | find_dts dt_info tnames' (tname::tnames) = - (case Symtab.lookup (dt_info, tname) of + (case Symtab.curried_lookup dt_info tname of NONE => primrec_err (quote tname ^ " is not a datatype") | SOME dt => if tnames' subset (map (#1 o snd) (#descr dt)) then diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/recdef_package.ML --- a/src/HOL/Tools/recdef_package.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/recdef_package.ML Mon Sep 05 17:38:18 2005 +0200 @@ -127,12 +127,12 @@ val print_recdefs = GlobalRecdefData.print; -fun get_recdef thy name = Symtab.lookup (#1 (GlobalRecdefData.get thy), name); +val get_recdef = Symtab.curried_lookup o #1 o GlobalRecdefData.get; fun put_recdef name info thy = let val (tab, hints) = GlobalRecdefData.get thy; - val tab' = Symtab.update_new ((name, info), tab) + val tab' = Symtab.curried_update_new (name, info) tab handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name); in GlobalRecdefData.put (tab', hints) thy end; diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Mon Sep 05 17:38:18 2005 +0200 @@ -42,8 +42,7 @@ val (s, _) = const_of (prop_of thm); in if Pattern.pattern (lhs_of thm) then - (CodegenData.put (Symtab.update ((s, - (thm, optmod) :: getOpt (Symtab.lookup (tab, s), [])), tab)) thy, thm) + (CodegenData.put (Symtab.curried_update_multi (s, (thm, optmod)) tab) thy, thm) else (warn thm; p) end handle TERM _ => (warn thm; p); @@ -51,10 +50,10 @@ let val tab = CodegenData.get thy; val (s, _) = const_of (prop_of thm); - in case Symtab.lookup (tab, s) of + in case Symtab.curried_lookup tab s of NONE => p - | SOME thms => (CodegenData.put (Symtab.update ((s, - gen_rem (eq_thm o apfst fst) (thms, thm)), tab)) thy, thm) + | SOME thms => (CodegenData.put (Symtab.curried_update (s, + gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy, thm) end handle TERM _ => (warn thm; p); fun del_redundant thy eqs [] = eqs @@ -65,7 +64,7 @@ in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end; fun get_equations thy defs (s, T) = - (case Symtab.lookup (CodegenData.get thy, s) of + (case Symtab.curried_lookup (CodegenData.get thy) s of NONE => ([], "") | SOME thms => let val thms' = del_redundant thy [] diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/record_package.ML Mon Sep 05 17:38:18 2005 +0200 @@ -17,7 +17,7 @@ val record_split_name: string val record_split_wrapper: string * wrapper val print_record_type_abbr: bool ref - val print_record_type_as_fields: bool ref + val print_record_type_as_fields: bool ref end; signature RECORD_PACKAGE = @@ -43,7 +43,7 @@ end; -structure RecordPackage:RECORD_PACKAGE = +structure RecordPackage:RECORD_PACKAGE = struct val rec_UNIV_I = thm "rec_UNIV_I"; @@ -63,7 +63,7 @@ val wN = "w"; val moreN = "more"; val schemeN = "_scheme"; -val ext_typeN = "_ext_type"; +val ext_typeN = "_ext_type"; val extN ="_ext"; val casesN = "_cases"; val ext_dest = "_sel"; @@ -94,7 +94,7 @@ fun timeit_msg s x = if !timing then (warning s; timeit x) else x (); fun timing_msg s = if !timing then warning s else (); - + (* syntax *) fun prune n xs = Library.drop (n, xs); @@ -136,9 +136,9 @@ fun mk_casesC (name,T,vT) Ts = (suffix casesN name, (Ts ---> vT) --> T --> vT) fun mk_cases (name,T,vT) f = - let val Ts = binder_types (fastype_of f) + let val Ts = binder_types (fastype_of f) in Const (mk_casesC (name,T,vT) Ts) $ f end; - + (* selector *) fun mk_selC sT (c,T) = (c,sT --> T); @@ -165,7 +165,7 @@ | dest_recT typ = raise TYPE ("RecordPackage.dest_recT", [typ], []); fun is_recT T = - (case try dest_recT T of NONE => false | SOME _ => true); + (case try dest_recT T of NONE => false | SOME _ => true); fun dest_recTs T = let val ((c, Ts), U) = dest_recT T @@ -179,7 +179,7 @@ | SOME l => SOME l) end handle TYPE _ => NONE -fun rec_id i T = +fun rec_id i T = let val rTs = dest_recTs T val rTs' = if i < 0 then rTs else Library.take (i,rTs) in Library.foldl (fn (s,(c,T)) => s ^ c) ("",rTs') end; @@ -199,7 +199,7 @@ }; fun make_record_info args parent fields extension induct = - {args = args, parent = parent, fields = fields, extension = extension, + {args = args, parent = parent, fields = fields, extension = extension, induct = induct}: record_info; @@ -224,20 +224,20 @@ equalities: thm Symtab.table, extinjects: thm list, extsplit: thm Symtab.table, (* maps extension name to split rule *) - splits: (thm*thm*thm*thm) Symtab.table, (* !!,!,EX - split-equalities,induct rule *) + splits: (thm*thm*thm*thm) Symtab.table, (* !!,!,EX - split-equalities,induct rule *) extfields: (string*typ) list Symtab.table, (* maps extension to its fields *) fieldext: (string*typ list) Symtab.table (* maps field to its extension *) }; -fun make_record_data +fun make_record_data records sel_upd equalities extinjects extsplit splits extfields fieldext = - {records = records, sel_upd = sel_upd, - equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits, + {records = records, sel_upd = sel_upd, + equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits, extfields = extfields, fieldext = fieldext }: record_data; structure RecordsData = TheoryDataFun (struct - val name = "HOL/records"; + val name = "HOL/records"; type T = record_data; val empty = @@ -251,7 +251,7 @@ ({records = recs1, sel_upd = {selectors = sels1, updates = upds1, simpset = ss1}, equalities = equalities1, - extinjects = extinjects1, + extinjects = extinjects1, extsplit = extsplit1, splits = splits1, extfields = extfields1, @@ -259,12 +259,12 @@ {records = recs2, sel_upd = {selectors = sels2, updates = upds2, simpset = ss2}, equalities = equalities2, - extinjects = extinjects2, - extsplit = extsplit2, + extinjects = extinjects2, + extsplit = extsplit2, splits = splits2, extfields = extfields2, fieldext = fieldext2}) = - make_record_data + make_record_data (Symtab.merge (K true) (recs1, recs2)) {selectors = Symtab.merge (K true) (sels1, sels2), updates = Symtab.merge (K true) (upds1, upds2), @@ -272,9 +272,9 @@ (Symtab.merge Thm.eq_thm (equalities1, equalities2)) (gen_merge_lists Thm.eq_thm extinjects1 extinjects2) (Symtab.merge Thm.eq_thm (extsplit1,extsplit2)) - (Symtab.merge (fn ((a,b,c,d),(w,x,y,z)) - => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso - Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z)) + (Symtab.merge (fn ((a,b,c,d),(w,x,y,z)) + => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso + Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z)) (splits1, splits2)) (Symtab.merge (K true) (extfields1,extfields2)) (Symtab.merge (K true) (fieldext1,fieldext2)); @@ -303,13 +303,13 @@ (* access 'records' *) -fun get_record thy name = Symtab.lookup (#records (RecordsData.get thy), name); +val get_record = Symtab.curried_lookup o #records o RecordsData.get; fun put_record name info thy = let - val {records, sel_upd, equalities, extinjects,extsplit,splits,extfields,fieldext} = + val {records, sel_upd, equalities, extinjects,extsplit,splits,extfields,fieldext} = RecordsData.get thy; - val data = make_record_data (Symtab.update ((name, info), records)) + val data = make_record_data (Symtab.curried_update (name, info) records) sel_upd equalities extinjects extsplit splits extfields fieldext; in RecordsData.put data thy end; @@ -317,22 +317,18 @@ val get_sel_upd = #sel_upd o RecordsData.get; -fun get_selectors sg name = Symtab.lookup (#selectors (get_sel_upd sg), name); -fun is_selector sg name = - case get_selectors sg (Sign.intern_const sg name) of - NONE => false - | SOME _ => true +val get_selectors = Symtab.curried_lookup o #selectors o get_sel_upd; +fun is_selector sg name = is_some (get_selectors sg (Sign.intern_const sg name)); - -fun get_updates sg name = Symtab.lookup (#updates (get_sel_upd sg), name); -fun get_simpset sg = #simpset (get_sel_upd sg); +val get_updates = Symtab.curried_lookup o #updates o get_sel_upd; +val get_simpset = #simpset o get_sel_upd; fun put_sel_upd names simps thy = let val sels = map (rpair ()) names; val upds = map (suffix updateN) names ~~ names; - val {records, sel_upd = {selectors, updates, simpset}, + val {records, sel_upd = {selectors, updates, simpset}, equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy; val data = make_record_data records {selectors = Symtab.extend (selectors, sels), @@ -345,23 +341,22 @@ fun add_record_equalities name thm thy = let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy; - val data = make_record_data records sel_upd - (Symtab.update_new ((name, thm), equalities)) extinjects extsplit + val data = make_record_data records sel_upd + (Symtab.curried_update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext; in RecordsData.put data thy end; -fun get_equalities sg name = - Symtab.lookup (#equalities (RecordsData.get sg), name); +val get_equalities =Symtab.curried_lookup o #equalities o RecordsData.get; (* access 'extinjects' *) fun add_extinjects thm thy = let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy; - val data = make_record_data records sel_upd equalities (extinjects@[thm]) extsplit + val data = make_record_data records sel_upd equalities (extinjects@[thm]) extsplit splits extfields fieldext; in RecordsData.put data thy end; @@ -371,73 +366,69 @@ fun add_extsplit name thm thy = let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy; - val data = make_record_data records sel_upd - equalities extinjects (Symtab.update_new ((name, thm), extsplit)) splits + val data = make_record_data records sel_upd + equalities extinjects (Symtab.curried_update_new (name, thm) extsplit) splits extfields fieldext; in RecordsData.put data thy end; -fun get_extsplit sg name = - Symtab.lookup (#extsplit (RecordsData.get sg), name); +val get_extsplit = Symtab.curried_lookup o #extsplit o RecordsData.get; (* access 'splits' *) fun add_record_splits name thmP thy = let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy; - val data = make_record_data records sel_upd - equalities extinjects extsplit (Symtab.update_new ((name, thmP), splits)) + val data = make_record_data records sel_upd + equalities extinjects extsplit (Symtab.curried_update_new (name, thmP) splits) extfields fieldext; in RecordsData.put data thy end; -fun get_splits sg name = - Symtab.lookup (#splits (RecordsData.get sg), name); +val get_splits = Symtab.curried_lookup o #splits o RecordsData.get; (* extension of a record name *) -fun get_extension sg name = - case Symtab.lookup (#records (RecordsData.get sg),name) of - SOME s => SOME (#extension s) - | NONE => NONE; +val get_extension = + Option.map #extension oo (Symtab.curried_lookup o #records o RecordsData.get); + (* access 'extfields' *) fun add_extfields name fields thy = let - val {records, sel_upd, equalities, extinjects, extsplit,splits, extfields, fieldext} = + val {records, sel_upd, equalities, extinjects, extsplit,splits, extfields, fieldext} = RecordsData.get thy; - val data = make_record_data records sel_upd - equalities extinjects extsplit splits - (Symtab.update_new ((name, fields), extfields)) fieldext; + val data = make_record_data records sel_upd + equalities extinjects extsplit splits + (Symtab.curried_update_new (name, fields) extfields) fieldext; in RecordsData.put data thy end; -fun get_extfields sg name = - Symtab.lookup (#extfields (RecordsData.get sg), name); +val get_extfields = Symtab.curried_lookup o #extfields o RecordsData.get; -fun get_extT_fields sg T = +fun get_extT_fields sg T = let val ((name,Ts),moreT) = dest_recT T; - val recname = let val (nm::recn::rst) = rev (NameSpace.unpack name) + val recname = let val (nm::recn::rst) = rev (NameSpace.unpack name) in NameSpace.pack (rev (nm::rst)) end; val midx = maxidx_of_typs (moreT::Ts); fun varify (a, S) = TVar ((a, midx), S); val varifyT = map_type_tfree varify; val {records,extfields,...} = RecordsData.get sg; - val (flds,(more,_)) = split_last (Symtab.lookup_multi (extfields,name)); - val args = map varifyT (snd (#extension (valOf (Symtab.lookup (records,recname))))); + val (flds,(more,_)) = split_last (Symtab.curried_lookup_multi extfields name); + val args = map varifyT (snd (#extension (the (Symtab.curried_lookup records recname)))); val (subst,_) = fold (Sign.typ_unify sg) (but_last args ~~ but_last Ts) (Vartab.empty,0); val flds' = map (apsnd ((Envir.norm_type subst) o varifyT)) flds; in (flds',(more,moreT)) end; -fun get_recT_fields sg T = - let +fun get_recT_fields sg T = + let val (root_flds,(root_more,root_moreT)) = get_extT_fields sg T; - val (rest_flds,rest_more) = - if is_recT root_moreT then get_recT_fields sg root_moreT + val (rest_flds,rest_more) = + if is_recT root_moreT then get_recT_fields sg root_moreT else ([],(root_more,root_moreT)); in (root_flds@rest_flds,rest_more) end; @@ -446,17 +437,16 @@ fun add_fieldext extname_types fields thy = let - val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = + val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = RecordsData.get thy; - val fieldext' = Library.foldl (fn (table,field) => Symtab.update_new ((field,extname_types),table)) - (fieldext,fields); - val data=make_record_data records sel_upd equalities extinjects extsplit + val fieldext' = + fold (fn field => Symtab.curried_update_new (field, extname_types)) fields fieldext; + val data=make_record_data records sel_upd equalities extinjects extsplit splits extfields fieldext'; in RecordsData.put data thy end; -fun get_fieldext sg name = - Symtab.lookup (#fieldext (RecordsData.get sg), name); +val get_fieldext = Symtab.curried_lookup o #fieldext o RecordsData.get; (* parent records *) @@ -522,9 +512,9 @@ | dest_ext_fields _ mark t = [dest_ext_field mark t] fun gen_ext_fields_tr sep mark sfx more sg t = - let + let val msg = "error in record input: "; - val fieldargs = dest_ext_fields sep mark t; + val fieldargs = dest_ext_fields sep mark t; fun splitargs (field::fields) ((name,arg)::fargs) = if can (unsuffix name) field then let val (args,rest) = splitargs fields fargs @@ -537,10 +527,10 @@ fun mk_ext (fargs as (name,arg)::_) = (case get_fieldext sg (Sign.intern_const sg name) of SOME (ext,_) => (case get_extfields sg ext of - SOME flds - => let val (args,rest) = + SOME flds + => let val (args,rest) = splitargs (map fst (but_last flds)) fargs; - val more' = mk_ext rest; + val more' = mk_ext rest; in list_comb (Syntax.const (suffix sfx ext),args@[more']) end | NONE => raise TERM(msg ^ "no fields defined for " @@ -548,12 +538,12 @@ | NONE => raise TERM (msg ^ name ^" is no proper field",[t])) | mk_ext [] = more - in mk_ext fieldargs end; + in mk_ext fieldargs end; fun gen_ext_type_tr sep mark sfx more sg t = - let + let val msg = "error in record-type input: "; - val fieldargs = dest_ext_fields sep mark t; + val fieldargs = dest_ext_fields sep mark t; fun splitargs (field::fields) ((name,arg)::fargs) = if can (unsuffix name) field then let val (args,rest) = splitargs fields fargs @@ -563,77 +553,77 @@ | splitargs (_::_) [] = raise TERM (msg ^ "expecting more fields", [t]) | splitargs _ _ = ([],[]); - fun get_sort xs n = (case assoc (xs,n) of - SOME s => s + fun get_sort xs n = (case assoc (xs,n) of + SOME s => s | NONE => Sign.defaultS sg); - - + + fun to_type t = Sign.certify_typ sg - (Sign.intern_typ sg + (Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t)); fun mk_ext (fargs as (name,arg)::_) = (case get_fieldext sg (Sign.intern_const sg name) of - SOME (ext,alphas) => + SOME (ext,alphas) => (case get_extfields sg ext of - SOME flds + SOME flds => (let val flds' = but_last flds; - val types = map snd flds'; + val types = map snd flds'; val (args,rest) = splitargs (map fst flds') fargs; val vartypes = map Type.varifyT types; val argtypes = map to_type args; val (subst,_) = fold (Sign.typ_unify sg) (vartypes ~~ argtypes) (Vartab.empty,0); - val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o - Envir.norm_type subst o Type.varifyT) + val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o + Envir.norm_type subst o Type.varifyT) (but_last alphas); - - val more' = mk_ext rest; - in list_comb (Syntax.const (suffix sfx ext),alphas'@[more']) - end handle TUNIFY => raise + + val more' = mk_ext rest; + in list_comb (Syntax.const (suffix sfx ext),alphas'@[more']) + end handle TUNIFY => raise TERM (msg ^ "type is no proper record (extension)", [t])) | NONE => raise TERM (msg ^ "no fields defined for " ^ ext,[t])) | NONE => raise TERM (msg ^ name ^" is no proper field",[t])) | mk_ext [] = more - in mk_ext fieldargs end; + in mk_ext fieldargs end; -fun gen_adv_record_tr sep mark sfx unit sg [t] = +fun gen_adv_record_tr sep mark sfx unit sg [t] = gen_ext_fields_tr sep mark sfx unit sg t | gen_adv_record_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts); -fun gen_adv_record_scheme_tr sep mark sfx sg [t, more] = - gen_ext_fields_tr sep mark sfx more sg t +fun gen_adv_record_scheme_tr sep mark sfx sg [t, more] = + gen_ext_fields_tr sep mark sfx more sg t | gen_adv_record_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts); -fun gen_adv_record_type_tr sep mark sfx unit sg [t] = +fun gen_adv_record_type_tr sep mark sfx unit sg [t] = gen_ext_type_tr sep mark sfx unit sg t | gen_adv_record_type_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts); -fun gen_adv_record_type_scheme_tr sep mark sfx sg [t, more] = - gen_ext_type_tr sep mark sfx more sg t +fun gen_adv_record_type_scheme_tr sep mark sfx sg [t, more] = + gen_ext_type_tr sep mark sfx more sg t | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts); val adv_record_tr = gen_adv_record_tr "_fields" "_field" extN HOLogic.unit; val adv_record_scheme_tr = gen_adv_record_scheme_tr "_fields" "_field" extN; -val adv_record_type_tr = - gen_adv_record_type_tr "_field_types" "_field_type" ext_typeN +val adv_record_type_tr = + gen_adv_record_type_tr "_field_types" "_field_type" ext_typeN (Syntax.term_of_typ false (HOLogic.unitT)); -val adv_record_type_scheme_tr = +val adv_record_type_scheme_tr = gen_adv_record_type_scheme_tr "_field_types" "_field_type" ext_typeN; val parse_translation = [("_record_update", record_update_tr), - ("_update_name", update_name_tr)]; + ("_update_name", update_name_tr)]; -val adv_parse_translation = +val adv_parse_translation = [("_record",adv_record_tr), ("_record_scheme",adv_record_scheme_tr), ("_record_type",adv_record_type_tr), - ("_record_type_scheme",adv_record_type_scheme_tr)]; + ("_record_type_scheme",adv_record_type_scheme_tr)]; (* print translations *) @@ -658,18 +648,18 @@ in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end; fun record_tr' sep mark record record_scheme unit sg t = - let + let fun field_lst t = (case strip_comb t of - (Const (ext,_),args) + (Const (ext,_),args) => (case try (unsuffix extN) (Sign.intern_const sg ext) of - SOME ext' + SOME ext' => (case get_extfields sg ext' of - SOME flds + SOME flds => (let val (f::fs) = but_last (map fst flds); - val flds' = Sign.extern_const sg f :: map NameSpace.base fs; - val (args',more) = split_last args; + val flds' = Sign.extern_const sg f :: map NameSpace.base fs; + val (args',more) = split_last args; in (flds'~~args')@field_lst more end handle UnequalLengths => [("",t)]) | NONE => [("",t)]) @@ -681,15 +671,15 @@ val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds'; in if null flds then raise Match - else if unit more - then Syntax.const record$flds'' + else if unit more + then Syntax.const record$flds'' else Syntax.const record_scheme$flds''$more end -fun gen_record_tr' name = +fun gen_record_tr' name = let val name_sfx = suffix extN name; val unit = (fn Const ("Unity",_) => true | _ => false); - fun tr' sg ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit sg + fun tr' sg ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit sg (list_comb (Syntax.const name_sfx,ts)) in (name_sfx,tr') end @@ -704,46 +694,46 @@ (* tm is term representation of a (nested) field type. We first reconstruct the *) (* type from tm so that we can continue on the type level rather then the term level.*) - fun get_sort xs n = (case assoc (xs,n) of - SOME s => s + fun get_sort xs n = (case assoc (xs,n) of + SOME s => s | NONE => Sign.defaultS sg); (* WORKAROUND: - * If a record type occurs in an error message of type inference there + * If a record type occurs in an error message of type inference there * may be some internal frees donoted by ??: - * (Const "_tfree",_)$Free ("??'a",_). - - * This will unfortunately be translated to Type ("??'a",[]) instead of - * TFree ("??'a",_) by typ_of_term, which will confuse unify below. + * (Const "_tfree",_)$Free ("??'a",_). + + * This will unfortunately be translated to Type ("??'a",[]) instead of + * TFree ("??'a",_) by typ_of_term, which will confuse unify below. * fixT works around. *) - fun fixT (T as Type (x,[])) = + fun fixT (T as Type (x,[])) = if String.isPrefix "??'" x then TFree (x,Sign.defaultS sg) else T | fixT (Type (x,xs)) = Type (x,map fixT xs) | fixT T = T; - - val T = fixT (Sign.intern_typ sg - (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm)); + + val T = fixT (Sign.intern_typ sg + (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm)); - fun mk_type_abbr subst name alphas = + fun mk_type_abbr subst name alphas = let val abbrT = Type (name, map (fn a => TVar ((a, 0), Sign.defaultS sg)) alphas); - in Syntax.term_of_typ (! Syntax.show_sorts) - (Sign.extern_typ sg (Envir.norm_type subst abbrT)) end; + in Syntax.term_of_typ (! Syntax.show_sorts) + (Sign.extern_typ sg (Envir.norm_type subst abbrT)) end; fun unify rT T = fst (Sign.typ_unify sg (Type.varifyT rT,T) (Vartab.empty,0)); in if !print_record_type_abbr then (case last_extT T of - SOME (name,_) - => if name = lastExt + SOME (name,_) + => if name = lastExt then - (let - val subst = unify schemeT T - in + (let + val subst = unify schemeT T + in if HOLogic.is_unitT (Envir.norm_type subst (TVar((zeta,0),Sign.defaultS sg))) then mk_type_abbr subst abbr alphas else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta]) - end handle TUNIFY => default_tr' sg tm) + end handle TUNIFY => default_tr' sg tm) else raise Match (* give print translation of specialised record a chance *) | _ => raise Match) else default_tr' sg tm @@ -751,39 +741,39 @@ fun record_type_tr' sep mark record record_scheme sg t = let - fun get_sort xs n = (case assoc (xs,n) of - SOME s => s + fun get_sort xs n = (case assoc (xs,n) of + SOME s => s | NONE => Sign.defaultS sg); val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t) fun term_of_type T = Syntax.term_of_typ (!Syntax.show_sorts) (Sign.extern_typ sg T); - + fun field_lst T = (case T of - Type (ext,args) + Type (ext,args) => (case try (unsuffix ext_typeN) ext of - SOME ext' + SOME ext' => (case get_extfields sg ext' of - SOME flds + SOME flds => (case get_fieldext sg (fst (hd flds)) of - SOME (_,alphas) + SOME (_,alphas) => (let val (f::fs) = but_last flds; val flds' = apfst (Sign.extern_const sg) f - ::map (apfst NameSpace.base) fs; - val (args',more) = split_last args; - val alphavars = map Type.varifyT (but_last alphas); + ::map (apfst NameSpace.base) fs; + val (args',more) = split_last args; + val alphavars = map Type.varifyT (but_last alphas); val (subst,_)= fold (Sign.typ_unify sg) (alphavars~~args') (Vartab.empty,0); val flds'' =map (apsnd (Envir.norm_type subst o Type.varifyT)) flds'; in flds''@field_lst more end - handle TUNIFY => [("",T)] + handle TUNIFY => [("",T)] | UnequalLengths => [("",T)]) | NONE => [("",T)]) | NONE => [("",T)]) - | NONE => [("",T)]) + | NONE => [("",T)]) | _ => [("",T)]) val (flds,(_,moreT)) = split_last (field_lst T); @@ -791,25 +781,25 @@ val flds'' = foldr1 (fn (x,y) => Syntax.const sep$x$y) flds'; in if not (!print_record_type_as_fields) orelse null flds then raise Match - else if moreT = HOLogic.unitT - then Syntax.const record$flds'' + else if moreT = HOLogic.unitT + then Syntax.const record$flds'' else Syntax.const record_scheme$flds''$term_of_type moreT end - + -fun gen_record_type_tr' name = +fun gen_record_type_tr' name = let val name_sfx = suffix ext_typeN name; - fun tr' sg ts = record_type_tr' "_field_types" "_field_type" - "_record_type" "_record_type_scheme" sg + fun tr' sg ts = record_type_tr' "_field_types" "_field_type" + "_record_type" "_record_type_scheme" sg (list_comb (Syntax.const name_sfx,ts)) in (name_sfx,tr') end - + fun gen_record_type_abbr_tr' abbr alphas zeta lastExt schemeT name = let val name_sfx = suffix ext_typeN name; - val default_tr' = record_type_tr' "_field_types" "_field_type" - "_record_type" "_record_type_scheme" + val default_tr' = record_type_tr' "_field_types" "_field_type" + "_record_type" "_record_type_scheme" fun tr' sg ts = record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT sg (list_comb (Syntax.const name_sfx,ts)) in (name_sfx, tr') end; @@ -824,27 +814,27 @@ then Tactic.prove sg [] [] (Logic.list_implies (map Logic.varify asms,Logic.varify prop)) (K (SkipProof.cheat_tac HOL.thy)) (* standard can take quite a while for large records, thats why - * we varify the proposition manually here.*) + * we varify the proposition manually here.*) else let val prf = Tactic.prove sg [] asms prop tac; - in if stndrd then standard prf else prf end; + in if stndrd then standard prf else prf end; -fun quick_and_dirty_prf noopt opt () = - if !record_quick_and_dirty_sensitive andalso !quick_and_dirty +fun quick_and_dirty_prf noopt opt () = + if !record_quick_and_dirty_sensitive andalso !quick_and_dirty then noopt () else opt (); fun prove_split_simp sg ss T prop = - let + let val {sel_upd={simpset,...},extsplit,...} = RecordsData.get sg; - val extsplits = - Library.foldl (fn (thms,(n,_)) => (list (Symtab.lookup (extsplit,n)))@thms) + val extsplits = + Library.foldl (fn (thms,(n,_)) => list (Symtab.curried_lookup extsplit n) @ thms) ([],dest_recTs T); val thms = (case get_splits sg (rec_id (~1) T) of - SOME (all_thm,_,_,_) => + SOME (all_thm,_,_,_) => all_thm::(case extsplits of [thm] => [] | _ => extsplits) (* [thm] is the same as all_thm *) - | NONE => extsplits) + | NONE => extsplits) in quick_and_dirty_prove true sg [] prop (fn _ => simp_tac (Simplifier.inherit_bounds ss simpset addsimps thms) 1) @@ -854,7 +844,7 @@ local fun eq (s1:string) (s2:string) = (s1 = s2); fun has_field extfields f T = - exists (fn (eN,_) => exists (eq f o fst) (Symtab.lookup_multi (extfields,eN))) + exists (fn (eN,_) => exists (eq f o fst) (Symtab.curried_lookup_multi extfields eN)) (dest_recTs T); in (* record_simproc *) @@ -867,7 +857,7 @@ * - If S is a more-selector we have to make sure that the update on component * X does not affect the selected subrecord. * - If X is a more-selector we have to make sure that S is not in the updated - * subrecord. + * subrecord. *) val record_simproc = Simplifier.simproc (Theory.sign_of HOL.thy) "record_simp" ["s (u k r)"] @@ -878,42 +868,42 @@ (case get_updates sg u of SOME u_name => let val {sel_upd={updates,...},extfields,...} = RecordsData.get sg; - + fun mk_eq_terms ((upd as Const (u,Type(_,[kT,_]))) $ k $ r) = - (case (Symtab.lookup (updates,u)) of + (case Symtab.curried_lookup updates u of NONE => NONE - | SOME u_name + | SOME u_name => if u_name = s - then let + then let val rv = ("r",rT) val rb = Bound 0 val kv = ("k",kT) - val kb = Bound 1 + val kb = Bound 1 in SOME (upd$kb$rb,kb,[kv,rv],true) end else if has_field extfields u_name rangeS orelse has_field extfields s kT then NONE - else (case mk_eq_terms r of - SOME (trm,trm',vars,update_s) - => let - val kv = ("k",kT) + else (case mk_eq_terms r of + SOME (trm,trm',vars,update_s) + => let + val kv = ("k",kT) val kb = Bound (length vars) - in SOME (upd$kb$trm,trm',kv::vars,update_s) end + in SOME (upd$kb$trm,trm',kv::vars,update_s) end | NONE - => let - val rv = ("r",rT) + => let + val rv = ("r",rT) val rb = Bound 0 val kv = ("k",kT) - val kb = Bound 1 + val kb = Bound 1 in SOME (upd$kb$rb,rb,[kv,rv],false) end)) - | mk_eq_terms r = NONE + | mk_eq_terms r = NONE in - (case mk_eq_terms (upd$k$r) of - SOME (trm,trm',vars,update_s) - => if update_s - then SOME (prove_split_simp sg ss domS + (case mk_eq_terms (upd$k$r) of + SOME (trm,trm',vars,update_s) + => if update_s + then SOME (prove_split_simp sg ss domS (list_all(vars,(equals rangeS$(sel$trm)$trm')))) - else SOME (prove_split_simp sg ss domS + else SOME (prove_split_simp sg ss domS (list_all(vars,(equals rangeS$(sel$trm)$(sel$trm'))))) | NONE => NONE) end @@ -921,91 +911,91 @@ | NONE => NONE) | _ => NONE)); -(* record_upd_simproc *) +(* record_upd_simproc *) (* simplify multiple updates: * (1) "r(|M:=3,N:=1,M:=2,N:=4|) == r(|M:=2,N:=4|)" * (2) "r(|M:= M r|) = r" * For (2) special care of "more" updates has to be taken: * r(|more := m; A := A r|) * If A is contained in the fields of m we cannot remove the update A := A r! - * (But r(|more := r; A := A (r(|more := r|))|) = r(|more := r|) + * (But r(|more := r; A := A (r(|more := r|))|) = r(|more := r|) *) val record_upd_simproc = Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u k r)"] (fn sg => fn ss => fn t => (case t of ((upd as Const (u, Type(_,[_,Type(_,[rT,_])]))) $ k $ r) => - let datatype ('a,'b) calc = Init of 'b | Inter of 'a + let datatype ('a,'b) calc = Init of 'b | Inter of 'a val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get sg; - - (*fun mk_abs_var x t = (x, fastype_of t);*) + + (*fun mk_abs_var x t = (x, fastype_of t);*) fun sel_name u = NameSpace.base (unsuffix updateN u); fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) = if has_field extfields s mT then upd else seed s r | seed _ r = r; - fun grow u uT k kT vars (sprout,skeleton) = - if sel_name u = moreN + fun grow u uT k kT vars (sprout,skeleton) = + if sel_name u = moreN then let val kv = ("k", kT); val kb = Bound (length vars); in ((Const (u,uT)$k$sprout,Const (u,uT)$kb$skeleton),kv::vars) end else ((sprout,skeleton),vars); fun is_upd_same (sprout,skeleton) u ((sel as Const (s,_))$r) = - if (unsuffix updateN u) = s andalso (seed s sprout) = r + if (unsuffix updateN u) = s andalso (seed s sprout) = r then SOME (sel,seed s skeleton) else NONE | is_upd_same _ _ _ = NONE - + fun init_seed r = ((r,Bound 0), [("r", rT)]); - + (* mk_updterm returns either * - Init (orig-term, orig-term-skeleton, vars) if no optimisation can be made, - * where vars are the bound variables in the skeleton - * - Inter (orig-term-skeleton,simplified-term-skeleton, + * where vars are the bound variables in the skeleton + * - Inter (orig-term-skeleton,simplified-term-skeleton, * vars, (term-sprout, skeleton-sprout)) * where "All vars. orig-term-skeleton = simplified-term-skeleton" is * the desired simplification rule, * the sprouts accumulate the "more-updates" on the way from the seed - * to the outermost update. It is only relevant to calculate the - * possible simplification for (2) + * to the outermost update. It is only relevant to calculate the + * possible simplification for (2) * The algorithm first walks down the updates to the seed-record while * memorising the updates in the already-table. While walking up the * updates again, the optimised term is constructed. *) - fun mk_updterm upds already + fun mk_updterm upds already (t as ((upd as Const (u,uT as (Type (_,[kT,_])))) $ k $ r)) = - if isSome (Symtab.lookup (upds,u)) - then let - fun rest already = mk_updterm upds already - in if u mem_string already - then (case (rest already r) of - Init ((sprout,skel),vars) => + if Symtab.defined upds u + then let + fun rest already = mk_updterm upds already + in if u mem_string already + then (case (rest already r) of + Init ((sprout,skel),vars) => let - val kv = (sel_name u, kT); + val kv = (sel_name u, kT); val kb = Bound (length vars); val (sprout',vars')= grow u uT k kT (kv::vars) (sprout,skel); in Inter (upd$kb$skel,skel,vars',sprout') end - | Inter (trm,trm',vars,sprout) => - let - val kv = (sel_name u, kT); + | Inter (trm,trm',vars,sprout) => + let + val kv = (sel_name u, kT); val kb = Bound (length vars); val (sprout',vars') = grow u uT k kT (kv::vars) sprout; - in Inter(upd$kb$trm,trm',kv::vars',sprout') end) - else - (case rest (u::already) r of - Init ((sprout,skel),vars) => + in Inter(upd$kb$trm,trm',kv::vars',sprout') end) + else + (case rest (u::already) r of + Init ((sprout,skel),vars) => (case is_upd_same (sprout,skel) u k of - SOME (sel,skel') => + SOME (sel,skel') => let - val (sprout',vars') = grow u uT k kT vars (sprout,skel); + val (sprout',vars') = grow u uT k kT vars (sprout,skel); in Inter(upd$(sel$skel')$skel,skel,vars',sprout') end - | NONE => + | NONE => let - val kv = (sel_name u, kT); + val kv = (sel_name u, kT); val kb = Bound (length vars); in Init ((upd$k$sprout,upd$kb$skel),kv::vars) end) - | Inter (trm,trm',vars,sprout) => + | Inter (trm,trm',vars,sprout) => (case is_upd_same sprout u k of SOME (sel,skel) => let @@ -1013,20 +1003,20 @@ in Inter(upd$(sel$skel)$trm,trm',vars',sprout') end | NONE => let - val kv = (sel_name u, kT) + val kv = (sel_name u, kT) val kb = Bound (length vars) val (sprout',vars') = grow u uT k kT (kv::vars) sprout in Inter (upd$kb$trm,upd$kb$trm',vars',sprout') end)) - end - else Init (init_seed t) - | mk_updterm _ _ t = Init (init_seed t); + end + else Init (init_seed t) + | mk_updterm _ _ t = Init (init_seed t); - in (case mk_updterm updates [] t of - Inter (trm,trm',vars,_) - => SOME (prove_split_simp sg ss rT + in (case mk_updterm updates [] t of + Inter (trm,trm',vars,_) + => SOME (prove_split_simp sg ss rT (list_all(vars,(equals rT$trm$trm')))) | _ => NONE) - end + end | _ => NONE)); end @@ -1040,8 +1030,8 @@ * e.g. r(|lots of updates|) = x * * record_eq_simproc record_split_simp_tac - * Complexity: #components * #updates #updates - * + * Complexity: #components * #updates #updates + * *) val record_eq_simproc = Simplifier.simproc (Theory.sign_of HOL.thy) "record_eq_simp" ["r = s"] @@ -1055,7 +1045,7 @@ | _ => NONE)); (* record_split_simproc *) -(* splits quantified occurrences of records, for which P holds. P can peek on the +(* splits quantified occurrences of records, for which P holds. P can peek on the * subterm starting at the quantified occurrence of the record (including the quantifier) * P t = 0: do not split * P t = ~1: completely split @@ -1069,11 +1059,11 @@ then (case rec_id (~1) T of "" => NONE | name - => let val split = P t - in if split <> 0 then + => let val split = P t + in if split <> 0 then (case get_splits sg (rec_id split T) of NONE => NONE - | SOME (all_thm, All_thm, Ex_thm,_) + | SOME (all_thm, All_thm, Ex_thm,_) => SOME (case quantifier of "all" => all_thm | "All" => All_thm RS HOL.eq_reflection @@ -1087,7 +1077,7 @@ val record_ex_sel_eq_simproc = Simplifier.simproc (Theory.sign_of HOL.thy) "record_ex_sel_eq_simproc" ["Ex t"] (fn sg => fn ss => fn t => - let + let fun prove prop = quick_and_dirty_prove true sg [] prop (fn _ => simp_tac (Simplifier.inherit_bounds ss (get_simpset sg) @@ -1095,22 +1085,22 @@ fun mkeq (lr,Teq,(sel,Tsel),x) i = (case get_selectors sg sel of SOME () => - let val x' = if not (loose_bvar1 (x,0)) - then Free ("x" ^ string_of_int i, range_type Tsel) + let val x' = if not (loose_bvar1 (x,0)) + then Free ("x" ^ string_of_int i, range_type Tsel) else raise TERM ("",[x]); val sel' = Const (sel,Tsel)$Bound 0; val (l,r) = if lr then (sel',x') else (x',sel'); in Const ("op =",Teq)$l$r end | NONE => raise TERM ("",[Const (sel,Tsel)])); - fun dest_sel_eq (Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X) = + fun dest_sel_eq (Const ("op =",Teq)$(Const (sel,Tsel)$Bound 0)$X) = (true,Teq,(sel,Tsel),X) | dest_sel_eq (Const ("op =",Teq)$X$(Const (sel,Tsel)$Bound 0)) = (false,Teq,(sel,Tsel),X) | dest_sel_eq _ = raise TERM ("",[]); - in - (case t of + in + (case t of (Const ("Ex",Tex)$Abs(s,T,t)) => (let val eq = mkeq (dest_sel_eq t) 0; val prop = list_all ([("r",T)], @@ -1118,54 +1108,54 @@ HOLogic.true_const)); in SOME (prove prop) end handle TERM _ => NONE) - | _ => NONE) + | _ => NONE) end) - + local val inductive_atomize = thms "induct_atomize"; val inductive_rulify1 = thms "induct_rulify1"; in (* record_split_simp_tac *) -(* splits (and simplifies) all records in the goal for which P holds. +(* splits (and simplifies) all records in the goal for which P holds. * For quantified occurrences of a record * P can peek on the whole subterm (including the quantifier); for free variables P * can only peek on the variable itself. * P t = 0: do not split * P t = ~1: completely split - * P t > 0: split up to given bound of record extensions + * P t > 0: split up to given bound of record extensions *) fun record_split_simp_tac thms P i st = let val sg = Thm.sign_of_thm st; - val {sel_upd={simpset,...},...} + val {sel_upd={simpset,...},...} = RecordsData.get sg; val has_rec = exists_Const (fn (s, Type (_, [Type (_, [T, _]), _])) => - (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T + (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T | _ => false); val goal = List.nth (Thm.prems_of st, i - 1); val frees = List.filter (is_recT o type_of) (term_frees goal); - fun mk_split_free_tac free induct_thm i = - let val cfree = cterm_of sg free; + fun mk_split_free_tac free induct_thm i = + let val cfree = cterm_of sg free; val (_$(_$r)) = concl_of induct_thm; val crec = cterm_of sg r; val thm = cterm_instantiate [(crec,cfree)] induct_thm; in EVERY [simp_tac (HOL_basic_ss addsimps inductive_atomize) i, rtac thm i, simp_tac (HOL_basic_ss addsimps inductive_rulify1) i] - end; + end; - fun split_free_tac P i (free as Free (n,T)) = - (case rec_id (~1) T of + fun split_free_tac P i (free as Free (n,T)) = + (case rec_id (~1) T of "" => NONE - | name => let val split = P free - in if split <> 0 then + | name => let val split = P free + in if split <> 0 then (case get_splits sg (rec_id split T) of NONE => NONE | SOME (_,_,_,induct_thm) @@ -1175,10 +1165,10 @@ | split_free_tac _ _ _ = NONE; val split_frees_tacs = List.mapPartial (split_free_tac P i) frees; - + val simprocs = if has_rec goal then [record_split_simproc P] else []; - - in st |> ((EVERY split_frees_tacs) + + in st |> ((EVERY split_frees_tacs) THEN (Simplifier.full_simp_tac (simpset addsimps thms addsimprocs simprocs) i)) end handle Empty => Seq.empty; end; @@ -1192,19 +1182,19 @@ val has_rec = exists_Const (fn (s, Type (_, [Type (_, [T, _]), _])) => - (s = "all" orelse s = "All") andalso is_recT T + (s = "all" orelse s = "All") andalso is_recT T | _ => false); - - val goal = List.nth (Thm.prems_of st, i - 1); + + val goal = List.nth (Thm.prems_of st, i - 1); fun is_all t = (case t of (Const (quantifier, _)$_) => if quantifier = "All" orelse quantifier = "all" then ~1 else 0 | _ => 0); - - in if has_rec goal - then Simplifier.full_simp_tac - (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i st + + in if has_rec goal + then Simplifier.full_simp_tac + (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i st else Seq.empty end handle Subscript => Seq.empty; @@ -1245,10 +1235,10 @@ fun simp_all_tac ss simps = ALLGOALS (Simplifier.asm_full_simp_tac (ss addsimps simps)); -(* do case analysis / induction according to rule on last parameter of ith subgoal - * (or on s if there are no parameters); +(* do case analysis / induction according to rule on last parameter of ith subgoal + * (or on s if there are no parameters); * Instatiation of record variable (and predicate) in rule is calculated to - * avoid problems with higher order unification. + * avoid problems with higher order unification. *) fun try_param_tac s rule i st = @@ -1287,10 +1277,10 @@ val (_$(_$x)) = Logic.strip_assums_concl (hd (prems_of exI')); val cx = cterm_of sg (fst (strip_comb x)); - in Seq.single (Library.foldl (fn (st,v) => - Seq.hd - (compose_tac (false, cterm_instantiate - [(cx,cterm_of sg (list_abs (params,Bound v)))] exI',1) + in Seq.single (Library.foldl (fn (st,v) => + Seq.hd + (compose_tac (false, cterm_instantiate + [(cx,cterm_of sg (list_abs (params,Bound v)))] exI',1) i st)) (st,((length params) - 1) downto 0)) end; @@ -1298,7 +1288,7 @@ let val UNIV = HOLogic.mk_UNIV repT; - val (thy',{set_def=SOME def, Abs_induct = abs_induct, + val (thy',{set_def=SOME def, Abs_induct = abs_induct, Abs_inject=abs_inject, Abs_inverse = abs_inverse,...}) = thy |> setmp TypedefPackage.quiet_mode true (TypedefPackage.add_typedef_i true NONE @@ -1308,12 +1298,12 @@ in (thy',map rewrite_rule [abs_inject, abs_inverse, abs_induct]) end; -fun mixit convs refls = +fun mixit convs refls = let fun f ((res,lhs,rhs),refl) = ((refl,List.revAppend (lhs,refl::tl rhs))::res,hd rhs::lhs,tl rhs); in #1 (Library.foldl f (([],[],convs),refls)) end; -fun extension_definition full name fields names alphas zeta moreT more vars thy = - let +fun extension_definition full name fields names alphas zeta moreT more vars thy = + let val base = Sign.base_name; val fieldTs = (map snd fields); val alphas_zeta = alphas@[zeta]; @@ -1330,20 +1320,20 @@ val idxms = 0 upto len; (* prepare declarations and definitions *) - + (*fields constructor*) val ext_decl = (mk_extC (name,extT) fields_moreTs); - (* - val ext_spec = Const ext_decl :== - (foldr (uncurry lambda) - (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))) (vars@[more])) - *) - val ext_spec = list_comb (Const ext_decl,vars@[more]) :== + (* + val ext_spec = Const ext_decl :== + (foldr (uncurry lambda) + (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))) (vars@[more])) + *) + val ext_spec = list_comb (Const ext_decl,vars@[more]) :== (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))); - - fun mk_ext args = list_comb (Const ext_decl, args); - (*destructors*) + fun mk_ext args = list_comb (Const ext_decl, args); + + (*destructors*) val _ = timing_msg "record extension preparing definitions"; val dest_decls = map (mk_selC extT o (apfst (suffix ext_dest))) bfields_more; @@ -1354,31 +1344,31 @@ end; val dest_specs = ListPair.map mk_dest_spec (idxms, fields_more); - + (*updates*) val upd_decls = map (mk_updC updN extT) bfields_more; fun mk_upd_spec (c,T) = let - val args = map (fn (n,nT) => if n=c then Free (base c,T) - else (mk_sel r (suffix ext_dest n,nT))) + val args = map (fn (n,nT) => if n=c then Free (base c,T) + else (mk_sel r (suffix ext_dest n,nT))) fields_more; in Const (mk_updC updN extT (c,T))$(Free (base c,T))$r :== mk_ext args end; val upd_specs = map mk_upd_spec fields_more; - + (* 1st stage: defs_thy *) fun mk_defs () = - thy + thy |> extension_typedef name repT (alphas@[zeta]) - |>> Theory.add_consts_i + |>> Theory.add_consts_i (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls)) |>>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs)) |>>> PureThy.add_defs_i false (map Thm.no_attributes upd_specs) val (defs_thy, (([abs_inject, abs_inverse, abs_induct],ext_def::dest_defs),upd_defs)) = timeit_msg "record extension type/selector/update defs:" mk_defs; - - + + (* prepare propositions *) val _ = timing_msg "record extension preparing propositions"; val vars_more = vars@[more]; @@ -1389,70 +1379,70 @@ val w = Free (wN, extT); val P = Free (variant variants "P", extT-->HOLogic.boolT); val C = Free (variant variants "C", HOLogic.boolT); - + val inject_prop = let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more; - in All (map dest_Free (vars_more@vars_more')) - ((HOLogic.eq_const extT $ - mk_ext vars_more$mk_ext vars_more') + in All (map dest_Free (vars_more@vars_more')) + ((HOLogic.eq_const extT $ + mk_ext vars_more$mk_ext vars_more') === foldr1 HOLogic.mk_conj (map HOLogic.mk_eq (vars_more ~~ vars_more'))) end; - + val induct_prop = (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s)); val cases_prop = - (All (map dest_Free vars_more) - (Trueprop (HOLogic.mk_eq (s,ext)) ==> Trueprop C)) + (All (map dest_Free vars_more) + (Trueprop (HOLogic.mk_eq (s,ext)) ==> Trueprop C)) ==> Trueprop C; - (*destructors*) + (*destructors*) val dest_conv_props = map (fn (c, x as Free (_,T)) => mk_sel ext (suffix ext_dest c,T) === x) named_vars_more; (*updates*) fun mk_upd_prop (i,(c,T)) = - let val x' = Free (variant variants (base c ^ "'"),T) + let val x' = Free (variant variants (base c ^ "'"),T) val args' = nth_update x' (i, vars_more) in mk_upd updN c x' ext === mk_ext args' end; val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more); val surjective_prop = - let val args = + let val args = map (fn (c, Free (_,T)) => mk_sel s (suffix ext_dest c,T)) named_vars_more; in s === mk_ext args end; val split_meta_prop = let val P = Free (variant variants "P", extT-->Term.propT) in - Logic.mk_equals + Logic.mk_equals (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext)) - end; + end; fun prove stndrd = quick_and_dirty_prove stndrd (Theory.sign_of defs_thy); val prove_standard = quick_and_dirty_prove true (Theory.sign_of defs_thy); fun prove_simp stndrd simps = let val tac = simp_all_tac HOL_ss simps in fn prop => prove stndrd [] prop (K tac) end; - + fun inject_prf () = (prove_simp true [ext_def,abs_inject,Pair_eq] inject_prop); val inject = timeit_msg "record extension inject proof:" inject_prf; fun induct_prf () = let val (assm, concl) = induct_prop in prove_standard [assm] concl (fn prems => - EVERY [try_param_tac rN abs_induct 1, + EVERY [try_param_tac rN abs_induct 1, simp_tac (HOL_ss addsimps [split_paired_all]) 1, resolve_tac (map (rewrite_rule [ext_def]) prems) 1]) end; val induct = timeit_msg "record extension induct proof:" induct_prf; fun cases_prf_opt () = - let + let val sg = (sign_of defs_thy); val (_$(Pvar$_)) = concl_of induct; - val ind = cterm_instantiate - [(cterm_of sg Pvar, cterm_of sg + val ind = cterm_instantiate + [(cterm_of sg Pvar, cterm_of sg (lambda w (HOLogic.imp$HOLogic.mk_eq(r,w)$C)))] induct; in standard (ObjectLogic.rulify (mp OF [ind, refl])) end; @@ -1468,26 +1458,26 @@ val cases_prf = quick_and_dirty_prf cases_prf_noopt cases_prf_opt; val cases = timeit_msg "record extension cases proof:" cases_prf; - - fun dest_convs_prf () = map (prove_simp false + + fun dest_convs_prf () = map (prove_simp false ([ext_def,abs_inverse]@Pair_sel_convs@dest_defs)) dest_conv_props; val dest_convs = timeit_msg "record extension dest_convs proof:" dest_convs_prf; fun dest_convs_standard_prf () = map standard dest_convs; - - val dest_convs_standard = - timeit_msg "record extension dest_convs_standard proof:" dest_convs_standard_prf; - fun upd_convs_prf_noopt () = map (prove_simp true (dest_convs_standard@upd_defs)) + val dest_convs_standard = + timeit_msg "record extension dest_convs_standard proof:" dest_convs_standard_prf; + + fun upd_convs_prf_noopt () = map (prove_simp true (dest_convs_standard@upd_defs)) upd_conv_props; fun upd_convs_prf_opt () = - let + let val sg = sign_of defs_thy; - fun mkrefl (c,T) = Thm.reflexive - (cterm_of sg (Free (variant variants (base c ^ "'"),T))); + fun mkrefl (c,T) = Thm.reflexive + (cterm_of sg (Free (variant variants (base c ^ "'"),T))); val refls = map mkrefl fields_more; val constr_refl = Thm.reflexive (cterm_of sg (head_of ext)); val dest_convs' = map mk_meta_eq dest_convs; - + fun mkthm (udef,(fld_refl,thms)) = let val bdyeq = Library.foldl (uncurry Thm.combination) (constr_refl,thms); (* (|N=N (|N=N,M=M,K=K,more=more|) @@ -1498,19 +1488,19 @@ *) val (_$(_$v$r)$_) = prop_of udef; val (_$v'$_) = prop_of fld_refl; - val udef' = cterm_instantiate + val udef' = cterm_instantiate [(cterm_of sg v,cterm_of sg v'), (cterm_of sg r,cterm_of sg ext)] udef; - in standard (Thm.transitive udef' bdyeq) end; - in map mkthm (rev upd_defs ~~ (mixit dest_convs' refls)) + in standard (Thm.transitive udef' bdyeq) end; + in map mkthm (rev upd_defs ~~ (mixit dest_convs' refls)) handle e => print_exn e end; - + val upd_convs_prf = quick_and_dirty_prf upd_convs_prf_noopt upd_convs_prf_opt; - val upd_convs = - timeit_msg "record extension upd_convs proof:" upd_convs_prf; + val upd_convs = + timeit_msg "record extension upd_convs proof:" upd_convs_prf; - fun surjective_prf () = + fun surjective_prf () = prove_standard [] surjective_prop (fn prems => (EVERY [try_param_tac rN induct 1, simp_tac (HOL_basic_ss addsimps dest_convs_standard) 1])); @@ -1527,42 +1517,42 @@ val (thm_thy,([inject',induct',cases',surjective',split_meta'], [dest_convs',upd_convs'])) = - defs_thy - |> (PureThy.add_thms o map Thm.no_attributes) + defs_thy + |> (PureThy.add_thms o map Thm.no_attributes) [("ext_inject", inject), ("ext_induct", induct), ("ext_cases", cases), ("ext_surjective", surjective), ("ext_split", split_meta)] |>>> (PureThy.add_thmss o map Thm.no_attributes) - [("dest_convs",dest_convs_standard),("upd_convs",upd_convs)] + [("dest_convs",dest_convs_standard),("upd_convs",upd_convs)] in (thm_thy,extT,induct',inject',dest_convs',split_meta',upd_convs') end; - + fun chunks [] [] = [] | chunks [] xs = [xs] | chunks (l::ls) xs = Library.take (l,xs)::chunks ls (Library.drop (l,xs)); - + fun chop_last [] = error "last: list should not be empty" | chop_last [x] = ([],x) | chop_last (x::xs) = let val (tl,l) = chop_last xs in (x::tl,l) end; - + fun subst_last s [] = error "subst_last: list should not be empty" | subst_last s ([x]) = [s] | subst_last s (x::xs) = (x::subst_last s xs); (* mk_recordT builds up the record type from the current extension tpye extT and a list - * of parent extensions, starting with the root of the record hierarchy -*) -fun mk_recordT extT parent_exts = + * of parent extensions, starting with the root of the record hierarchy +*) +fun mk_recordT extT parent_exts = foldr (fn ((parent,Ts),T) => Type (parent, subst_last T Ts)) extT parent_exts; fun obj_to_meta_all thm = let - fun E thm = case (SOME (spec OF [thm]) handle THM _ => NONE) of + fun E thm = case (SOME (spec OF [thm]) handle THM _ => NONE) of SOME thm' => E thm' | NONE => thm; val th1 = E thm; @@ -1584,7 +1574,7 @@ (* record_definition *) -fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy = +fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy = (* smlnj needs type annotation of parents *) let val sign = Theory.sign_of thy; @@ -1611,7 +1601,7 @@ val extN = full bname; val types = map snd fields; val alphas_fields = foldr add_typ_tfree_names [] types; - val alphas_ext = alphas inter alphas_fields; + val alphas_ext = alphas inter alphas_fields; val len = length fields; val variants = variantlist (map fst bfields, moreN::rN::rN ^ "'"::wN::parent_variants); val vars = ListPair.map Free (variants, types); @@ -1628,7 +1618,7 @@ val all_named_vars = (parent_names ~~ parent_vars) @ named_vars; - val zeta = variant alphas "'z"; + val zeta = variant alphas "'z"; val moreT = TFree (zeta, HOLogic.typeS); val more = Free (moreN, moreT); val full_moreN = full moreN; @@ -1638,42 +1628,42 @@ val named_vars_more = named_vars @[(full_moreN,more)]; val all_vars_more = all_vars @ [more]; val all_named_vars_more = all_named_vars @ [(full_moreN,more)]; - + (* 1st stage: extension_thy *) val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs,ext_split,u_convs) = thy |> Theory.add_path bname |> extension_definition full extN fields names alphas_ext zeta moreT more vars; - val _ = timing_msg "record preparing definitions"; + val _ = timing_msg "record preparing definitions"; val Type extension_scheme = extT; val extension_name = unsuffix ext_typeN (fst extension_scheme); - val extension = let val (n,Ts) = extension_scheme in (n,subst_last HOLogic.unitT Ts) end; - val extension_names = + val extension = let val (n,Ts) = extension_scheme in (n,subst_last HOLogic.unitT Ts) end; + val extension_names = (map ((unsuffix ext_typeN) o fst o #extension) parents) @ [extN]; val extension_id = Library.foldl (op ^) ("",extension_names); - + fun rec_schemeT n = mk_recordT extT (map #extension (prune n parents)); val rec_schemeT0 = rec_schemeT 0; - fun recT n = + fun recT n = let val (c,Ts) = extension in mk_recordT (Type (c,subst_last HOLogic.unitT Ts))(map #extension (prune n parents)) end; val recT0 = recT 0; - + fun mk_rec args n = let val (args',more) = chop_last args; - fun mk_ext' (((name,T),args),more) = mk_ext (name,T) (args@[more]); - fun build Ts = + fun mk_ext' (((name,T),args),more) = mk_ext (name,T) (args@[more]); + fun build Ts = foldr mk_ext' more (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args'))) - in - if more = HOLogic.unit - then build (map recT (0 upto parent_len)) + in + if more = HOLogic.unit + then build (map recT (0 upto parent_len)) else build (map rec_schemeT (0 upto parent_len)) end; - + val r_rec0 = mk_rec all_vars_more 0; val r_rec_unit0 = mk_rec (all_vars@[HOLogic.unit]) 0; @@ -1704,66 +1694,66 @@ in map (gen_record_type_tr') trnames end; - + (* prepare declarations *) val sel_decls = map (mk_selC rec_schemeT0) bfields_more; val upd_decls = map (mk_updC updateN rec_schemeT0) bfields_more; val make_decl = (makeN, all_types ---> recT0); - val fields_decl = (fields_selN, types ---> Type extension); + val fields_decl = (fields_selN, types ---> Type extension); val extend_decl = (extendN, recT0 --> moreT --> rec_schemeT0); val truncate_decl = (truncateN, rec_schemeT0 --> recT0); (* prepare definitions *) - - fun parent_more s = - if null parents then s + + fun parent_more s = + if null parents then s else mk_sel s (NameSpace.qualified (#name (List.last parents)) moreN, extT); fun parent_more_upd v s = - if null parents then v + if null parents then v else let val mp = NameSpace.qualified (#name (List.last parents)) moreN; in mk_upd updateN mp v s end; - + (*record (scheme) type abbreviation*) val recordT_specs = [(suffix schemeN bname, alphas @ [zeta], rec_schemeT0, Syntax.NoSyn), - (bname, alphas, recT0, Syntax.NoSyn)]; + (bname, alphas, recT0, Syntax.NoSyn)]; - (*selectors*) - fun mk_sel_spec (c,T) = - Const (mk_selC rec_schemeT0 (c,T)) + (*selectors*) + fun mk_sel_spec (c,T) = + Const (mk_selC rec_schemeT0 (c,T)) :== (lambda r0 (Const (mk_selC extT (suffix ext_dest c,T))$parent_more r0)); val sel_specs = map mk_sel_spec fields_more; (*updates*) fun mk_upd_spec (c,T) = - let - val new = mk_upd updN c (Free (base c,T)) (parent_more r0); + let + val new = mk_upd updN c (Free (base c,T)) (parent_more r0); in Const (mk_updC updateN rec_schemeT0 (c,T))$(Free (base c,T))$r0 :== (parent_more_upd new r0) end; - val upd_specs = map mk_upd_spec fields_more; + val upd_specs = map mk_upd_spec fields_more; (*derived operations*) val make_spec = Const (full makeN, all_types ---> recT0) $$ all_vars :== mk_rec (all_vars @ [HOLogic.unit]) 0; val fields_spec = Const (full fields_selN, types ---> Type extension) $$ vars :== mk_rec (all_vars @ [HOLogic.unit]) parent_len; - val extend_spec = + val extend_spec = Const (full extendN, recT0-->moreT-->rec_schemeT0) $ r_unit0 $ more :== mk_rec ((map (mk_sel r_unit0) all_fields) @ [more]) 0; val truncate_spec = Const (full truncateN, rec_schemeT0 --> recT0) $ r0 :== mk_rec ((map (mk_sel r0) all_fields) @ [HOLogic.unit]) 0; (* 2st stage: defs_thy *) - + fun mk_defs () = extension_thy - |> Theory.add_trfuns + |> Theory.add_trfuns ([],[],field_tr's, []) - |> Theory.add_advanced_trfuns + |> Theory.add_advanced_trfuns ([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[]) |> Theory.parent_path @@ -1771,30 +1761,30 @@ |> Theory.add_path bname |> Theory.add_consts_i (map2 (fn ((x, T), mx) => (x, T, mx)) (sel_decls, field_syntax @ [Syntax.NoSyn])) - |> (Theory.add_consts_i o map Syntax.no_syn) + |> (Theory.add_consts_i o map Syntax.no_syn) (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl]) |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs |>>> (PureThy.add_defs_i false o map Thm.no_attributes) upd_specs - |>>> (PureThy.add_defs_i false o map Thm.no_attributes) + |>>> (PureThy.add_defs_i false o map Thm.no_attributes) [make_spec, fields_spec, extend_spec, truncate_spec] val (defs_thy,((sel_defs,upd_defs),derived_defs)) = timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:" mk_defs; - + (* prepare propositions *) - val _ = timing_msg "record preparing propositions"; + val _ = timing_msg "record preparing propositions"; val P = Free (variant all_variants "P", rec_schemeT0-->HOLogic.boolT); - val C = Free (variant all_variants "C", HOLogic.boolT); + val C = Free (variant all_variants "C", HOLogic.boolT); val P_unit = Free (variant all_variants "P", recT0-->HOLogic.boolT); - (*selectors*) + (*selectors*) val sel_conv_props = map (fn (c, x as Free (_,T)) => mk_sel r_rec0 (c,T) === x) named_vars_more; - (*updates*) + (*updates*) fun mk_upd_prop (i,(c,T)) = - let val x' = Free (variant all_variants (base c ^ "'"),T) + let val x' = Free (variant all_variants (base c ^ "'"),T) val args' = nth_update x' (parent_fields_len + i, all_vars_more) in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end; val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more); @@ -1802,7 +1792,7 @@ (*induct*) val induct_scheme_prop = All (map dest_Free all_vars_more) (Trueprop (P $ r_rec0)) ==> Trueprop (P $ r0); - val induct_prop = + val induct_prop = (All (map dest_Free all_vars) (Trueprop (P_unit $ r_rec_unit0)), Trueprop (P_unit $ r_unit0)); @@ -1810,24 +1800,24 @@ val surjective_prop = let val args = map (fn (c,Free (_,T)) => mk_sel r0 (c,T)) all_named_vars_more in r0 === mk_rec args 0 end; - + (*cases*) val cases_scheme_prop = - (All (map dest_Free all_vars_more) - (Trueprop (HOLogic.mk_eq (r0,r_rec0)) ==> Trueprop C)) + (All (map dest_Free all_vars_more) + (Trueprop (HOLogic.mk_eq (r0,r_rec0)) ==> Trueprop C)) ==> Trueprop C; val cases_prop = - (All (map dest_Free all_vars) - (Trueprop (HOLogic.mk_eq (r_unit0,r_rec_unit0)) ==> Trueprop C)) + (All (map dest_Free all_vars) + (Trueprop (HOLogic.mk_eq (r_unit0,r_rec_unit0)) ==> Trueprop C)) ==> Trueprop C; (*split*) val split_meta_prop = let val P = Free (variant all_variants "P", rec_schemeT0-->Term.propT) in - Logic.mk_equals + Logic.mk_equals (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0)) - end; + end; val split_object_prop = let fun ALL vs t = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) t vs @@ -1842,9 +1832,9 @@ (*equality*) val equality_prop = - let - val s' = Free (rN ^ "'", rec_schemeT0) - fun mk_sel_eq (c,Free (_,T)) = mk_sel r0 (c,T) === mk_sel s' (c,T) + let + val s' = Free (rN ^ "'", rec_schemeT0) + fun mk_sel_eq (c,Free (_,T)) = mk_sel r0 (c,T) === mk_sel s' (c,T) val seleqs = map mk_sel_eq all_named_vars_more in All (map dest_Free [r0,s']) (Logic.list_implies (seleqs,r0 === s')) end; @@ -1852,29 +1842,29 @@ fun prove stndrd = quick_and_dirty_prove stndrd (Theory.sign_of defs_thy); val prove_standard = quick_and_dirty_prove true (Theory.sign_of defs_thy); - + fun prove_simp stndrd ss simps = let val tac = simp_all_tac ss simps in fn prop => prove stndrd [] prop (K tac) end; val ss = get_simpset (sign_of defs_thy); - fun sel_convs_prf () = map (prove_simp false ss + fun sel_convs_prf () = map (prove_simp false ss (sel_defs@ext_dest_convs)) sel_conv_props; val sel_convs = timeit_msg "record sel_convs proof:" sel_convs_prf; fun sel_convs_standard_prf () = map standard sel_convs - val sel_convs_standard = - timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf; + val sel_convs_standard = + timeit_msg "record sel_convs_standard proof:" sel_convs_standard_prf; - fun upd_convs_prf () = - map (prove_simp true ss (upd_defs@u_convs)) upd_conv_props; - + fun upd_convs_prf () = + map (prove_simp true ss (upd_defs@u_convs)) upd_conv_props; + val upd_convs = timeit_msg "record upd_convs proof:" upd_convs_prf; val parent_induct = if null parents then [] else [#induct (hd (rev parents))]; fun induct_scheme_prf () = prove_standard [] induct_scheme_prop (fn prems => - (EVERY [if null parent_induct + (EVERY [if null parent_induct then all_tac else try_param_tac rN (hd parent_induct) 1, try_param_tac rN ext_induct 1, asm_simp_tac HOL_basic_ss 1])); @@ -1890,18 +1880,18 @@ end; val induct = timeit_msg "record induct proof:" induct_prf; - fun surjective_prf () = + fun surjective_prf () = prove_standard [] surjective_prop (fn prems => (EVERY [try_param_tac rN induct_scheme 1, simp_tac (ss addsimps sel_convs_standard) 1])) val surjective = timeit_msg "record surjective proof:" surjective_prf; fun cases_scheme_prf_opt () = - let + let val sg = (sign_of defs_thy); val (_$(Pvar$_)) = concl_of induct_scheme; - val ind = cterm_instantiate - [(cterm_of sg Pvar, cterm_of sg + val ind = cterm_instantiate + [(cterm_of sg Pvar, cterm_of sg (lambda w (HOLogic.imp$HOLogic.mk_eq(r0,w)$C)))] induct_scheme; in standard (ObjectLogic.rulify (mp OF [ind, refl])) end; @@ -1934,38 +1924,38 @@ val split_meta_standard = standard split_meta; fun split_object_prf_opt () = - let + let val sg = sign_of defs_thy; val cPI= cterm_of sg (lambda r0 (Trueprop (P$r0))); val (_$Abs(_,_,P$_)) = fst (Logic.dest_equals (concl_of split_meta_standard)); val cP = cterm_of sg P; val split_meta' = cterm_instantiate [(cP,cPI)] split_meta_standard; val (l,r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop); - val cl = cterm_of sg (HOLogic.mk_Trueprop l); - val cr = cterm_of sg (HOLogic.mk_Trueprop r); + val cl = cterm_of sg (HOLogic.mk_Trueprop l); + val cr = cterm_of sg (HOLogic.mk_Trueprop r); val thl = assume cl (*All r. P r*) (* 1 *) |> obj_to_meta_all (*!!r. P r*) - |> equal_elim split_meta' (*!!n m more. P (ext n m more)*) - |> meta_to_obj_all (*All n m more. P (ext n m more)*) (* 2*) + |> equal_elim split_meta' (*!!n m more. P (ext n m more)*) + |> meta_to_obj_all (*All n m more. P (ext n m more)*) (* 2*) |> implies_intr cl (* 1 ==> 2 *) val thr = assume cr (*All n m more. P (ext n m more)*) |> obj_to_meta_all (*!!n m more. P (ext n m more)*) - |> equal_elim (symmetric split_meta') (*!!r. P r*) + |> equal_elim (symmetric split_meta') (*!!r. P r*) |> meta_to_obj_all (*All r. P r*) |> implies_intr cr (* 2 ==> 1 *) - in standard (thr COMP (thl COMP iffI)) end; + in standard (thr COMP (thl COMP iffI)) end; fun split_object_prf_noopt () = prove_standard [] split_object_prop (fn prems => - EVERY [rtac iffI 1, + EVERY [rtac iffI 1, REPEAT (rtac allI 1), etac allE 1, atac 1, rtac allI 1, rtac induct_scheme 1,REPEAT (etac allE 1),atac 1]); - val split_object_prf = quick_and_dirty_prf split_object_prf_noopt split_object_prf_opt; + val split_object_prf = quick_and_dirty_prf split_object_prf_noopt split_object_prf_opt; val split_object = timeit_msg "record split_object proof:" split_object_prf; - fun split_ex_prf () = + fun split_ex_prf () = prove_standard [] split_ex_prop (fn prems => EVERY [rtac iffI 1, etac exE 1, @@ -1978,19 +1968,19 @@ atac 1]); val split_ex = timeit_msg "record split_ex proof:" split_ex_prf; - fun equality_tac thms = + fun equality_tac thms = let val (s'::s::eqs) = rev thms; val ss' = ss addsimps (s'::s::sel_convs_standard); val eqs' = map (simplify ss') eqs; in simp_tac (HOL_basic_ss addsimps (s'::s::eqs')) 1 end; - + fun equality_prf () = prove_standard [] equality_prop (fn _ => fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in st |> (res_inst_tac [(rN, s)] cases_scheme 1 THEN res_inst_tac [(rN, s')] cases_scheme 1 - THEN (METAHYPS equality_tac 1)) + THEN (METAHYPS equality_tac 1)) (* simp_all_tac ss (sel_convs) would also work but is less efficient *) - end); + end); val equality = timeit_msg "record equality proof:" equality_prf; val (thms_thy,(([sel_convs',upd_convs',sel_defs',upd_defs',[split_meta',split_object',split_ex'], @@ -2007,7 +1997,7 @@ |>>> (PureThy.add_thms o map Thm.no_attributes) [("surjective", surjective), ("equality", equality)] - |>>> PureThy.add_thms + |>>> PureThy.add_thms [(("induct_scheme", induct_scheme), induct_type_global (suffix schemeN name)), (("induct", induct), induct_type_global name), (("cases_scheme", cases_scheme), cases_type_global (suffix schemeN name)), @@ -2021,14 +2011,14 @@ |> (#1 oo PureThy.add_thmss) [(("simps", sel_upd_simps), [Simplifier.simp_add_global]), (("iffs",iffs), [iff_add_global])] - |> put_record name (make_record_info args parent fields extension induct_scheme') + |> put_record name (make_record_info args parent fields extension induct_scheme') |> put_sel_upd (names @ [full_moreN]) sel_upd_simps |> add_record_equalities extension_id equality' |> add_extinjects ext_inject |> add_extsplit extension_name ext_split |> add_record_splits extension_id (split_meta',split_object',split_ex',induct_scheme') - |> add_extfields extension_name (fields @ [(full_moreN,moreT)]) - |> add_fieldext (extension_name,snd extension) (names @ [full_moreN]) + |> add_extfields extension_name (fields @ [(full_moreN,moreT)]) + |> add_fieldext (extension_name,snd extension) (names @ [full_moreN]) |> Theory.parent_path; in final_thy @@ -2040,7 +2030,7 @@ work to record_definition*) fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy = let - val _ = Theory.requires thy "Record" "record definitions"; + val _ = Theory.requires thy "Record" "record definitions"; val sign = Theory.sign_of thy; val _ = message ("Defining record " ^ quote bname ^ " ..."); @@ -2079,7 +2069,7 @@ (* errors *) val name = Sign.full_name sign bname; - val err_dup_record = + val err_dup_record = if is_none (get_record thy name) then [] else ["Duplicate definition of record " ^ quote name]; @@ -2126,7 +2116,7 @@ val setup = [RecordsData.init, Theory.add_trfuns ([], parse_translation, [], []), - Theory.add_advanced_trfuns ([], adv_parse_translation, [], []), + Theory.add_advanced_trfuns ([], adv_parse_translation, [], []), Simplifier.change_simpset_of Simplifier.addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]]; @@ -2139,8 +2129,8 @@ (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const); val recordP = - OuterSyntax.command "record" "define extensible record" K.thy_decl - (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z))); + OuterSyntax.command "record" "define extensible record" K.thy_decl + (record_decl >> (fn (x, (y, z)) => Toplevel.theory (add_record x y z))); val _ = OuterSyntax.add_parsers [recordP]; @@ -2150,4 +2140,4 @@ structure BasicRecordPackage: BASIC_RECORD_PACKAGE = RecordPackage; -open BasicRecordPackage; +open BasicRecordPackage; diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/refute.ML Mon Sep 05 17:38:18 2005 +0200 @@ -298,11 +298,11 @@ let val {interpreters, printers, parameters} = RefuteData.get thy in - case Symtab.lookup (parameters, name) of + case Symtab.curried_lookup parameters name of NONE => RefuteData.put {interpreters = interpreters, printers = printers, parameters = Symtab.extend (parameters, [(name, value)])} thy | SOME _ => RefuteData.put - {interpreters = interpreters, printers = printers, parameters = Symtab.update ((name, value), parameters)} thy + {interpreters = interpreters, printers = printers, parameters = Symtab.curried_update (name, value) parameters} thy end; (* ------------------------------------------------------------------------- *) @@ -312,7 +312,7 @@ (* theory -> string -> string option *) - fun get_default_param thy name = Symtab.lookup ((#parameters o RefuteData.get) thy, name); + val get_default_param = Symtab.curried_lookup o #parameters o RefuteData.get; (* ------------------------------------------------------------------------- *) (* get_default_params: returns a list of all '(name, value)' pairs that are *) @@ -321,7 +321,7 @@ (* theory -> (string * string) list *) - fun get_default_params thy = (Symtab.dest o #parameters o RefuteData.get) thy; + val get_default_params = Symtab.dest o #parameters o RefuteData.get; (* ------------------------------------------------------------------------- *) (* actual_params: takes a (possibly empty) list 'params' of parameters that *) diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/res_axioms.ML Mon Sep 05 17:38:18 2005 +0200 @@ -257,7 +257,7 @@ (*Populate the clause cache using the supplied theorems*) fun skolemlist [] thy = thy | skolemlist ((name,th)::nths) thy = - (case Symtab.lookup (!clause_cache,name) of + (case Symtab.curried_lookup (!clause_cache) name of NONE => let val (nnfth,ok) = (to_nnf thy th, true) handle THM _ => (asm_rl, false) @@ -265,8 +265,7 @@ if ok then let val (skoths,thy') = skolem thy (name, nnfth) val cls = Meson.make_cnf skoths nnfth - in clause_cache := - Symtab.update ((name, (th,cls)), !clause_cache); + in change clause_cache (Symtab.curried_update (name, (th, cls))); skolemlist nths thy' end else skolemlist nths thy @@ -277,17 +276,15 @@ fun cnf_axiom (name,th) = case name of "" => cnf_axiom_aux th (*no name, so can't cache*) - | s => case Symtab.lookup (!clause_cache,s) of + | s => case Symtab.curried_lookup (!clause_cache) s of NONE => let val cls = cnf_axiom_aux th - in clause_cache := Symtab.update ((s, (th,cls)), !clause_cache); cls - end + in change clause_cache (Symtab.curried_update (s, (th, cls))); cls end | SOME(th',cls) => if eq_thm(th,th') then cls else (*New theorem stored under the same name? Possible??*) let val cls = cnf_axiom_aux th - in clause_cache := Symtab.update ((s, (th,cls)), !clause_cache); cls - end; + in change clause_cache (Symtab.curried_update (s, (th, cls))); cls end; fun pairname th = (Thm.name_of_thm th, th); diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/res_clause.ML Mon Sep 05 17:38:18 2005 +0200 @@ -136,16 +136,16 @@ fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); fun make_fixed_const c = - case Symtab.lookup (const_trans_table,c) of + case Symtab.curried_lookup const_trans_table c of SOME c' => c' - | NONE => const_prefix ^ (ascii_of c); + | NONE => const_prefix ^ ascii_of c; fun make_fixed_type_const c = - case Symtab.lookup (type_const_trans_table,c) of + case Symtab.curried_lookup type_const_trans_table c of SOME c' => c' - | NONE => tconst_prefix ^ (ascii_of c); + | NONE => tconst_prefix ^ ascii_of c; -fun make_type_class clas = class_prefix ^ (ascii_of clas); +fun make_type_class clas = class_prefix ^ ascii_of clas; diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/HOL/Tools/typedef_package.ML Mon Sep 05 17:38:18 2005 +0200 @@ -62,9 +62,8 @@ end); fun put_typedef newT oldT Abs_name Rep_name thy = - TypedefData.put (Symtab.update_new - ((fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)), - TypedefData.get thy)) thy; + TypedefData.put (Symtab.curried_update_new + (fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)) (TypedefData.get thy)) thy; @@ -283,8 +282,10 @@ foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts); val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'') in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end; - fun lookup f T = getOpt (Option.map f (Symtab.lookup - (TypedefData.get thy, get_name T)), "") + fun lookup f T = + (case Symtab.curried_lookup (TypedefData.get thy) (get_name T) of + NONE => "" + | SOME s => f s); in (case strip_comb t of (Const (s, Type ("fun", [T, U])), ts) => @@ -303,7 +304,7 @@ | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps; fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) = - (case Symtab.lookup (TypedefData.get thy, s) of + (case Symtab.curried_lookup (TypedefData.get thy) s of NONE => NONE | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) => if isSome (Codegen.get_assoc_type thy tname) then NONE else diff -r df7c3b1f390a -r 193b84a70ca4 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/Pure/codegen.ML Mon Sep 05 17:38:18 2005 +0200 @@ -427,12 +427,13 @@ let val s' = NameSpace.pack ys val s'' = NameSpace.append module s' - in case Symtab.lookup (used, s'') of - NONE => ((module, s'), (Symtab.update_new ((s, (module, s')), tab), - Symtab.update_new ((s'', ()), used))) + in case Symtab.curried_lookup used s'' of + NONE => ((module, s'), + (Symtab.curried_update_new (s, (module, s')) tab, + Symtab.curried_update_new (s'', ()) used)) | SOME _ => find_name yss end - in case Symtab.lookup (tab, s) of + in case Symtab.curried_lookup tab s of NONE => find_name (Library.suffixes1 (NameSpace.unpack s)) | SOME name => (name, p) end; @@ -452,7 +453,7 @@ in ((gr, (tab1', tab2)), (module, s'')) end; fun get_const_id cname (gr, (tab1, tab2)) = - case Symtab.lookup (fst tab1, cname) of + case Symtab.curried_lookup (fst tab1) cname of NONE => error ("get_const_id: no such constant: " ^ quote cname) | SOME (module, s) => let @@ -468,7 +469,7 @@ in ((gr, (tab1, tab2')), (module, s'')) end; fun get_type_id tyname (gr, (tab1, tab2)) = - case Symtab.lookup (fst tab2, tyname) of + case Symtab.curried_lookup (fst tab2) tyname of NONE => error ("get_type_id: no such type: " ^ quote tyname) | SOME (module, s) => let @@ -556,15 +557,15 @@ NONE => defs | SOME _ => (case dest (prep_def (Thm.get_axiom thy name)) of NONE => defs - | SOME (s, (T, (args, rhs))) => Symtab.update - ((s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) :: - if_none (Symtab.lookup (defs, s)) []), defs))) + | SOME (s, (T, (args, rhs))) => Symtab.curried_update + (s, (T, (thyname, split_last (rename_terms (args @ [rhs])))) :: + if_none (Symtab.curried_lookup defs s) []) defs)) in foldl (fn ((thyname, axms), defs) => Symtab.foldl (add_def thyname) (defs, axms)) Symtab.empty axmss end; -fun get_defn thy defs s T = (case Symtab.lookup (defs, s) of +fun get_defn thy defs s T = (case Symtab.curried_lookup defs s of NONE => NONE | SOME ds => let val i = find_index (is_instance thy T o fst) ds @@ -828,7 +829,7 @@ (Graph.merge (fn ((_, module, _), (_, module', _)) => module = module') (gr, gr'), (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr - (map (fn s => case Symtab.lookup (graphs, s) of + (map (fn s => case Symtab.curried_lookup graphs s of NONE => error ("Undefined code module: " ^ s) | SOME gr => gr) modules)) handle Graph.DUPS ks => error ("Duplicate code for " ^ commas ks); @@ -1055,8 +1056,7 @@ "use \"" ^ name ^ ".ML\";\n") code)) :: code) else File.write (Path.unpack fname) (snd (hd code))); if lib then thy - else map_modules (fn graphs => - Symtab.update ((module, gr), graphs)) thy) + else map_modules (Symtab.curried_update (module, gr)) thy) end)); val code_libraryP = diff -r df7c3b1f390a -r 193b84a70ca4 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Mon Sep 05 17:38:17 2005 +0200 +++ b/src/ZF/Tools/datatype_package.ML Mon Sep 05 17:38:18 2005 +0200 @@ -383,8 +383,8 @@ (("recursor_eqns", recursor_eqns), []), (("free_iffs", free_iffs), []), (("free_elims", free_SEs), [])]) - |> DatatypesData.map (fn tab => Symtab.update ((big_rec_name, dt_info), tab)) - |> ConstructorsData.map (fn tab => foldr Symtab.update tab con_pairs) + |> DatatypesData.map (Symtab.curried_update (big_rec_name, dt_info)) + |> ConstructorsData.map (fold Symtab.curried_update con_pairs) |> Theory.parent_path, ind_result, {con_defs = con_defs,