obua@19093: (* Title: HOL/Import/scan.ML obua@19089: Author: Sebastian Skalberg, TU Muenchen / Steven Obua, TU Muenchen obua@19089: obua@19089: Scanner combinators for sequences. obua@19089: *) obua@19089: obua@19089: signature SCANNER = obua@19089: sig obua@19089: obua@19089: include SCANNER_SEQ obua@19089: obua@19089: exception SyntaxError obua@19089: obua@19089: type ('a,'b) scanner = 'a seq -> 'b * 'a seq obua@19089: obua@19089: val :-- : ('a,'b) scanner * ('b -> ('a,'c) scanner) wenzelm@32960: -> ('a,'b*'c) scanner obua@19089: val -- : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b*'c) scanner obua@19089: val >> : ('a,'b) scanner * ('b -> 'c) -> ('a,'c) scanner obua@19089: val --| : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b) scanner obua@19089: val |-- : ('a,'b) scanner * ('a,'c) scanner -> ('a,'c) scanner obua@19089: val ^^ : ('a,string) scanner * ('a,string) scanner wenzelm@32960: -> ('a,string) scanner obua@19089: val || : ('a,'b) scanner * ('a,'b) scanner -> ('a,'b) scanner obua@19089: val one : ('a -> bool) -> ('a,'a) scanner obua@19089: val anyone : ('a,'a) scanner obua@19089: val succeed : 'b -> ('a,'b) scanner obua@19089: val any : ('a -> bool) -> ('a,'a list) scanner obua@19089: val any1 : ('a -> bool) -> ('a,'a list) scanner obua@19089: val optional : ('a,'b) scanner -> 'b -> ('a,'b) scanner obua@19089: val option : ('a,'b) scanner -> ('a,'b option) scanner obua@19089: val repeat : ('a,'b) scanner -> ('a,'b list) scanner obua@19089: val repeat1 : ('a,'b) scanner -> ('a,'b list) scanner obua@19089: val repeat_fixed : int -> ('a, 'b) scanner -> ('a, 'b list) scanner obua@19089: val ahead : ('a,'b) scanner -> ('a,'b) scanner obua@19089: val unless : ('a, 'b) scanner -> ('a,'c) scanner -> ('a,'c) scanner obua@19089: val $$ : ''a -> (''a,''a) scanner obua@19089: val !! : ('a seq -> string) -> ('a,'b) scanner -> ('a,'b) scanner obua@19089: obua@19089: val scan_id : (string, string) scanner obua@19089: val scan_nat : (string, int) scanner obua@19089: obua@19089: val this : ''a list -> (''a, ''a list) scanner obua@19089: val this_string : string -> (string, string) scanner obua@19089: end obua@19089: obua@19089: functor Scanner (structure Seq : SCANNER_SEQ) : SCANNER = obua@19089: struct obua@19089: obua@19089: infix 7 |-- --| obua@19089: infix 5 :-- -- ^^ obua@19089: infix 3 >> obua@19089: infix 0 || obua@19089: obua@19089: exception SyntaxError obua@19089: exception Fail of string obua@19089: obua@19089: type 'a seq = 'a Seq.seq obua@19089: type ('a,'b) scanner = 'a seq -> 'b * 'a seq obua@19089: obua@19089: val pull = Seq.pull obua@19089: obua@19089: fun (sc1 :-- sc2) toks = obua@19089: let wenzelm@32960: val (x,toks2) = sc1 toks wenzelm@32960: val (y,toks3) = sc2 x toks2 obua@19089: in wenzelm@32960: ((x,y),toks3) obua@19089: end obua@19089: obua@19089: fun (sc1 -- sc2) toks = obua@19089: let wenzelm@32960: val (x,toks2) = sc1 toks wenzelm@32960: val (y,toks3) = sc2 toks2 obua@19089: in wenzelm@32960: ((x,y),toks3) obua@19089: end obua@19089: obua@19089: fun (sc >> f) toks = obua@19089: let wenzelm@32960: val (x,toks2) = sc toks obua@19089: in wenzelm@32960: (f x,toks2) obua@19089: end obua@19089: obua@19089: fun (sc1 --| sc2) toks = obua@19089: let wenzelm@32960: val (x,toks2) = sc1 toks wenzelm@32960: val (_,toks3) = sc2 toks2 obua@19089: in wenzelm@32960: (x,toks3) obua@19089: end obua@19089: obua@19089: fun (sc1 |-- sc2) toks = obua@19089: let wenzelm@32960: val (_,toks2) = sc1 toks obua@19089: in wenzelm@32960: sc2 toks2 obua@19089: end obua@19089: obua@19089: fun (sc1 ^^ sc2) toks = obua@19089: let wenzelm@32960: val (x,toks2) = sc1 toks wenzelm@32960: val (y,toks3) = sc2 toks2 obua@19089: in wenzelm@32960: (x^y,toks3) obua@19089: end obua@19089: obua@19089: fun (sc1 || sc2) toks = obua@19089: (sc1 toks) obua@19089: handle SyntaxError => sc2 toks obua@19089: obua@19089: fun anyone toks = case pull toks of NONE => raise SyntaxError | SOME x => x obua@19089: obua@19089: fun one p toks = case anyone toks of x as (t, toks) => if p t then x else raise SyntaxError obua@19089: obua@19089: fun succeed e toks = (e,toks) obua@19089: obua@19089: fun any p toks = obua@19089: case pull toks of wenzelm@32960: NONE => ([],toks) obua@19089: | SOME(x,toks2) => if p x wenzelm@32960: then wenzelm@32960: let wenzelm@32960: val (xs,toks3) = any p toks2 wenzelm@32960: in wenzelm@32960: (x::xs,toks3) wenzelm@32960: end wenzelm@32960: else ([],toks) obua@19089: obua@19089: fun any1 p toks = obua@19089: let wenzelm@32960: val (x,toks2) = one p toks wenzelm@32960: val (xs,toks3) = any p toks2 obua@19089: in wenzelm@32960: (x::xs,toks3) obua@19089: end obua@19089: obua@19089: fun optional sc def = sc || succeed def obua@19089: fun option sc = (sc >> SOME) || succeed NONE obua@19089: obua@19089: (* obua@19089: fun repeat sc = obua@19089: let wenzelm@32960: fun R toks = wenzelm@32960: let wenzelm@32960: val (x,toks2) = sc toks wenzelm@32960: val (xs,toks3) = R toks2 wenzelm@32960: in wenzelm@32960: (x::xs,toks3) wenzelm@32960: end wenzelm@32960: handle SyntaxError => ([],toks) obua@19089: in wenzelm@32960: R obua@19089: end obua@19089: *) obua@19089: obua@19089: (* A tail-recursive version of repeat. It is (ever so) slightly slower obua@19089: * than the above, non-tail-recursive version (due to the garbage generation obua@19089: * associated with the reversal of the list). However, this version will be obua@19089: * able to process input where the former version must give up (due to stack obua@19089: * overflow). The slowdown seems to be around the one percent mark. obua@19089: *) obua@19089: fun repeat sc = obua@19089: let wenzelm@32960: fun R xs toks = wenzelm@32960: case SOME (sc toks) handle SyntaxError => NONE of wenzelm@32960: SOME (x,toks2) => R (x::xs) toks2 wenzelm@32960: | NONE => (List.rev xs,toks) obua@19089: in wenzelm@32960: R [] obua@19089: end obua@19089: obua@19089: fun repeat1 sc toks = obua@19089: let wenzelm@32960: val (x,toks2) = sc toks wenzelm@32960: val (xs,toks3) = repeat sc toks2 obua@19089: in wenzelm@32960: (x::xs,toks3) obua@19089: end obua@19089: obua@19089: fun repeat_fixed n sc = obua@19089: let wenzelm@32960: fun R n xs toks = wenzelm@32960: if (n <= 0) then (List.rev xs, toks) wenzelm@32960: else case (sc toks) of (x, toks2) => R (n-1) (x::xs) toks2 obua@19089: in wenzelm@32960: R n [] obua@19089: end obua@19089: obua@19089: fun ahead (sc:'a->'b*'a) toks = (#1 (sc toks),toks) obua@19089: obua@19089: fun unless test sc toks = obua@19089: let wenzelm@32960: val test_failed = (test toks;false) handle SyntaxError => true obua@19089: in wenzelm@32960: if test_failed wenzelm@32960: then sc toks wenzelm@32960: else raise SyntaxError obua@19089: end obua@19089: obua@19089: fun $$ arg = one (fn x => x = arg) obua@19089: obua@19089: fun !! f sc toks = (sc toks wenzelm@32960: handle SyntaxError => raise Fail (f toks)) obua@19089: obua@19089: val scan_id = one Symbol.is_letter ^^ (any Symbol.is_letdig >> implode); obua@19089: obua@19089: val nat_of_list = the o Int.fromString o implode obua@19089: obua@19089: val scan_nat = repeat1 (one Symbol.is_digit) >> nat_of_list obua@19089: obua@19089: fun this [] = (fn toks => ([], toks)) obua@19089: | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs' obua@19089: obua@19089: fun this_string s = this (explode s) >> K s obua@19089: obua@19089: end obua@19089: