src/Pure/Thy/thy_load.ML
author wenzelm
Sun Jul 23 12:10:11 2000 +0200 (2000-07-23)
changeset 9416 9144976964e7
parent 9103 ef56f093259d
child 9655 a4d2da014ec3
permissions -rw-r--r--
removed all_sessions.graph;
improved graph 'directories';
tuned;
wenzelm@6168
     1
(*  Title:      Pure/Thy/thy_load.ML
wenzelm@6168
     2
    ID:         $Id$
wenzelm@6168
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8808
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@6168
     5
wenzelm@6168
     6
Theory loader primitives.
wenzelm@6168
     7
*)
wenzelm@6168
     8
wenzelm@6168
     9
signature BASIC_THY_LOAD =
wenzelm@6168
    10
sig
wenzelm@6168
    11
  val show_path: unit -> string list
wenzelm@6168
    12
  val add_path: string -> unit
wenzelm@6168
    13
  val del_path: string -> unit
wenzelm@7438
    14
  val with_path: string -> ('a -> 'b) -> 'a -> 'b
wenzelm@9103
    15
  val with_paths: string list -> ('a -> 'b) -> 'a -> 'b
wenzelm@6205
    16
  val reset_path: unit -> unit
wenzelm@6168
    17
end;
wenzelm@6168
    18
wenzelm@6168
    19
signature THY_LOAD =
wenzelm@6168
    20
sig
wenzelm@6168
    21
  include BASIC_THY_LOAD
wenzelm@7950
    22
  val cond_with_path: Path.T -> ('a -> 'b) -> 'a -> 'b
wenzelm@6205
    23
  val ml_path: string -> Path.T
wenzelm@7901
    24
  val thy_path: string -> Path.T
wenzelm@6232
    25
  val check_file: Path.T -> (Path.T * File.info) option
wenzelm@7940
    26
  val load_file: Path.T -> (Path.T * File.info)
wenzelm@7190
    27
  eqtype master
wenzelm@7190
    28
  val get_thy: master -> Path.T * File.info
wenzelm@7940
    29
  val check_thy: Path.T -> string -> bool -> master
wenzelm@7940
    30
  val deps_thy: Path.T -> string -> bool -> master * (string list * Path.T list)
wenzelm@7190
    31
  val load_thy: Path.T -> string -> bool -> bool -> master
wenzelm@6168
    32
end;
wenzelm@6168
    33
wenzelm@7940
    34
(*this backdoor sealed later*)
wenzelm@6168
    35
signature PRIVATE_THY_LOAD =
wenzelm@6168
    36
sig
wenzelm@6168
    37
  include THY_LOAD
wenzelm@7940
    38
  val deps_thy_fn: (string -> bool -> Path.T -> string list * Path.T list) ref
wenzelm@6205
    39
  val load_thy_fn: (string -> bool -> bool -> Path.T -> unit) ref
wenzelm@6168
    40
end;
wenzelm@6168
    41
wenzelm@6168
    42
structure ThyLoad: PRIVATE_THY_LOAD =
wenzelm@6168
    43
struct
wenzelm@6168
    44
wenzelm@6168
    45
wenzelm@6232
    46
(* maintain load path *)
wenzelm@6168
    47
wenzelm@6168
    48
val load_path = ref [Path.current];
wenzelm@6168
    49
fun change_path f = load_path := f (! load_path);
wenzelm@6168
    50
wenzelm@6168
    51
fun show_path () = map Path.pack (! load_path);
wenzelm@6484
    52
fun add_path s = change_path (cons (Path.unpack s));
wenzelm@6168
    53
fun del_path s = change_path (filter_out (equal (Path.unpack s)));
wenzelm@6205
    54
fun reset_path () = load_path := [Path.current];
wenzelm@7438
    55
fun with_path s f x = Library.setmp load_path (Path.unpack s :: ! load_path) f x;
wenzelm@9103
    56
fun with_paths ss f x = Library.setmp load_path (map Path.unpack ss @ ! load_path) f x;
wenzelm@6168
    57
wenzelm@7438
    58
fun cond_with_path path f x =
wenzelm@7190
    59
  if Path.is_current path then f x else Library.setmp load_path (path :: ! load_path) f x;
wenzelm@7190
    60
wenzelm@6168
    61
