src/Pure/Isar/args.ML
author ballarin
Fri Aug 29 15:19:02 2003 +0200 (2003-08-29)
changeset 14174 f3cafd2929d5
parent 11503 4c25eef6f325
child 14563 4bf2d10461f3
permissions -rw-r--r--
Methods rule_tac etc support static (Isar) contexts.
     1 (*  Title:      Pure/Isar/args.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Concrete argument syntax (of attributes and methods).
     7 *)
     8 
     9 signature ARGS =
    10 sig
    11   type T
    12   val val_of: T -> string
    13   val pos_of: T -> Position.T
    14   val str_of: T -> string
    15   val string_of: T -> string
    16   val ident: string * Position.T -> T
    17   val string: string * Position.T -> T
    18   val keyword: string * Position.T -> T
    19   val stopper: T * (T -> bool)
    20   val not_eof: T -> bool
    21   val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
    22   val !!! : (T list -> 'a) -> T list -> 'a
    23   val $$$ : string -> T list -> string * T list
    24   val add: T list -> string * T list
    25   val del: T list -> string * T list
    26   val colon: T list -> string * T list
    27   val query: T list -> string * T list
    28   val bang: T list -> string * T list
    29   val query_colon: T list -> string * T list
    30   val bang_colon: T list -> string * T list
    31   val parens: (T list -> 'a * T list) -> T list -> 'a * T list
    32   val bracks: (T list -> 'a * T list) -> T list -> 'a * T list
    33   val mode: string -> 'a * T list -> bool * ('a * T list)
    34   val name: T list -> string * T list
    35   val name_dummy: T list -> string option * T list
    36   val nat: T list -> int * T list
    37   val int: T list -> int * T list
    38   val var: T list -> indexname * T list
    39   val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    40   val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    41   val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    42   val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    43   val global_typ_no_norm: theory * T list -> typ * (theory * T list)
    44   val global_typ: theory * T list -> typ * (theory * T list)
    45   val global_term: theory * T list -> term * (theory * T list)
    46   val global_prop: theory * T list -> term * (theory * T list)
    47   val local_typ_no_norm: Proof.context * T list -> typ * (Proof.context * T list)
    48   val local_typ: Proof.context * T list -> typ * (Proof.context * T list)
    49   val local_term: Proof.context * T list -> term * (Proof.context * T list)
    50   val local_prop: Proof.context * T list -> term * (Proof.context * T list)
    51   val bang_facts: Proof.context * T list -> thm list * (Proof.context * T list)
    52   val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
    53     -> ((int -> tactic) -> tactic) * ('a * T list)
    54   type src
    55   val src: (string * T list) * Position.T -> src
    56   val dest_src: src -> (string * T list) * Position.T
    57   val attribs: T list -> src list * T list
    58   val opt_attribs: T list -> src list * T list
    59   val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> src -> 'a -> 'a * 'b
    60 end;
    61 
    62 structure Args: ARGS =
    63 struct
    64 
    65 
    66 (** datatype T **)
    67 
    68 datatype kind = Ident | String | Keyword | EOF;
    69 datatype T = Arg of kind * (string * Position.T);
    70 
    71 fun val_of (Arg (_, (x, _))) = x;
    72 fun pos_of (Arg (_, (_, pos))) = pos;
    73 
    74 fun str_of (Arg (Ident, (x, _))) = x
    75   | str_of (Arg (String, (x, _))) = quote x
    76   | str_of (Arg (Keyword, (x, _))) = x
    77   | str_of (Arg (EOF, _)) = "end-of-text";
    78 
    79 fun string_of (Arg (Ident, (x, _))) = x
    80   | string_of (Arg (String, (x, _))) = quote x
    81   | string_of (Arg (Keyword, (x, _))) = x
    82   | string_of (Arg (EOF, _)) = "";
    83 
    84 fun arg kind x_pos = Arg (kind, x_pos);
    85 val ident = arg Ident;
    86 val string = arg String;
    87 val keyword = arg Keyword;
    88 
    89 
    90 (* eof *)
    91 
    92 val eof = arg EOF ("", Position.none);
    93 
    94 fun is_eof (Arg (EOF, _)) = true
    95   | is_eof _ = false;
    96 
    97 val stopper = (eof, is_eof);
    98 val not_eof = not o is_eof;
    99 
   100 
   101 
   102 (** scanners **)
   103 
   104 (* position *)
   105 
   106 fun position scan = (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap;
   107 
   108 
   109 (* cut *)
   110 
   111 fun !!! scan =
   112   let
   113     fun get_pos [] = " (past end-of-text!)"
   114       | get_pos (Arg (_, (_, pos)) :: _) = Position.str_of pos;
   115 
   116     fun err (args, None) = "Argument syntax error" ^ get_pos args
   117       | err (args, Some msg) = "Argument syntax error" ^ get_pos args ^ ": " ^ msg;
   118   in Scan.!! err scan end;
   119 
   120 
   121 (* basic *)
   122 
   123 fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
   124 fun $$$ x = $$$$ x >> val_of;
   125 
   126 val add = $$$ "add";
   127 val del = $$$ "del";
   128 val colon = $$$ ":";
   129 val query = $$$ "?";
   130 val bang = $$$ "!";
   131 val query_colon = $$$ "?:";
   132 val bang_colon = $$$ "!:";
   133 
   134 fun parens scan = $$$ "(" |-- scan --| $$$ ")";
   135 fun bracks scan = $$$ "[" |-- scan --| $$$ "]";
   136 fun mode s = Scan.lift (Scan.optional (parens ($$$$ s) >> K true) false);
   137 
   138 val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
   139 val name_dummy = $$$ "_" >> K None || name >> Some;
   140 
   141 val keyword_symid =
   142   Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;
   143 
   144 fun kind f = Scan.one (K true) :--
   145   ((fn Arg (Ident, (x, _)) =>
   146     (case f x of Some y => Scan.succeed y | _ => Scan.fail)
   147   | _ => Scan.fail)
   148 (* o (fn (t as Arg (i, (s, _))) =>
   149   (warning (
   150     (case i of Ident => "Ident: " | String => "String: "
   151             | Keyword => "Keyword: " | EOF => "EOF: ")
   152     ^ s); t)) *) ) >> #2;
   153 
   154 val nat = kind Syntax.read_nat;
   155 val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
   156 
   157 (* Read variable name.  Leading `?' may be omitted if name contains no dot. *)
   158 val var = kind (apsome #1 o
   159       (fn s => (Some (Term.dest_Var (Syntax.read_var s)))
   160          handle _ => (Some (Term.dest_Var (Syntax.read_var ("?" ^ s))))
   161          handle _ => None));
   162 
   163 (* enumerations *)
   164 
   165 fun enum1 sep scan = scan -- Scan.repeat (Scan.lift ($$$ sep) |-- scan) >> op ::;
   166 fun enum sep scan = enum1 sep scan || Scan.succeed [];
   167 
   168 fun and_list1 scan = enum1 "and" scan;
   169 fun and_list scan = enum "and" scan;
   170 
   171 
   172 (* terms and types *)
   173 
   174 fun gen_item read = Scan.depend (fn st => name >> (pair st o read st));
   175 
   176 val global_typ_no_norm = gen_item (ProofContext.read_typ_no_norm o ProofContext.init);
   177 val global_typ = gen_item (ProofContext.read_typ o ProofContext.init);
   178 val global_term = gen_item (ProofContext.read_term o ProofContext.init);
   179 val global_prop = gen_item (ProofContext.read_prop o ProofContext.init);
   180 
   181 val local_typ_no_norm = gen_item ProofContext.read_typ_no_norm;
   182 val local_typ = gen_item ProofContext.read_typ;
   183 val local_term = gen_item ProofContext.read_term;
   184 val local_prop = gen_item ProofContext.read_prop;
   185 
   186 
   187 (* bang facts *)
   188 
   189 val bang_facts = Scan.depend (fn ctxt =>
   190   ($$$ "!" >> K (ProofContext.prems_of ctxt) || Scan.succeed []) >> pair ctxt);
   191 
   192 
   193 (* goal specification *)
   194 
   195 (* range *)
   196 
   197 val from_to =
   198   nat -- ($$$$ "-" |-- nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
   199   nat --| $$$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
   200   nat >> (fn i => fn tac => tac i) ||
   201   $$$$ "!" >> K ALLGOALS;
   202 
   203 val goal = $$$$ "[" |-- !!! (from_to --| $$$$ "]");
   204 fun goal_spec def = Scan.lift (Scan.optional goal def);
   205 
   206 
   207 (* args *)
   208 
   209 val exclude = explode "()[],";
   210 
   211 fun atom_arg blk = Scan.one (fn Arg (k, (x, _)) =>
   212   k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ",");
   213 
   214 fun paren_args l r scan = $$$$ l -- !!! (scan true -- $$$$ r)
   215   >> (fn (x, (ys, z)) => x :: ys @ [z]);
   216 
   217 fun args blk x = Scan.optional (args1 blk) [] x
   218 and args1 blk x =
   219   ((Scan.repeat1
   220     (Scan.repeat1 (atom_arg blk) ||
   221       paren_args "(" ")" args ||
   222       paren_args "[" "]" args)) >> flat) x;
   223 
   224 
   225 
   226 (** type src **)
   227 
   228 datatype src = Src of (string * T list) * Position.T;
   229 
   230 val src = Src;
   231 fun dest_src (Src src) = src;
   232 
   233 fun err_in_src kind msg (Src ((s, args), pos)) =
   234   error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": " ^ msg ^ "\n  " ^
   235     space_implode " " (map str_of args));
   236 
   237 
   238 (* argument syntax *)
   239 
   240 fun syntax kind scan (src as Src ((s, args), pos)) st =
   241   (case Scan.error (Scan.finite' stopper (Scan.option scan)) (st, args) of
   242     (Some x, (st', [])) => (st', x)
   243   | (_, (_, args')) => err_in_src kind "bad arguments" (Src ((s, args'), pos)));
   244 
   245 
   246 (* attribs *)
   247 
   248 fun list1 scan = scan -- Scan.repeat ($$$ "," |-- scan) >> op ::;
   249 fun list scan = list1 scan || Scan.succeed [];
   250 
   251 val attrib = position ((keyword_symid || name) -- !!! (args false)) >> src;
   252 val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
   253 val opt_attribs = Scan.optional attribs [];
   254 
   255 
   256 end;