src/Pure/Thy/read.ML
author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 74 208ab8773a73
permissions -rw-r--r--
Initial revision
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/read
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Sonia Mahjoub / Tobias Nipkow / L C Paulson
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  TU Muenchen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Reading and writing the theory definition files.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
For theory XXX, the  input file is called XXX.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
                the output file is called .XXX.thy.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
                and it then tries to read XXX.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
signature READTHY =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  val split_filename : string -> string * string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  val time_use_thy   : string -> unit
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
  val use_thy        : string -> unit
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
functor ReadthyFUN (ThySyn: THYSYN): READTHY =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
(*Convert Unix filename of the form path/file to "path/" and "file" ;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  if filename contains no slash, then it returns "" and "file" *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
fun split_filename name =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  let val (file,path) = take_prefix (apr(op<>,"/")) (rev (explode name))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  in  (implode(rev path), implode(rev file)) end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
(*create name of the output ML file for the theory*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
fun out_name thy = "." ^ thy ^ ".thy.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
fun read_thy path thy =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
    let val instream  = open_in (path ^ thy ^ ".thy")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
        val outstream = open_out (path ^ out_name thy)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
    in  output (outstream, ThySyn.read (explode(input(instream, 999999))));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
        close_out outstream;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
        close_in instream
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
fun file_exists file =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
  let val instream = open_in file in close_in instream; true end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
    handle Io _ => false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
(*Use the file if it exists*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
fun try_use file =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
  if file_exists file then use file else ();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
(*Read and convert the theory to a .XXX.thy.ML file and also try to read XXX.ML*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
fun use_thy name =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
    let val (path,thy) = split_filename name
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
    in  read_thy path thy;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
        use (path ^ out_name thy);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
        try_use (path ^ thy ^ ".ML")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
    end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
fun time_use_thy tname = timeit(fn()=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
   (writeln("\n**** Starting Theory " ^ tname ^ " ****");  use_thy tname;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
    writeln("\n**** Finished Theory " ^ tname ^ " ****")));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
end;