src/Pure/Thy/thy_load.ML
author wenzelm
Mon Jul 23 16:45:03 2007 +0200 (2007-07-23)
changeset 23935 2a4e42ec9a54
parent 23892 739707039b0d
child 23944 2ea068548a83
permissions -rw-r--r--
PrintMode.with_modes;
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@15801
     5
Theory loader primitives, including load path.
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@10252
    12
  val path_add: 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@17366
    22
  val ml_exts: string list
wenzelm@6205
    23
  val ml_path: string -> Path.T
wenzelm@7901
    24
  val thy_path: string -> Path.T
wenzelm@23885
    25
  val check_file: Path.T -> Path.T -> (Path.T * File.ident) option
wenzelm@23885
    26
  val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
wenzelm@23885
    27
  val check_thy: Path.T -> string -> bool -> (Path.T * File.ident) * (Path.T * File.ident) option
wenzelm@23885
    28
  val deps_thy: Path.T -> string -> bool ->
wenzelm@23872
    29
    ((Path.T * File.ident) * (Path.T * File.ident) option) * (string list * Path.T list)
wenzelm@23885
    30
  val load_ml: Path.T -> Path.T -> Path.T * File.ident
wenzelm@23885
    31
  val load_thy: Path.T -> string -> bool -> bool ->
wenzelm@23872
    32
    (Path.T * File.ident) * (Path.T * File.ident) option
wenzelm@6168
    33
end;
wenzelm@6168
    34
wenzelm@7940
    35
(*this backdoor sealed later*)
wenzelm@6168
    36
signature PRIVATE_THY_LOAD =
wenzelm@6168
    37
sig
wenzelm@6168
    38
  include THY_LOAD
wenzelm@23885
    39
  val load_thy_fn: (Path.T -> string -> bool -> bool ->
wenzelm@23872
    40
    (Path.T * File.ident) * (Path.T * File.ident) option) ref
wenzelm@6168
    41
end;
wenzelm@6168
    42
wenzelm@6168
    43
structure ThyLoad: PRIVATE_THY_LOAD =
wenzelm@6168
    44
struct
wenzelm@6168
    45
wenzelm@6168
    46
wenzelm@6232
    47
(* maintain load path *)
wenzelm@6168
    48
wenzelm@6168
    49
val load_path = ref [Path.current];
wenzelm@6168
    50
wenzelm@21858
    51
fun show_path () = map Path.implode (! load_path);
wenzelm@23872
    52
fun del_path s = change load_path (remove (op =) (Path.explode s));
wenzelm@23872
    53
fun add_path s = (del_path s; change load_path (cons (Path.explode s)));
wenzelm@23872
    54
fun path_add s = (del_path s; change load_path (fn path => path @ [Path.explode s]));
wenzelm@6205
    55
fun reset_path () = load_path := [Path.current];
wenzelm@21858
    56
fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.explode ss) f x;
wenzelm@9655
    57
fun with_path s f x = with_paths [s] f x;
wenzelm@6168
    58
wenzelm@6168
    59
wenzelm@6232
    60
(* file formats *)
wenzelm@6168
    61
wenzelm@23872
    62
val ml_exts = ["ML", "sml"];
wenzelm@6232
    63
val ml_path = Path.ext "ML" o Path.basic;
wenzelm@6232
    64
val thy_path = Path.ext "thy" o Path.basic;
wenzelm@6168
    65
wenzelm@6168
    66
wenzelm@23872
    67
(* check files *)
wenzelm@6232
    68
wenzelm@23892
    69
fun search_path dir path =
wenzelm@23892
    70
  distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
wenzelm@23892
    71
wenzelm@23885
    72
fun check_ext exts dir src_path =
wenzelm@6232
    73
  let
wenzelm@6232
    74
    val path = Path.expand src_path;
wenzelm@23872
    75
    val _ = Path.is_current path andalso error "Bad file specification";
wenzelm@6168
    76
wenzelm@23885
    77
    fun try_ext rel_path ext =
wenzelm@8750
    78
      let val ext_path = Path.expand (Path.ext ext rel_path)
wenzelm@23872
    79
      in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;
wenzelm@23885
    80
    fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
wenzelm@23892
    81
  in get_first try_prfx (search_path dir path) end;
wenzelm@6232
    82
wenzelm@23872
    83
val check_file = check_ext [];
wenzelm@23872
    84
val check_ml = check_ext ml_exts;
wenzelm@6168
    85
wenzelm@23885
    86
fun check_thy dir name ml =
wenzelm@23872
    87
  let val thy_file = thy_path name in
wenzelm@23885
    88
    (case check_file dir thy_file of
wenzelm@23872
    89
      NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
wenzelm@23892
    90
        " in " ^ commas_quote (map Path.implode (search_path dir thy_file)))
wenzelm@23885
    91
    | SOME thy_id => (thy_id, if ml then check_file dir (ml_path name) else NONE))
wenzelm@23872
    92
  end;
wenzelm@6232
    93
wenzelm@6232
    94
wenzelm@23872
    95
(* theory deps *)
wenzelm@7940
    96
wenzelm@23885
    97
fun deps_thy dir name ml =
wenzelm@23872
    98
  let
wenzelm@23885
    99
    val master as ((path, _), _) = check_thy dir name ml;
wenzelm@23872
   100
    val (name', imports, uses) =
wenzelm@23876
   101
      ThyHeader.read (Position.path path) (Source.of_string_limited (File.read path));
wenzelm@23872
   102
    val _ = name = name' orelse
wenzelm@23872
   103
      error ("Filename " ^ quote (Path.implode (Path.base path)) ^
wenzelm@23872
   104
        " does not agree with theory name " ^ quote name');
wenzelm@23872
   105
    val ml_file =
wenzelm@23885
   106
      if ml andalso is_some (check_file dir (ml_path name))
wenzelm@23872
   107
      then [ml_path name] else [];
wenzelm@23872
   108
  in (master, (imports, map (Path.explode o #1) uses @ ml_file)) end;
wenzelm@6484
   109
wenzelm@6168
   110
wenzelm@23872
   111
(* load files *)
wenzelm@6168
   112
wenzelm@23885
   113
fun load_ml dir raw_path =
wenzelm@23885
   114
  (case check_ml dir raw_path of
wenzelm@23872
   115
    NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
wenzelm@23872
   116
  | SOME (path, id) => (ML_Context.use path; (path, id)));
wenzelm@6168
   117
wenzelm@23872
   118
(*dependent on outer syntax*)
wenzelm@23885
   119
val load_thy_fn = ref (undefined: Path.T -> string -> bool -> bool ->
wenzelm@23872
   120
  (Path.T * File.ident) * (Path.T * File.ident) option);
wenzelm@23885
   121
fun load_thy dir name ml time = ! load_thy_fn dir name ml time;
wenzelm@6168
   122
wenzelm@6168
   123
end;
wenzelm@6168
   124
wenzelm@6168
   125
structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
wenzelm@6168
   126
open BasicThyLoad;