1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/General/README Wed Jan 13 12:44:33 1999 +0100
1.3 @@ -0,0 +1,20 @@
1.4 +
1.5 + Pure/General/
1.6 +
1.7 +
1.8 +This directory contains general purpose modules, all of which are
1.9 +exported.
1.10 +
1.11 + TableFun (generic tables)
1.12 + Symtab (tables indexed by strings)
1.13 + Object (generic objects of arbitrary type)
1.14 + Seq (unbounded sequences)
1.15 + NameSpace (hierarchically structured name spaces)
1.16 + Position (input positions)
1.17 + Path (abstract algebra of file paths)
1.18 + File (file system operations)
1.19 + History (histories of values, with undo and redo)
1.20 + Scan (generic scanner toolbox)
1.21 + Source (co-algebraic data sources)
1.22 + Symbol (generalized characters)
1.23 + Pretty (generic pretty printing module)
2.1 --- a/src/Pure/General/ROOT.ML Wed Jan 13 12:16:34 1999 +0100
2.2 +++ b/src/Pure/General/ROOT.ML Wed Jan 13 12:44:33 1999 +0100
2.3 @@ -12,6 +12,10 @@
2.4 use "path.ML";
2.5 use "file.ML";
2.6 use "history.ML";
2.7 +use "scan.ML";
2.8 +use "source.ML";
2.9 +use "symbol.ML";
2.10 +use "pretty.ML";
2.11
2.12 structure PureGeneral =
2.13 struct
2.14 @@ -23,4 +27,8 @@
2.15 structure Path = Path;
2.16 structure File = File;
2.17 structure History = History;
2.18 + structure Scan = Scan;
2.19 + structure Source = Source;
2.20 + structure Symbol = Symbol;
2.21 + structure Pretty = Pretty;
2.22 end;
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Pure/General/pretty.ML Wed Jan 13 12:44:33 1999 +0100
3.3 @@ -0,0 +1,249 @@
3.4 +(* Title: Pure/Syntax/pretty.ML
3.5 + ID: $Id$
3.6 + Author: Lawrence C Paulson
3.7 + Copyright 1991 University of Cambridge
3.8 +
3.9 +Generic pretty printing module.
3.10 +
3.11 +Loosely based on
3.12 + D. C. Oppen, "Pretty Printing",
3.13 + ACM Transactions on Programming Languages and Systems (1980), 465-483.
3.14 +
3.15 +The object to be printed is given as a tree with indentation and line
3.16 +breaking information. A "break" inserts a newline if the text until
3.17 +the next break is too long to fit on the current line. After the newline,
3.18 +text is indented to the level of the enclosing block. Normally, if a block
3.19 +is broken then all enclosing blocks will also be broken. Only "inconsistent
3.20 +breaks" are provided.
3.21 +
3.22 +The stored length of a block is used in breakdist (to treat each inner block as
3.23 +a unit for breaking).
3.24 +*)
3.25 +
3.26 +type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
3.27 + (unit -> unit) * (unit -> unit);
3.28 +
3.29 +signature PRETTY =
3.30 + sig
3.31 + type T
3.32 + val str: string -> T
3.33 + val strlen: string -> int -> T
3.34 + val sym: string -> T
3.35 + val spc: int -> T
3.36 + val brk: int -> T
3.37 + val fbrk: T
3.38 + val blk: int * T list -> T
3.39 + val lst: string * string -> T list -> T
3.40 + val quote: T -> T
3.41 + val commas: T list -> T list
3.42 + val breaks: T list -> T list
3.43 + val fbreaks: T list -> T list
3.44 + val block: T list -> T
3.45 + val strs: string list -> T
3.46 + val enclose: string -> string -> T list -> T
3.47 + val list: string -> string -> T list -> T
3.48 + val str_list: string -> string -> string list -> T
3.49 + val big_list: string -> T list -> T
3.50 + val string_of: T -> string
3.51 + val writeln: T -> unit
3.52 + val str_of: T -> string
3.53 + val pprint: T -> pprint_args -> unit
3.54 + val setdepth: int -> unit
3.55 + val setmargin: int -> unit
3.56 + end;
3.57 +
3.58 +structure Pretty : PRETTY =
3.59 +struct
3.60 +
3.61 +(*printing items: compound phrases, strings, and breaks*)
3.62 +datatype T =
3.63 + Block of T list * int * int | (*body, indentation, length*)
3.64 + String of string * int | (*text, length*)
3.65 + Break of bool * int; (*mandatory flag, width if not taken*);
3.66 +
3.67 +(*Add the lengths of the expressions until the next Break; if no Break then
3.68 + include "after", to account for text following this block. *)
3.69 +fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after)
3.70 + | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
3.71 + | breakdist (Break _ :: es, after) = 0
3.72 + | breakdist ([], after) = after;
3.73 +
3.74 +fun repstring a 0 = ""
3.75 + | repstring a 1 = a
3.76 + | repstring a k =
3.77 + if k mod 2 = 0 then repstring(a^a) (k div 2)
3.78 + else repstring(a^a) (k div 2) ^ a;
3.79 +
3.80 +(*** Type for lines of text: string, # of lines, position on line ***)
3.81 +
3.82 +type text = {tx: string, nl: int, pos: int};
3.83 +
3.84 +val emptytext = {tx="", nl=0, pos=0};
3.85 +
3.86 +fun blanks wd {tx,nl,pos} =
3.87 + {tx = tx ^ repstring " " wd,
3.88 + nl = nl,
3.89 + pos = pos+wd};
3.90 +
3.91 +fun newline {tx,nl,pos} =
3.92 + {tx = tx ^ "\n",
3.93 + nl = nl+1,
3.94 + pos = 0};
3.95 +
3.96 +fun string s len {tx,nl,pos:int} =
3.97 + {tx = tx ^ s,
3.98 + nl = nl,
3.99 + pos = pos + len};
3.100 +
3.101 +
3.102 +(*** Formatting ***)
3.103 +
3.104 +(* margin *)
3.105 +
3.106 +(*example values*)
3.107 +val margin = ref 80 (*right margin, or page width*)
3.108 +and breakgain = ref 4 (*minimum added space required of a break*)
3.109 +and emergencypos = ref 40; (*position too far to right*)
3.110 +
3.111 +fun setmargin m =
3.112 + (margin := m;
3.113 + breakgain := !margin div 20;
3.114 + emergencypos := !margin div 2);
3.115 +
3.116 +val () = setmargin 76;
3.117 +
3.118 +
3.119 +(*Search for the next break (at this or higher levels) and force it to occur*)
3.120 +fun forcenext [] = []
3.121 + | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
3.122 + | forcenext (e :: es) = e :: forcenext es;
3.123 +
3.124 +(*es is list of expressions to print;
3.125 + blockin is the indentation of the current block;
3.126 + after is the width of the following context until next break. *)
3.127 +fun format ([], _, _) text = text
3.128 + | format (e::es, blockin, after) (text as {pos,nl,...}) =
3.129 + (case e of
3.130 + Block(bes,indent,wd) =>
3.131 + let val blockin' = (pos + indent) mod !emergencypos
3.132 + val btext = format(bes, blockin', breakdist(es,after)) text
3.133 + (*If this block was broken then force the next break.*)
3.134 + val es2 = if nl < #nl(btext) then forcenext es else es
3.135 + in format (es2,blockin,after) btext end
3.136 + | String (s, len) => format (es,blockin,after) (string s len text)
3.137 + | Break(force,wd) => (*no break if text to next break fits on this line
3.138 + or if breaking would add only breakgain to space *)
3.139 + format (es,blockin,after)
3.140 + (if not force andalso
3.141 + pos+wd <= Int.max(!margin - breakdist(es,after),
3.142 + blockin + !breakgain)
3.143 + then blanks wd text (*just insert wd blanks*)
3.144 + else blanks blockin (newline text)));
3.145 +
3.146 +
3.147 +(*** Exported functions to create formatting expressions ***)
3.148 +
3.149 +fun length (Block (_, _, len)) = len
3.150 + | length (String (_, len)) = len
3.151 + | length (Break(_, wd)) = wd;
3.152 +
3.153 +fun str s = String (s, size s);
3.154 +fun strlen s len = String (s, len);
3.155 +fun sym s = String (s, Symbol.size s);
3.156 +
3.157 +fun spc n = str (repstring " " n);
3.158 +
3.159 +fun brk wd = Break (false, wd);
3.160 +val fbrk = Break (true, 0);
3.161 +
3.162 +fun blk (indent, es) =
3.163 + let
3.164 + fun sum([], k) = k
3.165 + | sum(e :: es, k) = sum (es, length e + k);
3.166 + in Block (es, indent, sum (es, 0)) end;
3.167 +
3.168 +(*Join the elements of es as a comma-separated list, bracketted by lp and rp*)
3.169 +fun lst(lp,rp) es =
3.170 + let fun add(e,es) = str"," :: brk 1 :: e :: es;
3.171 + fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
3.172 + | list(e::[]) = [str lp, e, str rp]
3.173 + | list([]) = []
3.174 + in blk(size lp, list es) end;
3.175 +
3.176 +
3.177 +(* utils *)
3.178 +
3.179 +fun quote prt =
3.180 + blk (1, [str "\"", prt, str "\""]);
3.181 +
3.182 +fun commas prts =
3.183 + flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
3.184 +
3.185 +fun breaks prts = separate (brk 1) prts;
3.186 +
3.187 +fun fbreaks prts = separate fbrk prts;
3.188 +
3.189 +fun block prts = blk (2, prts);
3.190 +
3.191 +val strs = block o breaks o (map str);
3.192 +
3.193 +fun enclose lpar rpar prts =
3.194 + block (str lpar :: (prts @ [str rpar]));
3.195 +
3.196 +fun list lpar rpar prts =
3.197 + enclose lpar rpar (commas prts);
3.198 +
3.199 +fun str_list lpar rpar strs =
3.200 + list lpar rpar (map str strs);
3.201 +
3.202 +fun big_list name prts =
3.203 + block (fbreaks (str name :: prts));
3.204 +
3.205 +
3.206 +
3.207 +(*** Pretty printing with depth limitation ***)
3.208 +
3.209 +val depth = ref 0; (*maximum depth; 0 means no limit*)
3.210 +
3.211 +fun setdepth dp = (depth := dp);
3.212 +
3.213 +(*Recursively prune blocks, discarding all text exceeding depth dp*)
3.214 +fun pruning dp (Block(bes,indent,wd)) =
3.215 + if dp>0 then blk(indent, map (pruning(dp-1)) bes)
3.216 + else str "..."
3.217 + | pruning dp e = e;
3.218 +
3.219 +fun prune dp e = if dp>0 then pruning dp e else e;
3.220 +
3.221 +
3.222 +fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext);
3.223 +
3.224 +val writeln = writeln o string_of;
3.225 +
3.226 +
3.227 +(*Create a single flat string: no line breaking*)
3.228 +fun str_of prt =
3.229 + let
3.230 + fun s_of (Block (prts, _, _)) = implode (map s_of prts)
3.231 + | s_of (String (s, _)) = s
3.232 + | s_of (Break (false, wd)) = repstring " " wd
3.233 + | s_of (Break (true, _)) = " ";
3.234 + in
3.235 + s_of (prune (! depth) prt)
3.236 + end;
3.237 +
3.238 +(*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
3.239 +fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
3.240 + let
3.241 + fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
3.242 + | pp (String (s, _)) = put_str s
3.243 + | pp (Break (false, wd)) = put_brk wd
3.244 + | pp (Break (true, _)) = put_fbrk ()
3.245 + and pp_lst [] = ()
3.246 + | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
3.247 + in
3.248 + pp (prune (! depth) prt)
3.249 + end;
3.250 +
3.251 +
3.252 +end;
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Pure/General/scan.ML Wed Jan 13 12:44:33 1999 +0100
4.3 @@ -0,0 +1,305 @@
4.4 +(* Title: Pure/Syntax/scan.ML
4.5 + ID: $Id$
4.6 + Author: Markus Wenzel and Tobias Nipkow, TU Muenchen
4.7 +
4.8 +Generic scanners (for potentially infinite input).
4.9 +*)
4.10 +
4.11 +infix 5 -- :-- |-- --| ^^;
4.12 +infix 3 >>;
4.13 +infix 0 ||;
4.14 +
4.15 +signature BASIC_SCAN =
4.16 +sig
4.17 + val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b
4.18 + val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
4.19 + val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
4.20 + val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
4.21 + val :-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
4.22 + val |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e
4.23 + val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e
4.24 + val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
4.25 + val $$ : ''a -> ''a list -> ''a * ''a list
4.26 +end;
4.27 +
4.28 +signature SCAN =
4.29 +sig
4.30 + include BASIC_SCAN
4.31 + val fail: 'a -> 'b
4.32 + val fail_with: ('a -> string) -> 'a -> 'b
4.33 + val succeed: 'a -> 'b -> 'a * 'b
4.34 + val one: ('a -> bool) -> 'a list -> 'a * 'a list
4.35 + val any: ('a -> bool) -> 'a list -> 'a list * 'a list
4.36 + val any1: ('a -> bool) -> 'a list -> 'a list * 'a list
4.37 + val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a
4.38 + val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
4.39 + val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
4.40 + val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
4.41 + val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
4.42 + val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
4.43 + val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd
4.44 + val first: ('a -> 'b) list -> 'a -> 'b
4.45 + val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
4.46 + val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
4.47 + val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
4.48 + val try: ('a -> 'b) -> 'a -> 'b
4.49 + val force: ('a -> 'b) -> 'a -> 'b
4.50 + val prompt: string -> ('a -> 'b) -> 'a -> 'b
4.51 + val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list))
4.52 + -> 'b * 'a list -> 'c * ('d * 'a list)
4.53 + val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
4.54 + val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
4.55 + val catch: ('a -> 'b) -> 'a -> 'b
4.56 + val error: ('a -> 'b) -> 'a -> 'b
4.57 + val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
4.58 + 'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
4.59 + ('d * 'b list -> 'f * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
4.60 + val source: string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
4.61 + 'b * ('b -> bool) -> ('b list -> 'd list * 'b list) ->
4.62 + ('b list -> 'e * 'b list) option -> 'a -> 'd list * 'c
4.63 + val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
4.64 + val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
4.65 + type lexicon
4.66 + val dest_lexicon: lexicon -> string list list
4.67 + val make_lexicon: string list list -> lexicon
4.68 + val empty_lexicon: lexicon
4.69 + val extend_lexicon: lexicon -> string list list -> lexicon
4.70 + val merge_lexicons: lexicon -> lexicon -> lexicon
4.71 + val literal: lexicon -> string list -> string list * string list
4.72 +end;
4.73 +
4.74 +structure Scan: SCAN =
4.75 +struct
4.76 +
4.77 +
4.78 +(** scanners **)
4.79 +
4.80 +exception MORE of string option; (*need more input (prompt)*)
4.81 +exception FAIL of string option; (*try alternatives (reason of failure)*)
4.82 +exception ABORT of string; (*dead end*)
4.83 +
4.84 +
4.85 +(* scanner combinators *)
4.86 +
4.87 +fun (scan >> f) xs = apfst f (scan xs);
4.88 +
4.89 +fun (scan1 || scan2) xs = scan1 xs handle FAIL _ => scan2 xs;
4.90 +
4.91 +(*dependent pairing*)
4.92 +fun (scan1 :-- scan2) xs =
4.93 + let
4.94 + val (x, ys) = scan1 xs;
4.95 + val (y, zs) = scan2 x ys;
4.96 + in ((x, y), zs) end;
4.97 +
4.98 +fun (scan1 -- scan2) = scan1 :-- (fn _ => scan2);
4.99 +fun (scan1 |-- scan2) = scan1 -- scan2 >> #2;
4.100 +fun (scan1 --| scan2) = scan1 -- scan2 >> #1;
4.101 +fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^;
4.102 +
4.103 +
4.104 +(* generic scanners *)
4.105 +
4.106 +fun fail _ = raise FAIL None;
4.107 +fun fail_with msg_of xs = raise FAIL (Some (msg_of xs));
4.108 +fun succeed y xs = (y, xs);
4.109 +
4.110 +fun one _ [] = raise MORE None
4.111 + | one pred (x :: xs) =
4.112 + if pred x then (x, xs) else raise FAIL None;
4.113 +
4.114 +fun $$ _ [] = raise MORE None
4.115 + | $$ a (x :: xs) =
4.116 + if a = x then (x, xs) else raise FAIL None;
4.117 +
4.118 +fun any _ [] = raise MORE None
4.119 + | any pred (lst as x :: xs) =
4.120 + if pred x then apfst (cons x) (any pred xs)
4.121 + else ([], lst);
4.122 +
4.123 +fun any1 pred = one pred -- any pred >> op ::;
4.124 +
4.125 +fun optional scan def = scan || succeed def;
4.126 +fun option scan = optional (scan >> Some) None;
4.127 +
4.128 +fun repeat scan xs = (scan -- repeat scan >> op :: || succeed []) xs;
4.129 +fun repeat1 scan = scan -- repeat scan >> op ::;
4.130 +
4.131 +fun max leq scan1 scan2 xs =
4.132 + (case (option scan1 xs, option scan2 xs) of
4.133 + ((None, _), (None, _)) => raise FAIL None (*looses FAIL msg!*)
4.134 + | ((Some tok1, xs'), (None, _)) => (tok1, xs')
4.135 + | ((None, _), (Some tok2, xs')) => (tok2, xs')
4.136 + | ((Some tok1, xs1'), (Some tok2, xs2')) =>
4.137 + if leq (tok2, tok1) then (tok1, xs1') else (tok2, xs2'));
4.138 +
4.139 +fun ahead scan xs = (fst (scan xs), xs);
4.140 +
4.141 +fun unless test scan =
4.142 + ahead (option test) :-- (fn None => scan | _ => fail) >> #2;
4.143 +
4.144 +fun first [] = fail
4.145 + | first (scan :: scans) = scan || first scans;
4.146 +
4.147 +
4.148 +(* state based scanners *)
4.149 +
4.150 +fun depend scan (st, xs) =
4.151 + let val ((st', y), xs') = scan st xs
4.152 + in (y, (st', xs')) end;
4.153 +
4.154 +fun lift scan (st, xs) =
4.155 + let val (y, xs') = scan xs
4.156 + in (y, (st, xs')) end;
4.157 +
4.158 +fun pass st scan xs =
4.159 + let val (y, (_, xs')) = scan (st, xs)
4.160 + in (y, xs') end;
4.161 +
4.162 +
4.163 +(* exception handling *)
4.164 +
4.165 +fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
4.166 +fun try scan xs = scan xs handle MORE _ => raise FAIL None | ABORT _ => raise FAIL None;
4.167 +fun force scan xs = scan xs handle MORE _ => raise FAIL None;
4.168 +fun prompt str scan xs = scan xs handle MORE None => raise MORE (Some str);
4.169 +fun catch scan xs = scan xs handle ABORT msg => raise FAIL (Some msg);
4.170 +fun error scan xs = scan xs handle ABORT msg => Library.error msg;
4.171 +
4.172 +
4.173 +(* finite scans *)
4.174 +
4.175 +fun finite' (stopper, is_stopper) scan (state, input) =
4.176 + let
4.177 + fun lost () = raise ABORT "Scanner bug: lost stopper of finite scan!";
4.178 +
4.179 + fun stop [] = lost ()
4.180 + | stop lst =
4.181 + let val (xs, x) = split_last lst
4.182 + in if is_stopper x then ((), xs) else lost () end;
4.183 + in
4.184 + if exists is_stopper input then
4.185 + raise ABORT "Stopper may not occur in input of finite scan!"
4.186 + else (force scan --| lift stop) (state, input @ [stopper])
4.187 + end;
4.188 +
4.189 +fun finite stopper scan xs =
4.190 + let val (y, ((), xs')) = finite' stopper (lift scan) ((), xs)
4.191 + in (y, xs') end;
4.192 +
4.193 +fun read stopper scan xs =
4.194 + (case error (finite stopper (option scan)) xs of
4.195 + (y as Some _, []) => y
4.196 + | _ => None);
4.197 +
4.198 +
4.199 +
4.200 +(* infinite scans -- draining state-based source *)
4.201 +
4.202 +fun drain def_prmpt get stopper scan ((state, xs), src) =
4.203 + (scan (state, xs), src) handle MORE prmpt =>
4.204 + (case get (if_none prmpt def_prmpt) src of
4.205 + ([], _) => (finite' stopper scan (state, xs), src)
4.206 + | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src'));
4.207 +
4.208 +fun source' def_prmpt get unget stopper scanner opt_recover (state, src) =
4.209 + let
4.210 + fun drain_with scan = drain def_prmpt get stopper scan;
4.211 +
4.212 + fun drain_loop recover inp =
4.213 + drain_with (catch scanner) inp handle FAIL msg =>
4.214 + (error_msg (if_none msg "Syntax error.");
4.215 + drain_loop recover (apfst snd (drain_with recover inp)));
4.216 +
4.217 + val ((ys, (state', xs')), src') =
4.218 + (case (get def_prmpt src, opt_recover) of
4.219 + (([], s), _) => (([], (state, [])), s)
4.220 + | ((xs, s), None) => drain_with (error scanner) ((state, xs), s)
4.221 + | ((xs, s), Some scan) => drain_loop scan ((state, xs), s));
4.222 + in
4.223 + (ys, (state', unget (xs', src')))
4.224 + end;
4.225 +
4.226 +fun source def_prmpt get unget stopper scan opt_recover src =
4.227 + let val (ys, ((), src')) =
4.228 + source' def_prmpt get unget stopper (lift scan) (apsome lift opt_recover) ((), src)
4.229 + in (ys, src') end;
4.230 +
4.231 +fun single scan = scan >> (fn x => [x]);
4.232 +fun bulk scan = scan -- repeat (try scan) >> (op ::);
4.233 +
4.234 +
4.235 +
4.236 +(** datatype lexicon **)
4.237 +
4.238 +datatype lexicon =
4.239 + Empty |
4.240 + Branch of string * string list * lexicon * lexicon * lexicon;
4.241 +
4.242 +val no_literal = [];
4.243 +
4.244 +
4.245 +(* dest_lexicon *)
4.246 +
4.247 +fun dest_lexicon Empty = []
4.248 + | dest_lexicon (Branch (_, [], lt, eq, gt)) =
4.249 + dest_lexicon lt @ dest_lexicon eq @ dest_lexicon gt
4.250 + | dest_lexicon (Branch (_, cs, lt, eq, gt)) =
4.251 + dest_lexicon lt @ [cs] @ dest_lexicon eq @ dest_lexicon gt;
4.252 +
4.253 +
4.254 +(* empty, extend, make, merge lexicons *)
4.255 +
4.256 +val empty_lexicon = Empty;
4.257 +
4.258 +fun extend_lexicon lexicon chrss =
4.259 + let
4.260 + fun ext (lex, chrs) =
4.261 + let
4.262 + fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
4.263 + if c < d then Branch (d, a, add lt chs, eq, gt)
4.264 + else if c > d then Branch (d, a, lt, eq, add gt chs)
4.265 + else Branch (d, if null cs then chrs else a, lt, add eq cs, gt)
4.266 + | add Empty [c] =
4.267 + Branch (c, chrs, Empty, Empty, Empty)
4.268 + | add Empty (c :: cs) =
4.269 + Branch (c, no_literal, Empty, add Empty cs, Empty)
4.270 + | add lex [] = lex;
4.271 + in add lex chrs end;
4.272 + in foldl ext (lexicon, chrss \\ dest_lexicon lexicon) end;
4.273 +
4.274 +val make_lexicon = extend_lexicon empty_lexicon;
4.275 +
4.276 +fun merge_lexicons lex1 lex2 =
4.277 + let
4.278 + val chss1 = dest_lexicon lex1;
4.279 + val chss2 = dest_lexicon lex2;
4.280 + in
4.281 + if chss2 subset chss1 then lex1
4.282 + else if chss1 subset chss2 then lex2
4.283 + else extend_lexicon lex1 chss2
4.284 + end;
4.285 +
4.286 +
4.287 +(* scan literal *)
4.288 +
4.289 +fun literal lex chrs =
4.290 + let
4.291 + fun lit Empty res _ = res
4.292 + | lit (Branch _) _ [] = raise MORE None
4.293 + | lit (Branch (d, a, lt, eq, gt)) res (chs as c :: cs) =
4.294 + if c < d then lit lt res chs
4.295 + else if c > d then lit gt res chs
4.296 + else lit eq (if a = no_literal then res else Some (a, cs)) cs;
4.297 + in
4.298 + (case lit lex None chrs of
4.299 + None => raise FAIL None
4.300 + | Some res => res)
4.301 + end;
4.302 +
4.303 +
4.304 +end;
4.305 +
4.306 +
4.307 +structure BasicScan: BASIC_SCAN = Scan;
4.308 +open BasicScan;
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/Pure/General/source.ML Wed Jan 13 12:44:33 1999 +0100
5.3 @@ -0,0 +1,150 @@
5.4 +(* Title: Pure/Syntax/source.ML
5.5 + ID: $Id$
5.6 + Author: Markus Wenzel, TU Muenchen
5.7 +
5.8 +Co-algebraic data sources.
5.9 +*)
5.10 +
5.11 +signature SOURCE =
5.12 +sig
5.13 + type ('a, 'b) source
5.14 + val set_prompt: string -> ('a, 'b) source -> ('a, 'b) source
5.15 + val get: ('a, 'b) source -> 'a list * ('a, 'b) source
5.16 + val unget: 'a list * ('a, 'b) source -> ('a, 'b) source
5.17 + val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option
5.18 + val exhaust: ('a, 'b) source -> 'a list
5.19 + val mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source
5.20 + val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source
5.21 + val of_list: 'a list -> ('a, 'a list) source
5.22 + val of_string: string -> (string, string list) source
5.23 + val of_file: string -> (string, string list) source
5.24 + val decorate_prompt_fn: (string -> string) ref
5.25 + val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
5.26 + val tty: (string, unit) source
5.27 + val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
5.28 + ('a * 'b list -> 'd * ('a * 'b list)) option ->
5.29 + ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
5.30 + val source: 'a * ('a -> bool) -> ('a list -> 'b list * 'a list) ->
5.31 + ('a list -> 'c * 'a list) option ->
5.32 + ('a, 'd) source -> ('b, ('a, 'd) source) source
5.33 +end;
5.34 +
5.35 +structure Source: SOURCE =
5.36 +struct
5.37 +
5.38 +
5.39 +(** datatype source **)
5.40 +
5.41 +datatype ('a, 'b) source =
5.42 + Source of
5.43 + {buffer: 'a list,
5.44 + info: 'b,
5.45 + prompt: string,
5.46 + drain: string -> 'b -> 'a list * 'b};
5.47 +
5.48 +fun make_source buffer info prompt drain =
5.49 + Source {buffer = buffer, info = info, prompt = prompt, drain = drain};
5.50 +
5.51 +
5.52 +(* prompt *)
5.53 +
5.54 +val default_prompt = "> ";
5.55 +
5.56 +fun set_prompt prompt (Source {buffer, info, prompt = _, drain}) =
5.57 + make_source buffer info prompt drain;
5.58 +
5.59 +
5.60 +(* get / unget *)
5.61 +
5.62 +fun get (Source {buffer = [], info, prompt, drain}) =
5.63 + let val (xs, info') = drain prompt info
5.64 + in (xs, make_source [] info' prompt drain) end
5.65 + | get (Source {buffer, info, prompt, drain}) =
5.66 + (buffer, make_source [] info prompt drain);
5.67 +
5.68 +fun unget (xs, Source {buffer, info, prompt, drain}) =
5.69 + make_source (xs @ buffer) info prompt drain;
5.70 +
5.71 +
5.72 +(* variations on get *)
5.73 +
5.74 +fun get_prompt prompt src = get (set_prompt prompt src);
5.75 +
5.76 +fun get_single src =
5.77 + (case get src of
5.78 + ([], _) => None
5.79 + | (x :: xs, src') => Some (x, unget (xs, src')));
5.80 +
5.81 +fun exhaust src =
5.82 + (case get src of
5.83 + ([], _) => []
5.84 + | (xs, src') => xs @ exhaust src');
5.85 +
5.86 +
5.87 +(* (map)filter *)
5.88 +
5.89 +fun drain_mapfilter f prompt src =
5.90 + let
5.91 + val (xs, src') = get_prompt prompt src;
5.92 + val xs' = Library.mapfilter f xs;
5.93 + in
5.94 + if null xs orelse not (null xs') then (xs', src')
5.95 + else drain_mapfilter f prompt src'
5.96 + end;
5.97 +
5.98 +fun mapfilter f src = make_source [] src default_prompt (drain_mapfilter f);
5.99 +fun filter pred = mapfilter (fn x => if pred x then Some x else None);
5.100 +
5.101 +
5.102 +
5.103 +(** build sources **)
5.104 +
5.105 +(* list source *)
5.106 +
5.107 +(*limiting the input buffer considerably improves performance*)
5.108 +val limit = 4000;
5.109 +
5.110 +fun drain_list _ xs = (take (limit, xs), drop (limit, xs));
5.111 +
5.112 +fun of_list xs = make_source [] xs default_prompt drain_list;
5.113 +val of_string = of_list o explode;
5.114 +val of_file = of_string o File.read;
5.115 +
5.116 +
5.117 +(* stream source *)
5.118 +
5.119 +val decorate_prompt_fn = ref (fn s:string => s);
5.120 +
5.121 +fun drain_stream instream outstream prompt () =
5.122 + (TextIO.output (outstream, ! decorate_prompt_fn prompt);
5.123 + TextIO.flushOut outstream;
5.124 + (explode (TextIO.inputLine instream), ()));
5.125 +
5.126 +fun of_stream instream outstream =
5.127 + make_source [] () default_prompt (drain_stream instream outstream);
5.128 +
5.129 +val tty = of_stream TextIO.stdIn TextIO.stdOut;
5.130 +
5.131 +
5.132 +
5.133 +(** compose sources **)
5.134 +
5.135 +fun drain_source source stopper scan recover prompt src =
5.136 + source prompt get_prompt unget stopper scan recover src;
5.137 +
5.138 +
5.139 +(* state-based *)
5.140 +
5.141 +fun source' init_state stopper scan recover src =
5.142 + make_source [] (init_state, src) default_prompt
5.143 + (drain_source Scan.source' stopper scan recover);
5.144 +
5.145 +
5.146 +(* non state-based *)
5.147 +
5.148 +fun source stopper scan recover src =
5.149 + make_source [] src default_prompt
5.150 + (drain_source Scan.source stopper scan recover);
5.151 +
5.152 +
5.153 +end;
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/Pure/General/symbol.ML Wed Jan 13 12:44:33 1999 +0100
6.3 @@ -0,0 +1,274 @@
6.4 +(* Title: Pure/Syntax/symbol.ML
6.5 + ID: $Id$
6.6 + Author: Markus Wenzel, TU Muenchen
6.7 +
6.8 +Generalized characters.
6.9 +*)
6.10 +
6.11 +signature SYMBOL =
6.12 +sig
6.13 + type symbol
6.14 + val space: symbol
6.15 + val eof: symbol
6.16 + val is_eof: symbol -> bool
6.17 + val not_eof: symbol -> bool
6.18 + val stopper: symbol * (symbol -> bool)
6.19 + val is_ascii: symbol -> bool
6.20 + val is_letter: symbol -> bool
6.21 + val is_digit: symbol -> bool
6.22 + val is_quasi_letter: symbol -> bool
6.23 + val is_letdig: symbol -> bool
6.24 + val is_blank: symbol -> bool
6.25 + val is_printable: symbol -> bool
6.26 + val beginning: symbol list -> string
6.27 + val scan: string list -> symbol * string list
6.28 + val explode: string -> symbol list
6.29 + val length: symbol list -> int
6.30 + val size: string -> int
6.31 + val input: string -> string
6.32 + val output: string -> string
6.33 + val source: bool -> (string, 'a) Source.source ->
6.34 + (symbol, (string, 'a) Source.source) Source.source
6.35 +end;
6.36 +
6.37 +structure Symbol: SYMBOL =
6.38 +struct
6.39 +
6.40 +
6.41 +(** encoding table (isabelle-0) **)
6.42 +
6.43 +val enc_start = 160;
6.44 +val enc_end = 255;
6.45 +
6.46 +val enc_vector =
6.47 +[
6.48 +(* GENERATED TEXT FOLLOWS - Do not edit! *)
6.49 + "\\<space2>",
6.50 + "\\<Gamma>",
6.51 + "\\<Delta>",
6.52 + "\\<Theta>",
6.53 + "\\<Lambda>",
6.54 + "\\<Pi>",
6.55 + "\\<Sigma>",
6.56 + "\\<Phi>",
6.57 + "\\<Psi>",
6.58 + "\\<Omega>",
6.59 + "\\<alpha>",
6.60 + "\\<beta>",
6.61 + "\\<gamma>",
6.62 + "\\<delta>",
6.63 + "\\<epsilon>",
6.64 + "\\<zeta>",
6.65 + "\\<eta>",
6.66 + "\\<theta>",
6.67 + "\\<kappa>",
6.68 + "\\<lambda>",
6.69 + "\\<mu>",
6.70 + "\\<nu>",
6.71 + "\\<xi>",
6.72 + "\\<pi>",
6.73 + "\\<rho>",
6.74 + "\\<sigma>",
6.75 + "\\<tau>",
6.76 + "\\<phi>",
6.77 + "\\<chi>",
6.78 + "\\<psi>",
6.79 + "\\<omega>",
6.80 + "\\<not>",
6.81 + "\\<and>",
6.82 + "\\<or>",
6.83 + "\\<forall>",
6.84 + "\\<exists>",
6.85 + "\\<And>",
6.86 + "\\<lceil>",
6.87 + "\\<rceil>",
6.88 + "\\<lfloor>",
6.89 + "\\<rfloor>",
6.90 + "\\<turnstile>",
6.91 + "\\<Turnstile>",
6.92 + "\\<lbrakk>",
6.93 + "\\<rbrakk>",
6.94 + "\\<cdot>",
6.95 + "\\<in>",
6.96 + "\\<subseteq>",
6.97 + "\\<inter>",
6.98 + "\\<union>",
6.99 + "\\<Inter>",
6.100 + "\\<Union>",
6.101 + "\\<sqinter>",
6.102 + "\\<squnion>",
6.103 + "\\<Sqinter>",
6.104 + "\\<Squnion>",
6.105 + "\\<bottom>",
6.106 + "\\<doteq>",
6.107 + "\\<equiv>",
6.108 + "\\<noteq>",
6.109 + "\\<sqsubset>",
6.110 + "\\<sqsubseteq>",
6.111 + "\\<prec>",
6.112 + "\\<preceq>",
6.113 + "\\<succ>",
6.114 + "\\<approx>",
6.115 + "\\<sim>",
6.116 + "\\<simeq>",
6.117 + "\\<le>",
6.118 + "\\<Colon>",
6.119 + "\\<leftarrow>",
6.120 + "\\<midarrow>",
6.121 + "\\<rightarrow>",
6.122 + "\\<Leftarrow>",
6.123 + "\\<Midarrow>",
6.124 + "\\<Rightarrow>",
6.125 + "\\<bow>",
6.126 + "\\<mapsto>",
6.127 + "\\<leadsto>",
6.128 + "\\<up>",
6.129 + "\\<down>",
6.130 + "\\<notin>",
6.131 + "\\<times>",
6.132 + "\\<oplus>",
6.133 + "\\<ominus>",
6.134 + "\\<otimes>",
6.135 + "\\<oslash>",
6.136 + "\\<subset>",
6.137 + "\\<infinity>",
6.138 + "\\<box>",
6.139 + "\\<diamond>",
6.140 + "\\<circ>",
6.141 + "\\<bullet>",
6.142 + "\\<parallel>",
6.143 + "\\<surd>",
6.144 + "\\<copyright>"
6.145 +(* END OF GENERATED TEXT *)
6.146 +];
6.147 +
6.148 +val enc_rel = enc_vector ~~ map chr (enc_start upto enc_end);
6.149 +
6.150 +val char_tab = Symtab.make enc_rel;
6.151 +val symbol_tab = Symtab.make (map swap enc_rel);
6.152 +
6.153 +fun lookup_symbol c =
6.154 + if ord c < enc_start then None
6.155 + else Symtab.lookup (symbol_tab, c);
6.156 +
6.157 +
6.158 +(* encode / decode *)
6.159 +
6.160 +fun char s = if_none (Symtab.lookup (char_tab, s)) s;
6.161 +fun symbol c = if_none (lookup_symbol c) c;
6.162 +
6.163 +fun symbol' c =
6.164 + (case lookup_symbol c of
6.165 + None => c
6.166 + | Some s => "\\" ^ s);
6.167 +
6.168 +
6.169 +
6.170 +(** type symbol **)
6.171 +
6.172 +type symbol = string;
6.173 +
6.174 +val space = " ";
6.175 +val eof = "";
6.176 +
6.177 +
6.178 +(* kinds *)
6.179 +
6.180 +fun is_eof s = s = eof;
6.181 +fun not_eof s = s <> eof;
6.182 +val stopper = (eof, is_eof);
6.183 +
6.184 +fun is_ascii s = size s = 1 andalso ord s < 128;
6.185 +
6.186 +fun is_letter s =
6.187 + size s = 1 andalso
6.188 + (ord "A" <= ord s andalso ord s <= ord "Z" orelse
6.189 + ord "a" <= ord s andalso ord s <= ord "z");
6.190 +
6.191 +fun is_digit s =
6.192 + size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9";
6.193 +
6.194 +fun is_quasi_letter "_" = true
6.195 + | is_quasi_letter "'" = true
6.196 + | is_quasi_letter s = is_letter s;
6.197 +
6.198 +val is_blank =
6.199 + fn " " => true | "\t" => true | "\n" => true | "\^L" => true
6.200 + | "\160" => true | "\\<space2>" => true
6.201 + | _ => false;
6.202 +
6.203 +val is_letdig = is_quasi_letter orf is_digit;
6.204 +
6.205 +fun is_printable s =
6.206 + size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse
6.207 + size s > 2 andalso nth_elem (2, explode s) <> "^";
6.208 +
6.209 +
6.210 +(* beginning *)
6.211 +
6.212 +val smash_blanks = map (fn s => if is_blank s then space else s);
6.213 +
6.214 +fun beginning raw_ss =
6.215 + let
6.216 + val (all_ss, _) = take_suffix is_blank raw_ss;
6.217 + val dots = if length all_ss > 10 then " ..." else "";
6.218 + val (ss, _) = take_suffix is_blank (take (10, all_ss));
6.219 + in implode (smash_blanks ss) ^ dots end;
6.220 +
6.221 +
6.222 +(* scan *)
6.223 +
6.224 +val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
6.225 +
6.226 +val scan =
6.227 + ($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
6.228 + !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs)
6.229 + (Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") ||
6.230 + Scan.one not_eof;
6.231 +
6.232 +
6.233 +(* source *)
6.234 +
6.235 +val recover = Scan.any1 ((not o is_blank) andf not_eof);
6.236 +
6.237 +fun source do_recover src =
6.238 + Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src;
6.239 +
6.240 +
6.241 +(* explode *)
6.242 +
6.243 +fun no_syms [] = true
6.244 + | no_syms ("\\" :: "<" :: _) = false
6.245 + | no_syms (c :: cs) = ord c < enc_start andalso no_syms cs;
6.246 +
6.247 +fun sym_explode str =
6.248 + let val chs = explode str in
6.249 + if no_syms chs then chs (*tune trivial case*)
6.250 + else map symbol (the (Scan.read stopper (Scan.repeat scan) chs))
6.251 + end;
6.252 +
6.253 +
6.254 +(* printable length *)
6.255 +
6.256 +fun sym_length ss = foldl (fn (n, c) => if is_printable c then n + 1 else n) (0, ss);
6.257 +val sym_size = sym_length o sym_explode;
6.258 +
6.259 +
6.260 +(* input / output *)
6.261 +
6.262 +fun input str =
6.263 + let val chs = explode str in
6.264 + if forall (fn c => ord c < enc_start) chs then str
6.265 + else implode (map symbol' chs)
6.266 + end;
6.267 +
6.268 +val output = implode o map char o sym_explode;
6.269 +
6.270 +
6.271 +(*final declarations of this structure!*)
6.272 +val explode = sym_explode;
6.273 +val length = sym_length;
6.274 +val size = sym_size;
6.275 +
6.276 +
6.277 +end;
7.1 --- a/src/Pure/IsaMakefile Wed Jan 13 12:16:34 1999 +0100
7.2 +++ b/src/Pure/IsaMakefile Wed Jan 13 12:44:33 1999 +0100
7.3 @@ -25,7 +25,8 @@
7.4
7.5 $(OUT)/Pure: General/ROOT.ML General/file.ML General/history.ML \
7.6 General/name_space.ML General/object.ML General/path.ML \
7.7 - General/position.ML General/seq.ML General/table.ML Isar/ROOT.ML \
7.8 + General/position.ML General/pretty.ML General/scan.ML General/seq.ML \
7.9 + General/source.ML General/symbol.ML General/table.ML Isar/ROOT.ML \
7.10 Isar/args.ML Isar/attrib.ML Isar/isar.ML Isar/isar_cmd.ML \
7.11 Isar/isar_syn.ML Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \
7.12 Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \
7.13 @@ -33,12 +34,11 @@
7.14 Isar/toplevel.ML ML-Systems/mlworks.ML ML-Systems/polyml.ML \
7.15 ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML \
7.16 Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
7.17 - Syntax/pretty.ML Syntax/printer.ML Syntax/scan.ML Syntax/source.ML \
7.18 - Syntax/symbol.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \
7.19 - Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML \
7.20 - Thy/ROOT.ML Thy/browser_info.ML Thy/context.ML Thy/thm_database.ML \
7.21 - Thy/thy_info.ML Thy/thy_parse.ML Thy/thy_read.ML Thy/thy_scan.ML \
7.22 - Thy/thy_syn.ML Thy/use.ML axclass.ML basis.ML deriv.ML display.ML \
7.23 + Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \
7.24 + Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML Thy/ROOT.ML \
7.25 + Thy/browser_info.ML Thy/context.ML Thy/thm_database.ML Thy/thy_info.ML \
7.26 + Thy/thy_parse.ML Thy/thy_read.ML Thy/thy_scan.ML Thy/thy_syn.ML \
7.27 + Thy/use.ML axclass.ML basis.ML deriv.ML display.ML \
7.28 drule.ML envir.ML goals.ML install_pp.ML library.ML locale.ML \
7.29 logic.ML net.ML object_logic.ML pattern.ML pure.ML pure_thy.ML \
7.30 search.ML sign.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML \
8.1 --- a/src/Pure/Syntax/README Wed Jan 13 12:16:34 1999 +0100
8.2 +++ b/src/Pure/Syntax/README Wed Jan 13 12:44:33 1999 +0100
8.3 @@ -4,12 +4,7 @@
8.4
8.5 This directory contains the source files for Isabelle's syntax module,
8.6 which includes a lexer, parser, pretty printer and macro system. Note
8.7 -that only the following structures are supposed to be exported:
8.8 -
8.9 - Pretty (generic pretty printing module)
8.10 - Scan (generic scanner toolbox)
8.11 - Source (co-algebraic data sources)
8.12 - Symbol (generalized characters)
8.13 +that only the following structures are exported:
8.14
8.15 Syntax (internal interface to the syntax module)
8.16 BasicSyntax (part of Syntax made pervasive)
9.1 --- a/src/Pure/Syntax/ROOT.ML Wed Jan 13 12:16:34 1999 +0100
9.2 +++ b/src/Pure/Syntax/ROOT.ML Wed Jan 13 12:44:33 1999 +0100
9.3 @@ -5,13 +5,6 @@
9.4 This file builds the syntax module.
9.5 *)
9.6
9.7 -(*generic modules*)
9.8 -use "scan.ML";
9.9 -use "source.ML";
9.10 -use "symbol.ML";
9.11 -use "pretty.ML";
9.12 -
9.13 -(*actual syntax module*)
9.14 use "lexicon.ML";
9.15 use "token_trans.ML";
9.16 use "ast.ML";
10.1 --- a/src/Pure/Syntax/pretty.ML Wed Jan 13 12:16:34 1999 +0100
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,249 +0,0 @@
10.4 -(* Title: Pure/Syntax/pretty.ML
10.5 - ID: $Id$
10.6 - Author: Lawrence C Paulson
10.7 - Copyright 1991 University of Cambridge
10.8 -
10.9 -Generic pretty printing module.
10.10 -
10.11 -Loosely based on
10.12 - D. C. Oppen, "Pretty Printing",
10.13 - ACM Transactions on Programming Languages and Systems (1980), 465-483.
10.14 -
10.15 -The object to be printed is given as a tree with indentation and line
10.16 -breaking information. A "break" inserts a newline if the text until
10.17 -the next break is too long to fit on the current line. After the newline,
10.18 -text is indented to the level of the enclosing block. Normally, if a block
10.19 -is broken then all enclosing blocks will also be broken. Only "inconsistent
10.20 -breaks" are provided.
10.21 -
10.22 -The stored length of a block is used in breakdist (to treat each inner block as
10.23 -a unit for breaking).
10.24 -*)
10.25 -
10.26 -type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
10.27 - (unit -> unit) * (unit -> unit);
10.28 -
10.29 -signature PRETTY =
10.30 - sig
10.31 - type T
10.32 - val str: string -> T
10.33 - val strlen: string -> int -> T
10.34 - val sym: string -> T
10.35 - val spc: int -> T
10.36 - val brk: int -> T
10.37 - val fbrk: T
10.38 - val blk: int * T list -> T
10.39 - val lst: string * string -> T list -> T
10.40 - val quote: T -> T
10.41 - val commas: T list -> T list
10.42 - val breaks: T list -> T list
10.43 - val fbreaks: T list -> T list
10.44 - val block: T list -> T
10.45 - val strs: string list -> T
10.46 - val enclose: string -> string -> T list -> T
10.47 - val list: string -> string -> T list -> T
10.48 - val str_list: string -> string -> string list -> T
10.49 - val big_list: string -> T list -> T
10.50 - val string_of: T -> string
10.51 - val writeln: T -> unit
10.52 - val str_of: T -> string
10.53 - val pprint: T -> pprint_args -> unit
10.54 - val setdepth: int -> unit
10.55 - val setmargin: int -> unit
10.56 - end;
10.57 -
10.58 -structure Pretty : PRETTY =
10.59 -struct
10.60 -
10.61 -(*printing items: compound phrases, strings, and breaks*)
10.62 -datatype T =
10.63 - Block of T list * int * int | (*body, indentation, length*)
10.64 - String of string * int | (*text, length*)
10.65 - Break of bool * int; (*mandatory flag, width if not taken*);
10.66 -
10.67 -(*Add the lengths of the expressions until the next Break; if no Break then
10.68 - include "after", to account for text following this block. *)
10.69 -fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after)
10.70 - | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
10.71 - | breakdist (Break _ :: es, after) = 0
10.72 - | breakdist ([], after) = after;
10.73 -
10.74 -fun repstring a 0 = ""
10.75 - | repstring a 1 = a
10.76 - | repstring a k =
10.77 - if k mod 2 = 0 then repstring(a^a) (k div 2)
10.78 - else repstring(a^a) (k div 2) ^ a;
10.79 -
10.80 -(*** Type for lines of text: string, # of lines, position on line ***)
10.81 -
10.82 -type text = {tx: string, nl: int, pos: int};
10.83 -
10.84 -val emptytext = {tx="", nl=0, pos=0};
10.85 -
10.86 -fun blanks wd {tx,nl,pos} =
10.87 - {tx = tx ^ repstring " " wd,
10.88 - nl = nl,
10.89 - pos = pos+wd};
10.90 -
10.91 -fun newline {tx,nl,pos} =
10.92 - {tx = tx ^ "\n",
10.93 - nl = nl+1,
10.94 - pos = 0};
10.95 -
10.96 -fun string s len {tx,nl,pos:int} =
10.97 - {tx = tx ^ s,
10.98 - nl = nl,
10.99 - pos = pos + len};
10.100 -
10.101 -
10.102 -(*** Formatting ***)
10.103 -
10.104 -(* margin *)
10.105 -
10.106 -(*example values*)
10.107 -val margin = ref 80 (*right margin, or page width*)
10.108 -and breakgain = ref 4 (*minimum added space required of a break*)
10.109 -and emergencypos = ref 40; (*position too far to right*)
10.110 -
10.111 -fun setmargin m =
10.112 - (margin := m;
10.113 - breakgain := !margin div 20;
10.114 - emergencypos := !margin div 2);
10.115 -
10.116 -val () = setmargin 76;
10.117 -
10.118 -
10.119 -(*Search for the next break (at this or higher levels) and force it to occur*)
10.120 -fun forcenext [] = []
10.121 - | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
10.122 - | forcenext (e :: es) = e :: forcenext es;
10.123 -
10.124 -(*es is list of expressions to print;
10.125 - blockin is the indentation of the current block;
10.126 - after is the width of the following context until next break. *)
10.127 -fun format ([], _, _) text = text
10.128 - | format (e::es, blockin, after) (text as {pos,nl,...}) =
10.129 - (case e of
10.130 - Block(bes,indent,wd) =>
10.131 - let val blockin' = (pos + indent) mod !emergencypos
10.132 - val btext = format(bes, blockin', breakdist(es,after)) text
10.133 - (*If this block was broken then force the next break.*)
10.134 - val es2 = if nl < #nl(btext) then forcenext es else es
10.135 - in format (es2,blockin,after) btext end
10.136 - | String (s, len) => format (es,blockin,after) (string s len text)
10.137 - | Break(force,wd) => (*no break if text to next break fits on this line
10.138 - or if breaking would add only breakgain to space *)
10.139 - format (es,blockin,after)
10.140 - (if not force andalso
10.141 - pos+wd <= Int.max(!margin - breakdist(es,after),
10.142 - blockin + !breakgain)
10.143 - then blanks wd text (*just insert wd blanks*)
10.144 - else blanks blockin (newline text)));
10.145 -
10.146 -
10.147 -(*** Exported functions to create formatting expressions ***)
10.148 -
10.149 -fun length (Block (_, _, len)) = len
10.150 - | length (String (_, len)) = len
10.151 - | length (Break(_, wd)) = wd;
10.152 -
10.153 -fun str s = String (s, size s);
10.154 -fun strlen s len = String (s, len);
10.155 -fun sym s = String (s, Symbol.size s);
10.156 -
10.157 -fun spc n = str (repstring " " n);
10.158 -
10.159 -fun brk wd = Break (false, wd);
10.160 -val fbrk = Break (true, 0);
10.161 -
10.162 -fun blk (indent, es) =
10.163 - let
10.164 - fun sum([], k) = k
10.165 - | sum(e :: es, k) = sum (es, length e + k);
10.166 - in Block (es, indent, sum (es, 0)) end;
10.167 -
10.168 -(*Join the elements of es as a comma-separated list, bracketted by lp and rp*)
10.169 -fun lst(lp,rp) es =
10.170 - let fun add(e,es) = str"," :: brk 1 :: e :: es;
10.171 - fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
10.172 - | list(e::[]) = [str lp, e, str rp]
10.173 - | list([]) = []
10.174 - in blk(size lp, list es) end;
10.175 -
10.176 -
10.177 -(* utils *)
10.178 -
10.179 -fun quote prt =
10.180 - blk (1, [str "\"", prt, str "\""]);
10.181 -
10.182 -fun commas prts =
10.183 - flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
10.184 -
10.185 -fun breaks prts = separate (brk 1) prts;
10.186 -
10.187 -fun fbreaks prts = separate fbrk prts;
10.188 -
10.189 -fun block prts = blk (2, prts);
10.190 -
10.191 -val strs = block o breaks o (map str);
10.192 -
10.193 -fun enclose lpar rpar prts =
10.194 - block (str lpar :: (prts @ [str rpar]));
10.195 -
10.196 -fun list lpar rpar prts =
10.197 - enclose lpar rpar (commas prts);
10.198 -
10.199 -fun str_list lpar rpar strs =
10.200 - list lpar rpar (map str strs);
10.201 -
10.202 -fun big_list name prts =
10.203 - block (fbreaks (str name :: prts));
10.204 -
10.205 -
10.206 -
10.207 -(*** Pretty printing with depth limitation ***)
10.208 -
10.209 -val depth = ref 0; (*maximum depth; 0 means no limit*)
10.210 -
10.211 -fun setdepth dp = (depth := dp);
10.212 -
10.213 -(*Recursively prune blocks, discarding all text exceeding depth dp*)
10.214 -fun pruning dp (Block(bes,indent,wd)) =
10.215 - if dp>0 then blk(indent, map (pruning(dp-1)) bes)
10.216 - else str "..."
10.217 - | pruning dp e = e;
10.218 -
10.219 -fun prune dp e = if dp>0 then pruning dp e else e;
10.220 -
10.221 -
10.222 -fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext);
10.223 -
10.224 -val writeln = writeln o string_of;
10.225 -
10.226 -
10.227 -(*Create a single flat string: no line breaking*)
10.228 -fun str_of prt =
10.229 - let
10.230 - fun s_of (Block (prts, _, _)) = implode (map s_of prts)
10.231 - | s_of (String (s, _)) = s
10.232 - | s_of (Break (false, wd)) = repstring " " wd
10.233 - | s_of (Break (true, _)) = " ";
10.234 - in
10.235 - s_of (prune (! depth) prt)
10.236 - end;
10.237 -
10.238 -(*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
10.239 -fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
10.240 - let
10.241 - fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
10.242 - | pp (String (s, _)) = put_str s
10.243 - | pp (Break (false, wd)) = put_brk wd
10.244 - | pp (Break (true, _)) = put_fbrk ()
10.245 - and pp_lst [] = ()
10.246 - | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
10.247 - in
10.248 - pp (prune (! depth) prt)
10.249 - end;
10.250 -
10.251 -
10.252 -end;
11.1 --- a/src/Pure/Syntax/scan.ML Wed Jan 13 12:16:34 1999 +0100
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,305 +0,0 @@
11.4 -(* Title: Pure/Syntax/scan.ML
11.5 - ID: $Id$
11.6 - Author: Markus Wenzel and Tobias Nipkow, TU Muenchen
11.7 -
11.8 -Generic scanners (for potentially infinite input).
11.9 -*)
11.10 -
11.11 -infix 5 -- :-- |-- --| ^^;
11.12 -infix 3 >>;
11.13 -infix 0 ||;
11.14 -
11.15 -signature BASIC_SCAN =
11.16 -sig
11.17 - val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b
11.18 - val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
11.19 - val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
11.20 - val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
11.21 - val :-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
11.22 - val |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e
11.23 - val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e
11.24 - val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
11.25 - val $$ : ''a -> ''a list -> ''a * ''a list
11.26 -end;
11.27 -
11.28 -signature SCAN =
11.29 -sig
11.30 - include BASIC_SCAN
11.31 - val fail: 'a -> 'b
11.32 - val fail_with: ('a -> string) -> 'a -> 'b
11.33 - val succeed: 'a -> 'b -> 'a * 'b
11.34 - val one: ('a -> bool) -> 'a list -> 'a * 'a list
11.35 - val any: ('a -> bool) -> 'a list -> 'a list * 'a list
11.36 - val any1: ('a -> bool) -> 'a list -> 'a list * 'a list
11.37 - val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a
11.38 - val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
11.39 - val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
11.40 - val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
11.41 - val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
11.42 - val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
11.43 - val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd
11.44 - val first: ('a -> 'b) list -> 'a -> 'b
11.45 - val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
11.46 - val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
11.47 - val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
11.48 - val try: ('a -> 'b) -> 'a -> 'b
11.49 - val force: ('a -> 'b) -> 'a -> 'b
11.50 - val prompt: string -> ('a -> 'b) -> 'a -> 'b
11.51 - val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list))
11.52 - -> 'b * 'a list -> 'c * ('d * 'a list)
11.53 - val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
11.54 - val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
11.55 - val catch: ('a -> 'b) -> 'a -> 'b
11.56 - val error: ('a -> 'b) -> 'a -> 'b
11.57 - val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
11.58 - 'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
11.59 - ('d * 'b list -> 'f * ('d * 'b list)) option -> 'd * 'a -> 'e list * ('d * 'c)
11.60 - val source: string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
11.61 - 'b * ('b -> bool) -> ('b list -> 'd list * 'b list) ->
11.62 - ('b list -> 'e * 'b list) option -> 'a -> 'd list * 'c
11.63 - val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
11.64 - val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
11.65 - type lexicon
11.66 - val dest_lexicon: lexicon -> string list list
11.67 - val make_lexicon: string list list -> lexicon
11.68 - val empty_lexicon: lexicon
11.69 - val extend_lexicon: lexicon -> string list list -> lexicon
11.70 - val merge_lexicons: lexicon -> lexicon -> lexicon
11.71 - val literal: lexicon -> string list -> string list * string list
11.72 -end;
11.73 -
11.74 -structure Scan: SCAN =
11.75 -struct
11.76 -
11.77 -
11.78 -(** scanners **)
11.79 -
11.80 -exception MORE of string option; (*need more input (prompt)*)
11.81 -exception FAIL of string option; (*try alternatives (reason of failure)*)
11.82 -exception ABORT of string; (*dead end*)
11.83 -
11.84 -
11.85 -(* scanner combinators *)
11.86 -
11.87 -fun (scan >> f) xs = apfst f (scan xs);
11.88 -
11.89 -fun (scan1 || scan2) xs = scan1 xs handle FAIL _ => scan2 xs;
11.90 -
11.91 -(*dependent pairing*)
11.92 -fun (scan1 :-- scan2) xs =
11.93 - let
11.94 - val (x, ys) = scan1 xs;
11.95 - val (y, zs) = scan2 x ys;
11.96 - in ((x, y), zs) end;
11.97 -
11.98 -fun (scan1 -- scan2) = scan1 :-- (fn _ => scan2);
11.99 -fun (scan1 |-- scan2) = scan1 -- scan2 >> #2;
11.100 -fun (scan1 --| scan2) = scan1 -- scan2 >> #1;
11.101 -fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^;
11.102 -
11.103 -
11.104 -(* generic scanners *)
11.105 -
11.106 -fun fail _ = raise FAIL None;
11.107 -fun fail_with msg_of xs = raise FAIL (Some (msg_of xs));
11.108 -fun succeed y xs = (y, xs);
11.109 -
11.110 -fun one _ [] = raise MORE None
11.111 - | one pred (x :: xs) =
11.112 - if pred x then (x, xs) else raise FAIL None;
11.113 -
11.114 -fun $$ _ [] = raise MORE None
11.115 - | $$ a (x :: xs) =
11.116 - if a = x then (x, xs) else raise FAIL None;
11.117 -
11.118 -fun any _ [] = raise MORE None
11.119 - | any pred (lst as x :: xs) =
11.120 - if pred x then apfst (cons x) (any pred xs)
11.121 - else ([], lst);
11.122 -
11.123 -fun any1 pred = one pred -- any pred >> op ::;
11.124 -
11.125 -fun optional scan def = scan || succeed def;
11.126 -fun option scan = optional (scan >> Some) None;
11.127 -
11.128 -fun repeat scan xs = (scan -- repeat scan >> op :: || succeed []) xs;
11.129 -fun repeat1 scan = scan -- repeat scan >> op ::;
11.130 -
11.131 -fun max leq scan1 scan2 xs =
11.132 - (case (option scan1 xs, option scan2 xs) of
11.133 - ((None, _), (None, _)) => raise FAIL None (*looses FAIL msg!*)
11.134 - | ((Some tok1, xs'), (None, _)) => (tok1, xs')
11.135 - | ((None, _), (Some tok2, xs')) => (tok2, xs')
11.136 - | ((Some tok1, xs1'), (Some tok2, xs2')) =>
11.137 - if leq (tok2, tok1) then (tok1, xs1') else (tok2, xs2'));
11.138 -
11.139 -fun ahead scan xs = (fst (scan xs), xs);
11.140 -
11.141 -fun unless test scan =
11.142 - ahead (option test) :-- (fn None => scan | _ => fail) >> #2;
11.143 -
11.144 -fun first [] = fail
11.145 - | first (scan :: scans) = scan || first scans;
11.146 -
11.147 -
11.148 -(* state based scanners *)
11.149 -
11.150 -fun depend scan (st, xs) =
11.151 - let val ((st', y), xs') = scan st xs
11.152 - in (y, (st', xs')) end;
11.153 -
11.154 -fun lift scan (st, xs) =
11.155 - let val (y, xs') = scan xs
11.156 - in (y, (st, xs')) end;
11.157 -
11.158 -fun pass st scan xs =
11.159 - let val (y, (_, xs')) = scan (st, xs)
11.160 - in (y, xs') end;
11.161 -
11.162 -
11.163 -(* exception handling *)
11.164 -
11.165 -fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
11.166 -fun try scan xs = scan xs handle MORE _ => raise FAIL None | ABORT _ => raise FAIL None;
11.167 -fun force scan xs = scan xs handle MORE _ => raise FAIL None;
11.168 -fun prompt str scan xs = scan xs handle MORE None => raise MORE (Some str);
11.169 -fun catch scan xs = scan xs handle ABORT msg => raise FAIL (Some msg);
11.170 -fun error scan xs = scan xs handle ABORT msg => Library.error msg;
11.171 -
11.172 -
11.173 -(* finite scans *)
11.174 -
11.175 -fun finite' (stopper, is_stopper) scan (state, input) =
11.176 - let
11.177 - fun lost () = raise ABORT "Scanner bug: lost stopper of finite scan!";
11.178 -
11.179 - fun stop [] = lost ()
11.180 - | stop lst =
11.181 - let val (xs, x) = split_last lst
11.182 - in if is_stopper x then ((), xs) else lost () end;
11.183 - in
11.184 - if exists is_stopper input then
11.185 - raise ABORT "Stopper may not occur in input of finite scan!"
11.186 - else (force scan --| lift stop) (state, input @ [stopper])
11.187 - end;
11.188 -
11.189 -fun finite stopper scan xs =
11.190 - let val (y, ((), xs')) = finite' stopper (lift scan) ((), xs)
11.191 - in (y, xs') end;
11.192 -
11.193 -fun read stopper scan xs =
11.194 - (case error (finite stopper (option scan)) xs of
11.195 - (y as Some _, []) => y
11.196 - | _ => None);
11.197 -
11.198 -
11.199 -
11.200 -(* infinite scans -- draining state-based source *)
11.201 -
11.202 -fun drain def_prmpt get stopper scan ((state, xs), src) =
11.203 - (scan (state, xs), src) handle MORE prmpt =>
11.204 - (case get (if_none prmpt def_prmpt) src of
11.205 - ([], _) => (finite' stopper scan (state, xs), src)
11.206 - | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src'));
11.207 -
11.208 -fun source' def_prmpt get unget stopper scanner opt_recover (state, src) =
11.209 - let
11.210 - fun drain_with scan = drain def_prmpt get stopper scan;
11.211 -
11.212 - fun drain_loop recover inp =
11.213 - drain_with (catch scanner) inp handle FAIL msg =>
11.214 - (error_msg (if_none msg "Syntax error.");
11.215 - drain_loop recover (apfst snd (drain_with recover inp)));
11.216 -
11.217 - val ((ys, (state', xs')), src') =
11.218 - (case (get def_prmpt src, opt_recover) of
11.219 - (([], s), _) => (([], (state, [])), s)
11.220 - | ((xs, s), None) => drain_with (error scanner) ((state, xs), s)
11.221 - | ((xs, s), Some scan) => drain_loop scan ((state, xs), s));
11.222 - in
11.223 - (ys, (state', unget (xs', src')))
11.224 - end;
11.225 -
11.226 -fun source def_prmpt get unget stopper scan opt_recover src =
11.227 - let val (ys, ((), src')) =
11.228 - source' def_prmpt get unget stopper (lift scan) (apsome lift opt_recover) ((), src)
11.229 - in (ys, src') end;
11.230 -
11.231 -fun single scan = scan >> (fn x => [x]);
11.232 -fun bulk scan = scan -- repeat (try scan) >> (op ::);
11.233 -
11.234 -
11.235 -
11.236 -(** datatype lexicon **)
11.237 -
11.238 -datatype lexicon =
11.239 - Empty |
11.240 - Branch of string * string list * lexicon * lexicon * lexicon;
11.241 -
11.242 -val no_literal = [];
11.243 -
11.244 -
11.245 -(* dest_lexicon *)
11.246 -
11.247 -fun dest_lexicon Empty = []
11.248 - | dest_lexicon (Branch (_, [], lt, eq, gt)) =
11.249 - dest_lexicon lt @ dest_lexicon eq @ dest_lexicon gt
11.250 - | dest_lexicon (Branch (_, cs, lt, eq, gt)) =
11.251 - dest_lexicon lt @ [cs] @ dest_lexicon eq @ dest_lexicon gt;
11.252 -
11.253 -
11.254 -(* empty, extend, make, merge lexicons *)
11.255 -
11.256 -val empty_lexicon = Empty;
11.257 -
11.258 -fun extend_lexicon lexicon chrss =
11.259 - let
11.260 - fun ext (lex, chrs) =
11.261 - let
11.262 - fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
11.263 - if c < d then Branch (d, a, add lt chs, eq, gt)
11.264 - else if c > d then Branch (d, a, lt, eq, add gt chs)
11.265 - else Branch (d, if null cs then chrs else a, lt, add eq cs, gt)
11.266 - | add Empty [c] =
11.267 - Branch (c, chrs, Empty, Empty, Empty)
11.268 - | add Empty (c :: cs) =
11.269 - Branch (c, no_literal, Empty, add Empty cs, Empty)
11.270 - | add lex [] = lex;
11.271 - in add lex chrs end;
11.272 - in foldl ext (lexicon, chrss \\ dest_lexicon lexicon) end;
11.273 -
11.274 -val make_lexicon = extend_lexicon empty_lexicon;
11.275 -
11.276 -fun merge_lexicons lex1 lex2 =
11.277 - let
11.278 - val chss1 = dest_lexicon lex1;
11.279 - val chss2 = dest_lexicon lex2;
11.280 - in
11.281 - if chss2 subset chss1 then lex1
11.282 - else if chss1 subset chss2 then lex2
11.283 - else extend_lexicon lex1 chss2
11.284 - end;
11.285 -
11.286 -
11.287 -(* scan literal *)
11.288 -
11.289 -fun literal lex chrs =
11.290 - let
11.291 - fun lit Empty res _ = res
11.292 - | lit (Branch _) _ [] = raise MORE None
11.293 - | lit (Branch (d, a, lt, eq, gt)) res (chs as c :: cs) =
11.294 - if c < d then lit lt res chs
11.295 - else if c > d then lit gt res chs
11.296 - else lit eq (if a = no_literal then res else Some (a, cs)) cs;
11.297 - in
11.298 - (case lit lex None chrs of
11.299 - None => raise FAIL None
11.300 - | Some res => res)
11.301 - end;
11.302 -
11.303 -
11.304 -end;
11.305 -
11.306 -
11.307 -structure BasicScan: BASIC_SCAN = Scan;
11.308 -open BasicScan;
12.1 --- a/src/Pure/Syntax/source.ML Wed Jan 13 12:16:34 1999 +0100
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,150 +0,0 @@
12.4 -(* Title: Pure/Syntax/source.ML
12.5 - ID: $Id$
12.6 - Author: Markus Wenzel, TU Muenchen
12.7 -
12.8 -Co-algebraic data sources.
12.9 -*)
12.10 -
12.11 -signature SOURCE =
12.12 -sig
12.13 - type ('a, 'b) source
12.14 - val set_prompt: string -> ('a, 'b) source -> ('a, 'b) source
12.15 - val get: ('a, 'b) source -> 'a list * ('a, 'b) source
12.16 - val unget: 'a list * ('a, 'b) source -> ('a, 'b) source
12.17 - val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option
12.18 - val exhaust: ('a, 'b) source -> 'a list
12.19 - val mapfilter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source
12.20 - val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source
12.21 - val of_list: 'a list -> ('a, 'a list) source
12.22 - val of_string: string -> (string, string list) source
12.23 - val of_file: string -> (string, string list) source
12.24 - val decorate_prompt_fn: (string -> string) ref
12.25 - val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
12.26 - val tty: (string, unit) source
12.27 - val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
12.28 - ('a * 'b list -> 'd * ('a * 'b list)) option ->
12.29 - ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
12.30 - val source: 'a * ('a -> bool) -> ('a list -> 'b list * 'a list) ->
12.31 - ('a list -> 'c * 'a list) option ->
12.32 - ('a, 'd) source -> ('b, ('a, 'd) source) source
12.33 -end;
12.34 -
12.35 -structure Source: SOURCE =
12.36 -struct
12.37 -
12.38 -
12.39 -(** datatype source **)
12.40 -
12.41 -datatype ('a, 'b) source =
12.42 - Source of
12.43 - {buffer: 'a list,
12.44 - info: 'b,
12.45 - prompt: string,
12.46 - drain: string -> 'b -> 'a list * 'b};
12.47 -
12.48 -fun make_source buffer info prompt drain =
12.49 - Source {buffer = buffer, info = info, prompt = prompt, drain = drain};
12.50 -
12.51 -
12.52 -(* prompt *)
12.53 -
12.54 -val default_prompt = "> ";
12.55 -
12.56 -fun set_prompt prompt (Source {buffer, info, prompt = _, drain}) =
12.57 - make_source buffer info prompt drain;
12.58 -
12.59 -
12.60 -(* get / unget *)
12.61 -
12.62 -fun get (Source {buffer = [], info, prompt, drain}) =
12.63 - let val (xs, info') = drain prompt info
12.64 - in (xs, make_source [] info' prompt drain) end
12.65 - | get (Source {buffer, info, prompt, drain}) =
12.66 - (buffer, make_source [] info prompt drain);
12.67 -
12.68 -fun unget (xs, Source {buffer, info, prompt, drain}) =
12.69 - make_source (xs @ buffer) info prompt drain;
12.70 -
12.71 -
12.72 -(* variations on get *)
12.73 -
12.74 -fun get_prompt prompt src = get (set_prompt prompt src);
12.75 -
12.76 -fun get_single src =
12.77 - (case get src of
12.78 - ([], _) => None
12.79 - | (x :: xs, src') => Some (x, unget (xs, src')));
12.80 -
12.81 -fun exhaust src =
12.82 - (case get src of
12.83 - ([], _) => []
12.84 - | (xs, src') => xs @ exhaust src');
12.85 -
12.86 -
12.87 -(* (map)filter *)
12.88 -
12.89 -fun drain_mapfilter f prompt src =
12.90 - let
12.91 - val (xs, src') = get_prompt prompt src;
12.92 - val xs' = Library.mapfilter f xs;
12.93 - in
12.94 - if null xs orelse not (null xs') then (xs', src')
12.95 - else drain_mapfilter f prompt src'
12.96 - end;
12.97 -
12.98 -fun mapfilter f src = make_source [] src default_prompt (drain_mapfilter f);
12.99 -fun filter pred = mapfilter (fn x => if pred x then Some x else None);
12.100 -
12.101 -
12.102 -
12.103 -(** build sources **)
12.104 -
12.105 -(* list source *)
12.106 -
12.107 -(*limiting the input buffer considerably improves performance*)
12.108 -val limit = 4000;
12.109 -
12.110 -fun drain_list _ xs = (take (limit, xs), drop (limit, xs));
12.111 -
12.112 -fun of_list xs = make_source [] xs default_prompt drain_list;
12.113 -val of_string = of_list o explode;
12.114 -val of_file = of_string o File.read;
12.115 -
12.116 -
12.117 -(* stream source *)
12.118 -
12.119 -val decorate_prompt_fn = ref (fn s:string => s);
12.120 -
12.121 -fun drain_stream instream outstream prompt () =
12.122 - (TextIO.output (outstream, ! decorate_prompt_fn prompt);
12.123 - TextIO.flushOut outstream;
12.124 - (explode (TextIO.inputLine instream), ()));
12.125 -
12.126 -fun of_stream instream outstream =
12.127 - make_source [] () default_prompt (drain_stream instream outstream);
12.128 -
12.129 -val tty = of_stream TextIO.stdIn TextIO.stdOut;
12.130 -
12.131 -
12.132 -
12.133 -(** compose sources **)
12.134 -
12.135 -fun drain_source source stopper scan recover prompt src =
12.136 - source prompt get_prompt unget stopper scan recover src;
12.137 -
12.138 -
12.139 -(* state-based *)
12.140 -
12.141 -fun source' init_state stopper scan recover src =
12.142 - make_source [] (init_state, src) default_prompt
12.143 - (drain_source Scan.source' stopper scan recover);
12.144 -
12.145 -
12.146 -(* non state-based *)
12.147 -
12.148 -fun source stopper scan recover src =
12.149 - make_source [] src default_prompt
12.150 - (drain_source Scan.source stopper scan recover);
12.151 -
12.152 -
12.153 -end;
13.1 --- a/src/Pure/Syntax/symbol.ML Wed Jan 13 12:16:34 1999 +0100
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,274 +0,0 @@
13.4 -(* Title: Pure/Syntax/symbol.ML
13.5 - ID: $Id$
13.6 - Author: Markus Wenzel, TU Muenchen
13.7 -
13.8 -Generalized characters.
13.9 -*)
13.10 -
13.11 -signature SYMBOL =
13.12 -sig
13.13 - type symbol
13.14 - val space: symbol
13.15 - val eof: symbol
13.16 - val is_eof: symbol -> bool
13.17 - val not_eof: symbol -> bool
13.18 - val stopper: symbol * (symbol -> bool)
13.19 - val is_ascii: symbol -> bool
13.20 - val is_letter: symbol -> bool
13.21 - val is_digit: symbol -> bool
13.22 - val is_quasi_letter: symbol -> bool
13.23 - val is_letdig: symbol -> bool
13.24 - val is_blank: symbol -> bool
13.25 - val is_printable: symbol -> bool
13.26 - val beginning: symbol list -> string
13.27 - val scan: string list -> symbol * string list
13.28 - val explode: string -> symbol list
13.29 - val length: symbol list -> int
13.30 - val size: string -> int
13.31 - val input: string -> string
13.32 - val output: string -> string
13.33 - val source: bool -> (string, 'a) Source.source ->
13.34 - (symbol, (string, 'a) Source.source) Source.source
13.35 -end;
13.36 -
13.37 -structure Symbol: SYMBOL =
13.38 -struct
13.39 -
13.40 -
13.41 -(** encoding table (isabelle-0) **)
13.42 -
13.43 -val enc_start = 160;
13.44 -val enc_end = 255;
13.45 -
13.46 -val enc_vector =
13.47 -[
13.48 -(* GENERATED TEXT FOLLOWS - Do not edit! *)
13.49 - "\\<space2>",
13.50 - "\\<Gamma>",
13.51 - "\\<Delta>",
13.52 - "\\<Theta>",
13.53 - "\\<Lambda>",
13.54 - "\\<Pi>",
13.55 - "\\<Sigma>",
13.56 - "\\<Phi>",
13.57 - "\\<Psi>",
13.58 - "\\<Omega>",
13.59 - "\\<alpha>",
13.60 - "\\<beta>",
13.61 - "\\<gamma>",
13.62 - "\\<delta>",
13.63 - "\\<epsilon>",
13.64 - "\\<zeta>",
13.65 - "\\<eta>",
13.66 - "\\<theta>",
13.67 - "\\<kappa>",
13.68 - "\\<lambda>",
13.69 - "\\<mu>",
13.70 - "\\<nu>",
13.71 - "\\<xi>",
13.72 - "\\<pi>",
13.73 - "\\<rho>",
13.74 - "\\<sigma>",
13.75 - "\\<tau>",
13.76 - "\\<phi>",
13.77 - "\\<chi>",
13.78 - "\\<psi>",
13.79 - "\\<omega>",
13.80 - "\\<not>",
13.81 - "\\<and>",
13.82 - "\\<or>",
13.83 - "\\<forall>",
13.84 - "\\<exists>",
13.85 - "\\<And>",
13.86 - "\\<lceil>",
13.87 - "\\<rceil>",
13.88 - "\\<lfloor>",
13.89 - "\\<rfloor>",
13.90 - "\\<turnstile>",
13.91 - "\\<Turnstile>",
13.92 - "\\<lbrakk>",
13.93 - "\\<rbrakk>",
13.94 - "\\<cdot>",
13.95 - "\\<in>",
13.96 - "\\<subseteq>",
13.97 - "\\<inter>",
13.98 - "\\<union>",
13.99 - "\\<Inter>",
13.100 - "\\<Union>",
13.101 - "\\<sqinter>",
13.102 - "\\<squnion>",
13.103 - "\\<Sqinter>",
13.104 - "\\<Squnion>",
13.105 - "\\<bottom>",
13.106 - "\\<doteq>",
13.107 - "\\<equiv>",
13.108 - "\\<noteq>",
13.109 - "\\<sqsubset>",
13.110 - "\\<sqsubseteq>",
13.111 - "\\<prec>",
13.112 - "\\<preceq>",
13.113 - "\\<succ>",
13.114 - "\\<approx>",
13.115 - "\\<sim>",
13.116 - "\\<simeq>",
13.117 - "\\<le>",
13.118 - "\\<Colon>",
13.119 - "\\<leftarrow>",
13.120 - "\\<midarrow>",
13.121 - "\\<rightarrow>",
13.122 - "\\<Leftarrow>",
13.123 - "\\<Midarrow>",
13.124 - "\\<Rightarrow>",
13.125 - "\\<bow>",
13.126 - "\\<mapsto>",
13.127 - "\\<leadsto>",
13.128 - "\\<up>",
13.129 - "\\<down>",
13.130 - "\\<notin>",
13.131 - "\\<times>",
13.132 - "\\<oplus>",
13.133 - "\\<ominus>",
13.134 - "\\<otimes>",
13.135 - "\\<oslash>",
13.136 - "\\<subset>",
13.137 - "\\<infinity>",
13.138 - "\\<box>",
13.139 - "\\<diamond>",
13.140 - "\\<circ>",
13.141 - "\\<bullet>",
13.142 - "\\<parallel>",
13.143 - "\\<surd>",
13.144 - "\\<copyright>"
13.145 -(* END OF GENERATED TEXT *)
13.146 -];
13.147 -
13.148 -val enc_rel = enc_vector ~~ map chr (enc_start upto enc_end);
13.149 -
13.150 -val char_tab = Symtab.make enc_rel;
13.151 -val symbol_tab = Symtab.make (map swap enc_rel);
13.152 -
13.153 -fun lookup_symbol c =
13.154 - if ord c < enc_start then None
13.155 - else Symtab.lookup (symbol_tab, c);
13.156 -
13.157 -
13.158 -(* encode / decode *)
13.159 -
13.160 -fun char s = if_none (Symtab.lookup (char_tab, s)) s;
13.161 -fun symbol c = if_none (lookup_symbol c) c;
13.162 -
13.163 -fun symbol' c =
13.164 - (case lookup_symbol c of
13.165 - None => c
13.166 - | Some s => "\\" ^ s);
13.167 -
13.168 -
13.169 -
13.170 -(** type symbol **)
13.171 -
13.172 -type symbol = string;
13.173 -
13.174 -val space = " ";
13.175 -val eof = "";
13.176 -
13.177 -
13.178 -(* kinds *)
13.179 -
13.180 -fun is_eof s = s = eof;
13.181 -fun not_eof s = s <> eof;
13.182 -val stopper = (eof, is_eof);
13.183 -
13.184 -fun is_ascii s = size s = 1 andalso ord s < 128;
13.185 -
13.186 -fun is_letter s =
13.187 - size s = 1 andalso
13.188 - (ord "A" <= ord s andalso ord s <= ord "Z" orelse
13.189 - ord "a" <= ord s andalso ord s <= ord "z");
13.190 -
13.191 -fun is_digit s =
13.192 - size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9";
13.193 -
13.194 -fun is_quasi_letter "_" = true
13.195 - | is_quasi_letter "'" = true
13.196 - | is_quasi_letter s = is_letter s;
13.197 -
13.198 -val is_blank =
13.199 - fn " " => true | "\t" => true | "\n" => true | "\^L" => true
13.200 - | "\160" => true | "\\<space2>" => true
13.201 - | _ => false;
13.202 -
13.203 -val is_letdig = is_quasi_letter orf is_digit;
13.204 -
13.205 -fun is_printable s =
13.206 - size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse
13.207 - size s > 2 andalso nth_elem (2, explode s) <> "^";
13.208 -
13.209 -
13.210 -(* beginning *)
13.211 -
13.212 -val smash_blanks = map (fn s => if is_blank s then space else s);
13.213 -
13.214 -fun beginning raw_ss =
13.215 - let
13.216 - val (all_ss, _) = take_suffix is_blank raw_ss;
13.217 - val dots = if length all_ss > 10 then " ..." else "";
13.218 - val (ss, _) = take_suffix is_blank (take (10, all_ss));
13.219 - in implode (smash_blanks ss) ^ dots end;
13.220 -
13.221 -
13.222 -(* scan *)
13.223 -
13.224 -val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
13.225 -
13.226 -val scan =
13.227 - ($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
13.228 - !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs)
13.229 - (Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") ||
13.230 - Scan.one not_eof;
13.231 -
13.232 -
13.233 -(* source *)
13.234 -
13.235 -val recover = Scan.any1 ((not o is_blank) andf not_eof);
13.236 -
13.237 -fun source do_recover src =
13.238 - Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src;
13.239 -
13.240 -
13.241 -(* explode *)
13.242 -
13.243 -fun no_syms [] = true
13.244 - | no_syms ("\\" :: "<" :: _) = false
13.245 - | no_syms (c :: cs) = ord c < enc_start andalso no_syms cs;
13.246 -
13.247 -fun sym_explode str =
13.248 - let val chs = explode str in
13.249 - if no_syms chs then chs (*tune trivial case*)
13.250 - else map symbol (the (Scan.read stopper (Scan.repeat scan) chs))
13.251 - end;
13.252 -
13.253 -
13.254 -(* printable length *)
13.255 -
13.256 -fun sym_length ss = foldl (fn (n, c) => if is_printable c then n + 1 else n) (0, ss);
13.257 -val sym_size = sym_length o sym_explode;
13.258 -
13.259 -
13.260 -(* input / output *)
13.261 -
13.262 -fun input str =
13.263 - let val chs = explode str in
13.264 - if forall (fn c => ord c < enc_start) chs then str
13.265 - else implode (map symbol' chs)
13.266 - end;
13.267 -
13.268 -val output = implode o map char o sym_explode;
13.269 -
13.270 -
13.271 -(*final declarations of this structure!*)
13.272 -val explode = sym_explode;
13.273 -val length = sym_length;
13.274 -val size = sym_size;
13.275 -
13.276 -
13.277 -end;