src/Pure/Isar/args.ML
author wenzelm
Mon Nov 16 11:02:07 1998 +0100 (1998-11-16)
changeset 5878 769abc29bb8e
parent 5822 3f824514ad88
child 5911 7da8033264fa
permissions -rw-r--r--
several args parsers;
include positions;
misc tuning;
     1 (*  Title:      Pure/Isar/args.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Concrete argument syntax (of attributes and methods).
     6 *)
     7 
     8 signature ARGS =
     9 sig
    10   type T
    11   val val_of: T -> string
    12   val pos_of: T -> Position.T
    13   val str_of: T -> string
    14   val ident: string * Position.T -> T
    15   val string: string * Position.T -> T
    16   val keyword: string * Position.T -> T
    17   val stopper: T * (T -> bool)
    18   val not_eof: T -> bool
    19   val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
    20   val !!! : (T list -> 'a) -> T list -> 'a
    21   val $$$ : string -> T list -> string * T list
    22   val name: T list -> string * T list
    23   val nat: T list -> int * T list
    24   val var: T list -> indexname * T list
    25   val enum1: string -> (T list -> 'a * T list) -> T list -> 'a list * T list
    26   val enum: string -> (T list -> 'a * T list) -> T list -> 'a list * T list
    27   val list1: (T list -> 'a * T list) -> T list -> 'a list * T list
    28   val list: (T list -> 'a * T list) -> T list -> 'a list * T list
    29   val global_typ: theory * T list -> typ * (theory * T list)
    30   val global_term: theory * T list -> term * (theory * T list)
    31   val global_prop: theory * T list -> term * (theory * T list)
    32   val global_pat: theory * T list -> term * (theory * T list)
    33   val local_typ: Proof.context * T list -> typ * (Proof.context * T list)
    34   val local_term: Proof.context * T list -> term * (Proof.context * T list)
    35   val local_prop: Proof.context * T list -> term * (Proof.context * T list)
    36   val local_pat: Proof.context * T list -> term * (Proof.context * T list)
    37   type src
    38   val src: (string * T list) * Position.T -> src
    39   val dest_src: src -> (string * T list) * Position.T
    40   val attribs: T list -> src list * T list
    41   val opt_attribs: T list -> src list * T list
    42   val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> 'a -> src -> 'a * 'b
    43 end;
    44 
    45 structure Args: ARGS =
    46 struct
    47 
    48 
    49 (** datatype T **)
    50 
    51 datatype kind = Ident | String | Keyword | EOF;
    52 datatype T = Arg of kind * (string * Position.T);
    53 
    54 fun val_of (Arg (_, (x, _))) = x;
    55 fun pos_of (Arg (_, (_, pos))) = pos;
    56 
    57 fun str_of (Arg (Ident, (x, _))) = enclose "'" "'" x
    58   | str_of (Arg (String, (x, _))) = quote x
    59   | str_of (Arg (Keyword, (x, _))) = x
    60   | str_of (Arg (EOF, _)) = "end-of-text";
    61 
    62 fun arg kind x_pos = Arg (kind, x_pos);
    63 val ident = arg Ident;
    64 val string = arg String;
    65 val keyword = arg Keyword;
    66 
    67 
    68 (* eof *)
    69 
    70 val eof = arg EOF ("", Position.none);
    71 
    72 fun is_eof (Arg (EOF, _)) = true
    73   | is_eof _ = false;
    74 
    75 val stopper = (eof, is_eof);
    76 val not_eof = not o is_eof;
    77 
    78 
    79 
    80 (** scanners **)
    81 
    82 (* position *)
    83 
    84 fun position scan = (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap;
    85 
    86 
    87 (* cut *)
    88 
    89 fun !!! scan =
    90   let
    91     fun get_pos [] = " (past end-of-text!)"
    92       | get_pos (Arg (_, (_, pos)) :: _) = Position.str_of pos;
    93 
    94     fun err (args, None) = "Argument syntax error" ^ get_pos args
    95       | err (args, Some msg) = "Argument syntax error" ^ get_pos args ^ ": " ^ msg;
    96   in Scan.!! err scan end;
    97 
    98 
    99 (* basic *)
   100 
   101 fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
   102 fun $$$ x = $$$$ x >> val_of;
   103 
   104 val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
   105 
   106 fun kind f = Scan.one (K true) :--
   107   (fn Arg (Ident, (x, _)) =>
   108     (case f x of Some y => Scan.succeed y | _ => Scan.fail)
   109   | _ => Scan.fail) >> #2;
   110 
   111 val nat = kind Syntax.read_nat;
   112 val var = kind (apsome #1 o try Term.dest_Var o Syntax.read_var);
   113 
   114 
   115 (* enumerations *)
   116 
   117 fun enum1 sep scan = scan -- Scan.repeat ($$$ sep |-- scan) >> op ::;
   118 fun enum sep scan = enum1 sep scan || Scan.succeed [];
   119 
   120 fun list1 scan = enum1 "," scan;
   121 fun list scan = enum "," scan;
   122 
   123 
   124 (* terms and types *)
   125 
   126 fun gen_item read = Scan.depend (fn st => name >> (pair st o read st));
   127 
   128 val global_typ = gen_item (ProofContext.read_typ o ProofContext.init);
   129 val global_term = gen_item (ProofContext.read_term o ProofContext.init);
   130 val global_prop = gen_item (ProofContext.read_prop o ProofContext.init);
   131 val global_pat = gen_item (ProofContext.read_pat o ProofContext.init);
   132 
   133 val local_typ = gen_item ProofContext.read_typ;
   134 val local_term = gen_item ProofContext.read_term;
   135 val local_prop = gen_item ProofContext.read_prop;
   136 val local_pat = gen_item ProofContext.read_pat;
   137 
   138 
   139 (* args *)
   140 
   141 val exclude = explode "(){}[],";
   142 
   143 fun atom_arg blk = Scan.one (fn Arg (k, (x, _)) =>
   144   k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ",");
   145 
   146 fun paren_args l r scan = $$$$ l -- !!! (scan true -- $$$$ r)
   147   >> (fn (x, (ys, z)) => x :: ys @ [z]);
   148 
   149 fun args blk x = Scan.optional (args1 blk) [] x
   150 and args1 blk x =
   151   ((Scan.repeat1
   152     (Scan.repeat1 (atom_arg blk) ||
   153       paren_args "(" ")" args ||
   154       paren_args "{" "}" args ||
   155       paren_args "[" "]" args)) >> flat) x;
   156 
   157 
   158 
   159 (** type src **)
   160 
   161 datatype src = Src of (string * T list) * Position.T;
   162 
   163 val src = Src;
   164 fun dest_src (Src src) = src;
   165 
   166 fun err_in_src kind msg (Src ((s, args), pos)) =
   167   error (kind ^ " " ^ s ^ Position.str_of pos ^ ": " ^ msg ^ "\n  " ^
   168     space_implode " " (map str_of args));
   169 
   170 
   171 (* argument syntax *)
   172 
   173 (* FIXME *)
   174 fun trace_src kind (Src ((s, args), pos)) =
   175   warning ("TRACE: " ^ space_implode " " (kind :: s :: map str_of args) ^ Position.str_of pos);
   176 
   177 fun syntax kind scan st (src as Src ((s, args), pos)) =
   178   (trace_src kind src;
   179   (case handle_error (Scan.error (Scan.finite' stopper (Scan.option scan))) (st, args) of
   180     OK (Some x, (st', [])) => (st', x)
   181   | OK (_, (_, args')) => err_in_src kind "bad arguments" (Src ((s, args'), pos))
   182   | Error msg => err_in_src kind ("\n" ^ msg) src));
   183 
   184 
   185 (* attribs *)
   186 
   187 val attrib = position (name -- !!! (args false)) >> src;
   188 val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
   189 val opt_attribs = Scan.optional attribs [];
   190 
   191 
   192 end;