methods: added simp_flags argument, added "depth_limit" flag;
authorwenzelm
Mon Jul 04 20:13:39 2005 +0200 (2005-07-04)
changeset 166847b58002668c0
parent 16683 f1ea17a4f222
child 16685 4ffc943c9c75
methods: added simp_flags argument, added "depth_limit" flag;
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/simplifier.ML	Mon Jul 04 17:09:15 2005 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Mon Jul 04 20:13:39 2005 +0200
     1.3 @@ -475,6 +475,11 @@
     1.4    Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
     1.5    Scan.succeed asm_full_simp_tac);
     1.6  
     1.7 +val simp_flags = Scan.repeat
     1.8 +  (Args.parens (Args.$$$ "depth_limit" -- Args.colon |-- Args.nat)
     1.9 +    >> setmp MetaSimplifier.simp_depth_limit)
    1.10 +  >> curry (Library.foldl op o) I;
    1.11 +
    1.12  val cong_modifiers =
    1.13   [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local):Method.modifier),
    1.14    Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add_local),
    1.15 @@ -494,16 +499,16 @@
    1.16     @ cong_modifiers;
    1.17  
    1.18  fun simp_args more_mods =
    1.19 -  Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options) (more_mods @ simp_modifiers');
    1.20 +  Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options -- Scan.lift simp_flags)
    1.21 +    (more_mods @ simp_modifiers');
    1.22  
    1.23 -
    1.24 -fun simp_method (prems, tac) ctxt = Method.METHOD (fn facts =>
    1.25 +fun simp_method ((prems, tac), FLAGS) ctxt = Method.METHOD (fn facts =>
    1.26    ALLGOALS (Method.insert_tac (prems @ facts)) THEN
    1.27 -    (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
    1.28 +    (FLAGS o CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt));
    1.29  
    1.30 -fun simp_method' (prems, tac) ctxt = Method.METHOD (fn facts =>
    1.31 +fun simp_method' ((prems, tac), FLAGS) ctxt = Method.METHOD (fn facts =>
    1.32    HEADGOAL (Method.insert_tac (prems @ facts) THEN'
    1.33 -      (CHANGED_PROP oo tac) (local_simpset_of ctxt)));
    1.34 +      ((FLAGS o CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
    1.35  
    1.36  
    1.37  (* setup methods *)