--- a/src/HOL/Lattices.thy Mon May 27 07:42:10 2013 +0200
+++ b/src/HOL/Lattices.thy Mon May 27 07:44:10 2013 +0200
@@ -49,9 +49,7 @@
obtains "a = a * b"
using assms by (unfold order_iff)
-end
-
-sublocale semilattice_order < ordering less_eq less
+sublocale ordering less_eq less
proof
fix a b
show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
@@ -79,9 +77,6 @@
then show "a \<preceq> c" by (rule orderI)
qed
-context semilattice_order
-begin
-
lemma cobounded1 [simp]:
"a * b \<preceq> a"
by (simp add: order_iff commute)
@@ -132,10 +127,13 @@
end
locale semilattice_neutr_order = semilattice_neutr + semilattice_order
+begin
-sublocale semilattice_neutr_order < ordering_top less_eq less 1
+sublocale ordering_top less_eq less 1
by default (simp add: order_iff)
+end
+
notation times (infixl "*" 70)
notation Groups.one ("1")
@@ -255,7 +253,10 @@
subsubsection {* Equational laws *}
-sublocale semilattice_inf < inf!: semilattice inf
+context semilattice_inf
+begin
+
+sublocale inf!: semilattice inf
proof
fix a b c
show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
@@ -266,26 +267,9 @@
by (rule antisym) auto
qed
-sublocale semilattice_sup < sup!: semilattice sup
-proof
- fix a b c
- show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
- by (rule antisym) (auto intro: le_supI1 le_supI2)
- show "a \<squnion> b = b \<squnion> a"
- by (rule antisym) auto
- show "a \<squnion> a = a"
- by (rule antisym) auto
-qed
-
-sublocale semilattice_inf < inf!: semilattice_order inf less_eq less
+sublocale inf!: semilattice_order inf less_eq less
by default (auto simp add: le_iff_inf less_le)
-sublocale semilattice_sup < sup!: semilattice_order sup greater_eq greater
- by default (auto simp add: le_iff_sup sup.commute less_le)
-
-context semilattice_inf
-begin
-
lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
by (fact inf.assoc)
@@ -317,6 +301,20 @@
context semilattice_sup
begin
+sublocale sup!: semilattice sup
+proof
+ fix a b c
+ show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
+ by (rule antisym) (auto intro: le_supI1 le_supI2)
+ show "a \<squnion> b = b \<squnion> a"
+ by (rule antisym) auto
+ show "a \<squnion> a = a"
+ by (rule antisym) auto
+qed
+
+sublocale sup!: semilattice_order sup greater_eq greater
+ by default (auto simp add: le_iff_sup sup.commute less_le)
+
lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
by (fact sup.assoc)
@@ -469,8 +467,9 @@
subsection {* Bounded lattices and boolean algebras *}
class bounded_semilattice_inf_top = semilattice_inf + top
+begin
-sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr inf top
+sublocale inf_top!: semilattice_neutr inf top
+ inf_top!: semilattice_neutr_order inf top less_eq less
proof
fix x
@@ -478,9 +477,12 @@
by (rule inf_absorb1) simp
qed
-class bounded_semilattice_sup_bot = semilattice_sup + bot
+end
-sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr sup bot
+class bounded_semilattice_sup_bot = semilattice_sup + bot
+begin
+
+sublocale sup_bot!: semilattice_neutr sup bot
+ sup_bot!: semilattice_neutr_order sup bot greater_eq greater
proof
fix x
@@ -488,6 +490,8 @@
by (rule sup_absorb1) simp
qed
+end
+
class bounded_lattice_bot = lattice + bot
begin
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon May 27 07:44:10 2013 +0200
@@ -521,11 +521,11 @@
(* FIXME: Make "SPASS_NEW_HOME" legacy. *)
val spass_config : atp_config =
{exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
- arguments =
- fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ =>
- "-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^
- file_name
- |> extra_options <> "" ? prefix (extra_options ^ " "),
+ arguments = fn _ => fn full_proofs => fn extra_options => fn timeout =>
+ fn file_name => fn _ =>
+ "-Isabelle=1 " ^ (if full_proofs then "-Splits=0 " else "") ^
+ "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name
+ |> extra_options <> "" ? prefix (extra_options ^ " "),
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
[(OldSPASS, "Unrecognized option Isabelle"),
@@ -711,12 +711,12 @@
fun remote_config system_name system_versions proof_delims known_failures
prem_role best_slice : atp_config =
{exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
- arguments =
- fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ =>
- (if command <> "" then "-c " ^ quote command ^ " " else "") ^
- "-s " ^ the_remote_system system_name system_versions ^ " " ^
- "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
- " " ^ file_name,
+ arguments = fn _ => fn _ => fn command => fn timeout => fn file_name =>
+ fn _ =>
+ (if command <> "" then "-c " ^ quote command ^ " " else "") ^
+ "-s " ^ the_remote_system system_name system_versions ^ " " ^
+ "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
+ " " ^ file_name,
proof_delims = union (op =) tstp_proof_delims proof_delims,
known_failures = known_failures @ known_perl_failures @ known_says_failures,
prem_role = prem_role,
--- a/src/HOL/Tools/Metis/metis_generate.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML Mon May 27 07:44:10 2013 +0200
@@ -111,14 +111,14 @@
t
| t => t)
-fun reveal_lam_lifted lambdas =
+fun reveal_lam_lifted lifted =
map_aterms (fn t as Const (s, _) =>
if String.isPrefix lam_lifted_prefix s then
- case AList.lookup (op =) lambdas s of
+ case AList.lookup (op =) lifted s of
SOME t =>
Const (@{const_name Metis.lambda}, dummyT)
$ map_types (map_type_tvar (K dummyT))
- (reveal_lam_lifted lambdas t)
+ (reveal_lam_lifted lifted t)
| NONE => t
else
t
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 27 07:44:10 2013 +0200
@@ -912,7 +912,7 @@
fun export (_, (output, _, _, _, _)) =
if dest_dir = "" then ()
else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
- val ((_, (_, pool, fact_names, _, sym_tab)),
+ val ((_, (_, pool, fact_names, lifted, sym_tab)),
(output, run_time, used_from, atp_proof, outcome)) =
with_cleanup clean_up run () |> tap export
val important_message =
@@ -951,7 +951,7 @@
()
val isar_params =
(debug, verbose, preplay_timeout, preplay_trace, isar_compress,
- pool, fact_names, sym_tab, atp_proof, goal)
+ pool, fact_names, lifted, sym_tab, atp_proof, goal)
val one_line_params =
(preplay, proof_banner mode name, used_facts,
choose_minimize_command ctxt params minimize_command name
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon May 27 07:44:10 2013 +0200
@@ -24,7 +24,8 @@
play * string * (string * stature) list * minimize_command * int * int
type isar_params =
bool * bool * Time.time option * bool * real * string Symtab.table
- * (string * stature) list vector * int Symtab.table * string proof * thm
+ * (string * stature) list vector * (string * term) list * int Symtab.table
+ * string proof * thm
val smtN : string
val string_of_reconstructor : reconstructor -> string
@@ -323,12 +324,25 @@
| aux t = t
in aux end
-fun decode_line ctxt sym_tab (name, role, u, rule, deps) =
+fun unlift_term lifted =
+ map_aterms (fn t as Const (s, _) =>
+ if String.isPrefix lam_lifted_prefix s then
+ case AList.lookup (op =) lifted s of
+ SOME t =>
+ (* FIXME: do something about the types *)
+ unlift_term lifted t
+ | NONE => t
+ else
+ t
+ | t => t)
+
+fun decode_line ctxt lifted sym_tab (name, role, u, rule, deps) =
let
val thy = Proof_Context.theory_of ctxt
val t =
u |> prop_of_atp ctxt true sym_tab
|> uncombine_term thy
+ |> unlift_term lifted
|> infer_formula_types ctxt
in (name, role, t, rule, deps) end
@@ -627,11 +641,12 @@
type isar_params =
bool * bool * Time.time option * bool * real * string Symtab.table
- * (string * stature) list vector * int Symtab.table * string proof * thm
+ * (string * stature) list vector * (string * term) list * int Symtab.table
+ * string proof * thm
fun isar_proof_text ctxt isar_proofs
(debug, verbose, preplay_timeout, preplay_trace, isar_compress, pool,
- fact_names, sym_tab, atp_proof, goal)
+ fact_names, lifted, sym_tab, atp_proof, goal)
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
let
val ((params, hyp_ts, concl_t), ctxt) = strip_subgoal goal subgoal ctxt
@@ -649,7 +664,7 @@
|> clean_up_atp_proof_dependencies
|> nasty_atp_proof pool
|> map_term_names_in_atp_proof repair_name
- |> map (decode_line ctxt sym_tab)
+ |> map (decode_line ctxt lifted sym_tab)
|> repair_waldmeister_endgame
|> rpair [] |-> fold_rev (add_line fact_names)
|> rpair [] |-> fold_rev add_nontrivial_line
--- a/src/HOL/Tools/case_translation.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML Mon May 27 07:44:10 2013 +0200
@@ -90,25 +90,30 @@
val lookup_by_case = Symtab.lookup o cases_of;
+
(** installation **)
fun case_error s = error ("Error in case expression:\n" ^ s);
val name_of = try (dest_Const #> fst);
+
(* parse translation *)
fun constrain_Abs tT t = Syntax.const @{syntax_const "_constrainAbs"} $ t $ tT;
fun case_tr err ctxt [t, u] =
let
- val thy = Proof_Context.theory_of ctxt;
+ val consts = Proof_Context.consts_of ctxt;
+ fun is_const s = can (Consts.the_constraint consts) (Consts.intern consts s);
- fun is_const s =
- Sign.declared_const thy (Proof_Context.intern_const ctxt s);
+ fun variant_free x used =
+ let val (x', used') = Name.variant x used
+ in if is_const x' then variant_free x' used' else (x', used') end;
- fun abs p tTs t = Syntax.const @{const_syntax case_abs} $
- fold constrain_Abs tTs (absfree p t);
+ fun abs p tTs t =
+ Syntax.const @{const_syntax case_abs} $
+ fold constrain_Abs tTs (absfree p t);
fun abs_pat (Const (@{syntax_const "_constrain"}, _) $ t $ tT) tTs =
abs_pat t (tT :: tTs)
@@ -119,7 +124,7 @@
(* replace occurrences of dummy_pattern by distinct variables *)
fun replace_dummies (Const (@{const_syntax dummy_pattern}, T)) used =
- let val (x, used') = Name.variant "x" used
+ let val (x, used') = variant_free "x" used
in (Free (x, T), used') end
| replace_dummies (t $ u) used =
let
@@ -129,9 +134,9 @@
| replace_dummies t used = (t, used);
fun dest_case1 (t as Const (@{syntax_const "_case1"}, _) $ l $ r) =
- let val (l', _) = replace_dummies l (Term.declare_term_frees t Name.context)
- in abs_pat l' []
- (Syntax.const @{const_syntax case_elem} $ Term_Position.strip_positions l' $ r)
+ let val (l', _) = replace_dummies l (Term.declare_term_frees t Name.context) in
+ abs_pat l' []
+ (Syntax.const @{const_syntax case_elem} $ Term_Position.strip_positions l' $ r)
end
| dest_case1 _ = case_error "dest_case1";
@@ -140,11 +145,11 @@
val errt = if err then @{term True} else @{term False};
in
- Syntax.const @{const_syntax case_guard} $ errt $ t $ (fold_rev
- (fn t => fn u =>
- Syntax.const @{const_syntax case_cons} $ dest_case1 t $ u)
- (dest_case2 u)
- (Syntax.const @{const_syntax case_nil}))
+ Syntax.const @{const_syntax case_guard} $ errt $ t $
+ (fold_rev
+ (fn t => fn u => Syntax.const @{const_syntax case_cons} $ dest_case1 t $ u)
+ (dest_case2 u)
+ (Syntax.const @{const_syntax case_nil}))
end
| case_tr _ _ _ = case_error "case_tr";
@@ -161,17 +166,19 @@
| mk_clause (Const (@{const_syntax case_elem}, _) $ pat $ rhs) xs _ =
Syntax.const @{syntax_const "_case1"} $
subst_bounds (map Syntax_Trans.mark_bound_abs xs, pat) $
- subst_bounds (map Syntax_Trans.mark_bound_body xs, rhs);
+ subst_bounds (map Syntax_Trans.mark_bound_body xs, rhs)
+ | mk_clause _ _ _ = raise Match;
fun mk_clauses (Const (@{const_syntax case_nil}, _)) = []
| mk_clauses (Const (@{const_syntax case_cons}, _) $ t $ u) =
- mk_clause t [] (Term.declare_term_frees t Name.context) ::
- mk_clauses u
+ mk_clause t [] (Term.declare_term_frees t Name.context) :: mk_clauses u
+ | mk_clauses _ = raise Match;
in
list_comb (Syntax.const @{syntax_const "_case_syntax"} $ x $
foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
(mk_clauses t), ts)
- end;
+ end
+ | case_tr' _ = raise Match;
val trfun_setup' = Sign.print_translation [(@{const_syntax "case_guard"}, K case_tr')];
@@ -204,13 +211,13 @@
(*Each pattern carries with it a tag i, which denotes the clause it
-came from. i = ~1 indicates that the clause was added by pattern
-completion.*)
+ came from. i = ~1 indicates that the clause was added by pattern
+ completion.*)
-fun add_row_used ((prfx, pats), (tm, tag)) =
+fun add_row_used ((prfx, pats), (tm, _)) =
fold Term.declare_term_frees (tm :: pats @ map Free prfx);
-(* try to preserve names given by user *)
+(*try to preserve names given by user*)
fun default_name "" (Free (name', _)) = name'
| default_name name _ = name;
@@ -220,8 +227,9 @@
let
val (_, T) = dest_Const c;
val Ts = binder_types T;
- val (names, _) = fold_map Name.variant
- (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts)) used;
+ val (names, _) =
+ fold_map Name.variant
+ (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts)) used;
val ty = body_type T;
val ty_theta = Type.raw_match (ty, colty) Vartab.empty
handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);
@@ -251,8 +259,7 @@
(* Partitioning *)
fun partition _ _ _ _ [] = raise CASE_ERROR ("partition: no rows", ~1)
- | partition used constructors colty res_ty
- (rows as (((prfx, _ :: ps), _) :: _)) =
+ | partition used constructors colty res_ty (rows as (((prfx, _ :: ps), _) :: _)) =
let
fun part [] [] = []
| part [] ((_, (_, i)) :: _) = raise CASE_ERROR ("Not a constructor pattern", i)
@@ -293,7 +300,7 @@
let
val get_info = lookup_by_constr_permissive ctxt;
- fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand", ~1)
+ fun expand _ _ _ ((_, []), _) = raise CASE_ERROR ("mk_case: expand", ~1)
| expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
if is_Free p then
let
@@ -308,11 +315,10 @@
fun mk _ [] = raise CASE_ERROR ("no rows", ~1)
| mk [] (((_, []), (tm, tag)) :: _) = ([tag], tm) (* Done *)
- | mk path (rows as ((row as ((_, [Free _]), _)) :: _ :: _)) = mk path [row]
+ | mk path ((row as ((_, [Free _]), _)) :: _ :: _) = mk path [row]
| mk (u :: us) (rows as ((_, _ :: _), _) :: _) =
let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in
- (case Option.map (apfst head_of)
- (find_first (not o is_Free o fst) col0) of
+ (case Option.map (apfst head_of) (find_first (not o is_Free o fst) col0) of
NONE =>
let
val rows' = map (fn ((v, _), row) => row ||>
@@ -326,8 +332,7 @@
val pty = body_type cT;
val used' = fold Term.declare_term_frees us used;
val nrows = maps (expand constructors used' pty) rows;
- val subproblems =
- partition used' constructors pty range_ty nrows;
+ val subproblems = partition used' constructors pty range_ty nrows;
val (pat_rect, dtrees) =
split_list (map (fn {new_formals, group, ...} =>
mk (new_formals @ us) group) subproblems);
@@ -509,13 +514,13 @@
encode_clause recur S T p $ encode_cases recur S T ps;
fun encode_case recur (t, ps as (pat, rhs) :: _) =
- let
- val tT = fastype_of t;
- val T = fastype_of rhs;
- in
- Const (@{const_name case_guard}, @{typ bool} --> tT --> (tT --> T) --> T) $
- @{term True} $ t $ (encode_cases recur (fastype_of pat) (fastype_of rhs) ps)
- end
+ let
+ val tT = fastype_of t;
+ val T = fastype_of rhs;
+ in
+ Const (@{const_name case_guard}, @{typ bool} --> tT --> (tT --> T) --> T) $
+ @{term True} $ t $ (encode_cases recur (fastype_of pat) (fastype_of rhs) ps)
+ end
| encode_case _ _ = case_error "encode_case";
fun strip_case' ctxt d (pat, rhs) =
@@ -542,8 +547,8 @@
(strip_case_full ctxt d x, maps (strip_case' ctxt d) clauses)
| NONE =>
(case t of
- (t $ u) => strip_case_full ctxt d t $ strip_case_full ctxt d u
- | (Abs (x, T, u)) =>
+ t $ u => strip_case_full ctxt d t $ strip_case_full ctxt d u
+ | Abs (x, T, u) =>
let val (x', u') = Term.dest_abs (x, T, u);
in Term.absfree (x', T) (strip_case_full ctxt d u') end
| _ => t));
@@ -577,17 +582,25 @@
fun print_case_translations ctxt =
let
- val cases = Symtab.dest (cases_of ctxt);
- fun show_case (_, data as (comb, ctrs)) =
- (Pretty.block o Pretty.fbreaks)
- [Pretty.block [Pretty.str (Tname_of_data data), Pretty.str ":"],
- Pretty.block [Pretty.brk 3, Pretty.block
- [Pretty.str "combinator:", Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt comb)]],
- Pretty.block [Pretty.brk 3, Pretty.block
- [Pretty.str "constructors:", Pretty.brk 1,
- Pretty.block (Pretty.commas (map (Pretty.quote o Syntax.pretty_term ctxt) ctrs))]]];
+ val cases = map snd (Symtab.dest (cases_of ctxt));
+ val type_space = Proof_Context.type_space ctxt;
+
+ val pretty_term = Syntax.pretty_term ctxt;
+
+ fun pretty_data (data as (comb, ctrs)) =
+ let
+ val name = Tname_of_data data;
+ val xname = Name_Space.extern ctxt type_space name;
+ val markup = Name_Space.markup type_space name;
+ val prt =
+ (Pretty.block o Pretty.fbreaks)
+ [Pretty.block [Pretty.mark_str (markup, xname), Pretty.str ":"],
+ Pretty.block [Pretty.str "combinator:", Pretty.brk 1, pretty_term comb],
+ Pretty.block (Pretty.str "constructors:" :: Pretty.brk 1 ::
+ Pretty.commas (map pretty_term ctrs))];
+ in (xname, prt) end;
in
- Pretty.big_list "case translations:" (map show_case cases)
+ Pretty.big_list "case translations:" (map #2 (sort_wrt #1 (map pretty_data cases)))
|> Pretty.writeln
end;
--- a/src/Pure/Isar/expression.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/Pure/Isar/expression.ML Mon May 27 07:44:10 2013 +0200
@@ -882,7 +882,7 @@
then
lthy
|> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
- Local_Theory.notes_kind Local_Theory.add_registration expression raw_eqns
+ Local_Theory.notes_kind Generic_Target.theory_registration expression raw_eqns
else
lthy
|> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
@@ -895,7 +895,7 @@
in
lthy
|> generic_interpretation prep_expr prep_prop prep_attr Element.witness_proof_eqs
- Local_Theory.notes_kind (Local_Theory.add_dependency locale) expression raw_eqns
+ Local_Theory.notes_kind (Generic_Target.locale_dependency locale) expression raw_eqns
end;
fun gen_sublocale_global prep_expr prep_loc prep_prop prep_attr before_exit raw_locale expression raw_eqns thy =
@@ -915,8 +915,8 @@
let
val _ = Local_Theory.assert_bottom true lthy;
val target = Named_Target.the_name lthy;
- val subscribe = if target = "" then Local_Theory.add_registration
- else Local_Theory.add_dependency target;
+ val subscribe = if target = "" then Generic_Target.theory_registration
+ else Generic_Target.locale_dependency target;
in
lthy
|> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
--- a/src/Pure/Isar/generic_target.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/Pure/Isar/generic_target.ML Mon May 27 07:44:10 2013 +0200
@@ -41,6 +41,10 @@
val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term * term -> term list ->
local_theory -> local_theory
val theory_declaration: declaration -> local_theory -> local_theory
+ val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
+ local_theory -> local_theory
+ val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
+ local_theory -> local_theory
end
structure Generic_Target: GENERIC_TARGET =
@@ -271,6 +275,16 @@
in generic_const same_shape prmode ((b', mx), rhs') end);
+(* registrations and dependencies *)
+
+val theory_registration =
+ Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
+
+fun locale_dependency locale dep_morph mixin export =
+ (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
+ #> Local_Theory.activate_nonbrittle dep_morph mixin export;
+
+
(** primitive theory operations **)
--- a/src/Pure/Isar/local_theory.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/Pure/Isar/local_theory.ML Mon May 27 07:44:10 2013 +0200
@@ -58,9 +58,7 @@
val const_alias: binding -> string -> local_theory -> local_theory
val activate: string * morphism -> (morphism * bool) option -> morphism ->
local_theory -> local_theory
- val add_registration: string * morphism -> (morphism * bool) option -> morphism ->
- local_theory -> local_theory
- val add_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
+ val activate_nonbrittle: string * morphism -> (morphism * bool) option -> morphism ->
local_theory -> local_theory
val init: Name_Space.naming -> operations -> Proof.context -> local_theory
val exit: local_theory -> Proof.context
@@ -308,19 +306,13 @@
(* activation of locale fragments *)
-fun activate_surface dep_morph mixin export =
+fun activate_nonbrittle dep_morph mixin export =
map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
(naming, operations, after_close, brittle,
(Context.proof_map ooo Locale.add_registration) dep_morph mixin export target));
fun activate dep_morph mixin export =
- mark_brittle #> activate_surface dep_morph mixin export;
-
-val add_registration = raw_theory o Context.theory_map ooo Locale.add_registration;
-
-fun add_dependency locale dep_morph mixin export =
- (raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
- #> activate_surface dep_morph mixin export;
+ mark_brittle #> activate_nonbrittle dep_morph mixin export;
(** init and exit **)
--- a/src/Pure/Isar/proof_context.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon May 27 07:44:10 2013 +0200
@@ -28,7 +28,6 @@
val set_defsort: sort -> Proof.context -> Proof.context
val default_sort: Proof.context -> indexname -> sort
val consts_of: Proof.context -> Consts.T
- val the_const_constraint: Proof.context -> string -> typ
val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
val facts_of: Proof.context -> Facts.T
@@ -264,8 +263,6 @@
fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
val consts_of = #1 o #consts o rep_data;
-val the_const_constraint = Consts.the_constraint o consts_of;
-
val facts_of = #facts o rep_data;
val cases_of = #cases o rep_data;
--- a/src/Pure/Syntax/syntax.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/Pure/Syntax/syntax.ML Mon May 27 07:44:10 2013 +0200
@@ -91,8 +91,6 @@
val mode_input: mode
val empty_syntax: syntax
val merge_syntax: syntax * syntax -> syntax
- val token_markers: string list
- val basic_nonterms: string list
val print_gram: syntax -> unit
val print_trans: syntax -> unit
val print_syntax: syntax -> unit
@@ -528,20 +526,6 @@
end;
-(* basic syntax *)
-
-val token_markers =
- ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
-
-val basic_nonterms =
- Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
- "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
- "any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
- "float_position", "xnum_position", "index", "struct", "tid_position",
- "tvar_position", "id_position", "longid_position", "var_position", "str_position",
- "type_name", "class_name"];
-
-
(** print syntax **)
--- a/src/Pure/Syntax/syntax_phases.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Mon May 27 07:44:10 2013 +0200
@@ -151,11 +151,16 @@
then [Ast.Variable (Lexicon.str_of_token tok)]
else [];
+ fun ast_of_position tok =
+ Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok));
+
+ fun ast_of_dummy a tok =
+ if raw then Ast.Constant a
+ else Ast.Appl [Ast.Constant "_constrain", Ast.Constant a, ast_of_position tok];
+
fun asts_of_position c tok =
if raw then asts_of_token tok
- else
- [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok),
- Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
+ else [Ast.Appl [Ast.Constant c, ast_of (Parser.Tip tok), ast_of_position tok]]
and asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
let
@@ -174,6 +179,12 @@
in [Ast.Constant (Lexicon.mark_type c)] end
| asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
| asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
+ | asts_of (Parser.Node (a as "\\<^const>dummy_pattern", [Parser.Tip tok])) =
+ [ast_of_dummy a tok]
+ | asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) =
+ [ast_of_dummy a tok]
+ | asts_of (Parser.Node ("_idtypdummy", pts as [Parser.Tip tok, _, _])) =
+ [Ast.Appl (Ast.Constant "_constrain" :: ast_of_dummy "_idtdummy" tok :: maps asts_of pts)]
| asts_of (Parser.Node (a, pts)) =
let
val _ = pts |> List.app
@@ -517,7 +528,7 @@
val {structs, fixes} = idents;
fun mark_atoms ((t as Const (c, _)) $ u) =
- if member (op =) Syntax.token_markers c
+ if member (op =) Pure_Thy.token_markers c
then t $ u else mark_atoms t $ mark_atoms u
| mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
| mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
--- a/src/Pure/Syntax/syntax_trans.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML Mon May 27 07:44:10 2013 +0200
@@ -121,9 +121,6 @@
fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty]
| idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
-fun idtypdummy_ast_tr [ty] = Ast.Appl [Ast.Constant "_constrain", Ast.Constant "_idtdummy", ty]
- | idtypdummy_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
-
fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
| lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
@@ -513,7 +510,6 @@
("_applC", fn _ => applC_ast_tr),
("_lambda", fn _ => lambda_ast_tr),
("_idtyp", fn _ => idtyp_ast_tr),
- ("_idtypdummy", fn _ => idtypdummy_ast_tr),
("_bigimpl", fn _ => bigimpl_ast_tr),
("_indexdefault", fn _ => indexdefault_ast_tr),
("_indexvar", fn _ => indexvar_ast_tr),
--- a/src/Pure/pure_thy.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/Pure/pure_thy.ML Mon May 27 07:44:10 2013 +0200
@@ -8,6 +8,7 @@
sig
val old_appl_syntax: theory -> bool
val old_appl_syntax_setup: theory -> theory
+ val token_markers: string list
end;
structure Pure_Thy: PURE_THY =
@@ -52,6 +53,9 @@
(* main content *)
+val token_markers =
+ ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
+
val _ = Context.>> (Context.map_theory
(Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
Old_Appl_Syntax.put false #>
@@ -60,8 +64,15 @@
(Binding.name "prop", 0, NoSyn),
(Binding.name "itself", 1, NoSyn),
(Binding.name "dummy", 0, NoSyn)]
- #> Sign.add_nonterminals_global (map Binding.name Syntax.basic_nonterms)
- #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) Syntax.token_markers)
+ #> Sign.add_nonterminals_global
+ (map Binding.name
+ (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
+ "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
+ "any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
+ "float_position", "xnum_position", "index", "struct", "tid_position",
+ "tvar_position", "id_position", "longid_position", "var_position", "str_position",
+ "type_name", "class_name"]))
+ #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) token_markers)
#> Sign.add_syntax_i
[("", typ "prop' => prop", Delimfix "_"),
("", typ "logic => any", Delimfix "_"),
@@ -153,7 +164,7 @@
("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
(const "==>", typ "prop => prop => prop", Delimfix "op ==>"),
- (const Term.dummy_patternN, typ "aprop", Delimfix "'_"),
+ (const "dummy_pattern", typ "aprop", Delimfix "'_"),
("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
(const "Pure.term", typ "logic => prop", Delimfix "TERM _"),
(const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
@@ -183,12 +194,12 @@
(Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
(Binding.name "prop", typ "prop => prop", NoSyn),
(Binding.name "TYPE", typ "'a itself", NoSyn),
- (Binding.name Term.dummy_patternN, typ "'a", Delimfix "'_")]
+ (Binding.name "dummy_pattern", typ "'a", Delimfix "'_")]
#> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
#> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
#> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
#> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
- #> Theory.add_deps_global Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
+ #> Theory.add_deps_global "dummy_pattern" ("dummy_pattern", typ "'a") []
#> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
#> Sign.parse_translation Syntax_Trans.pure_parse_translation
#> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
--- a/src/Pure/term.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/Pure/term.ML Mon May 27 07:44:10 2013 +0200
@@ -159,7 +159,6 @@
val maxidx_term: term -> int -> int
val has_abs: term -> bool
val dest_abs: string * typ * term -> string * term
- val dummy_patternN: string
val dummy_pattern: typ -> term
val dummy: term
val dummy_prop: term
@@ -925,9 +924,7 @@
(* dummy patterns *)
-val dummy_patternN = "dummy_pattern";
-
-fun dummy_pattern T = Const (dummy_patternN, T);
+fun dummy_pattern T = Const ("dummy_pattern", T);
val dummy = dummy_pattern dummyT;
val dummy_prop = dummy_pattern propT;
--- a/src/Tools/Code/code_target.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/Tools/Code/code_target.ML Mon May 27 07:44:10 2013 +0200
@@ -419,7 +419,7 @@
val value_name = "Value.value.value"
val program = prepared_program
|> Graph.new_node (value_name,
- Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
+ Code_Thingol.Fun (@{const_name dummy_pattern}, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
|> fold (curry (perhaps o try o Graph.add_edge) value_name) consts;
val (program_code, deresolve) = produce (mounted_serializer program);
val value_name' = the (deresolve value_name);
--- a/src/Tools/Code/code_thingol.ML Mon May 27 07:42:10 2013 +0200
+++ b/src/Tools/Code/code_thingol.ML Mon May 27 07:44:10 2013 +0200
@@ -938,24 +938,24 @@
val ty = fastype_of t;
val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
o dest_TFree))) t [];
- val t' = annotate thy algbr eqngr (Term.dummy_patternN, ty) [] t;
+ val t' = annotate thy algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
val stmt_value =
fold_map (translate_tyvar_sort thy algbr eqngr false) vs
##>> translate_typ thy algbr eqngr false ty
##>> translate_term thy algbr eqngr false NONE (t', NONE)
#>> (fn ((vs, ty), t) => Fun
- (Term.dummy_patternN, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
+ (@{const_name dummy_pattern}, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
fun term_value (dep, (naming, program1)) =
let
val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
- Graph.get_node program1 Term.dummy_patternN;
- val deps = Graph.immediate_succs program1 Term.dummy_patternN;
- val program2 = Graph.del_node Term.dummy_patternN program1;
+ Graph.get_node program1 @{const_name dummy_pattern};
+ val deps = Graph.immediate_succs program1 @{const_name dummy_pattern};
+ val program2 = Graph.del_node @{const_name dummy_pattern} program1;
val deps_all = Graph.all_succs program2 deps;
val program3 = Graph.restrict (member (op =) deps_all) program2;
in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
in
- ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN
+ ensure_stmt ((K o K) NONE) pair stmt_value @{const_name dummy_pattern}
#> snd
#> term_value
end;