src/Pure/Thy/thy_load.ML
author wenzelm
Sun, 21 Jan 2007 16:43:44 +0100
changeset 22145 fedad292f738
parent 21950 e97fd6480091
child 23872 f449381e2caa
permissions -rw-r--r--
moved File.use to ML_Context.use;
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
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15570
diff changeset
     5
Theory loader primitives, including load path.
6168
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
10252
dd46544e259d added path_add;
wenzelm
parents: 9696
diff changeset
    12
  val path_add: string -> unit
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    13
  val del_path: string -> unit
7438
2e0e4253b6c3 with_path;
wenzelm
parents: 7190
diff changeset
    14
  val with_path: string -> ('a -> 'b) -> 'a -> 'b
9103
ef56f093259d added with_paths;
wenzelm
parents: 8808
diff changeset
    15
  val with_paths: string list -> ('a -> 'b) -> 'a -> 'b
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    16
  val reset_path: unit -> unit
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    17
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    18
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    19
signature THY_LOAD =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    20
sig
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    21
  include BASIC_THY_LOAD
17366
325707c676e2 export ml_exts;
wenzelm
parents: 16269
diff changeset
    22
  val ml_exts: string list
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    23
  val ml_path: string -> Path.T
7901
c21c3d2256ef export thy_path;
wenzelm
parents: 7438
diff changeset
    24
  val thy_path: string -> Path.T
15157
faeb23489b73 Function check_file now takes optional path (current directory) as an argument.
berghofe
parents: 14981
diff changeset
    25
  val check_file: Path.T option -> Path.T -> (Path.T * File.info) option
faeb23489b73 Function check_file now takes optional path (current directory) as an argument.
berghofe
parents: 14981
diff changeset
    26
  val load_file: Path.T option -> Path.T -> (Path.T * File.info)
7190
ba6f09cd7769 simplified handling of ML file;
wenzelm
parents: 6978
diff changeset
    27
  eqtype master
ba6f09cd7769 simplified handling of ML file;
wenzelm
parents: 6978
diff changeset
    28
  val get_thy: master -> Path.T * File.info
7940
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
    29
  val check_thy: Path.T -> string -> bool -> master
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
    30
  val deps_thy: Path.T -> string -> bool -> master * (string list * Path.T list)
7190
ba6f09cd7769 simplified handling of ML file;
wenzelm
parents: 6978
diff changeset
    31
  val load_thy: Path.T -> string -> bool -> bool -> master
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    32
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    33
7940
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
    34
(*this backdoor sealed later*)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    35
signature PRIVATE_THY_LOAD =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    36
sig
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    37
  include THY_LOAD
7940
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
    38
  val deps_thy_fn: (string -> bool -> Path.T -> string list * Path.T list) ref
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    39
  val load_thy_fn: (string -> bool -> bool -> Path.T -> unit) ref
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    40
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    41
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    42
structure ThyLoad: PRIVATE_THY_LOAD =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    43
struct
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    44
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    45
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    46
(* maintain load path *)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    47
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    48
val load_path = ref [Path.current];
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    49
fun change_path f = load_path := f (! load_path);
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    50
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 17366
diff changeset
    51
fun show_path () = map Path.implode (! load_path);
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 17366
diff changeset
    52
fun del_path s = change_path (filter_out (equal (Path.explode s)));
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 17366
diff changeset
    53
fun add_path s = (del_path s; change_path (cons (Path.explode s)));
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 17366
diff changeset
    54
fun path_add s = (del_path s; change_path (fn path => path @ [Path.explode s]));
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    55
fun reset_path () = load_path := [Path.current];
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 17366
diff changeset
    56
fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.explode ss) f x;
9655
a4d2da014ec3 renamed cond_with_path to cond_add_path (add to front);
wenzelm
parents: 9103
diff changeset
    57
fun with_path s f x = with_paths [s] f x;
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    58
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    59
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    60
(* file formats *)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    61
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    62
val ml_exts = ["", "ML", "sml"];
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    63
val ml_path = Path.ext "ML" o Path.basic;
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    64
val thy_path = Path.ext "thy" o Path.basic;
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    65
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    66
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    67
(* check_file *)
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    68
15157
faeb23489b73 Function check_file now takes optional path (current directory) as an argument.
berghofe
parents: 14981
diff changeset
    69
fun check_file current src_path =
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    70
  let
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    71
    val path = Path.expand src_path;
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    72
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    73
    fun find_ext rel_path ext =
8750
36b165788421 check_file: keep expanded (!) absolute path;
wenzelm
parents: 7950
diff changeset
    74
      let val ext_path = Path.expand (Path.ext ext rel_path)
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
    75
      in Option.map (fn info => (File.full_path ext_path, info)) (File.info ext_path) end;
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    76
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    77
    fun find_dir dir =
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    78
      get_first (find_ext (Path.append dir path)) ml_exts;
13533
70de987e9fe3 check_file: disallow current dir (typically "");
wenzelm
parents: 12120
diff changeset
    79
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15157
diff changeset
    80
    fun add_current ps = (case current of NONE => ps
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15157
diff changeset
    81
          | (SOME p) => if Path.is_current p then ps else p :: ps);
15157
faeb23489b73 Function check_file now takes optional path (current directory) as an argument.
berghofe
parents: 14981
diff changeset
    82
