1(* makebase -- create the signature database from the Moscow ML 2 * library signatures. PS 1995-11-19, 2000-06-29 3 * 4 * Hacked for HOL help system, Konrad Slind, Nov. 2001. 5 *) 6 7structure makebase = struct 8 9fun curry f x y = f (x,y); 10fun single x = [x]; 11 12fun itstrings f [] = raise Fail "itstrings: empty list" 13 | itstrings f [x] = x 14 | itstrings f (h::t) = f h (itstrings f t); 15 16val normPath = (* string list -> string *) 17 OS.Path.toString o OS.Path.fromString o itstrings (curry OS.Path.concat); 18 19fun destProperSuffix s1 s2 = 20 let val sz1 = String.size s1 21 val sz2 = String.size s2 22 open Substring 23 in 24 if sz1 >= sz2 then NONE 25 else let val (prefix, suffix) = splitAt(full s2, sz2 - sz1) 26 in if string suffix = s1 then SOME (string prefix) else NONE 27 end 28 end; 29 30fun isTheory {comp,file=path,line} = 31 let open OS.Path 32 val {dir,file} = splitDirFile path 33 val {base,ext} = splitBaseExt file 34 in Option.isSome (destProperSuffix "Theory" base) 35 end 36 handle _ => false; 37 38fun isSigId {comp=Database.Term(_,SOME"HOL"),file,line} = false 39 | isSigId entry = not (isTheory entry) 40 41 42(*--------------------------------------------------------------------------- 43 Set values 44 ---------------------------------------------------------------------------*) 45(* The version number inserted in generated files: *) 46val version = 47 String.concat ["<a href=\"http://hol.sourceforge.net\">HOL 4, ", 48 Systeml.release, "-", Int.toString Systeml.version, 49 "</a>"] 50 51(* HOL distribution directory: *) 52val HOLpath = normPath [Systeml.HOLDIR]; 53 54(* Default directory containing the signature files: *) 55val libdirDef = normPath[HOLpath,"sigobj"] 56 57(* Default filename for the resulting help database: *) 58val helpfileDef = normPath[HOLpath, "help","HOL.Help"] 59 60(* Default filename for the HOL reference page: *) 61val HOLpageDef = normPath[HOLpath, "help","HOLindex.html"] 62 63(* Default filename for the ASCII format database: *) 64val txtIndexDef = "index.txt" 65 66(* Default filename for the LaTeX format database: *) 67val texIndexDef = "index.tex" 68 69(* Default directory for signatures in HTML format: *) 70val htmlDirDef = "htmlsigs" 71 72(* Default filename for the HTML format database for identifiers: *) 73val htmlIndexDef = normPath[HOLpath,"help","src-sml",htmlDirDef,"idIndex.html"] 74 75(* Default filename for the HTML format database for theories: *) 76val htmlTheoryIndexDef = 77 normPath[HOLpath,"help","src-sml",htmlDirDef,"TheoryIndex.html"] 78 79(* Default filename for the LaTeX signatures: *) 80val texSigs = "texsigsigs.tex" 81 82(* Signatures not to be included in the help database: *) 83val stoplist = []; 84 85(* The background colour in generated HTML files (HTML colour code): *) 86val bgcolor = "#fbf2e7"; 87 88(* To make the database, sort entries on normalized (lower case) name, 89 * lump together equal normalized names in entry lists, and sort these by 90 * structure name (except that a Str entry always precedes the others): 91 *) 92 93fun mkbase (entries : Database.entry list) = 94 let open Database 95 fun compname (e1, e2) = keycompare (getname e1, getname e2) 96 val entries = Listsort.sort compname entries 97 infix THEN 98 fun (comp1 THEN comp2) arg = 99 case comp1 arg of 100 EQUAL => comp2 arg 101 | res => res 102 fun kindof Str = "structure" 103 | kindof (Val _) = "val" 104 | kindof (Typ _) = "type" 105 | kindof (Exc _) = "exn" 106 | kindof (Con _) = "con" 107 | kindof (Term (_, NONE)) = "" 108 | kindof (Term (_, SOME kind)) = kind 109 fun kindCompare (e1 as {comp=c1, ...}, e2 as {comp=c2, ...}) = 110 String.compare(kindof c1, kindof c2) 111 fun nameCompare (e1, e2) = 112 String.compare(getname e1, getname e2) 113 fun fileCompare (e1, e2) = String.compare(#file e1, #file e2) 114 val entryCompare = kindCompare THEN nameCompare THEN fileCompare 115 (* Share strings if result=argument: *) 116 fun toLower s = 117 let val s' = String.map Char.toLower s 118 in if s=s' then s else s' end 119 (* Lump together names that differ only in capitalization; 120 then sort each lump using entryCompare *) 121 fun lump [] = [] 122 | lump (x1 :: xr) = 123 let fun mkLump lumpname lump = (toLower (getname lumpname), 124 Listsort.sort entryCompare lump) 125 fun h lump1name lump1 [] = [mkLump lump1name lump1] 126 | h lump1name lump1 (x1::xr) = 127 if compname(x1, lump1name) = EQUAL then 128 h lump1name (x1 :: lump1) xr 129 else 130 mkLump lump1name lump1 :: h x1 [x1] xr 131 in h x1 [x1] xr end 132 val lumps = lump entries : (string * entry list) list 133 fun mkOrderedTree xs = 134 let fun h 0 xs = (Empty, xs) 135 | h n xs = 136 let val m = n div 2 137 val (t1, l) = h m xs 138 val (key, value) = hd l 139 val yr = tl l 140 val (t2, zs) = h (n-m-1) yr 141 in (Node(key, value, t1, t2), zs) end 142 in #1 (h (length xs) xs) end 143 in 144 mkOrderedTree lumps 145 end 146 147(*---------------------------------------------------------------------------*) 148(* Additional stuff specific to HOL. *) 149(*---------------------------------------------------------------------------*) 150 151fun mk_HOLdocfile_entry (dir,s) = 152 let val content =String.substring(s,0,size s - 4) 153 in 154 {comp=Database.Term(Symbolic.tosymb content, SOME"HOL"), 155 file=normPath[dir,s], line=0} 156 end 157 158local fun is_adocfile s = 159 String.size s>5 andalso 160 String.extract(s, String.size s - 4, NONE) = ".txt" 161 fun is_docfile s = 162 String.size s>4 andalso 163 String.extract(s, String.size s - 4, NONE) = ".doc" 164in 165fun docdir_to_entries path (endpath, entries) = 166 let val L1 = List.filter is_adocfile 167 (Htmlsigs.listDir (normPath [path, endpath])) 168 in List.foldl (fn (s,l) => mk_HOLdocfile_entry (endpath,s)::l) entries L1 169 end 170end; 171 172fun okay_sig s = 173 String.isSuffix ".sig" s 174 andalso not (Option.isSome (List.find (fn e => e = s) Keepers.exclude)) 175 176fun dirToBase (sigdir, docdirs, filename) = 177 let 178 val doc_entryl = List.foldl (docdir_to_entries HOLpath) [] docdirs 179 val ok_sigs = List.filter okay_sig (Htmlsigs.listDir sigdir) 180 val res = List.foldl (Parsspec.processfile stoplist sigdir) 181 doc_entryl ok_sigs 182 val _ = print ("\nProcessed " ^ Int.toString (length res) 183 ^ " entries in total.\n"); 184 val _ = print ("Building database...\n"); 185 val db = mkbase res 186 val _ = print ("Writing database to file " ^ filename ^ "\n"); 187 in 188 Database.writebase(filename, db) 189 end 190 handle exn as OS.SysErr (str, _) => (print(str ^ "\n\n"); raise exn) 191 192fun main () = let 193 194val docdirs = 195 let val instr = TextIO.openIn 196 (OS.Path.concat(HOLpath,"tools/documentation-directories")) 197 handle _ => (print "Couldn't open documentation directories file"; 198 raise Fail "File not found") 199 val wholefile = TextIO.inputAll instr 200 val _ = TextIO.closeIn instr 201 in 202 map (normPath o single) (String.tokens Char.isSpace wholefile) 203 end 204 205val SRCFILES = 206 let open TextIO 207 val istrm = openIn (OS.Path.concat(HOLpath,"sigobj/SRCFILES")) 208 handle _ => (print "Couldn't open HOLDIR/sigobj/SRCFILES"; 209 raise Fail "File not found") 210 fun readlines acc = 211 case inputLine istrm of 212 NONE => List.rev acc 213 | SOME s => readlines (String.substring(s, 0, size s - 1) :: acc) 214 (* drop final newline *) 215 val wholefile = readlines [] before closeIn istrm 216 fun munge path = 217 let val {dir,file} = OS.Path.splitDirFile path 218 in case destProperSuffix "Theory" file 219 of SOME thy => (file, OS.Path.concat(dir,thy^"Script.sml")) 220 | NONE => (file,path^".sml") 221 end 222 in 223 map (munge o normPath o single) wholefile 224 end 225 226fun process (libdir, helpfile, txtIndex, 227 texIndex, htmldir, htmlIndex, htmlTheoryIndex, HOLpage) 228 = 229 (print ("Reading signatures in directory " ^ libdir ^ 230 "\nand writing help database in file " ^ helpfile ^ "\n") 231 ; dirToBase (libdir, docdirs, helpfile) 232 233 ; print ("\nWriting ASCII signature index in file " ^ txtIndex ^ "\n") 234 ; Printbase.printASCIIBase(helpfile, txtIndex) 235 236 ; print ("\nWriting Latex signature index in file " ^ texIndex ^ "\n") 237 ; Printbase.printLatexBase(helpfile, texIndex) 238 239 ; print ("\nCreating HTML versions of signature files\n") 240 ; Htmlsigs.sigsToHtml 241 version bgcolor stoplist helpfile HOLpath SRCFILES (libdir, htmldir) 242 243 ; print ("\nWriting HTML signature index in file " ^ htmlIndex ^ "\n") 244 ; Htmlsigs.printHTMLBase version bgcolor HOLpath 245 isSigId "HOL IDENTIFIER INDEX" (helpfile, htmlIndex) 246 247 ; print ("\nWriting HTML theory signature index in file " 248 ^ htmlTheoryIndex ^ "\n") 249 ; Htmlsigs.printHTMLBase version bgcolor HOLpath 250 isTheory "HOL THEORY BINDINGS" (helpfile, htmlTheoryIndex) 251 252 ; print ("\nWriting HOLPage\n") 253 ; HOLPage.printHOLPage version bgcolor HOLpath 254 htmlIndex htmlTheoryIndex (helpfile, HOLpage) 255 ) 256 257in 258 case CommandLine.arguments () of 259 [] => 260 process (libdirDef, helpfileDef, 261 txtIndexDef, texIndexDef, 262 htmlDirDef, htmlIndexDef, 263 htmlTheoryIndexDef, HOLpageDef) 264 | [libdir] => 265 process (libdir, helpfileDef, 266 txtIndexDef, texIndexDef, 267 htmlDirDef, htmlIndexDef, 268 htmlTheoryIndexDef, HOLpageDef) 269 | _ => print "Usage: makebase\n" 270end (* main *) 271 272end; 273