--- a/doc-src/IsarImplementation/Thy/Prelim.thy Fri Sep 24 15:37:36 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Fri Sep 24 15:53:13 2010 +0200
@@ -432,30 +432,30 @@
structure Terms = Theory_Data
(
- type T = term OrdList.T;
+ type T = term Ord_List.T;
val empty = [];
val extend = I;
fun merge (ts1, ts2) =
- OrdList.union Term_Ord.fast_term_ord ts1 ts2;
+ Ord_List.union Term_Ord.fast_term_ord ts1 ts2;
)
val get = Terms.get;
fun add raw_t thy =
let val t = Sign.cert_term thy raw_t
- in Terms.map (OrdList.insert Term_Ord.fast_term_ord t) thy end;
+ in Terms.map (Ord_List.insert Term_Ord.fast_term_ord t) thy end;
end;
*}
-text {* We use @{ML_type "term OrdList.T"} for reasonably efficient
+text {* We use @{ML_type "term Ord_List.T"} for reasonably efficient
representation of a set of terms: all operations are linear in the
number of stored elements. Here we assume that our users do not
care about the declaration order, since that data structure forces
its own arrangement of elements.
Observe how the @{verbatim merge} operation joins the data slots of
- the two constituents: @{ML OrdList.union} prevents duplication of
+ the two constituents: @{ML Ord_List.union} prevents duplication of
common data from different branches, thus avoiding the danger of
exponential blowup. (Plain list append etc.\ must never be used for
theory data merges.)
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML Fri Sep 24 15:37:36 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Fri Sep 24 15:53:13 2010 +0200
@@ -275,14 +275,14 @@
structure Filters = Theory_Data
(
- type T = (serial * (term -> bool)) OrdList.T
+ type T = (serial * (term -> bool)) Ord_List.T
val empty = []
val extend = I
- fun merge (fs1, fs2) = fold (OrdList.insert serial_ord) fs2 fs1
+ fun merge (fs1, fs2) = fold (Ord_List.insert serial_ord) fs2 fs1
)
fun add_assertion_filter f =
- Filters.map (OrdList.insert serial_ord (serial (), f))
+ Filters.map (Ord_List.insert serial_ord (serial (), f))
fun filter_assertions thy =
let
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Sep 24 15:37:36 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Sep 24 15:53:13 2010 +0200
@@ -1254,9 +1254,9 @@
fun partition_axioms_by_definitionality ctxt axioms def_names =
let
val axioms = sort (fast_string_ord o pairself fst) axioms
- val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
+ val defs = Ord_List.inter (fast_string_ord o apsnd fst) def_names axioms
val nondefs =
- OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
+ Ord_List.subtract (fast_string_ord o apsnd fst) def_names axioms
|> filter_out ((is_arity_type_axiom orf is_typedef_axiom ctxt true) o snd)
in pairself (map snd) (defs, nondefs) end
@@ -1289,7 +1289,7 @@
#> filter_out (is_class_axiom o snd)
val specs = Defs.all_specifications_of (Theory.defs_of thy)
val def_names = specs |> maps snd |> map_filter #def
- |> OrdList.make fast_string_ord
+ |> Ord_List.make fast_string_ord
val thys = thy :: Theory.ancestors_of thy
val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
val built_in_axioms = axioms_of_thys built_in_thys
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Sep 24 15:37:36 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Sep 24 15:53:13 2010 +0200
@@ -687,7 +687,7 @@
| call_sets [] uss vs = vs :: call_sets uss [] []
| call_sets ([] :: _) _ _ = []
| call_sets ((t :: ts) :: tss) uss vs =
- OrdList.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss)
+ Ord_List.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss)
val sets = call_sets (fun_calls t [] []) [] []
val indexed_sets = sets ~~ (index_seq 0 (length sets))
in
@@ -701,7 +701,7 @@
end
fun static_args_in_terms hol_ctxt x =
map (static_args_in_term hol_ctxt x)
- #> fold1 (OrdList.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
+ #> fold1 (Ord_List.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
fun overlapping_indices [] _ = []
| overlapping_indices _ [] = []
@@ -844,7 +844,7 @@
fun generality (js, _, _) = ~(length js)
fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
x1 <> x2 andalso length j2 < length j1 andalso
- OrdList.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1)
+ Ord_List.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1)
fun do_pass_1 _ [] [_] [_] = I
| do_pass_1 T skipped _ [] = do_pass_2 T skipped
| do_pass_1 T skipped all (z :: zs) =
--- a/src/HOL/Tools/SMT/smt_monomorph.ML Fri Sep 24 15:37:36 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML Fri Sep 24 15:53:13 2010 +0200
@@ -29,7 +29,7 @@
fun add_consts f =
collect_consts_if f (fn (n, T) => Symtab.map_entry n (insert (op =) T))
-val insert_const = OrdList.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
+val insert_const = Ord_List.insert (prod_ord fast_string_ord Term_Ord.typ_ord)
fun tvar_consts_of thm = collect_consts_if typ_has_tvars insert_const thm []
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Fri Sep 24 15:37:36 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Fri Sep 24 15:53:13 2010 +0200
@@ -136,10 +136,10 @@
type T = (int * builtins) list
val empty = []
val extend = I
- fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
+ fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
)
-fun add_builtins bs = Builtins.map (OrdList.insert fst_int_ord (serial (), bs))
+fun add_builtins bs = Builtins.map (Ord_List.insert fst_int_ord (serial (), bs))
fun get_builtins ctxt = map snd (Builtins.get (Context.Proof ctxt))
@@ -212,10 +212,10 @@
type T = (int * (term list -> string option)) list
val empty = []
val extend = I
- fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
+ fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
)
-fun add_logic l = Logics.map (OrdList.insert fst_int_ord (serial (), l))
+fun add_logic l = Logics.map (Ord_List.insert fst_int_ord (serial (), l))
fun choose_logic ctxt ts =
let
--- a/src/HOL/Tools/SMT/z3_interface.ML Fri Sep 24 15:37:36 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Fri Sep 24 15:53:13 2010 +0200
@@ -43,11 +43,11 @@
type T = (int * builtin_fun) list
val empty = []
val extend = I
- fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
+ fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
)
fun add_builtin_funs b =
- Builtins.map (OrdList.insert fst_int_ord (serial (), b))
+ Builtins.map (Ord_List.insert fst_int_ord (serial (), b))
fun get_builtin_funs ctxt c ts =
let
@@ -143,11 +143,11 @@
type T = (int * mk_builtins) list
val empty = []
val extend = I
- fun merge (bs1, bs2) = OrdList.union fst_int_ord bs2 bs1
+ fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
)
fun add_mk_builtins mk =
- Mk_Builtins.map (OrdList.insert fst_int_ord (serial (), mk))
+ Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk))
fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt))
--- a/src/HOL/Tools/sat_solver.ML Fri Sep 24 15:37:36 2010 +0200
+++ b/src/HOL/Tools/sat_solver.ML Fri Sep 24 15:53:13 2010 +0200
@@ -600,7 +600,7 @@
(* representation of clauses as ordered lists of literals (with duplicates removed) *)
(* prop_formula -> int list *)
fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) =
- OrdList.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
+ Ord_List.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
| clause_to_lit_list (PropLogic.BoolVar i) =
[i]
| clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) =
--- a/src/Pure/General/ord_list.ML Fri Sep 24 15:37:36 2010 +0200
+++ b/src/Pure/General/ord_list.ML Fri Sep 24 15:53:13 2010 +0200
@@ -18,7 +18,7 @@
val subtract: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
end;
-structure OrdList: ORD_LIST =
+structure Ord_List: ORD_LIST =
struct
type 'a T = 'a list;
--- a/src/Pure/old_term.ML Fri Sep 24 15:37:36 2010 +0200
+++ b/src/Pure/old_term.ML Fri Sep 24 15:53:13 2010 +0200
@@ -75,7 +75,7 @@
(*Accumulates the Vars in the term, suppressing duplicates.*)
fun add_term_vars (t, vars: term list) = case t of
- Var _ => OrdList.insert Term_Ord.term_ord t vars
+ Var _ => Ord_List.insert Term_Ord.term_ord t vars
| Abs (_,_,body) => add_term_vars(body,vars)
| f$t => add_term_vars (f, add_term_vars(t, vars))
| _ => vars;
@@ -84,7 +84,7 @@
(*Accumulates the Frees in the term, suppressing duplicates.*)
fun add_term_frees (t, frees: term list) = case t of
- Free _ => OrdList.insert Term_Ord.term_ord t frees
+ Free _ => Ord_List.insert Term_Ord.term_ord t frees
| Abs (_,_,body) => add_term_frees(body,frees)
| f$t => add_term_frees (f, add_term_frees(t, frees))
| _ => frees;
--- a/src/Pure/proofterm.ML Fri Sep 24 15:37:36 2010 +0200
+++ b/src/Pure/proofterm.ML Fri Sep 24 15:53:13 2010 +0200
@@ -24,8 +24,8 @@
| Promise of serial * term * typ list
| PThm of serial * ((string * term * typ list option) * proof_body future)
and proof_body = PBody of
- {oracles: (string * term) OrdList.T,
- thms: (serial * (string * term * proof_body future)) OrdList.T,
+ {oracles: (string * term) Ord_List.T,
+ thms: (serial * (string * term * proof_body future)) Ord_List.T,
proof: proof}
val %> : proof * term -> proof
@@ -46,9 +46,9 @@
val oracle_ord: oracle * oracle -> order
val thm_ord: pthm * pthm -> order
- val merge_oracles: oracle OrdList.T -> oracle OrdList.T -> oracle OrdList.T
- val merge_thms: pthm OrdList.T -> pthm OrdList.T -> pthm OrdList.T
- val all_oracles_of: proof_body -> oracle OrdList.T
+ val merge_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T
+ val merge_thms: pthm Ord_List.T -> pthm Ord_List.T -> pthm Ord_List.T
+ val all_oracles_of: proof_body -> oracle Ord_List.T
val approximate_proof_body: proof -> proof_body
(** primitive operations **)
@@ -163,8 +163,8 @@
| Promise of serial * term * typ list
| PThm of serial * ((string * term * typ list option) * proof_body future)
and proof_body = PBody of
- {oracles: (string * term) OrdList.T,
- thms: (serial * (string * term * proof_body future)) OrdList.T,
+ {oracles: (string * term) Ord_List.T,
+ thms: (serial * (string * term * proof_body future)) Ord_List.T,
proof: proof};
type oracle = string * term;
@@ -235,8 +235,8 @@
val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
-val merge_oracles = OrdList.union oracle_ord;
-val merge_thms = OrdList.union thm_ord;
+val merge_oracles = Ord_List.union oracle_ord;
+val merge_thms = Ord_List.union thm_ord;
val all_oracles_of =
let
@@ -259,8 +259,8 @@
| _ => I) [prf] ([], []);
in
PBody
- {oracles = OrdList.make oracle_ord oracles,
- thms = OrdList.make thm_ord thms,
+ {oracles = Ord_List.make oracle_ord oracles,
+ thms = Ord_List.make thm_ord thms,
proof = prf}
end;
--- a/src/Pure/sorts.ML Fri Sep 24 15:37:36 2010 +0200
+++ b/src/Pure/sorts.ML Fri Sep 24 15:53:13 2010 +0200
@@ -14,16 +14,16 @@
signature SORTS =
sig
- val make: sort list -> sort OrdList.T
- val subset: sort OrdList.T * sort OrdList.T -> bool
- val union: sort OrdList.T -> sort OrdList.T -> sort OrdList.T
- val subtract: sort OrdList.T -> sort OrdList.T -> sort OrdList.T
- val remove_sort: sort -> sort OrdList.T -> sort OrdList.T
- val insert_sort: sort -> sort OrdList.T -> sort OrdList.T
- val insert_typ: typ -> sort OrdList.T -> sort OrdList.T
- val insert_typs: typ list -> sort OrdList.T -> sort OrdList.T
- val insert_term: term -> sort OrdList.T -> sort OrdList.T
- val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
+ val make: sort list -> sort Ord_List.T
+ val subset: sort Ord_List.T * sort Ord_List.T -> bool
+ val union: sort Ord_List.T -> sort Ord_List.T -> sort Ord_List.T
+ val subtract: sort Ord_List.T -> sort Ord_List.T -> sort Ord_List.T
+ val remove_sort: sort -> sort Ord_List.T -> sort Ord_List.T
+ val insert_sort: sort -> sort Ord_List.T -> sort Ord_List.T
+ val insert_typ: typ -> sort Ord_List.T -> sort Ord_List.T
+ val insert_typs: typ list -> sort Ord_List.T -> sort Ord_List.T
+ val insert_term: term -> sort Ord_List.T -> sort Ord_List.T
+ val insert_terms: term list -> sort Ord_List.T -> sort Ord_List.T
type algebra
val classes_of: algebra -> serial Graph.T
val arities_of: algebra -> (class * sort list) list Symtab.table
@@ -37,7 +37,7 @@
val inter_sort: algebra -> sort * sort -> sort
val minimize_sort: algebra -> sort -> sort
val complete_sort: algebra -> sort -> sort
- val minimal_sorts: algebra -> sort list -> sort OrdList.T
+ val minimal_sorts: algebra -> sort list -> sort Ord_List.T
val certify_class: algebra -> class -> class (*exception TYPE*)
val certify_sort: algebra -> sort -> sort (*exception TYPE*)
val add_class: Pretty.pp -> class * class list -> algebra -> algebra
@@ -71,13 +71,13 @@
(** ordered lists of sorts **)
-val make = OrdList.make Term_Ord.sort_ord;
-val subset = OrdList.subset Term_Ord.sort_ord;
-val union = OrdList.union Term_Ord.sort_ord;
-val subtract = OrdList.subtract Term_Ord.sort_ord;
+val make = Ord_List.make Term_Ord.sort_ord;
+val subset = Ord_List.subset Term_Ord.sort_ord;
+val union = Ord_List.union Term_Ord.sort_ord;
+val subtract = Ord_List.subtract Term_Ord.sort_ord;
-val remove_sort = OrdList.remove Term_Ord.sort_ord;
-val insert_sort = OrdList.insert Term_Ord.sort_ord;
+val remove_sort = Ord_List.remove Term_Ord.sort_ord;
+val insert_sort = Ord_List.insert Term_Ord.sort_ord;
fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss
| insert_typ (TVar (_, S)) Ss = insert_sort S Ss
--- a/src/Pure/thm.ML Fri Sep 24 15:37:36 2010 +0200
+++ b/src/Pure/thm.ML Fri Sep 24 15:53:13 2010 +0200
@@ -15,7 +15,7 @@
{thy_ref: theory_ref,
T: typ,
maxidx: int,
- sorts: sort OrdList.T}
+ sorts: sort Ord_List.T}
val theory_of_ctyp: ctyp -> theory
val typ_of: ctyp -> typ
val ctyp_of: theory -> typ -> ctyp
@@ -28,9 +28,9 @@
t: term,
T: typ,
maxidx: int,
- sorts: sort OrdList.T}
+ sorts: sort Ord_List.T}
val crep_cterm: cterm ->
- {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort OrdList.T}
+ {thy_ref: theory_ref, t: term, T: ctyp, maxidx: int, sorts: sort Ord_List.T}
val theory_of_cterm: cterm -> theory
val term_of: cterm -> term
val cterm_of: theory -> term -> cterm
@@ -44,16 +44,16 @@
{thy_ref: theory_ref,
tags: Properties.T,
maxidx: int,
- shyps: sort OrdList.T,
- hyps: term OrdList.T,
+ shyps: sort Ord_List.T,
+ hyps: term Ord_List.T,
tpairs: (term * term) list,
prop: term}
val crep_thm: thm ->
{thy_ref: theory_ref,
tags: Properties.T,
maxidx: int,
- shyps: sort OrdList.T,
- hyps: cterm OrdList.T,
+ shyps: sort Ord_List.T,
+ hyps: cterm Ord_List.T,
tpairs: (cterm * cterm) list,
prop: cterm}
exception THM of string * int * thm list
@@ -163,7 +163,7 @@
{thy_ref: theory_ref,
T: typ,
maxidx: int,
- sorts: sort OrdList.T}
+ sorts: sort Ord_List.T}
with
fun rep_ctyp (Ctyp args) = args;
@@ -191,7 +191,7 @@
t: term,
T: typ,
maxidx: int,
- sorts: sort OrdList.T}
+ sorts: sort Ord_List.T}
with
exception CTERM of string * cterm list;
@@ -339,12 +339,12 @@
{thy_ref: theory_ref, (*dynamic reference to theory*)
tags: Properties.T, (*additional annotations/comments*)
maxidx: int, (*maximum index of any Var or TVar*)
- shyps: sort OrdList.T, (*sort hypotheses*)
- hyps: term OrdList.T, (*hypotheses*)
+ shyps: sort Ord_List.T, (*sort hypotheses*)
+ hyps: term Ord_List.T, (*hypotheses*)
tpairs: (term * term) list, (*flex-flex pairs*)
prop: term} (*conclusion*)
and deriv = Deriv of
- {promises: (serial * thm future) OrdList.T,
+ {promises: (serial * thm future) Ord_List.T,
body: Proofterm.proof_body}
with
@@ -380,9 +380,9 @@
fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop;
-val union_hyps = OrdList.union Term_Ord.fast_term_ord;
-val insert_hyps = OrdList.insert Term_Ord.fast_term_ord;
-val remove_hyps = OrdList.remove Term_Ord.fast_term_ord;
+val union_hyps = Ord_List.union Term_Ord.fast_term_ord;
+val insert_hyps = Ord_List.insert Term_Ord.fast_term_ord;
+val remove_hyps = Ord_List.remove Term_Ord.fast_term_ord;
(* merge theories of cterms/thms -- trivial absorption only *)
@@ -493,7 +493,7 @@
(Deriv {promises = ps1, body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
(Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
let
- val ps = OrdList.union promise_ord ps1 ps2;
+ val ps = Ord_List.union promise_ord ps1 ps2;
val oras = Proofterm.merge_oracles oras1 oras2;
val thms = Proofterm.merge_thms thms1 thms2;
val prf =
--- a/src/Pure/variable.ML Fri Sep 24 15:37:36 2010 +0200
+++ b/src/Pure/variable.ML Fri Sep 24 15:53:13 2010 +0200
@@ -77,7 +77,7 @@
binds: (typ * term) Vartab.table, (*term bindings*)
type_occs: string list Symtab.table, (*type variables -- possibly within term variables*)
maxidx: int, (*maximum var index*)
- sorts: sort OrdList.T, (*declared sort occurrences*)
+ sorts: sort Ord_List.T, (*declared sort occurrences*)
constraints:
typ Vartab.table * (*type constraints*)
sort Vartab.table}; (*default sorts*)