13533
70de987e9fe3 check_file: disallow current dir (typically "");
wenzelm
parents: 12120
diff changeset
    83
    val paths =
70de987e9fe3 check_file: disallow current dir (typically "");
wenzelm
parents: 12120
diff changeset
    84
      if Path.is_current path then error "Bad file specification"
15157
faeb23489b73 Function check_file now takes optional path (current directory) as an argument.
berghofe
parents: 14981
diff changeset
    85
      else if Path.is_basic path then add_current (! load_path)
faeb23489b73 Function check_file now takes optional path (current directory) as an argument.
berghofe
parents: 14981
diff changeset
    86
      else add_current [Path.current];
13533
70de987e9fe3 check_file: disallow current dir (typically "");
wenzelm
parents: 12120
diff changeset
    87
  in get_first find_dir paths end;
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    88
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
    89
7940
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
    90
(* load_file *)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    91
15157
faeb23489b73 Function check_file now takes optional path (current directory) as an argument.
berghofe
parents: 14981
diff changeset
    92
fun load_file current raw_path =
faeb23489b73 Function check_file now takes optional path (current directory) as an argument.
berghofe
parents: 14981
diff changeset
    93
  (case check_file current raw_path of
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 17366
diff changeset
    94
    NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
22145
fedad292f738 moved File.use to ML_Context.use;
wenzelm
parents: 21950
diff changeset
    95
  | SOME (path, info) => (ML_Context.use path; (path, info)));
7190
ba6f09cd7769 simplified handling of ML file;
wenzelm
parents: 6978
diff changeset
    96
ba6f09cd7769 simplified handling of ML file;
wenzelm
parents: 6978
diff changeset
    97
ba6f09cd7769 simplified handling of ML file;
wenzelm
parents: 6978
diff changeset
    98
(* datatype master *)
ba6f09cd7769 simplified handling of ML file;
wenzelm
parents: 6978
diff changeset
    99
ba6f09cd7769 simplified handling of ML file;
wenzelm
parents: 6978
diff changeset
   100
datatype master = Master of (Path.T * File.info) * (Path.T * File.info) option;
ba6f09cd7769 simplified handling of ML file;
wenzelm
parents: 6978
diff changeset
   101
ba6f09cd7769 simplified handling of ML file;
wenzelm
parents: 6978
diff changeset
   102
fun get_thy (Master (thy, _)) = thy;
6232
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
   103
4336add1c251 include full paths in file info;
wenzelm
parents: 6219
diff changeset
   104
7940
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   105
(* check / process theory files *)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   106
7940
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   107
local
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   108
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   109
fun check_thy_aux (name, ml) =
16269
2c05a7f662a3 tuned msg;
wenzelm
parents: 15801
diff changeset
   110
  let val thy_file = thy_path name in
2c05a7f662a3 tuned msg;
wenzelm
parents: 15801
diff changeset
   111
    case check_file NONE thy_file of
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 17366
diff changeset
   112
      NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
16269
2c05a7f662a3 tuned msg;
wenzelm
parents: 15801
diff changeset
   113
        " in dir(s) " ^ commas_quote (show_path ()))
2c05a7f662a3 tuned msg;
wenzelm
parents: 15801
diff changeset
   114
    | SOME thy_info => (thy_info, if ml then check_file NONE (ml_path name) else NONE)
2c05a7f662a3 tuned msg;
wenzelm
parents: 15801
diff changeset
   115
  end;
7940
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   116
21950
e97fd6480091 removed obsolete cond_add_path;
wenzelm
parents: 21858
diff changeset
   117
fun cond_add_path path f x =
e97fd6480091 removed obsolete cond_add_path;
wenzelm
parents: 21858
diff changeset
   118
  if Path.is_current path then f x else Library.setmp load_path (path :: ! load_path) f x;
e97fd6480091 removed obsolete cond_add_path;
wenzelm
parents: 21858
diff changeset
   119
7940
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   120
in
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   121
9655
a4d2da014ec3 renamed cond_with_path to cond_add_path (add to front);
wenzelm
parents: 9103
diff changeset
   122
fun check_thy dir name ml = Master (cond_add_path dir check_thy_aux (name, ml));
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
   123
7940
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   124
fun process_thy dir f name ml =
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   125
  let val master as Master ((path, _), _) = check_thy dir name ml
9655
a4d2da014ec3 renamed cond_with_path to cond_add_path (add to front);
wenzelm
parents: 9103
diff changeset
   126
  in (master, cond_add_path dir f path) end;
7940
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   127
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   128
end;
6484
3f098b0ec683 use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents: 6363
diff changeset
   129
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   130
7940
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   131
(* deps_thy and load_thy *)
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   132
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   133
(*hooks for theory syntax dependent operations*)
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   134
fun undefined _ = raise Match;
7940
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   135
val deps_thy_fn = ref (undefined: string -> bool -> Path.T -> string list * Path.T list);
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
   136
val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit);
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   137
7940
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   138
fun deps_thy dir name ml = process_thy dir (! deps_thy_fn name ml) name ml;
def6db239934 improved ml handling;
wenzelm
parents: 7901
diff changeset
   139
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
   140
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   141
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   142
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   143
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   144
structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   145
open BasicThyLoad;