src/Pure/Thy/thy_load.ML
author wenzelm
Tue, 27 Oct 2009 13:15:04 +0100
changeset 33221 5bb809208876
parent 32966 5b21661fe618
child 37216 3165bc303f66
permissions -rw-r--r--
tuned;
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
    Author:     Markus Wenzel, TU Muenchen
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     3
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15570
diff changeset
     4
Theory loader primitives, including load path.
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     5
*)
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     6
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     7
signature BASIC_THY_LOAD =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     8
sig
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
     9
  val show_path: unit -> string list
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    10
  val add_path: string -> unit
10252
dd46544e259d added path_add;
wenzelm
parents: 9696
diff changeset
    11
  val path_add: string -> unit
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    12
  val del_path: string -> unit
7438
2e0e4253b6c3 with_path;
wenzelm
parents: 7190
diff changeset
    13
  val with_path: string -> ('a -> 'b) -> 'a -> 'b
9103
ef56f093259d added with_paths;
wenzelm
parents: 8808
diff changeset
    14
  val with_paths: string list -> ('a -> 'b) -> 'a -> 'b
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    15
  val reset_path: unit -> unit
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    16
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    17
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    18
signature THY_LOAD =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    19
sig
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    20
  include BASIC_THY_LOAD
17366
325707c676e2 export ml_exts;
wenzelm
parents: 16269
diff changeset
    21
  val ml_exts: string list
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    22
  val ml_path: string -> Path.T
7901
c21c3d2256ef export thy_path;
wenzelm
parents: 7438
diff changeset
    23
  val thy_path: string -> Path.T
29418
d584715a3ebb added split_thy_path;
wenzelm
parents: 26881
diff changeset
    24
  val split_thy_path: Path.T -> Path.T * string
23885
09254a1622e3 simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents: 23876
diff changeset
    25
  val check_file: Path.T -> Path.T -> (Path.T * File.ident) option
09254a1622e3 simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents: 23876
diff changeset
    26
  val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
24189
1fa9852643a3 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents: 24065
diff changeset
    27
  val check_thy: Path.T -> string -> Path.T * File.ident
29515
53bda11e0d3b export check_name;
wenzelm
parents: 29418
diff changeset
    28
  val check_name: string -> string -> unit
24189
1fa9852643a3 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents: 24065
diff changeset
    29
  val deps_thy: Path.T -> string ->
1fa9852643a3 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents: 24065
diff changeset
    30
   {master: Path.T * File.ident, text: string list, imports: string list, uses: Path.T list}
23885
09254a1622e3 simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents: 23876
diff changeset
    31
  val load_ml: Path.T -> Path.T -> Path.T * File.ident
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    32
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    33
26616
b5fd3ad271ec eliminated backpatching of load_thy;
wenzelm
parents: 26455
diff changeset
    34
structure ThyLoad: THY_LOAD =
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    35
struct
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    36
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    37
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    38
(* maintain load path *)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    39
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32466
diff changeset
    40
local val load_path = Unsynchronized.ref [Path.current] in
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    41
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 17366
diff changeset
    42
fun show_path () = map Path.implode (! load_path);
23944
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    43
33221
wenzelm
parents: 32966
diff changeset
    44
fun del_path s =
wenzelm
parents: 32966
diff changeset
    45
  CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s)));
wenzelm
parents: 32966
diff changeset
    46
wenzelm
parents: 32966
diff changeset
    47
fun add_path s =
wenzelm
parents: 32966
diff changeset
    48
  CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
wenzelm
parents: 32966
diff changeset
    49
wenzelm
parents: 32966
diff changeset
    50
