src/Pure/Thy/thy_load.ML
author wenzelm
Sat Jan 30 10:42:40 1999 +0100 (1999-01-30 ago)
changeset 6168 9d5b74068bf9
child 6205 dd3d3da0f458
permissions -rw-r--r--
Theory loader primitives.
wenzelm@6168
     1
(*  Title:      Pure/Thy/thy_load.ML
wenzelm@6168
     2
    ID:         $Id$
wenzelm@6168
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6168
     4
wenzelm@6168
     5
Theory loader primitives.
wenzelm@6168
     6
*)
wenzelm@6168
     7
wenzelm@6168
     8
signature BASIC_THY_LOAD =
wenzelm@6168
     9
sig
wenzelm@6168
    10
  val show_path: unit -> string list
wenzelm@6168
    11
  val add_path: string -> unit
wenzelm@6168
    12
  val del_path: string -> unit
wenzelm@6168
    13
end;
wenzelm@6168
    14
wenzelm@6168
    15
signature THY_LOAD =
wenzelm@6168
    16
sig
wenzelm@6168
    17
  include BASIC_THY_LOAD
wenzelm@6168
    18
  val thy_ext: string
wenzelm@6168
    19
  val find_file: Path.T -> (Path.T * File.info) option
wenzelm@6168
    20
  val check_file: Path.T -> File.info option
wenzelm@6168
    21
  val load_file: Path.T -> File.info
wenzelm@6168
    22
  val check_thy: string -> File.info
wenzelm@6168
    23
  val deps_thy: string -> File.info * (string list * Path.T list)
wenzelm@6168
    24
  val load_thy: string -> File.info * theory
wenzelm@6168
    25
end;
wenzelm@6168
    26
wenzelm@6168
    27
signature PRIVATE_THY_LOAD =
wenzelm@6168
    28
sig
wenzelm@6168
    29
  include THY_LOAD
wenzelm@6168
    30
  val deps_thy_fn: (Path.T -> string list * Path.T list) ref
wenzelm@6168
    31
  val load_thy_fn: (Path.T -> theory) ref
wenzelm@6168
    32
end;
wenzelm@6168
    33
wenzelm@6168
    34
structure ThyLoad: PRIVATE_THY_LOAD =
wenzelm@6168
    35
struct
wenzelm@6168
    36
wenzelm@6168
    37
wenzelm@6168
    38
(* load path *)
wenzelm@6168
    39
wenzelm@6168
    40
val load_path = ref [Path.current];
wenzelm@6168
    41
fun change_path f = load_path := f (! load_path);
wenzelm@6168
    42
wenzelm@6168
    43
fun show_path () = map Path.pack (! load_path);
wenzelm@6168
    44
fun add_path s = change_path (fn path => path @ [Path.unpack s]);
wenzelm@6168
    45
fun del_path s = change_path (filter_out (equal (Path.unpack s)));
wenzelm@6168
    46
wenzelm@6168
    47
wenzelm@6168
    48
(* find / check file *)
wenzelm@6168
    49
wenzelm@6168
    50
fun find_file file_src =
wenzelm@6168
    51
  let
wenzelm@6168
    52
    val file = Path.expand file_src;
wenzelm@6168
    53
    fun find dir =
wenzelm@6168
    54
      let val full_path = Path.append dir file
wenzelm@6168
    55
      in apsome (pair full_path) (File.info full_path) end;
wenzelm@6168
    56
  in get_first find (if Path.is_basic file then ! load_path else [Path.current]) end;
wenzelm@6168
    57
wenzelm@6168
    58
wenzelm@6168
    59
(* process ML files *)
wenzelm@6168
    60
wenzelm@6168
    61
val check_file = apsome #2 o find_file;
wenzelm@6168
    62
wenzelm@6168
    63
fun load_file raw_path =
wenzelm@6168
    64
  (case find_file raw_path of
wenzelm@6168
    65
    Some (path, info) => (Use.use_path path; info)
wenzelm@6168
    66
  | None => error ("Could not find ML file " ^ quote (Path.pack raw_path)));
wenzelm@6168
    67
wenzelm@6168
    68
wenzelm@6168
    69
(* process theory files *)
wenzelm@6168
    70
wenzelm@6168
    71
val thy_ext = "thy";
wenzelm@6168
    72
wenzelm@6168
    73
fun process_thy f name =
wenzelm@6168
    74
  let val path = Path.ext thy_ext (Path.basic name) in
wenzelm@6168
    75
    (case find_file path of
wenzelm@6168
    76
      Some (path, info) => (info, f path)
wenzelm@6168
    77
    | None => error ("Could not find theory file " ^ quote (Path.pack path)))
wenzelm@6168
    78
  end;
wenzelm@6168
    79
wenzelm@6168
    80
(*hooks for theory syntax dependent operations*)
wenzelm@6168
    81
fun undefined _ = raise Match;
wenzelm@6168
    82
val deps_thy_fn = ref (undefined: Path.T -> string list * Path.T list);
wenzelm@6168
    83
val load_thy_fn = ref (undefined: Path.T -> theory);
wenzelm@6168
    84
wenzelm@6168
    85
val check_thy = #1 o process_thy (K ());
wenzelm@6168
    86
val deps_thy = process_thy (fn path => ! deps_thy_fn path);
wenzelm@6168
    87
val load_thy = process_thy (fn path => ! load_thy_fn path);
wenzelm@6168
    88
wenzelm@6168
    89
wenzelm@6168
    90
end;
wenzelm@6168
    91
wenzelm@6168
    92
structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
wenzelm@6168
    93
open BasicThyLoad;