(* Title: Pure/Isar/args.ML
ID: $Id$
Author: Markus Wenzel, TU Muenchen
Concrete argument syntax (of attributes and methods).
*)
signature ARGS =
sig
type T
val val_of: T -> string
val pos_of: T -> Position.T
val str_of: T -> string
val ident: string * Position.T -> T
val string: string * Position.T -> T
val keyword: string * Position.T -> T
val stopper: T * (T -> bool)
val not_eof: T -> bool
val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
val !!! : (T list -> 'a) -> T list -> 'a
val $$$ : string -> T list -> string * T list
val name: T list -> string * T list
val nat: T list -> int * T list
val var: T list -> indexname * T list
val enum1: string -> (T list -> 'a * T list) -> T list -> 'a list * T list
val enum: string -> (T list -> 'a * T list) -> T list -> 'a list * T list
val list1: (T list -> 'a * T list) -> T list -> 'a list * T list
val list: (T list -> 'a * T list) -> T list -> 'a list * T list
val global_typ: theory * T list -> typ * (theory * T list)
val global_term: theory * T list -> term * (theory * T list)
val global_prop: theory * T list -> term * (theory * T list)
val global_term_pat: theory * T list -> term * (theory * T list)
val global_prop_pat: theory * T list -> term * (theory * T list)
val local_typ: Proof.context * T list -> typ * (Proof.context * T list)
val local_term: Proof.context * T list -> term * (Proof.context * T list)
val local_prop: Proof.context * T list -> term * (Proof.context * T list)
val local_term_pat: Proof.context * T list -> term * (Proof.context * T list)
val local_prop_pat: Proof.context * T list -> term * (Proof.context * T list)
type src
val src: (string * T list) * Position.T -> src
val dest_src: src -> (string * T list) * Position.T
val attribs: T list -> src list * T list
val opt_attribs: T list -> src list * T list
val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> 'a -> src -> 'a * 'b
end;
structure Args: ARGS =
struct
(** datatype T **)
datatype kind = Ident | String | Keyword | EOF;
datatype T = Arg of kind * (string * Position.T);
fun val_of (Arg (_, (x, _))) = x;
fun pos_of (Arg (_, (_, pos))) = pos;
fun str_of (Arg (Ident, (x, _))) = enclose "'" "'" x
| str_of (Arg (String, (x, _))) = quote x
| str_of (Arg (Keyword, (x, _))) = x
| str_of (Arg (EOF, _)) = "end-of-text";
fun arg kind x_pos = Arg (kind, x_pos);
val ident = arg Ident;
val string = arg String;
val keyword = arg Keyword;
(* eof *)
val eof = arg EOF ("", Position.none);
fun is_eof (Arg (EOF, _)) = true
| is_eof _ = false;
val stopper = (eof, is_eof);
val not_eof = not o is_eof;
(** scanners **)
(* position *)
fun position scan = (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap;
(* cut *)
fun !!! scan =
let
fun get_pos [] = " (past end-of-text!)"
| get_pos (Arg (_, (_, pos)) :: _) = Position.str_of pos;
fun err (args, None) = "Argument syntax error" ^ get_pos args
| err (args, Some msg) = "Argument syntax error" ^ get_pos args ^ ": " ^ msg;
in Scan.!! err scan end;
(* basic *)
fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
fun $$$ x = $$$$ x >> val_of;
val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
fun kind f = Scan.one (K true) :--
(fn Arg (Ident, (x, _)) =>
(case f x of Some y => Scan.succeed y | _ => Scan.fail)
| _ => Scan.fail) >> #2;
val nat = kind Syntax.read_nat;
val var = kind (apsome #1 o try Term.dest_Var o Syntax.read_var);
(* enumerations *)
fun enum1 sep scan = scan -- Scan.repeat ($$$ sep |-- scan) >> op ::;
fun enum sep scan = enum1 sep scan || Scan.succeed [];
fun list1 scan = enum1 "," scan;
fun list scan = enum "," scan;
(* terms and types *)
fun gen_item read = Scan.depend (fn st => name >> (pair st o read st));
val global_typ = gen_item (ProofContext.read_typ o ProofContext.init);
val global_term = gen_item (ProofContext.read_term o ProofContext.init);
val global_prop = gen_item (ProofContext.read_prop o ProofContext.init);
val global_term_pat = gen_item (ProofContext.read_term_pat o ProofContext.init);
val global_prop_pat = gen_item (ProofContext.read_prop_pat o ProofContext.init);
val local_typ = gen_item ProofContext.read_typ;
val local_term = gen_item ProofContext.read_term;
val local_prop = gen_item ProofContext.read_prop;
val local_term_pat = gen_item ProofContext.read_term_pat;
val local_prop_pat = gen_item ProofContext.read_prop_pat;
(* args *)
val exclude = explode "(){}[],";
fun atom_arg blk = Scan.one (fn Arg (k, (x, _)) =>
k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ",");
fun paren_args l r scan = $$$$ l -- !!! (scan true -- $$$$ r)
>> (fn (x, (ys, z)) => x :: ys @ [z]);
fun args blk x = Scan.optional (args1 blk) [] x
and args1 blk x =
((Scan.repeat1
(Scan.repeat1 (atom_arg blk) ||
paren_args "(" ")" args ||
paren_args "{" "}" args ||
paren_args "[" "]" args)) >> flat) x;
(** type src **)
datatype src = Src of (string * T list) * Position.T;
val src = Src;
fun dest_src (Src src) = src;
fun err_in_src kind msg (Src ((s, args), pos)) =
error (kind ^ " " ^ s ^ Position.str_of pos ^ ": " ^ msg ^ "\n " ^
space_implode " " (map str_of args));
(* argument syntax *)
fun syntax kind scan st (src as Src ((s, args), pos)) =
(case handle_error (Scan.error (Scan.finite' stopper (Scan.option scan))) (st, args) of
OK (Some x, (st', [])) => (st', x)
| OK (_, (_, args')) => err_in_src kind "bad arguments" (Src ((s, args'), pos))
| Error msg => err_in_src kind ("\n" ^ msg) src);
(* attribs *)
val attrib = position (name -- !!! (args false)) >> src;
val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
val opt_attribs = Scan.optional attribs [];
end;