# HG changeset patch # User wenzelm # Date 1283550888 -7200 # Node ID 93a7365fb4ee504cbe37afed67e95516f51b5251 # Parent e7ecbe86d22e70b23abc4c112339971421f14adf turned eta_contract into proper configuration option; diff -r e7ecbe86d22e -r 93a7365fb4ee NEWS --- a/NEWS Fri Sep 03 22:57:21 2010 +0200 +++ b/NEWS Fri Sep 03 23:54:48 2010 +0200 @@ -30,6 +30,7 @@ ML (Config.T) Isar (attribute) + eta_contract eta_contract show_question_marks show_question_marks show_consts show_consts diff -r e7ecbe86d22e -r 93a7365fb4ee doc-src/TutorialI/Sets/Examples.thy --- a/doc-src/TutorialI/Sets/Examples.thy Fri Sep 03 22:57:21 2010 +0200 +++ b/doc-src/TutorialI/Sets/Examples.thy Fri Sep 03 23:54:48 2010 +0200 @@ -1,6 +1,6 @@ theory Examples imports Main Binomial begin -ML "eta_contract := false" +declare [[eta_contract = false]] ML "Pretty.margin_default := 64" text{*membership, intersection *} diff -r e7ecbe86d22e -r 93a7365fb4ee src/CCL/ROOT.ML --- a/src/CCL/ROOT.ML Fri Sep 03 22:57:21 2010 +0200 +++ b/src/CCL/ROOT.ML Fri Sep 03 23:54:48 2010 +0200 @@ -8,6 +8,4 @@ evaluation to weak head-normal form. *) -eta_contract := true; - use_thys ["Wfd", "Fix"]; diff -r e7ecbe86d22e -r 93a7365fb4ee src/CCL/Set.thy --- a/src/CCL/Set.thy Fri Sep 03 22:57:21 2010 +0200 +++ b/src/CCL/Set.thy Fri Sep 03 23:54:48 2010 +0200 @@ -4,6 +4,8 @@ imports FOL begin +declare [[eta_contract]] + typedecl 'a set arities set :: ("term") "term" diff -r e7ecbe86d22e -r 93a7365fb4ee src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Fri Sep 03 22:57:21 2010 +0200 +++ b/src/Pure/Isar/attrib.ML Fri Sep 03 23:54:48 2010 +0200 @@ -395,6 +395,7 @@ (register_config Syntax.show_structs_value #> register_config Syntax.show_question_marks_value #> register_config Syntax.ambiguity_level_value #> + register_config Syntax.eta_contract_value #> register_config Goal_Display.goals_limit_value #> register_config Goal_Display.show_main_goal_value #> register_config Goal_Display.show_consts_value #> diff -r e7ecbe86d22e -r 93a7365fb4ee src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Fri Sep 03 22:57:21 2010 +0200 +++ b/src/Pure/ProofGeneral/preferences.ML Fri Sep 03 23:54:48 2010 +0200 @@ -129,7 +129,7 @@ bool_pref Goal_Display.show_main_goal_default "show-main-goal" "Show main goal in proof state display", - bool_pref Syntax.eta_contract + bool_pref Syntax.eta_contract_default "eta-contract" "Print terms eta-contracted"]; diff -r e7ecbe86d22e -r 93a7365fb4ee src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Fri Sep 03 22:57:21 2010 +0200 +++ b/src/Pure/Syntax/printer.ML Fri Sep 03 23:54:48 2010 +0200 @@ -172,7 +172,7 @@ fun ast_of tm = (case strip_comb tm of - (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' t)) (map ast_of ts) + (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts) | ((c as Const ("_free", _)), Free (x, T) :: ts) => Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts) | ((c as Const ("_var", _)), Var (xi, T) :: ts) => diff -r e7ecbe86d22e -r 93a7365fb4ee src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Fri Sep 03 22:57:21 2010 +0200 +++ b/src/Pure/Syntax/syn_trans.ML Fri Sep 03 23:54:48 2010 +0200 @@ -6,7 +6,9 @@ signature SYN_TRANS0 = sig - val eta_contract: bool Unsynchronized.ref + val eta_contract_default: bool Unsynchronized.ref + val eta_contract_value: Config.value Config.T + val eta_contract: bool Config.T val atomic_abs_tr': string * typ * term -> term * term val preserve_binder_abs_tr': string -> string -> string * (term list -> term) val preserve_binder_abs2_tr': string -> string -> string * (term list -> term) @@ -49,7 +51,7 @@ signature SYN_TRANS = sig include SYN_TRANS1 - val abs_tr': term -> term + val abs_tr': Proof.context -> term -> term val prop_tr': term -> term val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast @@ -280,9 +282,12 @@ (*do (partial) eta-contraction before printing*) -val eta_contract = Unsynchronized.ref true; +val eta_contract_default = Unsynchronized.ref true; +val eta_contract_value = + Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default)); +val eta_contract = Config.bool eta_contract_value; -fun eta_contr tm = +fun eta_contr ctxt tm = let fun is_aprop (Const ("_aprop", _)) = true | is_aprop _ = false; @@ -298,13 +303,13 @@ | t' => Abs (a, T, t')) | eta_abs t = t; in - if ! eta_contract then eta_abs tm else tm + if Config.get ctxt eta_contract then eta_abs tm else tm end; -fun abs_tr' tm = +fun abs_tr' ctxt tm = uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t)) - (strip_abss strip_abs_vars strip_abs_body (eta_contr tm)); + (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm)); fun atomic_abs_tr' (x, T, t) = let val [xT] = Term.rename_wrt_term t [(x, T)] diff -r e7ecbe86d22e -r 93a7365fb4ee src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Fri Sep 03 22:57:21 2010 +0200 +++ b/src/Pure/Thy/thy_output.ML Fri Sep 03 23:54:48 2010 +0200 @@ -451,7 +451,7 @@ val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean); val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean); val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean); -val _ = add_option "eta_contract" (add_wrapper o setmp_CRITICAL Syntax.eta_contract o boolean); +val _ = add_option "eta_contract" (Config.put eta_contract o boolean); val _ = add_option "display" (Config.put display o boolean); val _ = add_option "break" (Config.put break o boolean); val _ = add_option "quotes" (Config.put quotes o boolean); diff -r e7ecbe86d22e -r 93a7365fb4ee src/ZF/ZF.thy --- a/src/ZF/ZF.thy Fri Sep 03 22:57:21 2010 +0200 +++ b/src/ZF/ZF.thy Fri Sep 03 23:54:48 2010 +0200 @@ -10,7 +10,7 @@ uses "~~/src/Tools/misc_legacy.ML" begin -ML {* eta_contract := false *} +declare [[eta_contract = false]] typedecl i arities i :: "term"