src/Pure/Thy/thy_load.ML
author wenzelm
Wed, 03 Feb 1999 20:25:53 +0100
changeset 6219 b360065c2b07
parent 6205 dd3d3da0f458
child 6232 4336add1c251
permissions -rw-r--r--
check_thy: include ML stamp;
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
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    20
  val find_file: Path.T -> (Path.T * File.info) option
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    21
  val check_file: Path.T -> File.info option
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    22
  val load_file: Path.T -> File.info
6219
b360065c2b07 check_thy: include ML stamp;
wenzelm
parents: 6205
diff changeset
    23
  val check_thy: string -> bool -> File.info
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    24
  val deps_thy: string -> bool -> File.info * (string list * Path.T list)
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    25
  val load_thy: string -> bool -> bool -> File.info
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    26
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    27
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    28
signature PRIVATE_THY_LOAD =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    29
sig
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    30
  include THY_LOAD
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    31
  val deps_thy_fn: (string -> bool -> Path.T -> string list * Path.T list) ref
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    32
  val load_thy_fn: (string -> bool -> bool -> Path.T -> unit) ref
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    33
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    34
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    35
structure ThyLoad: PRIVATE_THY_LOAD =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    36
struct
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    37
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    38
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    39
(* load path *)
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    40
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    41
val load_path = ref [Path.current];
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    42
fun change_path f = load_path := f (! load_path);
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    43
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    44
fun show_path () = map Path.pack (! load_path);
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    45
fun add_path s = change_path (fn path => path @ [Path.unpack s]);
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    46
fun del_path s = change_path (filter_out (equal (Path.unpack s)));
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    47
fun reset_path () = load_path := [Path.current];
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    48
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    49
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    50
(* find / check file *)
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    51
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    52
fun find_file file_src =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    53
  let
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    54
    val file = Path.expand file_src;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    55
    fun find dir =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    56
      let val full_path = Path.append dir file
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    57
      in apsome (pair full_path) (File.info full_path) end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    58
  in get_first find (if Path.is_basic file then ! load_path else [Path.current]) end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    59
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    60
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    61
(* process ML files *)
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    62
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    63
val check_file = apsome #2 o find_file;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    64
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    65
fun load_file raw_path =
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    66
  (case find_file raw_path of
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    67
    Some (path, info) => (Use.use_path path; info)
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    68
  | None => error ("Could not find ML file " ^ quote (Path.pack raw_path)));
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    69
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    70
val ml_path = Path.ext "ML" o Path.basic;
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    71
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    72
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    73
(* process theory files *)
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    74
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    75
val thy_ext = Path.ext "thy";
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    76
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    77
fun process_thy f name =
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    78
  let val path = thy_ext (Path.basic name) in
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    79
    (case find_file path of
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    80
      Some (path, info) => (info, f path)
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    81
    | None => error ("Could not find theory file " ^ quote (Path.pack path)))
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    82
  end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    83
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    84
(*hooks for theory syntax dependent operations*)
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    85
fun undefined _ = raise Match;
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    86
val deps_thy_fn = ref (undefined: string -> bool -> Path.T -> string list * Path.T list);
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    87
val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit);
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    88
6219
b360065c2b07 check_thy: include ML stamp;
wenzelm
parents: 6205
diff changeset
    89
fun check_thy name ml =
b360065c2b07 check_thy: include ML stamp;
wenzelm
parents: 6205
diff changeset
    90
  let val (thy_info, _) = process_thy (K ()) name in
b360065c2b07 check_thy: include ML stamp;
wenzelm
parents: 6205
diff changeset
    91
    (case if ml then check_file (ml_path name) else None of
b360065c2b07 check_thy: include ML stamp;
wenzelm
parents: 6205
diff changeset
    92
      None => thy_info
b360065c2b07 check_thy: include ML stamp;
wenzelm
parents: 6205
diff changeset
    93
    | Some info => File.join_info thy_info info)
b360065c2b07 check_thy: include ML stamp;
wenzelm
parents: 6205
diff changeset
    94
  end;
b360065c2b07 check_thy: include ML stamp;
wenzelm
parents: 6205
diff changeset
    95
6205
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    96
fun deps_thy name ml = process_thy (fn path => ! deps_thy_fn name ml path) name;
dd3d3da0f458 added reset_path;
wenzelm
parents: 6168
diff changeset
    97
fun load_thy name ml time = #1 (process_thy (fn path => ! load_thy_fn name ml time path) name);
6168
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    98
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
    99
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   100
end;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   101
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   102
structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
9d5b74068bf9 Theory loader primitives.
wenzelm
parents:
diff changeset
   103
open BasicThyLoad;