wenzelm@6232
    62
(* file formats *)
wenzelm@6168
    63
wenzelm@6232
    64
val ml_exts = ["", "ML", "sml"];
wenzelm@6232
    65
val ml_path = Path.ext "ML" o Path.basic;
wenzelm@6232
    66
val thy_path = Path.ext "thy" o Path.basic;
wenzelm@6168
    67
wenzelm@6168
    68
wenzelm@6232
    69
(* check_file *)
wenzelm@6232
    70
wenzelm@6232
    71
fun check_file src_path =
wenzelm@6232
    72
  let
wenzelm@6232
    73
    val path = Path.expand src_path;
wenzelm@6168
    74
wenzelm@6232
    75
    fun find_ext rel_path ext =
wenzelm@8750
    76
      let val ext_path = Path.expand (Path.ext ext rel_path)
wenzelm@6232
    77
      in apsome (fn info => (File.full_path ext_path, info)) (File.info ext_path) end;
wenzelm@6232
    78
wenzelm@6232
    79
    fun find_dir dir =
wenzelm@6232
    80
      get_first (find_ext (Path.append dir path)) ml_exts;
wenzelm@6232
    81
  in get_first find_dir (if Path.is_basic path then ! load_path else [Path.current]) end;
wenzelm@6232
    82
wenzelm@6232
    83
wenzelm@7940
    84
(* load_file *)
wenzelm@6168
    85
wenzelm@7940
    86
fun load_file raw_path =
wenzelm@6232
    87
  (case check_file raw_path of
wenzelm@6232
    88
    None => error ("Could not find ML file " ^ quote (Path.pack raw_path))
wenzelm@7940
    89
  | Some (path, info) => (File.symbol_use path; (path, info)));
wenzelm@7190
    90
wenzelm@7190
    91
wenzelm@7190
    92
(* datatype master *)
wenzelm@7190
    93
wenzelm@7190
    94
datatype master = Master of (Path.T * File.info) * (Path.T * File.info) option;
wenzelm@7190
    95
wenzelm@7190
    96
fun get_thy (Master (thy, _)) = thy;
wenzelm@6232
    97
wenzelm@6232
    98
wenzelm@7940
    99
(* check / process theory files *)
wenzelm@6168
   100
wenzelm@7940
   101
local
wenzelm@7940
   102
wenzelm@7940
   103
fun check_thy_aux (name, ml) =
wenzelm@6232
   104
  (case check_file (thy_path name) of
wenzelm@6484
   105
    None => error ("Could not find theory file for " ^ quote name ^ " in dir(s) " ^
wenzelm@6484
   106
      commas_quote (show_path ()))
wenzelm@7940
   107
  | Some thy_info => (thy_info, if ml then check_file (ml_path name) else None));
wenzelm@7940
   108
wenzelm@7940
   109
in
wenzelm@7940
   110
wenzelm@7940
   111
fun check_thy dir name ml = Master (cond_with_path dir check_thy_aux (name, ml));
wenzelm@6205
   112
wenzelm@7940
   113
fun process_thy dir f name ml =
wenzelm@7940
   114
  let val master as Master ((path, _), _) = check_thy dir name ml
wenzelm@7940
   115
  in (master, cond_with_path dir f path) end;
wenzelm@7940
   116
wenzelm@7940
   117
end;
wenzelm@6484
   118
wenzelm@6168
   119
wenzelm@7940
   120
(* deps_thy and load_thy *)
wenzelm@6168
   121
wenzelm@6168
   122
(*hooks for theory syntax dependent operations*)
wenzelm@6168
   123
fun undefined _ = raise Match;
wenzelm@7940
   124
val deps_thy_fn = ref (undefined: string -> bool -> Path.T -> string list * Path.T list);
wenzelm@6205
   125
val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit);
wenzelm@6168
   126
wenzelm@7940
   127
fun deps_thy dir name ml = process_thy dir (! deps_thy_fn name ml) name ml;
wenzelm@7940
   128
fun load_thy dir name ml time = #1 (process_thy dir (! load_thy_fn name ml time) name ml);
wenzelm@6168
   129
wenzelm@6168
   130
wenzelm@6168
   131
end;
wenzelm@6168
   132
wenzelm@6168
   133
structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
wenzelm@6168
   134
open BasicThyLoad;