src/Pure/Syntax/lexicon.ML
changeset 164 43506f0a98ae
parent 18 c9ec452ff08f
child 237 a7d3e712767a
equal deleted inserted replaced
163:ad90d96c2ec3 164:43506f0a98ae
     6 *)
     6 *)
     7 
     7 
     8 infix 5 -- ^^;
     8 infix 5 -- ^^;
     9 infix 3 >>;
     9 infix 3 >>;
    10 infix 0 ||;
    10 infix 0 ||;
       
    11 
       
    12 signature SCANNER =
       
    13 sig
       
    14   exception LEXICAL_ERROR
       
    15   val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
       
    16   val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
       
    17   val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
       
    18   val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
       
    19   val $$ : ''a -> ''a list -> ''a * ''a list
       
    20   val scan_empty: 'a list -> 'b list * 'a list
       
    21   val scan_one: ('a -> bool) -> 'a list -> 'a * 'a list
       
    22   val scan_any: ('a -> bool) -> 'a list -> 'a list * 'a list
       
    23   val scan_any1: ('a -> bool) -> 'a list -> 'a list * 'a list
       
    24   val scan_end: 'a list -> 'b list * 'a list
       
    25   val optional: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
       
    26   val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
       
    27   val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
       
    28 end;
    11 
    29 
    12 signature LEXICON0 =
    30 signature LEXICON0 =
    13 sig
    31 sig
    14   val is_identifier: string -> bool
    32   val is_identifier: string -> bool
    15   val string_of_vname: indexname -> string
    33   val string_of_vname: indexname -> string
    17   val scan_var: string -> term
    35   val scan_var: string -> term
    18 end;
    36 end;
    19 
    37 
    20 signature LEXICON =
    38 signature LEXICON =
    21 sig
    39 sig
       
    40   include SCANNER
    22   include LEXICON0
    41   include LEXICON0
    23   val is_xid: string -> bool
    42   val is_xid: string -> bool
    24   val is_tfree: string -> bool
    43   val is_tfree: string -> bool
    25   type lexicon
    44   type lexicon
    26   datatype token =
    45   datatype token =
    42   val is_terminal: string -> bool
    61   val is_terminal: string -> bool
    43   val empty_lexicon: lexicon
    62   val empty_lexicon: lexicon
    44   val extend_lexicon: lexicon -> string list -> lexicon
    63   val extend_lexicon: lexicon -> string list -> lexicon
    45   val mk_lexicon: string list -> lexicon
    64   val mk_lexicon: string list -> lexicon
    46   val tokenize: lexicon -> bool -> string -> token list
    65   val tokenize: lexicon -> bool -> string -> token list
    47 
       
    48   exception LEXICAL_ERROR
       
    49   val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
       
    50   val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
       
    51   val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
       
    52   val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
       
    53   val $$ : ''a -> ''a list -> ''a * ''a list
       
    54   val scan_empty: 'a list -> 'b list * 'a list
       
    55   val scan_one: ('a -> bool) -> 'a list -> 'a * 'a list
       
    56   val scan_any: ('a -> bool) -> 'a list -> 'a list * 'a list
       
    57   val scan_any1: ('a -> bool) -> 'a list -> 'a list * 'a list
       
    58   val scan_end: 'a list -> 'b list * 'a list
       
    59   val optional: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
       
    60   val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
       
    61   val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
       
    62 end;
    66 end;
    63 
    67 
    64 functor LexiconFun(): LEXICON =
    68 functor LexiconFun(): LEXICON =
    65 struct
    69 struct
    66 
    70 
   252 
   256 
   253 fun scan_one _ [] = raise LEXICAL_ERROR
   257 fun scan_one _ [] = raise LEXICAL_ERROR
   254   | scan_one pred (c :: cs) =
   258   | scan_one pred (c :: cs) =
   255       if pred c then (c, cs) else raise LEXICAL_ERROR;
   259       if pred c then (c, cs) else raise LEXICAL_ERROR;
   256 
   260 
   257 val scan_any = take_prefix;
   261 fun scan_any _ [] = ([], [])
       
   262   | scan_any pred (chs as c :: cs) =
       
   263       if pred c then apfst (cons c) (scan_any pred cs)
       
   264       else ([], chs);
   258 
   265 
   259 fun scan_any1 pred = scan_one pred -- scan_any pred >> op ::;
   266 fun scan_any1 pred = scan_one pred -- scan_any pred >> op ::;
   260 
   267 
   261 fun scan_rest cs = (cs, []);
   268 fun scan_rest cs = (cs, []);
   262 
   269