turned eta_contract into proper configuration option;
authorwenzelm
Fri Sep 03 23:54:48 2010 +0200 (2010-09-03 ago)
changeset 3912893a7365fb4ee
parent 39127 e7ecbe86d22e
child 39129 976af4e27cde
turned eta_contract into proper configuration option;
NEWS
doc-src/TutorialI/Sets/Examples.thy
src/CCL/ROOT.ML
src/CCL/Set.thy
src/Pure/Isar/attrib.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/Thy/thy_output.ML
src/ZF/ZF.thy
     1.1 --- a/NEWS	Fri Sep 03 22:57:21 2010 +0200
     1.2 +++ b/NEWS	Fri Sep 03 23:54:48 2010 +0200
     1.3 @@ -30,6 +30,7 @@
     1.4  
     1.5    ML (Config.T)                 Isar (attribute)
     1.6  
     1.7 +  eta_contract                  eta_contract
     1.8    show_question_marks           show_question_marks
     1.9    show_consts                   show_consts
    1.10  
     2.1 --- a/doc-src/TutorialI/Sets/Examples.thy	Fri Sep 03 22:57:21 2010 +0200
     2.2 +++ b/doc-src/TutorialI/Sets/Examples.thy	Fri Sep 03 23:54:48 2010 +0200
     2.3 @@ -1,6 +1,6 @@
     2.4  theory Examples imports Main Binomial begin
     2.5  
     2.6 -ML "eta_contract := false"
     2.7 +declare [[eta_contract = false]]
     2.8  ML "Pretty.margin_default := 64"
     2.9  
    2.10  text{*membership, intersection *}
     3.1 --- a/src/CCL/ROOT.ML	Fri Sep 03 22:57:21 2010 +0200
     3.2 +++ b/src/CCL/ROOT.ML	Fri Sep 03 23:54:48 2010 +0200
     3.3 @@ -8,6 +8,4 @@
     3.4  evaluation to weak head-normal form.
     3.5  *)
     3.6  
     3.7 -eta_contract := true;
     3.8 -
     3.9  use_thys ["Wfd", "Fix"];
     4.1 --- a/src/CCL/Set.thy	Fri Sep 03 22:57:21 2010 +0200
     4.2 +++ b/src/CCL/Set.thy	Fri Sep 03 23:54:48 2010 +0200
     4.3 @@ -4,6 +4,8 @@
     4.4  imports FOL
     4.5  begin
     4.6  
     4.7 +declare [[eta_contract]]
     4.8 +
     4.9  typedecl 'a set
    4.10  arities set :: ("term") "term"
    4.11  
     5.1 --- a/src/Pure/Isar/attrib.ML	Fri Sep 03 22:57:21 2010 +0200
     5.2 +++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 23:54:48 2010 +0200
     5.3 @@ -395,6 +395,7 @@
     5.4   (register_config Syntax.show_structs_value #>
     5.5    register_config Syntax.show_question_marks_value #>
     5.6    register_config Syntax.ambiguity_level_value #>
     5.7 +  register_config Syntax.eta_contract_value #>
     5.8    register_config Goal_Display.goals_limit_value #>
     5.9    register_config Goal_Display.show_main_goal_value #>
    5.10    register_config Goal_Display.show_consts_value #>
     6.1 --- a/src/Pure/ProofGeneral/preferences.ML	Fri Sep 03 22:57:21 2010 +0200
     6.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Fri Sep 03 23:54:48 2010 +0200
     6.3 @@ -129,7 +129,7 @@
     6.4    bool_pref Goal_Display.show_main_goal_default
     6.5      "show-main-goal"
     6.6      "Show main goal in proof state display",
     6.7 -  bool_pref Syntax.eta_contract
     6.8 +  bool_pref Syntax.eta_contract_default
     6.9      "eta-contract"
    6.10      "Print terms eta-contracted"];
    6.11  
     7.1 --- a/src/Pure/Syntax/printer.ML	Fri Sep 03 22:57:21 2010 +0200
     7.2 +++ b/src/Pure/Syntax/printer.ML	Fri Sep 03 23:54:48 2010 +0200
     7.3 @@ -172,7 +172,7 @@
     7.4  
     7.5      fun ast_of tm =
     7.6        (case strip_comb tm of
     7.7 -        (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' t)) (map ast_of ts)
     7.8 +        (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' ctxt t)) (map ast_of ts)
     7.9        | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
    7.10            Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
    7.11        | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
     8.1 --- a/src/Pure/Syntax/syn_trans.ML	Fri Sep 03 22:57:21 2010 +0200
     8.2 +++ b/src/Pure/Syntax/syn_trans.ML	Fri Sep 03 23:54:48 2010 +0200
     8.3 @@ -6,7 +6,9 @@
     8.4  
     8.5  signature SYN_TRANS0 =
     8.6  sig
     8.7 -  val eta_contract: bool Unsynchronized.ref
     8.8 +  val eta_contract_default: bool Unsynchronized.ref
     8.9 +  val eta_contract_value: Config.value Config.T
    8.10 +  val eta_contract: bool Config.T
    8.11    val atomic_abs_tr': string * typ * term -> term * term
    8.12    val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
    8.13    val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
    8.14 @@ -49,7 +51,7 @@
    8.15  signature SYN_TRANS =
    8.16  sig
    8.17    include SYN_TRANS1
    8.18 -  val abs_tr': term -> term
    8.19 +  val abs_tr': Proof.context -> term -> term
    8.20    val prop_tr': term -> term
    8.21    val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    8.22    val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    8.23 @@ -280,9 +282,12 @@
    8.24  
    8.25  (*do (partial) eta-contraction before printing*)
    8.26  
    8.27 -val eta_contract = Unsynchronized.ref true;
    8.28 +val eta_contract_default = Unsynchronized.ref true;
    8.29 +val eta_contract_value =
    8.30 +  Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
    8.31 +val eta_contract = Config.bool eta_contract_value;
    8.32  
    8.33 -fun eta_contr tm =
    8.34 +fun eta_contr ctxt tm =
    8.35    let
    8.36      fun is_aprop (Const ("_aprop", _)) = true
    8.37        | is_aprop _ = false;
    8.38 @@ -298,13 +303,13 @@
    8.39            | t' => Abs (a, T, t'))
    8.40        | eta_abs t = t;
    8.41    in
    8.42 -    if ! eta_contract then eta_abs tm else tm
    8.43 +    if Config.get ctxt eta_contract then eta_abs tm else tm
    8.44    end;
    8.45  
    8.46  
    8.47 -fun abs_tr' tm =
    8.48 +fun abs_tr' ctxt tm =
    8.49    uncurry (fold_rev (fn x => fn t => Lexicon.const "_abs" $ x $ t))
    8.50 -    (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
    8.51 +    (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
    8.52  
    8.53  fun atomic_abs_tr' (x, T, t) =
    8.54    let val [xT] = Term.rename_wrt_term t [(x, T)]
     9.1 --- a/src/Pure/Thy/thy_output.ML	Fri Sep 03 22:57:21 2010 +0200
     9.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Sep 03 23:54:48 2010 +0200
     9.3 @@ -451,7 +451,7 @@
     9.4  val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
     9.5  val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
     9.6  val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
     9.7 -val _ = add_option "eta_contract" (add_wrapper o setmp_CRITICAL Syntax.eta_contract o boolean);
     9.8 +val _ = add_option "eta_contract" (Config.put eta_contract o boolean);
     9.9  val _ = add_option "display" (Config.put display o boolean);
    9.10  val _ = add_option "break" (Config.put break o boolean);
    9.11  val _ = add_option "quotes" (Config.put quotes o boolean);
    10.1 --- a/src/ZF/ZF.thy	Fri Sep 03 22:57:21 2010 +0200
    10.2 +++ b/src/ZF/ZF.thy	Fri Sep 03 23:54:48 2010 +0200
    10.3 @@ -10,7 +10,7 @@
    10.4  uses "~~/src/Tools/misc_legacy.ML"
    10.5  begin
    10.6  
    10.7 -ML {* eta_contract := false *}
    10.8 +declare [[eta_contract = false]]
    10.9  
   10.10  typedecl i
   10.11  arities  i :: "term"