src/Pure/Thy/thy_load.ML
author wenzelm
Mon, 12 Jul 1999 22:23:59 +0200
changeset 6978 a5b67157b94d
parent 6641 254ab03bd082
child 7190 ba6f09cd7769
permissions -rw-r--r--
tmp_path: *add* path;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/thy_load.ML
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     4
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     5
Theory loader primitives.
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     6
*)
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     7
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     8
signature BASIC_THY_LOAD =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     9
sig
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    10
  val show_path: unit -> string list
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    11
  val add_path: string -> unit
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    12
  val del_path: string -> unit
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    13
  val reset_path: unit -> unit
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    14
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    15
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    16
signature THY_LOAD =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    17
sig
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    18
  include BASIC_THY_LOAD
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    19
  val ml_path: string -> Path.T
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    20
  val check_file: Path.T -> (Path.T * File.info) option
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    21
  val load_file: Path.T -> (Path.T * File.info)
6487
453901eb3412 improved auto dir handling;
wenzelm
parents: 6484
diff changeset
    22
  val check_thy: Path.T -> string -> bool -> (Path.T * File.info) list
453901eb3412 improved auto dir handling;
wenzelm
parents: 6484
diff changeset
    23
  val deps_thy: Path.T -> string -> bool ->
6484
3f098b0ec683 use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents: 6363
diff changeset
    24
    (Path.T * File.info) list * (string list * Path.T list)
6487
453901eb3412 improved auto dir handling;
wenzelm
parents: 6484
diff changeset
    25
  val load_thy: Path.T -> string -> bool -> bool -> (Path.T * File.info) list
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    26
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    27
6363
c784ab29f424 comment;
wenzelm
parents: 6232
diff changeset
    28
(*backdoor sealed later*)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    29
signature PRIVATE_THY_LOAD =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    30
sig
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    31
  include THY_LOAD
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    32
  val deps_thy_fn: (string -> bool -> Path.T -> string list * Path.T list) ref
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    33
  val load_thy_fn: (string -> bool -> bool -> Path.T -> unit) ref
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    34
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    35
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    36
structure ThyLoad: PRIVATE_THY_LOAD =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    37
struct
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    38
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    39
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    40
(* maintain load path *)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    41
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    42
val load_path = ref [Path.current];
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    43
fun change_path f = load_path := f (! load_path);
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    44
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    45
fun show_path () = map Path.pack (! load_path);
6484
3f098b0ec683 use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents: 6363
diff changeset
    46
fun add_path s = change_path (cons (Path.unpack s));
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    47
fun del_path s = change_path (filter_out (equal (Path.unpack s)));
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    48
fun reset_path () = load_path := [Path.current];
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    49
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    50
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    51
(* file formats *)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    52
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    53
val ml_exts = ["", "ML", "sml"];
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    54
val ml_path = Path.ext "ML" o Path.basic;
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    55
val thy_path = Path.ext "thy" o Path.basic;
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    56
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    57
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    58
(* check_file *)
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    59
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    60
fun check_file src_path =
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    61
  let
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    62
    val path = Path.expand src_path;
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    63
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    64
    fun find_ext rel_path ext =
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    65
      let val ext_path = Path.ext ext rel_path
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    66
      in apsome (fn info => (File.full_path ext_path, info)) (File.info ext_path) end;
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    67
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    68
    fun find_dir dir =
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    69
      get_first (find_ext (Path.append dir path)) ml_exts;
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    70
  in get_first find_dir (if Path.is_basic path then ! load_path else [Path.current]) end;
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    71
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    72
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    73
(* load_file *)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    74
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    75
fun load_file raw_path =
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    76
  (case check_file raw_path of
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    77
    None => error ("Could not find ML file " ^ quote (Path.pack raw_path))
6641
254ab03bd082 rearranged some modules;
wenzelm
parents: 6487
diff changeset
    78
  | Some (path, info) => (File.symbol_use path; (path, info)));
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    79
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    80
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    81
(* check_thy *)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    82
6487
453901eb3412 improved auto dir handling;
wenzelm
parents: 6484
diff changeset
    83
fun tmp_path path f x =
6978
a5b67157b94d tmp_path: *add* path;
wenzelm
parents: 6641
diff changeset
    84
  if Path.is_current path then f x else Library.setmp load_path (path :: ! load_path) f x;
6484
3f098b0ec683 use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents: 6363
diff changeset
    85
3f098b0ec683 use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents: 6363
diff changeset
    86
fun check_thy_aux name ml =
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    87
  (case check_file (thy_path name) of
6484
3f098b0ec683 use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents: 6363
diff changeset
    88
    None => error ("Could not find theory file for " ^ quote name ^ " in dir(s) " ^
3f098b0ec683 use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents: 6363
diff changeset
    89
      commas_quote (show_path ()))
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    90
  | Some thy_info => thy_info ::
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    91
      (case if ml then check_file (ml_path name) else None of
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    92
        None => []
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    93
      | Some info => [info]));
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    94
6484
3f098b0ec683 use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents: 6363
diff changeset
    95
fun check_thy dir name ml = tmp_path dir (check_thy_aux name) ml;
3f098b0ec683 use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents: 6363
diff changeset
    96
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    97
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    98
(* process theory files *)
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    99
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   100
(*hooks for theory syntax dependent operations*)
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   101
fun undefined _ = raise Match;
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
   102
val deps_thy_fn = ref (undefined: string -> bool -> Path.T -> string list * Path.T list);
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
   103
val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit);
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   104
6484
3f098b0ec683 use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents: 6363
diff changeset
   105
fun process_thy dir f name ml =
3f098b0ec683 use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents: 6363
diff changeset
   106
  let val master = check_thy dir name ml
6487
453901eb3412 improved auto dir handling;
wenzelm
parents: 6484
diff changeset
   107
  in (master, tmp_path dir f (#1 (hd master))) end;
6219
b360065c2b07 check_thy: include ML stamp;
wenzelm
parents: 6205
diff changeset
   108
6484
3f098b0ec683 use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents: 6363
diff changeset
   109
fun deps_thy dir name ml = process_thy dir (! deps_thy_fn name ml) name ml;
3f098b0ec683 use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents: 6363
diff changeset
   110
fun load_thy dir name ml time = #1 (process_thy dir (! load_thy_fn name ml time) name ml);
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   111
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   112
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   113
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   114
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   115
structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   116
open BasicThyLoad;