src/Pure/Isar/method.ML
changeset 27813 96fbe385a0d0
parent 27751 22c32eb18c23
child 29004 a5a91f387791
     1.1 --- a/src/Pure/Isar/method.ML	Sat Aug 09 22:43:54 2008 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Sat Aug 09 22:43:55 2008 +0200
     1.3 @@ -113,7 +113,6 @@
     1.4    val goal_args_ctxt': (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
     1.5      (Proof.context -> 'a -> int -> tactic) -> src -> Proof.context -> method
     1.6    val parse: OuterLex.token list -> text * OuterLex.token list
     1.7 -  val parse_args: Args.T list -> text * Args.T list
     1.8  end;
     1.9  
    1.10  structure Method: METHOD =
    1.11 @@ -470,6 +469,9 @@
    1.12  
    1.13  (** concrete syntax **)
    1.14  
    1.15 +structure P = OuterParse;
    1.16 +
    1.17 +
    1.18  (* basic *)
    1.19  
    1.20  fun syntax scan = Args.context_syntax "method" scan;
    1.21 @@ -525,7 +527,7 @@
    1.22  val ruleN = "rule";
    1.23  
    1.24  fun modifier name kind kind' att =
    1.25 -  Args.$$$ name |-- (kind >> K NONE || kind' |-- Args.nat --| Args.colon >> SOME)
    1.26 +  Args.$$$ name |-- (kind >> K NONE || kind' |-- P.nat --| Args.colon >> SOME)
    1.27      >> (pair (I: Proof.context -> Proof.context) o att);
    1.28  
    1.29  val iprover_modifiers =
    1.30 @@ -540,7 +542,7 @@
    1.31  in
    1.32  
    1.33  val iprover_meth =
    1.34 -  bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option Args.nat))
    1.35 +  bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option P.nat))
    1.36      (fn n => fn prems => fn ctxt => METHOD (fn facts =>
    1.37        HEADGOAL (insert_tac (prems @ facts) THEN'
    1.38        ObjectLogic.atomize_prems_tac THEN' iprover_tac ctxt n)));
    1.39 @@ -551,7 +553,7 @@
    1.40  (* tactic syntax *)
    1.41  
    1.42  fun nat_thms_args f = uncurry f oo
    1.43 -  (fst oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0) -- Attrib.thms));
    1.44 +  (fst oo syntax (Scan.lift (Scan.optional (Args.parens P.nat) 0) -- Attrib.thms));
    1.45  
    1.46  fun goal_args' args tac src ctxt = fst (syntax (Args.goal_spec HEADGOAL -- args >>
    1.47    (fn (quant, s) => SIMPLE_METHOD'' quant (tac s))) src ctxt);
    1.48 @@ -565,6 +567,30 @@
    1.49  fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac;
    1.50  
    1.51  
    1.52 +(* outer parser *)
    1.53 +
    1.54 +fun is_symid_meth s =
    1.55 +  s <> "|" andalso s <> "?" andalso s <> "+" andalso OuterLex.ident_or_symbolic s;
    1.56 +
    1.57 +local
    1.58 +
    1.59 +fun meth4 x =
    1.60 + (P.position (P.xname >> rpair []) >> (Source o Args.src) ||
    1.61 +  P.$$$ "(" |-- P.!!! (meth0 --| P.$$$ ")")) x
    1.62 +and meth3 x =
    1.63 + (meth4 --| P.$$$ "?" >> Try ||
    1.64 +  meth4 --| P.$$$ "+" >> Repeat1 ||
    1.65 +  meth4 -- (P.$$$ "[" |-- Scan.optional P.nat 1 --| P.$$$ "]") >> (SelectGoals o swap) ||
    1.66 +  meth4) x
    1.67 +and meth2 x =
    1.68 + (P.position (P.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) ||
    1.69 +  meth3) x
    1.70 +and meth1 x = (P.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
    1.71 +and meth0 x = (P.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
    1.72 +
    1.73 +in val parse = meth3 end;
    1.74 +
    1.75 +
    1.76  (* theory setup *)
    1.77  
    1.78  val _ = Context.>> (Context.map_theory
    1.79 @@ -589,63 +615,13 @@
    1.80      ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
    1.81      ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_tac,
    1.82        "rename parameters of goal"),
    1.83 -    ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac,
    1.84 +    ("rotate_tac", goal_args (Scan.optional P.int 1) Tactic.rotate_tac,
    1.85        "rotate assumptions of goal"),
    1.86 -    ("tactic", simple_args (Args.position Args.name) tactic, "ML tactic as proof method"),
    1.87 -    ("raw_tactic", simple_args (Args.position Args.name) raw_tactic,
    1.88 +    ("tactic", simple_args (P.position Args.name) tactic, "ML tactic as proof method"),
    1.89 +    ("raw_tactic", simple_args (P.position Args.name) raw_tactic,
    1.90        "ML tactic as raw proof method")]));
    1.91  
    1.92  
    1.93 -(* outer parser *)
    1.94 -
    1.95 -structure T = OuterLex;
    1.96 -structure P = OuterParse;
    1.97 -
    1.98 -fun is_symid_meth s =
    1.99 -  s <> "|" andalso s <> "?" andalso s <> "+" andalso T.is_sid s;
   1.100 -
   1.101 -local
   1.102 -
   1.103 -fun meth4 x =
   1.104 - (P.position (P.xname >> rpair []) >> (Source o Args.src) ||
   1.105 -  P.$$$ "(" |-- P.!!! (meth0 --| P.$$$ ")")) x
   1.106 -and meth3 x =
   1.107 - (meth4 --| P.$$$ "?" >> Try ||
   1.108 -  meth4 --| P.$$$ "+" >> Repeat1 ||
   1.109 -  meth4 -- (P.$$$ "[" |-- Scan.optional P.nat 1 --| P.$$$ "]") >> (SelectGoals o swap) ||
   1.110 -  meth4) x
   1.111 -and meth2 x =
   1.112 - (P.position (P.xname -- P.generic_args1 is_symid_meth) >> (Source o Args.src) ||
   1.113 -  meth3) x
   1.114 -and meth1 x = (P.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
   1.115 -and meth0 x = (P.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
   1.116 -
   1.117 -in val parse = meth3 end;
   1.118 -
   1.119 -
   1.120 -(* args parser *)
   1.121 -
   1.122 -local
   1.123 -
   1.124 -fun enum1 sep scan = scan ::: Scan.repeat (Args.$$$ sep |-- scan);
   1.125 -
   1.126 -fun meth4 x =
   1.127 - (Args.position (Args.name >> rpair []) >> (Source o Args.src) ||
   1.128 -  Args.$$$ "(" |-- Args.!!! (meth0 --| Args.$$$ ")")) x
   1.129 -and meth3 x =
   1.130 - (meth4 --| Args.$$$ "?" >> Try ||
   1.131 -  meth4 --| Args.$$$ "+" >> Repeat1 ||
   1.132 -  meth4 -- (Args.$$$ "[" |-- Scan.optional Args.nat 1 --| Args.$$$ "]") >> (SelectGoals o swap) ||
   1.133 -  meth4) x
   1.134 -and meth2 x =
   1.135 - (Args.position (Args.name -- Args.generic_args1 is_symid_meth) >> (Source o Args.src) ||
   1.136 -  meth3) x
   1.137 -and meth1 x = (enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
   1.138 -and meth0 x = (enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
   1.139 -
   1.140 -in val parse_args = meth3 end;
   1.141 -
   1.142 -
   1.143  (*final declarations of this structure!*)
   1.144  val unfold = unfold_meth;
   1.145  val fold = fold_meth;