# HG changeset patch # User wenzelm # Date 916227873 -3600 # Node ID 8ba2f25610f70f3d8e709a8f5d76478404352c1a # Parent c70bce7deb0f8d9c6900826a15c3655afbb2163b files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General; diff -r c70bce7deb0f -r 8ba2f25610f7 src/Pure/General/README --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/README Wed Jan 13 12:44:33 1999 +0100 @@ -0,0 +1,20 @@ + + Pure/General/ + + +This directory contains general purpose modules, all of which are +exported. + + TableFun (generic tables) + Symtab (tables indexed by strings) + Object (generic objects of arbitrary type) + Seq (unbounded sequences) + NameSpace (hierarchically structured name spaces) + Position (input positions) + Path (abstract algebra of file paths) + File (file system operations) + History (histories of values, with undo and redo) + Scan (generic scanner toolbox) + Source (co-algebraic data sources) + Symbol (generalized characters) + Pretty (generic pretty printing module) diff -r c70bce7deb0f -r 8ba2f25610f7 src/Pure/General/ROOT.ML --- a/src/Pure/General/ROOT.ML Wed Jan 13 12:16:34 1999 +0100 +++ b/src/Pure/General/ROOT.ML Wed Jan 13 12:44:33 1999 +0100 @@ -12,6 +12,10 @@ use "path.ML"; use "file.ML"; use "history.ML"; +use "scan.ML"; +use "source.ML"; +use "symbol.ML"; +use "pretty.ML"; structure PureGeneral = struct @@ -23,4 +27,8 @@ structure Path = Path; structure File = File; structure History = History; + structure Scan = Scan; + structure Source = Source; + structure Symbol = Symbol; + structure Pretty = Pretty; end; diff -r c70bce7deb0f -r 8ba2f25610f7 src/Pure/General/pretty.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/pretty.ML Wed Jan 13 12:44:33 1999 +0100 @@ -0,0 +1,249 @@ +(* Title: Pure/Syntax/pretty.ML + ID: $Id$ + Author: Lawrence C Paulson + Copyright 1991 University of Cambridge + +Generic pretty printing module. + +Loosely based on + D. C. Oppen, "Pretty Printing", + ACM Transactions on Programming Languages and Systems (1980), 465-483. + +The object to be printed is given as a tree with indentation and line +breaking information. A "break" inserts a newline if the text until +the next break is too long to fit on the current line. After the newline, +text is indented to the level of the enclosing block. Normally, if a block +is broken then all enclosing blocks will also be broken. Only "inconsistent +breaks" are provided. + +The stored length of a block is used in breakdist (to treat each inner block as +a unit for breaking). +*) + +type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) * + (unit -> unit) * (unit -> unit); + +signature PRETTY = + sig + type T + val str: string -> T + val strlen: string -> int -> T + val sym: string -> T + val spc: int -> T + val brk: int -> T + val fbrk: T + val blk: int * T list -> T + val lst: string * string -> T list -> T + val quote: T -> T + val commas: T list -> T list + val breaks: T list -> T list + val fbreaks: T list -> T list + val block: T list -> T + val strs: string list -> T + val enclose: string -> string -> T list -> T + val list: string -> string -> T list -> T + val str_list: string -> string -> string list -> T + val big_list: string -> T list -> T + val string_of: T -> string + val writeln: T -> unit + val str_of: T -> string + val pprint: T -> pprint_args -> unit + val setdepth: int -> unit + val setmargin: int -> unit + end; + +structure Pretty : PRETTY = +struct + +(*printing items: compound phrases, strings, and breaks*) +datatype T = + Block of T list * int * int | (*body, indentation, length*) + String of string * int | (*text, length*) + Break of bool * int; (*mandatory flag, width if not taken*); + +(*Add the lengths of the expressions until the next Break; if no Break then + include "after", to account for text following this block. *) +fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after) + | breakdist (String (s, len) :: es, after) = len + breakdist (es, after) + | breakdist (Break _ :: es, after) = 0 + | breakdist ([], after) = after; + +fun repstring a 0 = "" + | repstring a 1 = a + | repstring a k = + if k mod 2 = 0 then repstring(a^a) (k div 2) + else repstring(a^a) (k div 2) ^ a; + +(*** Type for lines of text: string, # of lines, position on line ***) + +type text = {tx: string, nl: int, pos: int}; + +val emptytext = {tx="", nl=0, pos=0}; + +fun blanks wd {tx,nl,pos} = + {tx = tx ^ repstring " " wd, + nl = nl, + pos = pos+wd}; + +fun newline {tx,nl,pos} = + {tx = tx ^ "\n", + nl = nl+1, + pos = 0}; + +fun string s len {tx,nl,pos:int} = + {tx = tx ^ s, + nl = nl, + pos = pos + len}; + + +(*** Formatting ***) + +(* margin *) + +(*example values*) +val margin = ref 80 (*right margin, or page width*) +and breakgain = ref 4 (*minimum added space required of a break*) +and emergencypos = ref 40; (*position too far to right*) + +fun setmargin m = + (margin := m; + breakgain := !margin div 20; + emergencypos := !margin div 2); + +val () = setmargin 76; + + +(*Search for the next break (at this or higher levels) and force it to occur*) +fun forcenext [] = [] + | forcenext (Break(_,wd) :: es) = Break(true,0) :: es + | forcenext (e :: es) = e :: forcenext es; + +(*es is list of expressions to print; + blockin is the indentation of the current block; + after is the width of the following context until next break. *) +fun format ([], _, _) text = text + | format (e::es, blockin, after) (text as {pos,nl,...}) = + (case e of + Block(bes,indent,wd) => + let val blockin' = (pos + indent) mod !emergencypos + val btext = format(bes, blockin', breakdist(es,after)) text + (*If this block was broken then force the next break.*) + val es2 = if nl < #nl(btext) then forcenext es else es + in format (es2,blockin,after) btext end + | String (s, len) => format (es,blockin,after) (string s len text) + | Break(force,wd) => (*no break if text to next break fits on this line + or if breaking would add only breakgain to space *) + format (es,blockin,after) + (if not force andalso + pos+wd <= Int.max(!margin - breakdist(es,after), + blockin + !breakgain) + then blanks wd text (*just insert wd blanks*) + else blanks blockin (newline text))); + + +(*** Exported functions to create formatting expressions ***) + +fun length (Block (_, _, len)) = len + | length (String (_, len)) = len + | length (Break(_, wd)) = wd; + +fun str s = String (s, size s); +fun strlen s len = String (s, len); +fun sym s = String (s, Symbol.size s); + +fun spc n = str (repstring " " n); + +fun brk wd = Break (false, wd); +val fbrk = Break (true, 0); + +fun blk (indent, es) = + let + fun sum([], k) = k + | sum(e :: es, k) = sum (es, length e + k); + in Block (es, indent, sum (es, 0)) end; + +(*Join the elements of es as a comma-separated list, bracketted by lp and rp*) +fun lst(lp,rp) es = + let fun add(e,es) = str"," :: brk 1 :: e :: es; + fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp]) + | list(e::[]) = [str lp, e, str rp] + | list([]) = [] + in blk(size lp, list es) end; + + +(* utils *) + +fun quote prt = + blk (1, [str "\"", prt, str "\""]); + +fun commas prts = + flat (separate [str ",", brk 1] (map (fn x => [x]) prts)); + +fun breaks prts = separate (brk 1) prts; + +fun fbreaks prts = separate fbrk prts; + +fun block prts = blk (2, prts); + +val strs = block o breaks o (map str); + +fun enclose lpar rpar prts = + block (str lpar :: (prts @ [str rpar])); + +fun list lpar rpar prts = + enclose lpar rpar (commas prts); + +fun str_list lpar rpar strs = + list lpar rpar (map str strs); + +fun big_list name prts = + block (fbreaks (str name :: prts)); + + + +(*** Pretty printing with depth limitation ***) + +val depth = ref 0; (*maximum depth; 0 means no limit*) + +fun setdepth dp = (depth := dp); + +(*Recursively prune blocks, discarding all text exceeding depth dp*) +fun pruning dp (Block(bes,indent,wd)) = + if dp>0 then blk(indent, map (pruning(dp-1)) bes) + else str "..." + | pruning dp e = e; + +fun prune dp e = if dp>0 then pruning dp e else e; + + +fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext); + +val writeln = writeln o string_of; + + +(*Create a single flat string: no line breaking*) +fun str_of prt = + let + fun s_of (Block (prts, _, _)) = implode (map s_of prts) + | s_of (String (s, _)) = s + | s_of (Break (false, wd)) = repstring " " wd + | s_of (Break (true, _)) = " "; + in + s_of (prune (! depth) prt) + end; + +(*Part of the interface to the Poly/ML and New Jersey ML pretty printers*) +fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) = + let + fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ()) + | pp (String (s, _)) = put_str s + | pp (Break (false, wd)) = put_brk wd + | pp (Break (true, _)) = put_fbrk () + and pp_lst [] = () + | pp_lst (prt :: prts) = (pp prt; pp_lst prts); + in + pp (prune (! depth) prt) + end; + + +end; diff -r c70bce7deb0f -r 8ba2f25610f7 src/Pure/General/scan.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/scan.ML Wed Jan 13 12:44:33 1999 +0100 @@ -0,0 +1,305 @@ +(* Title: Pure/Syntax/scan.ML + ID: $Id$ + Author: Markus Wenzel and Tobias Nipkow, TU Muenchen + +Generic scanners (for potentially infinite input). +*) + +infix 5 -- :-- |-- --| ^^; +infix 3 >>; +infix 0 ||; + +signature BASIC_SCAN = +sig + val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b + val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c + val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b + val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e + val :-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e + val |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e + val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e + val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c + val $$ : ''a -> ''a list -> ''a * ''a list +end; + +signature SCAN = +sig + include BASIC_SCAN + val fail: 'a -> 'b + val fail_with: ('a -> string) -> 'a -> 'b + val succeed: 'a -> 'b -> 'a * 'b + val one: ('a -> bool) -> 'a list -> 'a * 'a list + val any: ('a -> bool) -> 'a list -> 'a list * 'a list + val any1: ('a -> bool) -> 'a list -> 'a list * 'a list + val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a + val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a + val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a + val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a + val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b + val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a + val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd + val first: ('a -> 'b) list -> 'a -> 'b + val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e) + val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c) + val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e + val try: ('a -> 'b) -> 'a -> 'b + val force: ('a -> 'b) -> 'a -> 'b + val prompt: string -> ('a -> 'b) -> 'a -> 'b + val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list)) + -> 'b * 'a list -> 'c * ('d * 'a list) + val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list + val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option + val catch: ('a -> 'b) -> 'a -> 'b + val error: ('a -> 'b) -> 'a -> 'b + val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) -> + 'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) -> + ('d * 'b list -> 'f * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c) + val source: string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) -> + 'b * ('b -> bool) -> ('b list -> 'd list * 'b list) -> + ('b list -> 'e * 'b list) option -> 'a -> 'd list * 'c + val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a + val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a + type lexicon + val dest_lexicon: lexicon -> string list list + val make_lexicon: string list list -> lexicon + val empty_lexicon: lexicon + val extend_lexicon: lexicon -> string list list -> lexicon + val merge_lexicons: lexicon -> lexicon -> lexicon + val literal: lexicon -> string list -> string list * string list +end; + +structure Scan: SCAN = +struct + + +(** scanners **) + +exception MORE of string option; (*need more input (prompt)*) +exception FAIL of string option; (*try alternatives (reason of failure)*) +exception ABORT of string; (*dead end*) + + +(* scanner combinators *) + +fun (scan >> f) xs = apfst f (scan xs); + +fun (scan1 || scan2) xs = scan1 xs handle FAIL _ => scan2 xs; + +(*dependent pairing*) +fun (scan1 :-- scan2) xs = + let + val (x, ys) = scan1 xs; + val (y, zs) = scan2 x ys; + in ((x, y), zs) end; + +fun (scan1 -- scan2) = scan1 :-- (fn _ => scan2); +fun (scan1 |-- scan2) = scan1 -- scan2 >> #2; +fun (scan1 --| scan2) = scan1 -- scan2 >> #1; +fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^; + + +(* generic scanners *) + +fun fail _ = raise FAIL None; +fun fail_with msg_of xs = raise FAIL (Some (msg_of xs)); +fun succeed y xs = (y, xs); + +fun one _ [] = raise MORE None + | one pred (x :: xs) = + if pred x then (x, xs) else raise FAIL None; + +fun $$ _ [] = raise MORE None + | $$ a (x :: xs) = + if a = x then (x, xs) else raise FAIL None; + +fun any _ [] = raise MORE None + | any pred (lst as x :: xs) = + if pred x then apfst (cons x) (any pred xs) + else ([], lst); + +fun any1 pred = one pred -- any pred >> op ::; + +fun optional scan def = scan || succeed def; +fun option scan = optional (scan >> Some) None; + +fun repeat scan xs = (scan -- repeat scan >> op :: || succeed []) xs; +fun repeat1 scan = scan -- repeat scan >> op ::; + +fun max leq scan1 scan2 xs = + (case (option scan1 xs, option scan2 xs) of + ((None, _), (None, _)) => raise FAIL None (*looses FAIL msg!*) + | ((Some tok1, xs'), (None, _)) => (tok1, xs') + | ((None, _), (Some tok2, xs')) => (tok2, xs') + | ((Some tok1, xs1'), (Some tok2, xs2')) => + if leq (tok2, tok1) then (tok1, xs1') else (tok2, xs2')); + +fun ahead scan xs = (fst (scan xs), xs); + +fun unless test scan = + ahead (option test) :-- (fn None => scan | _ => fail) >> #2; + +fun first [] = fail + | first (scan :: scans) = scan || first scans; + + +(* state based scanners *) + +fun depend scan (st, xs) = + let val ((st', y), xs') = scan st xs + in (y, (st', xs')) end; + +fun lift scan (st, xs) = + let val (y, xs') = scan xs + in (y, (st, xs')) end; + +fun pass st scan xs = + let val (y, (_, xs')) = scan (st, xs) + in (y, xs') end; + + +(* exception handling *) + +fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg)); +fun try scan xs = scan xs handle MORE _ => raise FAIL None | ABORT _ => raise FAIL None; +fun force scan xs = scan xs handle MORE _ => raise FAIL None; +fun prompt str scan xs = scan xs handle MORE None => raise MORE (Some str); +fun catch scan xs = scan xs handle ABORT msg => raise FAIL (Some msg); +fun error scan xs = scan xs handle ABORT msg => Library.error msg; + + +(* finite scans *) + +fun finite' (stopper, is_stopper) scan (state, input) = + let + fun lost () = raise ABORT "Scanner bug: lost stopper of finite scan!"; + + fun stop [] = lost () + | stop lst = + let val (xs, x) = split_last lst + in if is_stopper x then ((), xs) else lost () end; + in + if exists is_stopper input then + raise ABORT "Stopper may not occur in input of finite scan!" + else (force scan --| lift stop) (state, input @ [stopper]) + end; + +fun finite stopper scan xs = + let val (y, ((), xs')) = finite' stopper (lift scan) ((), xs) + in (y, xs') end; + +fun read stopper scan xs = + (case error (finite stopper (option scan)) xs of + (y as Some _, []) => y + | _ => None); + + + +(* infinite scans -- draining state-based source *) + +fun drain def_prmpt get stopper scan ((state, xs), src) = + (scan (state, xs), src) handle MORE prmpt => + (case get (if_none prmpt def_prmpt) src of + ([], _) => (finite' stopper scan (state, xs), src) + | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src')); + +fun source' def_prmpt get unget stopper scanner opt_recover (state, src) = + let + fun drain_with scan = drain def_prmpt get stopper scan; + + fun drain_loop recover inp = + drain_with (catch scanner) inp handle FAIL msg => + (error_msg (if_none msg "Syntax error."); + drain_loop recover (apfst snd (drain_with recover inp))); + + val ((ys, (state', xs')), src') = + (case (get def_prmpt src, opt_recover) of + (([], s), _) => (([], (state, [])), s) + | ((xs, s), None) => drain_with (error scanner) ((state, xs), s) + | ((xs, s), Some scan) => drain_loop scan ((state, xs), s)); + in + (ys, (state', unget (xs', src'))) + end; + +fun source def_prmpt get unget stopper scan opt_recover src = + let val (ys, ((), src')) = + source' def_prmpt get unget stopper (lift scan) (apsome lift opt_recover) ((), src) + in (ys, src') end; + +fun single scan = scan >> (fn x => [x]); +fun bulk scan = scan -- repeat (try scan) >> (op ::); + + + +(** datatype lexicon **) + +datatype lexicon = + Empty | + Branch of string * string list * lexicon * lexicon * lexicon; + +val no_literal = []; + + +(* dest_lexicon *) + +fun dest_lexicon Empty = [] + | dest_lexicon (Branch (_, [], lt, eq, gt)) = + dest_lexicon lt @ dest_lexicon eq @ dest_lexicon gt + | dest_lexicon (Branch (_, cs, lt, eq, gt)) = + dest_lexicon lt @ [cs] @ dest_lexicon eq @ dest_lexicon gt; + + +(* empty, extend, make, merge lexicons *) + +val empty_lexicon = Empty; + +fun extend_lexicon lexicon chrss = + let + fun ext (lex, chrs) = + let + fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) = + if c < d then Branch (d, a, add lt chs, eq, gt) + else if c > d then Branch (d, a, lt, eq, add gt chs) + else Branch (d, if null cs then chrs else a, lt, add eq cs, gt) + | add Empty [c] = + Branch (c, chrs, Empty, Empty, Empty) + | add Empty (c :: cs) = + Branch (c, no_literal, Empty, add Empty cs, Empty) + | add lex [] = lex; + in add lex chrs end; + in foldl ext (lexicon, chrss \\ dest_lexicon lexicon) end; + +val make_lexicon = extend_lexicon empty_lexicon; + +fun merge_lexicons lex1 lex2 = + let + val chss1 = dest_lexicon lex1; + val chss2 = dest_lexicon lex2; + in + if chss2 subset chss1 then lex1 + else if chss1 subset chss2 then lex2 + else extend_lexicon lex1 chss2 + end; + + +(* scan literal *) + +fun literal lex chrs = + let + fun lit Empty res _ = res + | lit (Branch _) _ [] = raise MORE None + | lit (Branch (d, a, lt, eq, gt)) res (chs as c :: cs) = + if c < d then lit lt res chs + else if c > d then lit gt res chs + else lit eq (if a = no_literal then res else Some (a, cs)) cs; + in + (case lit lex None chrs of + None => raise FAIL None + | Some res => res) + end; + + +end; + + +structure BasicScan: BASIC_SCAN = Scan; +open BasicScan; diff -r c70bce7deb0f -r 8ba2f25610f7 src/Pure/General/source.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/source.ML Wed Jan 13 12:44:33 1999 +0100 @@ -0,0 +1,150 @@ +(* Title: Pure/Syntax/source.ML + ID: $Id$ + Author: Markus Wenzel, TU Muenchen + +Co-algebraic data sources. +*) + +signature SOURCE = +sig + type ('a, 'b) source + val set_prompt: string -> ('a, 'b) source -> ('a, 'b) source + val get: ('a, 'b) source -> 'a list * ('a, 'b) source + val unget: 'a list * ('a, 'b) source -> ('a, 'b) source + val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option + val exhaust: ('a, 'b) source -> 'a list + val mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source + val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source + val of_list: 'a list -> ('a, 'a list) source + val of_string: string -> (string, string list) source + val of_file: string -> (string, string list) source + val decorate_prompt_fn: (string -> string) ref + val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source + val tty: (string, unit) source + val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) -> + ('a * 'b list -> 'd * ('a * 'b list)) option -> + ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source + val source: 'a * ('a -> bool) -> ('a list -> 'b list * 'a list) -> + ('a list -> 'c * 'a list) option -> + ('a, 'd) source -> ('b, ('a, 'd) source) source +end; + +structure Source: SOURCE = +struct + + +(** datatype source **) + +datatype ('a, 'b) source = + Source of + {buffer: 'a list, + info: 'b, + prompt: string, + drain: string -> 'b -> 'a list * 'b}; + +fun make_source buffer info prompt drain = + Source {buffer = buffer, info = info, prompt = prompt, drain = drain}; + + +(* prompt *) + +val default_prompt = "> "; + +fun set_prompt prompt (Source {buffer, info, prompt = _, drain}) = + make_source buffer info prompt drain; + + +(* get / unget *) + +fun get (Source {buffer = [], info, prompt, drain}) = + let val (xs, info') = drain prompt info + in (xs, make_source [] info' prompt drain) end + | get (Source {buffer, info, prompt, drain}) = + (buffer, make_source [] info prompt drain); + +fun unget (xs, Source {buffer, info, prompt, drain}) = + make_source (xs @ buffer) info prompt drain; + + +(* variations on get *) + +fun get_prompt prompt src = get (set_prompt prompt src); + +fun get_single src = + (case get src of + ([], _) => None + | (x :: xs, src') => Some (x, unget (xs, src'))); + +fun exhaust src = + (case get src of + ([], _) => [] + | (xs, src') => xs @ exhaust src'); + + +(* (map)filter *) + +fun drain_mapfilter f prompt src = + let + val (xs, src') = get_prompt prompt src; + val xs' = Library.mapfilter f xs; + in + if null xs orelse not (null xs') then (xs', src') + else drain_mapfilter f prompt src' + end; + +fun mapfilter f src = make_source [] src default_prompt (drain_mapfilter f); +fun filter pred = mapfilter (fn x => if pred x then Some x else None); + + + +(** build sources **) + +(* list source *) + +(*limiting the input buffer considerably improves performance*) +val limit = 4000; + +fun drain_list _ xs = (take (limit, xs), drop (limit, xs)); + +fun of_list xs = make_source [] xs default_prompt drain_list; +val of_string = of_list o explode; +val of_file = of_string o File.read; + + +(* stream source *) + +val decorate_prompt_fn = ref (fn s:string => s); + +fun drain_stream instream outstream prompt () = + (TextIO.output (outstream, ! decorate_prompt_fn prompt); + TextIO.flushOut outstream; + (explode (TextIO.inputLine instream), ())); + +fun of_stream instream outstream = + make_source [] () default_prompt (drain_stream instream outstream); + +val tty = of_stream TextIO.stdIn TextIO.stdOut; + + + +(** compose sources **) + +fun drain_source source stopper scan recover prompt src = + source prompt get_prompt unget stopper scan recover src; + + +(* state-based *) + +fun source' init_state stopper scan recover src = + make_source [] (init_state, src) default_prompt + (drain_source Scan.source' stopper scan recover); + + +(* non state-based *) + +fun source stopper scan recover src = + make_source [] src default_prompt + (drain_source Scan.source stopper scan recover); + + +end; diff -r c70bce7deb0f -r 8ba2f25610f7 src/Pure/General/symbol.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/symbol.ML Wed Jan 13 12:44:33 1999 +0100 @@ -0,0 +1,274 @@ +(* Title: Pure/Syntax/symbol.ML + ID: $Id$ + Author: Markus Wenzel, TU Muenchen + +Generalized characters. +*) + +signature SYMBOL = +sig + type symbol + val space: symbol + val eof: symbol + val is_eof: symbol -> bool + val not_eof: symbol -> bool + val stopper: symbol * (symbol -> bool) + val is_ascii: symbol -> bool + val is_letter: symbol -> bool + val is_digit: symbol -> bool + val is_quasi_letter: symbol -> bool + val is_letdig: symbol -> bool + val is_blank: symbol -> bool + val is_printable: symbol -> bool + val beginning: symbol list -> string + val scan: string list -> symbol * string list + val explode: string -> symbol list + val length: symbol list -> int + val size: string -> int + val input: string -> string + val output: string -> string + val source: bool -> (string, 'a) Source.source -> + (symbol, (string, 'a) Source.source) Source.source +end; + +structure Symbol: SYMBOL = +struct + + +(** encoding table (isabelle-0) **) + +val enc_start = 160; +val enc_end = 255; + +val enc_vector = +[ +(* GENERATED TEXT FOLLOWS - Do not edit! *) + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\", + "\\" +(* END OF GENERATED TEXT *) +]; + +val enc_rel = enc_vector ~~ map chr (enc_start upto enc_end); + +val char_tab = Symtab.make enc_rel; +val symbol_tab = Symtab.make (map swap enc_rel); + +fun lookup_symbol c = + if ord c < enc_start then None + else Symtab.lookup (symbol_tab, c); + + +(* encode / decode *) + +fun char s = if_none (Symtab.lookup (char_tab, s)) s; +fun symbol c = if_none (lookup_symbol c) c; + +fun symbol' c = + (case lookup_symbol c of + None => c + | Some s => "\\" ^ s); + + + +(** type symbol **) + +type symbol = string; + +val space = " "; +val eof = ""; + + +(* kinds *) + +fun is_eof s = s = eof; +fun not_eof s = s <> eof; +val stopper = (eof, is_eof); + +fun is_ascii s = size s = 1 andalso ord s < 128; + +fun is_letter s = + size s = 1 andalso + (ord "A" <= ord s andalso ord s <= ord "Z" orelse + ord "a" <= ord s andalso ord s <= ord "z"); + +fun is_digit s = + size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9"; + +fun is_quasi_letter "_" = true + | is_quasi_letter "'" = true + | is_quasi_letter s = is_letter s; + +val is_blank = + fn " " => true | "\t" => true | "\n" => true | "\^L" => true + | "\160" => true | "\\" => true + | _ => false; + +val is_letdig = is_quasi_letter orf is_digit; + +fun is_printable s = + size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse + size s > 2 andalso nth_elem (2, explode s) <> "^"; + + +(* beginning *) + +val smash_blanks = map (fn s => if is_blank s then space else s); + +fun beginning raw_ss = + let + val (all_ss, _) = take_suffix is_blank raw_ss; + val dots = if length all_ss > 10 then " ..." else ""; + val (ss, _) = take_suffix is_blank (take (10, all_ss)); + in implode (smash_blanks ss) ^ dots end; + + +(* scan *) + +val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode); + +val scan = + ($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^ + !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs) + (Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") || + Scan.one not_eof; + + +(* source *) + +val recover = Scan.any1 ((not o is_blank) andf not_eof); + +fun source do_recover src = + Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src; + + +(* explode *) + +fun no_syms [] = true + | no_syms ("\\" :: "<" :: _) = false + | no_syms (c :: cs) = ord c < enc_start andalso no_syms cs; + +fun sym_explode str = + let val chs = explode str in + if no_syms chs then chs (*tune trivial case*) + else map symbol (the (Scan.read stopper (Scan.repeat scan) chs)) + end; + + +(* printable length *) + +fun sym_length ss = foldl (fn (n, c) => if is_printable c then n + 1 else n) (0, ss); +val sym_size = sym_length o sym_explode; + + +(* input / output *) + +fun input str = + let val chs = explode str in + if forall (fn c => ord c < enc_start) chs then str + else implode (map symbol' chs) + end; + +val output = implode o map char o sym_explode; + + +(*final declarations of this structure!*) +val explode = sym_explode; +val length = sym_length; +val size = sym_size; + + +end; diff -r c70bce7deb0f -r 8ba2f25610f7 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Wed Jan 13 12:16:34 1999 +0100 +++ b/src/Pure/IsaMakefile Wed Jan 13 12:44:33 1999 +0100 @@ -25,7 +25,8 @@ $(OUT)/Pure: General/ROOT.ML General/file.ML General/history.ML \ General/name_space.ML General/object.ML General/path.ML \ - General/position.ML General/seq.ML General/table.ML Isar/ROOT.ML \ + General/position.ML General/pretty.ML General/scan.ML General/seq.ML \ + General/source.ML General/symbol.ML General/table.ML Isar/ROOT.ML \ Isar/args.ML Isar/attrib.ML Isar/isar.ML Isar/isar_cmd.ML \ Isar/isar_syn.ML Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \ Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \ @@ -33,12 +34,11 @@ Isar/toplevel.ML ML-Systems/mlworks.ML ML-Systems/polyml.ML \ ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML \ Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \ - Syntax/pretty.ML Syntax/printer.ML Syntax/scan.ML Syntax/source.ML \ - Syntax/symbol.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \ - Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML \ - Thy/ROOT.ML Thy/browser_info.ML Thy/context.ML Thy/thm_database.ML \ - Thy/thy_info.ML Thy/thy_parse.ML Thy/thy_read.ML Thy/thy_scan.ML \ - Thy/thy_syn.ML Thy/use.ML axclass.ML basis.ML deriv.ML display.ML \ + Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \ + Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML Thy/ROOT.ML \ + Thy/browser_info.ML Thy/context.ML Thy/thm_database.ML Thy/thy_info.ML \ + Thy/thy_parse.ML Thy/thy_read.ML Thy/thy_scan.ML Thy/thy_syn.ML \ + Thy/use.ML axclass.ML basis.ML deriv.ML display.ML \ drule.ML envir.ML goals.ML install_pp.ML library.ML locale.ML \ logic.ML net.ML object_logic.ML pattern.ML pure.ML pure_thy.ML \ search.ML sign.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML \ diff -r c70bce7deb0f -r 8ba2f25610f7 src/Pure/Syntax/README --- a/src/Pure/Syntax/README Wed Jan 13 12:16:34 1999 +0100 +++ b/src/Pure/Syntax/README Wed Jan 13 12:44:33 1999 +0100 @@ -4,12 +4,7 @@ This directory contains the source files for Isabelle's syntax module, which includes a lexer, parser, pretty printer and macro system. Note -that only the following structures are supposed to be exported: - - Pretty (generic pretty printing module) - Scan (generic scanner toolbox) - Source (co-algebraic data sources) - Symbol (generalized characters) +that only the following structures are exported: Syntax (internal interface to the syntax module) BasicSyntax (part of Syntax made pervasive) diff -r c70bce7deb0f -r 8ba2f25610f7 src/Pure/Syntax/ROOT.ML --- a/src/Pure/Syntax/ROOT.ML Wed Jan 13 12:16:34 1999 +0100 +++ b/src/Pure/Syntax/ROOT.ML Wed Jan 13 12:44:33 1999 +0100 @@ -5,13 +5,6 @@ This file builds the syntax module. *) -(*generic modules*) -use "scan.ML"; -use "source.ML"; -use "symbol.ML"; -use "pretty.ML"; - -(*actual syntax module*) use "lexicon.ML"; use "token_trans.ML"; use "ast.ML"; diff -r c70bce7deb0f -r 8ba2f25610f7 src/Pure/Syntax/pretty.ML --- a/src/Pure/Syntax/pretty.ML Wed Jan 13 12:16:34 1999 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,249 +0,0 @@ -(* Title: Pure/Syntax/pretty.ML - ID: $Id$ - Author: Lawrence C Paulson - Copyright 1991 University of Cambridge - -Generic pretty printing module. - -Loosely based on - D. C. Oppen, "Pretty Printing", - ACM Transactions on Programming Languages and Systems (1980), 465-483. - -The object to be printed is given as a tree with indentation and line -breaking information. A "break" inserts a newline if the text until -the next break is too long to fit on the current line. After the newline, -text is indented to the level of the enclosing block. Normally, if a block -is broken then all enclosing blocks will also be broken. Only "inconsistent -breaks" are provided. - -The stored length of a block is used in breakdist (to treat each inner block as -a unit for breaking). -*) - -type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) * - (unit -> unit) * (unit -> unit); - -signature PRETTY = - sig - type T - val str: string -> T - val strlen: string -> int -> T - val sym: string -> T - val spc: int -> T - val brk: int -> T - val fbrk: T - val blk: int * T list -> T - val lst: string * string -> T list -> T - val quote: T -> T - val commas: T list -> T list - val breaks: T list -> T list - val fbreaks: T list -> T list - val block: T list -> T - val strs: string list -> T - val enclose: string -> string -> T list -> T - val list: string -> string -> T list -> T - val str_list: string -> string -> string list -> T - val big_list: string -> T list -> T - val string_of: T -> string - val writeln: T -> unit - val str_of: T -> string - val pprint: T -> pprint_args -> unit - val setdepth: int -> unit - val setmargin: int -> unit - end; - -structure Pretty : PRETTY = -struct - -(*printing items: compound phrases, strings, and breaks*) -datatype T = - Block of T list * int * int | (*body, indentation, length*) - String of string * int | (*text, length*) - Break of bool * int; (*mandatory flag, width if not taken*); - -(*Add the lengths of the expressions until the next Break; if no Break then - include "after", to account for text following this block. *) -fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after) - | breakdist (String (s, len) :: es, after) = len + breakdist (es, after) - | breakdist (Break _ :: es, after) = 0 - | breakdist ([], after) = after; - -fun repstring a 0 = "" - | repstring a 1 = a - | repstring a k = - if k mod 2 = 0 then repstring(a^a) (k div 2) - else repstring(a^a) (k div 2) ^ a; - -(*** Type for lines of text: string, # of lines, position on line ***) - -type text = {tx: string, nl: int, pos: int}; - -val emptytext = {tx="", nl=0, pos=0}; - -fun blanks wd {tx,nl,pos} = - {tx = tx ^ repstring " " wd, - nl = nl, - pos = pos+wd}; - -fun newline {tx,nl,pos} = - {tx = tx ^ "\n", - nl = nl+1, - pos = 0}; - -fun string s len {tx,nl,pos:int} = - {tx = tx ^ s, - nl = nl, - pos = pos + len}; - - -(*** Formatting ***) - -(* margin *) - -(*example values*) -val margin = ref 80 (*right margin, or page width*) -and breakgain = ref 4 (*minimum added space required of a break*) -and emergencypos = ref 40; (*position too far to right*) - -fun setmargin m = - (margin := m; - breakgain := !margin div 20; - emergencypos := !margin div 2); - -val () = setmargin 76; - - -(*Search for the next break (at this or higher levels) and force it to occur*) -fun forcenext [] = [] - | forcenext (Break(_,wd) :: es) = Break(true,0) :: es - | forcenext (e :: es) = e :: forcenext es; - -(*es is list of expressions to print; - blockin is the indentation of the current block; - after is the width of the following context until next break. *) -fun format ([], _, _) text = text - | format (e::es, blockin, after) (text as {pos,nl,...}) = - (case e of - Block(bes,indent,wd) => - let val blockin' = (pos + indent) mod !emergencypos - val btext = format(bes, blockin', breakdist(es,after)) text - (*If this block was broken then force the next break.*) - val es2 = if nl < #nl(btext) then forcenext es else es - in format (es2,blockin,after) btext end - | String (s, len) => format (es,blockin,after) (string s len text) - | Break(force,wd) => (*no break if text to next break fits on this line - or if breaking would add only breakgain to space *) - format (es,blockin,after) - (if not force andalso - pos+wd <= Int.max(!margin - breakdist(es,after), - blockin + !breakgain) - then blanks wd text (*just insert wd blanks*) - else blanks blockin (newline text))); - - -(*** Exported functions to create formatting expressions ***) - -fun length (Block (_, _, len)) = len - | length (String (_, len)) = len - | length (Break(_, wd)) = wd; - -fun str s = String (s, size s); -fun strlen s len = String (s, len); -fun sym s = String (s, Symbol.size s); - -fun spc n = str (repstring " " n); - -fun brk wd = Break (false, wd); -val fbrk = Break (true, 0); - -fun blk (indent, es) = - let - fun sum([], k) = k - | sum(e :: es, k) = sum (es, length e + k); - in Block (es, indent, sum (es, 0)) end; - -(*Join the elements of es as a comma-separated list, bracketted by lp and rp*) -fun lst(lp,rp) es = - let fun add(e,es) = str"," :: brk 1 :: e :: es; - fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp]) - | list(e::[]) = [str lp, e, str rp] - | list([]) = [] - in blk(size lp, list es) end; - - -(* utils *) - -fun quote prt = - blk (1, [str "\"", prt, str "\""]); - -fun commas prts = - flat (separate [str ",", brk 1] (map (fn x => [x]) prts)); - -fun breaks prts = separate (brk 1) prts; - -fun fbreaks prts = separate fbrk prts; - -fun block prts = blk (2, prts); - -val strs = block o breaks o (map str); - -fun enclose lpar rpar prts = - block (str lpar :: (prts @ [str rpar])); - -fun list lpar rpar prts = - enclose lpar rpar (commas prts); - -fun str_list lpar rpar strs = - list lpar rpar (map str strs); - -fun big_list name prts = - block (fbreaks (str name :: prts)); - - - -(*** Pretty printing with depth limitation ***) - -val depth = ref 0; (*maximum depth; 0 means no limit*) - -fun setdepth dp = (depth := dp); - -(*Recursively prune blocks, discarding all text exceeding depth dp*) -fun pruning dp (Block(bes,indent,wd)) = - if dp>0 then blk(indent, map (pruning(dp-1)) bes) - else str "..." - | pruning dp e = e; - -fun prune dp e = if dp>0 then pruning dp e else e; - - -fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext); - -val writeln = writeln o string_of; - - -(*Create a single flat string: no line breaking*) -fun str_of prt = - let - fun s_of (Block (prts, _, _)) = implode (map s_of prts) - | s_of (String (s, _)) = s - | s_of (Break (false, wd)) = repstring " " wd - | s_of (Break (true, _)) = " "; - in - s_of (prune (! depth) prt) - end; - -(*Part of the interface to the Poly/ML and New Jersey ML pretty printers*) -fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) = - let - fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ()) - | pp (String (s, _)) = put_str s - | pp (Break (false, wd)) = put_brk wd - | pp (Break (true, _)) = put_fbrk () - and pp_lst [] = () - | pp_lst (prt :: prts) = (pp prt; pp_lst prts); - in - pp (prune (! depth) prt) - end; - - -end; diff -r c70bce7deb0f -r 8ba2f25610f7 src/Pure/Syntax/scan.ML --- a/src/Pure/Syntax/scan.ML Wed Jan 13 12:16:34 1999 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,305 +0,0 @@ -(* Title: Pure/Syntax/scan.ML - ID: $Id$ - Author: Markus Wenzel and Tobias Nipkow, TU Muenchen - -Generic scanners (for potentially infinite input). -*) - -infix 5 -- :-- |-- --| ^^; -infix 3 >>; -infix 0 ||; - -signature BASIC_SCAN = -sig - val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b - val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c - val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b - val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e - val :-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e - val |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e - val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e - val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c - val $$ : ''a -> ''a list -> ''a * ''a list -end; - -signature SCAN = -sig - include BASIC_SCAN - val fail: 'a -> 'b - val fail_with: ('a -> string) -> 'a -> 'b - val succeed: 'a -> 'b -> 'a * 'b - val one: ('a -> bool) -> 'a list -> 'a * 'a list - val any: ('a -> bool) -> 'a list -> 'a list * 'a list - val any1: ('a -> bool) -> 'a list -> 'a list * 'a list - val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a - val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a - val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a - val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a - val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b - val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a - val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd - val first: ('a -> 'b) list -> 'a -> 'b - val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e) - val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c) - val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e - val try: ('a -> 'b) -> 'a -> 'b - val force: ('a -> 'b) -> 'a -> 'b - val prompt: string -> ('a -> 'b) -> 'a -> 'b - val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list)) - -> 'b * 'a list -> 'c * ('d * 'a list) - val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list - val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option - val catch: ('a -> 'b) -> 'a -> 'b - val error: ('a -> 'b) -> 'a -> 'b - val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) -> - 'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) -> - ('d * 'b list -> 'f * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c) - val source: string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) -> - 'b * ('b -> bool) -> ('b list -> 'd list * 'b list) -> - ('b list -> 'e * 'b list) option -> 'a -> 'd list * 'c - val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a - val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a - type lexicon - val dest_lexicon: lexicon -> string list list - val make_lexicon: string list list -> lexicon - val empty_lexicon: lexicon - val extend_lexicon: lexicon -> string list list -> lexicon - val merge_lexicons: lexicon -> lexicon -> lexicon - val literal: lexicon -> string list -> string list * string list -end; - -structure Scan: SCAN = -struct - - -(** scanners **) - -exception MORE of string option; (*need more input (prompt)*) -exception FAIL of string option; (*try alternatives (reason of failure)*) -exception ABORT of string; (*dead end*) - - -(* scanner combinators *) - -fun (scan >> f) xs = apfst f (scan xs); - -fun (scan1 || scan2) xs = scan1 xs handle FAIL _ => scan2 xs; - -(*dependent pairing*) -fun (scan1 :-- scan2) xs = - let - val (x, ys) = scan1 xs; - val (y, zs) = scan2 x ys; - in ((x, y), zs) end; - -fun (scan1 -- scan2) = scan1 :-- (fn _ => scan2); -fun (scan1 |-- scan2) = scan1 -- scan2 >> #2; -fun (scan1 --| scan2) = scan1 -- scan2 >> #1; -fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^; - - -(* generic scanners *) - -fun fail _ = raise FAIL None; -fun fail_with msg_of xs = raise FAIL (Some (msg_of xs)); -fun succeed y xs = (y, xs); - -fun one _ [] = raise MORE None - | one pred (x :: xs) = - if pred x then (x, xs) else raise FAIL None; - -fun $$ _ [] = raise MORE None - | $$ a (x :: xs) = - if a = x then (x, xs) else raise FAIL None; - -fun any _ [] = raise MORE None - | any pred (lst as x :: xs) = - if pred x then apfst (cons x) (any pred xs) - else ([], lst); - -fun any1 pred = one pred -- any pred >> op ::; - -fun optional scan def = scan || succeed def; -fun option scan = optional (scan >> Some) None; - -fun repeat scan xs = (scan -- repeat scan >> op :: || succeed []) xs; -fun repeat1 scan = scan -- repeat scan >> op ::; - -fun max leq scan1 scan2 xs = - (case (option scan1 xs, option scan2 xs) of - ((None, _), (None, _)) => raise FAIL None (*looses FAIL msg!*) - | ((Some tok1, xs'), (None, _)) => (tok1, xs') - | ((None, _), (Some tok2, xs')) => (tok2, xs') - | ((Some tok1, xs1'), (Some tok2, xs2')) => - if leq (tok2, tok1) then (tok1, xs1') else (tok2, xs2')); - -fun ahead scan xs = (fst (scan xs), xs); - -fun unless test scan = - ahead (option test) :-- (fn None => scan | _ => fail) >> #2; - -fun first [] = fail - | first (scan :: scans) = scan || first scans; - - -(* state based scanners *) - -fun depend scan (st, xs) = - let val ((st', y), xs') = scan st xs - in (y, (st', xs')) end; - -fun lift scan (st, xs) = - let val (y, xs') = scan xs - in (y, (st, xs')) end; - -fun pass st scan xs = - let val (y, (_, xs')) = scan (st, xs) - in (y, xs') end; - - -(* exception handling *) - -fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg)); -fun try scan xs = scan xs handle MORE _ => raise FAIL None | ABORT _ => raise FAIL None; -fun force scan xs = scan xs handle MORE _ => raise FAIL None; -fun prompt str scan xs = scan xs handle MORE None => raise MORE (Some str); -fun catch scan xs = scan xs handle ABORT msg => raise FAIL (Some msg); -fun error scan xs = scan xs handle ABORT msg => Library.error msg; - - -(* finite scans *) - -fun finite' (stopper, is_stopper) scan (state, input) = - let - fun lost () = raise ABORT "Scanner bug: lost stopper of finite scan!"; - - fun stop [] = lost () - | stop lst = - let val (xs, x) = split_last lst - in if is_stopper x then ((), xs) else lost () end; - in - if exists is_stopper input then - raise ABORT "Stopper may not occur in input of finite scan!" - else (force scan --| lift stop) (state, input @ [stopper]) - end; - -fun finite stopper scan xs = - let val (y, ((), xs')) = finite' stopper (lift scan) ((), xs) - in (y, xs') end; - -fun read stopper scan xs = - (case error (finite stopper (option scan)) xs of - (y as Some _, []) => y - | _ => None); - - - -(* infinite scans -- draining state-based source *) - -fun drain def_prmpt get stopper scan ((state, xs), src) = - (scan (state, xs), src) handle MORE prmpt => - (case get (if_none prmpt def_prmpt) src of - ([], _) => (finite' stopper scan (state, xs), src) - | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src')); - -fun source' def_prmpt get unget stopper scanner opt_recover (state, src) = - let - fun drain_with scan = drain def_prmpt get stopper scan; - - fun drain_loop recover inp = - drain_with (catch scanner) inp handle FAIL msg => - (error_msg (if_none msg "Syntax error."); - drain_loop recover (apfst snd (drain_with recover inp))); - - val ((ys, (state', xs')), src') = - (case (get def_prmpt src, opt_recover) of - (([], s), _) => (([], (state, [])), s) - | ((xs, s), None) => drain_with (error scanner) ((state, xs), s) - | ((xs, s), Some scan) => drain_loop scan ((state, xs), s)); - in - (ys, (state', unget (xs', src'))) - end; - -fun source def_prmpt get unget stopper scan opt_recover src = - let val (ys, ((), src')) = - source' def_prmpt get unget stopper (lift scan) (apsome lift opt_recover) ((), src) - in (ys, src') end; - -fun single scan = scan >> (fn x => [x]); -fun bulk scan = scan -- repeat (try scan) >> (op ::); - - - -(** datatype lexicon **) - -datatype lexicon = - Empty | - Branch of string * string list * lexicon * lexicon * lexicon; - -val no_literal = []; - - -(* dest_lexicon *) - -fun dest_lexicon Empty = [] - | dest_lexicon (Branch (_, [], lt, eq, gt)) = - dest_lexicon lt @ dest_lexicon eq @ dest_lexicon gt - | dest_lexicon (Branch (_, cs, lt, eq, gt)) = - dest_lexicon lt @ [cs] @ dest_lexicon eq @ dest_lexicon gt; - - -(* empty, extend, make, merge lexicons *) - -val empty_lexicon = Empty; - -fun extend_lexicon lexicon chrss = - let - fun ext (lex, chrs) = - let - fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) = - if c < d then Branch (d, a, add lt chs, eq, gt) - else if c > d then Branch (d, a, lt, eq, add gt chs) - else Branch (d, if null cs then chrs else a, lt, add eq cs, gt) - | add Empty [c] = - Branch (c, chrs, Empty, Empty, Empty) - | add Empty (c :: cs) = - Branch (c, no_literal, Empty, add Empty cs, Empty) - | add lex [] = lex; - in add lex chrs end; - in foldl ext (lexicon, chrss \\ dest_lexicon lexicon) end; - -val make_lexicon = extend_lexicon empty_lexicon; - -fun merge_lexicons lex1 lex2 = - let - val chss1 = dest_lexicon lex1; - val chss2 = dest_lexicon lex2; - in - if chss2 subset chss1 then lex1 - else if chss1 subset chss2 then lex2 - else extend_lexicon lex1 chss2 - end; - - -(* scan literal *) - -fun literal lex chrs = - let - fun lit Empty res _ = res - | lit (Branch _) _ [] = raise MORE None - | lit (Branch (d, a, lt, eq, gt)) res (chs as c :: cs) = - if c < d then lit lt res chs - else if c > d then lit gt res chs - else lit eq (if a = no_literal then res else Some (a, cs)) cs; - in - (case lit lex None chrs of - None => raise FAIL None - | Some res => res) - end; - - -end; - - -structure BasicScan: BASIC_SCAN = Scan; -open BasicScan; diff -r c70bce7deb0f -r 8ba2f25610f7 src/Pure/Syntax/source.ML --- a/src/Pure/Syntax/source.ML Wed Jan 13 12:16:34 1999 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,150 +0,0 @@ -(* Title: Pure/Syntax/source.ML - ID: $Id$ - Author: Markus Wenzel, TU Muenchen - -Co-algebraic data sources. -*) - -signature SOURCE = -sig - type ('a, 'b) source - val set_prompt: string -> ('a, 'b) source -> ('a, 'b) source - val get: ('a, 'b) source -> 'a list * ('a, 'b) source - val unget: 'a list * ('a, 'b) source -> ('a, 'b) source - val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option - val exhaust: ('a, 'b) source -> 'a list - val mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source - val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source - val of_list: 'a list -> ('a, 'a list) source - val of_string: string -> (string, string list) source - val of_file: string -> (string, string list) source - val decorate_prompt_fn: (string -> string) ref - val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source - val tty: (string, unit) source - val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) -> - ('a * 'b list -> 'd * ('a * 'b list)) option -> - ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source - val source: 'a * ('a -> bool) -> ('a list -> 'b list * 'a list) -> - ('a list -> 'c * 'a list) option -> - ('a, 'd) source -> ('b, ('a, 'd) source) source -end; - -structure Source: SOURCE = -struct - - -(** datatype source **) - -datatype ('a, 'b) source = - Source of - {buffer: 'a list, - info: 'b, - prompt: string, - drain: string -> 'b -> 'a list * 'b}; - -fun make_source buffer info prompt drain = - Source {buffer = buffer, info = info, prompt = prompt, drain = drain}; - - -(* prompt *) - -val default_prompt = "> "; - -fun set_prompt prompt (Source {buffer, info, prompt = _, drain}) = - make_source buffer info prompt drain; - - -(* get / unget *) - -fun get (Source {buffer = [], info, prompt, drain}) = - let val (xs, info') = drain prompt info - in (xs, make_source [] info' prompt drain) end - | get (Source {buffer, info, prompt, drain}) = - (buffer, make_source [] info prompt drain); - -fun unget (xs, Source {buffer, info, prompt, drain}) = - make_source (xs @ buffer) info prompt drain; - - -(* variations on get *) - -fun get_prompt prompt src = get (set_prompt prompt src); - -fun get_single src = - (case get src of - ([], _) => None - | (x :: xs, src') => Some (x, unget (xs, src'))); - -fun exhaust src = - (case get src of - ([], _) => [] - | (xs, src') => xs @ exhaust src'); - - -(* (map)filter *) - -fun drain_mapfilter f prompt src = - let - val (xs, src') = get_prompt prompt src; - val xs' = Library.mapfilter f xs; - in - if null xs orelse not (null xs') then (xs', src') - else drain_mapfilter f prompt src' - end; - -fun mapfilter f src = make_source [] src default_prompt (drain_mapfilter f); -fun filter pred = mapfilter (fn x => if pred x then Some x else None); - - - -(** build sources **) - -(* list source *) - -(*limiting the input buffer considerably improves performance*) -val limit = 4000; - -fun drain_list _ xs = (take (limit, xs), drop (limit, xs)); - -fun of_list xs = make_source [] xs default_prompt drain_list; -val of_string = of_list o explode; -val of_file = of_string o File.read; - - -(* stream source *) - -val decorate_prompt_fn = ref (fn s:string => s); - -fun drain_stream instream outstream prompt () = - (TextIO.output (outstream, ! decorate_prompt_fn prompt); - TextIO.flushOut outstream; - (explode (TextIO.inputLine instream), ())); - -fun of_stream instream outstream = - make_source [] () default_prompt (drain_stream instream outstream); - -val tty = of_stream TextIO.stdIn TextIO.stdOut; - - - -(** compose sources **) - -fun drain_source source stopper scan recover prompt src = - source prompt get_prompt unget stopper scan recover src; - - -(* state-based *) - -fun source' init_state stopper scan recover src = - make_source [] (init_state, src) default_prompt - (drain_source Scan.source' stopper scan recover); - - -(* non state-based *) - -fun source stopper scan recover src = - make_source [] src default_prompt - (drain_source Scan.source stopper scan recover); - - -end; diff -r c70bce7deb0f -r 8ba2f25610f7 src/Pure/Syntax/symbol.ML --- a/src/Pure/Syntax/symbol.ML Wed Jan 13 12:16:34 1999 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,274 +0,0 @@ -(* Title: Pure/Syntax/symbol.ML - ID: $Id$ - Author: Markus Wenzel, TU Muenchen - -Generalized characters. -*) - -signature SYMBOL = -sig - type symbol - val space: symbol - val eof: symbol - val is_eof: symbol -> bool - val not_eof: symbol -> bool - val stopper: symbol * (symbol -> bool) - val is_ascii: symbol -> bool - val is_letter: symbol -> bool - val is_digit: symbol -> bool - val is_quasi_letter: symbol -> bool - val is_letdig: symbol -> bool - val is_blank: symbol -> bool - val is_printable: symbol -> bool - val beginning: symbol list -> string - val scan: string list -> symbol * string list - val explode: string -> symbol list - val length: symbol list -> int - val size: string -> int - val input: string -> string - val output: string -> string - val source: bool -> (string, 'a) Source.source -> - (symbol, (string, 'a) Source.source) Source.source -end; - -structure Symbol: SYMBOL = -struct - - -(** encoding table (isabelle-0) **) - -val enc_start = 160; -val enc_end = 255; - -val enc_vector = -[ -(* GENERATED TEXT FOLLOWS - Do not edit! *) - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\", - "\\" -(* END OF GENERATED TEXT *) -]; - -val enc_rel = enc_vector ~~ map chr (enc_start upto enc_end); - -val char_tab = Symtab.make enc_rel; -val symbol_tab = Symtab.make (map swap enc_rel); - -fun lookup_symbol c = - if ord c < enc_start then None - else Symtab.lookup (symbol_tab, c); - - -(* encode / decode *) - -fun char s = if_none (Symtab.lookup (char_tab, s)) s; -fun symbol c = if_none (lookup_symbol c) c; - -fun symbol' c = - (case lookup_symbol c of - None => c - | Some s => "\\" ^ s); - - - -(** type symbol **) - -type symbol = string; - -val space = " "; -val eof = ""; - - -(* kinds *) - -fun is_eof s = s = eof; -fun not_eof s = s <> eof; -val stopper = (eof, is_eof); - -fun is_ascii s = size s = 1 andalso ord s < 128; - -fun is_letter s = - size s = 1 andalso - (ord "A" <= ord s andalso ord s <= ord "Z" orelse - ord "a" <= ord s andalso ord s <= ord "z"); - -fun is_digit s = - size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9"; - -fun is_quasi_letter "_" = true - | is_quasi_letter "'" = true - | is_quasi_letter s = is_letter s; - -val is_blank = - fn " " => true | "\t" => true | "\n" => true | "\^L" => true - | "\160" => true | "\\" => true - | _ => false; - -val is_letdig = is_quasi_letter orf is_digit; - -fun is_printable s = - size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse - size s > 2 andalso nth_elem (2, explode s) <> "^"; - - -(* beginning *) - -val smash_blanks = map (fn s => if is_blank s then space else s); - -fun beginning raw_ss = - let - val (all_ss, _) = take_suffix is_blank raw_ss; - val dots = if length all_ss > 10 then " ..." else ""; - val (ss, _) = take_suffix is_blank (take (10, all_ss)); - in implode (smash_blanks ss) ^ dots end; - - -(* scan *) - -val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode); - -val scan = - ($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^ - !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs) - (Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") || - Scan.one not_eof; - - -(* source *) - -val recover = Scan.any1 ((not o is_blank) andf not_eof); - -fun source do_recover src = - Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src; - - -(* explode *) - -fun no_syms [] = true - | no_syms ("\\" :: "<" :: _) = false - | no_syms (c :: cs) = ord c < enc_start andalso no_syms cs; - -fun sym_explode str = - let val chs = explode str in - if no_syms chs then chs (*tune trivial case*) - else map symbol (the (Scan.read stopper (Scan.repeat scan) chs)) - end; - - -(* printable length *) - -fun sym_length ss = foldl (fn (n, c) => if is_printable c then n + 1 else n) (0, ss); -val sym_size = sym_length o sym_explode; - - -(* input / output *) - -fun input str = - let val chs = explode str in - if forall (fn c => ord c < enc_start) chs then str - else implode (map symbol' chs) - end; - -val output = implode o map char o sym_explode; - - -(*final declarations of this structure!*) -val explode = sym_explode; -val length = sym_length; -val size = sym_size; - - -end;