fun path_add s =
wenzelm
parents: 32966
diff changeset
    51
  CRITICAL (fn () =>
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32466
diff changeset
    52
    (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
33221
wenzelm
parents: 32966
diff changeset
    53
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    54
fun reset_path () = load_path := [Path.current];
23944
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    55
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    56
fun with_paths ss f x =
33221
wenzelm
parents: 32966
diff changeset
    57
  CRITICAL (fn () =>
wenzelm
parents: 32966
diff changeset
    58
    setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x);
wenzelm
parents: 32966
diff changeset
    59
9655
a4d2da014ec3 renamed cond_with_path to cond_add_path (add to front);
wenzelm
parents: 9103
diff changeset
    60
fun with_path s f x = with_paths [s] f x;
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    61
23944
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    62
fun search_path dir path =
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    63
  distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    64
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    65
end;
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    66
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    67
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    68
(* file formats *)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    69
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
    70
val ml_exts = ["ML", "sml"];
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    71
val ml_path = Path.ext "ML" o Path.basic;
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    72
val thy_path = Path.ext "thy" o Path.basic;
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    73
29418
d584715a3ebb added split_thy_path;
wenzelm
parents: 26881
diff changeset
    74
fun split_thy_path path =
d584715a3ebb added split_thy_path;
wenzelm
parents: 26881
diff changeset
    75
  (case Path.split_ext path of
d584715a3ebb added split_thy_path;
wenzelm
parents: 26881
diff changeset
    76
    (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
d584715a3ebb added split_thy_path;
wenzelm
parents: 26881
diff changeset
    77
  | _ => error ("Bad theory file specification " ^ Path.implode path));
d584715a3ebb added split_thy_path;
wenzelm
parents: 26881
diff changeset
    78
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    79
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
    80
(* check files *)
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    81
32811
a692298ecbe0 eliminated redundant parameters;
wenzelm
parents: 32738
diff changeset
    82
fun check_ext exts paths src_path =
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    83
  let
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    84
    val path = Path.expand src_path;
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
    85
    val _ = Path.is_current path andalso error "Bad file specification";
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    86
23885
09254a1622e3 simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents: 23876
diff changeset
    87
    fun try_ext rel_path ext =
8750
36b165788421 check_file: keep expanded (!) absolute path;
wenzelm
parents: 7950
diff changeset
    88
      let val ext_path = Path.expand (Path.ext ext rel_path)
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
    89
      in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;
23885
09254a1622e3 simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents: 23876
diff changeset
    90
    fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
23944
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    91
  in get_first try_prfx paths end;
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    92
32811
a692298ecbe0 eliminated redundant parameters;
wenzelm
parents: 32738
diff changeset
    93
fun check_file dir path = check_ext [] (search_path dir path) path;
a692298ecbe0 eliminated redundant parameters;
wenzelm
parents: 32738
diff changeset
    94
fun check_ml dir path = check_ext ml_exts (search_path dir path) path;
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    95
24189
1fa9852643a3 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents: 24065
diff changeset
    96
fun check_thy dir name =
23944
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    97
  let
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    98
    val thy_file = thy_path name;
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
    99
    val paths = search_path dir thy_file;
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
   100
  in
32811
a692298ecbe0 eliminated redundant parameters;
wenzelm
parents: 32738
diff changeset
   101
    (case check_ext [] paths thy_file of
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
   102
      NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
23944
2ea068548a83 marked some CRITICAL sections;
wenzelm
parents: 23892
diff changeset
   103
        " in " ^ commas_quote (map Path.implode paths))
24189
1fa9852643a3 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents: 24065
diff changeset
   104
    | SOME thy_id => thy_id)
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
   105
  end;
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
   106
29515
53bda11e0d3b export check_name;
wenzelm
parents: 29418
diff changeset
   107
fun check_name name name' =
53bda11e0d3b export check_name;
wenzelm
parents: 29418
diff changeset
   108
  if name = name' then ()
53bda11e0d3b export check_name;
wenzelm
parents: 29418
diff changeset
   109
  else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
53bda11e0d3b export check_name;
wenzelm
parents: 29418
diff changeset
   110
    " does not agree with theory name " ^ quote name');
53bda11e0d3b export check_name;
wenzelm
parents: 29418
diff changeset
   111
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
   112
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
   113
(* theory deps *)
7940
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   114
24189
1fa9852643a3 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents: 24065
diff changeset
   115
fun deps_thy dir name =
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
   116
  let
24189
1fa9852643a3 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents: 24065
diff changeset
   117
    val master as (path, _) = check_thy dir name;
24065
21483400c2ca load_thy: avoid reloading of text;
wenzelm
parents: 23944
diff changeset
   118
    val text = explode (File.read path);
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
   119
    val (name', imports, uses) =
32466
a393b7e2a2f8 modernized Thy_Header;
wenzelm
parents: 29515
diff changeset
   120
      Thy_Header.read (Path.position path) (Source.of_list_limited 8000 text);
29515
53bda11e0d3b export check_name;
wenzelm
parents: 29418
diff changeset
   121
    val _ = check_name name name';
24189
1fa9852643a3 simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents: 24065
diff changeset
   122
    val uses = map (Path.explode o #1) uses;
24065
21483400c2ca load_thy: avoid reloading of text;
wenzelm
parents: 23944
diff changeset
   123
  in {master = master, text = text, imports = imports, uses = uses} end;
6484
3f098b0ec683 use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents: 6363
diff changeset
   124
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   125
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
   126
(* load files *)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   127
23885
09254a1622e3 simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents: 23876
diff changeset
   128
fun load_ml dir raw_path =
09254a1622e3 simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents: 23876
diff changeset
   129
  (case check_ml dir raw_path of
23872
f449381e2caa tuned signature;
wenzelm
parents: 22145
diff changeset
   130
    NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
26455
1757a6e049f4 reorganized signature of ML_Context;
wenzelm
parents: 24189
diff changeset
   131
  | SOME (path, id) => (ML_Context.eval_file path; (path, id)));
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   132
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   133
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   134
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32466
diff changeset
   135
structure Basic_Thy_Load: BASIC_THY_LOAD = ThyLoad;
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32466
diff changeset
   136
open Basic_Thy_Load;