(* conversion program for text, written for changing papers and source files *) fun u _ = use "cvt.ml" ; open List ; load "TextIO" ; open TextIO ; load "CharArray" ; load "MyLib" ; open MyLib ; (* val instr = openIn "cetph.tex" ; val text = inputAll instr ; val () = closeIn instr ; val stext = Substring.all text ; (* make list of substrings, which are maximal strings all of whose characters either do or do not satisfy f *) val toks = Substring.tokens (not o Char.isAlphaNum) stext ; val chars = Substring.explode stext ; val charr = CharArray.fromList chars ; (* changing dtx to dtx - easy, but only for changes where replacement has same number of characters - uses a character array *) fun chtok dtstrs tok = if List.exists (equal (Substring.string tok)) dtstrs then let val (_, i, _) = Substring.base tok ; in CharArray.update (charr, i, #"d") end else () ; fun p2t dtstrs = List.app (chtok dtstrs) toks ; fun p name = let val nchars = CharArray.foldr (op ::) [] charr ; val ntext = String.implode nchars ; val ostr = openOut (name ^ ".tex") ; val () = output (ostr, ntext) ; val () = closeOut ostr ; in () end ; *) (* p2t ["dts"] ; p "a" ; p2t ["dtn"] ; p "b" ; p2t ["dt"] ; p "c" ; p2t ["dtAY", "dtA", "dtY"] ; p "d" ; *) (* a more general string substitution routine *) (* now use set of tokens to deduce what are the non-tokens, and change string accordingly *) (* allss : int -> substring list -> string -> substring list given a starting index start, a list of substrings toks (which are in order and non-overlapping), and the whole string ws (of which the substrings toks are part) return a complete list of substrings (ie, including the gaps between the substrings in toks) *) fun allss start (tok :: toks) ws = let val (s, i, n) = Substring.base tok ; val true = ws = s ; (* assume implementation does this *) in if start < i then Substring.substring (s, start, i - start) :: tok :: allss (i + n) toks ws else if start = i then tok :: allss (i + n) toks ws else raise Fail "allss : start > i" end | allss start [] ws = if start < String.size ws then [Substring.extract (ws, start, NONE)] else if start = String.size ws then [] else raise Fail "allss : start > String.size ws" ; fun test_allss str = let val sstr = Substring.all str ; val ttoks = Substring.tokens (not o Char.isAlphaNum) sstr ; val ttoks' = Substring.tokens (Char.isAlphaNum) sstr ; val ts = allss 0 ttoks str ; val ts' = allss 0 ttoks' str ; val ss = map Substring.string ts ; val s = String.concat ss ; in (map Substring.base ts = map Substring.base ts', str = s) end ; (* subs : (string -> string) -> substring list -> string turn substrings into strings, apply map f, concatenate *) fun subs f toks = let val strs = map (f o Substring.string) toks ; in String.concat strs end ; (* chassoc : (''a * ''a) list -> ''a -> ''a use assoc list (arg1) to change arg2 (if found) otherwise return arg2 *) fun chassoc prs str = case MyLib.assoc prs str of NONE => str | SOME nstr => nstr ; (* trans : (string -> string) -> (char -> bool) -> string -> string tokenize using f, change strings using chs *) fun trans chs f str = let val toks = Substring.tokens f (Substring.all str) ; val allts = allss 0 toks str ; in subs chs allts end ; (* tf : (string -> string) -> string -> string -> unit read file, apply f to contents, write file *) fun tf sf infile ofile = let open TextIO ; val instr = openIn infile ; val text = inputAll instr ; val () = closeIn instr ; val ntext = sf text ; val ostr = openOut ofile ; val () = output (ostr, ntext) ; val () = closeOut ostr ; in () end ; (* tfs : (string -> string) -> string -> unit as tf, but overwrites existing file *) fun tfs sf file = tf sf file file ; (* tf (trans [("Pr", "Der")] Char.isAlphaNum) "d.tex" "e.tex" ; *) load "MyIO" ; open MyIO ; val files = ["Belnap.ML", "SN0.ML", "detab.ml", "HOL_DT.thy", "SN0.thy", "gen.ML", "Belnap.thy", "SN2.ML", "HOL_RA.ML", "lib.ML", "C8cases.ML", "SN2.thy", "C8cases.thy", "HOL_RA.thy", "makeCut.ML", "SNCE.ML", "CutRed.ML", "HOL_Rep.ML", "makeCut.thy", "SNCE.thy", "CutRed.thy", "HOL_Rep.thy", "makefile", "WC8.ML", "meta_proofs.ML", "HOL_C8.ML", "HOL_Rls.ML", "WC8.thy", "meta_proofs.thy", "HOL_C8.thy", "HOL_Rls.thy", "WC8cases.ML", "newSub.ML", "HOL_Cut.ML", "HOL_Sub.ML", "WC8cases.thy", "newSub.thy", "HOL_Cut.thy", "HOL_Sub.thy", "Wansing.ML", "orC8.ML", "HOL_Disp.ML", "HOLinML.ML", "Wansing.thy", "qed.ml", "HOL_Disp.thy", "NP.ML", "Wansing2.ML", "rsC8.ML", "HOL_DispC8.ML", "NP.thy", "Wansing2.thy", "sedscript", "stringSyntax.ML", "HOL_Elim.ML", "DT1.ML", "all.thy", "stringSyntax.thy", "HOL_Elim.thy", "DT_Sub.ML", "andC8.ML", "summ", "HOL_ElimC8.ML", "README", "compC8.ML", "RP.ML", "HOL_ElimC8.thy", "conC8.ML", "RP.thy", "texput.log", "HOL_Gen.ML", "cvt.ml", "torpg2", "SN.ML", "derivs.ML", "unC8.ML", "HOL_Gen.thy", "SN.thy", "derrls.ML", "unify.ML", "HOL_DT.ML"] : string list ; fun f st = let open String in case (sub (st, 0), sub (st, 1)) of (#"p", #"t") => implode (#"d" :: tl (explode st)) | _ => st end handle Subscript => st ; (* val files = ["cutelim.tex"] ; load "ListPair" ; val ps = ["dtl", "dts", "dtn", "dt", "dtAY", "dtA", "dtlA", "dtY"] ; val ds = ["dtl", "dts", "dtn", "dt", "dtAY", "dtA", "dtlA", "dtY"] ; val prs' = ListPair.zip (ps, ds) ; val prs = [("Pr", "Der"), ("pftr", "dtr"), ("pftree", "dertree")] @ prs' ; app (tfs (trans (chassoc prs) Char.isAlpha)) files ; app (tfs (trans (chassoc [("PT", "DT")]) Char.isUpper)) files ; app (tfs (trans f Char.isAlpha)) files ; *)